Commit 61e8aadd authored by Robbert Krebbers's avatar Robbert Krebbers

Consistent syntax for generalization in iLöb and iInduction.

As proposed by JH Jourdan in issue 34.
parent 7c762be1
...@@ -101,15 +101,16 @@ Separating logic specific tactics ...@@ -101,15 +101,16 @@ Separating logic specific tactics
The later modality The later modality
------------------ ------------------
- `iNext` : introduce a later by stripping laters from all hypotheses. - `iNext` : introduce a later by stripping laters from all hypotheses.
- `iLöb (x1 ... xn) as "IH"` : perform Löb induction by generalizing over the - `iLöb as "IH" forall (x1 ... xn)` : perform Löb induction while generalizing
Coq level variables `x1 ... xn` and the entire spatial context. over the Coq level variables `x1 ... xn` and the entire spatial context.
Induction Induction
--------- ---------
- `iInduction x as cpat "IH"` : perform induction on the Coq term `x`. The Coq - `iInduction x as cpat "IH" forall (x1 ... xn)` : perform induction on the Coq
introduction pattern is used to name the introduced variables. The induction term `x`. The Coq introduction pattern is used to name the introduced
hypotheses are inserted into the persistent context and given fresh names variables. The induction hypotheses are inserted into the persistent context
prefixed `IH`. and given fresh names prefixed `IH`. The tactic generalizes over the Coq level
variables `x1 ... xn` and the entire spatial context.
Rewriting Rewriting
--------- ---------
......
...@@ -91,7 +91,7 @@ Qed. ...@@ -91,7 +91,7 @@ Qed.
Lemma wp_strong_mono E1 E2 e Φ Ψ : Lemma wp_strong_mono E1 E2 e Φ Ψ :
E1 E2 ( v, Φ v ={E2}= Ψ v) WP e @ E1 {{ Φ }} WP e @ E2 {{ Ψ }}. E1 E2 ( v, Φ v ={E2}= Ψ v) WP e @ E1 {{ Φ }} WP e @ E2 {{ Ψ }}.
Proof. Proof.
iIntros (?) "[HΦ H]". iLöb (e) as "IH". rewrite !wp_unfold /wp_pre. iIntros (?) "[HΦ H]". iLöb as "IH" forall (e). rewrite !wp_unfold /wp_pre.
iDestruct "H" as "[Hv|[% H]]"; [iLeft|iRight]. iDestruct "H" as "[Hv|[% H]]"; [iLeft|iRight].
{ iDestruct "Hv" as (v) "[% Hv]". iExists v; iSplit; first done. { iDestruct "Hv" as (v) "[% Hv]". iExists v; iSplit; first done.
iApply ("HΦ" with "==>[-]"). by iApply (pvs_mask_mono E1 _). } iApply ("HΦ" with "==>[-]"). by iApply (pvs_mask_mono E1 _). }
...@@ -148,7 +148,7 @@ Qed. ...@@ -148,7 +148,7 @@ Qed.
Lemma wp_bind `{LanguageCtx Λ K} E e Φ : Lemma wp_bind `{LanguageCtx Λ K} E e Φ :
WP e @ E {{ v, WP K (of_val v) @ E {{ Φ }} }} WP K e @ E {{ Φ }}. WP e @ E {{ v, WP K (of_val v) @ E {{ Φ }} }} WP K e @ E {{ Φ }}.
Proof. Proof.
iIntros "H". iLöb (E e Φ) as "IH". rewrite wp_unfold /wp_pre. iIntros "H". iLöb as "IH" forall (E e Φ). rewrite wp_unfold /wp_pre.
iDestruct "H" as "[Hv|[% H]]". iDestruct "H" as "[Hv|[% H]]".
{ iDestruct "Hv" as (v) "[Hev Hv]"; iDestruct "Hev" as % <-%of_to_val. { iDestruct "Hv" as (v) "[Hev Hv]"; iDestruct "Hev" as % <-%of_to_val.
by iApply pvs_wp. } by iApply pvs_wp. }
......
...@@ -899,9 +899,34 @@ Tactic Notation "iInductionCore" constr(x) ...@@ -899,9 +899,34 @@ Tactic Notation "iInductionCore" constr(x)
end in end in
induction x as pat; fix_ihs. induction x as pat; fix_ihs.
Tactic Notation "iInduction" constr(x) Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH) :=
"as" simple_intropattern(pat) constr(IH) :=
iRevertIntros with (iInductionCore x as pat IH). iRevertIntros with (iInductionCore x as pat IH).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"forall" "(" ident(x1) ")" :=
iRevertIntros(x1) with (iInductionCore x as pat IH).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"forall" "(" ident(x1) ident(x2) ")" :=
iRevertIntros(x1 x2) with (iInductionCore x as pat IH).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"forall" "(" ident(x1) ident(x2) ident(x3) ")" :=
iRevertIntros(x1 x2 x3) with (iInductionCore x as pat IH).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ")" :=
iRevertIntros(x1 x2 x3 x4) with (iInductionCore x as pat IH).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ident(x5) ")" :=
iRevertIntros(x1 x2 x3 x4 x5) with (iInductionCore x as aat IH).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ident(x5) ident(x6) ")" :=
iRevertIntros(x1 x2 x3 x4 x5 x6) with (iInductionCore x as pat IH).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ident(x5) ident(x6)
ident(x7) ")" :=
iRevertIntros(x1 x2 x3 x4 x5 x6 x7) with (iInductionCore x as pat IH).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ident(x5) ident(x6)
ident(x7) ident(x8) ")" :=
iRevertIntros(x1 x2 x3 x4 x5 x6 x7 x8) with (iInductionCore x as pat IH).
(** * Löb Induction *) (** * Löb Induction *)
Tactic Notation "iLöbCore" "as" constr (IH) := Tactic Notation "iLöbCore" "as" constr (IH) :=
...@@ -911,26 +936,27 @@ Tactic Notation "iLöbCore" "as" constr (IH) := ...@@ -911,26 +936,27 @@ Tactic Notation "iLöbCore" "as" constr (IH) :=
Tactic Notation "iLöb" "as" constr (IH) := Tactic Notation "iLöb" "as" constr (IH) :=
iRevertIntros with (iLöbCore as IH). iRevertIntros with (iLöbCore as IH).
Tactic Notation "iLöb" "(" ident(x1) ")" "as" constr (IH) := Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ")" :=
iRevertIntros(x1) with (iLöbCore as IH). iRevertIntros(x1) with (iLöbCore as IH).
Tactic Notation "iLöb" "(" ident(x1) ident(x2) ")" "as" constr (IH) := Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2) ")" :=
iRevertIntros(x1 x2) with (iLöbCore as IH). iRevertIntros(x1 x2) with (iLöbCore as IH).
Tactic Notation "iLöb" "(" ident(x1) ident(x2) ident(x3) ")" "as" constr (IH) := Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
ident(x3) ")" :=
iRevertIntros(x1 x2 x3) with (iLöbCore as IH). iRevertIntros(x1 x2 x3) with (iLöbCore as IH).
Tactic Notation "iLöb" "(" ident(x1) ident(x2) ident(x3) ident(x4) ")" "as" Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
constr (IH):= ident(x3) ident(x4) ")" :=
iRevertIntros(x1 x2 x3 x4) with (iLöbCore as IH). iRevertIntros(x1 x2 x3 x4) with (iLöbCore as IH).
Tactic Notation "iLöb" "(" ident(x1) ident(x2) ident(x3) ident(x4) Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
ident(x5) ")" "as" constr (IH) := ident(x3) ident(x4) ident(x5) ")" :=
iRevertIntros(x1 x2 x3 x4 x5) with (iLöbCore as IH). iRevertIntros(x1 x2 x3 x4 x5) with (iLöbCore as IH).
Tactic Notation "iLöb" "(" ident(x1) ident(x2) ident(x3) ident(x4) Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
ident(x5) ident(x6) ")" "as" constr (IH) := ident(x3) ident(x4) ident(x5) ident(x6) ")" :=
iRevertIntros(x1 x2 x3 x4 x5 x6) with (iLöbCore as IH). iRevertIntros(x1 x2 x3 x4 x5 x6) with (iLöbCore as IH).
Tactic Notation "iLöb" "(" ident(x1) ident(x2) ident(x3) ident(x4) Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
ident(x5) ident(x6) ident(x7) ")" "as" constr (IH) := ident(x3) ident(x4) ident(x5) ident(x6) ident(x7) ")" :=
iRevertIntros(x1 x2 x3 x4 x5 x6 x7) with (iLöbCore as IH). iRevertIntros(x1 x2 x3 x4 x5 x6 x7) with (iLöbCore as IH).
Tactic Notation "iLöb" "(" ident(x1) ident(x2) ident(x3) ident(x4) Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
ident(x5) ident(x6) ident(x7) ident(x8) ")" "as" constr (IH) := ident(x3) ident(x4) ident(x5) ident(x6) ident(x7) ident(x8) ")" :=
iRevertIntros(x1 x2 x3 x4 x5 x6 x7 x8) with (iLöbCore as IH). iRevertIntros(x1 x2 x3 x4 x5 x6 x7 x8) with (iLöbCore as IH).
(** * Assert *) (** * Assert *)
......
...@@ -44,7 +44,7 @@ Section LiftingTests. ...@@ -44,7 +44,7 @@ Section LiftingTests.
n1 < n2 n1 < n2
Φ #(n2 - 1) WP FindPred #n2 #n1 @ E {{ Φ }}. Φ #(n2 - 1) WP FindPred #n2 #n1 @ E {{ Φ }}.
Proof. Proof.
iIntros (Hn) "HΦ". iLöb (n1 Hn) as "IH". iIntros (Hn) "HΦ". iLöb as "IH" forall (n1 Hn).
wp_rec. wp_let. wp_op. wp_let. wp_op=> ?; wp_if. wp_rec. wp_let. wp_op. wp_let. wp_op=> ?; wp_if.
- iApply ("IH" with "[%] HΦ"). omega. - iApply ("IH" with "[%] HΦ"). omega.
- iApply pvs_intro. by assert (n1 = n2 - 1) as -> by omega. - iApply pvs_intro. by assert (n1 = n2 - 1) as -> by omega.
......
...@@ -32,7 +32,7 @@ Lemma rev_acc_wp hd acc xs ys (Φ : val → iProp Σ) : ...@@ -32,7 +32,7 @@ Lemma rev_acc_wp hd acc xs ys (Φ : val → iProp Σ) :
WP rev hd acc {{ Φ }}. WP rev hd acc {{ Φ }}.
Proof. Proof.
iIntros "(#Hh & Hxs & Hys & HΦ)". iIntros "(#Hh & Hxs & Hys & HΦ)".
iLöb (hd acc xs ys Φ) as "IH". wp_rec. wp_let. iLöb as "IH" forall (hd acc xs ys Φ). wp_rec. wp_let.
destruct xs as [|x xs]; iSimplifyEq. destruct xs as [|x xs]; iSimplifyEq.
- wp_match. by iApply "HΦ". - wp_match. by iApply "HΦ".
- iDestruct "Hxs" as (l hd') "(% & Hx & Hxs)"; iSimplifyEq. - iDestruct "Hxs" as (l hd') "(% & Hx & Hxs)"; iSimplifyEq.
......
...@@ -41,7 +41,7 @@ Lemma sum_loop_wp `{!heapG Σ} v t l (n : Z) (Φ : val → iProp Σ) : ...@@ -41,7 +41,7 @@ Lemma sum_loop_wp `{!heapG Σ} v t l (n : Z) (Φ : val → iProp Σ) :
WP sum_loop v #l {{ Φ }}. WP sum_loop v #l {{ Φ }}.
Proof. Proof.
iIntros "(#Hh & Hl & Ht & HΦ)". iIntros "(#Hh & Hl & Ht & HΦ)".
iLöb (v t l n Φ) as "IH". wp_rec. wp_let. iLöb as "IH" forall (v t l n Φ). wp_rec. wp_let.
destruct t as [n'|tl tr]; simpl in *. destruct t as [n'|tl tr]; simpl in *.
- iDestruct "Ht" as "%"; subst. - iDestruct "Ht" as "%"; subst.
wp_match. wp_load. wp_op. wp_store. wp_match. wp_load. wp_op. wp_store.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment