diff options
Diffstat (limited to 'theories/Init')
| -rw-r--r-- | theories/Init/Datatypes.v | 25 | ||||
| -rw-r--r-- | theories/Init/Logic.v | 232 | ||||
| -rw-r--r-- | theories/Init/Logic_Type.v | 2 | ||||
| -rw-r--r-- | theories/Init/Nat.v | 297 | ||||
| -rw-r--r-- | theories/Init/Notations.v | 13 | ||||
| -rw-r--r-- | theories/Init/Peano.v | 139 | ||||
| -rw-r--r-- | theories/Init/Prelude.v | 6 | ||||
| -rw-r--r-- | theories/Init/Specif.v | 123 | ||||
| -rw-r--r-- | theories/Init/Tactics.v | 4 | ||||
| -rw-r--r-- | theories/Init/Wf.v | 22 | ||||
| -rw-r--r-- | theories/Init/vo.itarget | 1 |
11 files changed, 691 insertions, 173 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index e7e6ed9e..de615301 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -87,7 +87,7 @@ Hint Constructors eq_true : eq_true. Definition is_true b := b = true. (** [is_true] can be activated as a coercion by - (Local) Coercion is_true : bool >-> Prop. + ([Local]) [Coercion is_true : bool >-> Sortclass]. *) (** Additional rewriting lemmas about [eq_true] *) @@ -143,18 +143,20 @@ Arguments S _%nat. (********************************************************************) (** * Container datatypes *) +(* Set Universe Polymorphism. *) + (** [option A] is the extension of [A] with an extra element [None] *) Inductive option (A:Type) : Type := | Some : A -> option A | None : option A. -Arguments None [A]. +Arguments None {A}. -Definition option_map (A B:Type) (f:A->B) o := +Definition option_map (A B:Type) (f:A->B) (o : option A) : option B := match o with - | Some a => Some (f a) - | None => None + | Some a => @Some B (f a) + | None => @None B end. (** [sum A B], written [A + B], is the disjoint sum of [A] and [B] *) @@ -182,7 +184,8 @@ Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope. Arguments pair {A B} _ _. Section projections. - Variables A B : Type. + Context {A : Type} {B : Type}. + Definition fst (p:A * B) := match p with | (x, y) => x end. @@ -221,7 +224,7 @@ Inductive list (A : Type) : Type := | nil : list A | cons : A -> list A -> list A. -Arguments nil [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. @@ -244,8 +247,10 @@ Definition app (A : Type) : list A -> list A -> list A := | a :: l1 => a :: app l1 m end. + Infix "++" := app (right associativity, at level 60) : list_scope. +(* Unset Universe Polymorphism. *) (********************************************************************) (** * The comparison datatype *) @@ -310,6 +315,7 @@ Defined. 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. @@ -339,6 +345,9 @@ Arguments identity_rect [A] a P f y i. Definition ID := forall A:Type, A -> A. Definition id : ID := fun A x => x. +Definition IDProp := forall A:Prop, A -> A. +Definition idProp : IDProp := fun A x => x. + (* begin hide *) diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index e5f7a78b..d2971552 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,17 +8,23 @@ Set Implicit Arguments. -Require Import Notations. +Require Export Notations. + +Notation "A -> B" := (forall (_ : A), B) : type_scope. (** * Propositional connectives *) (** [True] is the always true proposition *) + Inductive True : Prop := I : True. (** [False] is the always false proposition *) Inductive False : Prop :=. +(** [proof_admitted] is used to implement the admit tactic *) +Axiom proof_admitted : False. + (** [not A], written [~A], is the negation of [A] *) Definition not (A:Prop) := A -> False. @@ -92,6 +98,36 @@ End Equivalence. Hint Unfold iff: extcore. +(** Backward direction of the equivalences above does not need assumptions *) + +Theorem and_iff_compat_l : forall A B C : Prop, + (B <-> C) -> (A /\ B <-> A /\ C). +Proof. + intros ? ? ? [Hl Hr]; split; intros [? ?]; (split; [ assumption | ]); + [apply Hl | apply Hr]; assumption. +Qed. + +Theorem and_iff_compat_r : forall A B C : Prop, + (B <-> C) -> (B /\ A <-> C /\ A). +Proof. + intros ? ? ? [Hl Hr]; split; intros [? ?]; (split; [ | assumption ]); + [apply Hl | apply Hr]; assumption. +Qed. + +Theorem or_iff_compat_l : forall A B C : Prop, + (B <-> C) -> (A \/ B <-> A \/ C). +Proof. + intros ? ? ? [Hl Hr]; split; (intros [?|?]; [left; assumption| right]); + [apply Hl | apply Hr]; assumption. +Qed. + +Theorem or_iff_compat_r : forall A B C : Prop, + (B <-> C) -> (B \/ A <-> C \/ A). +Proof. + intros ? ? ? [Hl Hr]; split; (intros [?|?]; [left| right; assumption]); + [apply Hl | apply Hr]; assumption. +Qed. + (** Some equivalences *) Theorem neg_false : forall A : Prop, ~ A <-> (A <-> False). @@ -104,73 +140,62 @@ Qed. Theorem and_cancel_l : forall A B C : Prop, (B -> A) -> (C -> A) -> ((A /\ B <-> A /\ C) <-> (B <-> C)). Proof. - intros; tauto. + intros A B C Hl Hr. + split; [ | apply and_iff_compat_l]; intros [HypL HypR]; split; intros. + + apply HypL; split; [apply Hl | ]; assumption. + + apply HypR; split; [apply Hr | ]; assumption. Qed. Theorem and_cancel_r : forall A B C : Prop, (B -> A) -> (C -> A) -> ((B /\ A <-> C /\ A) <-> (B <-> C)). Proof. - intros; tauto. + intros A B C Hl Hr. + split; [ | apply and_iff_compat_r]; intros [HypL HypR]; split; intros. + + apply HypL; split; [ | apply Hl ]; assumption. + + apply HypR; split; [ | apply Hr ]; assumption. Qed. Theorem and_comm : forall A B : Prop, A /\ B <-> B /\ A. Proof. - intros; tauto. + intros; split; intros [? ?]; split; assumption. Qed. Theorem and_assoc : forall A B C : Prop, (A /\ B) /\ C <-> A /\ B /\ C. Proof. - intros; tauto. + intros; split; [ intros [[? ?] ?]| intros [? [? ?]]]; repeat split; assumption. Qed. Theorem or_cancel_l : forall A B C : Prop, (B -> ~ A) -> (C -> ~ A) -> ((A \/ B <-> A \/ C) <-> (B <-> C)). Proof. - intros; tauto. + intros ? ? ? Fl Fr; split; [ | apply or_iff_compat_l]; intros [Hl Hr]; split; intros. + { destruct Hl; [ right | destruct Fl | ]; assumption. } + { destruct Hr; [ right | destruct Fr | ]; assumption. } Qed. Theorem or_cancel_r : forall A B C : Prop, (B -> ~ A) -> (C -> ~ A) -> ((B \/ A <-> C \/ A) <-> (B <-> C)). Proof. - intros; tauto. + intros ? ? ? Fl Fr; split; [ | apply or_iff_compat_r]; intros [Hl Hr]; split; intros. + { destruct Hl; [ left | | destruct Fl ]; assumption. } + { destruct Hr; [ left | | destruct Fr ]; assumption. } Qed. Theorem or_comm : forall A B : Prop, (A \/ B) <-> (B \/ A). Proof. - intros; tauto. + intros; split; (intros [? | ?]; [ right | left ]; assumption). Qed. Theorem or_assoc : forall A B C : Prop, (A \/ B) \/ C <-> A \/ B \/ C. Proof. - intros; tauto. -Qed. - -(** Backward direction of the equivalences above does not need assumptions *) - -Theorem and_iff_compat_l : forall A B C : Prop, - (B <-> C) -> (A /\ B <-> A /\ C). -Proof. - intros; tauto. -Qed. - -Theorem and_iff_compat_r : forall A B C : Prop, - (B <-> C) -> (B /\ A <-> C /\ A). -Proof. - intros; tauto. -Qed. - -Theorem or_iff_compat_l : forall A B C : Prop, - (B <-> C) -> (A \/ B <-> A \/ C). -Proof. - intros; tauto. -Qed. - -Theorem or_iff_compat_r : forall A B C : Prop, - (B <-> C) -> (B \/ A <-> C \/ A). -Proof. - intros; tauto. + intros; split; [ intros [[?|?]|?]| intros [?|[?|?]]]. + + left; assumption. + + right; left; assumption. + + right; right; assumption. + + left; left; assumption. + + left; right; assumption. + + right; assumption. Qed. - Lemma iff_and : forall A B : Prop, (A <-> B) -> (A -> B) /\ (B -> A). Proof. intros A B []; split; trivial. @@ -178,7 +203,7 @@ Qed. Lemma iff_to_and : forall A B : Prop, (A <-> B) <-> (A -> B) /\ (B -> A). Proof. - intros; tauto. + intros; split; intros [Hl Hr]; (split; intros; [ apply Hl | apply Hr]); assumption. Qed. (** [(IF_then_else P Q R)], written [IF P then Q else R] denotes @@ -204,11 +229,6 @@ 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, - 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. @@ -277,7 +297,8 @@ 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 I conj or_introl or_intror : core. +Hint Resolve eq_refl: core. Hint Resolve ex_intro ex_intro2: core. Section Logic_lemmas. @@ -297,19 +318,16 @@ Section Logic_lemmas. Proof. destruct 1; trivial. Defined. - Opaque eq_sym. Theorem eq_trans : x = y -> y = z -> x = z. Proof. destruct 2; trivial. Defined. - Opaque eq_trans. Theorem f_equal : x = y -> f x = f y. Proof. destruct 1; trivial. Defined. - Opaque f_equal. Theorem not_eq_sym : x <> y -> y <> x. Proof. @@ -320,7 +338,7 @@ 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 eq_sym with (1 := H0); assumption. + intros A x P H y H0. elim eq_sym with (1 := H0); assumption. Defined. Definition eq_rec_r : @@ -336,13 +354,40 @@ End Logic_lemmas. Module EqNotations. Notation "'rew' H 'in' H'" := (eq_rect _ _ H' _ H) - (at level 10, H' at level 10). + (at level 10, H' at level 10, + format "'[' 'rew' H in '/' H' ']'"). + Notation "'rew' [ P ] H 'in' H'" := (eq_rect _ P H' _ H) + (at level 10, H' at level 10, + format "'[' 'rew' [ P ] '/ ' H in '/' H' ']'"). Notation "'rew' <- H 'in' H'" := (eq_rect_r _ H' H) - (at level 10, H' at level 10). + (at level 10, H' at level 10, + format "'[' 'rew' <- H in '/' H' ']'"). + Notation "'rew' <- [ P ] H 'in' H'" := (eq_rect_r P H' H) + (at level 10, H' at level 10, + format "'[' 'rew' <- [ P ] '/ ' H in '/' H' ']'"). Notation "'rew' -> H 'in' H'" := (eq_rect _ _ H' _ H) (at level 10, H' at level 10, only parsing). + Notation "'rew' -> [ P ] H 'in' H'" := (eq_rect _ P H' _ H) + (at level 10, H' at level 10, only parsing). + End EqNotations. +Import EqNotations. + +Lemma rew_opp_r : forall A (P:A->Type) (x y:A) (H:x=y) (a:P y), rew H in rew <- H in a = a. +Proof. +intros. +destruct H. +reflexivity. +Defined. + +Lemma rew_opp_l : forall A (P:A->Type) (x y:A) (H:x=y) (a:P x), rew <- H in rew H in a = a. +Proof. +intros. +destruct H. +reflexivity. +Defined. + 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. @@ -376,6 +421,91 @@ Proof. destruct 1; destruct 1; destruct 1; destruct 1; destruct 1; reflexivity. Qed. +Theorem f_equal_compose : forall A B C (a b:A) (f:A->B) (g:B->C) (e:a=b), + f_equal g (f_equal f e) = f_equal (fun a => g (f a)) e. +Proof. + destruct e. reflexivity. +Defined. + +(** The goupoid structure of equality *) + +Theorem eq_trans_refl_l : forall A (x y:A) (e:x=y), eq_trans eq_refl e = e. +Proof. + destruct e. reflexivity. +Defined. + +Theorem eq_trans_refl_r : forall A (x y:A) (e:x=y), eq_trans e eq_refl = e. +Proof. + destruct e. reflexivity. +Defined. + +Theorem eq_sym_involutive : forall A (x y:A) (e:x=y), eq_sym (eq_sym e) = e. +Proof. + destruct e; reflexivity. +Defined. + +Theorem eq_trans_sym_inv_l : forall A (x y:A) (e:x=y), eq_trans (eq_sym e) e = eq_refl. +Proof. + destruct e; reflexivity. +Defined. + +Theorem eq_trans_sym_inv_r : forall A (x y:A) (e:x=y), eq_trans e (eq_sym e) = eq_refl. +Proof. + destruct e; reflexivity. +Defined. + +Theorem eq_trans_assoc : forall A (x y z t:A) (e:x=y) (e':y=z) (e'':z=t), + eq_trans e (eq_trans e' e'') = eq_trans (eq_trans e e') e''. +Proof. + destruct e''; reflexivity. +Defined. + +(** Extra properties of equality *) + +Theorem eq_id_comm_l : forall A (f:A->A) (Hf:forall a, a = f a), forall a, f_equal f (Hf a) = Hf (f a). +Proof. + intros. + unfold f_equal. + rewrite <- (eq_trans_sym_inv_l (Hf a)). + destruct (Hf a) at 1 2. + destruct (Hf a). + reflexivity. +Defined. + +Theorem eq_id_comm_r : forall A (f:A->A) (Hf:forall a, f a = a), forall a, f_equal f (Hf a) = Hf (f a). +Proof. + intros. + unfold f_equal. + rewrite <- (eq_trans_sym_inv_l (Hf (f (f a)))). + set (Hfsymf := fun a => eq_sym (Hf a)). + change (eq_sym (Hf (f (f a)))) with (Hfsymf (f (f a))). + pattern (Hfsymf (f (f a))). + destruct (eq_id_comm_l f Hfsymf (f a)). + destruct (eq_id_comm_l f Hfsymf a). + unfold Hfsymf. + destruct (Hf a). simpl. + rewrite eq_trans_refl_l. + reflexivity. +Defined. + +Lemma eq_trans_map_distr : forall A B x y z (f:A->B) (e:x=y) (e':y=z), f_equal f (eq_trans e e') = eq_trans (f_equal f e) (f_equal f e'). +Proof. +destruct e'. +reflexivity. +Defined. + +Lemma eq_sym_map_distr : forall A B (x y:A) (f:A->B) (e:x=y), eq_sym (f_equal f e) = f_equal f (eq_sym e). +Proof. +destruct e. +reflexivity. +Defined. + +Lemma eq_trans_sym_distr : forall A (x y z:A) (e:x=y) (e':y=z), eq_sym (eq_trans e e') = eq_trans (eq_sym e') (eq_sym e). +Proof. +destruct e, e'. +reflexivity. +Defined. + (* Aliases *) Notation sym_eq := eq_sym (compat "8.3"). @@ -474,7 +604,7 @@ Declare Right Step eq_trans. Lemma iff_stepl : forall A B C : Prop, (A <-> B) -> (A <-> C) -> (C <-> B). Proof. - intros; tauto. + intros ? ? ? [? ?] [? ?]; split; intros; auto. Qed. Declare Left Step iff_stepl. diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v index b2f83e03..1e126463 100644 --- a/theories/Init/Logic_Type.v +++ b/theories/Init/Logic_Type.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v new file mode 100644 index 00000000..afb46436 --- /dev/null +++ b/theories/Init/Nat.v @@ -0,0 +1,297 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import Notations Logic Datatypes. + +Local Open Scope nat_scope. + +(**********************************************************************) +(** * Peano natural numbers, definitions of operations *) +(**********************************************************************) + +(** This file is meant to be used as a whole module, + without importing it, leading to qualified definitions + (e.g. Nat.pred) *) + +Definition t := nat. + +(** ** Constants *) + +Definition zero := 0. +Definition one := 1. +Definition two := 2. + +(** ** Basic operations *) + +Definition succ := S. + +Definition pred n := + match n with + | 0 => n + | S u => u + end. + +Fixpoint add n m := + match n with + | 0 => m + | S p => S (p + m) + end + +where "n + m" := (add n m) : nat_scope. + +Definition double n := n + n. + +Fixpoint mul n m := + match n with + | 0 => 0 + | S p => m + p * m + end + +where "n * m" := (mul n m) : nat_scope. + +(** Truncated subtraction: [n-m] is [0] if [n<=m] *) + +Fixpoint sub n m := + match n, m with + | S k, S l => k - l + | _, _ => n + end + +where "n - m" := (sub n m) : nat_scope. + +(** ** Comparisons *) + +Fixpoint eqb n m : bool := + match n, m with + | 0, 0 => true + | 0, S _ => false + | S _, 0 => false + | S n', S m' => eqb n' m' + end. + +Fixpoint leb n m : bool := + match n, m with + | 0, _ => true + | _, 0 => false + | S n', S m' => leb n' m' + end. + +Definition ltb n m := leb (S n) m. + +Infix "=?" := eqb (at level 70) : nat_scope. +Infix "<=?" := leb (at level 70) : nat_scope. +Infix "<?" := ltb (at level 70) : nat_scope. + +Fixpoint compare n m : comparison := + match n, m with + | 0, 0 => Eq + | 0, S _ => Lt + | S _, 0 => Gt + | S n', S m' => compare n' m' + end. + +Infix "?=" := compare (at level 70) : nat_scope. + +(** ** Minimum, maximum *) + +Fixpoint max n m := + match n, m with + | 0, _ => m + | S n', 0 => n + | S n', S m' => S (max n' m') + end. + +Fixpoint min n m := + match n, m with + | 0, _ => 0 + | S n', 0 => 0 + | S n', S m' => S (min n' m') + end. + +(** ** Parity tests *) + +Fixpoint even n : bool := + match n with + | 0 => true + | 1 => false + | S (S n') => even n' + end. + +Definition odd n := negb (even n). + +(** ** Power *) + +Fixpoint pow n m := + match m with + | 0 => 1 + | S m => n * (n^m) + end + +where "n ^ m" := (pow n m) : nat_scope. + +(** ** Euclidean division *) + +(** This division is linear and tail-recursive. + In [divmod], [y] is the predecessor of the actual divisor, + and [u] is [y] minus the real remainder +*) + +Fixpoint divmod x y q u := + match x with + | 0 => (q,u) + | S x' => match u with + | 0 => divmod x' y (S q) y + | S u' => divmod x' y q u' + end + end. + +Definition div x y := + match y with + | 0 => y + | S y' => fst (divmod x y' 0 y') + end. + +Definition modulo x y := + match y with + | 0 => y + | S y' => y' - snd (divmod x y' 0 y') + end. + +Infix "/" := div : nat_scope. +Infix "mod" := modulo (at level 40, no associativity) : nat_scope. + + +(** ** Greatest common divisor *) + +(** We use Euclid algorithm, which is normally not structural, + but Coq is now clever enough to accept this (behind modulo + there is a subtraction, which now preserves being a subterm) +*) + +Fixpoint gcd a b := + match a with + | O => b + | S a' => gcd (b mod (S a')) (S a') + end. + +(** ** Square *) + +Definition square n := n * n. + +(** ** Square root *) + +(** The following square root function is linear (and tail-recursive). + With Peano representation, we can't do better. For faster algorithm, + see Psqrt/Zsqrt/Nsqrt... + + We search the square root of n = k + p^2 + (q - r) + with q = 2p and 0<=r<=q. We start with p=q=r=0, hence + looking for the square root of n = k. Then we progressively + decrease k and r. When k = S k' and r=0, it means we can use (S p) + as new sqrt candidate, since (S k')+p^2+2p = k'+(S p)^2. + When k reaches 0, we have found the biggest p^2 square contained + in n, hence the square root of n is p. +*) + +Fixpoint sqrt_iter k p q r := + match k with + | O => p + | S k' => match r with + | O => sqrt_iter k' (S p) (S (S q)) (S (S q)) + | S r' => sqrt_iter k' p q r' + end + end. + +Definition sqrt n := sqrt_iter n 0 0 0. + +(** ** Log2 *) + +(** This base-2 logarithm is linear and tail-recursive. + + In [log2_iter], we maintain the logarithm [p] of the counter [q], + while [r] is the distance between [q] and the next power of 2, + more precisely [q + S r = 2^(S p)] and [r<2^p]. At each + recursive call, [q] goes up while [r] goes down. When [r] + is 0, we know that [q] has almost reached a power of 2, + and we increase [p] at the next call, while resetting [r] + to [q]. + + Graphically (numbers are [q], stars are [r]) : + +<< + 10 + 9 + 8 + 7 * + 6 * + 5 ... + 4 + 3 * + 2 * + 1 * * +0 * * * +>> + + We stop when [k], the global downward counter reaches 0. + At that moment, [q] is the number we're considering (since + [k+q] is invariant), and [p] its logarithm. +*) + +Fixpoint log2_iter k p q r := + match k with + | O => p + | S k' => match r with + | O => log2_iter k' (S p) (S q) q + | S r' => log2_iter k' p (S q) r' + end + end. + +Definition log2 n := log2_iter (pred n) 0 1 0. + +(** Iterator on natural numbers *) + +Definition iter (n:nat) {A} (f:A->A) (x:A) : A := + nat_rect (fun _ => A) x (fun _ => f) n. + +(** Bitwise operations *) + +(** We provide here some bitwise operations for unary numbers. + Some might be really naive, they are just there for fullfiling + the same interface as other for natural representations. As + soon as binary representations such as NArith are available, + it is clearly better to convert to/from them and use their ops. +*) + +Fixpoint div2 n := + match n with + | 0 => 0 + | S 0 => 0 + | S (S n') => S (div2 n') + end. + +Fixpoint testbit a n : bool := + match n with + | 0 => odd a + | S n => testbit (div2 a) n + end. + +Definition shiftl a := nat_rect _ a (fun _ => double). +Definition shiftr a := nat_rect _ a (fun _ => div2). + +Fixpoint bitwise (op:bool->bool->bool) n a b := + match n with + | 0 => 0 + | S n' => + (if op (odd a) (odd b) then 1 else 0) + + 2*(bitwise op n' (div2 a) (div2 b)) + end. + +Definition land a b := bitwise andb a a b. +Definition lor a b := bitwise orb (max a b) a b. +Definition ldiff a b := bitwise (fun b b' => andb b (negb b')) a a b. +Definition lxor a b := bitwise xorb (max a b) a b. diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index c745f9c9..424ca0c8 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -10,6 +10,7 @@ (** Notations for propositional connectives *) +Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). 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). @@ -79,3 +80,13 @@ Delimit Scope core_scope with core. Open Scope core_scope. Open Scope type_scope. + +(** ML Tactic Notations *) + +Declare ML Module "coretactics". +Declare ML Module "extratactics". +Declare ML Module "eauto". +Declare ML Module "g_class". +Declare ML Module "g_eqdecide". +Declare ML Module "g_rewrite". +Declare ML Module "tauto". diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index ef2d9584..7a14ab39 100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -26,21 +26,22 @@ Require Import Notations. Require Import Datatypes. Require Import Logic. +Require Coq.Init.Nat. Open Scope nat_scope. Definition eq_S := f_equal S. +Definition f_equal_nat := f_equal (A:=nat). -Hint Resolve (f_equal S): v62. -Hint Resolve (f_equal (A:=nat)): core. +Hint Resolve eq_S: v62. +Hint Resolve f_equal_nat: core. (** The predecessor function *) -Definition pred (n:nat) : nat := match n with - | O => n - | S u => u - end. -Hint Resolve (f_equal pred): v62. +Notation pred := Nat.pred (compat "8.4"). + +Definition f_equal_pred := f_equal pred. +Hint Resolve f_equal_pred: v62. Theorem pred_Sn : forall n:nat, n = pred (S n). Proof. @@ -80,16 +81,13 @@ Hint Resolve n_Sn: core. (** Addition *) -Fixpoint plus (n m:nat) : nat := - match n with - | O => m - | S p => S (p + m) - end - -where "n + m" := (plus n m) : nat_scope. +Notation plus := Nat.add (compat "8.4"). +Infix "+" := Nat.add : nat_scope. -Hint Resolve (f_equal2 plus): v62. -Hint Resolve (f_equal2 (A1:=nat) (A2:=nat)): core. +Definition f_equal2_plus := f_equal2 plus. +Hint Resolve f_equal2_plus: v62. +Definition f_equal2_nat := f_equal2 (A1:=nat) (A2:=nat). +Hint Resolve f_equal2_nat: core. Lemma plus_n_O : forall n:nat, n = n + 0. Proof. @@ -99,7 +97,7 @@ Hint Resolve plus_n_O: core. Lemma plus_O_n : forall n:nat, 0 + n = n. Proof. - auto. + reflexivity. Qed. Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m. @@ -110,7 +108,7 @@ Hint Resolve plus_n_Sm: core. Lemma plus_Sn_m : forall n m:nat, S n + m = S (n + m). Proof. - auto. + reflexivity. Qed. (** Standard associated names *) @@ -120,15 +118,11 @@ Notation plus_succ_r_reverse := plus_n_Sm (compat "8.2"). (** Multiplication *) -Fixpoint mult (n m:nat) : nat := - match n with - | O => 0 - | S p => m + p * m - end - -where "n * m" := (mult n m) : nat_scope. +Notation mult := Nat.mul (compat "8.4"). +Infix "*" := Nat.mul : nat_scope. -Hint Resolve (f_equal2 mult): core. +Definition f_equal2_mult := f_equal2 mult. +Hint Resolve f_equal2_mult: core. Lemma mult_n_O : forall n:nat, 0 = n * 0. Proof. @@ -151,14 +145,8 @@ Notation mult_succ_r_reverse := mult_n_Sm (compat "8.2"). (** Truncated subtraction: [m-n] is [0] if [n>=m] *) -Fixpoint minus (n m:nat) : nat := - match n, m with - | O, _ => n - | S k, O => n - | S k, S l => k - l - end - -where "n - m" := (minus n m) : nat_scope. +Notation minus := Nat.sub (compat "8.4"). +Infix "-" := Nat.sub : nat_scope. (** Definition of the usual orders, the basic properties of [le] and [lt] can be found in files Le and Lt *) @@ -202,6 +190,16 @@ Proof. intros n m. exact (le_pred (S n) (S m)). Qed. +Theorem le_0_n : forall n, 0 <= n. +Proof. + induction n; constructor; trivial. +Qed. + +Theorem le_n_S : forall n m, n <= m -> S n <= S m. +Proof. + induction 1; constructor; trivial. +Qed. + (** Case analysis *) Theorem nat_case : @@ -224,73 +222,48 @@ 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. +Notation max := Nat.max (compat "8.4"). +Notation min := Nat.min (compat "8.4"). -Theorem max_l : forall n m : nat, m <= n -> max n m = n. +Lemma max_l n m : m <= n -> Nat.max n m = n. Proof. -induction n; destruct m; simpl; auto. inversion 1. -intros. apply f_equal. apply IHn. apply le_S_n. trivial. + revert m; induction n; destruct m; simpl; trivial. + - inversion 1. + - intros. apply f_equal, IHn, le_S_n; trivial. Qed. -Theorem max_r : forall n m : nat, n <= m -> max n m = m. +Lemma max_r n m : n <= m -> Nat.max n m = m. Proof. -induction n; destruct m; simpl; auto. inversion 1. -intros. apply f_equal. apply IHn. apply le_S_n. trivial. + revert m; induction n; destruct m; simpl; trivial. + - inversion 1. + - intros. apply f_equal, IHn, le_S_n; trivial. Qed. -Theorem min_l : forall n m : nat, n <= m -> min n m = n. +Lemma min_l n m : n <= m -> Nat.min n m = n. Proof. -induction n; destruct m; simpl; auto. inversion 1. -intros. apply f_equal. apply IHn. apply le_S_n. trivial. + revert m; induction n; destruct m; simpl; trivial. + - inversion 1. + - intros. apply f_equal, IHn, le_S_n; trivial. Qed. -Theorem min_r : forall n m : nat, m <= n -> min n m = m. +Lemma min_r n m : m <= n -> Nat.min n m = m. Proof. -induction n; destruct m; simpl; auto. inversion 1. -intros. apply f_equal. apply IHn. apply le_S_n. trivial. + revert m; induction n; destruct m; simpl; trivial. + - inversion 1. + - intros. apply f_equal, IHn, 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). +Lemma nat_rect_succ_r {A} (f: A -> A) (x:A) n : + nat_rect (fun _ => A) x (fun _ => f) (S n) = nat_rect (fun _ => A) (f x) (fun _ => f) n. Proof. induction n; intros; simpl; rewrite <- ?IHn; trivial. Qed. -Theorem nat_iter_plus : +Theorem nat_rect_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). + nat_rect (fun _ => A) x (fun _ => f) (n + m) = + nat_rect (fun _ => A) (nat_rect (fun _ => A) x (fun _ => f) m) (fun _ => f) n. 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 2614ce40..4894eba4 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,8 +8,10 @@ Require Export Notations. Require Export Logic. +Require Export Logic_Type. Require Export Datatypes. Require Export Specif. +Require Coq.Init.Nat. Require Export Peano. Require Export Coq.Init.Wf. Require Export Coq.Init.Tactics. @@ -20,7 +22,5 @@ Declare ML Module "decl_mode_plugin". Declare ML Module "cc_plugin". Declare ML Module "ground_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 cc5a1932..1384901b 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -45,11 +45,11 @@ 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. -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)) : +Notation "{ x : A | P }" := (sig (A:=A) (fun x => P)) : type_scope. +Notation "{ x : A | P & Q }" := (sig2 (A:=A) (fun x => P) (fun x => Q)) : type_scope. -Notation "{ x : A & P }" := (sigT (fun x:A => P)) : type_scope. -Notation "{ x : A & P & Q }" := (sigT2 (fun x:A => P) (fun x:A => Q)) : +Notation "{ x : A & P }" := (sigT (A:=A) (fun x => P)) : type_scope. +Notation "{ x : A & P & Q }" := (sigT2 (A:=A) (fun x => P) (fun x => Q)) : type_scope. Add Printing Let sig. @@ -65,24 +65,57 @@ Add Printing Let sigT2. [(proj1_sig y)] is the witness [a] and [(proj2_sig y)] is the proof of [(P a)] *) - +(* Set Universe Polymorphism. *) Section Subset_projections. Variable A : Type. Variable P : A -> Prop. Definition proj1_sig (e:sig P) := match e with - | exist a b => a + | exist _ a b => a end. Definition proj2_sig (e:sig P) := match e return P (proj1_sig e) with - | exist a b => b + | exist _ a b => b end. End Subset_projections. +(** [sig2] of a predicate can be projected to a [sig]. + + This allows [proj1_sig] and [proj2_sig] to be usable with [sig2]. + + The [let] statements occur in the body of the [exist] so that + [proj1_sig] of a coerced [X : sig2 P Q] will unify with [let (a, + _, _) := X in a] *) + +Definition sig_of_sig2 (A : Type) (P Q : A -> Prop) (X : sig2 P Q) : sig P + := exist P + (let (a, _, _) := X in a) + (let (x, p, _) as s return (P (let (a, _, _) := s in a)) := X in p). + +(** Projections of [sig2] + + An element [y] of a subset [{x:A | (P x) & (Q x)}] is the triple + of an [a] of type [A], a of a proof [h] that [a] satisfies [P], + and a proof [h'] that [a] satisfies [Q]. Then + [(proj1_sig (sig_of_sig2 y))] is the witness [a], + [(proj2_sig (sig_of_sig2 y))] is the proof of [(P a)], and + [(proj3_sig y)] is the proof of [(Q a)]. *) + +Section Subset_projections2. + + Variable A : Type. + Variables P Q : A -> Prop. + + Definition proj3_sig (e : sig2 P Q) := + let (a, b, c) return Q (proj1_sig (sig_of_sig2 e)) := e in c. + +End Subset_projections2. + + (** Projections of [sigT] An element [x] of a sigma-type [{y:A & P y}] is a dependent pair @@ -90,31 +123,71 @@ End Subset_projections. [(projT1 x)] is the first projection and [(projT2 x)] is the second projection, the type of which depends on the [projT1]. *) + + Section Projections. Variable A : Type. Variable P : A -> Type. Definition projT1 (x:sigT P) : A := match x with - | existT a _ => a + | existT _ a _ => a end. + Definition projT2 (x:sigT P) : P (projT1 x) := match x return P (projT1 x) with - | existT _ h => h + | existT _ _ h => h end. End Projections. +(** [sigT2] of a predicate can be projected to a [sigT]. + + This allows [projT1] and [projT2] to be usable with [sigT2]. + + The [let] statements occur in the body of the [existT] so that + [projT1] of a coerced [X : sigT2 P Q] will unify with [let (a, + _, _) := X in a] *) + +Definition sigT_of_sigT2 (A : Type) (P Q : A -> Type) (X : sigT2 P Q) : sigT P + := existT P + (let (a, _, _) := X in a) + (let (x, p, _) as s return (P (let (a, _, _) := s in a)) := X in p). + +(** Projections of [sigT2] + + An element [x] of a sigma-type [{y:A & P y & Q y}] is a dependent + pair made of an [a] of type [A], an [h] of type [P a], and an [h'] + of type [Q a]. Then, [(projT1 (sigT_of_sigT2 x))] is the first + projection, [(projT2 (sigT_of_sigT2 x))] is the second projection, + and [(projT3 x)] is the third projection, the types of which + depends on the [projT1]. *) + +Section Projections2. + + Variable A : Type. + Variables P Q : A -> Type. + + Definition projT3 (e : sigT2 P Q) := + let (a, b, c) return Q (projT1 (sigT_of_sigT2 e)) := e in c. + +End Projections2. + (** [sigT] of a predicate is equivalent to [sig] *) -Lemma sig_of_sigT : forall (A:Type) (P:A->Prop), sigT P -> sig P. -Proof. destruct 1 as (x,H); exists x; trivial. Defined. +Definition sig_of_sigT (A : Type) (P : A -> Prop) (X : sigT P) : sig P + := exist P (projT1 X) (projT2 X). + +Definition sigT_of_sig (A : Type) (P : A -> Prop) (X : sig P) : sigT P + := existT P (proj1_sig X) (proj2_sig X). -Lemma sigT_of_sig : forall (A:Type) (P:A->Prop), sig P -> sigT P. -Proof. destruct 1 as (x,H); exists x; trivial. Defined. +(** [sigT2] of a predicate is equivalent to [sig2] *) -Coercion sigT_of_sig : sig >-> sigT. -Coercion sig_of_sigT : sigT >-> sig. +Definition sig2_of_sigT2 (A : Type) (P Q : A -> Prop) (X : sigT2 P Q) : sig2 P Q + := exist2 P Q (projT1 (sigT_of_sigT2 X)) (projT2 (sigT_of_sigT2 X)) (projT3 X). + +Definition sigT2_of_sig2 (A : Type) (P Q : A -> Prop) (X : sig2 P Q) : sigT2 P Q + := existT2 P Q (proj1_sig (sig_of_sig2 X)) (proj2_sig (sig_of_sig2 X)) (proj3_sig X). (** [sumbool] is a boolean type equipped with the justification of their value *) @@ -142,6 +215,8 @@ Add Printing If sumor. Arguments inleft {A B} _ , [A] B _. Arguments inright {A B} _ , A [B] _. +(* Unset Universe Polymorphism. *) + (** Various forms of the axiom of choice for specifications *) Section Choice_lemmas. @@ -187,10 +262,10 @@ Section Dependent_choice_lemmas. (forall x:X, {y | R x y}) -> forall x0, {f : nat -> X | f O = x0 /\ forall n, R (f n) (f (S n))}. Proof. - intros H x0. + intros H x0. set (f:=fix f n := match n with O => x0 | S n' => proj1_sig (H (f n')) end). exists f. - split. reflexivity. + split. reflexivity. induction n; simpl; apply proj2_sig. Defined. @@ -203,12 +278,14 @@ End Dependent_choice_lemmas. [Inductive Exc [A:Type] : Type := value : A->(Exc A) | error : (Exc A)]. It is implemented using the option type. *) +Section Exc. + Variable A : Type. -Definition Exc := option. -Definition value := Some. -Definition error := @None. - -Arguments error [A]. + Definition Exc := option A. + Definition value := @Some A. + Definition error := @None A. +End Exc. +Arguments error {A}. Definition except := False_rec. (* for compatibility with previous versions *) diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 4a7b9283..9e828e6e 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -68,7 +68,7 @@ Ltac absurd_hyp H := let T := type of H in absurd T. -(* A useful complement to contradict. Here H:A while G allows to conclude ~A *) +(* A useful complement to contradict. Here H:A while G allows concluding ~A *) Ltac false_hyp H G := let T := type of H in absurd T; [ apply G | assumption ]. diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index 9db64787..6501b1e1 100644 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -150,3 +150,23 @@ End Well_founded_2. Notation Acc_iter := Fix_F (only parsing). (* compatibility *) Notation Acc_iter_2 := Fix_F_2 (only parsing). (* compatibility *) + + + +(* Added by Julien Forest on 13/11/20 *) +Section Acc_generator. + Variable A : Type. + Variable R : A -> A -> Prop. + + (* *Lazily* add 2^n - 1 Acc_intro on top of wf. + Needed for fast reductions using Function and Program Fixpoint + and probably using Fix and Fix_F_2 + *) + Fixpoint Acc_intro_generator n (wf : well_founded R) := + match n with + | O => wf + | S n => fun x => Acc_intro x (fun y _ => Acc_intro_generator n (Acc_intro_generator n wf) y) + end. + + +End Acc_generator. diff --git a/theories/Init/vo.itarget b/theories/Init/vo.itarget index f53d55e7..cc62e66c 100644 --- a/theories/Init/vo.itarget +++ b/theories/Init/vo.itarget @@ -7,3 +7,4 @@ Prelude.vo Specif.vo Tactics.vo Wf.vo +Nat.vo
\ No newline at end of file |