The Coq mailing list

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

Bonjour,

Je n'arrive pas à faire des preuves simples sur ce genre de points fixes
:

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

Theorem F0_is_0 : (F (0) (wf_nat (0)))=(0).
...
--------------------------------------------------

Où puis-je trouver de la documentation sur ce genre de techniques ? (je
n'ai pour l'instant rien trouver dans le manuel de Coq et dans le
tutorial de E. Giménez )

Cordialement,

David Pichardie.

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