The Coq mailing list

[t x <txrev319 AT gmail.com>]

The answer to (3) is apparently "yes", via "rewrite H; destruct b; reflexivity."

However, I'd love to understand (1), (2), and (4).

On Fri, Aug 16, 2013 at 4:26 AM, t x <txrev319 AT gmail.com> 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 ]

(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 ]

(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. ]

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

Thanks!