The Coq mailing list

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

Le Thu, 28 Jan 2010 03:55:46 +0100, Gyesik Lee <gslee AT ropas.snu.ac.kr> a  
écrit:

> Dear Jean-Francois, Matthieu and Razvan,
>
> many thanks for the explanations and hints.
>
> First, I see now more clearly that the "fix" tactic plays also the
> role of the general induction principle based on the transitive
> closure of the direct-subterm relation.
>
> Second, the Equations library looks very interesting and helpful.  I
> should have a look at it.
>
> Gyesik

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.

--
Cédric AUGER

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