The Coq mailing list

[t x <txrev319 AT gmail.com>]

Thanks for the detailed reply. (1)-(3) are fairly clear to me now.

I've started reading http://adam.chlipala.net/cpdt/html/Equality.html and I don't understand why
  "generalize (fhapp (fhapp b hls2) hls3)" is needed

  this is show at: https://gist.github.com/anonymous/6248428#file-cpdt-equality-v-L619

For pf and pf', I understand why we want to genearlize them -- we want to run "rewrite app_assoc" on them.

However, why are generalizing the (fhapp (fhapp b hls2) hls3) part? (Besides Coq complaining.)

Thanks!

On Fri, Aug 16, 2013 at 6:03 AM, Daniel Schepler <dschepler AT gmail.com> wrote:

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