typing.v 8.17 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 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 52 53 54 55 56 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 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 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

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
  | Add => TNat | Sub => TNat
  | Eq => TBool | Le => TBool | Lt => TBool
  end.

Inductive EqType : type  Prop :=
  | EqTUnit : EqType TUnit
  | EqTNat : EqType TNat
  | EqTBool : EqType TBool
  | EqTProd τ τ' : EqType τ  EqType τ'  EqType (TProd τ τ')
  | EqSum τ τ' : EqType τ  EqType τ'  EqType (TSum τ τ').

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
  | 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).
  { intros A H1 H2. rewrite /up=> s1 s2 [|x] //=; auto with f_equal omega. }
  induction Htyped => s1 s2 Hs; f_equal/=; eauto using lookup_lt_Some with omega.
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).
  - apply H1. rewrite iter_up in Hmc. destruct lt_dec; try omega.
    asimpl in *. cbv in x. replace (m + (x - m)) with x in Hmc by omega.
    inversion Hmc; omega.
  - 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 |].
      asimpl; rewrite H1; auto with omega.
  - 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 |].
      asimpl; rewrite H1; auto with omega.
  - 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 |].
      asimpl; rewrite H1; auto with omega.
Qed.

Definition env_subst (vs : list val) (x : var) : expr :=
  from_option id (Var x) (of_val <$> vs !! x).

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.
  - apply lookup_lt_Some in H. rewrite iter_up. destruct lt_dec; auto with omega.
  - f_equal. apply IHtyped.
  - by f_equal; rewrite map_length in IHtyped.
Qed.

Lemma n_closed_subst_head_simpl n e w ws :
  ( f, e.[upn n f] = e) 
  S (length ws) = n 
  e.[of_val w .: env_subst ws] = e.[env_subst (w :: ws)].
Proof.
  intros H1 H2.
  rewrite /env_subst. eapply n_closed_invariant; eauto=> /= -[|x] ? //=.
  destruct (lookup_lt_is_Some_2 ws x) as [v' Hv]; first omega; simpl.
  by rewrite Hv.
Qed.

Lemma typed_subst_head_simpl Δ τ e w ws :
  Δ  e : τ  length Δ = S (length ws) 
  e.[of_val w .: env_subst ws] = e.[env_subst (w :: ws)].
Proof. eauto using n_closed_subst_head_simpl, typed_n_closed. Qed.

Lemma n_closed_subst_head_simpl_2 n e w w' ws :
  ( f, e.[upn n f] = e)  (S (S (length ws))) = n 
  e.[of_val w .: of_val w' .: env_subst ws] = e.[env_subst (w :: w' :: ws)].
Proof.
  intros H1 H2.
  rewrite /env_subst. eapply n_closed_invariant; eauto => /= -[|[|x]] H3 //=.
  destruct (lookup_lt_is_Some_2 ws x) as [v' Hv]; first omega; simpl.
  by rewrite Hv.
Qed.

Lemma typed_subst_head_simpl_2 Δ τ e w w' ws :
  Δ  e : τ  length Δ = 2 + length ws 
  e.[of_val w .: of_val w' .: env_subst ws] = e.[env_subst (w :: w' :: ws)].
Proof. eauto using n_closed_subst_head_simpl_2, typed_n_closed. Qed.

Lemma empty_env_subst e : e.[env_subst []] = e.
Proof. change (env_subst []) with (@ids expr _). by asimpl. 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.
    + asimpl. constructor. rewrite lookup_app_r; auto with omega.
      rewrite lookup_app_r; auto with omega.
      rewrite lookup_app_r in H; auto with omega.
      match goal with
        |- _ !! ?A = _ => by replace A with (x - length Γ1) by omega
      end.
  - econstructor; eauto. by apply (IHtyped2 (_::_)). by apply (IHtyped3 (_::_)).
  - constructor. by apply (IHtyped (_ :: _ :: _)).
  - 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.