cleanup

secure-foundations · Sep 14, 2024 · 583efac · 583efac
1 parent 0373e50
commit 583efac
Show file tree

Hide file tree

Showing 9 changed files with 130 additions and 170 deletions.
diff --git a/src/examples/gmap_option.v b/src/examples/gmap_option.v
@@ -29,13 +29,13 @@ Definition gmap_mov (a b: gmap K (option V)) : Prop :=
 Lemma gmap_dot_comm x y
   : gmap_dot x y = gmap_dot y x.
 Proof.
-intros. unfold gmap_dot, gmerge. apply map_eq. intro. rewrite lookup_merge.
+intros. unfold gmap_dot, gmerge. apply map_eq. intro i. rewrite lookup_merge.
     rewrite lookup_merge. unfold diag_None. destruct (x !! i), (y !! i); trivial.
 Qed.
 
 Lemma gmap_dot_assoc x y z
   : gmap_dot x (gmap_dot y z) = gmap_dot (gmap_dot x y) z.
-Proof. intros. unfold gmap_dot, gmerge. apply map_eq. intro. rewrite lookup_merge.
+Proof. intros. unfold gmap_dot, gmerge. apply map_eq. intro i. rewrite lookup_merge.
     rewrite lookup_merge.
     rewrite lookup_merge.
     unfold diag_None.
@@ -47,30 +47,30 @@ Qed.
 Lemma gmap_dot_empty
   : ∀ x : gmap K (option V), gmap_dot x ∅ = x.
 Proof.
-intros. unfold gmap_dot. apply map_eq. intro. rewrite lookup_merge. rewrite lookup_empty.
+intros x. unfold gmap_dot. apply map_eq. intro i. rewrite lookup_merge. rewrite lookup_empty.
     unfold diag_None, gmerge. destruct (x !! i); trivial.
 Qed.
 
 Lemma gmap_dot_empty_left
   : ∀ x : gmap K (option V), gmap_dot ∅ x = x.
 Proof.
-intros. unfold gmap_dot. apply map_eq. intro. rewrite lookup_merge. rewrite lookup_empty.
+intros x. unfold gmap_dot. apply map_eq. intro i. rewrite lookup_merge. rewrite lookup_empty.
     unfold diag_None, gmerge. destruct (x !! i); trivial.
 Qed.
 
 Lemma lookup_gmap_dot_left a b k
   : gmap_valid (gmap_dot a b) -> (a !! k ≠ None) -> (gmap_dot a b) !! k = a !! k.
 Proof.
-  unfold gmap_valid, gmap_dot. intros.
-  have j := H k. rewrite lookup_merge.
+  unfold gmap_valid, gmap_dot. intros Q R.
+  have j := Q k. rewrite lookup_merge.
   rewrite lookup_merge in j. unfold diag_None, gmerge in *. destruct (a !! k), (b !! k);
   trivial; contradiction.
 Qed.
 
 Lemma lookup_gmap_dot_right a b k
   : gmap_valid (gmap_dot a b) -> (b !! k ≠ None) -> (gmap_dot a b) !! k = b !! k.
 Proof.
-  unfold gmap_valid, gmap_dot. intros. have j := H k. rewrite lookup_merge.
+  unfold gmap_valid, gmap_dot. intros Q R. have j := Q k. rewrite lookup_merge.
   rewrite lookup_merge in j. unfold diag_None, gmerge in *. destruct (a !! k), (b !! k);
   trivial; contradiction.
 Qed.
@@ -79,9 +79,9 @@ Lemma lookup_gmap_dot_3mid a b c k
   : gmap_valid (gmap_dot (gmap_dot a b) c) -> (b !! k ≠ None) ->
       gmap_dot (gmap_dot a b) c !! k = b !! k.
 Proof.
-  intros.
-  rewrite gmap_dot_comm in H.
-  rewrite gmap_dot_assoc in H.
+  intros Q R.
+  rewrite gmap_dot_comm in Q.
+  rewrite gmap_dot_assoc in Q.
   rewrite gmap_dot_comm.
   rewrite gmap_dot_assoc.
   apply lookup_gmap_dot_right; trivial.
@@ -91,8 +91,8 @@ Lemma lookup_gmap_dot_3left a b c k
   : gmap_valid (gmap_dot (gmap_dot a b) c) -> (a !! k ≠ None) ->
       gmap_dot (gmap_dot a b) c !! k = a !! k.
 Proof.
-  intros.
-  rewrite <- gmap_dot_assoc in H.
+  intros Q R.
+  rewrite <- gmap_dot_assoc in Q.
   rewrite <- gmap_dot_assoc.
   apply lookup_gmap_dot_left; trivial.
 Qed.
@@ -107,8 +107,8 @@ Qed.
 Lemma gmap_valid_left
   : ∀ x y : gmap K (option V), gmap_valid (gmap_dot x y) → gmap_valid x.
 Proof.
-  intros. unfold gmap_valid, gmap_dot in *.
-    intro. have h := H k. clear H. rewrite lookup_merge in h. unfold diag_None in h.
+  intros x y. unfold gmap_valid, gmap_dot in *.
+    intros Q k. have h := Q k. clear Q. rewrite lookup_merge in h. unfold diag_None in h.
         unfold gmerge in h.
         destruct (x !! k); trivial.
         destruct (y !! k); trivial. contradiction.
@@ -124,8 +124,8 @@ Lemma gmap_valid_update_singleton j x y (m: gmap K (option V)) :
   gmap_valid (gmap_dot {[j := Some x]} m) ->
   gmap_valid (gmap_dot {[j := Some y]} m).
 Proof.
-  intros. unfold gmap_valid, gmap_dot in *. intro.
-  have r := H k. rewrite lookup_merge. rewrite lookup_merge in r.
+  intros Q. unfold gmap_valid, gmap_dot in *. intro k.
+  have r := Q k. rewrite lookup_merge. rewrite lookup_merge in r.
   unfold gmerge, diag_None in *.
   have h : Decision (j = k) by solve_decision. destruct h.
   - subst k. rewrite lookup_singleton. rewrite lookup_singleton in r.
@@ -134,30 +134,6 @@ Proof.
     rewrite lookup_singleton_ne in r; trivial.
 Qed.
 
- (*
-#[refine]
-Global Instance gmap_tpcm : TPCM (gmap K (option V)) := {
-  m_valid p := gmap_valid p ;
-  dot a b := gmap_dot a b ;
-  mov a b := gmap_mov a b ;
-  unit := empty ;
-}.
- - apply gmap_valid_left.
- - unfold gmap_valid. intros. rewrite lookup_empty. trivial.
- - apply gmap_dot_empty.
- - intros. apply gmap_dot_comm.
- - intros. apply gmap_dot_assoc.
-  - intros. unfold gmap_mov. intro. trivial.
-  - intros. unfold gmap_mov in *. intros. apply H0. apply H. trivial.
-  - intros. split.
-    * unfold gmap_mov in H. apply H. apply H0.
-    * unfold gmap_mov in H. unfold gmap_mov. intro.
-        rewrite <- gmap_dot_assoc.
-        rewrite <- gmap_dot_assoc.
-        apply H.
-Defined.
-*)
-
 Definition gmap_le (a b : gmap K (option V)) := ∃ c , gmap_dot a c = b.
 
 Lemma le_of_subset (a b : gmap K (option V))
@@ -166,19 +142,19 @@ Proof.
   assert (∀ x : K * option V, Decision (match x with (k,v) => a !! k = None end)) as X
     by solve_decision.
   exists (map_filter (λ x , match x with (k,v) => a !! k = None end) X b).
-  unfold gmap_dot. apply map_eq. intro.
+  unfold gmap_dot. apply map_eq. intro i.
   have ff := f i.
   rewrite lookup_merge. unfold diag_None, gmerge. 
-  destruct (a !! i) eqn:ai.
+  destruct (a !! i) as [o|] eqn:ai.
   - rewrite map_lookup_filter.
-    unfold "≫=", option_bind. destruct (b!!i) eqn:bi.
-    + unfold guard. have fff := ff o. intuition. inversion H.
+    unfold "≫=", option_bind. destruct (b!!i) as [o0|] eqn:bi.
+    + unfold guard. have fff := ff o. have ffff := fff eq_refl. inversion ffff. subst o0.
       destruct (X (i, o)) as [e|e].
       * rewrite e in ai. discriminate.
       * trivial.
     + have fff := ff o. intuition.
   - rewrite map_lookup_filter.
-    unfold "≫=", option_bind. destruct (b!!i) eqn:bi; trivial.
+    unfold "≫=", option_bind. destruct (b!!i) as [o|] eqn:bi; trivial.
     destruct (X (i, o)); trivial.
     contradiction.
 Qed.
@@ -194,7 +170,7 @@ Lemma conjunct_and_gmap
 Proof.
   apply le_of_subset. intros k v e1.
   unfold gmap_dot in e1. rewrite lookup_merge in e1. unfold diag_None in e1.
-  destruct (a1 !! k) eqn:a1k; destruct (a2 !! k) eqn:a2k.
+  destruct (a1 !! k) as [o|] eqn:a1k; destruct (a2 !! k) as [o0|] eqn:a2k.
   - have l := a_disj _ _ _ a1k a2k. contradiction.
   - unfold gmerge in e1. inversion e1. subst o. unfold gmap_le in la1.
       destruct la1 as [d la]. subst c.
@@ -204,7 +180,7 @@ Proof.
       have gvk := gv k.
       rewrite lookup_merge in gvk. rewrite a1k in gvk. unfold diag_None in gvk.
       unfold gmerge. unfold gmerge in gvk. destruct (d !! k); trivial. contradiction.
-  - unfold gmerge in e1. inversion e1. subst o. unfold gmap_le in la2.
+  - unfold gmerge in e1. inversion e1. subst o0. unfold gmap_le in la2.
       destruct la2 as [d la]. subst c.
       unfold gmap_dot.
       unfold gmap_valid in gv. unfold gmap_dot in gv.

diff --git a/src/examples/hash_table_raw.v b/src/examples/hash_table_raw.v
@@ -88,7 +88,7 @@ Definition m (k: Key) (v: option Value) :=
 Lemma ht_valid_QueryFound j k v v0
   : V (ht_dot (s j (Some (k, v0))) (m k v)) -> v = Some v0.
 Proof.
-  unfold V, s, m. intros [z H]. destruct z. unfold ht_dot in *. unfold P in *.
+  unfold V, s, m. intros [z H]. destruct z as [ms slots]. unfold ht_dot in *. unfold P in *.
   repeat (rewrite gmap_dot_empty in H).
   repeat (rewrite gmap_dot_empty_left in H).
   destruct H as [H [H0 [H1 [H2 [H3 H4]]]]].
@@ -122,7 +122,7 @@ Lemma ht_valid_QueryReachedEnd k a v
   (is_full: full a k (hash k) ht_fixed_size)
   : V (ht_dot a (m k v)) -> v = None.
 Proof.
-  unfold V, s, m. intros [z H]. destruct z, a. unfold ht_dot in *. unfold P in *.
+  unfold V, s, m. intros [z H]. destruct z as [ms slots], a as [ms0 slots0]. unfold ht_dot in *. unfold P in *.
   unfold full in is_full.
   destruct H as [H [H0 [H1 [H2 [H3 H4]]]]].
   destruct is_full as [H5 [H6 [H7 H8]]].
@@ -139,7 +139,7 @@ Proof.
   repeat (rewrite gmap_dot_empty_left in H3).
   repeat (rewrite gmap_dot_empty in H4).
   repeat (rewrite gmap_dot_empty_left in H4).
-  destruct v; trivial. exfalso.
+  destruct v as [v|]; trivial. exfalso.
   have h := H3 k v.
   assert (gmap_dot {[k := Some (Some v)]} ms !! k = Some (Some (Some v))) as Q.
   {
@@ -167,7 +167,7 @@ Lemma ht_valid_QueryNotFound k a v j
   (is_full: full a k (hash k) j)
   : V (ht_dot (ht_dot a (m k v)) (s j None)) -> v = None.
 Proof.
-  unfold V, s, m. intros [z H]. destruct z, a. unfold ht_dot in *. unfold P in *.
+  unfold V, s, m. intros [z H]. destruct z as [ms slots], a as [ms0 slots0]. unfold ht_dot in *. unfold P in *.
   unfold full in is_full.
   destruct H as [H [H0 [H1 [H2 [H3 H4]]]]].
   destruct is_full as [H5 [H6 [H7 H8]]].
@@ -184,7 +184,7 @@ Proof.
   repeat (rewrite gmap_dot_empty_left in H3).
   repeat (rewrite gmap_dot_empty in H4).
   repeat (rewrite gmap_dot_empty_left in H4).
-  destruct v; trivial. exfalso.
+  destruct v as [v|]; trivial. exfalso.
   have h := H3 k v.
   assert (gmap_dot {[k := Some (Some v)]} ms !! k = Some (Some (Some v))) as Q.
   {
@@ -200,8 +200,8 @@ Proof.
   assert (i < j) as ihfs.
   {
     have hij : Decision (i < j) by solve_decision. destruct hij; trivial.
-    assert (j ≤ i) by lia.
-    have mm := H10 j H5 H11. destruct mm as [k1 [v1 mm]].
+    assert (j ≤ i) as Hle by lia.
+    have mm := H10 j H5 Hle. destruct mm as [k1 [v1 mm]].
     rewrite lookup_gmap_dot_3mid in mm.
     - rewrite lookup_singleton in mm. inversion mm.
     - trivial.
@@ -220,19 +220,19 @@ Lemma preserves_lt_fixed_size j a b slots
   : ∀ (i : nat) (e : option (option (Key * Value))),
     gmap_dot {[j := Some b]} slots !! i = Some e → i < ht_fixed_size.
 Proof.
-  intros.
+  intros i e Heq.
   (*have h : Decision (i = j) by solve_decision. destruct h.*)
-  destruct (gmap_dot {[j := Some a]} slots !! i) eqn:gd.
+  destruct (gmap_dot {[j := Some a]} slots !! i) as [o|] eqn:gd.
   - exact (ltfs i o gd).
-  - exfalso. unfold gmap_dot in H, gd.
-      rewrite lookup_merge in H.
+  - exfalso. unfold gmap_dot in Heq, gd.
+      rewrite lookup_merge in Heq.
       rewrite lookup_merge in gd.
       unfold diag_None, gmerge in *.
       have h : Decision (j = i) by solve_decision. destruct h.
       + subst j.
-        rewrite lookup_singleton in H.
+        rewrite lookup_singleton in Heq.
         rewrite lookup_singleton in gd. destruct (slots !! i); discriminate.
-      + rewrite lookup_singleton_ne in H; trivial.
+      + rewrite lookup_singleton_ne in Heq; trivial.
         rewrite lookup_singleton_ne in gd; trivial.
         destruct (slots !! i); discriminate.
 Qed.
@@ -296,8 +296,7 @@ Lemma preserves_unique_keys j k v v1 slots
     ∧ gmap_dot {[j := Some (Some (k, v))]} slots !! i2 = Some (Some (Some (k0, v3)))
     → i1 = i2.
 Proof.
-  intros.
-  destruct H as [H H0].
+  intros i1 i2 k0 v2 v3 [H H0].
   have ed : Decision (i1 = j) by solve_decision. destruct ed.
     - have ed : Decision (i2 = j) by solve_decision. destruct ed.
       + subst. trivial.
@@ -344,8 +343,8 @@ Proof.
     rewrite lookup_singleton in ac.
     destruct (slots !! j), (slots0 !! j); discriminate.
   - rewrite lookup_singleton_ne in ac; trivial.
-    destruct (slots !! i2), (slots0 !! i2); try inversion ac; try discriminate.
-    + subst o. inversion zz. inversion zz. subst k. contradiction.
+    destruct (slots !! i2) as [a1|], (slots0 !! i2) as [b1|]; try inversion ac; try discriminate.
+    + subst b1. inversion zz. inversion zz. subst k. contradiction.
 Qed.
 
 Lemma pukn_helper j k0 k v v1 slots v0 ms ms0 slots0 i2 v2

diff --git a/src/guarding/internal/auth_frag_util.v b/src/guarding/internal/auth_frag_util.v
@@ -1,9 +1,7 @@
+From iris.prelude Require Import options.
 From iris.algebra Require Export cmra updates.
 From iris.algebra Require Import proofmode_classes.
 From iris.algebra Require Import auth.
-From iris.algebra Require Import functions.
-From iris.algebra Require Import gmap.
-From iris.prelude Require Import options.
 
 From iris.base_logic Require Import upred.
 From iris.base_logic.lib Require Export own iprop.
@@ -12,8 +10,6 @@ From iris.proofmode Require Import ltac_tactics.
 From iris.proofmode Require Import tactics.
 From iris.proofmode Require Import coq_tactics.
 
-From stdpp Require Import numbers.
-
 Require Import guarding.own_and.
 
 Section AuthFragUtil.
@@ -25,9 +21,9 @@ Context `{Disc : CmraDiscrete C}.
 
 Lemma auth_op_rhs_is_frag (p: C) z (val : ✓ (● p ⋅ z)) : ∃ q , z = ◯ q.
 Proof.
-  destruct z. exists view_frag_proj. rename view_frag_proj into f.
+  destruct z as [a f]. exists f.
   unfold "◯", "◯V". f_equal.
-  destruct view_auth_proj; trivial.
+  destruct a as [p0|]; trivial.
   exfalso.
   unfold "●", "●V" in val.
 
@@ -42,7 +38,7 @@ Proof.
 
   rewrite /op /view_op_instance /view_auth_proj /view_frag_proj in val2.
   rewrite /valid /view_valid_instance /view_auth_proj in val2.
-  destruct p0.
+  destruct p0 as [d a].
   assert (Some (DfracOwn 1, to_agree p) ⋅ Some (d, a)
       = Some (DfracOwn 1 ⋅ d, to_agree p ⋅ a)) as Q.
     { trivial. }
@@ -66,8 +62,8 @@ Lemma rhs_has_auth (x y : C) (q1 q2: auth C)
 Proof.
   have ao := auth_op_rhs_is_frag x q1 v.
   destruct ao as [q ao]. subst q1.
-  destruct q2.
-  exists (◯ view_frag_proj).
+  destruct q2 as [a f].
+  exists (◯ f).
   unfold "●", "●V", "◯", "◯V".
 
   rewrite view_op_rw.
@@ -78,10 +74,10 @@ Proof.
     rewrite view_op_rw in eq.
     rewrite view_op_rw in eq.
 
-    inversion eq.
-    unfold view.view_auth_proj in H.
-    setoid_rewrite H.
-    + destruct view_auth_proj; trivial.
+    inversion eq as [Q R].
+    unfold view.view_auth_proj in Q.
+    setoid_rewrite Q.
+    + destruct a; trivial.
   - rewrite left_id. trivial.
 Qed.
 
@@ -258,11 +254,7 @@ Qed.
 Lemma auth_frag_disjointness_helper (q r : C) (a b : auth C)
   (eq1 : ◯ q ⋅ a ≡ ● r ⋅ b) : ◯ q ≼ b.
 Proof.
-  destruct a, b.
-  rename view_frag_proj into f.
-  rename view_auth_proj into g.
-  rename view_frag_proj0 into f0.
-  rename view_auth_proj0 into g0.
+  destruct a as [g f], b as [g0 f0].
   unfold "◯", "◯V" in eq1.
   unfold "●", "●V" in eq1.
   unfold "◯", "◯V".
@@ -273,9 +265,9 @@ Proof.
   replace (@View C C (@auth_view_rel C) (Some (DfracOwn 1, to_agree r)) ε ⋅ @View C C (@auth_view_rel C) g0 f0)
     with (@View C C (@auth_view_rel C) (Some (DfracOwn 1, to_agree r) ⋅ g0) (ε ⋅ f0)) in eq1 by trivial.
 
-  inversion eq1.
-  unfold view_frag_proj in H0.
-  generalize H0.
+  inversion eq1 as [Q R].
+  unfold view_frag_proj in R.
+  generalize R.
   rewrite ucmra_unit_left_id.
   intro X.
 

diff --git a/src/guarding/internal/wsat_util.v b/src/guarding/internal/wsat_util.v
@@ -1,10 +1,9 @@
-From stdpp Require Export coPset.
+From iris.prelude Require Import options.
 From iris.algebra Require Import gmap_view gset coPset.
 From iris.proofmode Require Import proofmode.
-From iris.base_logic.lib Require Export own.
-From iris.base_logic.lib Require Export wsat.
-From iris.prelude Require Import options.
+From iris.base_logic.lib Require Export own wsat.
 Import uPred.
+From stdpp Require Export coPset.
 From iris.algebra Require Import functions.
 
 Section wsat_util.
@@ -212,7 +211,7 @@ Lemma own_updateP_extra `{i : !inG Σ A} `{j : !inG Σ B} (P : A → gname → P
     (∀ (n : nat) (mz : option A) (N : gname → Prop) , ✓{n} (a ⋅? mz) → pred_finite N → ∃ (y: A) (γ': gname), P y γ' ∧ ✓{n} (y ⋅? mz) ∧ ¬ N γ') →
     (✓ b) →
     own γ a ⊢ |==> ∃ a' γ', ⌜P a' γ'⌝ ∗ own γ a' ∗ own γ' b.
-Proof using H Σ.
+Proof.
   intros Hupd Hvalb. rewrite !own.own_eq.
   rewrite -(bupd_mono (∃ m,
     ⌜ ∃ a' γ', m = (own.iRes_singleton γ a' ⋅ own.iRes_singleton γ' b) ∧ P a' γ' ⌝ ∧ uPred_ownM m)%I).