Experimenting with an `alternative' value interpretation

theories/tests/rules.v

 From iris.proofmode Require Import tactics.
 From iris_logrel Require Import logrel.
+From iris.program_logic Require Import hoare.
+
+Section prim.
+Context {M : ucmraT}.
+Implicit Types φ : Prop.
+Implicit Types P Q : uPred M.
+Implicit Types A : Type.
+Import uPred.
+Lemma test P Q :
+  (P → (Q → P))%I.
+Proof.
+  iIntros "HP". apply impl_intro_r.
+  rewrite and_elim_l. 
+  change (envs_entails (Envs Enil (Esnoc Enil "HP" P)) P).
+  iFrame.
+Qed.
+Lemma exist_impl {A} (Φ Ψ : A → uPred M) :
+  (∀ a, Φ a → Ψ a) -∗ ((∃ a, Φ a) → ∃ a, Ψ a).
+Proof.
+  apply impl_intro_r.
+  iIntros "HΦ".
+  rewrite and_exist_l.
+  iDestruct "HΦ" as (a) "HΦ".
+  iExists a. rewrite (and_mono_l (∀ a0 : A, Φ a0 → Ψ a0) _ (Φ a → Ψ a)).
+  - by rewrite impl_elim_l.
+  - iIntros "H". iApply "H".
+Qed.
+(* Lemma forall_wand {A} (Φ Ψ : A → uPred M) : *)
+(*   (∀ a, Φ a -∗ Ψ a) -∗ (∀ a, Φ a) -∗ ∀ a, Ψ a. *)
+(* Proof. *)
+(*   iIntros "HΦ Ha" (a). *)
+(*   by iApply "HΦ". *)
+(* Qed. *)
+Lemma and_impl (Φ1 Φ2 Ψ1 Ψ2 : uPred M) :
+  (Φ1 → Ψ1) -∗ 
+  (Φ2 → Ψ2) -∗
+  (Φ1 ∧ Φ2) → (Ψ1 ∧ Ψ2).
+Proof.
+  apply wand_intro_l.
+  apply impl_intro_r.
+  rewrite sep_and.
+  rewrite assoc. rewrite -(assoc uPred_and _ _ Φ1).
+  rewrite impl_elim_l. rewrite (comm uPred_and _ Ψ1).
+  rewrite -assoc. rewrite impl_elim_l. done.
+Qed.
+Lemma wand_wand (Φ1 Φ2 Ψ1 Ψ2 : uPred M) :
+  (Ψ1 -∗ Φ1) -∗ 
+  (Φ2 -∗ Ψ2) -∗
+  (Φ1 -∗ Φ2) -∗ (Ψ1 -∗ Ψ2).
+Proof.
+  iIntros "HΦ1 HΦ2 HΦ HΨ".
+  iApply "HΦ2". iApply "HΦ". by iApply "HΦ1".
+Qed.
+Lemma sep_wand (Φ1 Φ2 Ψ1 Ψ2 : uPred M) :
+  (Φ1 -∗ Ψ1) -∗ 
+  (Φ2 -∗ Ψ2) -∗
+  (Φ1 ∗ Φ2) -∗ (Ψ1 ∗ Ψ2).
+Proof.
+  iIntros "HΦ1 HΦ2 [HΦ HΦ']".
+  iSplitL "HΦ HΦ1".
+  - by iApply "HΦ1". 
+  - by iApply "HΦ2".
+Qed.
+Lemma or_wand (Φ1 Φ2 Ψ1 Ψ2 : uPred M) :
+  (Φ1 -∗ Ψ1) -∗ 
+  (Φ2 -∗ Ψ2) -∗
+  (Φ1 ∨ Φ2) -∗ (Ψ1 ∨ Ψ2).
+Proof.
+  iIntros "HΦ1 HΦ2 [HΦ | HΦ]".
+  - iLeft. by iApply "HΦ1". 
+  - iRight. by iApply "HΦ2".
+Qed.
+End prim.
+
+Section derived.
+Context `{irisG F_mu_ref_conc_lang Σ}.
+Implicit Types Φ Ψ : iProp Σ.
+
+Lemma fupd_wand (E : coPset) Φ Ψ :
+  (Φ -∗ Ψ) -∗ 
+  (|={E}=> Φ) -∗ (|={E}=> Ψ).
+Proof.
+  iIntros "HΦ". iMod 1 as "HΦ'".
+  iModIntro. by iApply "HΦ".
+Qed.
+Lemma wp_wand_flipped E e (Φ Ψ : val → iProp Σ) :
+  (∀ v, Φ v -∗ Ψ v) -∗ 
+  WP e @ E {{ Φ }} -∗ WP e @ E {{ Ψ }}.
+Proof.
+  iIntros "H1 H2". iApply (wp_wand with "H2 H1").
+Qed.
+End derived.
 
 Section test.
   Context `{logrelG Σ}.
+  Notation D := (prodC valC valC -n> iProp Σ).
+  Import uPred.
+
+  (* HACK: move somewhere else *)
+  Ltac auto_equiv :=
+    (* Deal with "pointwise_relation" *)
+    repeat lazymatch goal with
+           | |- pointwise_relation _ _ _ _ => intros ?
+           end;
+    (* Normalize away equalities. *)
+    repeat match goal with
+           | H : _ ≡{_}≡ _ |-  _ => apply (discrete_iff _ _) in H
+           | _ => progress simplify_eq
+           end;
+    (* repeatedly apply congruence lemmas and use the equalities in the hypotheses. *)
+    try (f_equiv; fast_done || auto_equiv).
+
+  Ltac solve_proper ::= solve_proper_core ltac:(fun _ => simpl; auto_equiv).
+
+  Program Definition interp_arrow_alt
+          (interp1 : listC D -n> D) (τ2 : type) : listC D -n> D :=
+    λne Δ ww,
+    (□ ∀ vv, interp1 Δ vv →
+             {⊤,⊤;Δ;∅} ⊨ (App (of_val (ww.1)) (of_val (vv.1)))
+                         ≤log≤
+                            (App (of_val (ww.2)) (of_val (vv.2))) : τ2)%I.
+  Solve Obligations with solve_proper.
+  Next Obligation.
+    intros τ2 interp n.
+    intros Δ1 Δ2 HΔ.
+    intros [v1 v2]. simpl.
+    auto_equiv.
+    by apply bin_log_related_ne.
+  Qed.
+
+  (* ALSO holds for vv : expr * expr *)
+  Lemma interp_expr_wat τ2 Δ (vv ww : prodC valC valC) ρ :
+    spec_ctx ρ -∗
+    ({Δ; ∅} ⊨ (App (vv.1) (ww.1)) ≤log≤ (App (vv.2) (ww.2)) : τ2) →
+    ⟦ τ2 ⟧ₑ Δ ((vv.1) (ww.1), (vv.2) (ww.2)).
+  Proof.
+    iIntros "#Hspec H /=".
+    rewrite bin_log_related_eq /bin_log_related_def.
+    iIntros (j K) "Hj /=".
+    iSpecialize ("H" $! ∅ ρ with "Hspec []").
+    { iAlways. by iApply interp_env_nil. }
+    rewrite /interp_expr /=.
+    iSpecialize ("H" $! j K).
+    rewrite /env_subst !fmap_empty !subst_p_empty.
+    iMod ("H" with "Hj"). done.
+  Qed.
+
+  Lemma interp_arrow_interp_alt τ1 τ2 Δ vv ρ :
+    spec_ctx ρ -∗
+    (interp ⊤ ⊤ (TArrow τ1 τ2) Δ vv -∗ interp_arrow_alt (interp ⊤ ⊤ τ1) τ2 Δ vv).
+  Proof.
+    iIntros "#Hs /= #Hvv". iAlways.
+    iIntros (ww) "Hww".
+    iApply (related_ret ⊤).
+    by iApply "Hvv".
+  Qed.
+  Lemma interp_arrow_alt_interp τ1 τ2 Δ vv ρ :
+    spec_ctx ρ -∗
+    (interp_arrow_alt (interp ⊤ ⊤ τ1) τ2 Δ vv -∗ interp ⊤ ⊤ (TArrow τ1 τ2) Δ vv).
+  Proof.
+    iIntros "#Hs /= #Hvv". iAlways.
+    iIntros (ww) "Hww".
+    iApply (interp_expr_wat with "Hs").
+    by iApply "Hvv".
+  Qed.
+
+  Fixpoint interp_alt (τ : type) : listC D -n> D :=
+    match τ return _ with
+    | TUnit => interp_unit
+    | TNat => interp_nat
+    | TBool => interp_bool
+    | TProd τ1 τ2 => interp_prod (interp_alt τ1) (interp_alt τ2)
+    | TSum τ1 τ2 => interp_sum (interp_alt τ1) (interp_alt τ2)
+    | TArrow τ1 τ2 =>
+      interp_arrow_alt (interp_alt τ1) τ2
+    | TVar x => ctx_lookup x
+    | TForall τ' => interp_forall ⊤ ⊤ (interp_alt τ')
+    | TExists τ' => interp_exists (interp_alt τ')
+    | TRec τ' => interp_rec (interp_alt τ')
+    | Tref τ' => interp_ref (interp_alt τ')
+    end.
+
+  Global Instance interp_alt_persistent τ Δ vv :
+    Persistent (interp_alt τ Δ vv).
+  Proof.
+    revert vv Δ; induction τ=> vv Δ; simpl; try apply _.
+    rewrite /Persistent /interp_rec fixpoint_unfold /interp_rec1 /=. eauto.
+  Qed.
+    
+  Ltac mononess :=
+    repeat match goal with
+    (* | |- envs_entails _ ((∃ _: _, _) -∗ (∃ _: _, _)) => *)
+    (*   iApply exist_wand; iIntros (?) *)
+    (* | |- envs_entails _ ((∀ _: _, _) -∗ (∀ _: _, _)) => *)
+    (*   iApply forall_wand; iIntros (?) *)
+    (* | |- envs_entails _ ((_ ∧ _) -∗ (_ ∧ _)) => iApply and_wand *)
+    | |- envs_entails _ ((_ ∨ _) -∗ (_ ∨ _)) => iApply or_wand
+    (* | |- envs_entails _ ((_ → _) -∗ (_ → _)) => iApply impl_wand' *)
+    | |- envs_entails _ ((_ -∗ _) -∗ (_ -∗ _)) => iApply wand_wand
+    | |- envs_entails _ ((WP _ @ _ {{ _ }}) -∗ (WP _ @ _ {{ _ }})) =>
+      iApply wp_wand_flipped; iIntros (?)
+    | |- envs_entails _ ((▷ _) -∗ (▷ _)) => iApply later_wand; iNext
+    | |- envs_entails _ ((□ _)%I -∗ (□ _)%I) => iApply persistently_wand
+    | |- envs_entails _ ((|={_}=> _ ) -∗ (|={_}=> _ )) => iApply fupd_wand
+    | |- envs_entails _ ((_ ∗ _) -∗ (_ ∗ _)) => iApply sep_wand
+    (* | |- (inv _ _)%I ≡ (inv _ _)%I => apply (contractive_proper _) *)
+    end.
+
+  Local Ltac solve_clause :=
+    first
+      [ iDestruct ("IH" $! _ _) as "[IH' _]";
+        iApply "IH'"
+      | iDestruct ("IH1" $! _ _) as "[IH' _]";
+        iApply "IH'"
+      | iDestruct ("IH" $! _ _) as "[_ IH']";
+        iApply "IH'"
+      | iDestruct ("IH1" $! _ _) as "[_ IH']";
+        iApply "IH'" ].
+
+  (* TODO: Something like Proper  and ==>  but inside Iris*)
+  Lemma interp_interp_alt τ Δ vv ρ :
+    spec_ctx ρ -∗ (interp ⊤ ⊤ τ Δ vv ↔ interp_alt τ Δ vv).
+  Proof.
+    iIntros "#Hspec".
+    iInduction (τ) as [] "IH" forall (vv Δ); simpl; eauto.
+    - iSplit.
+      iApply exist_impl; iIntros (?).
+      iApply exist_impl; iIntros (?).
+      iApply and_impl; eauto.
+      iApply and_impl; eauto.
+      iDestruct ("IH" $! a Δ) as "[IH'' IH']". done.
+      admit.
+    - iSplitL; mononess; eauto; solve_clause.
+    - iSplitL.
+      { mononess. iAlways.
+        mononess. rewrite !impl_wand.
+        mononess. solve_clause.
+        rewrite bin_log_related_eq /bin_log_related_def.
+        iIntros "HZ" (? ?) "? #Hg".
+        rewrite /env_subst !Closed_subst_p_id.
+        iApply "HZ". }
+      { mononess. iAlways.
+        mononess. rewrite !impl_wand.
+        mononess. solve_clause.
+        iApply (interp_expr_wat with "Hspec"). }
+    - iSplitL; mononess; eauto.
+      iLöb as "FP".
+      rewrite {2}fixpoint_unfold.
+      rewrite {2}(fixpoint_unfold (interp_rec1 (interp_alt τ) Δ)).
+      rewrite /interp_rec1 /=.
+      mononess; eauto.
+      admit. (* This is very annoying, our IH is not strong enough to deal with this *)
+    - iSplitL; mononess; eauto; solve_clause.
+    - iSplitL.
+      { repeat (mononess; try iAlways; rewrite ?impl_wand /=; eauto).
+        rewrite /interp_expr.
+        repeat (mononess; try iAlways; rewrite ?impl_wand /=; eauto). 
+        solve_clause. }
+      { repeat (mononess; try iAlways; rewrite ?impl_wand /=; eauto).
+        rewrite /interp_expr.
+        repeat (mononess; try iAlways; rewrite ?impl_wand /=; eauto). 
+        solve_clause. }
+    - iSplitL; mononess; eauto; solve_clause.
+    - iSplitL; mononess; eauto.
+      admit. admit. (* THIS IS NOT TRUE *)
+  Admitted.
+
+  (* Notation "〚 τ 〛" := (interp_alt τ). *)
+
+  Lemma bin_log_related_arrow_val_alt Δ Γ E (f x f' x' : binder) (e e' eb eb' : expr) (τ τ' : type) :
+    e = (rec: f x := eb)%E →
+    e' = (rec: f' x' := eb')%E →
+    Closed ∅ e →
+    Closed ∅ e' →
+    □(∀ v1 v2, interp_alt τ Δ (v1, v2) -∗
+      {Δ;Γ} ⊨ App e (of_val v1) ≤log≤ App e' (of_val v2) : τ') -∗
+    {E;Δ;Γ} ⊨ e ≤log≤ e' : TArrow τ τ'.
+  Proof.
+    iIntros (????) "#H".
+    subst e e'.
+    rewrite bin_log_related_eq.
+    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj".
+    cbn-[subst_p].
+    iModIntro.
+    rewrite {2}/env_subst Closed_subst_p_id.
+    iApply wp_value.
+    { rewrite /IntoVal. simpl. erewrite decide_left. done. }
+    rewrite /env_subst Closed_subst_p_id.
+    iExists (RecV f' x' eb').
+    iFrame "Hj". iAlways. iIntros ([v1 v2]) "Hvv".
+    iAssert (interp_alt τ Δ (v1, v2)) with "[Hvv]" as "Hvv".
+    { by iApply interp_interp_alt. }
+    iSpecialize ("H" $! v1 v2 with "Hvv Hs []").
+    { iAlways. iApply "HΓ". }
+    assert (Closed ∅ ((rec: f x := eb) v1)).
+    { unfold Closed in *. simpl.
+      intros. split_and?; auto. apply of_val_closed. }
+    assert (Closed ∅ ((rec: f' x' := eb') v2)).
+    { unfold Closed in *. simpl.
+      intros. split_and?; auto. apply of_val_closed. }
+    rewrite /env_subst. rewrite !Closed_subst_p_id. done.
+  Qed.
+
+  Lemma bin_log_related_val_alt Δ Γ E e e' τ v v' :
+    to_val e = Some v →
+    to_val e' = Some v' →
+    (|={E}=> interp_alt τ Δ (v, v')) ⊢ {E;Δ;Γ} ⊨ e ≤log≤ e' : τ.
+  Proof.
+    iIntros (He He') "Hτ".
+    iMod "Hτ" as "Hτ".
+    apply bin_log_related_spec_ctx.
+    iDestruct 1 as (ρ) "#Hρ".
+    rewrite -(related_ret ⊤).
+    iApply (interp_ret ⊤); eauto.
+    by iApply interp_interp_alt.
+  Qed.
 
+  (*****************************************************)
   (* TODO: interesting fact?
    bin_log_related_arrow_val can be proved using bin_log_related_arrow
    specifically, at some point we can update
@@ -16,7 +330,7 @@ Section test.
     e' = (rec: f' x' := eb')%E →
     Closed ∅ e →
     Closed ∅ e' →
-    □(∀ v1 v2, ⟦ τ ⟧ Δ (v1, v2) -∗
+    □(∀ v1 v2, interp_alt τ Δ (v1, v2) -∗
       {Δ;Γ} ⊨ App e (of_val v1) ≤log≤ App e' (of_val v2) : τ') -∗
     {E;Δ;Γ} ⊨ e ≤log≤ e' : TArrow τ τ'.
   Proof.