Derived lifting lemmas.

The proofs are neither short nor nice, but at least they compile
fast (4 sec for the whole file) and the statements look like
they would look like on paper.

iris/hoare_lifting.v

+Require Export iris.hoare iris.lifting.
+
+Local Notation "{{ P } } ef ?@ E {{ Q } }" :=
+  (default True%I ef (λ e, ht E P e Q))
+  (at level 74, format "{{  P  } }  ef  ?@  E  {{  Q  } }") : uPred_scope.
+Local Notation "{{ P } } ef ?@ E {{ Q } }" :=
+  (True ⊑ default True ef (λ e, ht E P e Q))
+  (at level 74, format "{{  P  } }  ef  ?@  E  {{  Q  } }") : C_scope.
+
+Section lifting.
+Context {Σ : iParam}.
+Implicit Types e : iexpr Σ.
+Import uPred.
+
+Lemma ht_lift_step E1 E2
+    (φ : iexpr Σ → istate Σ → option (iexpr Σ) → Prop) P P' Q1 Q2 R e1 σ1 :
+  E1 ⊆ E2 → to_val e1 = None →
+  (∃ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef) →
+  (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
+  (P >{E2,E1}> (ownP σ1 ★ ▷ P') ∧ ∀ e2 σ2 ef,
+    (■ φ e2 σ2 ef ★ ownP σ2 ★ P') >{E1,E2}> (Q1 e2 σ2 ef ★ Q2 e2 σ2 ef) ∧
+    {{ Q1 e2 σ2 ef }} e2 @ E2 {{ R }} ∧
+    {{ Q2 e2 σ2 ef }} ef ?@ coPset_all {{ λ _, True }})
+  ⊑ {{ P }} e1 @ E2 {{ R }}.
+Proof.
+  intros ?? Hsafe Hstep; apply (always_intro' _ _), impl_intro_l.
+  rewrite (associative _ P) {1}/vs always_elim impl_elim_r pvs_always_r.
+  rewrite -(wp_lift_step E1 E2 φ _ e1 σ1) //; apply pvs_mono.
+  rewrite always_and_sep_r' -associative; apply sep_mono; first done.
+  rewrite (later_intro (∀ _, _)) -later_sep; apply later_mono.
+  apply forall_intro=>e2; apply forall_intro=>σ2; apply forall_intro=>ef.
+  rewrite (forall_elim _ e2) (forall_elim _ σ2) (forall_elim _ ef).
+  apply wand_intro_l; rewrite !always_and_sep_l'.
+  rewrite (associative _ _ P') -(associative _ _ _ P') associative.
+  rewrite {1}/vs -always_wand_impl always_elim wand_elim_r.
+  rewrite pvs_frame_r; apply pvs_mono.
+  rewrite (commutative _ (Q1 _ _ _)) -associative (associative _ (Q1 _ _ _)).
+  rewrite {1}/ht -always_wand_impl always_elim wand_elim_r.
+  rewrite associative (commutative _ _ (wp _ _ _)) -associative.
+  apply sep_mono; first done.
+  destruct ef as [e'|]; simpl; [|by apply const_intro].
+  rewrite {1}/ht -always_wand_impl always_elim wand_elim_r; apply wp_mono=>v.
+  by apply const_intro.
+Qed.
+Lemma ht_lift_atomic E
+    (φ : iexpr Σ → istate Σ → option (iexpr Σ) → Prop) P e1 σ1 :
+  atomic e1 →
+  (∃ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef) →
+  (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
+  (∀ e2 σ2 ef, {{ ■ φ e2 σ2 ef ★ P }} ef ?@ coPset_all {{ λ _, True }}) ⊑
+  {{ ownP σ1 ★ ▷ P }} e1 @ E {{ λ v, ∃ σ2 ef, ownP σ2 ★ ■ φ (of_val v) σ2 ef }}.
+Proof.
+  intros ? Hsafe Hstep; set (φ' e σ ef := is_Some (to_val e) ∧ φ e σ ef).
+  rewrite -(ht_lift_step E E φ'  _ P
+    (λ e2 σ2 ef, ownP σ2 ★ ■ (φ' e2 σ2 ef))%I
+    (λ e2 σ2 ef, ■ φ e2 σ2 ef ★ P)%I);
+    try by (rewrite /φ'; eauto using atomic_not_value, atomic_step).
+  apply and_intro; [by rewrite -vs_reflexive; apply const_intro|].
+  apply forall_intro=>e2; apply forall_intro=>σ2; apply forall_intro=>ef.
+  rewrite (forall_elim _ e2) (forall_elim _ σ2) (forall_elim _ ef).
+  apply and_intro; [|apply and_intro; [|done]].
+  * rewrite -vs_impl; apply (always_intro' _ _),impl_intro_l;rewrite and_elim_l.
+    rewrite !associative; apply sep_mono; last done.
+    rewrite -!always_and_sep_l' -!always_and_sep_r'; apply const_elim_l=>-[??].
+    by repeat apply and_intro; try apply const_intro.
+  * apply (always_intro' _ _), impl_intro_l; rewrite and_elim_l.
+    rewrite -always_and_sep_r'; apply const_elim_r=>-[[v Hv] ?].
+    rewrite -(of_to_val e2 v) // -wp_value -pvs_intro.
+    rewrite -(exist_intro _ σ2) -(exist_intro _ ef) (of_to_val e2) //.
+    by rewrite -always_and_sep_r'; apply and_intro; try apply const_intro.
+Qed.
+Lemma ht_lift_pure_step E (φ : iexpr Σ → option (iexpr Σ) → Prop) P P' Q e1 :
+  to_val e1 = None →
+  (∀ σ1, ∃ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef) →
+  (∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ φ e2 ef) →
+  (∀ e2 ef,
+    {{ ■ φ e2 ef ★ P }} e2 @ E {{ Q }} ∧
+    {{ ■ φ e2 ef ★ P' }} ef ?@ coPset_all {{ λ _, True }})
+  ⊑ {{ ▷(P ★ P') }} e1 @ E {{ Q }}.
+Proof.
+  intros ? Hsafe Hstep; apply (always_intro' _ _), impl_intro_l.
+  rewrite -(wp_lift_pure_step E φ _ e1) //.
+  rewrite (later_intro (∀ _, _)) -later_and; apply later_mono.
+  apply forall_intro=>e2; apply forall_intro=>ef; apply impl_intro_l.
+  rewrite (forall_elim _ e2) (forall_elim _ ef).
+  rewrite always_and_sep_l' !always_and_sep_r' {1}(always_sep_dup' (■ _)).
+  rewrite {1}(associative _ (_ ★ _)%I) -(associative _ (■ _)%I).
+  rewrite (associative _ (■ _)%I P) -{1}(commutative _ P) -(associative _ P).
+  rewrite (associative _ (■ _)%I) associative -(associative _ (■ _ ★ P))%I.
+  rewrite (commutative _ (■ _ ★ P'))%I associative.
+  rewrite {1}/ht -always_wand_impl always_elim wand_elim_r.
+  rewrite -associative; apply sep_mono; first done.
+  destruct ef as [e'|]; simpl; [|by apply const_intro].
+  rewrite {1}/ht -always_wand_impl always_elim wand_elim_r; apply wp_mono=>v.
+  by apply const_intro.
+Qed.
+Lemma ht_lift_pure_determistic_step E
+    (φ : iexpr Σ → option (iexpr Σ) → Prop) P P' Q e1 e2 ef :
+  to_val e1 = None →
+  (∀ σ1, prim_step e1 σ1 e2 σ1 ef) →
+  (∀ σ1 e2' σ2 ef', prim_step e1 σ1 e2' σ2 ef' → σ1 = σ2 ∧ e2 = e2' ∧ ef = ef')→
+  ({{ P }} e2 @ E {{ Q }} ∧ {{ P' }} ef ?@ coPset_all {{ λ _, True }})
+  ⊑ {{ ▷(P ★ P') }} e1 @ E {{ Q }}.
+Proof.
+  intros ? Hsafe Hdet.
+  rewrite -(ht_lift_pure_step _ (λ e2' ef', e2 = e2' ∧ ef = ef')); eauto.
+  apply forall_intro=>e2'; apply forall_intro=>ef'; apply and_mono.
+  * apply (always_intro' _ _), impl_intro_l.
+    rewrite -always_and_sep_l' -associative; apply const_elim_l=>-[??]; subst.
+    by rewrite /ht always_elim impl_elim_r.
+  * destruct ef' as [e'|]; simpl; [|by apply const_intro].
+    apply (always_intro' _ _), impl_intro_l.
+    rewrite -always_and_sep_l' -associative; apply const_elim_l=>-[??]; subst.
+    by rewrite /= /ht always_elim impl_elim_r.
+Qed.
+End lifting.

iris/lifting.v

-Require Export iris.hoare.
+Require Export iris.weakestpre.
 Require Import iris.wsat.
 Local Hint Extern 10 (_ ≤ _) => omega.
 Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of.
@@ -6,13 +6,6 @@ Local Hint Extern 10 (✓{_} _) =>
   repeat match goal with H : wsat _ _ _ _ |- _ => apply wsat_valid in H end;
   solve_validN.
 
-Local Notation "{{ P } } ef ?@ E {{ Q } }" :=
-  (default True%I ef (λ e, ht E P e Q))
-  (at level 74, format "{{  P  } }  ef  ?@  E  {{  Q  } }") : uPred_scope.
-Local Notation "{{ P } } ef ?@ E {{ Q } }" :=
-  (True ⊑ default True ef (λ e, ht E P e Q))
-  (at level 74, format "{{  P  } }  ef  ?@  E  {{  Q  } }") : C_scope.
-
 Section lifting.
 Context {Σ : iParam}.
 Implicit Types v : ival Σ.