The Coq mailing list

[Ivan Scagnetto <scagnett AT dimi.uniud.it>]

According to Christine Paulin-Mohring:
> In order to check the well-formednes of fixpoint definition, Coq
> expands names but only transparent names. The so-called opaque names
> are considered as abstract proofs, there is no need to keep the
> underlying proof object. The default in Coq is that a theorem or
> lemma is opaque while a definition is transparent. But an opaque 
> constant can be made transparent using the command 
> Transparent WEIRD. A better solution is to replace the keywords
> Lemma / Qed. in the WEIRD definition by Definition / Defined.

This sounds correct in the case WEIRD is associated with a proof-term,
i.e. it is delta-reducible. But what if WEIRD is an axiom?  In such
case, it cannot be replaced by any proof term, and hence the
well-formedness check fails.  Nevertheless, the coinductive call can
be well-formed.  This is the case of the previous example: in the term

       (a [n:N](WEIRD (ex_intro N [_:N]A n FOO) n))

the "a" constructor should guard everything in its arguments.  In
particular, any FOO call which appears as an argument of WEIRD cannot
"step over" the "a" constructor...  Therefore, although Coq does not
accept this proof term, we expected it to be guarded.  Or is it not?


Have a Happy New Year,
Ivan and Marino