diff options
Diffstat (limited to 'theories/Init')
| -rwxr-xr-x | theories/Init/Datatypes.v | 121 | ||||
| -rwxr-xr-x | theories/Init/Logic.v | 279 | ||||
| -rwxr-xr-x | theories/Init/Logic_Type.v | 89 | ||||
| -rw-r--r-- | theories/Init/Notations.v | 78 | ||||
| -rwxr-xr-x | theories/Init/Peano.v | 210 | ||||
| -rwxr-xr-x | theories/Init/Prelude.v | 16 | ||||
| -rwxr-xr-x | theories/Init/Specif.v | 212 | ||||
| -rwxr-xr-x | theories/Init/Wf.v | 171 |
8 files changed, 1176 insertions, 0 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v new file mode 100755 index 00000000..6aeabe13 --- /dev/null +++ b/theories/Init/Datatypes.v @@ -0,0 +1,121 @@ +(************************************************************************) +(* 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.26.2.1 2004/07/16 19:31:03 herbelin Exp $ i*) + +Require Import Notations. +Require Import Logic. + +Set 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. + +Delimit 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 a. +Hint Resolve refl_identity: core v62. + +Implicit Arguments identity_ind [A]. +Implicit Arguments identity_rec [A]. +Implicit Arguments identity_rect [A]. + +(** [option A] is the extension of A with a dummy element None *) + +Inductive option (A:Set) : Set := + | Some : A -> option A + | None : option A. + +Implicit Arguments None [A]. + +(** [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. +Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope. + +Section projections. + Variables A B : Set. + Definition fst (p:A * B) := match p with + | (x, y) => x + end. + Definition snd (p:A * B) := match p with + | (x, y) => y + end. +End projections. + +Hint Resolve pair inl inr: core v62. + +Lemma surjective_pairing : + forall (A B:Set) (p:A * B), p = pair (fst p) (snd p). +Proof. +destruct p; reflexivity. +Qed. + +Lemma injective_projections : + forall (A B:Set) (p1 p2:A * B), + fst p1 = fst p2 -> snd p1 = snd p2 -> p1 = p2. +Proof. +destruct p1; destruct p2; simpl in |- *; intros Hfst Hsnd. +rewrite Hfst; rewrite Hsnd; reflexivity. +Qed. + + +(** Comparison *) + +Inductive comparison : Set := + | Eq : comparison + | Lt : comparison + | Gt : comparison. + +Definition CompOpp (r:comparison) := + match r with + | Eq => Eq + | Lt => Gt + | Gt => Lt + end. diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v new file mode 100755 index 00000000..bae8d4a1 --- /dev/null +++ b/theories/Init/Logic.v @@ -0,0 +1,279 @@ +(************************************************************************) +(* 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.29.2.1 2004/07/16 19:31:03 herbelin Exp $ i*) + +Set Implicit Arguments. + +Require Import Notations. + +(** * Propositional connectives *) + +(** [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. + +Hint Unfold not: core. + +Inductive and (A B:Prop) : Prop := + conj : A -> B -> A /\ B + where "A /\ B" := (and A B) : type_scope. + + +Section Conjunction. + + (** [and A B], written [A /\ B], is the conjunction of [A] and [B] + + [conj 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 : A /\ B -> A. + Proof. + destruct 1; trivial. + Qed. + + Theorem proj2 : A /\ B -> B. + Proof. + destruct 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) := (A -> B) /\ (B -> A). + +Notation "A <-> B" := (iff A B) : type_scope. + +Section Equivalence. + +Theorem iff_refl : forall A:Prop, A <-> A. + Proof. + split; auto. + Qed. + +Theorem iff_trans : forall A B C:Prop, (A <-> B) -> (B <-> C) -> (A <-> C). + Proof. + intros A B C [H1 H2] [H3 H4]; split; auto. + Qed. + +Theorem iff_sym : forall A B:Prop, (A <-> B) -> (B <-> A). + Proof. + intros A B [H1 H2]; split; auto. + Qed. + +End Equivalence. + +(** [(IF_then_else P Q R)], written [IF P then Q else R] denotes + either [P] and [Q], or [~P] and [Q] *) + +Definition IF_then_else (P Q R:Prop) := P /\ Q \/ ~ P /\ R. + +Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3) + (at level 200) : type_scope. + +(** * 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 : forall x:A, P x -> ex (A:=A) P. + +Inductive ex2 (A:Type) (P Q:A -> Prop) : Prop := + ex_intro2 : forall x:A, P x -> Q x -> ex2 (A:=A) P Q. + +Definition all (A:Type) (P:A -> Prop) := forall x:A, P x. + +(* Rule order is important to give printing priority to fully typed exists *) + +Notation "'exists' x , p" := (ex (fun x => p)) + (at level 200, x ident) : type_scope. +Notation "'exists' x : t , p" := (ex (fun x:t => p)) + (at level 200, x ident, format "'exists' '/ ' x : t , '/ ' p") + : type_scope. + +Notation "'exists2' x , p & q" := (ex2 (fun x => p) (fun x => q)) + (at level 200, x ident, p at level 200) : type_scope. +Notation "'exists2' x : t , p & q" := (ex2 (fun x:t => p) (fun x:t => q)) + (at level 200, x ident, t at level 200, p at level 200, + format "'exists2' '/ ' x : t , '/ ' '[' p & '/' q ']'") + : type_scope. + + +(** Derived rules for universal quantification *) + +Section universal_quantification. + + Variable A : Type. + Variable P : A -> Prop. + + Theorem inst : forall x:A, all (fun x => P x) -> P x. + Proof. + unfold all in |- *; auto. + Qed. + + Theorem gen : forall (B:Prop) (f:forall y:A, B -> P y), B -> all P. + Proof. + red in |- *; auto. + Qed. + +End universal_quantification. + +(** * Equality *) + +(** [eq 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. The type of [x] and [y] can be made explicit + using the notation [x = y :> A] *) + +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" := (x = y :>_) : type_scope. +Notation "x <> y :> T" := (~ x = y :>T) : type_scope. +Notation "x <> y" := (x <> y :>_) : type_scope. + +Implicit Arguments eq_ind [A]. +Implicit Arguments eq_rec [A]. +Implicit Arguments eq_rect [A]. + +Hint Resolve I conj or_introl or_intror refl_equal: core v62. +Hint Resolve ex_intro ex_intro2: core v62. + +Section Logic_lemmas. + + Theorem absurd : forall A C:Prop, A -> ~ A -> C. + Proof. + unfold not in |- *; intros A C h1 h2. + destruct (h2 h1). + Qed. + + Section equality. + Variables A B : Type. + Variable f : A -> B. + Variables x y z : A. + + Theorem sym_eq : x = y -> y = x. + Proof. + destruct 1; trivial. + Defined. + Opaque sym_eq. + + Theorem trans_eq : x = y -> y = z -> x = z. + Proof. + destruct 2; trivial. + Defined. + Opaque trans_eq. + + Theorem f_equal : x = y -> f x = f y. + Proof. + destruct 1; trivial. + Defined. + Opaque f_equal. + + Theorem sym_not_eq : x <> y -> y <> x. + Proof. + red in |- *; intros h1 h2; apply h1; destruct 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 : + forall (A:Type) (x:A) (P:A -> Prop), P x -> forall y:A, y = x -> P y. + intros A x P H y H0; elim sym_eq with (1 := H0); assumption. + Defined. + + Definition eq_rec_r : + forall (A:Type) (x:A) (P:A -> Set), P x -> forall y:A, y = x -> P y. + intros A x P H y H0; elim sym_eq with (1 := H0); assumption. + Defined. + + Definition eq_rect_r : + forall (A:Type) (x:A) (P:A -> Type), P x -> forall y:A, 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 : + forall (A1 A2 B:Type) (f:A1 -> A2 -> B) (x1 y1:A1) + (x2 y2:A2), x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2. +Proof. + destruct 1; destruct 1; reflexivity. +Qed. + +Theorem f_equal3 : + forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B) (x1 y1:A1) + (x2 y2:A2) (x3 y3:A3), + x1 = y1 -> x2 = y2 -> x3 = y3 -> f x1 x2 x3 = f y1 y2 y3. +Proof. + destruct 1; destruct 1; destruct 1; reflexivity. +Qed. + +Theorem f_equal4 : + forall (A1 A2 A3 A4 B:Type) (f:A1 -> A2 -> A3 -> A4 -> B) + (x1 y1:A1) (x2 y2:A2) (x3 y3:A3) (x4 y4:A4), + x1 = y1 -> x2 = y2 -> x3 = y3 -> x4 = y4 -> f x1 x2 x3 x4 = f y1 y2 y3 y4. +Proof. + destruct 1; destruct 1; destruct 1; destruct 1; reflexivity. +Qed. + +Theorem f_equal5 : + forall (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), + x1 = y1 -> + x2 = y2 -> + x3 = y3 -> x4 = y4 -> x5 = y5 -> f x1 x2 x3 x4 x5 = f y1 y2 y3 y4 y5. +Proof. + destruct 1; destruct 1; destruct 1; destruct 1; destruct 1; reflexivity. +Qed. + +Hint Immediate sym_eq sym_not_eq: core v62. diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v new file mode 100755 index 00000000..0e62e842 --- /dev/null +++ b/theories/Init/Logic_Type.v @@ -0,0 +1,89 @@ +(************************************************************************) +(* 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.19.2.1 2004/07/16 19:31:03 herbelin Exp $ i*) + +Set Implicit Arguments. + +(** This module defines quantification on the world [Type] + ([Logic.v] was defining it on the world [Set]) *) + +Require Import Datatypes. +Require Export Logic. + +Definition notT (A:Type) := A -> False. + +Section identity_is_a_congruence. + + Variables A B : Type. + Variable f : A -> B. + + Variables x y z : A. + + Lemma sym_id : identity x y -> identity y x. + Proof. + destruct 1; trivial. + Qed. + + Lemma trans_id : identity x y -> identity y z -> identity x z. + Proof. + destruct 2; trivial. + Qed. + + Lemma congr_id : identity x y -> identity (f x) (f y). + Proof. + destruct 1; trivial. + Qed. + + Lemma sym_not_id : notT (identity x y) -> notT (identity y x). + Proof. + red in |- *; intros H H'; apply H; destruct H'; trivial. + Qed. + +End identity_is_a_congruence. + +Definition identity_ind_r : + forall (A:Type) (a:A) (P:A -> Prop), P a -> forall y:A, identity y a -> P y. + intros A x P H y H0; case sym_id with (1 := H0); trivial. +Defined. + +Definition identity_rec_r : + forall (A:Type) (a:A) (P:A -> Set), P a -> forall y:A, identity y a -> P y. + intros A x P H y H0; case sym_id with (1 := H0); trivial. +Defined. + +Definition identity_rect_r : + forall (A:Type) (a:A) (P:A -> Type), P a -> forall y:A, identity y a -> P y. + intros A x P H y H0; case sym_id with (1 := H0); trivial. +Defined. + +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) := match H with + | pairT x _ => x + end. + Definition sndT (H:prodT A B) := match H with + | pairT _ y => y + end. + +End prodT_proj. + +Definition prodT_uncurry (A B C:Type) (f:prodT A B -> C) + (x:A) (y:B) : C := f (pairT x y). + +Definition prodT_curry (A B C:Type) (f:A -> B -> C) + (p:prodT A B) : C := match p with + | pairT x y => f x y + end. + +Hint Immediate sym_id sym_not_id: core v62. diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v new file mode 100644 index 00000000..2e7cb1fc --- /dev/null +++ b/theories/Init/Notations.v @@ -0,0 +1,78 @@ +(************************************************************************) +(* 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.24.2.1 2004/07/16 19:31:03 herbelin Exp $ i*) + +(** These are the notations whose level and associativity is imposed by Coq *) + +(** Notations for logical connectives *) + +Reserved Notation "x <-> y" (at level 95, no associativity). +Reserved Notation "x /\ y" (at level 80, right associativity). +Reserved Notation "x \/ y" (at level 85, right associativity). +Reserved Notation "~ x" (at level 75, right associativity). + +(** Notations for equality and inequalities *) + +Reserved Notation "x = y :> T" +(at level 70, y at next level, no associativity). +Reserved Notation "x = y" (at level 70, no associativity). +Reserved Notation "x = y = z" +(at level 70, no associativity, y at next level). + +Reserved Notation "x <> y :> T" +(at level 70, y at next level, no associativity). +Reserved Notation "x <> y" (at level 70, no associativity). + +Reserved Notation "x <= y" (at level 70, no associativity). +Reserved Notation "x < y" (at level 70, no associativity). +Reserved Notation "x >= y" (at level 70, no associativity). +Reserved Notation "x > y" (at level 70, no associativity). + +Reserved Notation "x <= y <= z" (at level 70, y at next level). +Reserved Notation "x <= y < z" (at level 70, y at next level). +Reserved Notation "x < y < z" (at level 70, y at next level). +Reserved Notation "x < y <= z" (at level 70, y at next level). + +(** Arithmetical notations (also used for type constructors) *) + +Reserved Notation "x + y" (at level 50, left associativity). +Reserved Notation "x - y" (at level 50, left associativity). +Reserved Notation "x * y" (at level 40, left associativity). +Reserved Notation "x / y" (at level 40, left associativity). +Reserved Notation "- x" (at level 35, right associativity). +Reserved Notation "/ x" (at level 35, right associativity). +Reserved Notation "x ^ y" (at level 30, right associativity). + +(** Notations for pairs *) + +Reserved Notation "( x , y , .. , z )" (at level 0). + +(** Notation "{ x }" is reserved and has a special status as component + of other notations; it is at level 0 to factor with {x:A|P} etc *) + +Reserved Notation "{ x }" (at level 0, x at level 99). + +(** Notations for sum-types *) + +Reserved Notation "{ A } + { B }" (at level 50, left associativity). +Reserved Notation "A + { B }" (at level 50, left associativity). + +(** Notations for sigma-types or subsets *) + +Reserved Notation "{ x : A | P }" (at level 0, x at level 99). +Reserved Notation "{ x : A | P & Q }" (at level 0, x at level 99). + +Reserved Notation "{ x : A & P }" (at level 0, x at level 99). +Reserved Notation "{ x : A & P & Q }" (at level 0, x at level 99). + +Delimit Scope type_scope with type. +Delimit Scope core_scope with core. + +Open Scope core_scope. +Open Scope type_scope. diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v new file mode 100755 index 00000000..789a020f --- /dev/null +++ b/theories/Init/Peano.v @@ -0,0 +1,210 @@ +(************************************************************************) +(* 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.23.2.1 2004/07/16 19:31:03 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 Import Notations. +Require Import Datatypes. +Require Import Logic. + +Open Scope nat_scope. + +Definition eq_S := f_equal S. + +Hint Resolve (f_equal S): v62. +Hint Resolve (f_equal (A:=nat)): core. + +(** The predecessor function *) + +Definition pred (n:nat) : nat := match n with + | O => 0 + | S u => u + end. +Hint Resolve (f_equal pred): v62. + +Theorem pred_Sn : forall n:nat, n = pred (S n). +Proof. + auto. +Qed. + +Theorem eq_add_S : forall n m:nat, S n = S m -> n = m. +Proof. + intros n m H; change (pred (S n) = pred (S m)) in |- *; auto. +Qed. + +Hint Immediate eq_add_S: core v62. + +(** A consequence of the previous axioms *) + +Theorem not_eq_S : forall n m:nat, n <> m -> S n <> S m. +Proof. + red in |- *; auto. +Qed. +Hint Resolve not_eq_S: core v62. + +Definition IsSucc (n:nat) : Prop := + match n with + | O => False + | S p => True + end. + + +Theorem O_S : forall n:nat, 0 <> S n. +Proof. + red in |- *; intros n H. + change (IsSucc 0) in |- *. + rewrite <- (sym_eq (x:=0) (y:=(S n))); [ exact I | assumption ]. +Qed. +Hint Resolve O_S: core v62. + +Theorem n_Sn : forall n:nat, n <> S n. +Proof. + induction n; auto. +Qed. +Hint Resolve n_Sn: core v62. + +(** Addition *) + +Fixpoint plus (n m:nat) {struct n} : nat := + match n with + | O => m + | S p => S (plus p m) + end. +Hint Resolve (f_equal2 plus): v62. +Hint Resolve (f_equal2 (A1:=nat) (A2:=nat)): core. + +Infix "+" := plus : nat_scope. + +Lemma plus_n_O : forall n:nat, n = n + 0. +Proof. + induction n; simpl in |- *; auto. +Qed. +Hint Resolve plus_n_O: core v62. + +Lemma plus_O_n : forall n:nat, 0 + n = n. +Proof. + auto. +Qed. + +Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m. +Proof. + intros n m; induction n; simpl in |- *; auto. +Qed. +Hint Resolve plus_n_Sm: core v62. + +Lemma plus_Sn_m : forall n m:nat, S n + m = S (n + m). +Proof. + auto. +Qed. + +(** Multiplication *) + +Fixpoint mult (n m:nat) {struct n} : nat := + match n with + | O => 0 + | S p => m + mult p m + end. +Hint Resolve (f_equal2 mult): core v62. + +Infix "*" := mult : nat_scope. + +Lemma mult_n_O : forall n:nat, 0 = n * 0. +Proof. + induction n; simpl in |- *; auto. +Qed. +Hint Resolve mult_n_O: core v62. + +Lemma mult_n_Sm : forall n m:nat, n * m + n = n * S m. +Proof. + intros; induction n as [| p H]; simpl in |- *; auto. + destruct H; rewrite <- plus_n_Sm; apply (f_equal S). + pattern m at 1 3 in |- *; elim m; simpl in |- *; auto. +Qed. +Hint Resolve mult_n_Sm: core v62. + +(** Definition of subtraction on [nat] : [m-n] is [0] if [n>=m] *) + +Fixpoint minus (n m:nat) {struct n} : nat := + match n, m with + | O, _ => 0 + | S k, O => S k + | S k, S l => minus k l + end. + +Infix "-" := 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 : forall m:nat, le n m -> le n (S m). + +Infix "<=" := le : nat_scope. + +Hint Constructors le: core v62. +(*i equivalent to : "Hints Resolve le_n le_S : core v62." i*) + +Definition lt (n m:nat) := S n <= m. +Hint Unfold lt: core v62. + +Infix "<" := lt : nat_scope. + +Definition ge (n m:nat) := m <= n. +Hint Unfold ge: core v62. + +Infix ">=" := ge : nat_scope. + +Definition gt (n m:nat) := m < n. +Hint Unfold gt: core v62. + +Infix ">" := gt : nat_scope. + +Notation "x <= y <= z" := (x <= y /\ y <= z) : nat_scope. +Notation "x <= y < z" := (x <= y /\ y < z) : nat_scope. +Notation "x < y < z" := (x < y /\ y < z) : nat_scope. +Notation "x < y <= z" := (x < y /\ y <= z) : nat_scope. + +(** Pattern-Matching on natural numbers *) + +Theorem nat_case : + forall (n:nat) (P:nat -> Prop), P 0 -> (forall m:nat, P (S m)) -> P n. +Proof. + induction n; auto. +Qed. + +(** Principle of double induction *) + +Theorem nat_double_ind : + forall R:nat -> nat -> Prop, + (forall n:nat, R 0 n) -> + (forall n:nat, R (S n) 0) -> + (forall n m:nat, R n m -> R (S n) (S m)) -> forall n m:nat, R n m. +Proof. + induction n; auto. + destruct m as [| n0]; auto. +Qed. + +(** Notations *) diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v new file mode 100755 index 00000000..2fe520c4 --- /dev/null +++ b/theories/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.11.2.1 2004/07/16 19:31:03 herbelin Exp $ i*) + +Require Export Notations. +Require Export Logic. +Require Export Datatypes. +Require Export Specif. +Require Export Peano. +Require Export Wf.
\ No newline at end of file diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v new file mode 100755 index 00000000..6855e689 --- /dev/null +++ b/theories/Init/Specif.v @@ -0,0 +1,212 @@ +(************************************************************************) +(* 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.25.2.1 2004/07/16 19:31:04 herbelin Exp $ i*) + +Set Implicit Arguments. + +(** Basic specifications : Sets containing logical information *) + +Require Import Notations. +Require Import Datatypes. +Require Import 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 : forall x:A, P x -> sig (A:=A) P. + +Inductive sig2 (A:Set) (P Q:A -> Prop) : Set := + exist2 : forall x:A, P x -> Q x -> sig2 (A:=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 : forall x:A, P x -> sigS (A:=A) P. + +Inductive sigS2 (A:Set) (P Q:A -> Set) : Set := + existS2 : forall x:A, P x -> Q x -> sigS2 (A:=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 (fun x:A => P)) : type_scope. +Notation "{ x : A | P & Q }" := (sig2 (fun x:A => P) (fun x:A => Q)) : + type_scope. +Notation "{ x : A & P }" := (sigS (fun x:A => P)) : type_scope. +Notation "{ x : A & P & Q }" := (sigS2 (fun x:A => P) (fun 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 P) := match e with + | exist a b => a + end. + + Definition proj2_sig (e:sig P) := + match e return P (proj1_sig e) with + | 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 (x:sigS P) : A := match x with + | existS a _ => a + end. + Definition projS2 (x:sigS P) : P (projS1 x) := + match x return P (projS1 x) with + | 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. + +Add Printing If sumbool. + +Inductive sumor (A:Set) (B:Prop) : Set := + | inleft : A -> A + {B} + | inright : B -> A + {B} + where "A + { B }" := (sumor A B) : type_scope. + +Add Printing If sumor. + +(** 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 : + (forall x:S, sig (fun y:S' => R x y)) -> + sig (fun f:S -> S' => forall z:S, R z (f z)). + Proof. + intro H. + exists (fun z:S => match H z with + | exist y _ => y + end). + intro z; destruct (H z); trivial. + Qed. + + Lemma Choice2 : + (forall x:S, sigS (fun y:S' => R' x y)) -> + sigS (fun f:S -> S' => forall z:S, R' z (f z)). + Proof. + intro H. + exists (fun z:S => match H z with + | existS y _ => y + end). + intro z; destruct (H z); trivial. + Qed. + + Lemma bool_choice : + (forall x:S, {R1 x} + {R2 x}) -> + sig + (fun f:S -> bool => + forall x:S, f x = true /\ R1 x \/ f x = false /\ R2 x). + Proof. + intro H. + exists + (fun z:S => match H z with + | left _ => true + | right _ => false + end). + intro z; destruct (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. + +Implicit Arguments error [A]. + +Definition except := False_rec. (* for compatibility with previous versions *) + +Implicit Arguments except [P]. + +Theorem absurd_set : forall (A:Prop) (C:Set), A -> ~ A -> C. +Proof. + intros A C h1 h2. + apply False_rec. + apply (h2 h1). +Qed. + +Hint Resolve left right inleft inright: core v62. + +(** Sigma Type at Type level [sigT] *) + +Inductive sigT (A:Type) (P:A -> Type) : Type := + existT : forall x:A, P x -> sigT (A:=A) P. + +Section projections_sigT. + + Variable A : Type. + Variable P : A -> Type. + + Definition projT1 (H:sigT P) : A := match H with + | existT x _ => x + end. + + Definition projT2 : forall x:sigT P, P (projT1 x) := + fun H:sigT P => match H return P (projT1 H) with + | existT x h => h + end. + +End projections_sigT. + diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v new file mode 100755 index 00000000..7ab3723d --- /dev/null +++ b/theories/Init/Wf.v @@ -0,0 +1,171 @@ +(************************************************************************) +(* 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. + +(*i $Id: Wf.v,v 1.17.2.1 2004/07/16 19:31:04 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 Import Notations. +Require Import Logic. +Require Import Datatypes. + +(** Well-founded induction principle on Prop *) + +Section 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 : forall x:A, (forall y:A, R y x -> Acc y) -> Acc x. + + Lemma Acc_inv : forall x:A, Acc x -> forall y:A, R y x -> Acc y. + destruct 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 : + forall x:A, + (forall y:A, R y x -> Acc y) -> (forall y:A, R y x -> P y) -> P x. + + Fixpoint Acc_rect (x:A) (a:Acc x) {struct a} : P x := + F (Acc_inv a) (fun (y:A) (h:R y x) => Acc_rect (x:=y) (Acc_inv a 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 : forall x:A, (forall y:A, R y x -> P y) -> P x. + + Fixpoint Acc_iter (x:A) (a:Acc x) {struct a} : P x := + F (fun (y:A) (h:R y x) => Acc_iter (x:=y) (Acc_inv a h)). + + End AccIter. + + (** A relation is well-founded if every element is accessible *) + + Definition well_founded := forall a:A, Acc a. + + (** well-founded induction on Set and Prop *) + + Hypothesis Rwf : well_founded. + + Theorem well_founded_induction_type : + forall P:A -> Type, + (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a. + Proof. + intros; apply (Acc_iter P); auto. + Defined. + + Theorem well_founded_induction : + forall P:A -> Set, + (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a. + Proof. + exact (fun P:A -> Set => well_founded_induction_type P). + Defined. + + Theorem well_founded_ind : + forall P:A -> Prop, + (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a. + Proof. + exact (fun P:A -> Prop => well_founded_induction_type P). + Defined. + +(** Building fixpoints *) + +Section FixPoint. + +Variable P : A -> Set. +Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x. + +Fixpoint Fix_F (x:A) (r:Acc x) {struct r} : P x := + F (fun (y:A) (p:R y x) => Fix_F (x:=y) (Acc_inv r p)). + +Definition Fix (x:A) := Fix_F (Rwf x). + +(** Proof that [well_founded_induction] satisfies the fixpoint equation. + It requires an extra property of the functional *) + +Hypothesis + F_ext : + forall (x:A) (f g:forall y:A, R y x -> P y), + (forall (y:A) (p:R y x), f y p = g y p) -> F f = F g. + +Scheme Acc_inv_dep := Induction for Acc Sort Prop. + +Lemma Fix_F_eq : + forall (x:A) (r:Acc x), + F (fun (y:A) (p:R y x) => Fix_F (Acc_inv r p)) = Fix_F r. +destruct r using Acc_inv_dep; auto. +Qed. + +Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F r = Fix_F s. +intro x; induction (Rwf x); intros. +rewrite <- (Fix_F_eq r); rewrite <- (Fix_F_eq s); intros. +apply F_ext; auto. +Qed. + + +Lemma Fix_eq : forall x:A, Fix x = F (fun (y:A) (p:R y x) => Fix y). +intro x; unfold Fix in |- *. +rewrite <- (Fix_F_eq (x:=x)). +apply F_ext; intros. +apply Fix_F_inv. +Qed. + +End FixPoint. + +End Well_founded. + +(** A recursor over pairs *) + +Section Well_founded_2. + + Variables A B : Set. + Variable R : A * B -> A * B -> Prop. + + Variable P : A -> B -> Type. + Variable + F : + forall (x:A) (x':B), + (forall (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')) {struct a} : + P x x' := + F + (fun (y:A) (y':B) (h:R (y, y') (x, x')) => + Acc_iter_2 (x:=y) (x':=y') (Acc_inv a (y, y') h)). + + Hypothesis Rwf : well_founded R. + + Theorem well_founded_induction_type_2 : + (forall (x:A) (x':B), + (forall (y:A) (y':B), R (y, y') (x, x') -> P y y') -> P x x') -> + forall (a:A) (b:B), P a b. + Proof. + intros; apply Acc_iter_2; auto. + Defined. + +End Well_founded_2. |