An axiomatization and implementation of machine integers.

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). *)

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 [H|H];
   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.

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.

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.

theories/proof_irrel.v

+(* Copyright (c) 2012-2013, 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.