The Coq mailing list

[quentin.carbonneaux AT inria.fr]

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.

On 12/13 14:20, Daniel de Rauglaudre wrote:
> Hi,
> 
> On Mon, Dec 13, 2010 at 11:56:26AM +0100, Jean-Francois Monin wrote:
> 
> > Yes. A recent and convenient tactic to get the same effect is revert. 
> > Something like
> >   intros a b; revert a; induction b etc.
> 
> Noticed. Thanks.
> 
> > Forgot to explain fix 2 : it is an undocumented tactic 
> > [...]
> > You have to know what you are doing, and some tactics like auto
> > become dangerous. [...]
> 
> I indeed experimented that. It copied my conclusion into the hypotheses!
> No surprised that "assumption" worked, but Qed did not. Morality: I prefer
> not touch "fix" now :-)
> 
> -- 
> Daniel de Rauglaudre
> http://pauillac.inria.fr/~ddr/