logrel.v 8.5 KB
Newer Older
Amin Timany's avatar
Amin Timany committed
1 2
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
Amin Timany's avatar
Amin Timany committed
3
From iris_examples.logrel.F_mu_ref Require Export rules typing.
Amin Timany's avatar
Amin Timany committed
4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
From iris.algebra Require Import list.
Import uPred.

Definition logN : namespace := nroot .@ "logN".

(** interp : is a unary logical relation. *)
Section logrel.
  Context `{heapG Σ}.
  Notation D := (valC -n> iProp Σ).
  Implicit Types τi : D.
  Implicit Types Δ : listC D.
  Implicit Types interp : listC D  D.

  Program Definition ctx_lookup (x : var) : listC D -n> D := λne Δ,
    from_option id (cconst True)%I (Δ !! x).
Ralf Jung's avatar
Ralf Jung committed
19
  Solve Obligations with solve_proper.
Amin Timany's avatar
Amin Timany committed
20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51

  Definition interp_unit : listC D -n> D := λne Δ w, w = UnitV%I.

  Program Definition interp_prod
      (interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ w,
    ( w1 w2, w = PairV w1 w2  interp1 Δ w1  interp2 Δ w2)%I.
  Solve Obligations with repeat intros ?; simpl; solve_proper.

  Program Definition interp_sum
      (interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ w,
    (( 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
      (interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ w,
    (  v, interp1 Δ v  WP App (# w) (# v) {{ interp2 Δ }})%I.
  Solve Obligations with repeat intros ?; simpl; solve_proper.

  Program Definition interp_forall
      (interp : listC D -n> D) : listC D -n> D := λne Δ w,
    (  τi : D,
      ( v, Persistent (τi v))  WP TApp (# w) {{ interp (τi :: Δ) }})%I.
  Solve Obligations with repeat intros ?; simpl; solve_proper.

  Definition interp_rec1
      (interp : listC D -n> D) (Δ : listC D) (τi : D) : D := λne w,
    ( ( v, w = FoldV v   interp (τi :: Δ) v))%I.

  Global Instance interp_rec1_contractive
    (interp : listC D -n> D) (Δ : listC D) : Contractive (interp_rec1 interp Δ).
  Proof. by solve_contractive. Qed.

Ralf Jung's avatar
Ralf Jung committed
52 53 54 55 56

  Lemma fixpoint_interp_rec1_eq (interp : listC D -n> D) Δ x :
    fixpoint (interp_rec1 interp Δ) x  interp_rec1 interp Δ (fixpoint (interp_rec1 interp Δ)) x.
  Proof. exact: (fixpoint_unfold (interp_rec1 interp Δ) x). Qed.

Amin Timany's avatar
Amin Timany committed
57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106
  Program Definition interp_rec (interp : listC D -n> D) : listC D -n> D := λne Δ,
    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
      (interp : listC D -n> D) : listC D -n> D := λne Δ w,
    ( l, w = LocV l  inv (logN .@ l) (interp_ref_inv l (interp Δ)))%I.
  Solve Obligations with solve_proper.

  Fixpoint interp (τ : type) : listC D -n> D :=
    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)
      (Δ : listC D) (vs : list val) : iProp Σ :=
    (length Γ = length vs  [] zip_with (λ τ,  τ  Δ) Γ vs)%I.
  Notation "⟦ Γ ⟧*" := (interp_env Γ).

  Definition interp_expr (τ : type) (Δ : listC D) (e : expr) : iProp Σ :=
    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's avatar
Ralf Jung committed
107
    rewrite /Persistent fixpoint_interp_rec1_eq /interp_rec1 /= intuitionistically_into_persistently.
Amin Timany's avatar
Amin Timany committed
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's avatar
Ralf Jung committed
131 132 133
      (* FIXME: Ideally we wouldn't have to do this kinf of surgery. *)
      change (bi_ofeC (uPredI (iResUR Σ))) with (uPredC (iResUR Σ)).
      rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia.
Amin Timany's avatar
Amin Timany committed
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's avatar
Ralf Jung committed
151 152
      (* FIXME: Ideally we wouldn't have to do this kinf of surgery. *)
      change (bi_ofeC (uPredI (iResUR Σ))) with (uPredC (iResUR Σ)).
Amin Timany's avatar
Amin Timany committed
153
      rewrite !lookup_app_r; [|lia ..].
Ralf Jung's avatar
Ralf Jung committed
154
      case EQ: (x - length Δ1) => [|n]; simpl.
Amin Timany's avatar
Amin Timany committed
155
      { symmetry. asimpl. apply (interp_weaken [] Δ1 Δ2 τ'). }
Ralf Jung's avatar
Ralf Jung committed
156 157
      change (bi_ofeC (uPredI (iResUR Σ))) with (uPredC (iResUR Σ)).
      rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia.
Amin Timany's avatar
Amin Timany committed
158 159 160 161
    - intros w; simpl; properness; auto. apply (IHτ (_ :: _)).
    - intros w; simpl; properness; auto. by apply IHτ.
  Qed.

Ralf Jung's avatar
Ralf Jung committed
162
  Lemma interp_subst Δ2 τ τ' v :  τ  ( τ'  Δ2 :: Δ2) v   τ.[τ'/]  Δ2 v.
Amin Timany's avatar
Amin Timany committed
163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200
  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.
    by apply sep_proper; [apply pure_proper; omega|].
  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 Γ).