1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (*#***********************************************************************)
21 (* v * The Coq Proof Assistant / The Coq Development Team *)
23 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
25 (* \VV/ **************************************************************)
27 (* // * This file is distributed under the terms of the *)
29 (* * GNU Lesser General Public License Version 2.1 *)
31 (*#***********************************************************************)
33 (*i $Id: Wf_nat.v,v 1.16.2.1 2004/07/16 19:31:01 herbelin Exp $ i*)
35 (*#* Well-founded relations and natural numbers *)
37 include "Arith/Lt.ma".
40 Open Local Scope nat_scope.
44 Implicit Types m n p : nat.
48 Section Well_founded_Nat
52 cic:/Coq/Arith/Wf_nat/Well_founded_Nat/A.var
56 cic:/Coq/Arith/Wf_nat/Well_founded_Nat/f.var
59 inline procedural "cic:/Coq/Arith/Wf_nat/ltof.con" as definition.
61 inline procedural "cic:/Coq/Arith/Wf_nat/gtof.con" as definition.
63 inline procedural "cic:/Coq/Arith/Wf_nat/well_founded_ltof.con" as theorem.
65 inline procedural "cic:/Coq/Arith/Wf_nat/well_founded_gtof.con" as theorem.
67 (*#* It is possible to directly prove the induction principle going
68 back to primitive recursion on natural numbers ([induction_ltof1])
69 or to use the previous lemmas to extract a program with a fixpoint
72 the ML-like program for [induction_ltof1] is : [[
73 let induction_ltof1 F a = indrec ((f a)+1) a
75 function 0 -> (function a -> error)
76 |(S m) -> (function a -> (F a (function y -> indrec y m)));;
79 the ML-like program for [induction_ltof2] is : [[
80 let induction_ltof2 F a = indrec a
81 where rec indrec a = F a indrec;;
84 inline procedural "cic:/Coq/Arith/Wf_nat/induction_ltof1.con" as theorem.
86 inline procedural "cic:/Coq/Arith/Wf_nat/induction_gtof1.con" as theorem.
88 inline procedural "cic:/Coq/Arith/Wf_nat/induction_ltof2.con" as theorem.
90 inline procedural "cic:/Coq/Arith/Wf_nat/induction_gtof2.con" as theorem.
92 (*#* If a relation [R] is compatible with [lt] i.e. if [x R y => f(x) < f(y)]
93 then [R] is well-founded. *)
96 cic:/Coq/Arith/Wf_nat/Well_founded_Nat/R.var
100 cic:/Coq/Arith/Wf_nat/Well_founded_Nat/H_compat.var
103 inline procedural "cic:/Coq/Arith/Wf_nat/well_founded_lt_compat.con" as theorem.
109 inline procedural "cic:/Coq/Arith/Wf_nat/lt_wf.con" as lemma.
111 inline procedural "cic:/Coq/Arith/Wf_nat/lt_wf_rec1.con" as lemma.
113 inline procedural "cic:/Coq/Arith/Wf_nat/lt_wf_rec.con" as lemma.
115 inline procedural "cic:/Coq/Arith/Wf_nat/lt_wf_ind.con" as lemma.
117 inline procedural "cic:/Coq/Arith/Wf_nat/gt_wf_rec.con" as lemma.
119 inline procedural "cic:/Coq/Arith/Wf_nat/gt_wf_ind.con" as lemma.
121 inline procedural "cic:/Coq/Arith/Wf_nat/lt_wf_double_rec.con" as lemma.
123 inline procedural "cic:/Coq/Arith/Wf_nat/lt_wf_double_ind.con" as lemma.
126 Hint Resolve lt_wf: arith.
130 Hint Resolve well_founded_lt_compat: arith.
138 cic:/Coq/Arith/Wf_nat/LT_WF_REL/A.var
142 cic:/Coq/Arith/Wf_nat/LT_WF_REL/R.var
145 (* Relational form of inversion *)
148 cic:/Coq/Arith/Wf_nat/LT_WF_REL/F.var
151 inline procedural "cic:/Coq/Arith/Wf_nat/inv_lt_rel.con" as definition.
154 cic:/Coq/Arith/Wf_nat/LT_WF_REL/F_compat.var
157 inline procedural "cic:/Coq/Arith/Wf_nat/acc_lt_rel.con" as remark.
159 inline procedural "cic:/Coq/Arith/Wf_nat/well_founded_inv_lt_rel_compat.con" as theorem.
165 inline procedural "cic:/Coq/Arith/Wf_nat/well_founded_inv_rel_inv_lt_rel.con" as lemma.