From c243cbf61639bd1b3560ef9d53b598e8b6573765 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Thu, 1 Dec 2016 17:55:11 +0100
Subject: [PATCH] Coq 8.6 compatibility
---
theories/lang/races.v | 2 +-
theories/lifetime/frac_borrow.v | 2 +-
theories/typing/perm_incl.v | 27 +++++++++++++++++++++------
3 files changed, 23 insertions(+), 8 deletions(-)
diff --git a/theories/lang/races.v b/theories/lang/races.v
index 43916151..5d78a388 100644
--- a/theories/lang/races.v
+++ b/theories/lang/races.v
@@ -201,7 +201,7 @@ Proof.
destruct Ha1 as [[]|[]| | |], Ha2 as [[]|[]| | |]=>//=; simpl in *;
repeat match goal with
- | H : _ = Na1Ord → _ |- _ => specialize (H (reflexivity Na1Ord)) || clear H
+ | H : _ = Na1Ord → _ |- _ => specialize (H (eq_refl Na1Ord)) || clear H
| H : False |- _ => destruct H
| H : ∃ _, _ |- _ => destruct H
end;
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index b77f8b33..0ae322ab 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -84,7 +84,7 @@ Section frac_bor.
{ change (qΦ + qq ≤ 1)%Qc in Hval. apply Qp_eq in HqΦq'. simpl in Hval, HqΦq'.
rewrite <-HqΦq', <-Qcplus_le_mono_l in Hval. apply Qcle_lt_or_eq in Hval.
destruct Hval as [Hval|Hval].
- by left; apply ->Qclt_minus_iff. by right; apply Qp_eq, Qc_is_canon. }
+ by left; apply ->Qclt_minus_iff. right; apply Qp_eq, Qc_is_canon. by rewrite Hval. }
- assert (q' = mk_Qp _ Hq'q + qq)%Qp as ->. { apply Qp_eq. simpl. ring. }
iDestruct "Hq'κ" as "[Hq'qκ Hqκ]".
iMod ("Hclose'" with "[HqΦ HΦqΦ Hown Hq'qκ]") as "Hqκ2".
diff --git a/theories/typing/perm_incl.v b/theories/typing/perm_incl.v
index 4e58a261..5a78834f 100644
--- a/theories/typing/perm_incl.v
+++ b/theories/typing/perm_incl.v
@@ -176,20 +176,35 @@ Section props.
{ apply Qcplus_pos_nonneg. apply Qp_prf. clear. induction ql. done.
apply Qcplus_nonneg_nonneg. apply Qclt_le_weak, Qp_prf. done. }
assert (q = q0 + mk_Qp _ Hpos)%Qp as ->. by by apply Qp_eq; rewrite -Hq.
- injection Hlen; intro Hlen'. rewrite perm_split_own_prod2 IH //.
+ injection Hlen; intro Hlen'. rewrite perm_split_own_prod2 IH //=.
apply perm_sep_proper.
+ rewrite /has_type /sep /=.
destruct (eval_expr ν) as [[[]|]|]; split; iIntros (tid) "_ H/=";
(try by iDestruct "H" as "[]"); (try by iDestruct "H" as (l) "[% _]");
(try by auto); by rewrite shift_loc_0.
- + cut (length tyl = length (q1 :: ql)); last done. clear. revert tyl.
- generalize 0%nat. induction (q1 :: ql)=>offs -[|ty tyl] Hlen //.
+ + (* FIXME RJ: These two 'change' make the goal look like it did in Coq 8.5
+ I found no way to reproduce the magic 8.5 did. *)
+ change ( foldr
+ (λ (qtyoffs : Qp * (type * nat)) (acc : perm),
+ ν +ₗ #(ty_size ty0) +ₗ #((qtyoffs.2).2) ◠own (qtyoffs.1) ((qtyoffs.2).1) ∗ acc)
+ ⊤ (combine (q1 :: ql) (combine_offs tyl 0))
+ ⇔ foldr
+ (λ (qtyoffs : Qp * (type * nat)) (acc : perm), ν +ₗ #((qtyoffs.2).2) ◠own (qtyoffs.1) ((qtyoffs.2).1) ∗ acc)
+ ⊤ (combine (q1 :: ql) (combine_offs tyl (0 + ty_size ty0)))).
+ cut (length tyl = length (q1 :: ql)); last done. clear. revert tyl.
+ generalize 0%nat. induction (q1 :: ql)=>offs -[|ty tyl] Hlen //=.
apply perm_sep_proper.
* rewrite /has_type /sep /=.
destruct (eval_expr ν) as [[[]|]|]; split; iIntros (tid) "_ H/=";
- (try by iDestruct "H" as "[]"); (try by iDestruct "H" as (l) "[% _]");
- (try by auto); by rewrite shift_loc_assoc_nat (comm plus).
- * etransitivity. apply IHl. by injection Hlen. do 3 f_equiv. lia.
+ (try by iDestruct "H" as "[]"); [|]; by rewrite shift_loc_assoc_nat (comm plus).
+ * change ( foldr
+ (λ (qtyoffs : Qp * (type * nat)) (acc : perm),
+ ν +ₗ #(ty_size ty0) +ₗ #((qtyoffs.2).2) ◠own (qtyoffs.1) ((qtyoffs.2).1) ∗ acc)
+ ⊤ (combine l (combine_offs tyl (offs + ty_size ty)))
+ ⇔ foldr
+ (λ (qtyoffs : Qp * (type * nat)) (acc : perm), ν +ₗ #((qtyoffs.2).2) ◠own (qtyoffs.1) ((qtyoffs.2).1) ∗ acc)
+ ⊤ (combine l (combine_offs tyl (offs + ty_size ty0 + ty_size ty)))).
+ etransitivity. apply IHl. by injection Hlen. do 3 f_equiv. lia.
Qed.
Lemma perm_split_uniq_bor_prod2 ty1 ty2 κ ν :
--
GitLab