logrel_binary.v 9.98 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.
Ralf Jung's avatar
Ralf Jung committed
3
From iris.base_logic Require Export invariants.
Amin Timany's avatar
Amin Timany committed
4
From iris_examples.logrel.F_mu_ref Require Export rules_binary typing.
Amin Timany's avatar
Amin Timany committed
5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27
From iris.algebra Require Import list.
From stdpp Require Import tactics.
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).

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

(** interp : is a unary logical relation. *)
Section logrel.
  Context `{heapG Σ, cfgSG Σ}.
Robbert Krebbers's avatar
Robbert Krebbers committed
28
  Notation D := (prodO valO valO -n> iProp Σ).
Amin Timany's avatar
Amin Timany committed
29
  Implicit Types τi : D.
Robbert Krebbers's avatar
Robbert Krebbers committed
30 31
  Implicit Types Δ : listO D.
  Implicit Types interp : listO D  D.
Amin Timany's avatar
Amin Timany committed
32

Robbert Krebbers's avatar
Robbert Krebbers committed
33
  Definition interp_expr (τi : listO D -n> D) (Δ : listO D)
Amin Timany's avatar
Amin Timany committed
34 35 36 37 38 39 40
      (ee : expr * expr) : iProp Σ := ( K,
     fill K (ee.2) 
    WP ee.1 {{ v,  v',  fill K (of_val v')  τi Δ (v, v') }})%I.
  Global Instance interp_expr_ne n :
    Proper (dist n ==> dist n ==> (=) ==> dist n) interp_expr.
  Proof. solve_proper. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
41
  Program Definition ctx_lookup (x : var) : listO D -n> D := λne Δ,
Amin Timany's avatar
Amin Timany committed
42
    from_option id (cconst True)%I (Δ !! x).
Ralf Jung's avatar
Ralf Jung committed
43
  Solve Obligations with solve_proper.
Amin Timany's avatar
Amin Timany committed
44

Robbert Krebbers's avatar
Robbert Krebbers committed
45
  Program Definition interp_unit : listO D -n> D := λne Δ ww,
Amin Timany's avatar
Amin Timany committed
46 47 48 49
    (ww.1 = UnitV  ww.2 = UnitV)%I.
  Solve Obligations with solve_proper_alt.

  Program Definition interp_prod
Robbert Krebbers's avatar
Robbert Krebbers committed
50
      (interp1 interp2 : listO D -n> D) : listO D -n> D := λne Δ ww,
Amin Timany's avatar
Amin Timany committed
51 52 53 54 55
    ( vv1 vv2, ww = (PairV (vv1.1) (vv2.1), PairV (vv1.2) (vv2.2)) 
                interp1 Δ vv1  interp2 Δ vv2)%I.
  Solve Obligations with repeat intros ?; simpl; auto_equiv.

  Program Definition interp_sum
Robbert Krebbers's avatar
Robbert Krebbers committed
56
      (interp1 interp2 : listO D -n> D) : listO D -n> D := λne Δ ww,
Amin Timany's avatar
Amin Timany committed
57 58 59 60 61
    (( vv, ww = (InjLV (vv.1), InjLV (vv.2))  interp1 Δ vv) 
     ( vv, ww = (InjRV (vv.1), InjRV (vv.2))  interp2 Δ vv))%I.
  Solve Obligations with repeat intros ?; simpl; auto_equiv.

  Program Definition interp_arrow
Robbert Krebbers's avatar
Robbert Krebbers committed
62
          (interp1 interp2 : listO D -n> D) : listO D -n> D :=
Amin Timany's avatar
Amin Timany committed
63 64 65 66 67 68 69 70
    λne Δ ww,
    (  vv, interp1 Δ vv 
             interp_expr
               interp2 Δ (App (of_val (ww.1)) (of_val (vv.1)),
                          App (of_val (ww.2)) (of_val (vv.2))))%I.
  Solve Obligations with repeat intros ?; simpl; auto_equiv.

  Program Definition interp_forall
Robbert Krebbers's avatar
Robbert Krebbers committed
71
      (interp : listO D -n> D) : listO D -n> D := λne Δ ww,
Amin Timany's avatar
Amin Timany committed
72 73 74 75 76 77 78
    (  τi,
           ww, Persistent (τi ww) 
          interp_expr
            interp (τi :: Δ) (TApp (of_val (ww.1)), TApp (of_val (ww.2))))%I.
  Solve Obligations with repeat intros ?; simpl; auto_equiv.

  Program Definition interp_rec1
Robbert Krebbers's avatar
Robbert Krebbers committed
79
      (interp : listO D -n> D) (Δ : listO D) (τi : D) : D := λne ww,
Amin Timany's avatar
Amin Timany committed
80 81 82 83
    (  vv, ww = (FoldV (vv.1), FoldV (vv.2))   interp (τi :: Δ) vv)%I.
  Solve Obligations with repeat intros ?; simpl; auto_equiv.

  Global Instance interp_rec1_contractive
Robbert Krebbers's avatar
Robbert Krebbers committed
84
    (interp : listO D -n> D) (Δ : listO D) : Contractive (interp_rec1 interp Δ).
Amin Timany's avatar
Amin Timany committed
85 86
  Proof. by solve_contractive. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
87
  Lemma fixpoint_interp_rec1_eq (interp : listO D -n> D) Δ x :
Ralf Jung's avatar
Ralf Jung committed
88 89 90
    fixpoint (interp_rec1 interp Δ) x  interp_rec1 interp Δ (fixpoint (interp_rec1 interp Δ)) x.
  Proof. exact: (fixpoint_unfold (interp_rec1 interp Δ) x). Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
91
  Program Definition interp_rec (interp : listO D -n> D) : listO D -n> D := λne Δ,
Amin Timany's avatar
Amin Timany committed
92 93 94 95 96 97 98 99 100 101
    fixpoint (interp_rec1 interp Δ).
  Next Obligation.
    intros interp n Δ1 Δ2 HΔ; apply fixpoint_ne => τi ww. solve_proper.
  Qed.

  Program Definition interp_ref_inv (ll : loc * loc) : D -n> iProp Σ := λne τi,
    ( vv, ll.1  vv.1  ll.2 ↦ₛ vv.2  τi vv)%I.
  Solve Obligations with repeat intros ?; simpl; auto_equiv.

  Program Definition interp_ref
Robbert Krebbers's avatar
Robbert Krebbers committed
102
      (interp : listO D -n> D) : listO D -n> D := λne Δ ww,
Amin Timany's avatar
Amin Timany committed
103 104 105 106
    ( ll, ww = (LocV (ll.1), LocV (ll.2)) 
           inv (logN .@ ll) (interp_ref_inv ll (interp Δ)))%I.
  Solve Obligations with repeat intros ?; simpl; auto_equiv.

Robbert Krebbers's avatar
Robbert Krebbers committed
107
  Fixpoint interp (τ : type) : listO D -n> D :=
Amin Timany's avatar
Amin Timany committed
108 109 110 111 112 113 114 115 116 117 118 119 120
    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's avatar
Robbert Krebbers committed
121
      (Δ : listO D) (vvs : list (val * val)) : iProp Σ :=
Amin Timany's avatar
Amin Timany committed
122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138
    (length Γ = length vvs  [] zip_with (λ τ,  τ  Δ) Γ vvs)%I.
  Notation "⟦ Γ ⟧*" := (interp_env Γ).

  Class env_Persistent Δ :=
    ctx_persistentP : Forall (λ τi,  vv, Persistent (τi vv)) Δ.
  Global Instance ctx_persistent_nil : env_Persistent [].
  Proof. by constructor. Qed.
  Global Instance ctx_persistent_cons τi Δ :
    ( vv, Persistent (τi vv))  env_Persistent Δ  env_Persistent (τi :: Δ).
  Proof. by constructor. Qed.
  Global Instance ctx_persistent_lookup Δ x vv :
    env_Persistent Δ  Persistent (ctx_lookup x Δ vv).
  Proof. intros HΔ; revert x; induction HΔ=>-[|?] /=; apply _. Qed.
  Global Instance interp_persistent τ Δ vv :
    env_Persistent Δ  Persistent ( τ  Δ vv).
  Proof.
    revert vv Δ; induction τ=> vv Δ HΔ; simpl; try apply _.
Ralf Jung's avatar
Ralf Jung committed
139
    rewrite /Persistent fixpoint_interp_rec1_eq /interp_rec1 /= intuitionistically_into_persistently.
Amin Timany's avatar
Amin Timany committed
140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163
    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 Γ Δ vvs :
    env_Persistent Δ  Persistent ( Γ * Δ vvs) := _.

  Lemma interp_weaken Δ1 Π Δ2 τ :
     τ.[upn (length Δ1) (ren (+ length Π))]  (Δ1 ++ Π ++ Δ2)
      τ  (Δ1 ++ Δ2).
  Proof.
    revert Δ1 Π Δ2. induction τ=> Δ1 Π Δ2; simpl; auto.
    - intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
    - intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
    - unfold interp_expr.
      intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
    - apply fixpoint_proper=> τi ww /=.
      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
164
      (* FIXME: Ideally we wouldn't have to do this kinf of surgery. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
165
      change (bi_ofeO (uPredI (iResUR Σ))) with (uPredO (iResUR Σ)).
Ralf Jung's avatar
Ralf Jung committed
166
      rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia.
Amin Timany's avatar
Amin Timany committed
167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184
    - unfold interp_expr.
      intros ww; simpl; properness; auto. by apply (IHτ (_ :: _)).
    - intros ww; 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; auto.
    - intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
    - intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
    - unfold interp_expr.
      intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
    - apply fixpoint_proper=> τi ww /=.
      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
185
      (* FIXME: Ideally we wouldn't have to do this kinf of surgery. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
186
      change (bi_ofeO (uPredI (iResUR Σ))) with (uPredO (iResUR Σ)).
Amin Timany's avatar
Amin Timany committed
187
      rewrite !lookup_app_r; [|lia ..].
Ralf Jung's avatar
Ralf Jung committed
188
      case EQ: (x - length Δ1) => [|n]; simpl.
Amin Timany's avatar
Amin Timany committed
189
      { symmetry. asimpl. apply (interp_weaken [] Δ1 Δ2 τ'). }
Robbert Krebbers's avatar
Robbert Krebbers committed
190
      change (bi_ofeO (uPredI (iResUR Σ))) with (uPredO (iResUR Σ)).
Ralf Jung's avatar
Ralf Jung committed
191
      rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia.
Amin Timany's avatar
Amin Timany committed
192 193 194 195 196
    - unfold interp_expr.
      intros ww; simpl; properness; auto. apply (IHτ (_ :: _)).
    - intros ww; simpl; properness; auto. by apply IHτ.
  Qed.

Ralf Jung's avatar
Ralf Jung committed
197
  Lemma interp_subst Δ2 τ τ' v :  τ  ( τ'  Δ2 :: Δ2) v   τ.[τ'/]  Δ2 v.
Amin Timany's avatar
Amin Timany committed
198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219
  Proof. apply (interp_subst_up []). Qed.

  Lemma interp_env_length Δ Γ vvs :  Γ * Δ vvs  length Γ = length vvs.
  Proof. by iIntros "[% ?]". Qed.

  Lemma interp_env_Some_l Δ Γ vvs x τ :
    Γ !! x = Some τ   Γ * Δ vvs   vv, vvs !! x = Some vv   τ  Δ vv.
  Proof.
    iIntros (?) "[Hlen HΓ]"; iDestruct "Hlen" as %Hlen.
    destruct (lookup_lt_is_Some_2 vvs 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 Δ :  [] * Δ [].
  Proof. iSplit; simpl; auto. Qed.
  Lemma interp_env_cons Δ Γ vvs τ vv :
     τ :: Γ * Δ (vv :: vvs)   τ  Δ vv   Γ * Δ vvs.
  Proof.
    rewrite /interp_env /= (assoc _ ( _  _ _)) -(comm _ _ = _%I) -assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
220
    by apply sep_proper; [apply pure_proper; lia|].
Amin Timany's avatar
Amin Timany committed
221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236
  Qed.

  Lemma interp_env_ren Δ (Γ : list type) vvs τi :
     subst (ren (+1)) <$> Γ * (τi :: Δ) vvs   Γ * Δ vvs.
  Proof.
    apply sep_proper; [apply pure_proper; by rewrite fmap_length|].
    revert Δ vvs τ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 (interp τ)).
Notation "⟦ Γ ⟧*" := (interp_env Γ).