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, 1425 insertions, 0 deletions
diff --git a/theories7/Init/Datatypes.v b/theories7/Init/Datatypes.v new file mode 100755 index 00000000..006ec08e --- /dev/null +++ b/theories7/Init/Datatypes.v @@ -0,0 +1,125 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..6ba9c7a1 --- /dev/null +++ b/theories7/Init/Logic.v @@ -0,0 +1,306 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..793b671c --- /dev/null +++ b/theories7/Init/Logic_Type.v @@ -0,0 +1,304 @@ +(************************************************************************) +(* 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 new file mode 100644 index 00000000..34bfcbfa --- /dev/null +++ b/theories7/Init/Notations.v @@ -0,0 +1,94 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..72d19399 --- /dev/null +++ b/theories7/Init/Peano.v @@ -0,0 +1,218 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..2752f462 --- /dev/null +++ b/theories7/Init/Prelude.v @@ -0,0 +1,16 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..c39e5ed8 --- /dev/null +++ b/theories7/Init/Specif.v @@ -0,0 +1,204 @@ +(************************************************************************) +(* 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 new file mode 100755 index 00000000..b65057eb --- /dev/null +++ b/theories7/Init/Wf.v @@ -0,0 +1,158 @@ +(************************************************************************) +(* 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. + |