The Coq mailing list

[AUGER <Cedric.Auger AT lri.fr>]

Le Thu, 28 Jan 2010 16:49:01 +0100, Razvan Voicu <razvan AT comp.nus.edu.sg>  
a écrit:

> Hi Cedric,
>
> You are right. However, I think using 'fix' is a matter of preference  
> after all. It is indeed unsound from a pure sequent-calculus point of  
> view, but in Coq the 'Guarded' command comes to the rescue, telling the  
> user if the type checker detects unguarded applications of the "unsound"  
> hypothesis up to the current point in the proof (one major disadvantage  
> is that you can't employ the automated tactics while the unsound  
> hypothesis is present in the current sequent, you must clear it first).
>
> I would actually appreciate a (yet another unsound) tactic that would  
> allow me to create mutually recursive 'fix' constructs.
>
> Here's another little gem using 'fix' :
>
> Inductive even : nat -> Prop :=
>   e0 : even 0
> | eS : forall n, even n -> even (S (S n)).
>
> Goal forall n, even n \/ ~ even n.
> fix circ 1.
> intros [|[|n]].
> left ; constructor.
> right ; intro H ; inversion H.
> assert (H := circ n) ; clear circ.
> destruct H.
> left ; constructor ; assumption.
> right ; intro H1; apply H ; inversion H1 ; assumption.
> Save.
>
> Razvan

I wasn't aware of this feature, I may have use of it one day...
But, "Guarded" should be IMO used only for debugging proofs,
meaning that you have fallen into some error.
I think also that "prevent is better than fixing" and knowing
that you are in an unguarded situation will not tell you how
to go in a guarded situation.


--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay