Fix to compile with Coq 8.12

logsem · Jul 29, 2020 · 49c96b4 · 49c96b4
1 parent 52e6c1c
commit 49c96b4
Show file tree

Hide file tree

Showing 6 changed files with 16 additions and 22 deletions.
diff --git a/opam b/opam
@@ -4,7 +4,7 @@ opam-version: "2.0"
 maintainer: ""
 authors: [ "anonymous" ]
 depends: [
-  "ocaml-base-compiler" {= "4.08.1"}
-  "coq" {= "8.9.1"}
-  "coq-iris" {= "3.2.0"}
+  "ocaml-base-compiler" {= "4.10.0"}
+  "coq" {= "8.12.0"}
+  "coq-iris" {= "3.3.0"}
 ]
diff --git a/theories/examples/awkward_example_adequacy.v b/theories/examples/awkward_example_adequacy.v
@@ -235,11 +235,11 @@ Section Adequacy.
     k ∈ dom (gset Addr) (mkregion a e l) →
     k ∈ region_addrs a e.
   Proof.
-    intros H.
+    intros H. eapply (@elem_of_list_to_set _ (gset Addr)); auto.
+    typeclasses eauto.
     pose proof (dom_mkregion_incl a e l) as HH.
     rewrite elem_of_subseteq in HH |- * => HH.
-    specialize (HH _ H). eapply elem_of_list_to_set; eauto.
-    Unshelve. apply _.
+    specialize (HH _ H). auto.
   Qed.
 
   Lemma in_dom_mkregion' a e l k:

diff --git a/theories/examples/contiguous.v b/theories/examples/contiguous.v
@@ -215,7 +215,7 @@ Section Contiguous.
      first inversion Hfirst.
     simpl in Hfirst. inversion Hfirst. subst.
     destruct al as [| hd tl ].
-    - inversion Hlast. omega.
+    - inversion Hlast. lia.
     - assert ((a0' :: hd :: tl) !! 0 = Some a0') as Ha0; auto.
       assert ((a0' :: hd :: tl) !! 1 = Some hd) as Ha; auto.
       apply (contiguous_spec _ Hcond) with 0 a0' hd in Ha0 as Hnext; auto.
@@ -237,7 +237,7 @@ Section Contiguous.
     - intros i' Hlen Hlast. inversion Hlast.
     - intros i' Hlen Hlast. destruct i'.
       + simpl. apply Hlast.
-      + simpl; simpl in Hlen. apply IHl; first omega.
+      + simpl; simpl in Hlen. apply IHl; first lia.
         assert (0 < length l) as Hl; first lia.
         destruct l; simpl in Hl; first by apply Nat.lt_irrefl in Hl. auto.
   Qed.

diff --git a/theories/ftlr/StoreU.v b/theories/ftlr/StoreU.v
@@ -604,11 +604,11 @@ Section fundamental.
                     - simpl. iDestruct "Hwdst" as "[YA YB]".
                       destruct (proj1 (verify_access_spec _ _) H7) as (A & B & C & D).
                       iDestruct (extract_from_region_inv with "YB") as (pp ?) "[E %]"; auto.
-                      split; try solve_addr. rewrite /addr_reg.max; destruct (Addr_le_dec b0 a); solve_addr.
+                      split; try solve_addr.
                     - simpl. iDestruct "Hwdst" as "[YA YC]".
                       destruct (proj1 (verify_access_spec _ _) H7) as (A & B & C & D).
                       iDestruct (extract_from_region_inv with "YC") as (pp ?) "[E %]"; auto.
-                      split; try solve_addr. rewrite /addr_reg.max; destruct (Addr_le_dec b0 a); solve_addr. }
+                      split; try solve_addr. }
                   destruct Hρ as [Hρ | Hρ]; rewrite Hregion in Hρ; inversion Hρ; try subst ρ; congruence.
                 * assert (HpwlU2: pwlU p' = true).
                   { destruct p0; simpl in H6; simpl in HwplU; try congruence; destruct p'; rewrite /PermFlows in H; inv H; simpl in H0; try congruence; reflexivity. }
@@ -834,14 +834,10 @@ Section fundamental.
                         destruct (proj1 (verify_access_spec _ _) H7) as (A & B & C & D).
                         iDestruct (extract_from_region_inv _ _ a with "YA") as (pp ?) "[E %]"; auto.
                         split; try solve_addr. rewrite /addr_reg.min; destruct (Addr_le_dec a0 e0); solve_addr.
-                        iPureIntro. rewrite /region_state_U_pwl.
-                        rewrite /region_state_pwl in H6; auto.
                       - simpl. iDestruct "Hwdst" as "[YA YB]".
                         destruct (proj1 (verify_access_spec _ _) H7) as (A & B & C & D).
                         iDestruct (extract_from_region_inv _ _ a with "YA") as (pp ?) "[E %]"; auto.
-                        split; try solve_addr. rewrite /addr_reg.min; destruct (Addr_le_dec a0 e0); solve_addr.
-                        iPureIntro. rewrite /region_state_U_pwl.
-                        rewrite /region_state_pwl in H6; auto. }
+                        split; try solve_addr. rewrite /addr_reg.min; destruct (Addr_le_dec a0 e0); solve_addr. }
                     destruct Hρ as [Hρ | Hρ]; rewrite Hregion in Hρ; inversion Hρ; try subst ρ; congruence.
                   * assert (HpwlU2: pwlU p' = true).
                     { destruct p0; simpl in H5; simpl in HwplU; try congruence; destruct p'; rewrite /PermFlows in H; inv H; simpl in H0; try congruence; reflexivity. }
@@ -880,13 +876,11 @@ Section fundamental.
                     - simpl. iDestruct "Hwdst" as "[YA YB]".
                       destruct (proj1 (verify_access_spec _ _) H7) as (A & B & C & D).
                       iDestruct (extract_from_region_inv b0 _ a' with "YA") as (pp ?) "[E %]"; auto.
-                      split; try solve_addr. rewrite /addr_reg.min; destruct (Addr_le_dec a0 e0); solve_addr.
-                      iPureIntro. left; auto.
+                      split; try solve_addr. iPureIntro. left; auto.
                     - simpl. iDestruct "Hwdst" as "[YA YC]".
                       destruct (proj1 (verify_access_spec _ _) H7) as (A & B & C & D).
                       iDestruct (extract_from_region_inv b0 _ a' with "YA") as (pp ?) "[E %]"; auto.
-                      split; try solve_addr. rewrite /addr_reg.min; destruct (Addr_le_dec a0 e0); solve_addr.
-                      iPureIntro. left; auto. }
+                      split; try solve_addr. iPureIntro. left; auto. }
                   destruct Hρ as [Hρ | Hρ]; rewrite H8 in Hρ; inversion Hρ; try subst ρ'; congruence.
                 * assert (HpwlU2: pwlU p'0 = true).
                   { destruct p0; simpl in H5; simpl in HwplU; try congruence; destruct p'0; rewrite /PermFlows in H; inv H; simpl in H0; try congruence; reflexivity. }

diff --git a/theories/fundamental.v b/theories/fundamental.v
@@ -63,7 +63,7 @@ Section fundamental.
     - (* Correct PC *)
       assert ((b <= a)%a ∧ (a < e)%a) as Hbae.
       { eapply in_range_is_correctPC; eauto.
-        unfold le_addr; omega. }
+        unfold le_addr; lia. }
       iDestruct (extract_from_region_inv _ _ a with "Hinv") as (p' Hfp) "(Hinva & Hstate_a)"; auto.
       iDestruct "Hstate_a" as %Hstate_a.
       assert (∃ (ρ : region_type), (std W) !! a = Some ρ ∧ ρ ≠ Revoked ∧ (∀ g, ρ ≠ Static g))

diff --git a/theories/region.v b/theories/region.v
@@ -75,7 +75,7 @@ Section region.
   Proof.
     revert b k. induction n; intros.
     - lia.
-    - assert (X: k = n \/ k < n) by omega; destruct X as [X | X].
+    - assert (X: k = n \/ k < n) by lia; destruct X as [X | X].
       + subst k. destruct n; simpl.
         * f_equal. solve_addr.
         * rewrite IHn; [| lia]. f_equal. solve_addr.
@@ -96,7 +96,7 @@ Section region.
      - simpl. apply not_elem_of_cons; split.
        + intro. apply Hne. solve_addr.
        + rewrite get_addrs_from_option_addr_comm.
-         apply IHn; omega. omega. omega. 
+         apply IHn; lia. lia. lia. 
    Qed.
 
    Lemma region_addrs_not_elem_of a n :