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___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
25 (* \VV/ *************************************************************)
27 (* // * This file is distributed under the terms of the *)
29 (* * GNU Lesser General Public License Version 2.1 *)
31 (*#**********************************************************************)
34 Set Implicit Arguments.
37 (*i $Id: Wf.v,v 1.17 2003/11/29 17:28:30 herbelin Exp $ i*)
39 (*#* This module proves the validity of
40 - well-founded recursion (also called course of values)
41 - well-founded induction
43 from a well-founded ordering on a given set *)
45 include "Init/Notations.ma".
47 include "Init/Logic.ma".
49 include "Init/Datatypes.ma".
51 (*#* Well-founded induction principle on Prop *)
58 cic:/Coq/Init/Wf/Well_founded/A.var
62 cic:/Coq/Init/Wf/Well_founded/R.var
65 (*#* The accessibility predicate is defined to be non-informative *)
67 inline procedural "cic:/Coq/Init/Wf/Acc.ind".
69 inline procedural "cic:/Coq/Init/Wf/Acc_inv.con" as lemma.
71 (*#* the informative elimination :
72 [let Acc_rec F = let rec wf x = F x wf in wf] *)
79 cic:/Coq/Init/Wf/Well_founded/AccRecType/P.var
83 cic:/Coq/Init/Wf/Well_founded/AccRecType/F.var
86 inline procedural "cic:/Coq/Init/Wf/Acc_rect.con" as definition.
92 inline procedural "cic:/Coq/Init/Wf/Acc_rec.con" as definition.
94 (*#* A simplified version of Acc_rec(t) *)
101 cic:/Coq/Init/Wf/Well_founded/AccIter/P.var
105 cic:/Coq/Init/Wf/Well_founded/AccIter/F.var
108 inline procedural "cic:/Coq/Init/Wf/Acc_iter.con" as definition.
114 (*#* A relation is well-founded if every element is accessible *)
116 inline procedural "cic:/Coq/Init/Wf/well_founded.con" as definition.
118 (*#* well-founded induction on Set and Prop *)
121 cic:/Coq/Init/Wf/Well_founded/Rwf.var
124 inline procedural "cic:/Coq/Init/Wf/well_founded_induction_type.con" as theorem.
126 inline procedural "cic:/Coq/Init/Wf/well_founded_induction.con" as theorem.
128 inline procedural "cic:/Coq/Init/Wf/well_founded_ind.con" as theorem.
130 (*#* Building fixpoints *)
137 cic:/Coq/Init/Wf/Well_founded/FixPoint/P.var
141 cic:/Coq/Init/Wf/Well_founded/FixPoint/F.var
144 inline procedural "cic:/Coq/Init/Wf/Fix_F.con" as definition.
146 inline procedural "cic:/Coq/Init/Wf/Fix.con" as definition.
148 (*#* Proof that [well_founded_induction] satisfies the fixpoint equation.
149 It requires an extra property of the functional *)
152 cic:/Coq/Init/Wf/Well_founded/FixPoint/F_ext.var
155 inline procedural "cic:/Coq/Init/Wf/Acc_inv_dep.con" as theorem.
157 inline procedural "cic:/Coq/Init/Wf/Fix_F_eq.con" as lemma.
159 inline procedural "cic:/Coq/Init/Wf/Fix_F_inv.con" as lemma.
161 inline procedural "cic:/Coq/Init/Wf/Fix_eq.con" as lemma.
171 (*#* A recursor over pairs *)
174 Section Well_founded_2
178 cic:/Coq/Init/Wf/Well_founded_2/A.var
182 cic:/Coq/Init/Wf/Well_founded_2/B.var
186 cic:/Coq/Init/Wf/Well_founded_2/R.var
190 cic:/Coq/Init/Wf/Well_founded_2/P.var
194 cic:/Coq/Init/Wf/Well_founded_2/F.var
197 inline procedural "cic:/Coq/Init/Wf/Acc_iter_2.con" as definition.
200 cic:/Coq/Init/Wf/Well_founded_2/Rwf.var
203 inline procedural "cic:/Coq/Init/Wf/well_founded_induction_type_2.con" as theorem.