summaryrefslogtreecommitdiff
path: root/theories/Init
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Init')
-rw-r--r--theories/Init/Datatypes.v38
-rw-r--r--theories/Init/Decimal.v163
-rw-r--r--theories/Init/Logic.v188
-rw-r--r--theories/Init/Logic_Type.v18
-rw-r--r--theories/Init/Nat.v68
-rw-r--r--theories/Init/Notations.v50
-rw-r--r--theories/Init/Peano.v34
-rw-r--r--theories/Init/Prelude.v16
-rw-r--r--theories/Init/Specif.v481
-rw-r--r--theories/Init/Tactics.v100
-rw-r--r--theories/Init/Tauto.v4
-rw-r--r--theories/Init/Wf.v10
-rw-r--r--theories/Init/_CoqProject2
-rw-r--r--theories/Init/vo.itarget11
14 files changed, 1059 insertions, 124 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index ddaf08bf..05b741f0 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
Set Implicit Arguments.
@@ -65,7 +67,7 @@ Infix "&&" := andb : bool_scope.
Lemma andb_prop : forall a b:bool, andb a b = true -> a = true /\ b = true.
Proof.
- destruct a; destruct b; intros; split; try (reflexivity || discriminate).
+ destruct a, b; repeat split; assumption.
Qed.
Hint Resolve andb_prop: bool.
@@ -262,6 +264,11 @@ Inductive comparison : Set :=
| Lt : comparison
| Gt : comparison.
+Lemma comparison_eq_stable : forall c c' : comparison, ~~ c = c' -> c = c'.
+Proof.
+ destruct c, c'; intro H; reflexivity || destruct H; discriminate.
+Qed.
+
Definition CompOpp (r:comparison) :=
match r with
| Eq => Eq
@@ -326,13 +333,12 @@ 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.
-
(******************************************************************)
(** * Misc Other Datatypes *)
(** [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] *)
+ sole inhabitant is denoted [identity_refl A a] *)
Inductive identity (A:Type) (a:A) : A -> Type :=
identity_refl : identity a a.
@@ -355,14 +361,14 @@ Definition idProp : IDProp := fun A x => x.
(* Compatibility *)
-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").
+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).
(* end hide *)
diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v
new file mode 100644
index 00000000..57163b1b
--- /dev/null
+++ b/theories/Init/Decimal.v
@@ -0,0 +1,163 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(** * Decimal numbers *)
+
+(** These numbers coded in base 10 will be used for parsing and printing
+ other Coq numeral datatypes in an human-readable way.
+ See the [Numeral Notation] command.
+ We represent numbers in base 10 as lists of decimal digits,
+ in big-endian order (most significant digit comes first). *)
+
+(** Unsigned integers are just lists of digits.
+ For instance, ten is (D1 (D0 Nil)) *)
+
+Inductive uint :=
+ | Nil
+ | D0 (_:uint)
+ | D1 (_:uint)
+ | D2 (_:uint)
+ | D3 (_:uint)
+ | D4 (_:uint)
+ | D5 (_:uint)
+ | D6 (_:uint)
+ | D7 (_:uint)
+ | D8 (_:uint)
+ | D9 (_:uint).
+
+(** [Nil] is the number terminator. Taken alone, it behaves as zero,
+ but rather use [D0 Nil] instead, since this form will be denoted
+ as [0], while [Nil] will be printed as [Nil]. *)
+
+Notation zero := (D0 Nil).
+
+(** For signed integers, we use two constructors [Pos] and [Neg]. *)
+
+Inductive int := Pos (d:uint) | Neg (d:uint).
+
+Delimit Scope uint_scope with uint.
+Bind Scope uint_scope with uint.
+Delimit Scope int_scope with int.
+Bind Scope int_scope with int.
+
+(** This representation favors simplicity over canonicity.
+ For normalizing numbers, we need to remove head zero digits,
+ and choose our canonical representation of 0 (here [D0 Nil]
+ for unsigned numbers and [Pos (D0 Nil)] for signed numbers). *)
+
+(** [nzhead] removes all head zero digits *)
+
+Fixpoint nzhead d :=
+ match d with
+ | D0 d => nzhead d
+ | _ => d
+ end.
+
+(** [unorm] : normalization of unsigned integers *)
+
+Definition unorm d :=
+ match nzhead d with
+ | Nil => zero
+ | d => d
+ end.
+
+(** [norm] : normalization of signed integers *)
+
+Definition norm d :=
+ match d with
+ | Pos d => Pos (unorm d)
+ | Neg d =>
+ match nzhead d with
+ | Nil => Pos zero
+ | d => Neg d
+ end
+ end.
+
+(** A few easy operations. For more advanced computations, use the conversions
+ with other Coq numeral datatypes (e.g. Z) and the operations on them. *)
+
+Definition opp (d:int) :=
+ match d with
+ | Pos d => Neg d
+ | Neg d => Pos d
+ end.
+
+(** For conversions with binary numbers, it is easier to operate
+ on little-endian numbers. *)
+
+Fixpoint revapp (d d' : uint) :=
+ match d with
+ | Nil => d'
+ | D0 d => revapp d (D0 d')
+ | D1 d => revapp d (D1 d')
+ | D2 d => revapp d (D2 d')
+ | D3 d => revapp d (D3 d')
+ | D4 d => revapp d (D4 d')
+ | D5 d => revapp d (D5 d')
+ | D6 d => revapp d (D6 d')
+ | D7 d => revapp d (D7 d')
+ | D8 d => revapp d (D8 d')
+ | D9 d => revapp d (D9 d')
+ end.
+
+Definition rev d := revapp d Nil.
+
+Module Little.
+
+(** Successor of little-endian numbers *)
+
+Fixpoint succ d :=
+ match d with
+ | Nil => D1 Nil
+ | D0 d => D1 d
+ | D1 d => D2 d
+ | D2 d => D3 d
+ | D3 d => D4 d
+ | D4 d => D5 d
+ | D5 d => D6 d
+ | D6 d => D7 d
+ | D7 d => D8 d
+ | D8 d => D9 d
+ | D9 d => D0 (succ d)
+ end.
+
+(** Doubling little-endian numbers *)
+
+Fixpoint double d :=
+ match d with
+ | Nil => Nil
+ | D0 d => D0 (double d)
+ | D1 d => D2 (double d)
+ | D2 d => D4 (double d)
+ | D3 d => D6 (double d)
+ | D4 d => D8 (double d)
+ | D5 d => D0 (succ_double d)
+ | D6 d => D2 (succ_double d)
+ | D7 d => D4 (succ_double d)
+ | D8 d => D6 (succ_double d)
+ | D9 d => D8 (succ_double d)
+ end
+
+with succ_double d :=
+ match d with
+ | Nil => D1 Nil
+ | D0 d => D1 (double d)
+ | D1 d => D3 (double d)
+ | D2 d => D5 (double d)
+ | D3 d => D7 (double d)
+ | D4 d => D9 (double d)
+ | D5 d => D1 (succ_double d)
+ | D6 d => D3 (succ_double d)
+ | D7 d => D5 (succ_double d)
+ | D8 d => D7 (succ_double d)
+ | D9 d => D9 (succ_double d)
+ end.
+
+End Little.
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 85123cc4..15ca5abc 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
Set Implicit Arguments.
@@ -125,6 +127,25 @@ Proof.
[apply Hl | apply Hr]; assumption.
Qed.
+Theorem imp_iff_compat_l : forall A B C : Prop,
+ (B <-> C) -> ((A -> B) <-> (A -> C)).
+Proof.
+ intros ? ? ? [Hl Hr]; split; intros H ?; [apply Hl | apply Hr]; apply H; assumption.
+Qed.
+
+Theorem imp_iff_compat_r : forall A B C : Prop,
+ (B <-> C) -> ((B -> A) <-> (C -> A)).
+Proof.
+ intros ? ? ? [Hl Hr]; split; intros H ?; [apply H, Hr | apply H, Hl]; assumption.
+Qed.
+
+Theorem not_iff_compat : forall A B : Prop,
+ (A <-> B) -> (~ A <-> ~B).
+Proof.
+ intros; apply imp_iff_compat_r; assumption.
+Qed.
+
+
(** Some equivalences *)
Theorem neg_false : forall A : Prop, ~ A <-> (A <-> False).
@@ -204,7 +225,7 @@ Proof.
Qed.
(** [(IF_then_else P Q R)], written [IF P then Q else R] denotes
- either [P] and [Q], or [~P] and [Q] *)
+ either [P] and [Q], or [~P] and [R] *)
Definition IF_then_else (P Q R:Prop) := P /\ Q \/ ~ P /\ R.
@@ -243,9 +264,16 @@ Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..))
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 ']' ']'")
+Notation "'exists2' x : A , p & q" := (ex2 (A:=A) (fun x => p) (fun x => q))
+ (at level 200, x ident, A at level 200, p at level 200, right associativity,
+ format "'[' 'exists2' '/ ' x : A , '/ ' '[' p & '/' q ']' ']'")
+ : type_scope.
+
+Notation "'exists2' ' x , p & q" := (ex2 (fun x => p) (fun x => q))
+ (at level 200, x strict pattern, p at level 200, right associativity) : type_scope.
+Notation "'exists2' ' x : A , p & q" := (ex2 (A:=A) (fun x => p) (fun x => q))
+ (at level 200, x strict pattern, A at level 200, p at level 200, right associativity,
+ format "'[' 'exists2' '/ ' ' x : A , '/ ' '[' p & '/' q ']' ']'")
: type_scope.
(** Derived rules for universal quantification *)
@@ -294,8 +322,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 : core.
-Hint Resolve 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.
@@ -424,7 +452,7 @@ Proof.
destruct e. reflexivity.
Defined.
-(** The goupoid structure of equality *)
+(** The groupoid structure of equality *)
Theorem eq_trans_refl_l : forall A (x y:A) (e:x=y), eq_trans eq_refl e = e.
Proof.
@@ -485,6 +513,11 @@ Proof.
reflexivity.
Defined.
+Lemma eq_refl_map_distr : forall A B x (f:A->B), f_equal f (eq_refl x) = eq_refl (f x).
+Proof.
+ reflexivity.
+Qed.
+
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'.
@@ -503,16 +536,29 @@ destruct e, e'.
reflexivity.
Defined.
+Lemma eq_trans_rew_distr : forall A (P:A -> Type) (x y z:A) (e:x=y) (e':y=z) (k:P x),
+ rew (eq_trans e e') in k = rew e' in rew e in k.
+Proof.
+ destruct e, e'; reflexivity.
+Qed.
+
+Lemma rew_const : forall A P (x y:A) (e:x=y) (k:P),
+ rew [fun _ => P] e in k = k.
+Proof.
+ destruct e; reflexivity.
+Qed.
+
+
(* Aliases *)
-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 sym_eq := eq_sym (only parsing).
+Notation trans_eq := eq_trans (only parsing).
+Notation sym_not_eq := 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").
+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).
Hint Immediate eq_sym not_eq_sym: core.
@@ -553,9 +599,10 @@ 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).
+ assert (H : x0 = x1) by (transitivity x; [symmetry|]; auto).
+ destruct H.
assumption.
-Qed.
+Qed.
Lemma forall_exists_coincide_unique_domain :
forall A (P:A->Prop),
@@ -567,7 +614,7 @@ Proof.
exists x. split; [trivial|].
destruct H with (Q:=fun x'=>x=x') as (_,Huniq).
apply Huniq. exists x; auto.
-Qed.
+Qed.
(** * Being inhabited *)
@@ -589,6 +636,11 @@ Proof.
destruct 1; auto.
Qed.
+Lemma inhabited_covariant (A B : Type) : (A -> B) -> inhabited A -> inhabited B.
+Proof.
+ intros f [x];exact (inhabits (f x)).
+Qed.
+
(** Declaration of stepl and stepr for eq and iff *)
Lemma eq_stepl : forall (A : Type) (x y z : A), x = y -> x = z -> z = y.
@@ -606,3 +658,97 @@ Qed.
Declare Left Step iff_stepl.
Declare Right Step iff_trans.
+
+Local Notation "'rew' 'dependent' H 'in' H'"
+ := (match H with
+ | eq_refl => H'
+ end)
+ (at level 10, H' at level 10,
+ format "'[' 'rew' 'dependent' '/ ' H in '/' H' ']'").
+
+(** Equality for [ex] *)
+Section ex.
+ Local Unset Implicit Arguments.
+ Definition eq_ex_uncurried {A : Type} (P : A -> Prop) {u1 v1 : A} {u2 : P u1} {v2 : P v1}
+ (pq : exists p : u1 = v1, rew p in u2 = v2)
+ : ex_intro P u1 u2 = ex_intro P v1 v2.
+ Proof.
+ destruct pq as [p q].
+ destruct q; simpl in *.
+ destruct p; reflexivity.
+ Qed.
+
+ Definition eq_ex {A : Type} {P : A -> Prop} (u1 v1 : A) (u2 : P u1) (v2 : P v1)
+ (p : u1 = v1) (q : rew p in u2 = v2)
+ : ex_intro P u1 u2 = ex_intro P v1 v2
+ := eq_ex_uncurried P (ex_intro _ p q).
+
+ Definition eq_ex_hprop {A} {P : A -> Prop} (P_hprop : forall (x : A) (p q : P x), p = q)
+ (u1 v1 : A) (u2 : P u1) (v2 : P v1)
+ (p : u1 = v1)
+ : ex_intro P u1 u2 = ex_intro P v1 v2
+ := eq_ex u1 v1 u2 v2 p (P_hprop _ _ _).
+
+ Lemma rew_ex {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : exists p, Q x p) {y} (H : x = y)
+ : rew [fun a => exists p, Q a p] H in u
+ = match u with
+ | ex_intro _ u1 u2
+ => ex_intro
+ (Q y)
+ (rew H in u1)
+ (rew dependent H in u2)
+ end.
+ Proof.
+ destruct H, u; reflexivity.
+ Qed.
+End ex.
+
+(** Equality for [ex2] *)
+Section ex2.
+ Local Unset Implicit Arguments.
+
+ Definition eq_ex2_uncurried {A : Type} (P Q : A -> Prop) {u1 v1 : A}
+ {u2 : P u1} {v2 : P v1}
+ {u3 : Q u1} {v3 : Q v1}
+ (pq : exists2 p : u1 = v1, rew p in u2 = v2 & rew p in u3 = v3)
+ : ex_intro2 P Q u1 u2 u3 = ex_intro2 P Q v1 v2 v3.
+ Proof.
+ destruct pq as [p q r].
+ destruct r, q, p; simpl in *.
+ reflexivity.
+ Qed.
+
+ Definition eq_ex2 {A : Type} {P Q : A -> Prop}
+ (u1 v1 : A)
+ (u2 : P u1) (v2 : P v1)
+ (u3 : Q u1) (v3 : Q v1)
+ (p : u1 = v1) (q : rew p in u2 = v2) (r : rew p in u3 = v3)
+ : ex_intro2 P Q u1 u2 u3 = ex_intro2 P Q v1 v2 v3
+ := eq_ex2_uncurried P Q (ex_intro2 _ _ p q r).
+
+ Definition eq_ex2_hprop {A} {P Q : A -> Prop}
+ (P_hprop : forall (x : A) (p q : P x), p = q)
+ (Q_hprop : forall (x : A) (p q : Q x), p = q)
+ (u1 v1 : A) (u2 : P u1) (v2 : P v1) (u3 : Q u1) (v3 : Q v1)
+ (p : u1 = v1)
+ : ex_intro2 P Q u1 u2 u3 = ex_intro2 P Q v1 v2 v3
+ := eq_ex2 u1 v1 u2 v2 u3 v3 p (P_hprop _ _ _) (Q_hprop _ _ _).
+
+ Lemma rew_ex2 {A x} {P : A -> Type}
+ (Q : forall a, P a -> Prop)
+ (R : forall a, P a -> Prop)
+ (u : exists2 p, Q x p & R x p) {y} (H : x = y)
+ : rew [fun a => exists2 p, Q a p & R a p] H in u
+ = match u with
+ | ex_intro2 _ _ u1 u2 u3
+ => ex_intro2
+ (Q y)
+ (R y)
+ (rew H in u1)
+ (rew dependent H in u2)
+ (rew dependent H in u3)
+ end.
+ Proof.
+ destruct H, u; reflexivity.
+ Qed.
+End ex2.
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index 4536dfc0..6f10a939 100644
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** This module defines type constructors for types in [Type]
@@ -66,7 +68,7 @@ Defined.
Hint Immediate identity_sym not_identity_sym: core.
-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").
+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).
diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v
index b8920586..ad1bc717 100644
--- a/theories/Init/Nat.v
+++ b/theories/Init/Nat.v
@@ -1,13 +1,15 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
Require Import Notations Logic Datatypes.
-
+Require Decimal.
Local Open Scope nat_scope.
(**********************************************************************)
@@ -134,6 +136,62 @@ Fixpoint pow n m :=
where "n ^ m" := (pow n m) : nat_scope.
+(** ** Tail-recursive versions of [add] and [mul] *)
+
+Fixpoint tail_add n m :=
+ match n with
+ | O => m
+ | S n => tail_add n (S m)
+ end.
+
+(** [tail_addmul r n m] is [r + n * m]. *)
+
+Fixpoint tail_addmul r n m :=
+ match n with
+ | O => r
+ | S n => tail_addmul (tail_add m r) n m
+ end.
+
+Definition tail_mul n m := tail_addmul 0 n m.
+
+(** ** Conversion with a decimal representation for printing/parsing *)
+
+Local Notation ten := (S (S (S (S (S (S (S (S (S (S O)))))))))).
+
+Fixpoint of_uint_acc (d:Decimal.uint)(acc:nat) :=
+ match d with
+ | Decimal.Nil => acc
+ | Decimal.D0 d => of_uint_acc d (tail_mul ten acc)
+ | Decimal.D1 d => of_uint_acc d (S (tail_mul ten acc))
+ | Decimal.D2 d => of_uint_acc d (S (S (tail_mul ten acc)))
+ | Decimal.D3 d => of_uint_acc d (S (S (S (tail_mul ten acc))))
+ | Decimal.D4 d => of_uint_acc d (S (S (S (S (tail_mul ten acc)))))
+ | Decimal.D5 d => of_uint_acc d (S (S (S (S (S (tail_mul ten acc))))))
+ | Decimal.D6 d => of_uint_acc d (S (S (S (S (S (S (tail_mul ten acc)))))))
+ | Decimal.D7 d => of_uint_acc d (S (S (S (S (S (S (S (tail_mul ten acc))))))))
+ | Decimal.D8 d => of_uint_acc d (S (S (S (S (S (S (S (S (tail_mul ten acc)))))))))
+ | Decimal.D9 d => of_uint_acc d (S (S (S (S (S (S (S (S (S (tail_mul ten acc))))))))))
+ end.
+
+Definition of_uint (d:Decimal.uint) := of_uint_acc d O.
+
+Fixpoint to_little_uint n acc :=
+ match n with
+ | O => acc
+ | S n => to_little_uint n (Decimal.Little.succ acc)
+ end.
+
+Definition to_uint n :=
+ Decimal.rev (to_little_uint n Decimal.zero).
+
+Definition of_int (d:Decimal.int) : option nat :=
+ match Decimal.norm d with
+ | Decimal.Pos u => Some (of_uint u)
+ | _ => None
+ end.
+
+Definition to_int n := Decimal.Pos (to_uint n).
+
(** ** Euclidean division *)
(** This division is linear and tail-recursive.
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 48fbe079..72073bb4 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** These are the notations whose level and associativity are imposed by Coq *)
@@ -66,15 +68,46 @@ Reserved Notation "{ x }" (at level 0, x at level 99).
(** Notations for sigma-types or subsets *)
+Reserved Notation "{ A } + { B }" (at level 50, left associativity).
+Reserved Notation "A + { B }" (at level 50, left associativity).
+
Reserved Notation "{ x | P }" (at level 0, x at level 99).
Reserved Notation "{ x | P & Q }" (at level 0, x at level 99).
Reserved Notation "{ x : A | P }" (at level 0, x at level 99).
Reserved Notation "{ x : A | P & Q }" (at level 0, x at level 99).
+Reserved Notation "{ x & P }" (at level 0, x at level 99).
Reserved Notation "{ x : A & P }" (at level 0, x at level 99).
Reserved Notation "{ x : A & P & Q }" (at level 0, x at level 99).
+Reserved Notation "{ ' pat | P }"
+ (at level 0, pat strict pattern, format "{ ' pat | P }").
+Reserved Notation "{ ' pat | P & Q }"
+ (at level 0, pat strict pattern, format "{ ' pat | P & Q }").
+
+Reserved Notation "{ ' pat : A | P }"
+ (at level 0, pat strict pattern, format "{ ' pat : A | P }").
+Reserved Notation "{ ' pat : A | P & Q }"
+ (at level 0, pat strict pattern, format "{ ' pat : A | P & Q }").
+
+Reserved Notation "{ ' pat : A & P }"
+ (at level 0, pat strict pattern, format "{ ' pat : A & P }").
+Reserved Notation "{ ' pat : A & P & Q }"
+ (at level 0, pat strict pattern, format "{ ' pat : A & P & Q }").
+
+(** Support for Gonthier-Ssreflect's "if c is pat then u else v" *)
+
+Module IfNotations.
+
+Notation "'if' c 'is' p 'then' u 'else' v" :=
+ (match c with p => u | _ => v end)
+ (at level 200, p pattern at level 100).
+
+End IfNotations.
+
+(** Scopes *)
+
Delimit Scope type_scope with type.
Delimit Scope function_scope with function.
Delimit Scope core_scope with core.
@@ -88,9 +121,6 @@ Open Scope type_scope.
(** ML Tactic Notations *)
-Declare ML Module "coretactics".
-Declare ML Module "extratactics".
-Declare ML Module "g_auto".
-Declare ML Module "g_class".
-Declare ML Module "g_eqdecide".
-Declare ML Module "g_rewrite".
+Declare ML Module "ltac_plugin".
+
+Global Set Default Proof Mode "Classic".
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 6c4a6350..d5322d09 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** The type [nat] of Peano natural numbers (built from [O] and [S])
@@ -37,7 +39,7 @@ Hint Resolve f_equal_nat: core.
(** The predecessor function *)
-Notation pred := Nat.pred (compat "8.4").
+Notation pred := Nat.pred (only parsing).
Definition f_equal_pred := f_equal pred.
@@ -79,7 +81,7 @@ Hint Resolve n_Sn: core.
(** Addition *)
-Notation plus := Nat.add (compat "8.4").
+Notation plus := Nat.add (only parsing).
Infix "+" := Nat.add : nat_scope.
Definition f_equal2_plus := f_equal2 plus.
@@ -90,7 +92,9 @@ Lemma plus_n_O : forall n:nat, n = n + 0.
Proof.
induction n; simpl; auto.
Qed.
-Hint Resolve plus_n_O: core.
+
+Remove Hints eq_refl : core.
+Hint Resolve plus_n_O eq_refl: core. (* We want eq_refl to have higher priority than plus_n_O *)
Lemma plus_O_n : forall n:nat, 0 + n = n.
Proof.
@@ -110,12 +114,12 @@ Qed.
(** Standard associated names *)
-Notation plus_0_r_reverse := plus_n_O (compat "8.2").
-Notation plus_succ_r_reverse := plus_n_Sm (compat "8.2").
+Notation plus_0_r_reverse := plus_n_O (only parsing).
+Notation plus_succ_r_reverse := plus_n_Sm (only parsing).
(** Multiplication *)
-Notation mult := Nat.mul (compat "8.4").
+Notation mult := Nat.mul (only parsing).
Infix "*" := Nat.mul : nat_scope.
Definition f_equal2_mult := f_equal2 mult.
@@ -137,12 +141,12 @@ Hint Resolve mult_n_Sm: core.
(** Standard associated names *)
-Notation mult_0_r_reverse := mult_n_O (compat "8.2").
-Notation mult_succ_r_reverse := mult_n_Sm (compat "8.2").
+Notation mult_0_r_reverse := mult_n_O (only parsing).
+Notation mult_succ_r_reverse := mult_n_Sm (only parsing).
(** Truncated subtraction: [m-n] is [0] if [n>=m] *)
-Notation minus := Nat.sub (compat "8.4").
+Notation minus := Nat.sub (only parsing).
Infix "-" := Nat.sub : nat_scope.
(** Definition of the usual orders, the basic properties of [le] and [lt]
@@ -219,8 +223,8 @@ Qed.
(** Maximum and minimum : definitions and specifications *)
-Notation max := Nat.max (compat "8.4").
-Notation min := Nat.min (compat "8.4").
+Notation max := Nat.max (only parsing).
+Notation min := Nat.min (only parsing).
Lemma max_l n m : m <= n -> Nat.max n m = n.
Proof.
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 03f2328d..802f18c0 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
Require Export Notations.
@@ -11,6 +13,7 @@ Require Export Logic.
Require Export Logic_Type.
Require Export Datatypes.
Require Export Specif.
+Require Coq.Init.Decimal.
Require Coq.Init.Nat.
Require Export Peano.
Require Export Coq.Init.Wf.
@@ -18,10 +21,7 @@ Require Export Coq.Init.Tactics.
Require Export Coq.Init.Tauto.
(* 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 "recdef_plugin".
(* Default substrings not considered by queries like SearchAbout *)
-Add Search Blacklist "_subproof" "Private_".
+Add Search Blacklist "_subproof" "_subterm" "Private_".
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 9fc00e80..b6afba29 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** Basic specifications : sets that may contain logical information *)
@@ -49,10 +51,20 @@ Notation "{ x | P & Q }" := (sig2 (fun x => P) (fun x => Q)) : type_scope.
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 & P }" := (sigT (fun x => P)) : type_scope.
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.
+Notation "{ ' pat | P }" := (sig (fun pat => P)) : type_scope.
+Notation "{ ' pat | P & Q }" := (sig2 (fun pat => P) (fun pat => Q)) : type_scope.
+Notation "{ ' pat : A | P }" := (sig (A:=A) (fun pat => P)) : type_scope.
+Notation "{ ' pat : A | P & Q }" := (sig2 (A:=A) (fun pat => P) (fun pat => Q)) :
+ type_scope.
+Notation "{ ' pat : A & P }" := (sigT (A:=A) (fun pat => P)) : type_scope.
+Notation "{ ' pat : A & P & Q }" := (sigT2 (A:=A) (fun pat => P) (fun pat => Q)) :
+ type_scope.
+
Add Printing Let sig.
Add Printing Let sig2.
Add Printing Let sigT.
@@ -103,7 +115,7 @@ Definition sig_of_sig2 (A : Type) (P Q : A -> Prop) (X : sig2 P Q) : sig P
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
+ [(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.
@@ -190,6 +202,435 @@ Definition sig2_of_sigT2 (A : Type) (P Q : A -> Prop) (X : sigT2 P Q) : sig2 P Q
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).
+(** η Principles *)
+Definition sigT_eta {A P} (p : { a : A & P a })
+ : p = existT _ (projT1 p) (projT2 p).
+Proof. destruct p; reflexivity. Defined.
+
+Definition sig_eta {A P} (p : { a : A | P a })
+ : p = exist _ (proj1_sig p) (proj2_sig p).
+Proof. destruct p; reflexivity. Defined.
+
+Definition sigT2_eta {A P Q} (p : { a : A & P a & Q a })
+ : p = existT2 _ _ (projT1 (sigT_of_sigT2 p)) (projT2 (sigT_of_sigT2 p)) (projT3 p).
+Proof. destruct p; reflexivity. Defined.
+
+Definition sig2_eta {A P Q} (p : { a : A | P a & Q a })
+ : p = exist2 _ _ (proj1_sig (sig_of_sig2 p)) (proj2_sig (sig_of_sig2 p)) (proj3_sig p).
+Proof. destruct p; reflexivity. Defined.
+
+(** [exists x : A, B] is equivalent to [inhabited {x : A | B}] *)
+Lemma exists_to_inhabited_sig {A P} : (exists x : A, P x) -> inhabited {x : A | P x}.
+Proof.
+ intros [x y]. exact (inhabits (exist _ x y)).
+Qed.
+
+Lemma inhabited_sig_to_exists {A P} : inhabited {x : A | P x} -> exists x : A, P x.
+Proof.
+ intros [[x y]];exists x;exact y.
+Qed.
+
+(** Equality of sigma types *)
+Import EqNotations.
+Local Notation "'rew' 'dependent' H 'in' H'"
+ := (match H with
+ | eq_refl => H'
+ end)
+ (at level 10, H' at level 10,
+ format "'[' 'rew' 'dependent' '/ ' H in '/' H' ']'").
+
+(** Equality for [sigT] *)
+Section sigT.
+ Local Unset Implicit Arguments.
+ (** Projecting an equality of a pair to equality of the first components *)
+ Definition projT1_eq {A} {P : A -> Type} {u v : { a : A & P a }} (p : u = v)
+ : projT1 u = projT1 v
+ := f_equal (@projT1 _ _) p.
+
+ (** Projecting an equality of a pair to equality of the second components *)
+ Definition projT2_eq {A} {P : A -> Type} {u v : { a : A & P a }} (p : u = v)
+ : rew projT1_eq p in projT2 u = projT2 v
+ := rew dependent p in eq_refl.
+
+ (** Equality of [sigT] is itself a [sigT] (forwards-reasoning version) *)
+ Definition eq_existT_uncurried {A : Type} {P : A -> Type} {u1 v1 : A} {u2 : P u1} {v2 : P v1}
+ (pq : { p : u1 = v1 & rew p in u2 = v2 })
+ : existT _ u1 u2 = existT _ v1 v2.
+ Proof.
+ destruct pq as [p q].
+ destruct q; simpl in *.
+ destruct p; reflexivity.
+ Defined.
+
+ (** Equality of [sigT] is itself a [sigT] (backwards-reasoning version) *)
+ Definition eq_sigT_uncurried {A : Type} {P : A -> Type} (u v : { a : A & P a })
+ (pq : { p : projT1 u = projT1 v & rew p in projT2 u = projT2 v })
+ : u = v.
+ Proof.
+ destruct u as [u1 u2], v as [v1 v2]; simpl in *.
+ apply eq_existT_uncurried; exact pq.
+ Defined.
+
+ (** Curried version of proving equality of sigma types *)
+ Definition eq_sigT {A : Type} {P : A -> Type} (u v : { a : A & P a })
+ (p : projT1 u = projT1 v) (q : rew p in projT2 u = projT2 v)
+ : u = v
+ := eq_sigT_uncurried u v (existT _ p q).
+
+ (** Equality of [sigT] when the property is an hProp *)
+ Definition eq_sigT_hprop {A P} (P_hprop : forall (x : A) (p q : P x), p = q)
+ (u v : { a : A & P a })
+ (p : projT1 u = projT1 v)
+ : u = v
+ := eq_sigT u v p (P_hprop _ _ _).
+
+ (** Equivalence of equality of [sigT] with a [sigT] of equality *)
+ (** We could actually prove an isomorphism here, and not just [<->],
+ but for simplicity, we don't. *)
+ Definition eq_sigT_uncurried_iff {A P}
+ (u v : { a : A & P a })
+ : u = v <-> { p : projT1 u = projT1 v & rew p in projT2 u = projT2 v }.
+ Proof.
+ split; [ intro; subst; exists eq_refl; reflexivity | apply eq_sigT_uncurried ].
+ Defined.
+
+ (** Induction principle for [@eq (sigT _)] *)
+ Definition eq_sigT_rect {A P} {u v : { a : A & P a }} (Q : u = v -> Type)
+ (f : forall p q, Q (eq_sigT u v p q))
+ : forall p, Q p.
+ Proof. intro p; specialize (f (projT1_eq p) (projT2_eq p)); destruct u, p; exact f. Defined.
+ Definition eq_sigT_rec {A P u v} (Q : u = v :> { a : A & P a } -> Set) := eq_sigT_rect Q.
+ Definition eq_sigT_ind {A P u v} (Q : u = v :> { a : A & P a } -> Prop) := eq_sigT_rec Q.
+
+ (** Equivalence of equality of [sigT] involving hProps with equality of the first components *)
+ Definition eq_sigT_hprop_iff {A P} (P_hprop : forall (x : A) (p q : P x), p = q)
+ (u v : { a : A & P a })
+ : u = v <-> (projT1 u = projT1 v)
+ := conj (fun p => f_equal (@projT1 _ _) p) (eq_sigT_hprop P_hprop u v).
+
+ (** Non-dependent classification of equality of [sigT] *)
+ Definition eq_sigT_nondep {A B : Type} (u v : { a : A & B })
+ (p : projT1 u = projT1 v) (q : projT2 u = projT2 v)
+ : u = v
+ := @eq_sigT _ _ u v p (eq_trans (rew_const _ _) q).
+
+ (** Classification of transporting across an equality of [sigT]s *)
+ Lemma rew_sigT {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : { p : P x & Q x p }) {y} (H : x = y)
+ : rew [fun a => { p : P a & Q a p }] H in u
+ = existT
+ (Q y)
+ (rew H in projT1 u)
+ (rew dependent H in (projT2 u)).
+ Proof.
+ destruct H, u; reflexivity.
+ Defined.
+End sigT.
+
+(** Equality for [sig] *)
+Section sig.
+ Local Unset Implicit Arguments.
+ (** Projecting an equality of a pair to equality of the first components *)
+ Definition proj1_sig_eq {A} {P : A -> Prop} {u v : { a : A | P a }} (p : u = v)
+ : proj1_sig u = proj1_sig v
+ := f_equal (@proj1_sig _ _) p.
+
+ (** Projecting an equality of a pair to equality of the second components *)
+ Definition proj2_sig_eq {A} {P : A -> Prop} {u v : { a : A | P a }} (p : u = v)
+ : rew proj1_sig_eq p in proj2_sig u = proj2_sig v
+ := rew dependent p in eq_refl.
+
+ (** Equality of [sig] is itself a [sig] (forwards-reasoning version) *)
+ Definition eq_exist_uncurried {A : Type} {P : A -> Prop} {u1 v1 : A} {u2 : P u1} {v2 : P v1}
+ (pq : { p : u1 = v1 | rew p in u2 = v2 })
+ : exist _ u1 u2 = exist _ v1 v2.
+ Proof.
+ destruct pq as [p q].
+ destruct q; simpl in *.
+ destruct p; reflexivity.
+ Defined.
+
+ (** Equality of [sig] is itself a [sig] (backwards-reasoning version) *)
+ Definition eq_sig_uncurried {A : Type} {P : A -> Prop} (u v : { a : A | P a })
+ (pq : { p : proj1_sig u = proj1_sig v | rew p in proj2_sig u = proj2_sig v })
+ : u = v.
+ Proof.
+ destruct u as [u1 u2], v as [v1 v2]; simpl in *.
+ apply eq_exist_uncurried; exact pq.
+ Defined.
+
+ (** Curried version of proving equality of sigma types *)
+ Definition eq_sig {A : Type} {P : A -> Prop} (u v : { a : A | P a })
+ (p : proj1_sig u = proj1_sig v) (q : rew p in proj2_sig u = proj2_sig v)
+ : u = v
+ := eq_sig_uncurried u v (exist _ p q).
+
+ (** Induction principle for [@eq (sig _)] *)
+ Definition eq_sig_rect {A P} {u v : { a : A | P a }} (Q : u = v -> Type)
+ (f : forall p q, Q (eq_sig u v p q))
+ : forall p, Q p.
+ Proof. intro p; specialize (f (proj1_sig_eq p) (proj2_sig_eq p)); destruct u, p; exact f. Defined.
+ Definition eq_sig_rec {A P u v} (Q : u = v :> { a : A | P a } -> Set) := eq_sig_rect Q.
+ Definition eq_sig_ind {A P u v} (Q : u = v :> { a : A | P a } -> Prop) := eq_sig_rec Q.
+
+ (** Equality of [sig] when the property is an hProp *)
+ Definition eq_sig_hprop {A} {P : A -> Prop} (P_hprop : forall (x : A) (p q : P x), p = q)
+ (u v : { a : A | P a })
+ (p : proj1_sig u = proj1_sig v)
+ : u = v
+ := eq_sig u v p (P_hprop _ _ _).
+
+ (** Equivalence of equality of [sig] with a [sig] of equality *)
+ (** We could actually prove an isomorphism here, and not just [<->],
+ but for simplicity, we don't. *)
+ Definition eq_sig_uncurried_iff {A} {P : A -> Prop}
+ (u v : { a : A | P a })
+ : u = v <-> { p : proj1_sig u = proj1_sig v | rew p in proj2_sig u = proj2_sig v }.
+ Proof.
+ split; [ intro; subst; exists eq_refl; reflexivity | apply eq_sig_uncurried ].
+ Defined.
+
+ (** Equivalence of equality of [sig] involving hProps with equality of the first components *)
+ Definition eq_sig_hprop_iff {A} {P : A -> Prop} (P_hprop : forall (x : A) (p q : P x), p = q)
+ (u v : { a : A | P a })
+ : u = v <-> (proj1_sig u = proj1_sig v)
+ := conj (fun p => f_equal (@proj1_sig _ _) p) (eq_sig_hprop P_hprop u v).
+
+ Lemma rew_sig {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : { p : P x | Q x p }) {y} (H : x = y)
+ : rew [fun a => { p : P a | Q a p }] H in u
+ = exist
+ (Q y)
+ (rew H in proj1_sig u)
+ (rew dependent H in proj2_sig u).
+ Proof.
+ destruct H, u; reflexivity.
+ Defined.
+End sig.
+
+(** Equality for [sigT] *)
+Section sigT2.
+ (* We make [sigT_of_sigT2] a coercion so we can use [projT1], [projT2] on [sigT2] *)
+ Local Coercion sigT_of_sigT2 : sigT2 >-> sigT.
+ Local Unset Implicit Arguments.
+ (** Projecting an equality of a pair to equality of the first components *)
+ Definition sigT_of_sigT2_eq {A} {P Q : A -> Type} {u v : { a : A & P a & Q a }} (p : u = v)
+ : u = v :> { a : A & P a }
+ := f_equal _ p.
+ Definition projT1_of_sigT2_eq {A} {P Q : A -> Type} {u v : { a : A & P a & Q a }} (p : u = v)
+ : projT1 u = projT1 v
+ := projT1_eq (sigT_of_sigT2_eq p).
+
+ (** Projecting an equality of a pair to equality of the second components *)
+ Definition projT2_of_sigT2_eq {A} {P Q : A -> Type} {u v : { a : A & P a & Q a }} (p : u = v)
+ : rew projT1_of_sigT2_eq p in projT2 u = projT2 v
+ := rew dependent p in eq_refl.
+
+ (** Projecting an equality of a pair to equality of the third components *)
+ Definition projT3_eq {A} {P Q : A -> Type} {u v : { a : A & P a & Q a }} (p : u = v)
+ : rew projT1_of_sigT2_eq p in projT3 u = projT3 v
+ := rew dependent p in eq_refl.
+
+ (** Equality of [sigT2] is itself a [sigT2] (forwards-reasoning version) *)
+ Definition eq_existT2_uncurried {A : Type} {P Q : A -> Type}
+ {u1 v1 : A} {u2 : P u1} {v2 : P v1} {u3 : Q u1} {v3 : Q v1}
+ (pqr : { p : u1 = v1
+ & rew p in u2 = v2 & rew p in u3 = v3 })
+ : existT2 _ _ u1 u2 u3 = existT2 _ _ v1 v2 v3.
+ Proof.
+ destruct pqr as [p q r].
+ destruct r, q, p; simpl.
+ reflexivity.
+ Defined.
+
+ (** Equality of [sigT2] is itself a [sigT2] (backwards-reasoning version) *)
+ Definition eq_sigT2_uncurried {A : Type} {P Q : A -> Type} (u v : { a : A & P a & Q a })
+ (pqr : { p : projT1 u = projT1 v
+ & rew p in projT2 u = projT2 v & rew p in projT3 u = projT3 v })
+ : u = v.
+ Proof.
+ destruct u as [u1 u2 u3], v as [v1 v2 v3]; simpl in *.
+ apply eq_existT2_uncurried; exact pqr.
+ Defined.
+
+ (** Curried version of proving equality of sigma types *)
+ Definition eq_sigT2 {A : Type} {P Q : A -> Type} (u v : { a : A & P a & Q a })
+ (p : projT1 u = projT1 v)
+ (q : rew p in projT2 u = projT2 v)
+ (r : rew p in projT3 u = projT3 v)
+ : u = v
+ := eq_sigT2_uncurried u v (existT2 _ _ p q r).
+
+ (** Equality of [sigT2] when the second property is an hProp *)
+ Definition eq_sigT2_hprop {A P Q} (Q_hprop : forall (x : A) (p q : Q x), p = q)
+ (u v : { a : A & P a & Q a })
+ (p : u = v :> { a : A & P a })
+ : u = v
+ := eq_sigT2 u v (projT1_eq p) (projT2_eq p) (Q_hprop _ _ _).
+
+ (** Equivalence of equality of [sigT2] with a [sigT2] of equality *)
+ (** We could actually prove an isomorphism here, and not just [<->],
+ but for simplicity, we don't. *)
+ Definition eq_sigT2_uncurried_iff {A P Q}
+ (u v : { a : A & P a & Q a })
+ : u = v
+ <-> { p : projT1 u = projT1 v
+ & rew p in projT2 u = projT2 v & rew p in projT3 u = projT3 v }.
+ Proof.
+ split; [ intro; subst; exists eq_refl; reflexivity | apply eq_sigT2_uncurried ].
+ Defined.
+
+ (** Induction principle for [@eq (sigT2 _ _)] *)
+ Definition eq_sigT2_rect {A P Q} {u v : { a : A & P a & Q a }} (R : u = v -> Type)
+ (f : forall p q r, R (eq_sigT2 u v p q r))
+ : forall p, R p.
+ Proof.
+ intro p.
+ specialize (f (projT1_of_sigT2_eq p) (projT2_of_sigT2_eq p) (projT3_eq p)).
+ destruct u, p; exact f.
+ Defined.
+ Definition eq_sigT2_rec {A P Q u v} (R : u = v :> { a : A & P a & Q a } -> Set) := eq_sigT2_rect R.
+ Definition eq_sigT2_ind {A P Q u v} (R : u = v :> { a : A & P a & Q a } -> Prop) := eq_sigT2_rec R.
+
+ (** Equivalence of equality of [sigT2] involving hProps with equality of the first components *)
+ Definition eq_sigT2_hprop_iff {A P Q} (Q_hprop : forall (x : A) (p q : Q x), p = q)
+ (u v : { a : A & P a & Q a })
+ : u = v <-> (u = v :> { a : A & P a })
+ := conj (fun p => f_equal (@sigT_of_sigT2 _ _ _) p) (eq_sigT2_hprop Q_hprop u v).
+
+ (** Non-dependent classification of equality of [sigT] *)
+ Definition eq_sigT2_nondep {A B C : Type} (u v : { a : A & B & C })
+ (p : projT1 u = projT1 v) (q : projT2 u = projT2 v) (r : projT3 u = projT3 v)
+ : u = v
+ := @eq_sigT2 _ _ _ u v p (eq_trans (rew_const _ _) q) (eq_trans (rew_const _ _) r).
+
+ (** Classification of transporting across an equality of [sigT2]s *)
+ Lemma rew_sigT2 {A x} {P : A -> Type} (Q R : forall a, P a -> Prop)
+ (u : { p : P x & Q x p & R x p })
+ {y} (H : x = y)
+ : rew [fun a => { p : P a & Q a p & R a p }] H in u
+ = existT2
+ (Q y)
+ (R y)
+ (rew H in projT1 u)
+ (rew dependent H in projT2 u)
+ (rew dependent H in projT3 u).
+ Proof.
+ destruct H, u; reflexivity.
+ Defined.
+End sigT2.
+
+(** Equality for [sig2] *)
+Section sig2.
+ (* We make [sig_of_sig2] a coercion so we can use [proj1], [proj2] on [sig2] *)
+ Local Coercion sig_of_sig2 : sig2 >-> sig.
+ Local Unset Implicit Arguments.
+ (** Projecting an equality of a pair to equality of the first components *)
+ Definition sig_of_sig2_eq {A} {P Q : A -> Prop} {u v : { a : A | P a & Q a }} (p : u = v)
+ : u = v :> { a : A | P a }
+ := f_equal _ p.
+ Definition proj1_sig_of_sig2_eq {A} {P Q : A -> Prop} {u v : { a : A | P a & Q a }} (p : u = v)
+ : proj1_sig u = proj1_sig v
+ := proj1_sig_eq (sig_of_sig2_eq p).
+
+ (** Projecting an equality of a pair to equality of the second components *)
+ Definition proj2_sig_of_sig2_eq {A} {P Q : A -> Prop} {u v : { a : A | P a & Q a }} (p : u = v)
+ : rew proj1_sig_of_sig2_eq p in proj2_sig u = proj2_sig v
+ := rew dependent p in eq_refl.
+
+ (** Projecting an equality of a pair to equality of the third components *)
+ Definition proj3_sig_eq {A} {P Q : A -> Prop} {u v : { a : A | P a & Q a }} (p : u = v)
+ : rew proj1_sig_of_sig2_eq p in proj3_sig u = proj3_sig v
+ := rew dependent p in eq_refl.
+
+ (** Equality of [sig2] is itself a [sig2] (fowards-reasoning version) *)
+ Definition eq_exist2_uncurried {A} {P Q : A -> Prop}
+ {u1 v1 : A} {u2 : P u1} {v2 : P v1} {u3 : Q u1} {v3 : Q v1}
+ (pqr : { p : u1 = v1
+ | rew p in u2 = v2 & rew p in u3 = v3 })
+ : exist2 _ _ u1 u2 u3 = exist2 _ _ v1 v2 v3.
+ Proof.
+ destruct pqr as [p q r].
+ destruct r, q, p; simpl.
+ reflexivity.
+ Defined.
+
+ (** Equality of [sig2] is itself a [sig2] (backwards-reasoning version) *)
+ Definition eq_sig2_uncurried {A} {P Q : A -> Prop} (u v : { a : A | P a & Q a })
+ (pqr : { p : proj1_sig u = proj1_sig v
+ | rew p in proj2_sig u = proj2_sig v & rew p in proj3_sig u = proj3_sig v })
+ : u = v.
+ Proof.
+ destruct u as [u1 u2 u3], v as [v1 v2 v3]; simpl in *.
+ apply eq_exist2_uncurried; exact pqr.
+ Defined.
+
+ (** Curried version of proving equality of sigma types *)
+ Definition eq_sig2 {A} {P Q : A -> Prop} (u v : { a : A | P a & Q a })
+ (p : proj1_sig u = proj1_sig v)
+ (q : rew p in proj2_sig u = proj2_sig v)
+ (r : rew p in proj3_sig u = proj3_sig v)
+ : u = v
+ := eq_sig2_uncurried u v (exist2 _ _ p q r).
+
+ (** Equality of [sig2] when the second property is an hProp *)
+ Definition eq_sig2_hprop {A} {P Q : A -> Prop} (Q_hprop : forall (x : A) (p q : Q x), p = q)
+ (u v : { a : A | P a & Q a })
+ (p : u = v :> { a : A | P a })
+ : u = v
+ := eq_sig2 u v (proj1_sig_eq p) (proj2_sig_eq p) (Q_hprop _ _ _).
+
+ (** Equivalence of equality of [sig2] with a [sig2] of equality *)
+ (** We could actually prove an isomorphism here, and not just [<->],
+ but for simplicity, we don't. *)
+ Definition eq_sig2_uncurried_iff {A P Q}
+ (u v : { a : A | P a & Q a })
+ : u = v
+ <-> { p : proj1_sig u = proj1_sig v
+ | rew p in proj2_sig u = proj2_sig v & rew p in proj3_sig u = proj3_sig v }.
+ Proof.
+ split; [ intro; subst; exists eq_refl; reflexivity | apply eq_sig2_uncurried ].
+ Defined.
+
+ (** Induction principle for [@eq (sig2 _ _)] *)
+ Definition eq_sig2_rect {A P Q} {u v : { a : A | P a & Q a }} (R : u = v -> Type)
+ (f : forall p q r, R (eq_sig2 u v p q r))
+ : forall p, R p.
+ Proof.
+ intro p.
+ specialize (f (proj1_sig_of_sig2_eq p) (proj2_sig_of_sig2_eq p) (proj3_sig_eq p)).
+ destruct u, p; exact f.
+ Defined.
+ Definition eq_sig2_rec {A P Q u v} (R : u = v :> { a : A | P a & Q a } -> Set) := eq_sig2_rect R.
+ Definition eq_sig2_ind {A P Q u v} (R : u = v :> { a : A | P a & Q a } -> Prop) := eq_sig2_rec R.
+
+ (** Equivalence of equality of [sig2] involving hProps with equality of the first components *)
+ Definition eq_sig2_hprop_iff {A} {P Q : A -> Prop} (Q_hprop : forall (x : A) (p q : Q x), p = q)
+ (u v : { a : A | P a & Q a })
+ : u = v <-> (u = v :> { a : A | P a })
+ := conj (fun p => f_equal (@sig_of_sig2 _ _ _) p) (eq_sig2_hprop Q_hprop u v).
+
+ (** Non-dependent classification of equality of [sig] *)
+ Definition eq_sig2_nondep {A} {B C : Prop} (u v : @sig2 A (fun _ => B) (fun _ => C))
+ (p : proj1_sig u = proj1_sig v) (q : proj2_sig u = proj2_sig v) (r : proj3_sig u = proj3_sig v)
+ : u = v
+ := @eq_sig2 _ _ _ u v p (eq_trans (rew_const _ _) q) (eq_trans (rew_const _ _) r).
+
+ (** Classification of transporting across an equality of [sig2]s *)
+ Lemma rew_sig2 {A x} {P : A -> Type} (Q R : forall a, P a -> Prop)
+ (u : { p : P x | Q x p & R x p })
+ {y} (H : x = y)
+ : rew [fun a => { p : P a | Q a p & R a p }] H in u
+ = exist2
+ (Q y)
+ (R y)
+ (rew H in proj1_sig u)
+ (rew dependent H in proj2_sig u)
+ (rew dependent H in proj3_sig u).
+ Proof.
+ destruct H, u; reflexivity.
+ Defined.
+End sig2.
+
+
(** [sumbool] is a boolean type equipped with the justification of
their value *)
@@ -263,10 +704,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.
@@ -304,16 +745,16 @@ Hint Resolve exist exist2 existT existT2: core.
(* Compatibility *)
-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").
+Notation sigS := sigT (compat "8.6").
+Notation existS := existT (compat "8.6").
+Notation sigS_rect := sigT_rect (compat "8.6").
+Notation sigS_rec := sigT_rec (compat "8.6").
+Notation sigS_ind := sigT_ind (compat "8.6").
+Notation projS1 := projT1 (compat "8.6").
+Notation projS2 := projT2 (compat "8.6").
+
+Notation sigS2 := sigT2 (compat "8.6").
+Notation existS2 := existT2 (compat "8.6").
+Notation sigS2_rect := sigT2_rect (compat "8.6").
+Notation sigS2_rec := sigT2_rec (compat "8.6").
+Notation sigS2_ind := sigT2_ind (compat "8.6").
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 5d1e87ae..8df533e7 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
Require Import Notations.
@@ -236,3 +238,93 @@ Tactic Notation "clear" "dependent" hyp(h) :=
Tactic Notation "revert" "dependent" hyp(h) :=
generalize dependent h.
+
+(** Provide an error message for dependent induction that reports an import is
+required to use it. Importing Coq.Program.Equality will shadow this notation
+with the actual [dependent induction] tactic. *)
+
+Tactic Notation "dependent" "induction" ident(H) :=
+ fail "To use dependent induction, first [Require Import Coq.Program.Equality.]".
+
+(** *** [inversion_sigma] *)
+(** The built-in [inversion] will frequently leave equalities of
+ dependent pairs. When the first type in the pair is an hProp or
+ otherwise simplifies, [inversion_sigma] is useful; it will replace
+ the equality of pairs with a pair of equalities, one involving a
+ term casted along the other. This might also prove useful for
+ writing a version of [inversion] / [dependent destruction] which
+ does not lose information, i.e., does not turn a goal which is
+ provable into one which requires axiom K / UIP. *)
+
+Ltac simpl_proj_exist_in H :=
+ repeat match type of H with
+ | context G[proj1_sig (exist _ ?x ?p)]
+ => let G' := context G[x] in change G' in H
+ | context G[proj2_sig (exist _ ?x ?p)]
+ => let G' := context G[p] in change G' in H
+ | context G[projT1 (existT _ ?x ?p)]
+ => let G' := context G[x] in change G' in H
+ | context G[projT2 (existT _ ?x ?p)]
+ => let G' := context G[p] in change G' in H
+ | context G[proj3_sig (exist2 _ _ ?x ?p ?q)]
+ => let G' := context G[q] in change G' in H
+ | context G[projT3 (existT2 _ _ ?x ?p ?q)]
+ => let G' := context G[q] in change G' in H
+ | context G[sig_of_sig2 (@exist2 ?A ?P ?Q ?x ?p ?q)]
+ => let G' := context G[@exist A P x p] in change G' in H
+ | context G[sigT_of_sigT2 (@existT2 ?A ?P ?Q ?x ?p ?q)]
+ => let G' := context G[@existT A P x p] in change G' in H
+ end.
+Ltac induction_sigma_in_using H rect :=
+ let H0 := fresh H in
+ let H1 := fresh H in
+ induction H as [H0 H1] using (rect _ _ _ _);
+ simpl_proj_exist_in H0;
+ simpl_proj_exist_in H1.
+Ltac induction_sigma2_in_using H rect :=
+ let H0 := fresh H in
+ let H1 := fresh H in
+ let H2 := fresh H in
+ induction H as [H0 H1 H2] using (rect _ _ _ _ _);
+ simpl_proj_exist_in H0;
+ simpl_proj_exist_in H1;
+ simpl_proj_exist_in H2.
+Ltac inversion_sigma_step :=
+ match goal with
+ | [ H : _ = exist _ _ _ |- _ ]
+ => induction_sigma_in_using H @eq_sig_rect
+ | [ H : _ = existT _ _ _ |- _ ]
+ => induction_sigma_in_using H @eq_sigT_rect
+ | [ H : exist _ _ _ = _ |- _ ]
+ => induction_sigma_in_using H @eq_sig_rect
+ | [ H : existT _ _ _ = _ |- _ ]
+ => induction_sigma_in_using H @eq_sigT_rect
+ | [ H : _ = exist2 _ _ _ _ _ |- _ ]
+ => induction_sigma2_in_using H @eq_sig2_rect
+ | [ H : _ = existT2 _ _ _ _ _ |- _ ]
+ => induction_sigma2_in_using H @eq_sigT2_rect
+ | [ H : exist2 _ _ _ _ _ = _ |- _ ]
+ => induction_sigma_in_using H @eq_sig2_rect
+ | [ H : existT2 _ _ _ _ _ = _ |- _ ]
+ => induction_sigma_in_using H @eq_sigT2_rect
+ end.
+Ltac inversion_sigma := repeat inversion_sigma_step.
+
+(** A version of [time] that works for constrs *)
+
+Ltac time_constr tac :=
+ let eval_early := match goal with _ => restart_timer end in
+ let ret := tac () in
+ let eval_early := match goal with _ => finish_timing ( "Tactic evaluation" ) end in
+ ret.
+
+(** Useful combinators *)
+
+Ltac assert_fails tac :=
+ tryif tac then fail 0 tac "succeeds" else idtac.
+Ltac assert_succeeds tac :=
+ tryif (assert_fails tac) then fail 0 tac "fails" else idtac.
+Tactic Notation "assert_succeeds" tactic3(tac) :=
+ assert_succeeds tac.
+Tactic Notation "assert_fails" tactic3(tac) :=
+ assert_fails tac.
diff --git a/theories/Init/Tauto.v b/theories/Init/Tauto.v
index 1e409607..87b7a9a3 100644
--- a/theories/Init/Tauto.v
+++ b/theories/Init/Tauto.v
@@ -2,7 +2,7 @@ Require Import Notations.
Require Import Datatypes.
Require Import Logic.
-Local Declare ML Module "tauto".
+Declare ML Module "tauto_plugin".
Local Ltac not_dep_intros :=
repeat match goal with
@@ -27,7 +27,7 @@ Local Ltac simplif flags :=
| id: ?X1 |- _ => is_disj flags X1; elim id; intro; clear id
| id0: (forall (_: ?X1), ?X2), id1: ?X1|- _ =>
(* generalize (id0 id1); intro; clear id0 does not work
- (see Marco Maggiesi's bug PR#301)
+ (see Marco Maggiesi's BZ#301)
so we instead use Assert and exact. *)
assert X2; [exact (id0 id1) | clear id0]
| id: forall (_ : ?X1), ?X2|- _ =>
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index b5b17e5e..c27ffa33 100644
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** * This module proves the validity of
diff --git a/theories/Init/_CoqProject b/theories/Init/_CoqProject
new file mode 100644
index 00000000..bff79d34
--- /dev/null
+++ b/theories/Init/_CoqProject
@@ -0,0 +1,2 @@
+-R .. Coq
+-arg -noinit
diff --git a/theories/Init/vo.itarget b/theories/Init/vo.itarget
deleted file mode 100644
index 99877065..00000000
--- a/theories/Init/vo.itarget
+++ /dev/null
@@ -1,11 +0,0 @@
-Datatypes.vo
-Logic_Type.vo
-Logic.vo
-Notations.vo
-Peano.vo
-Prelude.vo
-Specif.vo
-Tactics.vo
-Wf.vo
-Nat.vo
-Tauto.vo
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 09:07:29 +0000