The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Friday, August 16, 2013 04:26:55 AM t x wrote:
> Hi,
> 
>   This is my minimal confusion example:
> https://gist.github.com/anonymous/6247310
> 
>   The example is a bit silly -- but it comes from a legitimate source,
> studying "Lemma fmiddle_middle" of DepList.v of lambda tamer. (Though I
> might introduced errors.)
> 
>   Here are things I am confused on:
> 
> (1) Why does "Fixpoint silly" even get accepted? Why is it that all objects
> of type H can match against "eq_refl" ?
> [ this seems like black magic to me ]

Just look at the definition of eq:

Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x

Essentially, this is saying that for a fixed type A and element x of A, the 
only way to prove anything of the form x = ? is @eq_refl A x; and if you 
destruct the equality, you can convert the ? into x (especially if the ? is 
just a variable).

(By the way, it's pointless to make silly a Fixpoint -- there's no recursion 
here, just a single match.)

> 
> (2) Why does the "destruct (lem_000 n)" line of lem_002 work? "Print
> lem_000." is a big complicated expression. I don't see why it should match
> against eq_refl.
> [ this also seems like black magic to me ]

"destruct (lem_000 n)" I think first abstracts out the term (lem_000 n) in 
the 
hypotheses and goal, and then does the destruction.  So it's sort of the same 
thing as what you did to get to lemma_003.

> (3) Is lemma_003 even provable in Coq? And if so, how do I prove it in Coq?
> [ I'm divided on this. On one hand, it shouldn't be true since not all
> proofs necessarily have to be equal to eq_refl. On the other hand, given
> (1), apparently all proofs are eq_refl, so it's therefore trivially true. ]

An easier proof of lemma_003 than what you followed up with would be to start 
with "destruct H" and then either "reflexivity", or "simpl" if you want to 
see 
more clearly why "reflexivity" works.

> (4) What section of what manual should I read up on clear up these
> knowledge gaps?

I'd say read up on dependent pattern matching, and maybe look at the type 
signature and definition of "eq_rect".

Now the real kicker is: despite the fact that eq_rect is the only constructor 
of equality proofs, it's impossible to prove in general:
forall (A:Type) (x:A) (H:x=x), H = eq_refl.
(!)  Technically, the insurmountable obstacle you run into in trying to write 
a proof of this is: to do a match on H, you need it to be of the form
match H as H' in (_ = y) return (function of y and H') with ... end
where substituting in H for H' and x for y in the function returns H = 
eq_refl.  
It turns out it's impossible to generalize "H = eq_refl" in such a way that 
you 
can construct a proof of (f x eq_refl).

On the other hand, it *is* possible to prove
forall (A:Type) (x:A) (P : forall y:A, x = y -> Prop),
  P x eq_refl -> forall (y:A) (H:x=y), P y H.
But not
forall (A:Type) (x:A) (P : x = x -> Prop),
  P eq_refl -> forall (H:x=x), P x H.
I guess what I'm trying to say above is that the freedom to vary the right 
hand side of the equality is essential to being able to destruct the equality.
-- 
Daniel Schepler