The Coq mailing list

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

Le Mon, 13 Dec 2010 16:00:57 +0100,
quentin.carbonneaux AT inria.fr
 a écrit :

> Hello,
> 
> here is the proof using refine, I don't find it much safer than the
> one using the fix tactic: I had to use the 'Guarded' command !
> 
> Lemma sum_S : forall a b : nat, sum a (S b) = S (sum a b).
> Proof.
> refine (
>   fix sum_S (a b : nat) {struct b} :=
>     match b with
>     | 0 => _
>     | S b' => _
>     end); simpl.
> 
>  reflexivity.
>  rewrite <- (sum_S (S a) b'). reflexivity.
> Qed.
> 
> Using the wildcard "_" we can specify only a part of the proof lambda
> term, then we can use classical tactics to fill the gaps. (with care
> because the sum_S premise must be called only with its second
> argument structurally smaller than b).
> 
> {struct b} means that the proof is decreasing relatively to 'b'; if
> not specified it seems that coq constrains 'a' to be the decreasing
> argument.
> 

In the same spirit, here is a trick to have no problems with
the guards in recursion:

>>>
(* this tactic makes an transparent term of the hypothesis
 * into an opaque one; I didn't used "assume (type_of H)...",
 * since it would produce a "let ..." in the proof term.
 * I never used it, so it may have flaws
 * *)
Ltac hide H :=
 generalize H; clear dependent H; intro H.

Lemma sum_S : forall a b : nat, sum a (S b) = S (sum a b).
Proof.
refine (
  fix sum_S (a b : nat) {struct b} :=
    match b with
    | 0 => _
    | S b' => let sum_rec a := sum_S a b' in _
    end); (try hide sum_rec); clear sum_S; simpl.
(* you define a good hypothesis in the term,
 * and then remove sum_S, so that you are in a good state.
 * for this example, we could also have done:
 * "let sum_rec := sum_S (S a) b'"
 * *)

 reflexivity.

 case sum_rec.
 reflexivity.
Qed.
<<<
In fact I lied when I said you won't have problems with guards,
since the first time, I wrote {struct a} instead of {struct b},
and coq didn't complained; but at least, manually checking is easier.
Furthermore, if you try:
>>>
Lemma sum_S : forall a b : nat, sum a (S b) = S (sum a b).
Proof.
refine (
  fix sum_S (a b : nat) {struct a} :=
    match b with
    | 0 => _
    | S b' => let sum_rec := sum_S (S a) b' in _
    end); (try hide sum_rec); clear sum_S; admit.
Qed.
<<<
Then you will see that your proof skeleton is not guarded
(I did induction on {struct a} instead of {struct b}),
so you can instantaneously check all your guarded conditions,
instead of checking it after each tactic/branch.

I think coq should make some checks at this step, since it has all the
elements to perform a type checking.

For me, some cool stuff would be that "fix" doesn't generate a
usable hypothesis but some anonymous information in the stack of
hypothesis, like:

[forall a [α as subterm of b], sum a (S α) = S (sum α b)]
<Some hypothesis>

then, when you do "case b" or "destruct b", it should pop some named
usable hypothesis:

[forall a [α as subterm of (S b)], sum a (S α) = S (sum a α)]
IHSum_s: forall a, sum a (S b) = sum a (S b) = S (sum a b)

This feature would be even more interesting in the case of mutual
recursion:

I know mainly 2 ways to do mutual induction:
* Induction Scheme, which is heavy to use (each time you define an
  inductive, you have to generate its induction principle and
  remember the order of its arguments)
* Have the syntax "Lemma L1: ... with L2: ... with L3: ..."
  which is more readable and understandable, but which cannot
  take its structural argument as argument.
  (The structural argument is guessed at Qed time,
   but I had some examples which took more than 20 sec to
   type check, and when doing it manually with "refine (fix ...
   with ...)", it did less than 3 sec. to compute)
  Furthermore, in this solution, you have no guard checking.

So having such a feature would make the second point a lot better.