diff options
Diffstat (limited to 'theories/Init')
| -rwxr-xr-x | theories/Init/Datatypes.v | 115 | ||||
| -rwxr-xr-x | theories/Init/Logic.v | 242 | ||||
| -rwxr-xr-x | theories/Init/Logic_Type.v | 287 | ||||
| -rw-r--r-- | theories/Init/Notations.v | 109 | ||||
| -rwxr-xr-x | theories/Init/Peano.v | 208 | ||||
| -rwxr-xr-x | theories/Init/Prelude.v | 2 | ||||
| -rwxr-xr-x | theories/Init/Specif.v | 192 | ||||
| -rwxr-xr-x | theories/Init/Wf.v | 129 |
8 files changed, 515 insertions, 769 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index d93bbbac1..d5a1179c8 100755 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -8,117 +8,114 @@ (*i $Id$ i*) -Require Notations. -Require Logic. +Require Import Notations. +Require Import Logic. Set Implicit Arguments. -V7only [Unset Implicit Arguments.]. (** [unit] is a singleton datatype with sole inhabitant [tt] *) -Inductive unit : Set := tt : unit. +Inductive unit : Set := + tt : unit. (** [bool] is the datatype of the booleans values [true] and [false] *) -Inductive bool : Set := true : bool - | false : bool. +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. +Inductive nat : Set := + | O : nat + | S : nat -> nat. -Delimits Scope nat_scope with nat. +Delimit Scope nat_scope with nat. Bind Scope nat_scope with nat. -Arguments Scope S [ nat_scope ]. +Arguments Scope S [nat_scope]. (** [Empty_set] has no inhabitant *) -Inductive Empty_set:Set :=. +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. +Inductive identity (A:Type) (a:A) : A -> Set := + refl_identity : identity (A:=A) a a. +Hint 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 []. -]. +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). +Inductive option (A:Set) : Set := + | Some : A -> option A + | None : option A. -Implicits None [1]. -V7only [Implicits None [].]. +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). +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). +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 )" := (pair ? ? x y) : core_scope V8only "x , y". +Notation "x , y" := (pair x y) : 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. + 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. -V7only [ -Notation Fst := (fst ? ?). -Notation Snd := (snd ? ?). -]. -Hints Resolve pair inl inr : core v62. +Hint Resolve pair inl inr: core v62. -Lemma surjective_pairing : (A,B:Set;p:A*B)p=(pair A B (Fst p) (Snd p)). +Lemma surjective_pairing : + forall (A B:Set) (p:A * B), p = pair (fst p) (snd p). Proof. -NewDestruct p; Reflexivity. +destruct p; reflexivity. Qed. -Lemma injective_projections : - (A,B:Set;p1,p2:A*B)(Fst p1)=(Fst p2)->(Snd p1)=(Snd p2)->p1=p2. +Lemma injective_projections : + forall (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. +destruct p1; destruct p2; simpl in |- *; 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. +Inductive comparison : Set := + | Eq : comparison + | Lt : comparison + | Gt : comparison. + +Definition CompOpp (r:comparison) := + match r with + | Eq => Eq + | Lt => Gt + | Gt => Lt + end.
\ No newline at end of file diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index dc067a4b7..7cfe160a0 100755 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -9,30 +9,27 @@ (*i $Id$ i*) Set Implicit Arguments. -V7only [Unset Implicit Arguments.]. -Require Notations. +Require Import Notations. (** [True] is the always true proposition *) -Inductive True : Prop := I : True. +Inductive True : Prop := + I : True. (** [False] is the always false proposition *) -Inductive False : Prop := . +Inductive False : Prop :=. (** [not A], written [~A], is the negation of [A] *) -Definition not := [A:Prop]A->False. +Definition not (A:Prop) := A -> False. Notation "~ x" := (not x) : type_scope. -Hints Unfold not : core. +Hint Unfold not: core. -Inductive and [A,B:Prop] : Prop := conj : A -> B -> A /\ B +Inductive and (A B:Prop) : Prop := + conj : A -> B -> A /\ B + where "A /\ B" := (and A B) : type_scope. -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. @@ -43,61 +40,58 @@ Section Conjunction. [proj1] and [proj2] are first and second projections of a conjunction *) - Variables A,B : Prop. + Variables A B : Prop. - Theorem proj1 : (and A B) -> A. + Theorem proj1 : A /\ B -> A. Proof. - NewDestruct 1; Trivial. + destruct 1; trivial. Qed. - Theorem proj2 : (and A B) -> B. + Theorem proj2 : A /\ B -> B. Proof. - NewDestruct 1; Trivial. + 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. +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)). +Definition iff (A B:Prop) := (A -> B) /\ (B -> A). Notation "A <-> B" := (iff A B) : type_scope. Section Equivalence. -Theorem iff_refl : (A:Prop) (iff A A). +Theorem iff_refl : forall A:Prop, A <-> A. Proof. - Split; Auto. + split; auto. Qed. -Theorem iff_trans : (a,b,c:Prop) (iff a b) -> (iff b c) -> (iff a c). +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. + intros A B C [H1 H2] [H3 H4]; split; auto. Qed. -Theorem iff_sym : (A,B:Prop) (iff A B) -> (iff B A). +Theorem iff_sym : forall A B:Prop, (A <-> B) -> (B <-> A). Proof. - Intros A B (H1,H2); Split; Auto. + 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.]. +Definition IF_then_else (P Q R:Prop) := P /\ Q \/ ~ P /\ R. -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). +Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3) + (at level 200) : type_scope. (** First-order quantifiers *) @@ -114,57 +108,42 @@ Notation "'IF' c1 'then' c2 'else' c3" := (IF c1 c2 c3) construction [(all A P)], or simply [(All P)], is provided as an abbreviation of [(x:A)(P x)] *) -Inductive ex [A:Type;P:A->Prop] : Prop - := ex_intro : (x:A)(P x)->(ex A P). +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 : (x:A)(P x)->(Q x)->(ex2 A P Q). +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](x:A)(P x). +Definition all (A:Type) (P:A -> Prop) := forall x:A, P x. (*Rule order is important to give printing priority to fully typed ALL and EX*) -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). - -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). - -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). -]. +Notation "'exists' x | p" := (ex (fun x => p)) + (at level 200, x ident, p at level 99) : type_scope. +Notation "'exists' x : t | p" := (ex (fun x:t => p)) + (at level 200, x ident, p at level 99) : type_scope. + +Notation "'exists2' x | p & q" := (ex2 (fun x => p) (fun x => q)) + (at level 200, x ident, p, q at level 99) : 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, q at level 99) : type_scope. + (** Universal quantification *) Section universal_quantification. Variable A : Type. - Variable P : A->Prop. + Variable P : A -> Prop. - Theorem inst : (x:A)(all ? [x](P x))->(P x). + Theorem inst : forall x:A, all (fun x => P x) -> P x. Proof. - Unfold all; Auto. + unfold all in |- *; auto. Qed. - Theorem gen : (B:Prop)(f:(y:A)B->(P y))B->(all A P). + Theorem gen : forall (B:Prop) (f:forall y:A, B -> P y), B -> all P. Proof. - Red; Auto. + red in |- *; auto. Qed. End universal_quantification. @@ -177,66 +156,60 @@ Section universal_quantification. 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. +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. +Notation "x = y" := (x = y :>_) : type_scope. +Notation "x <> y :> T" := (~ x = y :>T) : 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 []. -]. +Implicit Arguments eq_ind [A]. +Implicit Arguments eq_rec [A]. +Implicit Arguments eq_rect [A]. -Hints Resolve I conj or_introl or_intror refl_equal : core v62. -Hints Resolve ex_intro ex_intro2 : core v62. +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 : (A:Prop)(C:Prop) A -> (not A) -> C. + Theorem absurd : forall A C:Prop, A -> ~ A -> C. Proof. - Unfold not; Intros A C h1 h2. - NewDestruct (h2 h1). + unfold not in |- *; intros A C h1 h2. + destruct (h2 h1). Qed. Section equality. - Variable A,B : Type. - Variable f : A->B. - Variable x,y,z : A. + Variables A B : Type. + Variable f : A -> B. + Variables x y z : A. - Theorem sym_eq : (eq ? x y) -> (eq ? y x). + Theorem sym_eq : x = y -> y = x. Proof. - NewDestruct 1; Trivial. + destruct 1; trivial. Defined. Opaque sym_eq. - Theorem trans_eq : (eq ? x y) -> (eq ? y z) -> (eq ? x z). + Theorem trans_eq : x = y -> y = z -> x = z. Proof. - NewDestruct 2; Trivial. + destruct 2; trivial. Defined. Opaque trans_eq. - Theorem f_equal : (eq ? x y) -> (eq ? (f x) (f y)). + Theorem f_equal : x = y -> f x = f y. Proof. - NewDestruct 1; Trivial. + destruct 1; trivial. Defined. Opaque f_equal. - Theorem sym_not_eq : (not (eq ? x y)) -> (not (eq ? y x)). + Theorem sym_not_eq : x <> y -> y <> x. Proof. - Red; Intros h1 h2; Apply h1; NewDestruct h2; Trivial. + red in |- *; intros h1 h2; apply h1; destruct h2; trivial. Qed. - Definition sym_equal := sym_eq. + Definition sym_equal := sym_eq. Definition sym_not_equal := sym_not_eq. - Definition trans_equal := trans_eq. + Definition trans_equal := trans_eq. End equality. @@ -250,56 +223,53 @@ Section Logic_lemmas. 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. + 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 : (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. + 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 : (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. + 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 : (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)). +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. - NewDestruct 1; NewDestruct 1; Reflexivity. + destruct 1; destruct 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)). +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. - NewDestruct 1; NewDestruct 1; NewDestruct 1; Reflexivity. + destruct 1; destruct 1; destruct 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)). +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. - NewDestruct 1; NewDestruct 1; NewDestruct 1; NewDestruct 1; Reflexivity. + destruct 1; destruct 1; destruct 1; destruct 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)). +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. - NewDestruct 1; NewDestruct 1; NewDestruct 1; NewDestruct 1; NewDestruct 1; - Reflexivity. + destruct 1; destruct 1; destruct 1; destruct 1; destruct 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). -]. +Hint Immediate sym_eq sym_not_eq: core v62. diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v index 1249e62ea..7f88476a4 100755 --- a/theories/Init/Logic_Type.v +++ b/theories/Init/Logic_Type.v @@ -9,294 +9,81 @@ (*i $Id$ 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 Import 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 notT (A:Type) := A -> False. -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). -Notation "'EXT' x : t | p" := (ex ? [x:t]p) (at level 10, p at level 8). - -(* -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). - -Notation "x === y" := (identityT ? x y) - (at level 5, no associativity) : type_scope. - -(* -Hints Resolve refl_identityT : core v62. -*) -]. Section identity_is_a_congruence. - Variables A,B : Type. - Variable f : A->B. + Variables A B : Type. + Variable f : A -> B. - Variable x,y,z : A. + Variables x y z : A. - Lemma sym_id : (identityT ? x y) -> (identityT ? y x). + Lemma sym_id : identity x y -> identity y x. Proof. - NewDestruct 1; Trivial. + destruct 1; trivial. Qed. - Lemma trans_id : (identityT ? x y) -> (identityT ? y z) -> (identityT ? x z). + Lemma trans_id : identity x y -> identity y z -> identity x z. Proof. - NewDestruct 2; Trivial. + destruct 2; trivial. Qed. - Lemma congr_id : (identityT ? x y)->(identityT ? (f x) (f y)). + Lemma congr_id : identity x y -> identity (f x) (f y). Proof. - NewDestruct 1; Trivial. + destruct 1; trivial. Qed. - Lemma sym_not_id : (notT (identityT ? x y)) -> (notT (identityT ? y x)). + Lemma sym_not_id : notT (identity x y) -> notT (identity y x). Proof. - Red; Intros H H'; Apply H; NewDestruct H'; Trivial. + red in |- *; intros H H'; apply H; destruct 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. + 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 : - (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. +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 : - (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. +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. -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 := identityT_ind_r (only parsing). -Notation identityT_rec_r := identityT_rec_r (only parsing). -Notation identityT_rect_r := identityT_rect_r (only parsing). -]. -Inductive prodT [A,B:Type] : Type := pairT : A -> B -> (prodT A B). +Inductive prodT (A B:Type) : Type := + pairT : A -> B -> prodT A B. Section prodT_proj. - Variables A, B : Type. + 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. + 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)((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. +Definition prodT_uncurry (A B C:Type) (f:prodT A B -> C) + (x:A) (y:B) : C := f (pairT x y). -Hints Immediate sym_id sym_not_id : core v62. +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. -V7only [ -Implicits fstT [1 2]. -Implicits sndT [1 2]. -Implicits pairT [1 2]. -]. +Hint Immediate sym_id sym_not_id: core v62. diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index 624f6c902..ce1d4d7c9 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -12,97 +12,80 @@ (** 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). +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 *) -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). +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). -Uninterpreted Notation "x <> y :> T" - (at level 5, y at next level, no associativity). -Uninterpreted Notation "x <> y" - (at level 5, no associativity). +Reserved Notation "x <> y :> T" +(at level 70, y at next level, no associativity). +Reserved Notation "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" (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). -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). +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) *) -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, left associativity). +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, left associativity). (** Notations for pairs *) -Uninterpreted Notation "( x , y )" (at level 0) - V8only "x , y" (at level 250, left associativity). +Reserved Notation "x , y" (at level 250, left associativity). (** Notations for sum-types *) (* Home-made factorization at level 4 to parse B+{x:A|P} without parentheses *) -Uninterpreted Notation "B + { x : A | P }" - (at level 4, left associativity, only parsing) - V8only (at level 50, x at level 99, left associativity, only parsing). +Reserved Notation "B + { x : A | P }" +(at level 50, x at level 99, left associativity, only parsing). -Uninterpreted Notation "B + { x : A | P & Q }" - (at level 4, left associativity, only parsing) - V8only (at level 50, x at level 99, left associativity, only parsing). +Reserved Notation "B + { x : A | P & Q }" +(at level 50, x at level 99, left associativity, only parsing). -Uninterpreted Notation "B + { x : A & P }" - (at level 4, left associativity, only parsing) - V8only (at level 50, x at level 99, left associativity, only parsing). +Reserved Notation "B + { x : A & P }" +(at level 50, x at level 99, left associativity, only parsing). -Uninterpreted Notation "B + { x : A & P & Q }" - (at level 4, left associativity, only parsing) - V8only (at level 50, x at level 99, left associativity, only parsing). +Reserved Notation "B + { x : A & P & Q }" +(at level 50, x at level 99, left associativity, only parsing). (* At level 1 to factor with {x:A|P} etc *) -Uninterpreted Notation "{ A } + { B }" (at level 1) - V8only (at level 0, A at level 99). +Reserved Notation "{ A } + { B }" (at level 0, A at level 99). -Uninterpreted Notation "A + { B }" (at level 4, left associativity) - V8only (at level 50, B at level 99, left associativity). +Reserved Notation "A + { B }" +(at level 50, B at level 99, 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). +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). -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). +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). -Delimits Scope type_scope with type. -Delimits Scope core_scope with core. +Delimit Scope type_scope with type. +Delimit Scope core_scope with core. Open Scope core_scope. -Open Scope type_scope. +Open Scope type_scope.
\ No newline at end of file diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index 2356c9cb5..3506b9bab 100755 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -23,196 +23,188 @@ 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. +Require Import Notations. +Require Import Datatypes. +Require Import Logic. Open Scope nat_scope. -Definition eq_S := (f_equal nat nat S). +Definition eq_S := f_equal S. -Hint eq_S : v62 := Resolve (f_equal nat nat S). -Hint eq_nat_unary : core := Resolve (f_equal nat). +Hint Resolve (f_equal S): v62. +Hint Resolve (f_equal (A:=nat)): core. (** 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). +Definition pred (n:nat) : nat := match n with + | O => 0 + | S u => u + end. +Hint Resolve (f_equal pred): v62. -Theorem pred_Sn : (m:nat) m=(pred (S m)). +Theorem pred_Sn : forall n:nat, n = pred (S n). Proof. - Auto. + auto. Qed. -Theorem eq_add_S : (n,m:nat) (S n)=(S m) -> n=m. +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)); Auto. + intros n m H; change (pred (S n) = pred (S m)) in |- *; auto. Qed. -Hints Immediate eq_add_S : core v62. +Hint 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)). +Theorem not_eq_S : forall n m:nat, n <> m -> S n <> S m. Proof. - Red; Auto. + red in |- *; auto. Qed. -Hints Resolve not_eq_S : core v62. +Hint Resolve not_eq_S: core v62. -Definition IsSucc : nat->Prop - := [n:nat]Cases n of O => False | (S p) => True end. +Definition IsSucc (n:nat) : Prop := + match n with + | O => False + | S p => True + end. -Theorem O_S : (n:nat)~(O=(S n)). +Theorem O_S : forall n:nat, 0 <> S n. Proof. - Red;Intros n H. - Change (IsSucc O). - Rewrite <- (sym_eq nat O (S n));[Exact I | Assumption]. + red in |- *; intros n H. + change (IsSucc 0) in |- *. + rewrite <- (sym_eq (x:=0) (y:=(S n))); [ exact I | assumption ]. Qed. -Hints Resolve O_S : core v62. +Hint Resolve O_S: core v62. -Theorem n_Sn : (n:nat) ~(n=(S n)). +Theorem n_Sn : forall n:nat, n <> S n. Proof. - NewInduction n ; Auto. + induction n; auto. Qed. -Hints Resolve n_Sn : core v62. +Hint 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). +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. -V8Infix "+" plus : nat_scope. +Infix "+" := plus : nat_scope. -Lemma plus_n_O : (n:nat) n=(plus n O). +Lemma plus_n_O : forall n:nat, n = n + 0. Proof. - NewInduction n ; Simpl ; Auto. + induction n; simpl in |- *; auto. Qed. -Hints Resolve plus_n_O : core v62. +Hint Resolve plus_n_O: core v62. -Lemma plus_O_n : (n:nat) (plus O n)=n. +Lemma plus_O_n : forall n:nat, 0 + n = n. Proof. - Auto. + auto. Qed. -Lemma plus_n_Sm : (n,m:nat) (S (plus n m))=(plus n (S m)). +Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m. Proof. - Intros n m; NewInduction n; Simpl; Auto. + intros n m; induction n; simpl in |- *; auto. Qed. -Hints Resolve plus_n_Sm : core v62. +Hint Resolve plus_n_Sm: core v62. -Lemma plus_Sn_m : (n,m:nat)(plus (S n) m)=(S (plus n m)). +Lemma plus_Sn_m : forall n m:nat, S n + m = S (n + m). Proof. - Auto. + 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). +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. -V8Infix "*" mult : nat_scope. +Infix "*" := mult : nat_scope. -Lemma mult_n_O : (n:nat) O=(mult n O). +Lemma mult_n_O : forall n:nat, 0 = n * 0. Proof. - NewInduction n; Simpl; Auto. + induction n; simpl in |- *; auto. Qed. -Hints Resolve mult_n_O : core v62. +Hint Resolve mult_n_O: core v62. -Lemma mult_n_Sm : (n,m:nat) (plus (mult n m) n)=(mult n (S m)). +Lemma mult_n_Sm : forall n m:nat, n * m + n = 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. + 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. -Hints Resolve mult_n_Sm : core v62. +Hint 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. +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. -V8Infix "-" minus : nat_scope. +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 : (m:nat)(le n m)->(le n (S m)). +Inductive le (n:nat) : nat -> Prop := + | le_n : le n n + | le_S : forall m:nat, le n m -> le n (S m). -V8Infix "<=" le : nat_scope. +Infix "<=" := le : nat_scope. -Hint constr_le : core v62 := Constructors le. +Hint Constructors le: core v62. (*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. +Definition lt (n m:nat) := S n <= m. +Hint Unfold lt: core v62. -V8Infix "<" lt : nat_scope. +Infix "<" := lt : nat_scope. -Definition ge := [n,m:nat](le m n). -Hints Unfold ge : core v62. +Definition ge (n m:nat) := m <= n. +Hint Unfold ge: core v62. -V8Infix ">=" ge : nat_scope. +Infix ">=" := ge : nat_scope. -Definition gt := [n,m:nat](lt m n). -Hints Unfold gt : core v62. +Definition gt (n m:nat) := m < n. +Hint Unfold gt: core v62. -V8Infix ">" gt : nat_scope. +Infix ">" := 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. +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 : (n:nat)(P:nat->Prop)(P O)->((m:nat)(P (S m)))->(P n). +Theorem nat_case : + forall (n:nat) (P:nat -> Prop), P 0 -> (forall m:nat, P (S m)) -> P n. Proof. - NewInduction n ; Auto. + induction 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). +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. - NewInduction n; Auto. - NewDestruct m; Auto. + induction n; auto. + destruct m as [| n0]; 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/theories/Init/Prelude.v b/theories/Init/Prelude.v index 7325cc771..f5be0d594 100755 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -13,4 +13,4 @@ Require Export Logic. Require Export Datatypes. Require Export Specif. Require Export Peano. -Require Export Wf. +Require Export Wf.
\ No newline at end of file diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 2e49fab04..eb775505f 100755 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -9,13 +9,12 @@ (*i $Id$ i*) Set Implicit Arguments. -V7only [Unset Implicit Arguments.]. (** Basic specifications : Sets containing logical information *) -Require Notations. -Require Datatypes. -Require Logic. +Require Import Notations. +Require Import Datatypes. +Require Import Logic. (** Subsets *) @@ -24,31 +23,33 @@ Require Logic. 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 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 : (x:A)(P x) -> (Q x) -> (sig2 A P Q). +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 : (x:A)(P x) -> (sigS A P). +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 : (x:A)(P x) -> (Q x) -> (sigS2 A P Q). +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 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. +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. @@ -60,15 +61,17 @@ Add Printing Let sigS2. Section Subset_projections. - Variable A:Set. - Variable P:A->Prop. + Variable A : Set. + Variable P : A -> Prop. - Definition proj1_sig := - [e:(sig A P)]Cases e of (exist a b) => a end. + Definition proj1_sig (e:sig P) := match e with + | 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. + Definition proj2_sig (e:sig P) := + match e return P (proj1_sig e) with + | exist a b => b + end. End Subset_projections. @@ -77,46 +80,46 @@ End Subset_projections. Section Projections. - Variable A:Set. - Variable P:A->Set. + 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. + 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} +Inductive sumbool (A B:Prop) : Set := + | left : A -> {A} + {B} + | right : B -> {A} + {B} + where "{ A } + { B }" := (sumbool A B) : type_scope. -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. +Inductive sumor (A:Set) (B:Prop) : Set := + | inleft : A -> A + {B} + | inright : B -> A + {B} + where "A + { B }" := (sumor A B) : type_scope. (* Factorizing "sumor" at level 4 to parse B+{x:A|P} without parentheses *) -Notation "B + { x : A | P }" := B + (sig A [x:A]P) +Notation "B + { x : A | P }" := (B + sig (fun x:A => P)) (only parsing) : type_scope. -Notation "B + { x : A | P & Q }" := B + (sig2 A [x:A]P [x:A]Q) +Notation "B + { x : A | P & Q }" := (B + sig2 (fun x:A => P) (fun x:A => Q)) (only parsing) : type_scope. -Notation "B + { x : A & P }" := B + (sigS A [x:A]P) +Notation "B + { x : A & P }" := (B + sigS (fun x:A => P)) (only parsing) : type_scope. -Notation "B + { x : A & P & Q }" := B + (sigS2 A [x:A]P [x:A]Q) +Notation "B + { x : A & P & Q }" := (B + sigS2 (fun x:A => P) (fun x:A => Q)) (only parsing) : type_scope. (** Choice *) @@ -125,35 +128,46 @@ 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. + 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))). + 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 [z:S]Cases (H z) of (exist y _) => y end. - Intro z; NewDestruct (H z); Trivial. + intro H. + exists (fun z:S => match H z with + | exist y _ => y + end). + intro z; destruct (H z); trivial. Qed. - Lemma Choice2 : ((x:S)(sigS ? [y:S'](R' x y))) -> - (sigS ? [f:S->S'](z:S)(R' z (f z))). + 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 [z:S]Cases (H z) of (existS y _) => y end. - Intro z; NewDestruct (H z); Trivial. + intro H. + exists (fun z:S => match H z with + | existS y _ => y + end). + intro z; destruct (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)))). + 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 [z:S]Cases (H z) of (left _) => true | (right _) => false end. - Intro z; NewDestruct (H z); Auto. + 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. @@ -165,51 +179,41 @@ End Choice_lemmas. Definition Exc := option. Definition value := Some. -Definition error := !None. +Definition error := @None. -Implicits error [1]. +Implicit Arguments error [A]. Definition except := False_rec. (* for compatibility with previous versions *) -Implicits except [1]. +Implicit Arguments except [P]. -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. +Theorem absurd_set : forall (A:Prop) (C:Set), A -> ~ A -> C. Proof. - Intros A C h1 h2. - Apply False_rec. - Apply (h2 h1). + intros A C h1 h2. + apply False_rec. + apply (h2 h1). Qed. -Hints Resolve left right inleft inright : core v62. +Hint 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). +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. + 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 projT1 (H:sigT P) : A := match H with + | 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. + 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. -V7only [ -Notation ProjS1 := (projS1 ? ?). -Notation ProjS2 := (projS2 ? ?). -Notation Value := (value ?). -]. - diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index ee7da4ba6..476ec4a54 100755 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -7,7 +7,6 @@ (***********************************************************************) Set Implicit Arguments. -V7only [Unset Implicit Arguments.]. (*i $Id$ i*) @@ -17,24 +16,24 @@ V7only [Unset Implicit Arguments.]. from a well-founded ordering on a given set *) -Require Notations. -Require Logic. -Require Datatypes. +Require Import Notations. +Require Import Logic. +Require Import Datatypes. (** Well-founded induction principle on Prop *) -Chapter Well_founded. +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 : (x:A)((y:A)(R y x)->(Acc y))->(Acc x). + Inductive Acc : A -> Prop := + Acc_intro : forall x:A, (forall 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. + Lemma Acc_inv : forall x:A, Acc x -> forall y:A, R y x -> Acc y. + destruct 1; trivial. Defined. (** the informative elimination : @@ -42,50 +41,56 @@ Chapter Well_founded. 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). + 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)] : (P x) - := (F x (Acc_inv x a) ([y:A][h:(R y x)](Acc_rect y (Acc_inv x a y h)))). + 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). + 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). + Variable F : forall x:A, (forall 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)))). + 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 := (a:A)(Acc a). + Definition well_founded := forall 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). + 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. + 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). + forall P:A -> Set, + (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a. Proof. - Exact [P:A->Set](well_founded_induction_type P). + exact (fun 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). + 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 [P:A->Prop](well_founded_induction_type P). + exact (fun P:A -> Prop => well_founded_induction_type P). Defined. (** Building fixpoints *) @@ -93,40 +98,41 @@ Chapter Well_founded. Section FixPoint. Variable P : A -> Set. -Variable F : (x:A)((y:A)(R y x)->(P y))->(P x). +Variable F : forall x:A, (forall 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))). +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 x (Rwf x)). +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 : - (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). +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 - : (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. +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 : (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. +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 : (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. +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. @@ -135,24 +141,31 @@ End Well_founded. (** A recursor over pairs *) -Chapter Well_founded_2. +Section Well_founded_2. - Variable A,B : Set. + Variables 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). + 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. + intros; apply Acc_iter_2; auto. Defined. End Well_founded_2. - |