The Coq mailing list

[Sidi <Sidi.Ould_Biha AT inria.fr>]

Thanks for the help. Both solution proof the example with div_aux but
only "dependent inversion" success with my working recursive definition.
The solution with case give a "horrible" term and refelxivity fails to
solve the resulting equality.

Regards.

On Tue, 2010-06-29 at 15:27 +0800, Jean-Francois Monin wrote:
> Like this:
> 
> Proof.
> intros. case H. simpl. reflexivity.
> Qed.
> 
> Bottom line: eliminate H since it is the engine (better: the fuel)
> of your function.
> 
> Hope this helps,
> JF
> 
> On Tue, Jun 29, 2010 at 02:52:28PM +0800, Sidi wrote:
> > Hi,
> > 
> > I have some problems with proving some basic proprieties on a function
> > defined recursively on a well founded predicate. Using the example given
> > in the "Rec Coq Tutorial", the function I defined looks like :
> > 
> > Fixpoint div_aux (x y : nat) (H : Acc lt x) {struct H} : nat :=
> >   match x as n return (x = n -> nat) with
> >   | 0 => fun _ : x = 0 => 0
> >   | S n => fun H0 : x = S n =>
> >       match eq_nat_dec y 0 with
> >       | left _ => y
> >       | right T => S (div_aux (x - y) y (minus_decrease x y H
> >                      (eq_ind_r (fun x0 => x0 <> 0) (sym_not_eq (O_S n))
> > H0) T))
> >       end
> >   end (refl_equal x).
> > 
> > I understand that this is not the better way to define the division, but
> > i do a pattern matching on x since in my original function i need to do
> > a recursive call on a subterm of x and H.
> > 
> > With this definition of div_aux, my question is how can I proof this
> > simple lemma :
> > 
> > Lemma div0 : forall y (H : Acc lt 0), div_aux 0 y H = 0.
> > Proof.
> > intros. unfold div_aux.
> > 
> > PS : The .v source file is the following
> > 
> > Require Import Minus.
> > Require Import Arith.
> > 
> > Lemma minus_smaller_S : forall x y : nat, x - y < S x.
> > Proof.
> > intros x y; pattern y, x; elim x using nat_double_ind.
> > destruct n; auto with arith.
> > simpl; auto with arith.
> > simpl; auto with arith.
> > Qed.
> > 
> > Lemma minus_smaller_positive : forall x y : nat, x <> 0 -> y <> 0 -> x -
> > y < x.
> > Proof.
> > destruct x; destruct y; simpl; intros; try tauto. apply minus_smaller_S.
> > Qed.
> > 
> > Definition minus_decrease : forall x y:nat, Acc lt x -> x <> 0 -> y <> 0
> > ->
> > Acc lt (x - y).
> > Proof.
> > intros x y H; case H.
> > intros Hz posz posy.
> > apply Hz; apply minus_smaller_positive; assumption.
> > Defined.
> > 
> > Fixpoint div_aux (x y : nat) (H : Acc lt x) {struct H} : nat :=
> >   match x as n return (x = n -> nat) with
> >   | 0 => fun _ : x = 0 => 0
> >   | S n => fun H0 : x = S n =>
> >       match eq_nat_dec y 0 with
> >       | left _ => y
> >       | right T => S (div_aux (x - y) y (minus_decrease x y H
> >                      (eq_ind_r (fun x0 => x0 <> 0) (sym_not_eq (O_S n))
> > H0) T))
> >       end
> >   end (refl_equal x).
> > 
> > Lemma div0 : forall y (H : Acc lt 0), div_aux 0 y H = 0.
> > Proof.
> > intros. unfold div_aux.
> > 
> > ---
> > 
> > Sidi
> > 
> > 
> > 
> > 
> > 
>