diff options
Diffstat (limited to 'theories7/Init')
| -rwxr-xr-x | theories7/Init/Datatypes.v | 125 | ||||
| -rwxr-xr-x | theories7/Init/Logic.v | 306 | ||||
| -rwxr-xr-x | theories7/Init/Logic_Type.v | 304 | ||||
| -rw-r--r-- | theories7/Init/Notations.v | 94 | ||||
| -rwxr-xr-x | theories7/Init/Peano.v | 218 | ||||
| -rwxr-xr-x | theories7/Init/Prelude.v | 16 | ||||
| -rwxr-xr-x | theories7/Init/Specif.v | 204 | ||||
| -rwxr-xr-x | theories7/Init/Wf.v | 158 |
8 files changed, 0 insertions, 1425 deletions
diff --git a/theories7/Init/Datatypes.v b/theories7/Init/Datatypes.v deleted file mode 100755 index 006ec08e..00000000 --- a/theories7/Init/Datatypes.v +++ /dev/null @@ -1,125 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: Datatypes.v,v 1.3.2.1 2004/07/16 19:31:26 herbelin Exp $ i*) - -Require Notations. -Require Logic. - -Set Implicit Arguments. -V7only [Unset Implicit Arguments.]. - -(** [unit] is a singleton datatype with sole inhabitant [tt] *) - -Inductive unit : Set := tt : unit. - -(** [bool] is the datatype of the booleans values [true] and [false] *) - -Inductive bool : Set := true : bool - | false : bool. - -Add Printing If bool. - -(** [nat] is the datatype of natural numbers built from [O] and successor [S]; - note that zero is the letter O, not the numeral 0 *) - -Inductive nat : Set := O : nat - | S : nat->nat. - -Delimits Scope nat_scope with nat. -Bind Scope nat_scope with nat. -Arguments Scope S [ nat_scope ]. - -(** [Empty_set] has no inhabitant *) - -Inductive Empty_set:Set :=. - -(** [identity A a] is the family of datatypes on [A] whose sole non-empty - member is the singleton datatype [identity A a a] whose - sole inhabitant is denoted [refl_identity A a] *) - -Inductive identity [A:Type; a:A] : A->Set := - refl_identity: (identity A a a). -Hints Resolve refl_identity : core v62. - -Implicits identity_ind [1]. -Implicits identity_rec [1]. -Implicits identity_rect [1]. -V7only [ -Implicits identity_ind []. -Implicits identity_rec []. -Implicits identity_rect []. -]. - -(** [option A] is the extension of A with a dummy element None *) - -Inductive option [A:Set] : Set := Some : A -> (option A) | None : (option A). - -Implicits None [1]. -V7only [Implicits None [].]. - -(** [sum A B], equivalently [A + B], is the disjoint sum of [A] and [B] *) -(* Syntax defined in Specif.v *) -Inductive sum [A,B:Set] : Set - := inl : A -> (sum A B) - | inr : B -> (sum A B). - -Notation "x + y" := (sum x y) : type_scope. - -(** [prod A B], written [A * B], is the product of [A] and [B]; - the pair [pair A B a b] of [a] and [b] is abbreviated [(a,b)] *) - -Inductive prod [A,B:Set] : Set := pair : A -> B -> (prod A B). -Add Printing Let prod. - -Notation "x * y" := (prod x y) : type_scope. -V7only [Notation "( x , y )" := (pair ? ? x y) : core_scope.]. -V8Notation "( x , y , .. , z )" := (pair ? ? .. (pair ? ? x y) .. z) : core_scope. - -Section projections. - Variables A,B:Set. - Definition fst := [p:(prod A B)]Cases p of (pair x y) => x end. - Definition snd := [p:(prod A B)]Cases p of (pair x y) => y end. -End projections. - -V7only [ -Notation Fst := (fst ? ?). -Notation Snd := (snd ? ?). -]. -Hints Resolve pair inl inr : core v62. - -Lemma surjective_pairing : (A,B:Set;p:A*B)p=(pair A B (Fst p) (Snd p)). -Proof. -NewDestruct p; Reflexivity. -Qed. - -Lemma injective_projections : - (A,B:Set;p1,p2:A*B)(Fst p1)=(Fst p2)->(Snd p1)=(Snd p2)->p1=p2. -Proof. -NewDestruct p1; NewDestruct p2; Simpl; Intros Hfst Hsnd. -Rewrite Hfst; Rewrite Hsnd; Reflexivity. -Qed. - -V7only[ -(** Parsing only of things in [Datatypes.v] *) -Notation "< A , B > ( x , y )" := (pair A B x y) (at level 1, only parsing, A annot). -Notation "< A , B > 'Fst' ( p )" := (fst A B p) (at level 1, only parsing, A annot). -Notation "< A , B > 'Snd' ( p )" := (snd A B p) (at level 1, only parsing, A annot). -]. - -(** Comparison *) - -Inductive relation : Set := - EGAL :relation | INFERIEUR : relation | SUPERIEUR : relation. - -Definition Op := [r:relation] - Cases r of - EGAL => EGAL - | INFERIEUR => SUPERIEUR - | SUPERIEUR => INFERIEUR - end. diff --git a/theories7/Init/Logic.v b/theories7/Init/Logic.v deleted file mode 100755 index 6ba9c7a1..00000000 --- a/theories7/Init/Logic.v +++ /dev/null @@ -1,306 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: Logic.v,v 1.6.2.1 2004/07/16 19:31:26 herbelin Exp $ i*) - -Set Implicit Arguments. -V7only [Unset Implicit Arguments.]. - -Require Notations. - -(** [True] is the always true proposition *) -Inductive True : Prop := I : True. - -(** [False] is the always false proposition *) -Inductive False : Prop := . - -(** [not A], written [~A], is the negation of [A] *) -Definition not := [A:Prop]A->False. - -Notation "~ x" := (not x) : type_scope. - -Hints Unfold not : core. - -Inductive and [A,B:Prop] : Prop := conj : A -> B -> A /\ B - -where "A /\ B" := (and A B) : type_scope. - -V7only[ -Notation "< P , Q > { p , q }" := (conj P Q p q) (P annot, at level 1). -]. - -Section Conjunction. - - (** [and A B], written [A /\ B], is the conjunction of [A] and [B] - - [conj A B p q], written [<p,q>] is a proof of [A /\ B] as soon as - [p] is a proof of [A] and [q] a proof of [B] - - [proj1] and [proj2] are first and second projections of a conjunction *) - - Variables A,B : Prop. - - Theorem proj1 : (and A B) -> A. - Proof. - NewDestruct 1; Trivial. - Qed. - - Theorem proj2 : (and A B) -> B. - Proof. - NewDestruct 1; Trivial. - Qed. - -End Conjunction. - -(** [or A B], written [A \/ B], is the disjunction of [A] and [B] *) - -Inductive or [A,B:Prop] : Prop := - or_introl : A -> A \/ B - | or_intror : B -> A \/ B - -where "A \/ B" := (or A B) : type_scope. - -(** [iff A B], written [A <-> B], expresses the equivalence of [A] and [B] *) - -Definition iff := [A,B:Prop] (and (A->B) (B->A)). - -Notation "A <-> B" := (iff A B) : type_scope. - -Section Equivalence. - -Theorem iff_refl : (A:Prop) (iff A A). - Proof. - Split; Auto. - Qed. - -Theorem iff_trans : (a,b,c:Prop) (iff a b) -> (iff b c) -> (iff a c). - Proof. - Intros A B C (H1,H2) (H3,H4); Split; Auto. - Qed. - -Theorem iff_sym : (A,B:Prop) (iff A B) -> (iff B A). - Proof. - Intros A B (H1,H2); Split; Auto. - Qed. - -End Equivalence. - -(** [(IF P Q R)], or more suggestively [(either P and_then Q or_else R)], - denotes either [P] and [Q], or [~P] and [Q] *) -Definition IF_then_else := [P,Q,R:Prop] (or (and P Q) (and (not P) R)). -V7only [Notation IF:=IF_then_else.]. - -Notation "'IF' c1 'then' c2 'else' c3" := (IF c1 c2 c3) - (at level 1, c1, c2, c3 at level 8) : type_scope - V8only (at level 200). - -(** First-order quantifiers *) - - (** [ex A P], or simply [exists x, P x], expresses the existence of an - [x] of type [A] which satisfies the predicate [P] ([A] is of type - [Set]). This is existential quantification. *) - - (** [ex2 A P Q], or simply [exists2 x, P x & Q x], expresses the - existence of an [x] of type [A] which satisfies both the predicates - [P] and [Q] *) - - (** Universal quantification (especially first-order one) is normally - written [forall x:A, P x]. For duality with existential quantification, - the construction [all P] is provided too *) - -Inductive ex [A:Type;P:A->Prop] : Prop - := ex_intro : (x:A)(P x)->(ex A P). - -Inductive ex2 [A:Type;P,Q:A->Prop] : Prop - := ex_intro2 : (x:A)(P x)->(Q x)->(ex2 A P Q). - -Definition all := [A:Type][P:A->Prop](x:A)(P x). - -(* Rule order is important to give printing priority to fully typed exists *) - -V7only [ Notation Ex := (ex ?). ]. -Notation "'EX' x | p" := (ex ? [x]p) - (at level 10, p at level 8) : type_scope - V8only "'exists' x , p" (at level 200, x ident, p at level 99). -Notation "'EX' x : t | p" := (ex ? [x:t]p) - (at level 10, p at level 8) : type_scope - V8only "'exists' x : t , p" (at level 200, x ident, p at level 99, format - "'exists' '/ ' x : t , '/ ' p"). - -V7only [ Notation Ex2 := (ex2 ?). ]. -Notation "'EX' x | p & q" := (ex2 ? [x]p [x]q) - (at level 10, p, q at level 8) : type_scope - V8only "'exists2' x , p & q" (at level 200, x ident, p, q at level 99). -Notation "'EX' x : t | p & q" := (ex2 ? [x:t]p [x:t]q) - (at level 10, p, q at level 8) : type_scope - V8only "'exists2' x : t , p & q" - (at level 200, x ident, t at level 200, p, q at level 99, format - "'exists2' '/ ' x : t , '/ ' '[' p & '/' q ']'"). - -V7only [Notation All := (all ?). -Notation "'ALL' x | p" := (all ? [x]p) - (at level 10, p at level 8) : type_scope - V8only (at level 200, x ident, p at level 200). -Notation "'ALL' x : t | p" := (all ? [x:t]p) - (at level 10, p at level 8) : type_scope - V8only (at level 200, x ident, t, p at level 200). -]. - -(** Universal quantification *) - -Section universal_quantification. - - Variable A : Type. - Variable P : A->Prop. - - Theorem inst : (x:A)(all ? [x](P x))->(P x). - Proof. - Unfold all; Auto. - Qed. - - Theorem gen : (B:Prop)(f:(y:A)B->(P y))B->(all A P). - Proof. - Red; Auto. - Qed. - - End universal_quantification. - -(** Equality *) - -(** [eq A x y], or simply [x=y], expresses the (Leibniz') equality - of [x] and [y]. Both [x] and [y] must belong to the same type [A]. - The definition is inductive and states the reflexivity of the equality. - The others properties (symmetry, transitivity, replacement of - equals) are proved below *) - -Inductive eq [A:Type;x:A] : A->Prop - := refl_equal : x = x :> A - -where "x = y :> A" := (!eq A x y) : type_scope. - -Notation "x = y" := (eq ? x y) : type_scope. -Notation "x <> y :> T" := ~ (!eq T x y) : type_scope. -Notation "x <> y" := ~ x=y : type_scope. - -Implicits eq_ind [1]. -Implicits eq_rec [1]. -Implicits eq_rect [1]. -V7only [ -Implicits eq_ind []. -Implicits eq_rec []. -Implicits eq_rect []. -]. - -Hints Resolve I conj or_introl or_intror refl_equal : core v62. -Hints Resolve ex_intro ex_intro2 : core v62. - -Section Logic_lemmas. - - Theorem absurd : (A:Prop)(C:Prop) A -> (not A) -> C. - Proof. - Unfold not; Intros A C h1 h2. - NewDestruct (h2 h1). - Qed. - - Section equality. - Variable A,B : Type. - Variable f : A->B. - Variable x,y,z : A. - - Theorem sym_eq : (eq ? x y) -> (eq ? y x). - Proof. - NewDestruct 1; Trivial. - Defined. - Opaque sym_eq. - - Theorem trans_eq : (eq ? x y) -> (eq ? y z) -> (eq ? x z). - Proof. - NewDestruct 2; Trivial. - Defined. - Opaque trans_eq. - - Theorem f_equal : (eq ? x y) -> (eq ? (f x) (f y)). - Proof. - NewDestruct 1; Trivial. - Defined. - Opaque f_equal. - - Theorem sym_not_eq : (not (eq ? x y)) -> (not (eq ? y x)). - Proof. - Red; Intros h1 h2; Apply h1; NewDestruct h2; Trivial. - Qed. - - Definition sym_equal := sym_eq. - Definition sym_not_equal := sym_not_eq. - Definition trans_equal := trans_eq. - - End equality. - -(* Is now a primitive principle - Theorem eq_rect: (A:Type)(x:A)(P:A->Type)(P x)->(y:A)(eq ? x y)->(P y). - Proof. - Intros. - Cut (identity A x y). - NewDestruct 1; Auto. - NewDestruct H; Auto. - Qed. -*) - - Definition eq_ind_r : (A:Type)(x:A)(P:A->Prop)(P x)->(y:A)(eq ? y x)->(P y). - Intros A x P H y H0; Elim sym_eq with 1:= H0; Assumption. - Defined. - - Definition eq_rec_r : (A:Type)(x:A)(P:A->Set)(P x)->(y:A)(eq ? y x)->(P y). - Intros A x P H y H0; Elim sym_eq with 1:= H0; Assumption. - Defined. - - Definition eq_rect_r : (A:Type)(x:A)(P:A->Type)(P x)->(y:A)(eq ? y x)->(P y). - Intros A x P H y H0; Elim sym_eq with 1:= H0; Assumption. - Defined. -End Logic_lemmas. - -Theorem f_equal2 : (A1,A2,B:Type)(f:A1->A2->B)(x1,y1:A1)(x2,y2:A2) - (eq ? x1 y1) -> (eq ? x2 y2) -> (eq ? (f x1 x2) (f y1 y2)). -Proof. - NewDestruct 1; NewDestruct 1; Reflexivity. -Qed. - -Theorem f_equal3 : (A1,A2,A3,B:Type)(f:A1->A2->A3->B)(x1,y1:A1)(x2,y2:A2) - (x3,y3:A3)(eq ? x1 y1) -> (eq ? x2 y2) -> (eq ? x3 y3) - -> (eq ? (f x1 x2 x3) (f y1 y2 y3)). -Proof. - NewDestruct 1; NewDestruct 1; NewDestruct 1; Reflexivity. -Qed. - -Theorem f_equal4 : (A1,A2,A3,A4,B:Type)(f:A1->A2->A3->A4->B) - (x1,y1:A1)(x2,y2:A2)(x3,y3:A3)(x4,y4:A4) - (eq ? x1 y1) -> (eq ? x2 y2) -> (eq ? x3 y3) -> (eq ? x4 y4) - -> (eq ? (f x1 x2 x3 x4) (f y1 y2 y3 y4)). -Proof. - NewDestruct 1; NewDestruct 1; NewDestruct 1; NewDestruct 1; Reflexivity. -Qed. - -Theorem f_equal5 : (A1,A2,A3,A4,A5,B:Type)(f:A1->A2->A3->A4->A5->B) - (x1,y1:A1)(x2,y2:A2)(x3,y3:A3)(x4,y4:A4)(x5,y5:A5) - (eq ? x1 y1) -> (eq ? x2 y2) -> (eq ? x3 y3) -> (eq ? x4 y4) -> (eq ? x5 y5) - -> (eq ? (f x1 x2 x3 x4 x5) (f y1 y2 y3 y4 y5)). -Proof. - NewDestruct 1; NewDestruct 1; NewDestruct 1; NewDestruct 1; NewDestruct 1; - Reflexivity. -Qed. - -Hints Immediate sym_eq sym_not_eq : core v62. - -V7only[ -(** Parsing only of things in [Logic.v] *) -Notation "< A > 'All' ( P )" :=(all A P) (A annot, at level 1, only parsing). -Notation "< A > x = y" := (eq A x y) - (A annot, at level 1, x at level 0, only parsing). -Notation "< A > x <> y" := ~(eq A x y) - (A annot, at level 1, x at level 0, only parsing). -]. diff --git a/theories7/Init/Logic_Type.v b/theories7/Init/Logic_Type.v deleted file mode 100755 index 793b671c..00000000 --- a/theories7/Init/Logic_Type.v +++ /dev/null @@ -1,304 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: Logic_Type.v,v 1.3.2.1 2004/07/16 19:31:26 herbelin Exp $ i*) - -Set Implicit Arguments. -V7only [Unset Implicit Arguments.]. - -(** This module defines quantification on the world [Type] - ([Logic.v] was defining it on the world [Set]) *) - -Require Datatypes. -Require Export Logic. - -V7only [ -(* -(** [allT A P], or simply [(ALLT x | P(x))], stands for [(x:A)(P x)] - when [A] is of type [Type] *) - -Definition allT := [A:Type][P:A->Prop](x:A)(P x). -*) - -Notation allT := all (only parsing). -Notation inst := Logic.inst (only parsing). -Notation gen := Logic.gen (only parsing). - -(* Order is important to give printing priority to fully typed ALL and EX *) - -Notation AllT := (all ?). -Notation "'ALLT' x | p" := (all ? [x]p) (at level 10, p at level 8). -Notation "'ALLT' x : t | p" := (all ? [x:t]p) (at level 10, p at level 8). - -(* -Section universal_quantification. - -Variable A : Type. -Variable P : A->Prop. - -Theorem inst : (x:A)(allT ? [x](P x))->(P x). -Proof. -Unfold all; Auto. -Qed. - -Theorem gen : (B:Prop)(f:(y:A)B->(P y))B->(allT A P). -Proof. -Red; Auto. -Qed. - -End universal_quantification. -*) - -(* -(** * Existential Quantification *) - -(** [exT A P], or simply [(EXT x | P(x))], stands for the existential - quantification on the predicate [P] when [A] is of type [Type] *) - -(** [exT2 A P Q], or simply [(EXT x | P(x) & Q(x))], stands for the - existential quantification on both [P] and [Q] when [A] is of - type [Type] *) -Inductive exT [A:Type;P:A->Prop] : Prop - := exT_intro : (x:A)(P x)->(exT A P). -*) - -Notation exT := ex (only parsing). -Notation exT_intro := ex_intro (only parsing). -Notation exT_ind := ex_ind (only parsing). - -Notation ExT := (ex ?). -Notation "'EXT' x | p" := (ex ? [x]p) - (at level 10, p at level 8, only parsing). -Notation "'EXT' x : t | p" := (ex ? [x:t]p) - (at level 10, p at level 8, only parsing). - -(* -Inductive exT2 [A:Type;P,Q:A->Prop] : Prop - := exT_intro2 : (x:A)(P x)->(Q x)->(exT2 A P Q). -*) - -Notation exT2 := ex2 (only parsing). -Notation exT_intro2 := ex_intro2 (only parsing). -Notation exT2_ind := ex2_ind (only parsing). - -Notation ExT2 := (ex2 ?). -Notation "'EXT' x | p & q" := (ex2 ? [x]p [x]q) - (at level 10, p, q at level 8). -Notation "'EXT' x : t | p & q" := (ex2 ? [x:t]p [x:t]q) - (at level 10, p, q at level 8). - -(* -(** Leibniz equality : [A:Type][x,y:A] (P:A->Prop)(P x)->(P y) - - [eqT A x y], or simply [x==y], is Leibniz' equality when [A] is of - type [Type]. This equality satisfies reflexivity (by definition), - symmetry, transitivity and stability by congruence *) - - -Inductive eqT [A:Type;x:A] : A -> Prop - := refl_eqT : (eqT A x x). - -Hints Resolve refl_eqT (* exT_intro2 exT_intro *) : core v62. -*) - -Notation eqT := eq (only parsing). -Notation refl_eqT := refl_equal (only parsing). -Notation eqT_ind := eq_ind (only parsing). -Notation eqT_rect := eq_rect (only parsing). -Notation eqT_rec := eq_rec (only parsing). - -Notation "x == y" := (eq ? x y) (at level 5, no associativity, only parsing). - -(** Parsing only of things in [Logic_type.v] *) - -Notation "< A > x == y" := (eq A x y) - (A annot, at level 1, x at level 0, only parsing). - -(* -Section Equality_is_a_congruence. - - Variables A,B : Type. - Variable f : A->B. - - Variable x,y,z : A. - - Lemma sym_eqT : (eqT ? x y) -> (eqT ? y x). - Proof. - NewDestruct 1; Trivial. - Qed. - - Lemma trans_eqT : (eqT ? x y) -> (eqT ? y z) -> (eqT ? x z). - Proof. - NewDestruct 2; Trivial. - Qed. - - Lemma congr_eqT : (eqT ? x y)->(eqT ? (f x) (f y)). - Proof. - NewDestruct 1; Trivial. - Qed. - - Lemma sym_not_eqT : ~(eqT ? x y) -> ~(eqT ? y x). - Proof. - Red; Intros H H'; Apply H; NewDestruct H'; Trivial. - Qed. - -End Equality_is_a_congruence. -*) - -Notation sym_eqT := sym_eq (only parsing). -Notation trans_eqT := trans_eq (only parsing). -Notation congr_eqT := f_equal (only parsing). -Notation sym_not_eqT := sym_not_eq (only parsing). - -(* -Hints Immediate sym_eqT sym_not_eqT : core v62. -*) - -(** This states the replacement of equals by equals *) - -(* -Definition eqT_ind_r : (A:Type)(x:A)(P:A->Prop)(P x)->(y:A)(eqT ? y x)->(P y). -Intros A x P H y H0; Case sym_eqT with 1:=H0; Trivial. -Defined. - -Definition eqT_rec_r : (A:Type)(x:A)(P:A->Set)(P x)->(y:A)(eqT ? y x)->(P y). -Intros A x P H y H0; Case sym_eqT with 1:=H0; Trivial. -Defined. - -Definition eqT_rect_r : (A:Type)(x:A)(P:A->Type)(P x)->(y:A)(eqT ? y x)->(P y). -Intros A x P H y H0; Case sym_eqT with 1:=H0; Trivial. -Defined. -*) - -Notation eqT_ind_r := eq_ind_r (only parsing). -Notation eqT_rec_r := eq_rec_r (only parsing). -Notation eqT_rect_r := eq_rect_r (only parsing). - -(** Some datatypes at the [Type] level *) -(* -Inductive EmptyT: Type :=. -Inductive UnitT : Type := IT : UnitT. -*) - -Notation EmptyT := False (only parsing). -Notation UnitT := unit (only parsing). -Notation IT := tt. -]. -Definition notT := [A:Type] A->EmptyT. - -V7only [ -(** Have you an idea of what means [identityT A a b]? No matter! *) - -(* -Inductive identityT [A:Type; a:A] : A -> Type := - refl_identityT : (identityT A a a). -*) - -Notation identityT := identity (only parsing). -Notation refl_identityT := refl_identity (only parsing). - -Notation "< A > x === y" := (!identityT A x y) - (A annot, at level 1, x at level 0, only parsing) : type_scope. - -Notation "x === y" := (identityT ? x y) - (at level 5, no associativity, only parsing) : type_scope. - -(* -Hints Resolve refl_identityT : core v62. -*) -]. -Section identity_is_a_congruence. - - Variables A,B : Type. - Variable f : A->B. - - Variable x,y,z : A. - - Lemma sym_id : (identityT ? x y) -> (identityT ? y x). - Proof. - NewDestruct 1; Trivial. - Qed. - - Lemma trans_id : (identityT ? x y) -> (identityT ? y z) -> (identityT ? x z). - Proof. - NewDestruct 2; Trivial. - Qed. - - Lemma congr_id : (identityT ? x y)->(identityT ? (f x) (f y)). - Proof. - NewDestruct 1; Trivial. - Qed. - - Lemma sym_not_id : (notT (identityT ? x y)) -> (notT (identityT ? y x)). - Proof. - Red; Intros H H'; Apply H; NewDestruct H'; Trivial. - Qed. - -End identity_is_a_congruence. - -Definition identity_ind_r : - (A:Type) - (a:A) - (P:A->Prop) - (P a)->(y:A)(identityT ? y a)->(P y). - Intros A x P H y H0; Case sym_id with 1:= H0; Trivial. -Defined. - -Definition identity_rec_r : - (A:Type) - (a:A) - (P:A->Set) - (P a)->(y:A)(identityT ? y a)->(P y). - Intros A x P H y H0; Case sym_id with 1:= H0; Trivial. -Defined. - -Definition identity_rect_r : - (A:Type) - (a:A) - (P:A->Type) - (P a)->(y:A)(identityT ? y a)->(P y). - Intros A x P H y H0; Case sym_id with 1:= H0; Trivial. -Defined. - -V7only [ -Notation sym_idT := sym_id (only parsing). -Notation trans_idT := trans_id (only parsing). -Notation congr_idT := congr_id (only parsing). -Notation sym_not_idT := sym_not_id (only parsing). -Notation identityT_ind_r := identity_ind_r (only parsing). -Notation identityT_rec_r := identity_rec_r (only parsing). -Notation identityT_rect_r := identity_rect_r (only parsing). -]. -Inductive prodT [A,B:Type] : Type := pairT : A -> B -> (prodT A B). - -Section prodT_proj. - - Variables A, B : Type. - - Definition fstT := [H:(prodT A B)]Cases H of (pairT x _) => x end. - Definition sndT := [H:(prodT A B)]Cases H of (pairT _ y) => y end. - -End prodT_proj. - -Definition prodT_uncurry : (A,B,C:Type)((prodT A B)->C)->A->B->C := - [A,B,C:Type; f:((prodT A B)->C); x:A; y:B] - (f (pairT A B x y)). - -Definition prodT_curry : (A,B,C:Type)(A->B->C)->(prodT A B)->C := - [A,B,C:Type; f:(A->B->C); p:(prodT A B)] - Cases p of - | (pairT x y) => (f x y) - end. - -Hints Immediate sym_id sym_not_id : core v62. - -V7only [ -Implicits fstT [1 2]. -Implicits sndT [1 2]. -Implicits pairT [1 2]. -]. diff --git a/theories7/Init/Notations.v b/theories7/Init/Notations.v deleted file mode 100644 index 34bfcbfa..00000000 --- a/theories7/Init/Notations.v +++ /dev/null @@ -1,94 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: Notations.v,v 1.5.2.1 2004/07/16 19:31:26 herbelin Exp $ i*) - -(** These are the notations whose level and associativity is imposed by Coq *) - -(** Notations for logical connectives *) - -Uninterpreted Notation "x <-> y" (at level 8, right associativity) - V8only (at level 95, no associativity). -Uninterpreted Notation "x /\ y" (at level 6, right associativity) - V8only (at level 80, right associativity). -Uninterpreted Notation "x \/ y" (at level 7, right associativity) - V8only (at level 85, right associativity). -Uninterpreted Notation "~ x" (at level 5, right associativity) - V8only (at level 75, right associativity). - -(** Notations for equality and inequalities *) - -Uninterpreted Notation "x = y :> T" - (at level 5, y at next level, no associativity). -Uninterpreted Notation "x = y" - (at level 5, no associativity). -Uninterpreted Notation "x = y = z" - (at level 5, no associativity, y at next level). - -Uninterpreted Notation "x <> y :> T" - (at level 5, y at next level, no associativity). -Uninterpreted Notation "x <> y" - (at level 5, no associativity). - -Uninterpreted V8Notation "x <= y" (at level 70, no associativity). -Uninterpreted V8Notation "x < y" (at level 70, no associativity). -Uninterpreted V8Notation "x >= y" (at level 70, no associativity). -Uninterpreted V8Notation "x > y" (at level 70, no associativity). - -Uninterpreted V8Notation "x <= y <= z" (at level 70, y at next level). -Uninterpreted V8Notation "x <= y < z" (at level 70, y at next level). -Uninterpreted V8Notation "x < y < z" (at level 70, y at next level). -Uninterpreted V8Notation "x < y <= z" (at level 70, y at next level). - -(** Arithmetical notations (also used for type constructors) *) - -Uninterpreted Notation "x + y" (at level 4, left associativity). -Uninterpreted V8Notation "x - y" (at level 50, left associativity). -Uninterpreted Notation "x * y" (at level 3, right associativity) - V8only (at level 40, left associativity). -Uninterpreted V8Notation "x / y" (at level 40, left associativity). -Uninterpreted V8Notation "- x" (at level 35, right associativity). -Uninterpreted V8Notation "/ x" (at level 35, right associativity). -Uninterpreted V8Notation "x ^ y" (at level 30, right associativity). - -(** Notations for pairs *) - -V7only [Uninterpreted Notation "( x , y )" (at level 0) V8only.]. -Uninterpreted V8Notation "( x , y , .. , z )" (at level 0). - -(** Notation "{ x }" is reserved and has a special status as component - of other notations; it is at level 1 to factor with {x:A|P} etc *) - -Uninterpreted Notation "{ x }" (at level 1) - V8only (at level 0, x at level 99). - -(** Notations for sum-types *) - -Uninterpreted Notation "{ A } + { B }" (at level 4, left associativity) - V8only (at level 50, left associativity). - -Uninterpreted Notation "A + { B }" (at level 4, left associativity) - V8only (at level 50, left associativity). - -(** Notations for sigma-types or subsets *) - -Uninterpreted Notation "{ x : A | P }" (at level 1) - V8only (at level 0, x at level 99). -Uninterpreted Notation "{ x : A | P & Q }" (at level 1) - V8only (at level 0, x at level 99). - -Uninterpreted Notation "{ x : A & P }" (at level 1) - V8only (at level 0, x at level 99). -Uninterpreted Notation "{ x : A & P & Q }" (at level 1) - V8only (at level 0, x at level 99). - -Delimits Scope type_scope with type. -Delimits Scope core_scope with core. - -Open Scope core_scope. -Open Scope type_scope. diff --git a/theories7/Init/Peano.v b/theories7/Init/Peano.v deleted file mode 100755 index 72d19399..00000000 --- a/theories7/Init/Peano.v +++ /dev/null @@ -1,218 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: Peano.v,v 1.1.2.1 2004/07/16 19:31:26 herbelin Exp $ i*) - -(** Natural numbers [nat] built from [O] and [S] are defined in Datatypes.v *) - -(** This module defines the following operations on natural numbers : - - predecessor [pred] - - addition [plus] - - multiplication [mult] - - less or equal order [le] - - less [lt] - - greater or equal [ge] - - greater [gt] - - This module states various lemmas and theorems about natural numbers, - including Peano's axioms of arithmetic (in Coq, these are in fact provable) - Case analysis on [nat] and induction on [nat * nat] are provided too *) - -Require Notations. -Require Datatypes. -Require Logic. - -Open Scope nat_scope. - -Definition eq_S := (f_equal nat nat S). - -Hint eq_S : v62 := Resolve (f_equal nat nat S). -Hint eq_nat_unary : core := Resolve (f_equal nat). - -(** The predecessor function *) - -Definition pred : nat->nat := [n:nat](Cases n of O => O | (S u) => u end). -Hint eq_pred : v62 := Resolve (f_equal nat nat pred). - -Theorem pred_Sn : (m:nat) m=(pred (S m)). -Proof. - Auto. -Qed. - -Theorem eq_add_S : (n,m:nat) (S n)=(S m) -> n=m. -Proof. - Intros n m H ; Change (pred (S n))=(pred (S m)); Auto. -Qed. - -Hints Immediate eq_add_S : core v62. - -(** A consequence of the previous axioms *) - -Theorem not_eq_S : (n,m:nat) ~(n=m) -> ~((S n)=(S m)). -Proof. - Red; Auto. -Qed. -Hints Resolve not_eq_S : core v62. - -Definition IsSucc : nat->Prop - := [n:nat]Cases n of O => False | (S p) => True end. - - -Theorem O_S : (n:nat)~(O=(S n)). -Proof. - Red;Intros n H. - Change (IsSucc O). - Rewrite <- (sym_eq nat O (S n));[Exact I | Assumption]. -Qed. -Hints Resolve O_S : core v62. - -Theorem n_Sn : (n:nat) ~(n=(S n)). -Proof. - NewInduction n ; Auto. -Qed. -Hints Resolve n_Sn : core v62. - -(** Addition *) - -Fixpoint plus [n:nat] : nat -> nat := - [m:nat]Cases n of - O => m - | (S p) => (S (plus p m)) end. -Hint eq_plus : v62 := Resolve (f_equal2 nat nat nat plus). -Hint eq_nat_binary : core := Resolve (f_equal2 nat nat). - -V8Infix "+" plus : nat_scope. - -Lemma plus_n_O : (n:nat) n=(plus n O). -Proof. - NewInduction n ; Simpl ; Auto. -Qed. -Hints Resolve plus_n_O : core v62. - -Lemma plus_O_n : (n:nat) (plus O n)=n. -Proof. - Auto. -Qed. - -Lemma plus_n_Sm : (n,m:nat) (S (plus n m))=(plus n (S m)). -Proof. - Intros n m; NewInduction n; Simpl; Auto. -Qed. -Hints Resolve plus_n_Sm : core v62. - -Lemma plus_Sn_m : (n,m:nat)(plus (S n) m)=(S (plus n m)). -Proof. - Auto. -Qed. - -(** Multiplication *) - -Fixpoint mult [n:nat] : nat -> nat := - [m:nat]Cases n of O => O - | (S p) => (plus m (mult p m)) end. -Hint eq_mult : core v62 := Resolve (f_equal2 nat nat nat mult). - -V8Infix "*" mult : nat_scope. - -Lemma mult_n_O : (n:nat) O=(mult n O). -Proof. - NewInduction n; Simpl; Auto. -Qed. -Hints Resolve mult_n_O : core v62. - -Lemma mult_n_Sm : (n,m:nat) (plus (mult n m) n)=(mult n (S m)). -Proof. - Intros; NewInduction n as [|p H]; Simpl; Auto. - NewDestruct H; Rewrite <- plus_n_Sm; Apply (f_equal nat nat S). - Pattern 1 3 m; Elim m; Simpl; Auto. -Qed. -Hints Resolve mult_n_Sm : core v62. - -(** Definition of subtraction on [nat] : [m-n] is [0] if [n>=m] *) - -Fixpoint minus [n:nat] : nat -> nat := - [m:nat]Cases n m of - O _ => O - | (S k) O => (S k) - | (S k) (S l) => (minus k l) - end. - -V8Infix "-" minus : nat_scope. - -(** Definition of the usual orders, the basic properties of [le] and [lt] - can be found in files Le and Lt *) - -(** An inductive definition to define the order *) - -Inductive le [n:nat] : nat -> Prop - := le_n : (le n n) - | le_S : (m:nat)(le n m)->(le n (S m)). - -V8Infix "<=" le : nat_scope. - -Hint constr_le : core v62 := Constructors le. -(*i equivalent to : "Hints Resolve le_n le_S : core v62." i*) - -Definition lt := [n,m:nat](le (S n) m). -Hints Unfold lt : core v62. - -V8Infix "<" lt : nat_scope. - -Definition ge := [n,m:nat](le m n). -Hints Unfold ge : core v62. - -V8Infix ">=" ge : nat_scope. - -Definition gt := [n,m:nat](lt m n). -Hints Unfold gt : core v62. - -V8Infix ">" gt : nat_scope. - -V8Notation "x <= y <= z" := (le x y)/\(le y z) : nat_scope. -V8Notation "x <= y < z" := (le x y)/\(lt y z) : nat_scope. -V8Notation "x < y < z" := (lt x y)/\(lt y z) : nat_scope. -V8Notation "x < y <= z" := (lt x y)/\(le y z) : nat_scope. - -(** Pattern-Matching on natural numbers *) - -Theorem nat_case : (n:nat)(P:nat->Prop)(P O)->((m:nat)(P (S m)))->(P n). -Proof. - NewInduction n ; Auto. -Qed. - -(** Principle of double induction *) - -Theorem nat_double_ind : (R:nat->nat->Prop) - ((n:nat)(R O n)) -> ((n:nat)(R (S n) O)) - -> ((n,m:nat)(R n m)->(R (S n) (S m))) - -> (n,m:nat)(R n m). -Proof. - NewInduction n; Auto. - NewDestruct m; Auto. -Qed. - -(** Notations *) -V7only[ -Syntax constr - level 0: - S [ (S $p) ] -> [$p:"nat_printer":9] - | O [ O ] -> ["(0)"]. -]. - -V7only [ -(* For parsing/printing based on scopes *) -Module nat_scope. -Infix 4 "+" plus : nat_scope. -Infix 3 "*" mult : nat_scope. -Infix 4 "-" minus : nat_scope. -Infix NONA 5 "<=" le : nat_scope. -Infix NONA 5 "<" lt : nat_scope. -Infix NONA 5 ">=" ge : nat_scope. -Infix NONA 5 ">" gt : nat_scope. -End nat_scope. -]. diff --git a/theories7/Init/Prelude.v b/theories7/Init/Prelude.v deleted file mode 100755 index 2752f462..00000000 --- a/theories7/Init/Prelude.v +++ /dev/null @@ -1,16 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: Prelude.v,v 1.1.2.1 2004/07/16 19:31:26 herbelin Exp $ i*) - -Require Export Notations. -Require Export Logic. -Require Export Datatypes. -Require Export Specif. -Require Export Peano. -Require Export Wf. diff --git a/theories7/Init/Specif.v b/theories7/Init/Specif.v deleted file mode 100755 index c39e5ed8..00000000 --- a/theories7/Init/Specif.v +++ /dev/null @@ -1,204 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: Specif.v,v 1.2.2.1 2004/07/16 19:31:26 herbelin Exp $ i*) - -Set Implicit Arguments. -V7only [Unset Implicit Arguments.]. - -(** Basic specifications : Sets containing logical information *) - -Require Notations. -Require Datatypes. -Require Logic. - -(** Subsets *) - -(** [(sig A P)], or more suggestively [{x:A | (P x)}], denotes the subset - of elements of the Set [A] which satisfy the predicate [P]. - Similarly [(sig2 A P Q)], or [{x:A | (P x) & (Q x)}], denotes the subset - of elements of the Set [A] which satisfy both [P] and [Q]. *) - -Inductive sig [A:Set;P:A->Prop] : Set - := exist : (x:A)(P x) -> (sig A P). - -Inductive sig2 [A:Set;P,Q:A->Prop] : Set - := exist2 : (x:A)(P x) -> (Q x) -> (sig2 A P Q). - -(** [(sigS A P)], or more suggestively [{x:A & (P x)}], is a subtle variant - of subset where [P] is now of type [Set]. - Similarly for [(sigS2 A P Q)], also written [{x:A & (P x) & (Q x)}]. *) - -Inductive sigS [A:Set;P:A->Set] : Set - := existS : (x:A)(P x) -> (sigS A P). - -Inductive sigS2 [A:Set;P,Q:A->Set] : Set - := existS2 : (x:A)(P x) -> (Q x) -> (sigS2 A P Q). - -Arguments Scope sig [type_scope type_scope]. -Arguments Scope sig2 [type_scope type_scope type_scope]. -Arguments Scope sigS [type_scope type_scope]. -Arguments Scope sigS2 [type_scope type_scope type_scope]. - -Notation "{ x : A | P }" := (sig A [x:A]P) : type_scope. -Notation "{ x : A | P & Q }" := (sig2 A [x:A]P [x:A]Q) : type_scope. -Notation "{ x : A & P }" := (sigS A [x:A]P) : type_scope. -Notation "{ x : A & P & Q }" := (sigS2 A [x:A]P [x:A]Q) : type_scope. - -Add Printing Let sig. -Add Printing Let sig2. -Add Printing Let sigS. -Add Printing Let sigS2. - - -(** Projections of sig *) - -Section Subset_projections. - - Variable A:Set. - Variable P:A->Prop. - - Definition proj1_sig := - [e:(sig A P)]Cases e of (exist a b) => a end. - - Definition proj2_sig := - [e:(sig A P)] - <[e:(sig A P)](P (proj1_sig e))>Cases e of (exist a b) => b end. - -End Subset_projections. - - -(** Projections of sigS *) - -Section Projections. - - Variable A:Set. - Variable P:A->Set. - - (** An element [y] of a subset [{x:A & (P x)}] is the pair of an [a] of - type [A] and of a proof [h] that [a] satisfies [P]. - Then [(projS1 y)] is the witness [a] - and [(projS2 y)] is the proof of [(P a)] *) - - Definition projS1 : (sigS A P) -> A - := [x:(sigS A P)]Cases x of (existS a _) => a end. - Definition projS2 : (x:(sigS A P))(P (projS1 x)) - := [x:(sigS A P)]<[x:(sigS A P)](P (projS1 x))> - Cases x of (existS _ h) => h end. - -End Projections. - - -(** Extended_booleans *) - -Inductive sumbool [A,B:Prop] : Set - := left : A -> {A}+{B} - | right : B -> {A}+{B} - -where "{ A } + { B }" := (sumbool A B) : type_scope. - -Inductive sumor [A:Set;B:Prop] : Set - := inleft : A -> A+{B} - | inright : B -> A+{B} - -where "A + { B }" := (sumor A B) : type_scope. - -(** Choice *) - -Section Choice_lemmas. - - (** The following lemmas state various forms of the axiom of choice *) - - Variables S,S':Set. - Variable R:S->S'->Prop. - Variable R':S->S'->Set. - Variables R1,R2 :S->Prop. - - Lemma Choice : ((x:S)(sig ? [y:S'](R x y))) -> - (sig ? [f:S->S'](z:S)(R z (f z))). - Proof. - Intro H. - Exists [z:S]Cases (H z) of (exist y _) => y end. - Intro z; NewDestruct (H z); Trivial. - Qed. - - Lemma Choice2 : ((x:S)(sigS ? [y:S'](R' x y))) -> - (sigS ? [f:S->S'](z:S)(R' z (f z))). - Proof. - Intro H. - Exists [z:S]Cases (H z) of (existS y _) => y end. - Intro z; NewDestruct (H z); Trivial. - Qed. - - Lemma bool_choice : - ((x:S)(sumbool (R1 x) (R2 x))) -> - (sig ? [f:S->bool] (x:S)( ((f x)=true /\ (R1 x)) - \/ ((f x)=false /\ (R2 x)))). - Proof. - Intro H. - Exists [z:S]Cases (H z) of (left _) => true | (right _) => false end. - Intro z; NewDestruct (H z); Auto. - Qed. - -End Choice_lemmas. - - (** A result of type [(Exc A)] is either a normal value of type [A] or - an [error] : - [Inductive Exc [A:Set] : Set := value : A->(Exc A) | error : (Exc A)] - it is implemented using the option type. *) - -Definition Exc := option. -Definition value := Some. -Definition error := !None. - -Implicits error [1]. - -Definition except := False_rec. (* for compatibility with previous versions *) - -Implicits except [1]. - -V7only [ -Notation Except := (!except ?) (only parsing). -Notation Error := (!error ?) (only parsing). -V7only [Implicits error [].]. -V7only [Implicits except [].]. -]. -Theorem absurd_set : (A:Prop)(C:Set)A->(~A)->C. -Proof. - Intros A C h1 h2. - Apply False_rec. - Apply (h2 h1). -Qed. - -Hints Resolve left right inleft inright : core v62. - -(** Sigma Type at Type level [sigT] *) - -Inductive sigT [A:Type;P:A->Type] : Type - := existT : (x:A)(P x) -> (sigT A P). - -Section projections_sigT. - - Variable A:Type. - Variable P:A->Type. - - Definition projT1 : (sigT A P) -> A - := [H:(sigT A P)]Cases H of (existT x _) => x end. - - Definition projT2 : (x:(sigT A P))(P (projT1 x)) - := [H:(sigT A P)]<[H:(sigT A P)](P (projT1 H))> - Cases H of (existT x h) => h end. - -End projections_sigT. - -V7only [ -Notation ProjS1 := (projS1 ? ?). -Notation ProjS2 := (projS2 ? ?). -Notation Value := (value ?). -]. - diff --git a/theories7/Init/Wf.v b/theories7/Init/Wf.v deleted file mode 100755 index b65057eb..00000000 --- a/theories7/Init/Wf.v +++ /dev/null @@ -1,158 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -Set Implicit Arguments. -V7only [Unset Implicit Arguments.]. - -(*i $Id: Wf.v,v 1.1.2.1 2004/07/16 19:31:26 herbelin Exp $ i*) - -(** This module proves the validity of - - well-founded recursion (also called course of values) - - well-founded induction - - from a well-founded ordering on a given set *) - -Require Notations. -Require Logic. -Require Datatypes. - -(** Well-founded induction principle on Prop *) - -Chapter Well_founded. - - Variable A : Set. - Variable R : A -> A -> Prop. - - (** The accessibility predicate is defined to be non-informative *) - - Inductive Acc : A -> Prop - := Acc_intro : (x:A)((y:A)(R y x)->(Acc y))->(Acc x). - - Lemma Acc_inv : (x:A)(Acc x) -> (y:A)(R y x) -> (Acc y). - NewDestruct 1; Trivial. - Defined. - - (** the informative elimination : - [let Acc_rec F = let rec wf x = F x wf in wf] *) - - Section AccRecType. - Variable P : A -> Type. - Variable F : (x:A)((y:A)(R y x)->(Acc y))->((y:A)(R y x)->(P y))->(P x). - - Fixpoint Acc_rect [x:A;a:(Acc x)] : (P x) - := (F x (Acc_inv x a) ([y:A][h:(R y x)](Acc_rect y (Acc_inv x a y h)))). - - End AccRecType. - - Definition Acc_rec [P:A->Set] := (Acc_rect P). - - (** A simplified version of Acc_rec(t) *) - - Section AccIter. - Variable P : A -> Type. - Variable F : (x:A)((y:A)(R y x)-> (P y))->(P x). - - Fixpoint Acc_iter [x:A;a:(Acc x)] : (P x) - := (F x ([y:A][h:(R y x)](Acc_iter y (Acc_inv x a y h)))). - - End AccIter. - - (** A relation is well-founded if every element is accessible *) - - Definition well_founded := (a:A)(Acc a). - - (** well-founded induction on Set and Prop *) - - Hypothesis Rwf : well_founded. - - Theorem well_founded_induction_type : - (P:A->Type)((x:A)((y:A)(R y x)->(P y))->(P x))->(a:A)(P a). - Proof. - Intros; Apply (Acc_iter P); Auto. - Defined. - - Theorem well_founded_induction : - (P:A->Set)((x:A)((y:A)(R y x)->(P y))->(P x))->(a:A)(P a). - Proof. - Exact [P:A->Set](well_founded_induction_type P). - Defined. - - Theorem well_founded_ind : - (P:A->Prop)((x:A)((y:A)(R y x)->(P y))->(P x))->(a:A)(P a). - Proof. - Exact [P:A->Prop](well_founded_induction_type P). - Defined. - -(** Building fixpoints *) - -Section FixPoint. - -Variable P : A -> Set. -Variable F : (x:A)((y:A)(R y x)->(P y))->(P x). - -Fixpoint Fix_F [x:A;r:(Acc x)] : (P x) := - (F x [y:A][p:(R y x)](Fix_F y (Acc_inv x r y p))). - -Definition fix := [x:A](Fix_F x (Rwf x)). - -(** Proof that [well_founded_induction] satisfies the fixpoint equation. - It requires an extra property of the functional *) - -Hypothesis F_ext : - (x:A)(f,g:(y:A)(R y x)->(P y)) - ((y:A)(p:(R y x))((f y p)=(g y p)))->(F x f)=(F x g). - -Scheme Acc_inv_dep := Induction for Acc Sort Prop. - -Lemma Fix_F_eq - : (x:A)(r:(Acc x)) - (F x [y:A][p:(R y x)](Fix_F y (Acc_inv x r y p)))=(Fix_F x r). -NewDestruct r using Acc_inv_dep; Auto. -Qed. - -Lemma Fix_F_inv : (x:A)(r,s:(Acc x))(Fix_F x r)=(Fix_F x s). -Intro x; NewInduction (Rwf x); Intros. -Rewrite <- (Fix_F_eq x r); Rewrite <- (Fix_F_eq x s); Intros. -Apply F_ext; Auto. -Qed. - - -Lemma Fix_eq : (x:A)(fix x)=(F x [y:A][p:(R y x)](fix y)). -Intro x; Unfold fix. -Rewrite <- (Fix_F_eq x). -Apply F_ext; Intros. -Apply Fix_F_inv. -Qed. - -End FixPoint. - -End Well_founded. - -(** A recursor over pairs *) - -Chapter Well_founded_2. - - Variable A,B : Set. - Variable R : A * B -> A * B -> Prop. - - Variable P : A -> B -> Type. - Variable F : (x:A)(x':B)((y:A)(y':B)(R (y,y') (x,x'))-> (P y y'))->(P x x'). - - Fixpoint Acc_iter_2 [x:A;x':B;a:(Acc ? R (x,x'))] : (P x x') - := (F x x' ([y:A][y':B][h:(R (y,y') (x,x'))](Acc_iter_2 y y' (Acc_inv ? ? (x,x') a (y,y') h)))). - - Hypothesis Rwf : (well_founded ? R). - - Theorem well_founded_induction_type_2 : - ((x:A)(x':B)((y:A)(y':B)(R (y,y') (x,x'))->(P y y'))->(P x x'))->(a:A)(b:B)(P a b). - Proof. - Intros; Apply Acc_iter_2; Auto. - Defined. - -End Well_founded_2. - |