Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

program_logic/hoare.v

@@ -107,15 +107,14 @@ Proof. setoid_rewrite (comm _ _ R); apply ht_frame_l. Qed.
 Lemma ht_frame_step_l E E1 E2 P R1 R2 R3 e Φ :
   to_val e = None → E ⊥ E1 → E2 ⊆ E1 →
   ((R1 ={E1,E2}=> ▷ R2) ∧ (R2 ={E2,E1}=> R3) ∧ {{ P }} e @ E {{ Φ }})
-    ⊢ {{ R1 ★ P }} e @ (E ∪ E1) {{ λ v, R3 ★ Φ v }}.
+    ⊢ {{ R1 ★ P }} e @ E ∪ E1 {{ λ v, R3 ★ Φ v }}.
 Proof.
   iIntros {???} "[#Hvs1 [#Hvs2 #Hwp]] ! [HR HP]".
   iApply (wp_frame_step_l E E1 E2); try done.
-  iSplitL "HR".
-  - iPvs "Hvs1" "HR" as "HR"; first by set_solver.
-    iPvsIntro. iNext. iPvs "Hvs2" "HR" as "HR"; first by set_solver.
-    iPvsIntro. iApply "HR".
-  - iApply "Hwp" "HP".
+  iSplitL "HR"; [|by iApply "Hwp"].
+  iPvs "Hvs1" "HR"; first by set_solver.
+  iPvsIntro. iNext.
+  by iPvs "Hvs2" "Hvs1"; first by set_solver.
 Qed.
 
 Lemma ht_frame_step_r E E1 E2 P R1 R2 R3 e Φ :
@@ -123,10 +122,9 @@ Lemma ht_frame_step_r E E1 E2 P R1 R2 R3 e Φ :
   ((R1 ={E1,E2}=> ▷ R2) ∧ (R2 ={E2,E1}=> R3) ∧ {{ P }} e @ E {{ Φ }})
     ⊢ {{ R1 ★ P }} e @ (E ∪ E1) {{ λ v, Φ v ★ R3 }}.
 Proof.
-  iIntros {???} "[Hvs1 [Hvs2 Hwp]]".
+  iIntros {???} "[#Hvs1 [#Hvs2 #Hwp]]".
   setoid_rewrite (comm _ _ R3).
-  iApply ht_frame_step_l; try eassumption.
-  iSplit; last iSplit; done.
+  iApply (ht_frame_step_l _ _ E2); by repeat iSplit.
 Qed.
 
 Lemma ht_frame_step_l' E P R e Φ :

program_logic/viewshifts.v

@@ -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.

program_logic/weakestpre.v

@@ -198,33 +198,37 @@ Proof.
 Qed.
 Lemma wp_frame_step_r E E1 E2 e Φ R :
   to_val e = None → E ⊥ E1 → E2 ⊆ E1 →
-  (WP e @ E {{ Φ }} ★ |={E1,E2}=> ▷ |={E2,E1}=> R)
-  ⊢ WP e @ (E ∪ E1) {{ v, Φ v ★ R }}.
+    (WP e @ E {{ Φ }} ★ |={E1,E2}=> ▷ |={E2,E1}=> R)
+  ⊢ WP e @ E ∪ E1 {{ v, Φ v ★ R }}.
+Proof.
   rewrite wp_eq pvs_eq=> He ??.
   uPred.unseal; split; intros n r' Hvalid (r&rR&Hr&Hwp&HR); cofe_subst.
   constructor; [done|]=>rf k Ef σ1 ?? Hws1.
   destruct Hwp as [|n r e ? Hgo]; [by rewrite to_of_val in He|].
   (* "execute" HR *)
-  edestruct (HR (r ⋅ rf) (S k) (E ∪ Ef) σ1) as [s [Hvs Hws2]]; [omega|set_solver| |].
-  { eapply wsat_change, Hws1; first by set_solver+.
-    rewrite assoc [rR ⋅ _]comm. done. } clear Hws1 HR.
+  destruct (HR (r ⋅ rf) (S k) (E ∪ Ef) σ1) as (s&Hvs&Hws2); auto.
+  { eapply wsat_proper, Hws1; first by set_solver+.
+    by rewrite assoc [rR ⋅ _]comm. }
+  clear Hws1 HR.
   (* Take a step *)
-  destruct (Hgo (s⋅rf) k (E2 ∪ Ef) σ1) as [Hsafe Hstep]; [done|set_solver| |].
-  { eapply wsat_change, Hws2; first by set_solver+.
-    rewrite !assoc [s ⋅ _]comm. done. } clear Hgo.
+  destruct (Hgo (s⋅rf) k (E2 ∪ Ef) σ1) as [Hsafe Hstep]; auto.
+  { eapply wsat_proper, Hws2; first by set_solver+.
+    by rewrite !assoc [s ⋅ _]comm. }
+  clear Hgo.
   split; [done|intros e2 σ2 ef ?].
   destruct (Hstep e2 σ2 ef) as (r2&r2'&Hws3&?&?); auto. clear Hws2.
   (* Execute 2nd part of the view shift *)
-  edestruct (Hvs (r2 ⋅ r2' ⋅ rf) k (E ∪ Ef) σ2) as [t [HR Hws4]]; [omega|set_solver| |].
-  { eapply wsat_change, Hws3; first by set_solver+.
-    rewrite !assoc [_ ⋅ s]comm !assoc. done. } clear Hvs Hws3.
+  destruct (Hvs (r2 ⋅ r2' ⋅ rf) k (E ∪ Ef) σ2) as (t&HR&Hws4); auto.
+  { eapply wsat_proper, Hws3; first by set_solver+.
+    by rewrite !assoc [_ ⋅ s]comm !assoc. }
+  clear Hvs Hws3.
   (* Execute the rest of e *)
   exists (r2 ⋅ t), r2'. split_and?; auto.
-  - eapply wsat_change, Hws4; first by set_solver+.
-    rewrite !assoc [_ ⋅ t]comm. done.
-  - rewrite -uPred_sep_eq. move:(wp_frame_r). rewrite wp_eq=>Hframe.
+  - eapply wsat_proper, Hws4; first by set_solver+.
+    by rewrite !assoc [_ ⋅ t]comm.
+  - rewrite -uPred_sep_eq. move: wp_frame_r. rewrite wp_eq=>Hframe.
     apply Hframe; first by auto. uPred.unseal; exists r2, t; split_and?; auto.
-    move:(wp_mask_frame_mono). rewrite wp_eq=>Hmask.
+    move: wp_mask_frame_mono. rewrite wp_eq=>Hmask.
     eapply (Hmask E); by auto.
 Qed.
 Lemma wp_bind `{LanguageCtx Λ K} E e Φ :

program_logic/wsat.v

@@ -42,11 +42,11 @@ Proof.
 Qed.
 Global Instance wsat_ne n : Proper (dist n ==> iff) (@wsat Λ Σ n E σ) | 1.
 Proof. by intros E σ w1 w2 Hw; split; apply wsat_ne'. Qed.
-Global Instance wsat_proper n : Proper ((≡) ==> iff) (@wsat Λ Σ n E σ) | 1.
+Global Instance wsat_proper' n : Proper ((≡) ==> iff) (@wsat Λ Σ n E σ) | 1.
 Proof. by intros E σ w1 w2 Hw; apply wsat_ne, equiv_dist. Qed.
-Lemma wsat_change n E1 E2 σ r1 r2 :
+Lemma wsat_proper n E1 E2 σ r1 r2 :
   E1 = E2 → r1 ≡ r2 → wsat n E1 σ r1 → wsat n E2 σ r2.
-Proof. move=>->->. done. Qed.
+Proof. by move=>->->. Qed.
 Lemma wsat_le n n' E σ r : wsat n E σ r → n' ≤ n → wsat n' E σ r.
 Proof.
   destruct n as [|n], n' as [|n']; simpl; try by (auto with lia).

proofmode/coq_tactics.v

@@ -260,8 +260,17 @@ Proof.
 Qed.
 
 (** * 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) →

proofmode/pviewshifts.v

@@ -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.
@@ -106,7 +109,7 @@ Tactic Notation "iPvsCore" constr(H) :=
     eapply tac_pvs_elim_fsa with _ _ _ _ H _ _ _;
       [env_cbv; reflexivity || fail "iPvs:" H "not found"
       |let P := match goal with |- FSASplit ?P _ _ _ _ => P end in
-       apply _ || fail "iPvs: " P "not a pvs"
+       apply _ || fail "iPvs:" P "not a pvs"
       |env_cbv; reflexivity|simpl]
   end.
 

proofmode/tactics.v

@@ -63,13 +63,10 @@ Tactic Notation "iClear" "★" :=
 
 (** * Assumptions *)
 Tactic Notation "iExact" constr(H) :=
-  eapply tac_exact with H _; (* (i:=H) *)
-    env_cbv;
-    lazymatch goal with
-    | |- None = Some _ => fail "iExact:" H "not found"
-    | |- Some (_, ?P) = Some _ =>
-       reflexivity || fail "iExact:" H ":" P "does not match goal"
-    end.
+  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
   end.
+
 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"]
+  end.
 
 (** * False *)
 Tactic Notation "iExFalso" := apply tac_ex_falso.
@@ -302,8 +311,8 @@ Tactic Notation "iApply" open_constr (lem) :=
   iPoseProof lem as (fun H => repeat (iForallSpecialize H _); first
     [iExact H
     |eapply tac_apply with _ H _ _ _;
-       [env_cbv; reflexivity || fail "iApply:" lem "not found"
-       |apply _ || fail "iApply: cannot apply" lem|]]).
+       [env_cbv; reflexivity || fail 1 "iApply:" lem "not found"
+       |apply _ || fail 1 "iApply: cannot apply" lem|]]).
 Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) "}" :=
   iSpecialize H { x1 }; last iApply H.
 Tactic Notation "iApply" open_constr (H) "{" open_constr(x1)
@@ -335,8 +344,8 @@ Tactic Notation "iApply" open_constr (lem) constr(Hs) :=
   iPoseProof lem Hs as (fun H => first
     [iExact H
     |eapply tac_apply with _ H _ _ _;
-       [env_cbv; reflexivity || fail "iApply:" lem "not found"
-       |apply _ || fail "iApply: cannot apply" lem|]]).
+       [env_cbv; reflexivity || fail 1 "iApply:" lem "not found"
+       |apply _ || fail 1 "iApply: cannot apply" lem|]]).
 Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) "}" constr(Hs) :=
   iSpecialize H { x1 }; last iApply H Hs.
 Tactic Notation "iApply" open_constr (H) "{" open_constr(x1) open_constr(x2) "}"