The Coq mailing list

[David Pichardie <david.pichardie AT inria.fr>]

Just to complete my previous solution: since you don't need induction  
here, the fixpoint equation is sufficient.


Lemma div0_bis : forall y, div 0 y = 0.
Proof.
  intros; rewrite div_equation; trivial.
Qed.

David.


Le 29 juin 10 à 08:52, Sidi a écrit :

> 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