The Coq mailing list

[Eduardo Gimenez <Eduardo.Gimenez AT trusted-logic.fr>]

Hi Amy,

Cofix is a tactic for proving theorems by co-induction. If the goal of 
theorem t is A, Cofix introduces the hypothesis t:A into the context,
and generates a proof term of the form CoFixpoint t : A := ....

The tactic is not documented since it may generate proof terms
that do not respect Coq's guardedness condition. Actually, for a 
co-recursively defined proof to be accepted, any application of t must be 
guarded by at least one constructor of A, and only by constructors of A. 
Unfortunately, checking this conditions during the construction of the proof 
is too much time-consuming, and would make the time neccessary for applying a 
tactic to be linear on the size of the proof.  As a consequence, it is 
possible that sometimes Coq rejects to save a proof  constructed using the 
Cofix tactic, since it does not respect the guardedness condition.. For 
instance, the tactic Cofix;Assumption always succeeds if the goal is a 
co-inductive type, but, as it does not produce an acceptable term, so Coq's 
typechecker rejects it when the user tries to save it (using the Qed command, 
for instance). The command "Guarded" can be used during the construction of 
the proof in order to test whether the proof is well-formed up to that point. 

You will find some extra explanations and examples in my paper "A Tutorial on 
Recursive Types in Coq" , available at Coq's page 
http://coq.inria.fr/doc-eng.html

Hope this brief explanation helps...
Best wishes,
Eduardo.

On Monday 01 April 2002 21:39, Amy Felty wrote:
> We noticed the use of the Cofix tactic in some example proof development
> that we came across, but we haven't been able to find a description of
> this tactic in the documentation.  Can anyone explain how it works?
> Please send any response to both myself and Guy Beaulieu.  Thank you in
> advance.
>
> Amy Felty
>
> -------------------
> To unsubscribe, mail 
> coq-club-request AT pauillac.inria.fr
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Coq-Club Archives: http://coq.inria.fr/mailing-lists/coqclub/
-------------------
To unsubscribe, mail 
coq-club-request AT pauillac.inria.fr
Bug reports: http://coq.inria.fr/bin/coq-bugs
Coq-Club Archives: http://coq.inria.fr/mailing-lists/coqclub/