The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT imag.fr>]

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
> 
> 
> 
> 
> 

-- 
Jean-Francois Monin
CNRS-LIAMA, Project FORMES  &  Universite de Grenoble 1

Office 3-605, FIT, Tsinghua University
Haidian District, Beijing 100084, CHINA
Tel: +86 10 62 79 69 79 ext 605
Fax@LIAMA:
 +86 10 6264 7458