From 134a7e5170da7f4897c4d384c13ae627b8d766b4 Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Fri, 12 Jan 2018 17:04:17 +0100 Subject: [PATCH] Experimenting with an `alternative' value interpretation --- theories/tests/rules.v | 320 ++++++++++++++++++++++++++++++++++++++++- 1 file changed, 317 insertions(+), 3 deletions(-) diff --git a/theories/tests/rules.v b/theories/tests/rules.v index dbcf3dc..515c702 100644 --- a/theories/tests/rules.v +++ b/theories/tests/rules.v @@ -1,11 +1,325 @@ 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 + (*****************************************************) + (* TODO: interesting fact? + bin_log_related_arrow_val can be proved using bin_log_related_arrow specifically, at some point we can update {Δ; Γ} ⊨ v1 ≤log≤ v2 : τ to @@ -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. -- GitLab