Its clear from your code that for two cons-constructed lists to be equal then both the heads and the tails need to be equal (the logical consequence of injCons and injCons2) but this is clearly not necessary to refute both equalities to provide a proof of inequality (you have seen this in the first two cases :)
(a :: as) = (b :: bs) => (a = b) /\ (as = bs)
=
¬(a = b) \/ ¬(as = bs) => ¬(a :: as = b :: bs)
So to refute the built in equality you have to pick one of the possible proofs to convince Epigram even if you have both.
Peter
On 04/04/06, Laszlo Nemeth <
[EMAIL PROTECTED]> wrote:
Hi,
You asked for it :).
------------------------------------------------------------------------------
( p : Eq (cons a as) (cons b bs) !
let !--------------------------------!
! injCons p : Eq as bs )
injCons p <= case p
{ injCons (rfl (cons a as)) => rfl as
}
------------------------------------------------------------------------------
( p : Eq (cons a as) (cons b bs) !
let !--------------------------------!
! injCons2 p : Eq a b )
injCons2 p <= case p
{ injCons2 (rfl (cons a as)) => rfl a
}
------------------------------------------------------------------------------
( p1 : Dec (Eq a b) ; p2 : Dec (Eq as bs) !
let !----------------------------------------------------!
! decEqCons p1 p2 : Dec (Eq (cons a as) (cons b bs)) )
decEqCons p1 p2 <= case p1
{ decEqCons (yes a') p2 <= case p2
{ decEqCons (yes a'') (yes a) <= case a''
{ decEqCons (yes (rfl a)) (yes a') <= case a'
{ decEqCons (yes (rfl a)) (yes (rfl as)) => yes (rfl (cons a as))
}
}
decEqCons (yes a') (no f) => no (lam p => f (injCons p))
}
decEqCons (no f) p2 <= case p2
{ decEqCons (no f) (yes a) <= case a
{ decEqCons (no f) (yes (rfl as)) => no (lam p => f (injCons2 p))
}
decEqCons (no f') (no f) => no (lam p => f' (injCons2 p))
}
}
------------------------------------------------------------------------------
The first three cases are unsurprising, but when neither the heads nor
the tails are equal epigram accepts the explanation that the heads are
not equal. I expected that 'f' (ie that the tails are different too)
would have to appear on the rhs! Why does epigram allow me to lose that
information???
Thanks, Laszlo
Peter Morris wrote:
> Hi all,
>
> Sorry for the black out in coverage on the list recently (which you
> may or may not have noticed) we should now be functional again, so if
> you have been itching to ask a question or start a discussion then,
> please, go ahead.
>
> Peter
>
