The Coq mailing list

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

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