Commit 25114815 authored by Robbert Krebbers's avatar Robbert Krebbers

Make iExact and iAssumption work under pvs and always.

parent 8bf6270c
......@@ -114,8 +114,7 @@ Proof.
iSplitL "HR"; [|by iApply "Hwp"].
iPvs "Hvs1" "HR"; first by set_solver.
iPvsIntro. iNext.
iPvs "Hvs2" "Hvs1"; first by set_solver.
by iPvsIntro.
by iPvs "Hvs2" "Hvs1"; first by set_solver.
Lemma ht_frame_step_r E E1 E2 P R1 R2 R3 e Φ :
......@@ -125,7 +124,7 @@ Lemma ht_frame_step_r E E1 E2 P R1 R2 R3 e Φ :
iIntros {???} "[#Hvs1 [#Hvs2 #Hwp]]".
setoid_rewrite (comm _ _ R3).
iApply ht_frame_step_l; try eassumption. repeat iSplit; by iIntros "!".
iApply (ht_frame_step_l _ _ E2); by repeat iSplit.
Lemma ht_frame_step_l' E P R e Φ :
......@@ -71,10 +71,10 @@ Qed.
Lemma vs_transitive' E P Q R : ((P ={E}=> Q) (Q ={E}=> R)) (P ={E}=> R).
Proof. apply vs_transitive; set_solver. Qed.
Lemma vs_reflexive E P : P ={E}=> P.
Proof. iIntros "! HP"; by iPvsIntro. Qed.
Proof. by iIntros "! HP". Qed.
Lemma vs_impl E P Q : (P Q) (P ={E}=> Q).
Proof. iIntros "#HPQ ! HP". iPvsIntro. by iApply "HPQ". Qed.
Proof. iIntros "#HPQ ! HP". by iApply "HPQ". Qed.
Lemma vs_frame_l E1 E2 P Q R : (P ={E1,E2}=> Q) (R P ={E1,E2}=> R Q).
Proof. iIntros "#Hvs ! [HR HP]". iFrame "HR". by iApply "Hvs". Qed.
......@@ -260,8 +260,17 @@ Proof.
(** * Basic rules *)
Lemma tac_exact Δ i p P : envs_lookup i Δ = Some (p,P) Δ P.
Proof. intros. by rewrite envs_lookup_sound' // sep_elim_l. Qed.
Class ToAssumption (p : bool) (P Q : uPred M) :=
to_assumption : (if p then P else P) Q.
Global Instance to_assumption_exact p P : ToAssumption p P P.
Proof. destruct p; by rewrite /ToAssumption ?always_elim. Qed.
Global Instance to_assumption_always P Q :
ToAssumption true P Q ToAssumption true P ( Q).
Proof. rewrite /ToAssumption=><-. by rewrite always_always. Qed.
Lemma tac_assumption Δ i p P Q :
envs_lookup i Δ = Some (p,P) ToAssumption p P Q Δ Q.
Proof. intros. by rewrite envs_lookup_sound // sep_elim_l. Qed.
Lemma tac_rename Δ Δ' i j p P Q :
envs_lookup i Δ = Some (p,P)
......@@ -7,6 +7,9 @@ Section pvs.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types P Q : iProp Λ Σ.
Global Instance to_assumption_pvs E p P Q :
ToAssumption p P Q ToAssumption p P (|={E}=> Q)%I.
Proof. rewrite /ToAssumption=>->. apply pvs_intro. Qed.
Global Instance sep_split_pvs E P Q1 Q2 :
SepSplit P Q1 Q2 SepSplit (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
Proof. rewrite /SepSplit=><-. apply pvs_sep. Qed.
......@@ -63,13 +63,10 @@ Tactic Notation "iClear" "★" :=
(** * Assumptions *)
Tactic Notation "iExact" constr(H) :=
eapply tac_exact with H _; (* (i:=H) *)
lazymatch goal with
| |- None = Some _ => fail "iExact:" H "not found"
| |- Some (_, ?P) = Some _ =>
reflexivity || fail "iExact:" H ":" P "does not match goal"
eapply tac_assumption with H _ _; (* (i:=H) *)
[env_cbv; reflexivity || fail "iExact:" H "not found"
|let P := match goal with |- ToAssumption _ ?P _ => P end in
apply _ || fail "iExact:" H ":" P "does not match goal"].
Tactic Notation "iAssumptionCore" :=
let rec find Γ i P :=
......@@ -82,9 +79,21 @@ Tactic Notation "iAssumptionCore" :=
| |- envs_lookup ?i (Envs ?Γp ?Γs) = Some (_, ?P) =>
is_evar i; first [find Γp i P | find Γs i P]; env_cbv; reflexivity
Tactic Notation "iAssumption" :=
eapply tac_exact; iAssumptionCore;
match goal with |- _ = Some (_, ?P) => fail "iAssumption:" P "not found" end.
let Hass := fresh in
let rec find p Γ Q :=
match Γ with
| Esnoc ?Γ ?j ?P => first
[pose proof (_ : ToAssumption p P Q) as Hass;
apply (tac_assumption _ j p P); [env_cbv; reflexivity|apply Hass]
|find p Γ Q]
end in
match goal with
| |- of_envs (Envs ?Γp ?Γs) ?Q =>
first [find true Γp Q | find false Γs Q
|fail "iAssumption:" Q "not found"]
(** * False *)
Tactic Notation "iExFalso" := apply tac_ex_falso.
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment