From c490d8581c3cefa0dbae505ed465feaf1fbd077b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Thu, 14 Mar 2013 20:13:29 +0100
Subject: [PATCH] An axiomatization and implementation of machine integers.

theories/base.v  6 ++++++
theories/decidable.v  44 ++++++++++++++++++++++
theories/list.v  11 +++++++++++
theories/numbers.v  14 ++++++++++++++
theories/proof_irrel.v  41 +++++++++++++++++++++++++++++++++++++++
5 files changed, 95 insertions(+), 21 deletions()
create mode 100644 theories/proof_irrel.v
diff git a/theories/base.v b/theories/base.v
index e07bc30..49cc37e 100644
 a/theories/base.v
+++ b/theories/base.v
@@ 120,6 +120,12 @@ Instance sum_inhabited_r {A B} (iB : Inhabited A) : Inhabited (A + B) :=
end.
Instance option_inhabited {A} : Inhabited (option A) := populate None.
+(** ** Proof irrelevant types *)
+(** This type class collects types that are proof irrelevant. That means, all
+elements of the type are equal. We use this notion only used for propositions,
+but by universe polymorphism we can generalize it. *)
+Class ProofIrrel (A : Type) : Prop := proof_irrel (x y : A) : x = y.
+
(** ** Setoid equality *)
(** We define an operational type class for setoid equality. This is based on
(Spitters/van der Weegen, 2011). *)
diff git a/theories/decidable.v b/theories/decidable.v
index 662d208..ecce351 100644
 a/theories/decidable.v
+++ b/theories/decidable.v
@@ 3,7 +3,7 @@
(** This file collects theorems, definitions, tactics, related to propositions
with a decidable equality. Such propositions are collected by the [Decision]
type class. *)
Require Export base tactics.
+Require Export proof_irrel.
Hint Extern 200 (Decision _) => progress (lazy beta) : typeclass_instances.
@@ 24,28 +24,38 @@ Lemma decide_rel_correct {A B} (R : A → B → Prop) `{∀ x y, Decision (R x y
(x : A) (y : B) : decide_rel R x y = decide (R x y).
Proof. done. Qed.
+Lemma decide_true {A} `{Decision P} (x y : A) :
+ P → (if decide P then x else y) = x.
+Proof. by destruct (decide P). Qed.
+Lemma decide_false {A} `{Decision P} (x y : A) :
+ ¬P → (if decide P then x else y) = y.
+Proof. by destruct (decide P). Qed.
+
(** The tactic [destruct_decide] destructs a sumbool [dec]. If one of the
components is double negated, it will try to remove the double negation. *)
Ltac destruct_decide dec :=
 let H := fresh in
+Tactic Notation "destruct_decide" constr(dec) "as" ident(H) :=
destruct dec as [HH];
try match type of H with
 ¬¬_ => apply dec_stable in H
end.
+Tactic Notation "destruct_decide" constr(dec) :=
+ let H := fresh in destruct_decide dec as H.
(** The tactic [case_decide] performs case analysis on an arbitrary occurrence
of [decide] or [decide_rel] in the conclusion or hypotheses. *)
Ltac case_decide :=
+Tactic Notation "case_decide" "as" ident(Hd) :=
match goal with
 H : context [@decide ?P ?dec]  _ =>
 destruct_decide (@decide P dec)
+ destruct_decide (@decide P dec) as Hd
 H : context [@decide_rel _ _ ?R ?x ?y ?dec]  _ =>
 destruct_decide (@decide_rel _ _ R x y dec)
+ destruct_decide (@decide_rel _ _ R x y dec) as Hd
  context [@decide ?P ?dec] =>
 destruct_decide (@decide P dec)
+ destruct_decide (@decide P dec) as Hd
  context [@decide_rel _ _ ?R ?x ?y ?dec] =>
 destruct_decide (@decide_rel _ _ R x y dec)
+ destruct_decide (@decide_rel _ _ R x y dec) as Hd
end.
+Tactic Notation "case_decide" :=
+ let H := fresh in case_decide as H.
(** The tactic [solve_decision] uses Coq's [decide equality] tactic together
with instance resolution to automatically generate decision procedures. *)
@@ 107,23 +117,11 @@ Definition dexist `{∀ x : A, Decision (P x)} (x : A) (p : P x) : dsig P :=
x↾bool_decide_pack _ p.
Lemma dsig_eq `(P : A → Prop) `{∀ x, Decision (P x)}
(x y : dsig P) : x = y ↔ `x = `y.
Proof.
 split.
 * destruct x, y. apply proj1_sig_inj.
 * intro. destruct x as [x Hx], y as [y Hy].
 simpl in *. subst. f_equal.
 revert Hx Hy. case (bool_decide (P y)).
 + by intros [] [].
 + done.
Qed.
+Proof. apply (sig_eq_pi _). Qed.
Lemma dexists_proj1 `(P : A → Prop) `{∀ x, Decision (P x)} (x : dsig P) p :
dexist (`x) p = x.
Proof. by apply dsig_eq. Qed.
Global Instance dsig_eq_dec `(P : A → Prop) `{∀ x, Decision (P x)}
 `{∀ x y : A, Decision (x = y)} (x y : dsig P) : Decision (x = y).
Proof. refine (cast_if (decide (`x = `y))); by rewrite dsig_eq. Defined.

(** * Instances of Decision *)
(** Instances of [Decision] for operators of propositional logic. *)
Instance True_dec: Decision True := left I.
@@ 164,3 +162,7 @@ Instance curry_dec `(P_dec : ∀ (x : A) (y : B), Decision (P x y)) p :
end.
Instance uncurry_dec `(P_dec : ∀ (p : A * B), Decision (P p)) x y :
Decision (uncurry P x y) := P_dec (x,y).
+
+Instance sig_eq_dec `(P : A → Prop) `{∀ x, ProofIrrel (P x)}
+ `{∀ x y : A, Decision (x = y)} (x y : sig P) : Decision (x = y).
+Proof. refine (cast_if (decide (`x = `y))); by rewrite sig_eq_pi. Defined.
diff git a/theories/list.v b/theories/list.v
index f40467c..c817ee5 100644
 a/theories/list.v
+++ b/theories/list.v
@@ 812,6 +812,9 @@ Proof.
revert i.
induction n; intros [?]; naive_solver auto with lia.
Qed.
+Lemma replicate_S n (x : A) :
+ replicate (S n) x = x :: replicate n x.
+Proof. done. Qed.
Lemma replicate_plus n m (x : A) :
replicate (n + m) x = replicate n x ++ replicate m x.
Proof. induction n; simpl; f_equal; auto. Qed.
@@ 829,6 +832,14 @@ Lemma drop_replicate_plus n m (x : A) :
drop n (replicate (n + m) x) = replicate m x.
Proof. rewrite drop_replicate. f_equal. lia. Qed.
+Lemma reverse_replicate n (x : A) :
+ reverse (replicate n x) = replicate n x.
+Proof.
+ induction n as [n IH]; [done].
+ simpl. rewrite reverse_cons, IH. change [x] with (replicate 1 x).
+ by rewrite <replicate_plus, plus_comm.
+Qed.
+
(** ** Properties of the [resize] function *)
Lemma resize_spec (l : list A) n x :
resize n x l = take n l ++ replicate (n  length l) x.
diff git a/theories/numbers.v b/theories/numbers.v
index d08d8c3..2315710 100644
 a/theories/numbers.v
+++ b/theories/numbers.v
@@ 165,12 +165,26 @@ Notation "(<)" := Z.lt (only parsing) : Z_scope.
Infix "`div`" := Z.div (at level 35) : Z_scope.
Infix "`mod`" := Z.modulo (at level 35) : Z_scope.
+Infix "`quot`" := Z.quot (at level 35) : Z_scope.
+Infix "`rem`" := Z.rem (at level 35) : Z_scope.
Instance Z_eq_dec: ∀ x y : Z, Decision (x = y) := Z.eq_dec.
Instance Z_le_dec: ∀ x y : Z, Decision (x ≤ y)%Z := Z_le_dec.
Instance Z_lt_dec: ∀ x y : Z, Decision (x < y)%Z := Z_lt_dec.
Instance Z_inhabited: Inhabited Z := populate 1%Z.
+(* Note that we cannot disable simpl for [Z.of_nat] as that would break
+[omega] and [lia]. *)
+Arguments Z.to_nat _ : simpl never.
+Arguments Z.mul _ _ : simpl never.
+Arguments Z.add _ _ : simpl never.
+Arguments Z.opp _ : simpl never.
+Arguments Z.pow _ _ : simpl never.
+Arguments Z.div _ _ : simpl never.
+Arguments Z.modulo _ _ : simpl never.
+Arguments Z.quot _ _ : simpl never.
+Arguments Z.rem _ _ : simpl never.
+
(** * Notations and properties of [Qc] *)
Notation "2" := (1+1)%Qc : Qc_scope.
Infix "≤" := Qcle : Qc_scope.
diff git a/theories/proof_irrel.v b/theories/proof_irrel.v
new file mode 100644
index 0000000..4a61167
 /dev/null
+++ b/theories/proof_irrel.v
@@ 0,0 +1,41 @@
+(* Copyright (c) 20122013, Robbert Krebbers. *)
+(* This file is distributed under the terms of the BSD license. *)
+(** This file collects facts on proof irrelevant types/propositions. *)
+Require Export Eqdep_dec tactics.
+
+Hint Extern 200 (ProofIrrel _) => progress (lazy beta) : typeclass_instances.
+
+Instance: ProofIrrel True.
+Proof. by intros [] []. Qed.
+Instance: ProofIrrel False.
+Proof. by intros []. Qed.
+
+Instance and_pi (A B : Prop) :
+ ProofIrrel A → ProofIrrel B → ProofIrrel (A ∧ B).
+Proof. intros ?? [??] [??]. by f_equal. Qed.
+Instance prod_pi (A B : Type) :
+ ProofIrrel A → ProofIrrel B → ProofIrrel (A * B).
+Proof. intros ?? [??] [??]. by f_equal. Qed.
+
+Instance eq_pi {A} `{∀ x y : A, Decision (x = y)} (x y : A) :
+ ProofIrrel (x = y).
+Proof.
+ intros ??. apply eq_proofs_unicity.
+ intros x' y'. destruct (decide (x' = y')); tauto.
+Qed.
+
+Instance Is_true_pi (b : bool) : ProofIrrel (Is_true b).
+Proof. destruct b; simpl; apply _. Qed.
+
+Lemma sig_eq_pi `(P : A → Prop) `{∀ x, ProofIrrel (P x)}
+ (x y : sig P) : x = y ↔ `x = `y.
+Proof.
+ split.
+ * destruct x, y. apply proj1_sig_inj.
+ * destruct x as [x Hx], y as [y Hy]; simpl; intros; subst.
+ f_equal. apply proof_irrel.
+Qed.
+
+Lemma exists_proj1_pi `(P : A → Prop) `{∀ x, ProofIrrel (P x)}
+ (x : sig P) p : `x ↾ p = x.
+Proof. by apply (sig_eq_pi _). Qed.

2.24.1