diff options
Diffstat (limited to 'theories/Init')
| -rw-r--r-- | theories/Init/Datatypes.v | 204 | ||||
| -rw-r--r-- | theories/Init/Logic.v | 140 | ||||
| -rw-r--r-- | theories/Init/Logic_Type.v | 14 | ||||
| -rw-r--r-- | theories/Init/Notations.v | 4 | ||||
| -rw-r--r-- | theories/Init/Peano.v | 120 | ||||
| -rw-r--r-- | theories/Init/Prelude.v | 8 | ||||
| -rw-r--r-- | theories/Init/Specif.v | 64 | ||||
| -rw-r--r-- | theories/Init/Tactics.v | 22 | ||||
| -rw-r--r-- | theories/Init/Wf.v | 6 |
9 files changed, 369 insertions, 213 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index deadec43..fc620f71 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -1,25 +1,33 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Datatypes.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Set Implicit Arguments. Require Import Notations. Require Import Logic. Declare ML Module "nat_syntax_plugin". +(********************************************************************) +(** * Datatypes with zero and one element *) + +(** [Empty_set] is a datatype with no inhabitant *) + +Inductive Empty_set : Set :=. (** [unit] is a singleton datatype with sole inhabitant [tt] *) Inductive unit : Set := tt : unit. + +(********************************************************************) +(** * The boolean datatype *) + (** [bool] is the datatype of the boolean values [true] and [false] *) Inductive bool : Set := @@ -53,9 +61,7 @@ Definition negb (b:bool) := if b then false else true. Infix "||" := orb : bool_scope. Infix "&&" := andb : bool_scope. -(*******************************) -(** * Properties of [andb] *) -(*******************************) +(** Basic properties of [andb] *) Lemma andb_prop : forall a b:bool, andb a b = true -> a = true /\ b = true. Proof. @@ -66,7 +72,7 @@ Hint Resolve andb_prop: bool. Lemma andb_true_intro : forall b1 b2:bool, b1 = true /\ b2 = true -> andb b1 b2 = true. Proof. - destruct b1; destruct b2; simpl in |- *; tauto || auto with bool. + destruct b1; destruct b2; simpl; intros [? ?]; assumption. Qed. Hint Resolve andb_true_intro: bool. @@ -104,6 +110,22 @@ Proof. intros P b H H0; destruct H0 in H; assumption. Defined. +(** The [BoolSpec] inductive will be used to relate a [boolean] value + and two propositions corresponding respectively to the [true] + case and the [false] case. + Interest: [BoolSpec] behave nicely with [case] and [destruct]. + See also [Bool.reflect] when [Q = ~P]. +*) + +Inductive BoolSpec (P Q : Prop) : bool -> Prop := + | BoolSpecT : P -> BoolSpec P Q true + | BoolSpecF : Q -> BoolSpec P Q false. +Hint Constructors BoolSpec. + + +(********************************************************************) +(** * Peano natural numbers *) + (** [nat] is the datatype of natural numbers built from [O] and successor [S]; note that the constructor name is the letter O. Numbers in [nat] can be denoted using a decimal notation; @@ -115,23 +137,11 @@ Inductive nat : Set := Delimit Scope nat_scope with nat. Bind Scope nat_scope with nat. -Arguments Scope S [nat_scope]. +Arguments S _%nat. -(** [Empty_set] has no inhabitant *) -Inductive Empty_set : Set :=. - -(** [identity A a] is the family of datatypes on [A] whose sole non-empty - member is the singleton datatype [identity A a a] whose - sole inhabitant is denoted [refl_identity A a] *) - -Inductive identity (A:Type) (a:A) : A -> Type := - identity_refl : identity a a. -Hint Resolve identity_refl: core. - -Implicit Arguments identity_ind [A]. -Implicit Arguments identity_rec [A]. -Implicit Arguments identity_rect [A]. +(********************************************************************) +(** * Container datatypes *) (** [option A] is the extension of [A] with an extra element [None] *) @@ -139,7 +149,7 @@ Inductive option (A:Type) : Type := | Some : A -> option A | None : option A. -Implicit Arguments None [A]. +Arguments None [A]. Definition option_map (A B:Type) (f:A->B) o := match o with @@ -155,6 +165,9 @@ Inductive sum (A B:Type) : Type := Notation "x + y" := (sum x y) : type_scope. +Arguments inl {A B} _ , [A] B _. +Arguments inr {A B} _ , A [B] _. + (** [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)] *) @@ -166,6 +179,8 @@ Add Printing Let prod. Notation "x * y" := (prod x y) : type_scope. Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope. +Arguments pair {A B} _ _. + Section projections. Variables A B : Type. Definition fst (p:A * B) := match p with @@ -188,7 +203,7 @@ Lemma injective_projections : 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. + destruct p1; destruct p2; simpl; intros Hfst Hsnd. rewrite Hfst; rewrite Hsnd; reflexivity. Qed. @@ -200,7 +215,40 @@ Definition prod_curry (A B C:Type) (f:A -> B -> C) | pair x y => f x y end. -(** Comparison *) +(** Polymorphic lists and some operations *) + +Inductive list (A : Type) : Type := + | nil : list A + | cons : A -> list A -> list A. + +Arguments nil [A]. +Infix "::" := cons (at level 60, right associativity) : list_scope. +Delimit Scope list_scope with list. +Bind Scope list_scope with list. + +Local Open Scope list_scope. + +Definition length (A : Type) : list A -> nat := + fix length l := + match l with + | nil => O + | _ :: l' => S (length l') + end. + +(** Concatenation of two lists *) + +Definition app (A : Type) : list A -> list A -> list A := + fix app l m := + match l with + | nil => m + | a :: l1 => a :: app l1 m + end. + +Infix "++" := app (right associativity, at level 60) : list_scope. + + +(********************************************************************) +(** * The comparison datatype *) Inductive comparison : Set := | Eq : comparison @@ -229,81 +277,81 @@ Proof. split; intros; apply CompOpp_inj; rewrite CompOpp_involutive; auto. Qed. -(** The [CompSpec] inductive will be used to relate a [compare] function - (returning a comparison answer) and some equality and order predicates. - Interest: [CompSpec] behave nicely with [case] and [destruct]. *) +(** The [CompareSpec] inductive relates a [comparison] value with three + propositions, one for each possible case. Typically, it can be used to + specify a comparison function via some equality and order predicates. + Interest: [CompareSpec] behave nicely with [case] and [destruct]. *) -Inductive CompSpec {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Prop := - | CompEq : eq x y -> CompSpec eq lt x y Eq - | CompLt : lt x y -> CompSpec eq lt x y Lt - | CompGt : lt y x -> CompSpec eq lt x y Gt. -Hint Constructors CompSpec. +Inductive CompareSpec (Peq Plt Pgt : Prop) : comparison -> Prop := + | CompEq : Peq -> CompareSpec Peq Plt Pgt Eq + | CompLt : Plt -> CompareSpec Peq Plt Pgt Lt + | CompGt : Pgt -> CompareSpec Peq Plt Pgt Gt. +Hint Constructors CompareSpec. -(** For having clean interfaces after extraction, [CompSpec] is declared +(** For having clean interfaces after extraction, [CompareSpec] is declared in Prop. For some situations, it is nonetheless useful to have a - version in Type. Interestingly, these two versions are equivalent. -*) + version in Type. Interestingly, these two versions are equivalent. *) -Inductive CompSpecT {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Type := - | CompEqT : eq x y -> CompSpecT eq lt x y Eq - | CompLtT : lt x y -> CompSpecT eq lt x y Lt - | CompGtT : lt y x -> CompSpecT eq lt x y Gt. -Hint Constructors CompSpecT. +Inductive CompareSpecT (Peq Plt Pgt : Prop) : comparison -> Type := + | CompEqT : Peq -> CompareSpecT Peq Plt Pgt Eq + | CompLtT : Plt -> CompareSpecT Peq Plt Pgt Lt + | CompGtT : Pgt -> CompareSpecT Peq Plt Pgt Gt. +Hint Constructors CompareSpecT. -Lemma CompSpec2Type : forall A (eq lt:A->A->Prop) x y c, - CompSpec eq lt x y c -> CompSpecT eq lt x y c. +Lemma CompareSpec2Type : forall Peq Plt Pgt c, + CompareSpec Peq Plt Pgt c -> CompareSpecT Peq Plt Pgt c. Proof. destruct c; intros H; constructor; inversion_clear H; auto. Defined. -(** Identity *) +(** As an alternate formulation, one may also directly refer to predicates + [eq] and [lt] for specifying a comparison, rather that fully-applied + propositions. This [CompSpec] is now a particular case of [CompareSpec]. *) -Definition ID := forall A:Type, A -> A. -Definition id : ID := fun A x => x. +Definition CompSpec {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Prop := + CompareSpec (eq x y) (lt x y) (lt y x). +Definition CompSpecT {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Type := + CompareSpecT (eq x y) (lt x y) (lt y x). +Hint Unfold CompSpec CompSpecT. -(** Polymorphic lists and some operations *) +Lemma CompSpec2Type : forall A (eq lt:A->A->Prop) x y c, + CompSpec eq lt x y c -> CompSpecT eq lt x y c. +Proof. intros. apply CompareSpec2Type; assumption. Defined. -Inductive list (A : Type) : Type := - | nil : list A - | cons : A -> list A -> list A. -Implicit Arguments nil [A]. -Infix "::" := cons (at level 60, right associativity) : list_scope. -Delimit Scope list_scope with list. -Bind Scope list_scope with list. +(******************************************************************) +(** * Misc Other Datatypes *) -Local Open Scope list_scope. +(** [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] *) -Definition length (A : Type) : list A -> nat := - fix length l := - match l with - | nil => O - | _ :: l' => S (length l') - end. +Inductive identity (A:Type) (a:A) : A -> Type := + identity_refl : identity a a. +Hint Resolve identity_refl: core. -(** Concatenation of two lists *) +Arguments identity_ind [A] a P f y i. +Arguments identity_rec [A] a P f y i. +Arguments identity_rect [A] a P f y i. -Definition app (A : Type) : list A -> list A -> list A := - fix app l m := - match l with - | nil => m - | a :: l1 => a :: app l1 m - end. +(** Identity type *) + +Definition ID := forall A:Type, A -> A. +Definition id : ID := fun A x => x. -Infix "++" := app (right associativity, at level 60) : list_scope. (* begin hide *) (* 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). +Notation prodT := prod (compat "8.2"). +Notation pairT := pair (compat "8.2"). +Notation prodT_rect := prod_rect (compat "8.2"). +Notation prodT_rec := prod_rec (compat "8.2"). +Notation prodT_ind := prod_ind (compat "8.2"). +Notation fstT := fst (compat "8.2"). +Notation sndT := snd (compat "8.2"). +Notation prodT_uncurry := prod_uncurry (compat "8.2"). +Notation prodT_curry := prod_curry (compat "8.2"). (* end hide *) diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index b95d78a4..4e6df444 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Logic.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Set Implicit Arguments. Require Import Notations. @@ -64,6 +62,9 @@ Inductive or (A B:Prop) : Prop := where "A \/ B" := (or A B) : type_scope. +Arguments or_introl [A B] _, [A] B _. +Arguments or_intror [A B] _, A [B] _. + (** [iff A B], written [A <-> B], expresses the equivalence of [A] and [B] *) Definition iff (A B:Prop) := (A -> B) /\ (B -> A). @@ -95,53 +96,53 @@ Hint Unfold iff: extcore. Theorem neg_false : forall A : Prop, ~ A <-> (A <-> False). Proof. -intro A; unfold not; split. -intro H; split; [exact H | intro H1; elim H1]. -intros [H _]; exact H. + intro A; unfold not; split. + - intro H; split; [exact H | intro H1; elim H1]. + - intros [H _]; exact H. Qed. Theorem and_cancel_l : forall A B C : Prop, (B -> A) -> (C -> A) -> ((A /\ B <-> A /\ C) <-> (B <-> C)). Proof. -intros; tauto. + intros; tauto. Qed. Theorem and_cancel_r : forall A B C : Prop, (B -> A) -> (C -> A) -> ((B /\ A <-> C /\ A) <-> (B <-> C)). Proof. -intros; tauto. + intros; tauto. Qed. Theorem and_comm : forall A B : Prop, A /\ B <-> B /\ A. Proof. -intros; tauto. + intros; tauto. Qed. Theorem and_assoc : forall A B C : Prop, (A /\ B) /\ C <-> A /\ B /\ C. Proof. -intros; tauto. + intros; tauto. Qed. Theorem or_cancel_l : forall A B C : Prop, (B -> ~ A) -> (C -> ~ A) -> ((A \/ B <-> A \/ C) <-> (B <-> C)). Proof. -intros; tauto. + intros; tauto. Qed. Theorem or_cancel_r : forall A B C : Prop, (B -> ~ A) -> (C -> ~ A) -> ((B \/ A <-> C \/ A) <-> (B <-> C)). Proof. -intros; tauto. + intros; tauto. Qed. Theorem or_comm : forall A B : Prop, (A \/ B) <-> (B \/ A). Proof. -intros; tauto. + intros; tauto. Qed. Theorem or_assoc : forall A B C : Prop, (A \/ B) \/ C <-> A \/ B \/ C. Proof. -intros; tauto. + intros; tauto. Qed. (** Backward direction of the equivalences above does not need assumptions *) @@ -149,35 +150,35 @@ Qed. Theorem and_iff_compat_l : forall A B C : Prop, (B <-> C) -> (A /\ B <-> A /\ C). Proof. -intros; tauto. + intros; tauto. Qed. Theorem and_iff_compat_r : forall A B C : Prop, (B <-> C) -> (B /\ A <-> C /\ A). Proof. -intros; tauto. + intros; tauto. Qed. Theorem or_iff_compat_l : forall A B C : Prop, (B <-> C) -> (A \/ B <-> A \/ C). Proof. -intros; tauto. + intros; tauto. Qed. Theorem or_iff_compat_r : forall A B C : Prop, (B <-> C) -> (B \/ A <-> C \/ A). Proof. -intros; tauto. + intros; tauto. Qed. Lemma iff_and : forall A B : Prop, (A <-> B) -> (A -> B) /\ (B -> A). Proof. -intros A B []; split; trivial. + intros A B []; split; trivial. Qed. Lemma iff_to_and : forall A B : Prop, (A <-> B) <-> (A -> B) /\ (B -> A). Proof. -intros; tauto. + intros; tauto. Qed. (** [(IF_then_else P Q R)], written [IF P then Q else R] denotes @@ -218,11 +219,9 @@ 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, 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 ']'") +Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..)) + (at level 200, x binder, right associativity, + format "'[' 'exists' '/ ' x .. y , '/ ' p ']'") : type_scope. Notation "'exists2' x , p & q" := (ex2 (fun x => p) (fun x => q)) @@ -241,12 +240,12 @@ Section universal_quantification. Theorem inst : forall x:A, all (fun x => P x) -> P x. Proof. - unfold all in |- *; auto. + unfold all; auto. Qed. Theorem gen : forall (B:Prop) (f:forall y:A, B -> P y), B -> all P. Proof. - red in |- *; auto. + red; auto. Qed. End universal_quantification. @@ -271,11 +270,12 @@ Notation "x = y" := (x = y :>_) : type_scope. Notation "x <> y :> T" := (~ x = y :>T) : type_scope. Notation "x <> y" := (x <> y :>_) : type_scope. -Implicit Arguments eq [ [A] ]. +Arguments eq {A} x _. +Arguments eq_refl {A x} , [A] x. -Implicit Arguments eq_ind [A]. -Implicit Arguments eq_rec [A]. -Implicit Arguments eq_rect [A]. +Arguments eq_ind [A] x P _ y _. +Arguments eq_rec [A] x P _ y _. +Arguments eq_rect [A] x P _ y _. Hint Resolve I conj or_introl or_intror eq_refl: core. Hint Resolve ex_intro ex_intro2: core. @@ -284,7 +284,7 @@ Section Logic_lemmas. Theorem absurd : forall A C:Prop, A -> ~ A -> C. Proof. - unfold not in |- *; intros A C h1 h2. + unfold not; intros A C h1 h2. destruct (h2 h1). Qed. @@ -313,7 +313,7 @@ Section Logic_lemmas. Theorem not_eq_sym : x <> y -> y <> x. Proof. - red in |- *; intros h1 h2; apply h1; destruct h2; trivial. + red; intros h1 h2; apply h1; destruct h2; trivial. Qed. End equality. @@ -334,6 +334,15 @@ Section Logic_lemmas. Defined. End Logic_lemmas. +Module EqNotations. + Notation "'rew' H 'in' H'" := (eq_rect _ _ H' _ H) + (at level 10, H' at level 10). + Notation "'rew' <- H 'in' H'" := (eq_rect_r _ H' H) + (at level 10, H' at level 10). + Notation "'rew' -> H 'in' H'" := (eq_rect _ _ H' _ H) + (at level 10, H' at level 10, only parsing). +End EqNotations. + 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. @@ -369,14 +378,14 @@ Qed. (* Aliases *) -Notation sym_eq := eq_sym (only parsing). -Notation trans_eq := eq_trans (only parsing). -Notation sym_not_eq := not_eq_sym (only parsing). +Notation sym_eq := eq_sym (compat "8.3"). +Notation trans_eq := eq_trans (compat "8.3"). +Notation sym_not_eq := not_eq_sym (compat "8.3"). -Notation refl_equal := eq_refl (only parsing). -Notation sym_equal := eq_sym (only parsing). -Notation trans_equal := eq_trans (only parsing). -Notation sym_not_equal := not_eq_sym (only parsing). +Notation refl_equal := eq_refl (compat "8.3"). +Notation sym_equal := eq_sym (compat "8.3"). +Notation trans_equal := eq_trans (compat "8.3"). +Notation sym_not_equal := not_eq_sym (compat "8.3"). Hint Immediate eq_sym not_eq_sym: core. @@ -392,26 +401,47 @@ 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. +Notation "'exists' ! x .. y , p" := + (ex (unique (fun x => .. (ex (unique (fun y => p))) ..))) + (at level 200, x binder, right associativity, + format "'[' 'exists' ! '/ ' x .. y , '/ ' 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. + - 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. +Lemma forall_exists_unique_domain_coincide : + forall A (P:A->Prop), (exists! x, P x) -> + forall Q:A->Prop, (forall x, P x -> Q x) <-> (exists x, P x /\ Q x). +Proof. + intros A P (x & Hp & Huniq); split. + - intro; exists x; auto. + - intros (x0 & HPx0 & HQx0) x1 HPx1. + replace x1 with x0 by (transitivity x; [symmetry|]; auto). + assumption. +Qed. + +Lemma forall_exists_coincide_unique_domain : + forall A (P:A->Prop), + (forall Q:A->Prop, (forall x, P x -> Q x) <-> (exists x, P x /\ Q x)) + -> (exists! x, P x). +Proof. + intros A P H. + destruct H with (Q:=P) as ((x & Hx & _),_); [trivial|]. + exists x. split; [trivial|]. + destruct H with (Q:=fun x'=>x=x') as (_,Huniq). + apply Huniq. exists x; auto. +Qed. + (** * Being inhabited *) (** The predicate [inhabited] can be used in different contexts. If [A] is @@ -436,7 +466,7 @@ Qed. Lemma eq_stepl : forall (A : Type) (x y z : A), x = y -> x = z -> z = y. Proof. -intros A x y z H1 H2. rewrite <- H2; exact H1. + intros A x y z H1 H2. rewrite <- H2; exact H1. Qed. Declare Left Step eq_stepl. @@ -444,7 +474,7 @@ Declare Right Step eq_trans. Lemma iff_stepl : forall A B C : Prop, (A <-> B) -> (A <-> C) -> (C <-> B). Proof. -intros; tauto. + intros; tauto. Qed. Declare Left Step iff_stepl. diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v index bf4031d5..0281c516 100644 --- a/theories/Init/Logic_Type.v +++ b/theories/Init/Logic_Type.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Logic_Type.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** This module defines type constructors for types in [Type] ([Datatypes.v] and [Logic.v] defined them for types in [Set]) *) @@ -46,7 +44,7 @@ Section identity_is_a_congruence. Lemma not_identity_sym : notT (identity x y) -> notT (identity y x). Proof. - red in |- *; intros H H'; apply H; destruct H'; trivial. + red; intros H H'; apply H; destruct H'; trivial. Qed. End identity_is_a_congruence. @@ -68,7 +66,7 @@ Defined. Hint Immediate identity_sym not_identity_sym: core v62. -Notation refl_id := identity_refl (only parsing). -Notation sym_id := identity_sym (only parsing). -Notation trans_id := identity_trans (only parsing). -Notation sym_not_id := not_identity_sym (only parsing). +Notation refl_id := identity_refl (compat "8.3"). +Notation sym_id := identity_sym (compat "8.3"). +Notation trans_id := identity_trans (compat "8.3"). +Notation sym_not_id := not_identity_sym (compat "8.3"). diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index 3619d827..323dab90 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Notations.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** These are the notations whose level and associativity are imposed by Coq *) (** Notations for propositional connectives *) diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index abf843bf..8c6fba50 100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Peano.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** The type [nat] of Peano natural numbers (built from [O] and [S]) is defined in [Datatypes.v] *) @@ -28,7 +26,6 @@ Require Import Notations. Require Import Datatypes. Require Import Logic. -Unset Boxed Definitions. Open Scope nat_scope. @@ -52,18 +49,12 @@ Qed. (** Injectivity of successor *) -Theorem eq_add_S : forall n m:nat, S n = S m -> n = m. -Proof. - 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. - +Definition eq_add_S n m (H: S n = S m): n = m := f_equal pred H. Hint Immediate eq_add_S: core. Theorem not_eq_S : forall n m:nat, n <> m -> S n <> S m. Proof. - red in |- *; auto. + red; auto. Qed. Hint Resolve not_eq_S: core. @@ -102,7 +93,7 @@ Hint Resolve (f_equal2 (A1:=nat) (A2:=nat)): core. Lemma plus_n_O : forall n:nat, n = n + 0. Proof. - induction n; simpl in |- *; auto. + induction n; simpl; auto. Qed. Hint Resolve plus_n_O: core. @@ -113,7 +104,7 @@ Qed. Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m. Proof. - intros n m; induction n; simpl in |- *; auto. + intros n m; induction n; simpl; auto. Qed. Hint Resolve plus_n_Sm: core. @@ -124,8 +115,8 @@ Qed. (** Standard associated names *) -Notation plus_0_r_reverse := plus_n_O (only parsing). -Notation plus_succ_r_reverse := plus_n_Sm (only parsing). +Notation plus_0_r_reverse := plus_n_O (compat "8.2"). +Notation plus_succ_r_reverse := plus_n_Sm (compat "8.2"). (** Multiplication *) @@ -141,22 +132,22 @@ Hint Resolve (f_equal2 mult): core. Lemma mult_n_O : forall n:nat, 0 = n * 0. Proof. - induction n; simpl in |- *; auto. + induction n; simpl; auto. Qed. Hint Resolve mult_n_O: core. Lemma mult_n_Sm : forall n m:nat, n * m + n = n * S m. Proof. - intros; induction n as [| p H]; simpl in |- *; auto. - destruct H; rewrite <- plus_n_Sm; apply (f_equal S). - pattern m at 1 3 in |- *; elim m; simpl in |- *; auto. + intros; induction n as [| p H]; simpl; auto. + destruct H; rewrite <- plus_n_Sm; apply eq_S. + pattern m at 1 3; elim m; simpl; auto. Qed. Hint Resolve mult_n_Sm: core. (** Standard associated names *) -Notation mult_0_r_reverse := mult_n_O (only parsing). -Notation mult_succ_r_reverse := mult_n_Sm (only parsing). +Notation mult_0_r_reverse := mult_n_O (compat "8.2"). +Notation mult_succ_r_reverse := mult_n_Sm (compat "8.2"). (** Truncated subtraction: [m-n] is [0] if [n>=m] *) @@ -201,6 +192,16 @@ 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. +Theorem le_pred : forall n m, n <= m -> pred n <= pred m. +Proof. +induction 1; auto. destruct m; simpl; auto. +Qed. + +Theorem le_S_n : forall n m, S n <= S m -> n <= m. +Proof. +intros n m. exact (le_pred (S n) (S m)). +Qed. + (** Case analysis *) Theorem nat_case : @@ -218,5 +219,78 @@ Theorem nat_double_ind : (forall n m:nat, R n m -> R (S n) (S m)) -> forall n m:nat, R n m. Proof. induction n; auto. - destruct m as [| n0]; auto. + destruct m; auto. +Qed. + +(** Maximum and minimum : definitions and specifications *) + +Fixpoint max n m : nat := + match n, m with + | O, _ => m + | S n', O => n + | S n', S m' => S (max n' m') + end. + +Fixpoint min n m : nat := + match n, m with + | O, _ => 0 + | S n', O => 0 + | S n', S m' => S (min n' m') + end. + +Theorem max_l : forall n m : nat, m <= n -> max n m = n. +Proof. +induction n; destruct m; simpl; auto. inversion 1. +intros. apply f_equal. apply IHn. apply le_S_n. trivial. +Qed. + +Theorem max_r : forall n m : nat, n <= m -> max n m = m. +Proof. +induction n; destruct m; simpl; auto. inversion 1. +intros. apply f_equal. apply IHn. apply le_S_n. trivial. +Qed. + +Theorem min_l : forall n m : nat, n <= m -> min n m = n. +Proof. +induction n; destruct m; simpl; auto. inversion 1. +intros. apply f_equal. apply IHn. apply le_S_n. trivial. +Qed. + +Theorem min_r : forall n m : nat, m <= n -> min n m = m. +Proof. +induction n; destruct m; simpl; auto. inversion 1. +intros. apply f_equal. apply IHn. apply le_S_n. trivial. +Qed. + +(** [n]th iteration of the function [f] *) + +Fixpoint nat_iter (n:nat) {A} (f:A->A) (x:A) : A := + match n with + | O => x + | S n' => f (nat_iter n' f x) + end. + +Lemma nat_iter_succ_r n {A} (f:A->A) (x:A) : + nat_iter (S n) f x = nat_iter n f (f x). +Proof. + induction n; intros; simpl; rewrite <- ?IHn; trivial. +Qed. + +Theorem nat_iter_plus : + forall (n m:nat) {A} (f:A -> A) (x:A), + nat_iter (n + m) f x = nat_iter n f (nat_iter m f x). +Proof. + induction n; intros; simpl; rewrite ?IHn; trivial. +Qed. + +(** Preservation of invariants : if [f : A->A] preserves the invariant [Inv], + then the iterates of [f] also preserve it. *) + +Theorem nat_iter_invariant : + forall (n:nat) {A} (f:A -> A) (P : A -> Prop), + (forall x, P x -> P (f x)) -> + forall x, P x -> P (nat_iter n f x). +Proof. + induction n; simpl; trivial. + intros A f P Hf x Hx. apply Hf, IHn; trivial. Qed. diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 5fcb2671..e723cadf 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Prelude.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Export Notations. Require Export Logic. Require Export Datatypes. @@ -18,9 +16,11 @@ Require Export Coq.Init.Tactics. (* Initially available plugins (+ nat_syntax_plugin loaded in Datatypes) *) Declare ML Module "extraction_plugin". +Declare ML Module "decl_mode_plugin". Declare ML Module "cc_plugin". Declare ML Module "ground_plugin". -Declare ML Module "dp_plugin". Declare ML Module "recdef_plugin". Declare ML Module "subtac_plugin". Declare ML Module "xml_plugin". +(* Default substrings not considered by queries like SearchAbout *) +Add Search Blacklist "_admitted" "_subproof" "Private_". diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 5a951d14..d1610f0a 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Specif.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** Basic specifications : sets that may contain logical information *) Set Implicit Arguments. @@ -40,10 +38,10 @@ Inductive sigT2 (A:Type) (P Q:A -> Type) : Type := (* Notations *) -Arguments Scope sig [type_scope type_scope]. -Arguments Scope sig2 [type_scope type_scope type_scope]. -Arguments Scope sigT [type_scope type_scope]. -Arguments Scope sigT2 [type_scope type_scope type_scope]. +Arguments sig (A P)%type. +Arguments sig2 (A P Q)%type. +Arguments sigT (A P)%type. +Arguments sigT2 (A P Q)%type. Notation "{ x | P }" := (sig (fun x => P)) : type_scope. Notation "{ x | P & Q }" := (sig2 (fun x => P) (fun x => Q)) : type_scope. @@ -62,7 +60,7 @@ Add Printing Let sigT2. (** Projections of [sig] - An element [y] of a subset [{x:A & (P x)}] is the pair of an [a] + 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)] *) @@ -128,6 +126,9 @@ Inductive sumbool (A B:Prop) : Set := Add Printing If sumbool. +Arguments left {A B} _, [A] B _. +Arguments right {A B} _ , A [B] _. + (** [sumor] is an option type equipped with the justification of why it may not be a regular value *) @@ -138,6 +139,9 @@ Inductive sumor (A:Type) (B:Prop) : Type := Add Printing If sumor. +Arguments inleft {A B} _ , [A] B _. +Arguments inright {A B} _ , A [B] _. + (** Various forms of the axiom of choice for specifications *) Section Choice_lemmas. @@ -152,16 +156,16 @@ Section Choice_lemmas. Proof. intro H. exists (fun z => proj1_sig (H z)). - intro z; destruct (H z); trivial. - Qed. + intro z; destruct (H z); assumption. + Defined. Lemma Choice2 : (forall x:S, {y:S' & R' x y}) -> {f:S -> S' & forall z:S, R' z (f z)}. Proof. intro H. exists (fun z => projT1 (H z)). - intro z; destruct (H z); trivial. - Qed. + intro z; destruct (H z); assumption. + Defined. Lemma bool_choice : (forall x:S, {R1 x} + {R2 x}) -> @@ -170,7 +174,7 @@ Section Choice_lemmas. intro H. exists (fun z:S => if H z then true else false). intro z; destruct (H z); auto. - Qed. + Defined. End Choice_lemmas. @@ -188,7 +192,7 @@ Section Dependent_choice_lemmas. exists f. split. reflexivity. induction n; simpl; apply proj2_sig. - Qed. + Defined. End Dependent_choice_lemmas. @@ -204,34 +208,34 @@ Definition Exc := option. Definition value := Some. Definition error := @None. -Implicit Arguments error [A]. +Arguments error [A]. Definition except := False_rec. (* for compatibility with previous versions *) -Implicit Arguments except [P]. +Arguments except [P] _. Theorem absurd_set : forall (A:Prop) (C:Set), A -> ~ A -> C. Proof. intros A C h1 h2. apply False_rec. apply (h2 h1). -Qed. +Defined. Hint Resolve left right inleft inright: core v62. Hint Resolve exist exist2 existT existT2: core. (* 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). +Notation sigS := sigT (compat "8.2"). +Notation existS := existT (compat "8.2"). +Notation sigS_rect := sigT_rect (compat "8.2"). +Notation sigS_rec := sigT_rec (compat "8.2"). +Notation sigS_ind := sigT_ind (compat "8.2"). +Notation projS1 := projT1 (compat "8.2"). +Notation projS2 := projT2 (compat "8.2"). + +Notation sigS2 := sigT2 (compat "8.2"). +Notation existS2 := existT2 (compat "8.2"). +Notation sigS2_rect := sigT2_rect (compat "8.2"). +Notation sigS2_rec := sigT2_rec (compat "8.2"). +Notation sigS2_ind := sigT2_ind (compat "8.2"). diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 1fa4a77f..23d9d10e 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Tactics.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Import Notations. Require Import Logic. Require Import Specif. @@ -77,18 +75,22 @@ Ltac false_hyp H G := (* A case with no loss of information. *) -Ltac case_eq x := generalize (refl_equal x); pattern x at -1; case x. +Ltac case_eq x := generalize (eq_refl x); pattern x at -1; case x. + +(* use either discriminate or injection on a hypothesis *) + +Ltac destr_eq H := discriminate H || (try (injection H; clear H; intro H)). (* Similar variants of destruct *) Tactic Notation "destruct_with_eqn" constr(x) := - destruct x as []_eqn. + destruct x eqn:?. Tactic Notation "destruct_with_eqn" ident(n) := - try intros until n; destruct n as []_eqn. + try intros until n; destruct n eqn:?. Tactic Notation "destruct_with_eqn" ":" ident(H) constr(x) := - destruct x as []_eqn:H. + destruct x eqn:H. Tactic Notation "destruct_with_eqn" ":" ident(H) ident(n) := - try intros until n; destruct n as []_eqn:H. + try intros until n; destruct n eqn:H. (** Break every hypothesis of a certain type *) @@ -187,6 +189,10 @@ Ltac easy := Tactic Notation "now" tactic(t) := t; easy. +(** Slightly more than [easy]*) + +Ltac easy' := repeat split; simpl; easy || now destruct 1. + (** A tactic to document or check what is proved at some point of a script *) Ltac now_show c := change c. diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index 5a5f672b..c9fcb570 100644 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Wf.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** * This module proves the validity of - well-founded recursion (also known as course of values) - well-founded induction @@ -105,7 +103,7 @@ Section Well_founded. Lemma Fix_eq : forall x:A, Fix x = F (fun (y:A) (p:R y x) => Fix y). Proof. - intro x; unfold Fix in |- *. + intro x; unfold Fix. rewrite <- Fix_F_eq. apply F_ext; intros. apply Fix_F_inv. |