logrel.v 8.5 KB
 Amin Timany committed Dec 14, 2017 1 2 ``````From iris.proofmode Require Import tactics. From iris.program_logic Require Export weakestpre. `````` Amin Timany committed Dec 14, 2017 3 ``````From iris_examples.logrel.F_mu_ref Require Export rules typing. `````` Amin Timany committed Dec 14, 2017 4 5 6 7 8 9 10 11 ``````From iris.algebra Require Import list. Import uPred. Definition logN : namespace := nroot .@ "logN". (** interp : is a unary logical relation. *) Section logrel. Context `{heapG Σ}. `````` Robbert Krebbers committed Jun 18, 2019 12 `````` Notation D := (valO -n> iProp Σ). `````` Amin Timany committed Dec 14, 2017 13 `````` Implicit Types τi : D. `````` Robbert Krebbers committed Jun 18, 2019 14 15 `````` Implicit Types Δ : listO D. Implicit Types interp : listO D → D. `````` Amin Timany committed Dec 14, 2017 16 `````` `````` Robbert Krebbers committed Jun 18, 2019 17 `````` Program Definition ctx_lookup (x : var) : listO D -n> D := λne Δ, `````` Amin Timany committed Dec 14, 2017 18 `````` from_option id (cconst True)%I (Δ !! x). `````` Ralf Jung committed Jun 23, 2018 19 `````` Solve Obligations with solve_proper. `````` Amin Timany committed Dec 14, 2017 20 `````` `````` Robbert Krebbers committed Jun 18, 2019 21 `````` Definition interp_unit : listO D -n> D := λne Δ w, ⌜w = UnitV⌝%I. `````` Amin Timany committed Dec 14, 2017 22 23 `````` Program Definition interp_prod `````` Robbert Krebbers committed Jun 18, 2019 24 `````` (interp1 interp2 : listO D -n> D) : listO D -n> D := λne Δ w, `````` Amin Timany committed Dec 14, 2017 25 26 27 28 `````` (∃ w1 w2, ⌜w = PairV w1 w2⌝ ∧ interp1 Δ w1 ∧ interp2 Δ w2)%I. Solve Obligations with repeat intros ?; simpl; solve_proper. Program Definition interp_sum `````` Robbert Krebbers committed Jun 18, 2019 29 `````` (interp1 interp2 : listO D -n> D) : listO D -n> D := λne Δ w, `````` Amin Timany committed Dec 14, 2017 30 31 32 33 `````` ((∃ w1, ⌜w = InjLV w1⌝ ∧ interp1 Δ w1) ∨ (∃ w2, ⌜w = InjRV w2⌝ ∧ interp2 Δ w2))%I. Solve Obligations with repeat intros ?; simpl; solve_proper. Program Definition interp_arrow `````` Robbert Krebbers committed Jun 18, 2019 34 `````` (interp1 interp2 : listO D -n> D) : listO D -n> D := λne Δ w, `````` Amin Timany committed Dec 14, 2017 35 36 37 38 `````` (□ ∀ v, interp1 Δ v → WP App (# w) (# v) {{ interp2 Δ }})%I. Solve Obligations with repeat intros ?; simpl; solve_proper. Program Definition interp_forall `````` Robbert Krebbers committed Jun 18, 2019 39 `````` (interp : listO D -n> D) : listO D -n> D := λne Δ w, `````` Amin Timany committed Dec 14, 2017 40 41 42 43 44 `````` (□ ∀ τi : D, ⌜(∀ v, Persistent (τi v))⌝ → WP TApp (# w) {{ interp (τi :: Δ) }})%I. Solve Obligations with repeat intros ?; simpl; solve_proper. Definition interp_rec1 `````` Robbert Krebbers committed Jun 18, 2019 45 `````` (interp : listO D -n> D) (Δ : listO D) (τi : D) : D := λne w, `````` Amin Timany committed Dec 14, 2017 46 47 48 `````` (□ (∃ v, ⌜w = FoldV v⌝ ∧ ▷ interp (τi :: Δ) v))%I. Global Instance interp_rec1_contractive `````` Robbert Krebbers committed Jun 18, 2019 49 `````` (interp : listO D -n> D) (Δ : listO D) : Contractive (interp_rec1 interp Δ). `````` Amin Timany committed Dec 14, 2017 50 51 `````` Proof. by solve_contractive. Qed. `````` Ralf Jung committed Jun 23, 2018 52 `````` `````` Robbert Krebbers committed Jun 18, 2019 53 `````` Lemma fixpoint_interp_rec1_eq (interp : listO D -n> D) Δ x : `````` Ralf Jung committed Jun 23, 2018 54 55 56 `````` fixpoint (interp_rec1 interp Δ) x ≡ interp_rec1 interp Δ (fixpoint (interp_rec1 interp Δ)) x. Proof. exact: (fixpoint_unfold (interp_rec1 interp Δ) x). Qed. `````` Robbert Krebbers committed Jun 18, 2019 57 `````` Program Definition interp_rec (interp : listO D -n> D) : listO D -n> D := λne Δ, `````` Amin Timany committed Dec 14, 2017 58 59 60 61 62 63 64 65 66 67 `````` fixpoint (interp_rec1 interp Δ). Next Obligation. intros interp n Δ1 Δ2 HΔ; apply fixpoint_ne => τi w. solve_proper. Qed. Program Definition interp_ref_inv (l : loc) : D -n> iProp Σ := λne τi, (∃ v, l ↦ v ∗ τi v)%I. Solve Obligations with solve_proper. Program Definition interp_ref `````` Robbert Krebbers committed Jun 18, 2019 68 `````` (interp : listO D -n> D) : listO D -n> D := λne Δ w, `````` Amin Timany committed Dec 14, 2017 69 70 71 `````` (∃ l, ⌜w = LocV l⌝ ∧ inv (logN .@ l) (interp_ref_inv l (interp Δ)))%I. Solve Obligations with solve_proper. `````` Robbert Krebbers committed Jun 18, 2019 72 `````` Fixpoint interp (τ : type) : listO D -n> D := `````` Amin Timany committed Dec 14, 2017 73 74 75 76 77 78 79 80 81 82 83 84 85 `````` match τ return _ with | TUnit => interp_unit | TProd τ1 τ2 => interp_prod (interp τ1) (interp τ2) | TSum τ1 τ2 => interp_sum (interp τ1) (interp τ2) | TArrow τ1 τ2 => interp_arrow (interp τ1) (interp τ2) | TVar x => ctx_lookup x | TForall τ' => interp_forall (interp τ') | TRec τ' => interp_rec (interp τ') | Tref τ' => interp_ref (interp τ') end. Notation "⟦ τ ⟧" := (interp τ). Definition interp_env (Γ : list type) `````` Robbert Krebbers committed Jun 18, 2019 86 `````` (Δ : listO D) (vs : list val) : iProp Σ := `````` Amin Timany committed Dec 14, 2017 87 88 89 `````` (⌜length Γ = length vs⌝ ∗ [∗] zip_with (λ τ, ⟦ τ ⟧ Δ) Γ vs)%I. Notation "⟦ Γ ⟧*" := (interp_env Γ). `````` Robbert Krebbers committed Jun 18, 2019 90 `````` Definition interp_expr (τ : type) (Δ : listO D) (e : expr) : iProp Σ := `````` Amin Timany committed Dec 14, 2017 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 `````` WP e {{ ⟦ τ ⟧ Δ }}%I. Class env_Persistent Δ := ctx_persistent : Forall (λ τi, ∀ v, Persistent (τi v)) Δ. Global Instance ctx_persistent_nil : env_Persistent []. Proof. by constructor. Qed. Global Instance ctx_persistent_cons τi Δ : (∀ v, Persistent (τi v)) → env_Persistent Δ → env_Persistent (τi :: Δ). Proof. by constructor. Qed. Global Instance ctx_persistent_lookup Δ x v : env_Persistent Δ → Persistent (ctx_lookup x Δ v). Proof. intros HΔ; revert x; induction HΔ=>-[|?] /=; apply _. Qed. Global Instance interp_persistent τ Δ v : env_Persistent Δ → Persistent (⟦ τ ⟧ Δ v). Proof. revert v Δ; induction τ=> v Δ HΔ; simpl; try apply _. `````` Ralf Jung committed Jun 23, 2018 107 `````` rewrite /Persistent fixpoint_interp_rec1_eq /interp_rec1 /= intuitionistically_into_persistently. `````` Amin Timany committed Dec 14, 2017 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 `````` by apply persistently_intro'. Qed. Global Instance interp_env_base_persistent Δ Γ vs : env_Persistent Δ → TCForall Persistent (zip_with (λ τ, ⟦ τ ⟧ Δ) Γ vs). Proof. intros HΔ. revert vs. induction Γ => vs; simpl; destruct vs; constructor; apply _. Qed. Global Instance interp_env_persistent Γ Δ vs : env_Persistent Δ → Persistent (⟦ Γ ⟧* Δ vs) := _. Lemma interp_weaken Δ1 Π Δ2 τ : ⟦ τ.[upn (length Δ1) (ren (+ length Π))] ⟧ (Δ1 ++ Π ++ Δ2) ≡ ⟦ τ ⟧ (Δ1 ++ Δ2). Proof. revert Δ1 Π Δ2. induction τ=> Δ1 Π Δ2; simpl; auto. - intros w; simpl; properness; auto. by apply IHτ1. by apply IHτ2. - intros w; simpl; properness; auto. by apply IHτ1. by apply IHτ2. - intros w; simpl; properness; auto. by apply IHτ1. by apply IHτ2. - apply fixpoint_proper=> τi w /=. properness; auto. apply (IHτ (_ :: _)). - rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl. { by rewrite !lookup_app_l. } `````` Ralf Jung committed Jun 23, 2018 131 `````` (* FIXME: Ideally we wouldn't have to do this kinf of surgery. *) `````` Robbert Krebbers committed Jun 18, 2019 132 `````` change (bi_ofeO (uPredI (iResUR Σ))) with (uPredO (iResUR Σ)). `````` Ralf Jung committed Jun 23, 2018 133 `````` rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia. `````` Amin Timany committed Dec 14, 2017 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 `````` - intros w; simpl; properness; auto. apply (IHτ (_ :: _)). - intros w; simpl; properness; auto. by apply IHτ. Qed. Lemma interp_subst_up Δ1 Δ2 τ τ' : ⟦ τ ⟧ (Δ1 ++ interp τ' Δ2 :: Δ2) ≡ ⟦ τ.[upn (length Δ1) (τ' .: ids)] ⟧ (Δ1 ++ Δ2). Proof. revert Δ1 Δ2; induction τ=> Δ1 Δ2; simpl. - done. - intros w; simpl; properness; auto. by apply IHτ1. by apply IHτ2. - intros w; simpl; properness; auto. by apply IHτ1. by apply IHτ2. - intros w; simpl; properness; auto. by apply IHτ1. by apply IHτ2. - apply fixpoint_proper=> τi w /=. properness; auto. apply (IHτ (_ :: _)). - rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl. { by rewrite !lookup_app_l. } `````` Ralf Jung committed Jun 23, 2018 151 `````` (* FIXME: Ideally we wouldn't have to do this kinf of surgery. *) `````` Robbert Krebbers committed Jun 18, 2019 152 `````` change (bi_ofeO (uPredI (iResUR Σ))) with (uPredO (iResUR Σ)). `````` Amin Timany committed Dec 14, 2017 153 `````` rewrite !lookup_app_r; [|lia ..]. `````` Ralf Jung committed Jun 23, 2018 154 `````` case EQ: (x - length Δ1) => [|n]; simpl. `````` Amin Timany committed Dec 14, 2017 155 `````` { symmetry. asimpl. apply (interp_weaken [] Δ1 Δ2 τ'). } `````` Robbert Krebbers committed Jun 18, 2019 156 `````` change (bi_ofeO (uPredI (iResUR Σ))) with (uPredO (iResUR Σ)). `````` Ralf Jung committed Jun 23, 2018 157 `````` rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia. `````` Amin Timany committed Dec 14, 2017 158 159 160 161 `````` - intros w; simpl; properness; auto. apply (IHτ (_ :: _)). - intros w; simpl; properness; auto. by apply IHτ. Qed. `````` Ralf Jung committed Jun 23, 2018 162 `````` Lemma interp_subst Δ2 τ τ' v : ⟦ τ ⟧ (⟦ τ' ⟧ Δ2 :: Δ2) v ≡ ⟦ τ.[τ'/] ⟧ Δ2 v. `````` Amin Timany committed Dec 14, 2017 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 `````` Proof. apply (interp_subst_up []). Qed. Lemma interp_env_length Δ Γ vs : ⟦ Γ ⟧* Δ vs ⊢ ⌜length Γ = length vs⌝. Proof. by iIntros "[% ?]". Qed. Lemma interp_env_Some_l Δ Γ vs x τ : Γ !! x = Some τ → ⟦ Γ ⟧* Δ vs ⊢ ∃ v, ⌜vs !! x = Some v⌝ ∧ ⟦ τ ⟧ Δ v. Proof. iIntros (?) "[Hlen HΓ]"; iDestruct "Hlen" as %Hlen. destruct (lookup_lt_is_Some_2 vs x) as [v Hv]. { by rewrite -Hlen; apply lookup_lt_Some with τ. } iExists v; iSplit. done. iApply (big_sepL_elem_of with "HΓ"). apply elem_of_list_lookup_2 with x. rewrite lookup_zip_with; by simplify_option_eq. Qed. Lemma interp_env_nil Δ : (⟦ [] ⟧* Δ [])%I. Proof. iSplit; simpl; auto. Qed. Lemma interp_env_cons Δ Γ vs τ v : ⟦ τ :: Γ ⟧* Δ (v :: vs) ⊣⊢ ⟦ τ ⟧ Δ v ∗ ⟦ Γ ⟧* Δ vs. Proof. rewrite /interp_env /= (assoc _ (⟦ _ ⟧ _ _)) -(comm _ ⌜(_ = _)⌝%I) -assoc. `````` Robbert Krebbers committed Nov 08, 2018 185 `````` by apply sep_proper; [apply pure_proper; lia|]. `````` Amin Timany committed Dec 14, 2017 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 `````` Qed. Lemma interp_env_ren Δ (Γ : list type) (vs : list val) τi : ⟦ subst (ren (+1)) <\$> Γ ⟧* (τi :: Δ) vs ⊣⊢ ⟦ Γ ⟧* Δ vs. Proof. apply sep_proper; [apply pure_proper; by rewrite fmap_length|]. revert Δ vs τi; induction Γ=> Δ [|v vs] τi; csimpl; auto. apply sep_proper; auto. apply (interp_weaken [] [τi] Δ). Qed. End logrel. Typeclasses Opaque interp_env. Notation "⟦ τ ⟧" := (interp τ). Notation "⟦ τ ⟧ₑ" := (interp_expr τ). Notation "⟦ Γ ⟧*" := (interp_env Γ).``````