The Coq mailing list

[Razvan Voicu <razvan AT comp.nus.edu.sg>]

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


AUGER wrote:
> As far as I know, fix tactic is just
> fix a n.
> "refine (fix a {struct nth_term} := _)."
> or something like that,
>  that is you will have a "a: [Goal]" in your hypothesis,
>  which you will able to use at any time.
>  This feature is in fact inconsistant, try:
>
> Lemma Absurd: False.
> Proof.
>  generalize tt.
>  fix dummy 1.
>  assumption.
> Qed.
>
> Hopefully type checking denies this proof, but you found a "Proof 
> completed."
> before Qed, meaning that you proceded without guardedness.
> For huge proofs, it can be a pain in the neck to correct it.
>
> In fact some interesting feature would be to print a new kind of 
> hypothesis
> only available for information (not usable) and generate an hypothesis 
> each time
> the main term is destructured.
> ======================================================================
> For example:
>
> Theorem le_Pfact: forall x:nat, exists y, Pfact x y.
> Proof.
>  intro; new_induction x.
>   exists 1; constructor.
>  destruct x.
>   exists 1; constructor.
>  destruct Hx0 as [y P]; exists (x * y); constructor.
>  exact P.
> Qed.
>
> would have the following execution:
> Theorem le_Pfact: forall x:nat, exists y, Pfact x y.
> Proof.
> (*
> ______________________________________(1/1)
> forall x : nat, exists y : nat, Pfact x y
> *)
>  intro; new_induction x.
> (*
> ______________________________________(1/2)
> exists y : nat, Pfact 0 y
> *)
>   exists 1; constructor.
> (*
> (* Hxn : exists y : nat, Pfact xn y [where xn is a subterm of x]*)
> x : nat
> Hx : exists y : nat, Pfact x y
> ______________________________________(1/1)
> exists y : nat, Pfact (S x) y
> *)
>  destruct x.
> (*
> Hx : exists y : nat, Pfact 0 y
> ______________________________________(1/2)
> exists y : nat, Pfact 1 y
> *)
>   exists 1; constructor.
> (*
> (* Hxn : exists y : nat, Pfact xn y [where xn is a subterm of x]*)
> x : nat
> Hx : exists y : nat, Pfact (S x) y
> Hx0 : exists y : nat, Pfact x y
> ______________________________________(1/1)
> exists y : nat, Pfact (S (S x)) y
> *)
>  destruct Hx0 as [y P]; exists (x * y); constructor.
> (*
> (* Hxn : exists y : nat, Pfact xn y [where xn is a subterm of x]*)
> x : nat
> Hx : exists y : nat, Pfact (S x) y
> y : nat
> P : Pfact x y
> ______________________________________(1/1)
> Pfact x y
> *)
>  exact P.
> (*
> Proof completed.
> *)
> Qed.
>
> If the above is unreadable, try:
>
> Ltac new_induction x :=
>  destruct x; [|assert (Hx:exists y, Pfact x y);[admit|]].
> Ltac new_destruct x :=
>  destruct x; [|assert (Hx0:exists y, Pfact x y);[admit|]].
>
> Theorem le_Pfact: forall x:nat, exists y, Pfact x y.
> Proof.
>  intro; new_induction x.
>   exists 1; constructor.
>  new_destruct x.
>   exists 1; constructor.
>  destruct Hx0 as [y P]; exists (x * y); constructor.
>  exact P.
> Qed.
>
> to understand what I mean
> (it is a simulation of the feature, in real tactics,
>  we don't want to use "admit").
>
> ============================================================
> One last thing about recursion, but it is out of topic,
> as far as I know, we have no way to indicate the decreasing
> argument in:
>
> Lemma A: ...
> with B: ...
> .
>
> For that I have to do:
>
> Lemma A: ...
> .
> Proof.
>  refine (fix A: ... {struct ...} := _
>          with B: ... {struct ...} := _
>      for A).
> (*lemma A*)
> ...
> (*lemma B*)
> .
>
> Which can be syntactically awfull, and produces a proof of A and none 
> of B.
> Not giving the decreasing argument can lead in way too long 
> computation to
> determine which one to choose and only few seconds if we indicate it 
> directly.
> I have once met this problem.
>
> I know there may exist some solutions with Program or Induction Scheme,
> but for such low level things, there should exist simple ways to do it.