From 89f354f036e13725aac6ce969c729a04101daf03 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Thu, 16 Jun 2016 17:24:53 +0200 Subject: [PATCH] Introduce iDestruct num tactic. This introduces n hypotheses and destructs the nth one. --- heap_lang/lib/barrier/proof.v | 2 +- heap_lang/lib/lock.v | 4 +- program_logic/auth.v | 2 +- program_logic/boxes.v | 7 +-- program_logic/invariants.v | 2 +- program_logic/sts.v | 2 +- proofmode/tactics.v | 112 +++++++++++++++++++--------------- tests/barrier_client.v | 4 +- tests/joining_existentials.v | 4 +- 9 files changed, 74 insertions(+), 65 deletions(-) diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v index 31ab9d3f..fad80b68 100644 --- a/heap_lang/lib/barrier/proof.v +++ b/heap_lang/lib/barrier/proof.v @@ -171,7 +171,7 @@ Lemma recv_split E l P1 P2 : nclose N ⊆ E → recv l (P1 ★ P2) ={E}=> recv l P1 ★ recv l P2. Proof. rename P1 into R1; rename P2 into R2. rewrite {1}/recv /barrier_ctx. - iIntros {?} "Hr"; iDestruct "Hr" as {γ P Q i} "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)". + iIntros {?}. iDestruct 1 as {γ P Q i} "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)". iApply pvs_trans'. iSts γ as [p I]; iDestruct "Hγ" as "[Hl Hr]". iPvs (saved_prop_alloc_strong _ (R1: ∙%CF iProp) I) as {i1} "[% #Hi1]". diff --git a/heap_lang/lib/lock.v b/heap_lang/lib/lock.v index eb11bbb5..3d880164 100644 --- a/heap_lang/lib/lock.v +++ b/heap_lang/lib/lock.v @@ -44,9 +44,7 @@ Global Instance is_lock_persistent l R : PersistentP (is_lock l R). Proof. apply _. Qed. Lemma locked_is_lock l R : locked l R ⊢ is_lock l R. -Proof. - rewrite /is_lock. iIntros "Hl"; iDestruct "Hl" as {N γ} "(?&?&?&_)". eauto. -Qed. +Proof. rewrite /is_lock. iDestruct 1 as {N γ} "(?&?&?&_)"; eauto. Qed. Lemma newlock_spec N (R : iProp) Φ : heapN ⊥ N → diff --git a/program_logic/auth.v b/program_logic/auth.v index b53bcacb..6f966d98 100644 --- a/program_logic/auth.v +++ b/program_logic/auth.v @@ -101,7 +101,7 @@ Section auth. rewrite ->(left_id _ _) in Ha'; setoid_subst. iApply pvs_fsa_fsa; iApply fsa_wand_r; iSplitL "HΨ Hφ". { iApply "HΨ"; by iSplit. } - iIntros {v} "Ha". iDestruct "Ha" as {b} "(% & Hφ & HΨ)". + iIntros {v}; iDestruct 1 as {b} "(% & Hφ & HΨ)". iPvs (own_update _ with "Hγ") as "[Hγ Hγf]"; first eapply auth_update; eauto. iPvsIntro. iSplitL "Hφ Hγ"; last by iApply "HΨ". iNext. iExists (b ⋅ af). by iFrame. diff --git a/program_logic/boxes.v b/program_logic/boxes.v index ee8f117a..d46352a1 100644 --- a/program_logic/boxes.v +++ b/program_logic/boxes.v @@ -60,8 +60,7 @@ Lemma box_own_auth_agree γ b1 b2 : box_own_auth γ (● Excl' b1) ★ box_own_auth γ (◯ Excl' b2) ⊢ b1 = b2. Proof. rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_l. - iIntros "Hb". - by iDestruct "Hb" as % [[[] [=]%leibniz_equiv] ?]%auth_valid_discrete. + by iDestruct 1 as % [[[] [=]%leibniz_equiv] ?]%auth_valid_discrete. Qed. Lemma box_own_auth_update E γ b1 b2 b3 : @@ -95,7 +94,7 @@ Lemma box_insert f P Q : ▷ box N f P ={N}=> ∃ γ, f !! γ = None ★ slice N γ Q ★ ▷ box N (<[γ:=false]> f) (Q ★ P). Proof. - iIntros "H"; iDestruct "H" as {Φ} "[#HeqP Hf]". + iDestruct 1 as {Φ} "[#HeqP Hf]". iPvs (own_alloc_strong (● Excl' false ⋅ ◯ Excl' false, Some (to_agree (Next (iProp_unfold Q)))) _ (dom _ f)) as {γ} "[Hdom Hγ]"; first done. @@ -187,7 +186,7 @@ Lemma box_empty_all f P Q : map_Forall (λ _, (true =)) f → box N f P ={N}=> ▷ P ★ box N (const false <\$> f) P. Proof. - iIntros {?} "H"; iDestruct "H" as {Φ} "[#HeqP Hf]". + iDestruct 1 as {Φ} "[#HeqP Hf]". iAssert ([★ map] γ↦b ∈ f, ▷ Φ γ ★ box_own_auth γ (◯ Excl' false) ★ box_own_prop γ (Φ γ) ★ inv N (slice_inv γ (Φ γ)))%I with "|==>[Hf]" as "[HΦ ?]". { iApply (pvs_big_sepM _ _ f); iApply (big_sepM_impl _ _ f); iFrame "Hf". diff --git a/program_logic/invariants.v b/program_logic/invariants.v index 3fb3ba67..813d2613 100644 --- a/program_logic/invariants.v +++ b/program_logic/invariants.v @@ -37,7 +37,7 @@ Lemma inv_open E N P : inv N P ⊢ ∃ E', ■ (E ∖ nclose N ⊆ E' ⊆ E) ★ |={E,E'}=> ▷ P ★ (▷ P ={E',E}=★ True). Proof. - rewrite /inv. iIntros {?} "Hinv". iDestruct "Hinv" as {i} "[% #Hi]". + rewrite /inv. iDestruct 1 as {i} "[% #Hi]". iExists (E ∖ {[ i ]}). iSplit. { iPureIntro. set_solver. } iPvs (pvs_openI' with "Hi") as "HP"; [set_solver..|]. iPvsIntro. iSplitL "HP"; first done. iIntros "HP". diff --git a/program_logic/sts.v b/program_logic/sts.v index 4455a68b..e6ebf515 100644 --- a/program_logic/sts.v +++ b/program_logic/sts.v @@ -108,7 +108,7 @@ Section sts. iRevert "Hγ"; rewrite sts_op_auth_frag //; iIntros "Hγ". iApply pvs_fsa_fsa; iApply fsa_wand_r; iSplitL "HΨ Hφ". { iApply "HΨ"; by iSplit. } - iIntros {a} "H"; iDestruct "H" as {s' T'} "(% & Hφ & HΨ)". + iIntros {a}; iDestruct 1 as {s' T'} "(% & Hφ & HΨ)". iPvs (own_update with "Hγ") as "Hγ"; first eauto using sts_update_auth. iRevert "Hγ"; rewrite -sts_op_auth_frag_up; iIntros "[Hγ Hγf]". iPvsIntro; iSplitL "Hφ Hγ"; last by iApply "HΨ". diff --git a/proofmode/tactics.v b/proofmode/tactics.v index 944b2118..882c35f4 100644 --- a/proofmode/tactics.v +++ b/proofmode/tactics.v @@ -435,7 +435,7 @@ Local Tactic Notation "iExistDestruct" constr(H) [env_cbv; reflexivity || fail "iExistDestruct:" Hx "not fresh" |revert y; intros x]. -(** * Destruct tactic *) +(** * Basic destruct tactic *) Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) := let rec go Hz pat := lazymatch pat with @@ -485,55 +485,6 @@ Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1) simple_intropattern(x8) "}" constr(pat) := iExistDestruct H as x1 H; iDestructHyp H as { x2 x3 x4 x5 x6 x7 x8 } pat. -Tactic Notation "iDestructHelp" open_constr(lem) "as" tactic(tac) := - lazymatch type of lem with - | string => tac lem - | iTrm => - lazymatch lem with - | @iTrm string ?H _ hnil ?pat => - iSpecializePat H pat; last tac H - | _ => let H := iFresh in iPoseProof lem as H; last tac H; try apply _ - end - | _ => let H := iFresh in iPoseProof lem as H; last tac H; try apply _ - end. - -Tactic Notation "iDestruct" open_constr(H) "as" constr(pat) := - iDestructHelp H as (fun H => iDestructHyp H as pat). -Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1) "}" - constr(pat) := - iDestructHelp H as (fun H => iDestructHyp H as { x1 } pat). -Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1) - simple_intropattern(x2) "}" constr(pat) := - iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 } pat). -Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1) - simple_intropattern(x2) simple_intropattern(x3) "}" constr(pat) := - iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 } pat). -Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1) - simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) "}" - constr(pat) := - iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 } pat). -Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1) - simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) - simple_intropattern(x5) "}" constr(pat) := - iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 } pat). -Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1) - simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) - simple_intropattern(x5) simple_intropattern(x6) "}" constr(pat) := - iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 x6 } pat). -Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1) - simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) - simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) "}" - constr(pat) := - iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 } pat). -Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1) - simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) - simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) - simple_intropattern(x8) "}" constr(pat) := - iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 x8 } pat). - -Tactic Notation "iDestruct" open_constr(H) "as" "%" simple_intropattern(pat) := - let Htmp := iFresh in iDestruct H as Htmp; last iPure Htmp as pat. - (** * Always *) Tactic Notation "iAlways":= apply tac_always_intro; @@ -676,6 +627,67 @@ Tactic Notation "iIntros" "{" simple_intropattern(x1) simple_intropattern(x2) "}" constr(p) := iIntros { x1 x2 x3 x4 x5 x6 x7 x8 }; iIntros p. +(** * Destruct tactic *) +Tactic Notation "iDestructHelp" open_constr(lem) "as" tactic(tac) := + let intro_destruct n := + let rec go n' := + lazymatch n' with + | 0 => fail "iDestruct: cannot introduce" n "hypotheses" + | 1 => repeat iIntroForall; let H := iFresh in iIntro H; tac H + | S ?n' => repeat iIntroForall; let H := iFresh in iIntro H; go n' + end in intros; try iProof; go n in + lazymatch type of lem with + | nat => intro_destruct lem + | Z => (* to make it work in Z_scope. We should just be able to bind + tactic notation arguments to notation scopes. *) + let n := eval compute in (Z.to_nat lem) in intro_destruct n + | string => tac lem + | iTrm => + lazymatch lem with + | @iTrm string ?H _ hnil ?pat => + iSpecializePat H pat; last tac H + | _ => let H := iFresh in iPoseProof lem as H; last tac H; try apply _ + end + | _ => let H := iFresh in iPoseProof lem as H; last tac H; try apply _ + end. + +Tactic Notation "iDestruct" open_constr(H) "as" constr(pat) := + iDestructHelp H as (fun H => iDestructHyp H as pat). +Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1) "}" + constr(pat) := + iDestructHelp H as (fun H => iDestructHyp H as { x1 } pat). +Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1) + simple_intropattern(x2) "}" constr(pat) := + iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 } pat). +Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1) + simple_intropattern(x2) simple_intropattern(x3) "}" constr(pat) := + iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 } pat). +Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1) + simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) "}" + constr(pat) := + iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 } pat). +Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1) + simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) + simple_intropattern(x5) "}" constr(pat) := + iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 } pat). +Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1) + simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) + simple_intropattern(x5) simple_intropattern(x6) "}" constr(pat) := + iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 x6 } pat). +Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1) + simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) + simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) "}" + constr(pat) := + iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 } pat). +Tactic Notation "iDestruct" open_constr(H) "as" "{" simple_intropattern(x1) + simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) + simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) + simple_intropattern(x8) "}" constr(pat) := + iDestructHelp H as (fun H => iDestructHyp H as { x1 x2 x3 x4 x5 x6 x7 x8 } pat). + +Tactic Notation "iDestruct" open_constr(H) "as" "%" simple_intropattern(pat) := + let Htmp := iFresh in iDestruct H as Htmp; last iPure Htmp as pat. + (* This is pretty ugly, but without Ltac support for manipulating lists of idents I do not know how to do this better. *) Local Ltac iLöbHelp IH tac_before tac_after := diff --git a/tests/barrier_client.v b/tests/barrier_client.v index e1699c43..7665f27c 100644 --- a/tests/barrier_client.v +++ b/tests/barrier_client.v @@ -22,7 +22,7 @@ Section client. Lemma y_inv_split q l : y_inv q l ⊢ (y_inv (q/2) l ★ y_inv (q/2) l). Proof. - iIntros "Hl"; iDestruct "Hl" as {f} "[[Hl1 Hl2] #Hf]". + iDestruct 1 as {f} "[[Hl1 Hl2] #Hf]". iSplitL "Hl1"; iExists f; by iSplitL; try iAlways. Qed. @@ -32,7 +32,7 @@ Section client. Proof. iIntros "[#Hh Hrecv]". wp_lam. wp_let. wp_apply wait_spec; iFrame "Hrecv". - iIntros "Hy"; iDestruct "Hy" as {f} "[Hy #Hf]". + iDestruct 1 as {f} "[Hy #Hf]". wp_seq. wp_load. iApply wp_wand_r; iSplitR; [iApply "Hf"|by iIntros {v} "_"]. Qed. diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v index 34089756..bfb6b48f 100644 --- a/tests/joining_existentials.v +++ b/tests/joining_existentials.v @@ -34,7 +34,7 @@ Lemma worker_spec e γ l (Φ Ψ : X → iProp) : ⊢ WP wait #l ;; e {{ _, barrier_res γ Ψ }}. Proof. iIntros "[Hl #He]". wp_apply wait_spec; iFrame "Hl". - iIntros "Hγ"; iDestruct "Hγ" as {x} "[#Hγ Hx]". + iDestruct 1 as {x} "[#Hγ Hx]". wp_seq. iApply wp_wand_l. iSplitR; [|by iApply "He"]. iIntros {v} "?"; iExists x; by iSplit. Qed. @@ -45,7 +45,7 @@ Context {Ψ_join : ∀ x, (Ψ1 x ★ Ψ2 x) ⊢ Ψ x}. Lemma P_res_split γ : barrier_res γ Φ ⊢ barrier_res γ Φ1 ★ barrier_res γ Φ2. Proof. - iIntros "Hγ"; iDestruct "Hγ" as {x} "[#Hγ Hx]". + iDestruct 1 as {x} "[#Hγ Hx]". iDestruct (Φ_split with "Hx") as "[H1 H2]". by iSplitL "H1"; iExists x; iSplit. Qed. -- GitLab