typing.v 7.76 KB
Newer Older
Amin Timany's avatar
Amin Timany committed
1
From iris_examples.logrel.F_mu_ref_conc Require Export lang.
Amin Timany's avatar
Amin Timany committed
2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21

Inductive type :=
  | TUnit : type
  | TNat : type
  | TBool : type
  | TProd : type  type  type
  | TSum : type  type  type
  | TArrow : type  type  type
  | TRec (τ : {bind 1 of type})
  | TVar (x : var)
  | TForall (τ : {bind 1 of type})
  | Tref (τ : type).

Instance Ids_type : Ids type. derive. Defined.
Instance Rename_type : Rename type. derive. Defined.
Instance Subst_type : Subst type. derive. Defined.
Instance SubstLemmas_typer : SubstLemmas type. derive. Qed.

Fixpoint binop_res_type (op : binop) : type :=
  match op with
22
  | Add => TNat | Sub => TNat | Mult => TNat
Amin Timany's avatar
Amin Timany committed
23 24 25 26 27 28 29
  | Eq => TBool | Le => TBool | Lt => TBool
  end.

Inductive EqType : type  Prop :=
  | EqTUnit : EqType TUnit
  | EqTNat : EqType TNat
  | EqTBool : EqType TBool
Amin Timany's avatar
Amin Timany committed
30
  | EQRef τ : EqType (Tref τ).
Amin Timany's avatar
Amin Timany committed
31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52

Reserved Notation "Γ ⊢ₜ e : τ" (at level 74, e, τ at next level).

Inductive typed (Γ : list type) : expr  type  Prop :=
  | Var_typed x τ : Γ !! x = Some τ  Γ  Var x : τ
  | Unit_typed : Γ  Unit : TUnit
  | Nat_typed n : Γ  #n n : TNat
  | Bool_typed b : Γ  # b : TBool
  | BinOp_typed op e1 e2 :
     Γ  e1 : TNat  Γ  e2 : TNat  Γ  BinOp op e1 e2 : binop_res_type op
  | Pair_typed e1 e2 τ1 τ2 : Γ  e1 : τ1  Γ  e2 : τ2  Γ  Pair e1 e2 : TProd τ1 τ2
  | Fst_typed e τ1 τ2 : Γ  e : TProd τ1 τ2  Γ  Fst e : τ1
  | Snd_typed e τ1 τ2 : Γ  e : TProd τ1 τ2  Γ  Snd e : τ2
  | InjL_typed e τ1 τ2 : Γ  e : τ1  Γ  InjL e : TSum τ1 τ2
  | InjR_typed e τ1 τ2 : Γ  e : τ2  Γ  InjR e : TSum τ1 τ2
  | Case_typed e0 e1 e2 τ1 τ2 τ3 :
     Γ  e0 : TSum τ1 τ2  τ1 :: Γ  e1 : τ3  τ2 :: Γ  e2 : τ3 
     Γ  Case e0 e1 e2 : τ3
  | If_typed e0 e1 e2 τ :
     Γ  e0 : TBool  Γ  e1 : τ  Γ  e2 : τ  Γ  If e0 e1 e2 : τ
  | Rec_typed e τ1 τ2 :
     TArrow τ1 τ2 :: τ1 :: Γ  e : τ2  Γ  Rec e : TArrow τ1 τ2
53 54 55 56 57 58
  | Lam_typed e τ1 τ2 :
      τ1 :: Γ  e : τ2  Γ  Lam e : TArrow τ1 τ2
  | LetIn_typed e1 e2 τ1 τ2 :
      Γ  e1 : τ1  τ1 :: Γ  e2 : τ2  Γ  LetIn e1 e2 : τ2
  | Seq_typed e1 e2 τ1 τ2 :
      Γ  e1 : τ1  Γ  e2 : τ2  Γ  Seq e1 e2 : τ2
Amin Timany's avatar
Amin Timany committed
59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82
  | App_typed e1 e2 τ1 τ2 :
     Γ  e1 : TArrow τ1 τ2  Γ  e2 : τ1  Γ  App e1 e2 : τ2
  | TLam_typed e τ :
     subst (ren (+1)) <$> Γ  e : τ  Γ  TLam e : TForall τ
  | TApp_typed e τ τ' : Γ  e : TForall τ  Γ  TApp e : τ.[τ'/]
  | TFold e τ : Γ  e : τ.[TRec τ/]  Γ  Fold e : TRec τ
  | TUnfold e τ : Γ  e : TRec τ  Γ  Unfold e : τ.[TRec τ/]
  | TFork e : Γ  e : TUnit  Γ  Fork e : TUnit
  | TAlloc e τ : Γ  e : τ  Γ  Alloc e : Tref τ
  | TLoad e τ : Γ  e : Tref τ  Γ  Load e : τ
  | TStore e e' τ : Γ  e : Tref τ  Γ  e' : τ  Γ  Store e e' : TUnit
  | TCAS e1 e2 e3 τ :
     EqType τ  Γ  e1 : Tref τ  Γ  e2 : τ  Γ  e3 : τ 
     Γ  CAS e1 e2 e3 : TBool
where "Γ ⊢ₜ e : τ" := (typed Γ e τ).

Lemma typed_subst_invariant Γ e τ s1 s2 :
  Γ  e : τ  ( x, x < length Γ  s1 x = s2 x)  e.[s1] = e.[s2].
Proof.
  intros Htyped; revert s1 s2.
  assert ( x Γ, x < length (subst (ren (+1)) <$> Γ)  x < length Γ).
  { intros ??. by rewrite fmap_length. } 
  assert ( {A} `{Ids A} `{Rename A} (s1 s2 : nat  A) x,
    (x  0  s1 (pred x) = s2 (pred x))  up s1 x = up s2 x).
Robbert Krebbers's avatar
Robbert Krebbers committed
83 84
  { intros A H1 H2. rewrite /up=> s1 s2 [|x] //=; auto with f_equal lia. }
  induction Htyped => s1 s2 Hs; f_equal/=; eauto using lookup_lt_Some with lia.
Amin Timany's avatar
Amin Timany committed
85 86 87 88 89 90 91 92 93 94
Qed.
Lemma n_closed_invariant n (e : expr) s1 s2 :
  ( f, e.[upn n f] = e)  ( x, x < n  s1 x = s2 x)  e.[s1] = e.[s2].
Proof.
  intros Hnc. specialize (Hnc (ren (+1))).
  revert n Hnc s1 s2.
  induction e => m Hmc s1 s2 H1; asimpl in *; try f_equal;
    try (match goal with H : _ |- _ => eapply H end; eauto;
         try inversion Hmc; try match goal with H : _ |- _ => by rewrite H end;
         fail).
Robbert Krebbers's avatar
Robbert Krebbers committed
95 96
  - apply H1. rewrite iter_up in Hmc. destruct lt_dec; try lia.
    asimpl in *. injection Hmc as Hmc. unfold var in *. omega.
Amin Timany's avatar
Amin Timany committed
97 98 99 100 101 102
  - unfold upn in *.
    change (e.[up (up (upn m (ren (+1))))]) with
    (e.[iter (S (S m)) up (ren (+1))]) in *.
    apply (IHe (S (S m))).
    + inversion Hmc; match goal with H : _ |- _ => (by rewrite H) end.
    + intros [|[|x]] H2; [by cbv|by cbv |].
Robbert Krebbers's avatar
Robbert Krebbers committed
103
      asimpl; rewrite H1; auto with lia.
104 105 106 107 108 109 110 111
  - apply (IHe (S m)).
    + inversion Hmc; match goal with H : _ |- _ => (by rewrite H) end.
    + intros [|x] H2; [by cbv |].
      asimpl; rewrite H1; auto with lia.
  - apply (IHe0 (S m)).
    + inversion Hmc; match goal with H : _ |- _ => (by rewrite H) end.
    + intros [|x] H2; [by cbv |].
      asimpl; rewrite H1; auto with lia.
Amin Timany's avatar
Amin Timany committed
112 113 114 115 116
  - change (e1.[up (upn m (ren (+1)))]) with
    (e1.[iter (S m) up (ren (+1))]) in *.
    apply (IHe0 (S m)).
    + inversion Hmc; match goal with H : _ |- _ => (by rewrite H) end.
    + intros [|x] H2; [by cbv |].
Robbert Krebbers's avatar
Robbert Krebbers committed
117
      asimpl; rewrite H1; auto with lia.
Amin Timany's avatar
Amin Timany committed
118 119 120 121 122
  - change (e2.[up (upn m (ren (+1)))]) with
    (e2.[upn (S m) (ren (+1))]) in *.
    apply (IHe1 (S m)).
    + inversion Hmc; match goal with H : _ |- _ => (by rewrite H) end.
    + intros [|x] H2; [by cbv |].
Robbert Krebbers's avatar
Robbert Krebbers committed
123
      asimpl; rewrite H1; auto with lia.
Amin Timany's avatar
Amin Timany committed
124 125
Qed.

Amin Timany's avatar
Amin Timany committed
126 127 128 129 130 131 132 133 134 135 136 137 138 139 140
Fixpoint env_subst (vs : list val) : var  expr :=
  match vs with
  | [] => ids
  | v :: vs' => (of_val v) .: env_subst vs'
  end.

Lemma env_subst_lookup vs x v :
  vs !! x = Some v  env_subst vs x = of_val v.
Proof.
  revert vs; induction x => vs.
  - by destruct vs; inversion 1.
  - destruct vs as [|w vs]; first by inversion 1.
    rewrite -lookup_tail /=.
    apply IHx.
Qed.
Amin Timany's avatar
Amin Timany committed
141 142 143 144

Lemma typed_n_closed Γ τ e : Γ  e : τ  ( f, e.[upn (length Γ) f] = e).
Proof.
  intros H. induction H => f; asimpl; simpl in *; auto with f_equal.
Robbert Krebbers's avatar
Robbert Krebbers committed
145
  - apply lookup_lt_Some in H. rewrite iter_up. destruct lt_dec; auto with lia.
Amin Timany's avatar
Amin Timany committed
146 147 148 149 150 151 152 153 154 155 156 157 158 159
  - f_equal. apply IHtyped.
  - by f_equal; rewrite map_length in IHtyped.
Qed.

(** Weakening *)
Lemma context_gen_weakening ξ Γ' Γ e τ :
  Γ' ++ Γ  e : τ 
  Γ' ++ ξ ++ Γ  e.[upn (length Γ') (ren (+ (length ξ)))] : τ.
Proof.
  intros H1.
  remember (Γ' ++ Γ) as Ξ. revert Γ' Γ ξ HeqΞ.
  induction H1 => Γ1 Γ2 ξ HeqΞ; subst; asimpl in *; eauto using typed.
  - rewrite iter_up; destruct lt_dec as [Hl | Hl].
    + constructor. rewrite lookup_app_l; trivial. by rewrite lookup_app_l in H.
Robbert Krebbers's avatar
Robbert Krebbers committed
160 161 162
    + asimpl. constructor. rewrite lookup_app_r; auto with lia.
      rewrite lookup_app_r; auto with lia.
      rewrite lookup_app_r in H; auto with lia.
Amin Timany's avatar
Amin Timany committed
163
      match goal with
Robbert Krebbers's avatar
Robbert Krebbers committed
164
        |- _ !! ?A = _ => by replace A with (x - length Γ1) by lia
Amin Timany's avatar
Amin Timany committed
165 166 167
      end.
  - econstructor; eauto. by apply (IHtyped2 (_::_)). by apply (IHtyped3 (_::_)).
  - constructor. by apply (IHtyped (_ :: _ :: _)).
168 169
  - constructor. by apply (IHtyped (_ :: _)).
  - econstructor; eauto. by apply (IHtyped2 (_::_)).
Amin Timany's avatar
Amin Timany committed
170 171 172 173 174 175 176 177 178 179 180 181 182 183 184
  - constructor.
    specialize (IHtyped
      (subst (ren (+1)) <$> Γ1) (subst (ren (+1)) <$> Γ2) (subst (ren (+1)) <$> ξ)).
    asimpl in *. rewrite ?map_length in IHtyped.
    repeat rewrite fmap_app. apply IHtyped.
    by repeat rewrite fmap_app.
Qed.

Lemma context_weakening ξ Γ e τ :
  Γ  e : τ  ξ ++ Γ  e.[(ren (+ (length ξ)))] : τ.
Proof. eapply (context_gen_weakening _ []). Qed.

Lemma closed_context_weakening ξ Γ e τ :
  ( f, e.[f] = e)  Γ  e : τ  ξ ++ Γ  e : τ.
Proof. intros H1 H2. erewrite <- H1. by eapply context_weakening. Qed.