diff options
Diffstat (limited to 'theories/Init')
| -rw-r--r-- | theories/Init/Datatypes.v | 32 | ||||
| -rw-r--r-- | theories/Init/Logic.v | 92 | ||||
| -rw-r--r-- | theories/Init/Peano.v | 17 | ||||
| -rw-r--r-- | theories/Init/Tactics.v | 38 |
4 files changed, 88 insertions, 91 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index fdd7ba35..56dc7e95 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Datatypes.v 8872 2006-05-29 07:36:28Z herbelin $ i*) +(*i $Id: Datatypes.v 9245 2006-10-17 12:53:34Z notin $ i*) Set Implicit Arguments. @@ -48,7 +48,7 @@ Inductive Empty_set : Set :=. sole inhabitant is denoted [refl_identity A a] *) Inductive identity (A:Type) (a:A) : A -> Type := - refl_identity : identity (A:=A) a a. + refl_identity : identity (A:=A) a a. Hint Resolve refl_identity: core v62. Implicit Arguments identity_ind [A]. @@ -65,8 +65,8 @@ Implicit Arguments None [A]. Definition option_map (A B:Type) (f:A->B) o := match o with - | Some a => Some (f a) - | None => None + | Some a => Some (f a) + | None => None end. (** [sum A B], written [A + B], is the disjoint sum of [A] and [B] *) @@ -81,7 +81,7 @@ Notation "x + y" := (sum x y) : type_scope. the pair [pair A B a b] of [a] and [b] is abbreviated [(a,b)] *) Inductive prod (A B:Type) : Type := - pair : A -> B -> prod A B. + pair : A -> B -> prod A B. Add Printing Let prod. Notation "x * y" := (prod x y) : type_scope. @@ -90,27 +90,27 @@ Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope. Section projections. Variables A B : Type. Definition fst (p:A * B) := match p with - | (x, y) => x + | (x, y) => x end. Definition snd (p:A * B) := match p with - | (x, y) => y + | (x, y) => y end. End projections. Hint Resolve pair inl inr: core v62. Lemma surjective_pairing : - forall (A B:Type) (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:Type) (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) @@ -130,9 +130,9 @@ Inductive comparison : Set := Definition CompOpp (r:comparison) := match r with - | Eq => Eq - | Lt => Gt - | Gt => Lt + | Eq => Eq + | Lt => Gt + | Gt => Lt end. (* Compatibility *) diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 71583718..8b487432 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -6,17 +6,17 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Logic.v 8936 2006-06-09 15:43:33Z herbelin $ i*) +(*i $Id: Logic.v 9245 2006-10-17 12:53:34Z notin $ i*) Set Implicit Arguments. Require Import Notations. -(** *** Propositional connectives *) +(** * Propositional connectives *) (** [True] is the always true proposition *) Inductive True : Prop := - I : True. + I : True. (** [False] is the always false proposition *) Inductive False : Prop :=. @@ -36,8 +36,8 @@ Hint Unfold not: core. [proj1] and [proj2] are first and second projections of a conjunction *) Inductive and (A B:Prop) : Prop := - conj : A -> B -> A /\ B - + conj : A -> B -> A /\ B + where "A /\ B" := (and A B) : type_scope. Section Conjunction. @@ -46,12 +46,12 @@ Section Conjunction. 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. @@ -97,7 +97,7 @@ 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, right associativity) : type_scope. -(** *** First-order quantifiers *) +(** * 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 @@ -112,16 +112,16 @@ Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3) is provided too. *) -(* Remark: [exists x, Q] denotes [ex (fun x => Q)] so that [exists x, +(** 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. @@ -131,14 +131,14 @@ Notation "'exists' x , p" := (ex (fun x => p)) (at level 200, x ident, right associativity) : type_scope. Notation "'exists' x : t , p" := (ex (fun x:t => p)) (at level 200, x ident, right associativity, - format "'[' 'exists' '/ ' x : t , '/ ' p ']'") + 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, 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, right associativity, - format "'[' 'exists2' '/ ' x : t , '/ ' '[' p & '/' q ']' ']'") + format "'[' 'exists2' '/ ' x : t , '/ ' '[' p & '/' q ']' ']'") : type_scope. (** Derived rules for universal quantification *) @@ -150,17 +150,17 @@ 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 *) +(** * Equality *) (** [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]. @@ -202,27 +202,27 @@ 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. @@ -231,14 +231,14 @@ Section Logic_lemmas. 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. @@ -246,34 +246,34 @@ 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. @@ -294,22 +294,26 @@ Definition uniqueness (A:Type) (P:A->Prop) := forall x y, P x -> P y -> x = y. Notation "'exists' ! x , P" := (ex (unique (fun x => P))) (at level 200, x ident, right associativity, - format "'[' 'exists' ! '/ ' x , '/ ' P ']'") : type_scope. + 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. + 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 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. + 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/Peano.v b/theories/Init/Peano.v index c0416b63..3df2b566 100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Peano.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Peano.v 9245 2006-10-17 12:53:34Z notin $ i*) (** The type [nat] of Peano natural numbers (built from [O] and [S]) is defined in [Datatypes.v] *) @@ -47,14 +47,16 @@ 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. @@ -65,19 +67,18 @@ Proof. Qed. Hint Resolve not_eq_S: core v62. -(** Zero is not the successor of a number *) - Definition IsSucc (n:nat) : Prop := match n with | O => False | 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. diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index ce37715e..ba210dd6 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Tactics.v 8100 2006-02-27 12:10:03Z letouzey $ i*) +(*i $Id: Tactics.v 9268 2006-10-24 12:56:16Z herbelin $ i*) Require Import Notations. Require Import Logic. @@ -15,7 +15,7 @@ Require Import Logic. (* A shorter name for generalize + clear, can be seen as an anti-intro *) -Ltac revert H := generalize H; clear H. +Tactic Notation "revert" ne_hyp_list(l) := generalize l; clear l. (* to contradict an hypothesis without copying its type. *) @@ -49,24 +49,16 @@ Ltac f_equal := | _ => idtac end. -(* Rewriting in all hypothesis. *) - -Ltac rewrite_all Eq := match type of Eq with - ?a = ?b => - generalize Eq; clear Eq; - match goal with - | H : context [a] |- _ => intro Eq; rewrite Eq in H; rewrite_all Eq - | _ => intro Eq; try rewrite Eq - end - end. - -Ltac rewrite_all_rev Eq := match type of Eq with - ?a = ?b => - generalize Eq; clear Eq; - match goal with - | H : context [b] |- _ => intro Eq; rewrite <- Eq in H; rewrite_all_rev Eq - | _ => intro Eq; try rewrite <- Eq - end - end. - -Tactic Notation "rewrite_all" "<-" constr(H) := rewrite_all_rev H. +(* 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. |