The Coq mailing list

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

J'ai trouvé un début de solution dans le module Coq.Init.Wf.

Désolé pour le dérangement.

Pour information :

Require Peano_dec.
Require Arith.

Axiom lemme_dec : (n:nat) ~n=(0) -> (lt (minus n (1)) n).

Fixpoint F [n:nat; H:(Acc nat lt n)] :nat :=
  if (eq_nat_dec n (0)) then [p](0)
                        else [p](F (minus n (1)) (Acc_inv nat lt n H (minus
n (1)) (lemme_dec n p))).

Axiom wf_nat : (well_founded nat lt).

Scheme Acc_inv_dep := Induction for Acc Sort Prop.

Lemma F_eq : (n:nat)(H:(Acc nat lt n))
  (if (eq_nat_dec n (0)) then [p](0)
                        else [p](F (minus n (1)) (Acc_inv nat lt n H (minus
n (1)) (lemme_dec n p))))
  =   (F n H).
Intros n H.
Elim H using Acc_inv_dep.
Intros.
Simpl.
Auto.
Qed.

Theorem F0_is_0 : (F (0) (wf_nat (0)))=(0).
Case (F_eq (0) (wf_nat (0))).
Simpl.
Reflexivity.
Qed.


-------------------
To unsubscribe, mail 
coq-club-request AT pauillac.inria.fr
Bug reports: http://coq.inria.fr/bin/coq-bugs
Coq-Club Archives: http://coq.inria.fr/mailing-lists/coqclub/