Commit 8b563357 authored by Robbert Krebbers's avatar Robbert Krebbers

Support multiple hypotheses in iCombine.

This fixes issue #72.
parent 94861f1d
......@@ -6,6 +6,8 @@ Set Default Proof Using "Type".
Import uPred.
Import env_notations.
Local Notation "b1 && b2" := (if b1 then b2 else false) : bool_scope.
Record envs (M : ucmraT) :=
Envs { env_persistent : env (uPred M); env_spatial : env (uPred M) }.
Add Printing Constructor envs.
......@@ -51,6 +53,17 @@ Definition envs_lookup_delete {M} (i : string)
| None => '(P,Γs') env_lookup_delete i Γs; Some (false, P, Envs Γp Γs')
end.
Fixpoint envs_lookup_delete_list {M} (js : list string) (remove_persistent : bool)
(Δ : envs M) : option (bool * list (uPred M) * envs M) :=
match js with
| [] => Some (true, [], Δ)
| j :: js =>
'(p,P,Δ') envs_lookup_delete j Δ;
let Δ' := if p then (if remove_persistent then Δ' else Δ) else Δ' in
'(q,Hs,Δ'') envs_lookup_delete_list js remove_persistent Δ';
Some (p && q, P :: Hs, Δ'')
end.
Definition envs_snoc {M} (Δ : envs M)
(p : bool) (j : string) (P : uPred M) : envs M :=
let (Γp,Γs) := Δ in
......@@ -102,7 +115,6 @@ Definition envs_split {M} (lr : bool)
'(Δ1,Δ2) envs_split_go js Δ (envs_clear_spatial Δ);
if lr then Some (Δ1,Δ2) else Some (Δ2,Δ1).
(* Coq versions of the tactics *)
Section tactics.
Context {M : ucmraT}.
......@@ -167,6 +179,21 @@ Lemma envs_lookup_delete_sound' Δ Δ' i p P :
envs_lookup_delete i Δ = Some (p,P,Δ') Δ P Δ'.
Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound'. Qed.
Lemma envs_lookup_delete_list_sound Δ Δ' js rp p Ps :
envs_lookup_delete_list js rp Δ = Some (p, Ps,Δ') Δ ?p [] Ps Δ'.
Proof.
revert Δ Δ' p Ps. induction js as [|j js IH]=> Δ Δ'' p Ps ?; simplify_eq/=.
{ by rewrite always_pure left_id. }
destruct (envs_lookup_delete j Δ) as [[[q1 P] Δ']|] eqn:Hj; simplify_eq/=.
apply envs_lookup_delete_Some in Hj as [Hj ->].
destruct (envs_lookup_delete_list js rp _) as [[[q2 Ps'] ?]|] eqn:?; simplify_eq/=.
rewrite always_if_sep -assoc. destruct q1; simpl.
- destruct rp.
+ rewrite envs_lookup_sound //; simpl. by rewrite IH // (always_elim_if q2).
+ rewrite envs_lookup_persistent_sound //. by rewrite IH // (always_elim_if q2).
- rewrite envs_lookup_sound // IH //; simpl. by rewrite always_if_elim.
Qed.
Lemma envs_lookup_snoc Δ i p P :
envs_lookup i Δ = None envs_lookup i (envs_snoc Δ p i P) = Some (p, P).
Proof.
......@@ -703,26 +730,27 @@ Proof.
Qed.
(** * Combining *)
Lemma tac_combine Δ1 Δ2 Δ3 Δ4 i1 p P1 i2 q P2 j P Q :
envs_lookup_delete i1 Δ1 = Some (p,P1,Δ2)
envs_lookup_delete i2 (if p then Δ1 else Δ2) = Some (q,P2,Δ3)
FromSep P P1 P2
envs_app (p && q) (Esnoc Enil j P)
(if q then (if p then Δ1 else Δ2) else Δ3) = Some Δ4
(Δ4 Q) Δ1 Q.
Proof.
intros [? ->]%envs_lookup_delete_Some [? ->]%envs_lookup_delete_Some ?? <-.
destruct p.
- rewrite envs_lookup_persistent_sound //. destruct q.
+ rewrite envs_lookup_persistent_sound // envs_app_sound //; simpl.
by rewrite right_id assoc -always_sep (from_sep P) wand_elim_r.
+ rewrite envs_lookup_sound // envs_app_sound //; simpl.
by rewrite right_id assoc always_elim (from_sep P) wand_elim_r.
- rewrite envs_lookup_sound //; simpl. destruct q.
+ rewrite envs_lookup_persistent_sound // envs_app_sound //; simpl.
by rewrite right_id assoc always_elim (from_sep P) wand_elim_r.
+ rewrite envs_lookup_sound // envs_app_sound //; simpl.
by rewrite right_id assoc (from_sep P) wand_elim_r.
Class FromSeps {M} (P : uPred M) (Qs : list (uPred M)) :=
from_seps : [] Qs P.
Arguments from_seps {_} _ _ {_}.
Global Instance from_seps_nil : @FromSeps M True [].
Proof. done. Qed.
Global Instance from_seps_singleton P : FromSeps P [P] | 1.
Proof. by rewrite /FromSeps /= right_id. Qed.
Global Instance from_seps_cons P P' Q Qs :
FromSeps P' Qs FromSep P Q P' FromSeps P (Q :: Qs) | 2.
Proof. by rewrite /FromSeps /FromSep /= => ->. Qed.
Lemma tac_combine Δ1 Δ2 Δ3 js p Ps j P Q :
envs_lookup_delete_list js false Δ1 = Some (p, Ps, Δ2)
FromSeps P Ps
envs_app p (Esnoc Enil j P) Δ2 = Some Δ3
(Δ3 Q) Δ1 Q.
Proof.
intros ??? <-. rewrite envs_lookup_delete_list_sound //.
rewrite from_seps. rewrite envs_app_sound //; simpl.
by rewrite right_id wand_elim_r.
Qed.
(** * Conjunction/separating conjunction elimination *)
......
......@@ -578,15 +578,17 @@ Local Tactic Notation "iAndDestructChoice" constr(H) "as" constr(lr) constr(H')
apply _ || fail "iAndDestructChoice: cannot destruct" P
|env_cbv; reflexivity || fail "iAndDestructChoice:" H' " not fresh"|].
Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(H) :=
eapply tac_combine with _ _ _ H1 _ _ H2 _ _ H _;
[env_cbv; reflexivity || fail "iCombine:" H1 "not found"
|env_cbv; reflexivity || fail "iCombine:" H2 "not found"
|let P1 := match goal with |- FromSep _ ?P1 _ => P1 end in
let P2 := match goal with |- FromSep _ _ ?P2 => P2 end in
apply _ || fail "iCombine: cannot combine" P1 "and" P2
(** * Combinining hypotheses *)
Tactic Notation "iCombine" constr(Hs) "as" constr(H) :=
let Hs := words Hs in
eapply tac_combine with _ _ Hs _ _ H _;
[env_cbv; reflexivity || fail "iCombine:" Hs "not found"
|apply _
|env_cbv; reflexivity || fail "iCombine:" H "not fresh"|].
Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(H) :=
iCombine [H1;H2] as H.
(** * Existential *)
Tactic Notation "iExists" uconstr(x1) :=
iStartProof;
......
......@@ -142,3 +142,7 @@ Qed.
Lemma demo_16 (M : ucmraT) (P Q R : uPred M) `{!PersistentP R} :
P - Q - R - R Q P R False.
Proof. eauto with iFrame. Qed.
Lemma demo_17 (M : ucmraT) (P Q R : uPred M) `{!PersistentP R} :
P - Q - R - R Q P R False.
Proof. iIntros "HP HQ #HR". iCombine "HR HQ HP HR" as "H". auto. Qed.
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