I’m trying to wrap my brain around the essence of the problems with dependent programming and equality. Some proofs are more difficult or impossible to do without the
JMeq axiom. I’ve been trying to formulate a minimal example that captures the essence of this problem:
Inductive inf : (unit -> Type) := | infc : inf tt -> inf tt. Lemma match_eq (c : inf tt) (e : tt = tt) : match e in _ = y return inf y with | eq_refl => infc c end = infc c.
As far as I can see, this is not provable without axioms. Can anyone confirm this or give a counterexample? The closest I’ve gotten is:
refine ( match e as e0 in _ = f return forall (c0 : inf f), match e0 in _ = g return inf g with | eq_refl => infc c end = infc c0 with | eq_refl => _ end c).
The error message Coq gives here is very confusing by the way. It says that
infc c0 has type
inf f but should have type
inf (). If I then change it to
infc c, Coq changes its mind and tells us it
c has type
inf () but should have type
inf f. This seems to be related to the usage of
unit. If I change the argument of
bool, the error disappears (but the lemma is still not provable).