From 8aa27f29c3498b7cb6732919b2c8f5e67f8cf5a1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 22 Oct 2020 13:07:12 +0200
Subject: [PATCH] fix some cases of relying on unstable/generated names
---
theories/algebra/cmra.v | 2 +-
theories/algebra/cofe_solver.v | 4 ++--
theories/algebra/csum.v | 4 ++--
theories/algebra/frac.v | 2 +-
theories/algebra/gmap.v | 4 ++--
theories/algebra/ufrac.v | 2 +-
theories/base_logic/upred.v | 2 +-
theories/bi/monpred.v | 2 +-
theories/heap_lang/lang.v | 4 +++-
theories/program_logic/ectx_language.v | 4 ++--
theories/program_logic/language.v | 2 +-
11 files changed, 17 insertions(+), 15 deletions(-)
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index b8ea167eb..6afa47b6a 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1493,7 +1493,7 @@ Section option.
Global Instance cancelable_Some a :
IdFree a → Cancelable a → Cancelable (Some a).
Proof.
- intros Hirr ?? [b|] [c|] ? EQ; inversion_clear EQ.
+ intros Hirr ? n [b|] [c|] ? EQ; inversion_clear EQ.
- constructor. by apply (cancelableN a).
- destruct (Hirr b); [|eauto using dist_le with lia].
by eapply (cmra_validN_op_l 0 a b), (cmra_validN_le n); last lia.
diff --git a/theories/algebra/cofe_solver.v b/theories/algebra/cofe_solver.v
index 3fd8fe168..9330d77eb 100644
--- a/theories/algebra/cofe_solver.v
+++ b/theories/algebra/cofe_solver.v
@@ -118,8 +118,8 @@ Proof. by assert (k = j) by lia; subst; rewrite !coerce_id. Qed.
Lemma gg_gg {k i i1 i2 j} : ∀ (H1: k = i + j) (H2: k = i2 + (i1 + j)) (x: A k),
gg i (coerce H1 x) = gg i1 (gg i2 (coerce H2 x)).
Proof.
- intros ? -> x. assert (i = i2 + i1) as -> by lia. revert j x H1.
- induction i2 as [|i2 IH]; intros j X H1; simplify_eq/=;
+ intros Hij -> x. assert (i = i2 + i1) as -> by lia. revert j x Hij.
+ induction i2 as [|i2 IH]; intros j X Hij; simplify_eq/=;
[by rewrite coerce_id|by rewrite g_coerce IH].
Qed.
Lemma ff_ff {k i i1 i2 j} : ∀ (H1: i + k = j) (H2: i1 + (i2 + k) = j) (x: A k),
diff --git a/theories/algebra/csum.v b/theories/algebra/csum.v
index 2089b469b..c418dd97b 100644
--- a/theories/algebra/csum.v
+++ b/theories/algebra/csum.v
@@ -92,8 +92,8 @@ Global Program Instance csum_cofe `{Cofe A, Cofe B} : Cofe csumO :=
Next Obligation.
intros ?? n c; rewrite /compl /csum_compl.
feed inversion (chain_cauchy c 0 n); first auto with lia; constructor.
- + rewrite (conv_compl n (csum_chain_l c a')) /=. destruct (c n); naive_solver.
- + rewrite (conv_compl n (csum_chain_r c b')) /=. destruct (c n); naive_solver.
+ + rewrite (conv_compl n (csum_chain_l c _)) /=. destruct (c n); naive_solver.
+ + rewrite (conv_compl n (csum_chain_r c _)) /=. destruct (c n); naive_solver.
Qed.
Global Instance csum_ofe_discrete :
diff --git a/theories/algebra/frac.v b/theories/algebra/frac.v
index 017254200..1e6da09a8 100644
--- a/theories/algebra/frac.v
+++ b/theories/algebra/frac.v
@@ -44,7 +44,7 @@ Proof.
Qed.
Global Instance frac_cancelable (q : frac) : Cancelable q.
-Proof. intros ?????. by apply Qp_eq, (inj (Qcplus q)), (Qp_eq (q+y) (q+z))%Qp. Qed.
+Proof. intros n y z ??. by apply Qp_eq, (inj (Qcplus q)), (Qp_eq (q+y) (q+z))%Qp. Qed.
Global Instance frac_id_free (q : frac) : IdFree q.
Proof. intros p _. apply Qp_plus_id_free. Qed.
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 37b8f8b61..ed15a0559 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -436,13 +436,13 @@ Section freshness.
pred_infinite I →
✓ x → (∀ i, m !! i = None → I i → Q (<[i:=x]>m)) → m ~~>: Q.
Proof.
- move=> HP ? HQ. eapply alloc_updateP_strong_dep with (f := λ _, x); eauto.
+ move=> HP ? HQ. eapply (alloc_updateP_strong_dep _ _ _ (λ _, x)); eauto.
Qed.
Lemma alloc_updateP (Q : gmap K A → Prop) m x :
✓ x → (∀ i, m !! i = None → Q (<[i:=x]>m)) → m ~~>: Q.
Proof.
move=>??.
- eapply alloc_updateP_strong with (I:=λ _, True);
+ eapply (alloc_updateP_strong _ (λ _, True));
eauto using pred_infinite_True.
Qed.
Lemma alloc_updateP_cofinite (Q : gmap K A → Prop) (J : gset K) m x :
diff --git a/theories/algebra/ufrac.v b/theories/algebra/ufrac.v
index f6b3a44fc..1988da55a 100644
--- a/theories/algebra/ufrac.v
+++ b/theories/algebra/ufrac.v
@@ -32,7 +32,7 @@ Proof. apply discrete_cmra_discrete. Qed.
End ufrac.
Global Instance ufrac_cancelable (q : ufrac) : Cancelable q.
-Proof. intros ?????. by apply Qp_eq, (inj (Qcplus q)), (Qp_eq (q+y) (q+z))%Qp. Qed.
+Proof. intros n y z ??. by apply Qp_eq, (inj (Qcplus q)), (Qp_eq (q+y) (q+z))%Qp. Qed.
Global Instance ufrac_id_free (q : ufrac) : IdFree q.
Proof.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index b3e6fb96c..8b443a61b 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -149,7 +149,7 @@ Section cofe.
Next Obligation.
intros n c; split=>i x Hin Hv.
etrans; [|by symmetry; apply (chain_cauchy c i n)]. split=>H; [by apply H|].
- repeat intro. apply (chain_cauchy c n' i)=>//. by eapply uPred_mono.
+ repeat intro. apply (chain_cauchy c _ i)=>//. by eapply uPred_mono.
Qed.
End cofe.
Arguments uPredO : clear implicits.
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index a81009a0d..d94391caf 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -797,7 +797,7 @@ Qed.
Lemma monPred_at_later i P : (▷ P) i ⊣⊢ ▷ P i.
Proof. by unseal. Qed.
Lemma monPred_at_laterN n i P : (▷^n P) i ⊣⊢ ▷^n P i.
-Proof. induction n; first done. rewrite /= monPred_at_later IHn //. Qed.
+Proof. induction n as [|? IHn]; first done. rewrite /= monPred_at_later IHn //. Qed.
Lemma monPred_at_except_0 i P : (◇ P) i ⊣⊢ ◇ P i.
Proof. by unseal. Qed.
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index d23eabdd2..7d4f4f0b5 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -716,7 +716,9 @@ Proof. revert κ e2. induction Ki; inversion_clear 1; simplify_option_eq; eauto.
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
to_val e1 = None → to_val e2 = None →
fill_item Ki1 e1 = fill_item Ki2 e2 → Ki1 = Ki2.
-Proof. revert Ki1. induction Ki2, Ki1; naive_solver eauto with f_equal. Qed.
+Proof.
+ revert Ki1. induction Ki2; intros Ki1; induction Ki1; naive_solver eauto with f_equal.
+Qed.
Lemma alloc_fresh v n σ :
let l := fresh_locs (dom (gset loc) σ.(heap)) in
diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 774fe60df..ebf94a867 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -249,7 +249,7 @@ Section ectx_language.
prim_step (fill K e1) σ1 κ e2 σ2 efs →
∃ e2', e2 = fill K e2' ∧ head_step e1 σ1 κ e2' σ2 efs.
Proof.
- intros (κ'&e2''&σ2''&efs''&?HhstepK) [K' e1' e2' HKe1 -> Hstep].
+ intros (κ'&e2''&σ2''&efs''&HhstepK) [K' e1' e2' HKe1 -> Hstep].
edestruct (step_by_val K) as [K'' ?];
eauto using val_head_stuck; simplify_eq/=.
rewrite -fill_comp in HKe1; simplify_eq.
@@ -277,7 +277,7 @@ Section ectx_language.
- eauto using fill_not_val.
- intros ?????? [K' e1' e2' Heq1 Heq2 Hstep].
by exists (comp_ectx K K') e1' e2'; rewrite ?Heq1 ?Heq2 ?fill_comp.
- - intros e1 σ1 κ e2 σ2 ? Hnval [K'' e1'' e2'' Heq1 -> Hstep].
+ - intros e1 σ1 κ e2 σ2 efs Hnval [K'' e1'' e2'' Heq1 -> Hstep].
destruct (step_by_val K K'' e1 e1'' σ1 κ e2'' σ2 efs) as [K' ->]; eauto.
rewrite -fill_comp in Heq1; apply (inj (fill _)) in Heq1.
exists (fill K' e2''); rewrite -fill_comp; split; auto.
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index fb982fd7c..603391006 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -310,7 +310,7 @@ Section language.
t2 = <[i:=e']>t1 ++ efs ∧
prim_step e σ1 κ e' σ2 efs).
Proof.
- intros [κ [e σ e' σ' ? t11 t12 ?? Hstep]] Hps; simplify_eq/=.
+ intros [κ [e σ e' σ' efs t11 t12 ?? Hstep]] Hps; simplify_eq/=.
apply Forall2_app_inv_l in Hps
as (t31&?&Hpsteps&(e''&t32&Hps&?&->)%Forall2_cons_inv_l&->).
destruct Hps as [e|e1 e2 e3 [_ Hprs]].
--
GitLab