helm/software/matita/contribs/procedural/Coq/Init/Wf.mma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "Coq.ma".
  18
  19 (*#***********************************************************************)
  20
  21 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
  22
  23 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
  24
  25 (*   \VV/  **************************************************************)
  26
  27 (*    //   *      This file is distributed under the terms of the       *)
  28
  29 (*         *       GNU Lesser General Public License Version 2.1        *)
  30
  31 (*#***********************************************************************)
  32
  33 (* UNEXPORTED
  34 Set Implicit Arguments.
  35 *)
  36
  37 (*i $Id: Wf.v,v 1.17.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
  38
  39 (*#* This module proves the validity of
  40     - well-founded recursion (also called course of values)
  41     - well-founded induction
  42
  43    from a well-founded ordering on a given set *)
  44
  45 include "Init/Notations.ma".
  46
  47 include "Init/Logic.ma".
  48
  49 include "Init/Datatypes.ma".
  50
  51 (*#* Well-founded induction principle on Prop *)
  52
  53 (* UNEXPORTED
  54 Section Well_founded
  55 *)
  56
  57 (* UNEXPORTED
  58 cic:/Coq/Init/Wf/Well_founded/A.var
  59 *)
  60
  61 (* UNEXPORTED
  62 cic:/Coq/Init/Wf/Well_founded/R.var
  63 *)
  64
  65 (*#* The accessibility predicate is defined to be non-informative *)
  66
  67 inline procedural "cic:/Coq/Init/Wf/Acc.ind".
  68
  69 inline procedural "cic:/Coq/Init/Wf/Acc_inv.con" as lemma.
  70
  71 (*#* the informative elimination :
  72      [let Acc_rec F = let rec wf x = F x wf in wf] *)
  73
  74 (* UNEXPORTED
  75 Section AccRecType
  76 *)
  77
  78 (* UNEXPORTED
  79 cic:/Coq/Init/Wf/Well_founded/AccRecType/P.var
  80 *)
  81
  82 (* UNEXPORTED
  83 cic:/Coq/Init/Wf/Well_founded/AccRecType/F.var
  84 *)
  85
  86 inline procedural "cic:/Coq/Init/Wf/Acc_rect.con" as definition.
  87
  88 (* UNEXPORTED
  89 End AccRecType
  90 *)
  91
  92 inline procedural "cic:/Coq/Init/Wf/Acc_rec.con" as definition.
  93
  94 (*#* A simplified version of Acc_rec(t) *)
  95
  96 (* UNEXPORTED
  97 Section AccIter
  98 *)
  99
 100 (* UNEXPORTED
 101 cic:/Coq/Init/Wf/Well_founded/AccIter/P.var
 102 *)
 103
 104 (* UNEXPORTED
 105 cic:/Coq/Init/Wf/Well_founded/AccIter/F.var
 106 *)
 107
 108 inline procedural "cic:/Coq/Init/Wf/Acc_iter.con" as definition.
 109
 110 (* UNEXPORTED
 111 End AccIter
 112 *)
 113
 114 (*#* A relation is well-founded if every element is accessible *)
 115
 116 inline procedural "cic:/Coq/Init/Wf/well_founded.con" as definition.
 117
 118 (*#* well-founded induction on Set and Prop *)
 119
 120 (* UNEXPORTED
 121 cic:/Coq/Init/Wf/Well_founded/Rwf.var
 122 *)
 123
 124 inline procedural "cic:/Coq/Init/Wf/well_founded_induction_type.con" as theorem.
 125
 126 inline procedural "cic:/Coq/Init/Wf/well_founded_induction.con" as theorem.
 127
 128 inline procedural "cic:/Coq/Init/Wf/well_founded_ind.con" as theorem.
 129
 130 (*#* Building fixpoints  *)
 131
 132 (* UNEXPORTED
 133 Section FixPoint
 134 *)
 135
 136 (* UNEXPORTED
 137 cic:/Coq/Init/Wf/Well_founded/FixPoint/P.var
 138 *)
 139
 140 (* UNEXPORTED
 141 cic:/Coq/Init/Wf/Well_founded/FixPoint/F.var
 142 *)
 143
 144 inline procedural "cic:/Coq/Init/Wf/Fix_F.con" as definition.
 145
 146 inline procedural "cic:/Coq/Init/Wf/Fix.con" as definition.
 147
 148 (*#* Proof that [well_founded_induction] satisfies the fixpoint equation.
 149     It requires an extra property of the functional *)
 150
 151 (* UNEXPORTED
 152 cic:/Coq/Init/Wf/Well_founded/FixPoint/F_ext.var
 153 *)
 154
 155 inline procedural "cic:/Coq/Init/Wf/Acc_inv_dep.con" as theorem.
 156
 157 inline procedural "cic:/Coq/Init/Wf/Fix_F_eq.con" as lemma.
 158
 159 inline procedural "cic:/Coq/Init/Wf/Fix_F_inv.con" as lemma.
 160
 161 inline procedural "cic:/Coq/Init/Wf/Fix_eq.con" as lemma.
 162
 163 (* UNEXPORTED
 164 End FixPoint
 165 *)
 166
 167 (* UNEXPORTED
 168 End Well_founded
 169 *)
 170
 171 (*#* A recursor over pairs *)
 172
 173 (* UNEXPORTED
 174 Section Well_founded_2
 175 *)
 176
 177 (* UNEXPORTED
 178 cic:/Coq/Init/Wf/Well_founded_2/A.var
 179 *)
 180
 181 (* UNEXPORTED
 182 cic:/Coq/Init/Wf/Well_founded_2/B.var
 183 *)
 184
 185 (* UNEXPORTED
 186 cic:/Coq/Init/Wf/Well_founded_2/R.var
 187 *)
 188
 189 (* UNEXPORTED
 190 cic:/Coq/Init/Wf/Well_founded_2/P.var
 191 *)
 192
 193 (* UNEXPORTED
 194 cic:/Coq/Init/Wf/Well_founded_2/F.var
 195 *)
 196
 197 inline procedural "cic:/Coq/Init/Wf/Acc_iter_2.con" as definition.
 198
 199 (* UNEXPORTED
 200 cic:/Coq/Init/Wf/Well_founded_2/Rwf.var
 201 *)
 202
 203 inline procedural "cic:/Coq/Init/Wf/well_founded_induction_type_2.con" as theorem.
 204
 205 (* UNEXPORTED
 206 End Well_founded_2
 207 *)
 208