logrel_binary.v 10.5 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
3
From iris.base_logic Require Export big_op invariants.
4
From iris_logrel.F_mu_ref_conc Require Export rules_binary typing.
5 6
From iris.algebra Require Import list.
From iris.prelude Require Import tactics.
7 8
Import uPred.

9
(* HACK: move somewhere else *)
10
Ltac auto_equiv ::=
11 12 13 14 15 16 17 18 19 20
  (* Deal with "pointwise_relation" *)
  repeat lazymatch goal with
  | |- pointwise_relation _ _ _ _ => intros ?
  end;
  (* Normalize away equalities. *)
  repeat match goal with
  | H : _ {_} _ |-  _ => apply (timeless_iff _ _) in H
  | _ => progress simplify_eq
  end;
  (* repeatedly apply congruence lemmas and use the equalities in the hypotheses. *)
21
  try (f_equiv; fast_done || auto_equiv).
22

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

25 26
(** interp : is a unary logical relation. *)
Section logrel.
27
  Context `{heapIG Σ, cfgSG Σ}.
Robbert Krebbers's avatar
Robbert Krebbers committed
28
  Notation D := (prodC valC valC -n> iProp Σ).
29 30 31 32
  Implicit Types τi : D.
  Implicit Types Δ : listC D.
  Implicit Types interp : listC D  D.

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

41 42 43 44 45 46 47 48
  Program Definition ctx_lookup (x : var) : listC D -n> D := λne Δ,
    from_option id (cconst True)%I (Δ !! x).
  Solve Obligations with solve_proper_alt.

  Program Definition interp_unit : listC D -n> D := λne Δ ww,
    (ww.1 = UnitV  ww.2 = UnitV)%I.
  Solve Obligations with solve_proper_alt.
  Program Definition interp_nat : listC D -n> D := λne Δ ww,
Amin Timany's avatar
Amin Timany committed
49
    ( n : nat, ww.1 = #nv n  ww.2 = #nv n)%I.
50 51
  Solve Obligations with solve_proper.
  Program Definition interp_bool : listC D -n> D := λne Δ ww,
Amin Timany's avatar
Amin Timany committed
52
    ( b : bool, ww.1 = #v b  ww.2 = #v b)%I.
53 54 55 56 57 58 59 60 61 62 63 64 65 66 67
  Solve Obligations with solve_proper.

  Program Definition interp_prod
      (interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ ww,
    ( vv1 vv2, ww = (PairV (vv1.1) (vv2.1), PairV (vv1.2) (vv2.2)) 
                interp1 Δ vv1  interp2 Δ vv2)%I.
  Solve Obligations with solve_proper.

  Program Definition interp_sum
      (interp1 interp2 : listC D -n> D) : listC D -n> D := λne Δ ww,
    (( vv, ww = (InjLV (vv.1), InjLV (vv.2))  interp1 Δ vv) 
     ( vv, ww = (InjRV (vv.1), InjRV (vv.2))  interp2 Δ vv))%I.
  Solve Obligations with solve_proper.

  Program Definition interp_arrow
68 69 70 71
          (interp1 interp2 : listC D -n> D) : listC D -n> D :=
    λne Δ ww,
    (  vv, interp1 Δ vv 
             interp_expr
Amin Timany's avatar
Amin Timany committed
72 73
               interp2 Δ (App (of_val (ww.1)) (of_val (vv.1)),
                          App (of_val (ww.2)) (of_val (vv.2))))%I.
74 75 76 77
  Solve Obligations with solve_proper.

  Program Definition interp_forall
      (interp : listC D -n> D) : listC D -n> D := λne Δ ww,
78 79 80
    (  τi,
          (  ww, PersistentP (τi ww)) 
          interp_expr
Amin Timany's avatar
Amin Timany committed
81
            interp (τi :: Δ) (TApp (of_val (ww.1)), TApp (of_val (ww.2))))%I.
82 83 84 85 86 87 88 89 90
  Solve Obligations with solve_proper.

  Program Definition interp_rec1
      (interp : listC D -n> D) (Δ : listC D) (τi : D) : D := λne ww,
    (  vv, ww = (FoldV (vv.1), FoldV (vv.2))   interp (τi :: Δ) vv)%I.
  Solve Obligations with solve_proper.

  Global Instance interp_rec1_contractive
    (interp : listC D -n> D) (Δ : listC D) : Contractive (interp_rec1 interp Δ).
91
  Proof.
92 93 94
    intros n τi1 τi2 Hτi ww; cbn.
    apply always_ne, exist_ne; intros vv; apply and_ne; trivial.
    apply later_contractive =>i Hi. by rewrite Hτi.
95 96
  Qed.

97 98
  Program Definition interp_rec (interp : listC D -n> D) : listC D -n> D := λne Δ,
    fixpoint (interp_rec1 interp Δ).
99
  Next Obligation.
100 101 102
    intros interp n Δ1 Δ2 HΔ; apply fixpoint_ne => τi ww. solve_proper.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
103
  Program Definition interp_ref_inv (ll : loc * loc) : D -n> iProp Σ := λne τi,
104 105 106 107 108 109
    ( vv, ll.1 ↦ᵢ vv.1  ll.2 ↦ₛ vv.2  τi vv)%I.
  Solve Obligations with solve_proper.

  Program Definition interp_ref
      (interp : listC D -n> D) : listC D -n> D := λne Δ ww,
    ( ll, ww = (LocV (ll.1), LocV (ll.2)) 
110
           inv (logN .@ ll) (interp_ref_inv ll (interp Δ)))%I.
111 112 113 114 115 116 117 118 119 120 121 122 123 124
  Solve Obligations with solve_proper.

  Fixpoint interp (τ : type) : listC D -n> D :=
    match τ return _ with
    | TUnit => interp_unit
    | TNat => interp_nat
    | TBool => interp_bool
    | 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 τ')
125
    end.
126
  Notation "⟦ τ ⟧" := (interp τ).
127

128
  Definition interp_env (Γ : list type)
Robbert Krebbers's avatar
Robbert Krebbers committed
129
      (Δ : listC D) (vvs : list (val * val)) : iProp Σ :=
130
    (length Γ = length vvs  [] zip_with (λ τ,  τ  Δ) Γ vvs)%I.
131 132 133
  Notation "⟦ Γ ⟧*" := (interp_env Γ).

  Class env_PersistentP Δ :=
134
    ctx_persistentP : Forall (λ τi,  vv, PersistentP (τi vv)) Δ.
135
  Global Instance ctx_persistent_nil : env_PersistentP [].
136 137
  Proof. by constructor. Qed.
  Global Instance ctx_persistent_cons τi Δ :
138
    ( vv, PersistentP (τi vv))  env_PersistentP Δ  env_PersistentP (τi :: Δ).
139 140
  Proof. by constructor. Qed.
  Global Instance ctx_persistent_lookup Δ x vv :
141
    env_PersistentP Δ  PersistentP (ctx_lookup x Δ vv).
142
  Proof. intros HΔ; revert x; induction HΔ=>-[|?] /=; apply _. Qed.
143 144
  Global Instance interp_persistent τ Δ vv :
    env_PersistentP Δ  PersistentP ( τ  Δ vv).
145
  Proof.
146 147 148
    revert vv Δ; induction τ=> vv Δ HΔ; simpl; try apply _.
    rewrite /PersistentP /interp_rec fixpoint_unfold /interp_rec1 /=.
    by apply always_intro'.
149
  Qed.
150 151
  Global Instance interp_env_persistent Γ Δ vvs :
    env_PersistentP Δ  PersistentP ( Γ * Δ vvs) := _.
152

153
  Lemma interp_weaken Δ1 Π Δ2 τ :
Robbert Krebbers's avatar
Robbert Krebbers committed
154
     τ.[upn (length Δ1) (ren (+ length Π))]  (Δ1 ++ Π ++ Δ2)
155
      τ  (Δ1 ++ Δ2).
156
  Proof.
157 158 159 160 161 162
    revert Δ1 Π Δ2. induction τ=> Δ1 Π Δ2; simpl; auto.
    - intros ww; simpl; properness; auto.
    - intros ww; simpl; properness; auto.
    - intros ww; simpl; properness; 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.
163 164
    - unfold interp_expr.
      intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
165 166 167 168 169
    - apply fixpoint_proper=> τi ww /=.
      properness; auto. apply (IHτ (_ :: _)).
    - rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
      { by rewrite !lookup_app_l. }
      rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia. done.
170 171
    - unfold interp_expr.
      intros ww; simpl; properness; auto. by apply (IHτ (_ :: _)).
172 173 174 175
    - intros ww; simpl; properness; auto. by apply IHτ.
  Qed.

  Lemma interp_subst_up Δ1 Δ2 τ τ' :
176
     τ  (Δ1 ++ interp τ' Δ2 :: Δ2)
Robbert Krebbers's avatar
Robbert Krebbers committed
177
      τ.[upn (length Δ1) (τ' .: ids)]  (Δ1 ++ Δ2).
178
  Proof.
179 180 181 182 183 184
    revert Δ1 Δ2; induction τ=> Δ1 Δ2; simpl; auto.
    - intros ww; simpl; properness; auto.
    - intros ww; simpl; properness; auto.
    - intros ww; simpl; properness; 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.
185 186
    - unfold interp_expr.
      intros ww; simpl; properness; auto. by apply IHτ1. by apply IHτ2.
187 188 189 190 191 192 193 194
    - apply fixpoint_proper=> τi ww /=.
      properness; auto. apply (IHτ (_ :: _)).
    - rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
      { by rewrite !lookup_app_l. }
      rewrite !lookup_app_r; [|lia ..].
      destruct (x - length Δ1) as [|n] eqn:?; simpl.
      { symmetry. asimpl. apply (interp_weaken [] Δ1 Δ2 τ'). }
      rewrite !lookup_app_r; [|lia ..]. do 2 f_equiv. lia. done.
195 196
    - unfold interp_expr.
      intros ww; simpl; properness; auto. apply (IHτ (_ :: _)).
197 198 199
    - intros ww; simpl; properness; auto. by apply IHτ.
  Qed.

200
  Lemma interp_subst Δ2 τ τ' :  τ  ( τ'  Δ2 :: Δ2)   τ.[τ'/]  Δ2.
201 202
  Proof. apply (interp_subst_up []). Qed.

203 204 205 206 207
  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.
208
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
209
    iIntros (?) "[Hlen HΓ]"; iDestruct "Hlen" as %Hlen.
210 211
    destruct (lookup_lt_is_Some_2 vvs x) as [v Hv].
    { by rewrite -Hlen; apply lookup_lt_Some with τ. }
212
    iExists v; iSplit. done. iApply (big_sep_elem_of with "HΓ").
213 214 215 216 217 218 219
    apply elem_of_list_lookup_2 with x.
    rewrite lookup_zip_with; by simplify_option_eq.
  Qed.

  Lemma interp_env_nil Δ : True   [] * Δ [].
  Proof. iIntros ""; iSplit; auto. Qed.
  Lemma interp_env_cons Δ Γ vvs τ vv :
220
     τ :: Γ * Δ (vv :: vvs) ⊣⊢  τ  Δ vv   Γ * Δ vvs.
221 222
  Proof.
    rewrite /interp_env /= (assoc _ ( _  _ _)) -(comm _ (_ = _)%I) -assoc.
223
    by apply sep_proper; [apply pure_proper; omega|].
224 225 226 227 228
  Qed.

  Lemma interp_env_ren Δ (Γ : list type) vvs τi :
     subst (ren (+1)) <$> Γ * (τi :: Δ) vvs ⊣⊢  Γ * Δ vvs.
  Proof.
229
    apply sep_proper; [apply pure_proper; by rewrite fmap_length|].
230
    revert Δ vvs τi; induction Γ=> Δ [|v vs] τi; csimpl; auto.
231
    apply sep_proper; auto. apply (interp_weaken [] [τi] Δ).
232 233
  Qed.

234
  Lemma interp_EqType_agree τ v v' Δ :
235
    env_PersistentP Δ  EqType τ  interp τ Δ (v, v')   (v = v').
236
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
237
    intros ? Hτ; revert v v'; induction Hτ; iIntros (v v') "#H1 /=".
Robbert Krebbers's avatar
Robbert Krebbers committed
238
    - by iDestruct "H1" as "[% %]"; subst.
Robbert Krebbers's avatar
Robbert Krebbers committed
239 240 241
    - by iDestruct "H1" as (n) "[% %]"; subst.
    - by iDestruct "H1" as (b) "[% %]"; subst.
    - iDestruct "H1" as ([??] [??]) "[% [H1 H2]]"; simplify_eq/=.
242
      rewrite IHHτ1 IHHτ2.
Robbert Krebbers's avatar
Robbert Krebbers committed
243
      by iDestruct "H1" as "%"; iDestruct "H2" as "%"; subst.
244
    - iDestruct "H1" as "[H1|H1]".
Robbert Krebbers's avatar
Robbert Krebbers committed
245
      + iDestruct "H1" as ([??]) "[% H1]"; simplify_eq/=.
246
        rewrite IHHτ1. by iDestruct "H1" as "%"; subst.
Robbert Krebbers's avatar
Robbert Krebbers committed
247
      + iDestruct "H1" as ([??]) "[% H1]"; simplify_eq/=.
248
        rewrite IHHτ2. by iDestruct "H1" as "%"; subst.
249
  Qed.
250
End logrel.
251 252 253

Typeclasses Opaque interp_env.
Notation "⟦ τ ⟧" := (interp τ).
254
Notation "⟦ τ ⟧ₑ" := (interp_expr (interp τ)).
255
Notation "⟦ Γ ⟧*" := (interp_env Γ).