On Thursday 23 December 2010 12:52:07 pm Daniel Peebles wrote:
Fair enough :) that'll teach me to hypothesize something without thinking about it! I guess I could amend my coinductive proof:
http://hpaste.org/paste/42516/mirrormirror_with_bottom#p42517
does that cover bottom-ness adequately? I can't say I've thought through it terribly carefully.
That isn't the usual way to model partially defined values. For instance, you can write functions with that datatype that would not be monotone: pdefined :: {A : Set} -> Tree A -> Bool pdefined ⊥ = false pdefined _ = true It's somewhat more accurate to take the partiality monad: data D (A : Set) : Set where now : A -> D A later : ∞ (D A) -> D A ⊥ : {A : Set} -> D A ⊥ = later (♯ ⊥) Then we're interested in an equivalence relation on D As where two values are equal if they either both diverge, or both converge to equal inhabitants of A (not worrying about how many steps each takes to do so). Then, the partially defined trees are given by: mutual {A} Tree = D Tree' data Tree' : Set where node : Tree -> A -> Tree -> Tree' tip : Tree' And equivalence of these trees makes use of the above equivalence for D- wrapped things. (It's actually a little weird that this works, I think, if you expect Tree' to be a least fixed point; but Agda does not work that way). If you're just interested in proving mirror (mirror x) = x, though, this is probably overkill. Your original type should be isomorphic to the Haskell type in a set theoretic way of thinking, and the definition of mirror does what the Haskell function would do at all the values. So the fact that you can write functions on that Agda type that would have no corresponding implementation in Haskell is kind of irrelevant. -- Dan