From 49c96b4f348ece5cf7b84a5e4d5b0825cc1df9cb Mon Sep 17 00:00:00 2001 From: Alix Trieu Date: Wed, 29 Jul 2020 15:57:19 +0200 Subject: [PATCH] Fix to compile with Coq 8.12 --- opam | 6 +++--- theories/examples/awkward_example_adequacy.v | 6 +++--- theories/examples/contiguous.v | 4 ++-- theories/ftlr/StoreU.v | 16 +++++----------- theories/fundamental.v | 2 +- theories/region.v | 4 ++-- 6 files changed, 16 insertions(+), 22 deletions(-) diff --git a/opam b/opam index 3233f98..7cd0d22 100644 --- 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 index 2aba07b..76aa2ee 100644 --- 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 index e26c486..8b961c0 100644 --- 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 index dea7209..c737b82 100644 --- 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 index 6075d43..624ae98 100644 --- 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 index a07163e..eebe31a 100644 --- 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 :