From 9fdd672472a77a4c65aa1239ad22ebb0efd1e79e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 15 Aug 2024 13:25:27 +0200
Subject: [PATCH] Update code to use new `iInduction` syntax.
---
iris/base_logic/lib/later_credits.v | 2 +-
iris/bi/lib/relations.v | 8 ++++----
iris/program_logic/lifting.v | 2 +-
iris/program_logic/total_adequacy.v | 2 +-
iris/program_logic/total_lifting.v | 2 +-
iris/program_logic/weakestpre.v | 2 +-
iris_heap_lang/derived_laws.v | 2 +-
iris_heap_lang/lib/array.v | 10 +++++-----
iris_heap_lang/primitive_laws.v | 4 ++--
tests/heap_lang.v | 6 +++---
tests/list_reverse.v | 2 +-
tests/proofmode.ref | 10 +++++-----
tests/proofmode.v | 26 +++++++++++++-------------
tests/tree_sum.v | 6 +++---
14 files changed, 42 insertions(+), 42 deletions(-)
diff --git a/iris/base_logic/lib/later_credits.v b/iris/base_logic/lib/later_credits.v
index bcc7f3311..8f08f6c30 100644
--- a/iris/base_logic/lib/later_credits.v
+++ b/iris/base_logic/lib/later_credits.v
@@ -379,7 +379,7 @@ Module le_upd.
iPoseProof (H C) as "Hc". iSpecialize ("Hc" with "Hâ—¯").
iPoseProof (le_upd_elim_complete m with "Hâ— Hc") as "H".
simpl. iMod "H". iModIntro. iNext.
- clear H. iInduction m as [|m] "IH"; simpl; [done|].
+ clear H. iInduction m as [|m IH]; simpl; [done|].
iMod "H". iNext. by iApply "IH".
Qed.
End le_upd.
diff --git a/iris/bi/lib/relations.v b/iris/bi/lib/relations.v
index be4223c72..6724d8719 100644
--- a/iris/bi/lib/relations.v
+++ b/iris/bi/lib/relations.v
@@ -306,7 +306,7 @@ Section general.
Lemma bi_nsteps_trans n m x y z :
bi_nsteps R n x y -∗ bi_nsteps R m y z -∗ bi_nsteps R (n + m) x z.
Proof.
- iInduction n as [|n] "IH" forall (x); simpl.
+ iInduction n as [|n IH] forall (x); simpl.
- iIntros "Heq". iRewrite "Heq". auto.
- iDestruct 1 as (x') "[Hxx' Hx'y]". iIntros "Hyz".
iExists x'. iFrame "Hxx'". iApply ("IH" with "Hx'y Hyz").
@@ -323,7 +323,7 @@ Section general.
Lemma bi_nsteps_add_inv n m x z :
bi_nsteps R (n + m) x z ⊢ ∃ y, bi_nsteps R n x y ∗ bi_nsteps R m y z.
Proof.
- iInduction n as [|n] "IH" forall (x).
+ iInduction n as [|n IH] forall (x).
- iIntros "Hxz". iExists x. auto.
- iDestruct 1 as (y) "[Hxy Hyz]".
iDestruct ("IH" with "Hyz") as (y') "[Hyy' Hy'z]".
@@ -368,7 +368,7 @@ Section general.
iExists (S n). iSplitR; first auto with lia.
iApply (bi_nsteps_l with "Hxx' Hx'y").
- iDestruct 1 as (n ?) "Hxy".
- iInduction n as [|n] "IH" forall (y). { lia. }
+ iInduction n as [|n IH] forall (y). { lia. }
rewrite bi_nsteps_inv_r.
iDestruct "Hxy" as (x') "[Hxx' Hx'y]".
destruct n.
@@ -387,7 +387,7 @@ Section general.
iDestruct "IH" as (n) "Hx'y".
iExists (S n). iApply (bi_nsteps_l with "Hxx' Hx'y").
- iDestruct 1 as (n) "Hxy".
- iInduction n as [|n] "IH" forall (y).
+ iInduction n as [|n IH] forall (y).
{ simpl. iRewrite "Hxy". iApply bi_rtc_refl. }
iDestruct (bi_nsteps_inv_r with "Hxy") as (x') "[Hxx' Hx'y]".
iApply (bi_rtc_r with "[Hxx'] Hx'y").
diff --git a/iris/program_logic/lifting.v b/iris/program_logic/lifting.v
index 5bcd190ea..06018dad0 100644
--- a/iris/program_logic/lifting.v
+++ b/iris/program_logic/lifting.v
@@ -159,7 +159,7 @@ Lemma wp_pure_step_fupd `{!Inhabited (state Λ)} s E E' e1 e2 φ n Φ :
(|={E}[E']▷=>^n £ n -∗ WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
Proof.
iIntros (Hexec Hφ) "Hwp". specialize (Hexec Hφ).
- iInduction Hexec as [e|n e1 e2 e3 [Hsafe ?]] "IH"; simpl.
+ iInduction Hexec as [e|n e1 e2 e3 [Hsafe ?] ? IH]; simpl.
{ iMod lc_zero as "Hz". by iApply "Hwp". }
iApply wp_lift_pure_det_step_no_fork.
- intros σ. specialize (Hsafe σ). destruct s; eauto using reducible_not_val.
diff --git a/iris/program_logic/total_adequacy.v b/iris/program_logic/total_adequacy.v
index 17ce1bda3..526cb85e3 100644
--- a/iris/program_logic/total_adequacy.v
+++ b/iris/program_logic/total_adequacy.v
@@ -98,7 +98,7 @@ Proof.
iMod ("IH" with "[% //]") as "($ & Hσ & [IH _] & IHfork)".
iModIntro. iExists (length efs + nt). iFrame "Hσ".
iApply (twptp_app [_] with "(IH [//])").
- clear. iInduction efs as [|e efs] "IH"; simpl.
+ clear. iInduction efs as [|e efs IH]; simpl.
{ rewrite twptp_unfold /twptp_pre. iIntros (t2 σ1 ns κ κs σ2 nt1 Hstep).
destruct Hstep; simplify_eq/=; discriminate_list. }
iDestruct "IHfork" as "[[IH' _] IHfork]".
diff --git a/iris/program_logic/total_lifting.v b/iris/program_logic/total_lifting.v
index 8502c6240..35353ae8a 100644
--- a/iris/program_logic/total_lifting.v
+++ b/iris/program_logic/total_lifting.v
@@ -82,7 +82,7 @@ Lemma twp_pure_step `{!Inhabited (state Λ)} s E e1 e2 φ n Φ :
WP e2 @ s; E [{ Φ }] ⊢ WP e1 @ s; E [{ Φ }].
Proof.
iIntros (Hexec Hφ) "Hwp". specialize (Hexec Hφ).
- iInduction Hexec as [e|n e1 e2 e3 [Hsafe ?]] "IH"; simpl; first done.
+ iInduction Hexec as [e|n e1 e2 e3 [Hsafe ?] ? IH]; simpl; first done.
iApply twp_lift_pure_det_step_no_fork; [done|naive_solver|].
iModIntro. by iApply "IH".
Qed.
diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index 8e8e796b0..e9623aa7e 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -265,7 +265,7 @@ Proof.
iIntros "!>" (e2 σ2 efs Hstep) "Hcred". iMod ("H" $! e2 σ2 efs with "[% //] Hcred") as "H".
iIntros "!>!>". iMod "H". iMod "HP". iModIntro.
revert n Hn. generalize (num_laters_per_step ns)=>n0 n Hn.
- iInduction n as [|n] "IH" forall (n0 Hn).
+ iInduction n as [|n IH] forall (n0 Hn).
- iApply (step_fupdN_wand with "H"). iIntros ">($ & Hwp & $)". iMod "HP".
iModIntro. iApply (wp_strong_mono with "Hwp"); [done|set_solver|].
iIntros (v) "HΦ". iApply ("HΦ" with "HP").
diff --git a/iris_heap_lang/derived_laws.v b/iris_heap_lang/derived_laws.v
index a57ce3d1c..8f1552a1d 100644
--- a/iris_heap_lang/derived_laws.v
+++ b/iris_heap_lang/derived_laws.v
@@ -96,7 +96,7 @@ Lemma pointsto_seq_array l dq v n :
([∗ list] i ∈ seq 0 n, (l +ₗ (i : nat)) ↦{dq} v) -∗
l ↦∗{dq} replicate n v.
Proof.
- rewrite /array. iInduction n as [|n'] "IH" forall (l); simpl.
+ rewrite /array. iInduction n as [|n' IH] forall (l); simpl.
{ done. }
iIntros "[$ Hl]". rewrite -fmap_S_seq big_sepL_fmap.
setoid_rewrite Nat2Z.inj_succ. setoid_rewrite <-Z.add_1_l.
diff --git a/iris_heap_lang/lib/array.v b/iris_heap_lang/lib/array.v
index 8ed608ab8..99bc65034 100644
--- a/iris_heap_lang/lib/array.v
+++ b/iris_heap_lang/lib/array.v
@@ -57,7 +57,7 @@ Section proof.
[[{ l ↦∗ vs }]] array_free #l #n @ s; E [[{ RET #(); True }]].
Proof.
iIntros (Hlen Φ) "Hl HΦ".
- iInduction vs as [|v vs] "IH" forall (l n Hlen); subst n; wp_rec; wp_pures.
+ iInduction vs as [|v vs IH] forall (l n Hlen); subst n; wp_rec; wp_pures.
{ iApply "HΦ". done. }
iDestruct (array_cons with "Hl") as "[Hv Hl]".
wp_free. wp_pures. iApply ("IH" with "[] Hl"); eauto with lia.
@@ -77,7 +77,7 @@ Section proof.
[[{ RET #(); dst ↦∗ vsrc ∗ src ↦∗{dq} vsrc }]].
Proof.
iIntros (Hvdst Hvsrc Φ) "[Hdst Hsrc] HΦ".
- iInduction vdst as [|v1 vdst] "IH" forall (n dst src vsrc Hvdst Hvsrc);
+ iInduction vdst as [|v1 vdst IH] forall (n dst src vsrc Hvdst Hvsrc);
destruct vsrc as [|v2 vsrc]; simplify_eq/=; try lia; wp_rec; wp_pures.
{ iApply "HΦ". auto with iFrame. }
iDestruct (array_cons with "Hdst") as "[Hv1 Hdst]".
@@ -139,7 +139,7 @@ Section proof.
}}}.
Proof.
iIntros (Hn Φ) "[Hl Hf] HΦ".
- iInduction k as [|k] "IH" forall (i Hn); simplify_eq/=; wp_rec; wp_pures.
+ iInduction k as [|k IH] forall (i Hn); simplify_eq/=; wp_rec; wp_pures.
{ rewrite bool_decide_eq_true_2; last (repeat f_equal; lia).
wp_pures. iApply ("HΦ" $! []). auto. }
rewrite bool_decide_eq_false_2; last naive_solver lia.
@@ -166,7 +166,7 @@ Section proof.
}]].
Proof.
iIntros (Hn Φ) "[Hl Hf] HΦ".
- iInduction k as [|k] "IH" forall (i Hn); simplify_eq/=; wp_rec; wp_pures.
+ iInduction k as [|k IH] forall (i Hn); simplify_eq/=; wp_rec; wp_pures.
{ rewrite bool_decide_eq_true_2; last (repeat f_equal; lia).
wp_pures. iApply ("HΦ" $! []). auto. }
rewrite bool_decide_eq_false_2; last naive_solver lia.
@@ -232,7 +232,7 @@ Section proof.
([∗ list] k↦v ∈ vs, ∃ x, ⌜v = g x⌠∗ Q k x) -∗
∃ xs, ⌜ vs = g <$> xs ⌠∗ [∗ list] k↦x ∈ xs, Q k x.
Proof.
- iIntros "Hvs". iInduction vs as [|v vs] "IH" forall (Q); simpl.
+ iIntros "Hvs". iInduction vs as [|v vs IH] forall (Q); simpl.
{ iExists []. by auto. }
iDestruct "Hvs" as "[(%x & -> & Hv) Hvs]".
iDestruct ("IH" with "Hvs") as (xs ->) "Hxs".
diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index 522bc118c..7ba12c508 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -360,7 +360,7 @@ Lemma heap_array_to_seq_meta l vs (n : nat) :
([∗ map] l' ↦ _ ∈ heap_array l vs, meta_token l' ⊤) -∗
[∗ list] i ∈ seq 0 n, meta_token (l +ₗ (i : nat)) ⊤.
Proof.
- iIntros (<-) "Hvs". iInduction vs as [|v vs] "IH" forall (l)=> //=.
+ iIntros (<-) "Hvs". iInduction vs as [|v vs IH] forall (l)=> //=.
rewrite big_opM_union; last first.
{ apply map_disjoint_spec=> l' v1 v2 /lookup_singleton_Some [-> _].
intros (j&w&?&Hjl&?&?)%heap_array_lookup.
@@ -375,7 +375,7 @@ Lemma heap_array_to_seq_pointsto l v (n : nat) :
([∗ map] l' ↦ ov ∈ heap_array l (replicate n v), gen_heap.pointsto l' (DfracOwn 1) ov) -∗
[∗ list] i ∈ seq 0 n, (l +ₗ (i : nat)) ↦ v.
Proof.
- iIntros "Hvs". iInduction n as [|n] "IH" forall (l); simpl.
+ iIntros "Hvs". iInduction n as [|n IH] forall (l); simpl.
{ done. }
rewrite big_opM_union; last first.
{ apply map_disjoint_spec=> l' v1 v2 /lookup_singleton_Some [-> _].
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index b8d209d82..7271517ac 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -106,7 +106,7 @@ Section tests.
Φ #(n2 - 1) -∗ WP FindPred #n2 #n1 @ E [{ Φ }].
Proof.
iIntros (Hn) "HΦ".
- iInduction (Z.gt_wf n2 n1) as [n1' _] "IH" forall (Hn).
+ iInduction (Z.gt_wf n2 n1) as [n1' _ IH] forall (Hn).
wp_rec. wp_pures. case_bool_decide; wp_if.
- iApply ("IH" with "[%] [%] HΦ"); lia.
- by assert (n1' = n2 - 1)%Z as -> by lia.
@@ -133,12 +133,12 @@ Section tests.
side-condition of the [=] operator. *)
Lemma Id_wp (n : nat) : ⊢ WP Id #n {{ v, ⌜ v = #() ⌠}}.
Proof.
- iInduction n as [|n] "IH"; wp_rec; wp_pures; first done.
+ iInduction n as [|n IH]; wp_rec; wp_pures; first done.
by replace (S n - 1)%Z with (n:Z) by lia.
Qed.
Lemma Id_twp (n : nat) : ⊢ WP Id #n [{ v, ⌜ v = #() ⌠}].
Proof.
- iInduction n as [|n] "IH"; wp_rec; wp_pures; first done.
+ iInduction n as [|n IH]; wp_rec; wp_pures; first done.
by replace (S n - 1)%Z with (n:Z) by lia.
Qed.
diff --git a/tests/list_reverse.v b/tests/list_reverse.v
index 4f98fa490..c3f3abe87 100644
--- a/tests/list_reverse.v
+++ b/tests/list_reverse.v
@@ -34,7 +34,7 @@ Lemma rev_acc_wp hd acc xs ys :
[[{ w, RET w; is_list w (reverse xs ++ ys) }]].
Proof.
iIntros (Φ) "[Hxs Hys] HΦ". Show.
- iInduction xs as [|x xs] "IH" forall (hd acc ys Φ);
+ iInduction xs as [|x xs IH] forall (hd acc ys Φ);
iSimplifyEq; wp_rec; wp_let.
- Show. wp_match. by iApply "HΦ".
- iDestruct "Hxs" as (l hd' ->) "[Hx Hxs]".
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index fb7915240..086a9622a 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -436,15 +436,15 @@ Tactic failure: iCombine: cannot find 'gives' clause for hypotheses
1 goal
PROP : bi
- l, t1 : tree
+ l, r : tree
Φ : tree → PROP
============================
"Hleaf" : Φ leaf
- "Hnode" : ∀ l0 r : tree, Φ l0 -∗ Φ r -∗ Φ (node l0 r)
- "IH" : Φ l
- "IH1" : Φ t1
+ "Hnode" : ∀ l0 r0 : tree, Φ l0 -∗ Φ r0 -∗ Φ (node l0 r0)
+ "IHl" : Φ l
+ "IHr" : Φ r
--------------------------------------â–¡
- Φ (node l t1)
+ Φ (node l r)
The command has indeed failed with message:
Tactic failure: iSpecialize: cannot instantiate (∀ _ : φ, P -∗ False)%I with
P.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index c19cac183..5a72ba424 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -989,14 +989,14 @@ Lemma test_iInduction_wf (x : nat) P Q :
â–¡ P -∗ Q -∗ ⌜ (x + 0 = x)%nat âŒ.
Proof.
iIntros "#HP HQ".
- iInduction (lt_wf x) as [[|x] _] "IH"; simpl; first done.
+ iInduction (lt_wf x) as [[|x] _ IH]; simpl; first done.
rewrite (inj_iff S). by iApply ("IH" with "[%]"); first lia.
Qed.
Lemma test_iInduction_using (m : gmap nat nat) (Φ : nat → nat → PROP) y :
([∗ map] x ↦ i ∈ m, Φ y x) -∗ ([∗ map] x ↦ i ∈ m, emp ∗ Φ y x).
Proof.
- iIntros "Hm". iInduction m as [|i x m] "IH" using map_ind forall(y).
+ iIntros "Hm". iInduction m as [|i x m ? IH] using map_ind forall (y).
- by rewrite !big_sepM_empty.
- rewrite !big_sepM_insert //. iDestruct "Hm" as "[$ ?]".
by iApply "IH".
@@ -1010,7 +1010,7 @@ Lemma test_iInduction_big_sepL_impl' {A} (Φ Ψ : nat → A → PROP) (l1 l2 : l
[∗ list] k↦x ∈ l2, Ψ k x.
Proof.
iIntros (Hlen) "Hl #Himpl".
- iInduction l1 as [|x1 l1] "IH" forall (Φ Ψ l2 Hlen).
+ iInduction l1 as [|x1 l1 IH] forall (Φ Ψ l2 Hlen).
Abort.
Inductive tree := leaf | node (l r: tree).
@@ -1019,10 +1019,10 @@ Check "test_iInduction_multiple_IHs".
Lemma test_iInduction_multiple_IHs (t: tree) (Φ : tree → PROP) :
□ Φ leaf -∗ □ (∀ l r, Φ l -∗ Φ r -∗ Φ (node l r)) -∗ Φ t.
Proof.
- iIntros "#Hleaf #Hnode". iInduction t as [|l r] "IH".
+ iIntros "#Hleaf #Hnode". iInduction t as [|l IHl r IHr].
- iExact "Hleaf".
- - Show. (* should have "IH" and "IH1", since [node] has two trees *)
- iApply ("Hnode" with "IH IH1").
+ - Show. (* should have "IHl" and "IHr", since [node] has two trees *)
+ iApply ("Hnode" with "IHl IHr").
Qed.
Lemma test_iIntros_start_proof :
@@ -1619,11 +1619,11 @@ Lemma test_iInduction_revert_pure (n : nat) (Hn : 0 < n) (P : nat → PROP) :
⊢ P n.
Proof.
(* Check that we consistently get [<affine> _ -∗], not [→] *)
- iInduction n as [|n] "IH" forall (Hn); first lia.
+ iInduction n as [|n IH] forall (Hn); first lia.
Show.
Restart.
Proof.
- iInduction n as [|n] "IH"; first lia.
+ iInduction n as [|n IH]; first lia.
Show.
Abort.
@@ -1632,11 +1632,11 @@ Lemma test_iInduction_revert_pure_affine `{!BiAffine PROP}
(n : nat) (Hn : 0 < n) (P : nat → PROP) : ⊢ P n.
Proof.
(* Check that we consistently get [-∗], not [→]; and no [<affine>] *)
- iInduction n as [|n] "IH" forall (Hn); first lia.
+ iInduction n as [|n IH] forall (Hn); first lia.
Show.
Restart.
Proof.
- iInduction n as [|n] "IH"; first lia.
+ iInduction n as [|n IH]; first lia.
Show.
Abort.
@@ -2054,7 +2054,7 @@ Check "iInduction_wrong_sel_pat".
Lemma iInduction_wrong_sel_pat (n m : nat) (P Q : nat → PROP) :
⌜ n = m ⌠-∗ P n -∗ P m.
Proof.
- Fail iInduction n as [|n] "IH" forall m.
+ Fail iInduction n as [|n IH] forall m.
Abort.
Check "test_iIntros_let_entails_fail".
@@ -2287,7 +2287,7 @@ Section mutual_induction.
□ (∀ l, (∀ x, ⌜ x ∈ l ⌠→ P x) -∗ P (Tree l)) -∗
∀ t, P t.
Proof.
- iIntros "#H" (t). iInduction t as [] "IH".
+ iIntros "#H" (t). iInduction t as [l IH].
Show. (* make sure that the induction hypothesis is exactly what we want *)
iApply "H". iIntros (x ?). by iApply (big_sepL_elem_of with "IH").
Qed.
@@ -2314,7 +2314,7 @@ Section mutual_induction.
∀ t, P t.
Proof.
iIntros "#H" (t).
- Fail iInduction t as [] "IH" using ntree_ind_alt.
+ Fail iInduction t as [l IH] using ntree_ind_alt.
Abort.
End mutual_induction.
diff --git a/tests/tree_sum.v b/tests/tree_sum.v
index b5683256d..c151d1ecf 100644
--- a/tests/tree_sum.v
+++ b/tests/tree_sum.v
@@ -40,13 +40,13 @@ Lemma sum_loop_wp `{!heapGS Σ} v t l (n : Z) :
[[{ RET #(); l ↦ #(sum t + n) ∗ is_tree v t }]].
Proof.
iIntros (Φ) "[Hl Ht] HΦ".
- iInduction t as [n'|tl ? tr] "IH" forall (v l n Φ); simpl; wp_rec; wp_let.
+ iInduction t as [n'|tl IHl tr IHr] forall (v l n Φ); simpl; wp_rec; wp_let.
- iDestruct "Ht" as "%"; subst.
wp_load. wp_store.
by iApply ("HΦ" with "[$Hl]").
- iDestruct "Ht" as (ll lr vl vr ->) "(Hll & Htl & Hlr & Htr)".
- wp_load. wp_apply ("IH" with "Hl Htl"). iIntros "[Hl Htl]".
- wp_load. wp_apply ("IH1" with "Hl Htr"). iIntros "[Hl Htr]".
+ wp_load. wp_apply ("IHl" with "Hl Htl"). iIntros "[Hl Htl]".
+ wp_load. wp_apply ("IHr" with "Hl Htr"). iIntros "[Hl Htr]".
iApply "HΦ". iSplitL "Hl".
{ by replace (sum tl + sum tr + n)%Z with (sum tr + (sum tl + n))%Z by lia. }
iExists ll, lr, vl, vr. by iFrame.
--
GitLab