diff options
Diffstat (limited to 'theories/Init')
| -rw-r--r--[-rwxr-xr-x] | theories/Init/Datatypes.v | 85 | ||||
| -rw-r--r--[-rwxr-xr-x] | theories/Init/Logic.v | 180 | ||||
| -rw-r--r--[-rwxr-xr-x] | theories/Init/Logic_Type.v | 36 | ||||
| -rw-r--r-- | theories/Init/Notations.v | 14 | ||||
| -rw-r--r--[-rwxr-xr-x] | theories/Init/Peano.v | 65 | ||||
| -rw-r--r--[-rwxr-xr-x] | theories/Init/Prelude.v | 5 | ||||
| -rw-r--r--[-rwxr-xr-x] | theories/Init/Specif.v | 151 | ||||
| -rw-r--r-- | theories/Init/Tactics.v | 64 | ||||
| -rw-r--r--[-rwxr-xr-x] | theories/Init/Wf.v | 102 |
9 files changed, 415 insertions, 287 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 6aeabe13..56dc7e95 100755..100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -6,19 +6,19 @@ (* * 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*) +(*i $Id: Datatypes.v 9245 2006-10-17 12:53:34Z notin $ i*) + +Set Implicit Arguments. 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] *) +(** [bool] is the datatype of the boolean values [true] and [false] *) Inductive bool : Set := | true : bool @@ -27,7 +27,9 @@ Inductive bool : Set := 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 *) + note that the constructor name is the letter O. + Numbers in [nat] can be denoted using a decimal notation; + e.g. [3%nat] abbreviates [S (S (S O))] *) Inductive nat : Set := | O : nat @@ -45,25 +47,31 @@ Inductive Empty_set : Set :=. 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. +Inductive identity (A:Type) (a:A) : A -> Type := + 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 *) +(** [option A] is the extension of [A] with an extra element [None] *) -Inductive option (A:Set) : Set := +Inductive option (A:Type) : Type := | 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] *) +Definition option_map (A B:Type) (f:A->B) o := + match o with + | Some a => Some (f a) + | None => None + end. + +(** [sum A B], written [A + B], is the disjoint sum of [A] and [B] *) (* Syntax defined in Specif.v *) -Inductive sum (A B:Set) : Set := +Inductive sum (A B:Type) : Type := | inl : A -> sum A B | inr : B -> sum A B. @@ -72,39 +80,46 @@ 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. +Inductive prod (A B:Type) : Type := + 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. + Variables A B : Type. + 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). + forall (A B:Type) (p:A * B), p = pair (fst p) (snd p). Proof. -destruct p; reflexivity. + 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. + forall (A B:Type) (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. + destruct p1; destruct p2; simpl in |- *; intros Hfst Hsnd. + rewrite Hfst; rewrite Hsnd; reflexivity. Qed. +Definition prod_uncurry (A B C:Type) (f:prod A B -> C) + (x:A) (y:B) : C := f (pair x y). + +Definition prod_curry (A B C:Type) (f:A -> B -> C) + (p:prod A B) : C := match p with + | pair x y => f x y + end. (** Comparison *) @@ -115,7 +130,19 @@ Inductive comparison : Set := Definition CompOpp (r:comparison) := match r with - | Eq => Eq - | Lt => Gt - | Gt => Lt + | Eq => Eq + | Lt => Gt + | Gt => Lt end. + +(* Compatibility *) + +Notation prodT := prod (only parsing). +Notation pairT := pair (only parsing). +Notation prodT_rect := prod_rect (only parsing). +Notation prodT_rec := prod_rec (only parsing). +Notation prodT_ind := prod_ind (only parsing). +Notation fstT := fst (only parsing). +Notation sndT := snd (only parsing). +Notation prodT_uncurry := prod_uncurry (only parsing). +Notation prodT_curry := prod_curry (only parsing). diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index bae8d4a1..8b487432 100755..100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -6,7 +6,7 @@ (* * 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*) +(*i $Id: Logic.v 9245 2006-10-17 12:53:34Z notin $ i*) Set Implicit Arguments. @@ -16,7 +16,7 @@ Require Import Notations. (** [True] is the always true proposition *) Inductive True : Prop := - I : True. + I : True. (** [False] is the always false proposition *) Inductive False : Prop :=. @@ -28,13 +28,6 @@ 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 @@ -42,16 +35,23 @@ Section Conjunction. [proj1] and [proj2] are first and second projections of a conjunction *) +Inductive and (A B:Prop) : Prop := + conj : A -> B -> A /\ B + +where "A /\ B" := (and A B) : type_scope. + +Section Conjunction. + Variables A B : Prop. Theorem proj1 : A /\ B -> A. Proof. - destruct 1; trivial. + destruct 1; trivial. Qed. Theorem proj2 : A /\ B -> B. Proof. - destruct 1; trivial. + destruct 1; trivial. Qed. End Conjunction. @@ -61,7 +61,8 @@ End Conjunction. Inductive or (A B:Prop) : Prop := | or_introl : A -> A \/ B | or_intror : B -> A \/ B - where "A \/ B" := (or A B) : type_scope. + +where "A \/ B" := (or A B) : type_scope. (** [iff A B], written [A <-> B], expresses the equivalence of [A] and [B] *) @@ -94,44 +95,52 @@ End Equivalence. 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. + (at level 200, right associativity) : type_scope. + +(** * First-order quantifiers *) + +(** [ex P], or simply [exists x, P x], or also [exists x:A, P x], + expresses the existence of an [x] of some type [A] in [Set] which + satisfies the predicate [P]. This is existential quantification. + + [ex2 P Q], or simply [exists2 x, P x & Q x], or also + [exists2 x:A, P x & Q x], expresses the existence of an [x] of + type [A] which satisfies both predicates [P] and [Q]. + + Universal quantification is primitively written [forall x:A, Q]. By + symmetry with existential quantification, the construction [all P] + is provided too. *) +(** Remark: [exists x, Q] denotes [ex (fun x => Q)] so that [exists x, + P x] is in fact equivalent to [ex (fun x => P x)] which may be not + convertible to [ex P] if [P] is not itself an abstraction *) + + Inductive ex (A:Type) (P:A -> Prop) : Prop := - ex_intro : forall x:A, P x -> ex (A:=A) P. + 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. + 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. + (at level 200, x ident, right associativity) : type_scope. Notation "'exists' x : t , p" := (ex (fun x:t => p)) - (at level 200, x ident, format "'exists' '/ ' x : t , '/ ' p") + (at level 200, x ident, right associativity, + 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. + (at level 200, x ident, p at level 200, right associativity) : 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 ']'") + (at level 200, x ident, t at level 200, p at level 200, right associativity, + format "'[' 'exists2' '/ ' x : t , '/ ' '[' p & '/' q ']' ']'") : type_scope. - (** Derived rules for universal quantification *) Section universal_quantification. @@ -141,28 +150,31 @@ Section universal_quantification. Theorem inst : forall x:A, all (fun x => P x) -> P x. Proof. - unfold all in |- *; auto. + unfold all in |- *; auto. Qed. Theorem gen : forall (B:Prop) (f:forall y:A, B -> P y), B -> all P. Proof. - red in |- *; auto. + 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]. +(** [eq x y], or simply [x=y] expresses the 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] *) + equals by equals) are proved below. The type of [x] and [y] can be + made explicit using the notation [x = y :> A]. This is Leibniz equality + as it expresses that [x] and [y] are equal iff every property on + [A] which is true of [x] is also true of [y] *) Inductive eq (A:Type) (x:A) : A -> Prop := refl_equal : x = x :>A - where "x = y :> A" := (@eq A x y) : type_scope. + +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. @@ -190,53 +202,43 @@ Section Logic_lemmas. Theorem sym_eq : x = y -> y = x. Proof. - destruct 1; trivial. + destruct 1; trivial. Defined. Opaque sym_eq. Theorem trans_eq : x = y -> y = z -> x = z. Proof. - destruct 2; trivial. + destruct 2; trivial. Defined. Opaque trans_eq. Theorem f_equal : x = y -> f x = f y. Proof. - destruct 1; trivial. + 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. + 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. + 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. @@ -244,36 +246,74 @@ Section Logic_lemmas. 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. + 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. + 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. + 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. + 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. + +(** Basic definitions about relations and properties *) + +Definition subrelation (A B : Type) (R R' : A->B->Prop) := + forall x y, R x y -> R' x y. + +Definition unique (A : Type) (P : A->Prop) (x:A) := + P x /\ forall (x':A), P x' -> x=x'. + +Definition uniqueness (A:Type) (P:A->Prop) := forall x y, P x -> P y -> x = y. + +(** Unique existence *) + +Notation "'exists' ! x , P" := (ex (unique (fun x => P))) + (at level 200, x ident, right associativity, + format "'[' 'exists' ! '/ ' x , '/ ' P ']'") : type_scope. +Notation "'exists' ! x : A , P" := + (ex (unique (fun x:A => P))) + (at level 200, x ident, right associativity, + format "'[' 'exists' ! '/ ' x : A , '/ ' P ']'") : type_scope. + +Lemma unique_existence : forall (A:Type) (P:A->Prop), + ((exists x, P x) /\ uniqueness P) <-> (exists! x, P x). +Proof. + intros A P; split. + intros ((x,Hx),Huni); exists x; red; auto. + intros (x,(Hx,Huni)); split. + exists x; assumption. + intros x' x'' Hx' Hx''; transitivity x. + symmetry; auto. + auto. +Qed. + +(** Being inhabited *) + +Inductive inhabited (A:Type) : Prop := inhabits : A -> inhabited A. + +Hint Resolve inhabits: core. diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v index 0e62e842..dbe944b0 100755..100644 --- a/theories/Init/Logic_Type.v +++ b/theories/Init/Logic_Type.v @@ -6,18 +6,22 @@ (* * 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*) +(*i $Id: Logic_Type.v 8866 2006-05-28 16:21:04Z herbelin $ i*) -Set Implicit Arguments. +(** This module defines type constructors for types in [Type] + ([Datatypes.v] and [Logic.v] defined them for types in [Set]) *) -(** This module defines quantification on the world [Type] - ([Logic.v] was defining it on the world [Set]) *) +Set Implicit Arguments. Require Import Datatypes. Require Export Logic. +(** Negation of a type in [Type] *) + Definition notT (A:Type) := A -> False. +(** Properties of [identity] *) + Section identity_is_a_congruence. Variables A B : Type. @@ -62,28 +66,4 @@ Definition identity_rect_r : 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 index e0a18747..416647b4 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Notations.v,v 1.24.2.2 2004/08/01 09:36:44 herbelin Exp $ i*) +(*i $Id: Notations.v 8866 2006-05-28 16:21:04Z herbelin $ i*) (** These are the notations whose level and associativity are imposed by Coq *) @@ -54,17 +54,17 @@ Reserved Notation "x ^ y" (at level 30, right associativity). 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 *) + of other notations such as "{ A } + { B }" and "A + { B }" (which + are at the same level than "x + y"); + "{ x }" is at level 0 to factor with "{ x : A | P }" *) 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 | P }" (at level 0, x at level 99). +Reserved Notation "{ x | 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). diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index 789a020f..3df2b566 100755..100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -6,9 +6,10 @@ (* * 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*) +(*i $Id: Peano.v 9245 2006-10-17 12:53:34Z notin $ i*) -(** Natural numbers [nat] built from [O] and [S] are defined in Datatypes.v *) +(** The type [nat] of Peano natural numbers (built from [O] and [S]) + is defined in [Datatypes.v] *) (** This module defines the following operations on natural numbers : - predecessor [pred] @@ -19,13 +20,15 @@ - 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 *) + It states various lemmas and theorems about natural numbers, + including Peano's axioms of arithmetic (in Coq, these are provable). + Case analysis on [nat] and induction on [nat * nat] are provided too + *) Require Import Notations. Require Import Datatypes. Require Import Logic. +Unset Boxed Definitions. Open Scope nat_scope. @@ -44,18 +47,20 @@ Hint Resolve (f_equal pred): v62. Theorem pred_Sn : forall n:nat, n = pred (S n). Proof. - auto. + simpl; reflexivity. Qed. +(** Injectivity of successor *) + 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. + intros n m Sn_eq_Sm. + replace (n=m) with (pred (S n) = pred (S m)) by auto using pred_Sn. + rewrite Sn_eq_Sm; trivial. 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. @@ -68,12 +73,12 @@ Definition IsSucc (n:nat) : Prop := | S p => True end. +(** Zero is not the successor of a number *) 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 ]. + unfold not; intros n H. + inversion H. Qed. Hint Resolve O_S: core v62. @@ -88,13 +93,14 @@ Hint Resolve n_Sn: core v62. Fixpoint plus (n m:nat) {struct n} : nat := match n with | O => m - | S p => S (plus p m) - end. + | S p => S (p + m) + end + +where "n + m" := (plus n m) : nat_scope. + 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. @@ -122,11 +128,12 @@ Qed. 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. + | S p => m + p * m + end -Infix "*" := mult : nat_scope. +where "n * m" := (mult n m) : nat_scope. + +Hint Resolve (f_equal2 mult): core v62. Lemma mult_n_O : forall n:nat, 0 = n * 0. Proof. @@ -142,27 +149,25 @@ Proof. Qed. Hint Resolve mult_n_Sm: core v62. -(** Definition of subtraction on [nat] : [m-n] is [0] if [n>=m] *) +(** Truncated subtraction: [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. + | S k, S l => k - l + end -Infix "-" := minus : nat_scope. +where "n - m" := (minus n m) : 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). + | le_n : n <= n + | le_S : forall m:nat, n <= m -> n <= S m -Infix "<=" := le : nat_scope. +where "n <= m" := (le n m) : nat_scope. Hint Constructors le: core v62. (*i equivalent to : "Hints Resolve le_n le_S : core v62." i*) @@ -187,7 +192,7 @@ 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 *) +(** Case analysis *) Theorem nat_case : forall (n:nat) (P:nat -> Prop), P 0 -> (forall m:nat, P (S m)) -> P n. diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 2fe520c4..5f6f1eab 100755..100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -6,11 +6,12 @@ (* * 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*) +(*i $Id: Prelude.v 8642 2006-03-17 10:09:02Z notin $ 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 +Require Export Wf. +Require Export Tactics. diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 6855e689..dd2f7697 100755..100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -6,62 +6,71 @@ (* * 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*) +(*i $Id: Specif.v 8866 2006-05-28 16:21:04Z herbelin $ i*) -Set Implicit Arguments. +(** Basic specifications : sets that may contain logical information *) -(** Basic specifications : Sets containing logical information *) +Set Implicit Arguments. Require Import Notations. Require Import Datatypes. Require Import Logic. -(** Subsets *) +(** Subsets and Sigma-types *) -(** [(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]. *) +(** [(sig A P)], or more suggestively [{x:A | P x}], denotes the subset + of elements of the type [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 type [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 sig (A:Type) (P:A -> Prop) : Type := + exist : forall x:A, P x -> sig P. -Inductive sig2 (A:Set) (P Q:A -> Prop) : Set := - exist2 : forall x:A, P x -> Q x -> sig2 (A:=A) P Q. +Inductive sig2 (A:Type) (P Q:A -> Prop) : Type := + exist2 : forall x:A, P x -> Q x -> sig2 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. +(** [(sigT A P)], or more suggestively [{x:A & (P x)}] is a Sigma-type. + Similarly for [(sigT2 A P Q)], also written [{x:A & (P x) & (Q x)}]. *) + +Inductive sigT (A:Type) (P:A -> Type) : Type := + existT : forall x:A, P x -> sigT P. -Inductive sigS2 (A:Set) (P Q:A -> Set) : Set := - existS2 : forall x:A, P x -> Q x -> sigS2 (A:=A) P Q. +Inductive sigT2 (A:Type) (P Q:A -> Type) : Type := + existT2 : forall x:A, P x -> Q x -> sigT2 P Q. + +(* Notations *) 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]. +Arguments Scope sigT [type_scope type_scope]. +Arguments Scope sigT2 [type_scope type_scope type_scope]. +Notation "{ x | P }" := (sig (fun x => P)) : type_scope. +Notation "{ x | P & Q }" := (sig2 (fun x => P) (fun x => Q)) : 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)) : +Notation "{ x : A & P }" := (sigT (fun x:A => P)) : type_scope. +Notation "{ x : A & P & Q }" := (sigT2 (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. +Add Printing Let sigT. +Add Printing Let sigT2. + + +(** Projections of [sig] + 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 + [(proj1_sig y)] is the witness [a] and [(proj2_sig y)] is the + proof of [(P a)] *) -(** Projections of sig *) Section Subset_projections. - Variable A : Set. + Variable A : Type. Variable P : A -> Prop. Definition proj1_sig (e:sig P) := match e with @@ -76,30 +85,31 @@ Section Subset_projections. End Subset_projections. -(** Projections of sigS *) +(** Projections of [sigT] -Section Projections. + An element [x] of a sigma-type [{y:A & P y}] is a dependent pair + made of an [a] of type [A] and an [h] of type [P a]. Then, + [(projT1 x)] is the first projection and [(projT2 x)] is the + second projection, the type of which depends on the [projT1]. *) - Variable A : Set. - Variable P : A -> Set. +Section Projections. - (** 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)] *) + Variable A : Type. + Variable P : A -> Type. - Definition projS1 (x:sigS P) : A := match x with - | existS a _ => a + Definition projT1 (x:sigT P) : A := match x with + | existT a _ => a end. - Definition projS2 (x:sigS P) : P (projS1 x) := - match x return P (projS1 x) with - | existS _ h => h + Definition projT2 (x:sigT P) : P (projT1 x) := + match x return P (projT1 x) with + | existT _ h => h end. End Projections. -(** Extended_booleans *) +(** [sumbool] is a boolean type equipped with the justification of + their value *) Inductive sumbool (A B:Prop) : Set := | left : A -> {A} + {B} @@ -108,19 +118,20 @@ Inductive sumbool (A B:Prop) : Set := Add Printing If sumbool. -Inductive sumor (A:Set) (B:Prop) : Set := +(** [sumor] is an option type equipped with the justification of why + it may not be a regular value *) + +Inductive sumor (A:Type) (B:Prop) : Type := | inleft : A -> A + {B} | inright : B -> A + {B} where "A + { B }" := (sumor A B) : type_scope. Add Printing If sumor. -(** Choice *) +(** Various forms of the axiom of choice for specifications *) 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. @@ -138,12 +149,12 @@ Section Choice_lemmas. 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)). + (forall x:S, sigT (fun y:S' => R' x y)) -> + sigT (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 + | existT y _ => y end). intro z; destruct (H z); trivial. Qed. @@ -167,8 +178,10 @@ 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. *) + + [Inductive Exc [A:Type] : Type := value : A->(Exc A) | error : (Exc A)]. + + It is implemented using the option type. *) Definition Exc := option. Definition value := Some. @@ -189,24 +202,18 @@ 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. - +(* Compatibility *) + +Notation sigS := sigT (only parsing). +Notation existS := existT (only parsing). +Notation sigS_rect := sigT_rect (only parsing). +Notation sigS_rec := sigT_rec (only parsing). +Notation sigS_ind := sigT_ind (only parsing). +Notation projS1 := projT1 (only parsing). +Notation projS2 := projT2 (only parsing). + +Notation sigS2 := sigT2 (only parsing). +Notation existS2 := existT2 (only parsing). +Notation sigS2_rect := sigT2_rect (only parsing). +Notation sigS2_rec := sigT2_rec (only parsing). +Notation sigS2_ind := sigT2_ind (only parsing). diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v new file mode 100644 index 00000000..ba210dd6 --- /dev/null +++ b/theories/Init/Tactics.v @@ -0,0 +1,64 @@ +(************************************************************************) +(* 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: Tactics.v 9268 2006-10-24 12:56:16Z herbelin $ i*) + +Require Import Notations. +Require Import Logic. + +(** Useful tactics *) + +(* A shorter name for generalize + clear, can be seen as an anti-intro *) + +Tactic Notation "revert" ne_hyp_list(l) := generalize l; clear l. + +(* to contradict an hypothesis without copying its type. *) + +Ltac absurd_hyp h := + let T := type of h in + absurd T. + +(* Transforming a negative goal [ H:~A |- ~B ] into a positive one [ B |- A ]*) + +Ltac swap H := intro; apply H; clear H. + +(* A case with no loss of information. *) + +Ltac case_eq x := generalize (refl_equal x); pattern x at -1; case x. + +(* A tactic for easing the use of lemmas f_equal, f_equal2, ... *) + +Ltac f_equal := + let cg := try congruence in + let r := try reflexivity in + match goal with + | |- ?f ?a = ?f' ?a' => cut (a=a'); [cg|r] + | |- ?f ?a ?b = ?f' ?a' ?b' => + cut (b=b');[cut (a=a');[cg|r]|r] + | |- ?f ?a ?b ?c = ?f' ?a' ?b' ?c'=> + cut (c=c');[cut (b=b');[cut (a=a');[cg|r]|r]|r] + | |- ?f ?a ?b ?c ?d= ?f' ?a' ?b' ?c' ?d'=> + cut (d=d');[cut (c=c');[cut (b=b');[cut (a=a');[cg|r]|r]|r]|r] + | |- ?f ?a ?b ?c ?d ?e= ?f' ?a' ?b' ?c' ?d' ?e'=> + cut (e=e');[cut (d=d');[cut (c=c');[cut (b=b');[cut (a=a');[cg|r]|r]|r]|r]|r] + | _ => idtac + end. + +(* Rewriting in all hypothesis several times everywhere *) + +Tactic Notation "rewrite_all" constr(eq) := repeat rewrite eq in *. +Tactic Notation "rewrite_all" "<-" constr(eq) := repeat rewrite <- eq in *. + +(* Keeping a copy of an expression *) + +Ltac remembertac x a := + let x := fresh x in + let H := fresh "Heq" x in + (set (x:=a) in *; assert (H: x=a) by reflexivity; clearbody x). + +Tactic Notation "remember" constr(c) "as" ident(x) := remembertac x c. diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index 7ab3723d..4e0f3745 100755..100644 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -6,61 +6,59 @@ (* * 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*) +(*i $Id: Wf.v 8988 2006-06-25 22:15:32Z letouzey $ 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 *) + from a well-founded ordering on a given set *) + +Set Implicit Arguments. Require Import Notations. Require Import Logic. Require Import Datatypes. -(** Well-founded induction principle on Prop *) +(** Well-founded induction principle on [Prop] *) Section Well_founded. - Variable A : Set. + Variable A : Type. 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. + Inductive Acc (x: A) : Prop := + Acc_intro : (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 : + (** 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. + 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)). + F (Acc_inv a) (fun (y:A) (h:R y x) => Acc_rect (Acc_inv a h)). End AccRecType. Definition Acc_rec (P:A -> Set) := Acc_rect P. - (** A simplified version of Acc_rec(t) *) + (** A simplified version of [Acc_rect] *) Section AccIter. - Variable P : A -> Type. + 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)). + F (fun (y:A) (h:R y x) => Acc_iter (Acc_inv a h)). End AccIter. @@ -68,7 +66,7 @@ Section Well_founded. Definition well_founded := forall a:A, Acc a. - (** well-founded induction on Set and Prop *) + (** Well-founded induction on [Set] and [Prop] *) Hypothesis Rwf : well_founded. @@ -95,47 +93,48 @@ Section Well_founded. (** Building fixpoints *) -Section FixPoint. + 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)). + Variable P : A -> Type. + Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x. -Definition Fix (x:A) := Fix_F (Rwf x). + Notation Fix_F := (Acc_iter P F) (only parsing). (* alias *) -(** Proof that [well_founded_induction] satisfies the fixpoint equation. - It requires an extra property of the functional *) + Definition Fix (x:A) := Acc_iter P F (Rwf x). -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. + (** Proof that [well_founded_induction] satisfies the fixpoint equation. + It requires an extra property of the functional *) -Scheme Acc_inv_dep := Induction for Acc Sort Prop. + 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. -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. + Scheme Acc_inv_dep := Induction for Acc Sort Prop. -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_F_eq : + forall (x:A) (r:Acc x), + F (fun (y:A) (p:R y x) => Fix_F y (Acc_inv r p)) = Fix_F x r. + Proof. + destruct r using Acc_inv_dep; auto. + Qed. + Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F x r = Fix_F x s. + Proof. + 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. + Lemma Fix_eq : forall x:A, Fix x = F (fun (y:A) (p:R y x) => Fix y). + Proof. + intro x; unfold Fix in |- *. + rewrite <- (Fix_F_eq (x:=x)). + apply F_ext; intros. + apply Fix_F_inv. + Qed. -End FixPoint. + End FixPoint. End Well_founded. @@ -147,6 +146,8 @@ Section Well_founded_2. Variable R : A * B -> A * B -> Prop. Variable P : A -> B -> Type. + + Section Acc_iter_2. Variable F : forall (x:A) (x':B), @@ -157,6 +158,7 @@ Section Well_founded_2. 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)). + End Acc_iter_2. Hypothesis Rwf : well_founded R. @@ -169,3 +171,5 @@ Section Well_founded_2. Defined. End Well_founded_2. + +Notation Fix_F := Acc_iter (only parsing). (* compatibility *) |