typing.v 9.01 KB
Newer Older
1
From iris_logrel.F_mu_ref_conc Require Export lang.
Amin Timany's avatar
Amin Timany committed
2 3

Inductive type :=
4 5 6 7 8 9 10 11 12
  | 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})
13
  | TExists (τ : {bind 1 of type})
14
  | Tref (τ : type).
Amin Timany's avatar
Amin Timany committed
15 16 17 18 19 20

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.

21
Fixpoint binop_res_type (op : binop) : type :=
22 23 24 25 26
  match op with
  | Add => TNat | Sub => TNat
  | Eq => TBool | Le => TBool | Lt => TBool
  end.

27
Inductive EqType : type  Prop :=
28 29 30 31 32 33 34
  | 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).
35

Amin Timany's avatar
Amin Timany committed
36
Inductive typed (Γ : list type) : expr  type  Prop :=
37 38
  | Var_typed x τ : Γ !! x = Some τ  Γ ⊢ₜ Var x : τ
  | Unit_typed : Γ ⊢ₜ Unit : TUnit
Amin Timany's avatar
Amin Timany committed
39 40
  | Nat_typed n : Γ ⊢ₜ #n n : TNat
  | Bool_typed b : Γ ⊢ₜ # b : TBool
41 42 43 44 45 46 47 48 49 50 51 52
  | 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 : τ
53 54
  | Rec_typed e τ1 τ2 :
     TArrow τ1 τ2 :: τ1 :: Γ ⊢ₜ e : τ2  Γ ⊢ₜ Rec e : TArrow τ1 τ2
55 56 57
  | App_typed e1 e2 τ1 τ2 :
     Γ ⊢ₜ e1 : TArrow τ1 τ2  Γ ⊢ₜ e2 : τ1  Γ ⊢ₜ App e1 e2 : τ2
  | TLam_typed e τ :
58
     subst (ren (+1)) <$> Γ ⊢ₜ e : τ  Γ ⊢ₜ TLam e : TForall τ
59 60 61
  | TApp_typed e τ τ' : Γ ⊢ₜ e : TForall τ  Γ ⊢ₜ TApp e : τ.[τ'/]
  | TFold e τ : Γ ⊢ₜ e : τ.[TRec τ/]  Γ ⊢ₜ Fold e : TRec τ
  | TUnfold e τ : Γ ⊢ₜ e : TRec τ  Γ ⊢ₜ Unfold e : τ.[TRec τ/]
62 63 64 65
  | TPack e τ τ' : Γ ⊢ₜ e : τ.[τ'/]  Γ ⊢ₜ Pack e : TExists τ
  | TUnpack e1 e2 τ τ2 : Γ ⊢ₜ e1 : TExists τ 
      τ :: (subst (ren (+1)) <$> Γ) ⊢ₜ e2 : (subst (ren (+1)) τ2) 
      Γ ⊢ₜ Unpack e1 e2 : τ2                                                        
66 67 68 69 70 71 72 73
  | 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 τ).
Amin Timany's avatar
Amin Timany committed
74 75

Lemma typed_subst_invariant Γ e τ s1 s2 :
76
  Γ ⊢ₜ e : τ  ( x, x < length Γ  s1 x = s2 x)  e.[s1] = e.[s2].
Amin Timany's avatar
Amin Timany committed
77 78
Proof.
  intros Htyped; revert s1 s2.
79 80 81 82
  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).
Amin Timany's avatar
Amin Timany committed
83
  { intros A H1 H2. rewrite /up=> s1 s2 [|x] //=; auto with f_equal omega. }
84
  induction Htyped => s1 s2 Hs; f_equal/=; eauto using lookup_lt_Some with omega.
Amin Timany's avatar
Amin Timany committed
85
Qed.
86
Lemma n_closed_invariant n (e : expr) s1 s2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
87
  ( f, e.[upn n f] = e)  ( x, x < n  s1 x = s2 x)  e.[s1] = e.[s2].
88 89 90
Proof.
  intros Hnc. specialize (Hnc (ren (+1))).
  revert n Hnc s1 s2.
91
  induction e => m Hmc s1 s2 H1; asimpl in *; try f_equal;
92
    try (match goal with H : _ |- _ => eapply H end; eauto;
93
         try inversion Hmc; try match goal with H : _ |- _ => by rewrite H end;
94 95 96 97 98
         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 *.
Robbert Krebbers's avatar
Robbert Krebbers committed
99
    change (e.[up (up (upn m (ren (+1))))]) with
100 101 102 103 104
    (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.
Robbert Krebbers's avatar
Robbert Krebbers committed
105
  - change (e1.[up (upn m (ren (+1)))]) with
106 107 108 109 110
    (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.
Robbert Krebbers's avatar
Robbert Krebbers committed
111 112
  - change (e2.[up (upn m (ren (+1)))]) with
    (e2.[upn (S m) (ren (+1))]) in *.
113 114 115 116
    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.
117 118 119 120
  - apply (IHe0 (S m)); eauto. 
    + inversion Hmc; match goal with H : _ |- _ => (by rewrite H) end.
    + intros [|x] Hx. reflexivity.
      asimpl. rewrite H1; eauto with omega.
121 122
Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
126
Lemma typed_n_closed Γ τ e : Γ ⊢ₜ e : τ  ( f, e.[upn (length Γ) f] = e).
127
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
128
  intros H. induction H => f; asimpl; simpl in *; auto with f_equal.
129
  - apply lookup_lt_Some in H. rewrite iter_up. destruct lt_dec; auto with omega.
Robbert Krebbers's avatar
Robbert Krebbers committed
130
  - f_equal. apply IHtyped.
131
  - by f_equal; rewrite map_length in IHtyped.
132
  - f_equal. apply IHtyped1. rewrite map_length in IHtyped2. auto.
133 134 135
Qed.

Lemma n_closed_subst_head_simpl n e w ws :
Robbert Krebbers's avatar
Robbert Krebbers committed
136
  ( f, e.[upn n f] = e) 
Robbert Krebbers's avatar
Robbert Krebbers committed
137
  S (length ws) = n 
Amin Timany's avatar
Amin Timany committed
138
  e.[of_val w .: env_subst ws] = e.[env_subst (w :: ws)].
139 140 141 142
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.
143
  by rewrite Hv.
144 145
Qed.

Amin Timany's avatar
Amin Timany committed
146
Lemma typed_subst_head_simpl Δ τ e w ws :
147
  Δ ⊢ₜ e : τ  length Δ = S (length ws) 
Amin Timany's avatar
Amin Timany committed
148
  e.[of_val w .: env_subst ws] = e.[env_subst (w :: ws)].
Robbert Krebbers's avatar
Robbert Krebbers committed
149
Proof. eauto using n_closed_subst_head_simpl, typed_n_closed. Qed.
Amin Timany's avatar
Amin Timany committed
150

151
Lemma n_closed_subst_head_simpl_2 n e w w' ws :
Robbert Krebbers's avatar
Robbert Krebbers committed
152
  ( f, e.[upn n f] = e)  (S (S (length ws))) = n 
Amin Timany's avatar
Amin Timany committed
153
  e.[of_val w .: of_val w' .: env_subst ws] = e.[env_subst (w :: w' :: ws)].
154 155 156 157
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.
158
  by rewrite Hv.
159 160
Qed.

161
Lemma typed_subst_head_simpl_2 Δ τ e w w' ws :
162
  Δ ⊢ₜ e : τ  length Δ = 2 + length ws 
Amin Timany's avatar
Amin Timany committed
163
  e.[of_val w .: of_val w' .: env_subst ws] = e.[env_subst (w :: w' :: ws)].
Robbert Krebbers's avatar
Robbert Krebbers committed
164
Proof. eauto using n_closed_subst_head_simpl_2, typed_n_closed. Qed.
Amin Timany's avatar
Amin Timany committed
165

166 167
Lemma empty_env_subst e : e.[env_subst []] = e.
Proof. change (env_subst []) with (@ids expr _). by asimpl. Qed.
Amin Timany's avatar
Amin Timany committed
168

169 170 171
(** Weakening *)
Lemma context_gen_weakening ξ Γ' Γ e τ :
  Γ' ++ Γ ⊢ₜ e : τ 
Robbert Krebbers's avatar
Robbert Krebbers committed
172
  Γ' ++ ξ ++ Γ ⊢ₜ e.[upn (length Γ') (ren (+ (length ξ)))] : τ.
Amin Timany's avatar
Amin Timany committed
173
Proof.
174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192
  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.
193 194 195 196 197
  - econstructor; eauto. 
    specialize (IHtyped2 (τ :: (subst (ren (+1)) <$> Γ1)) (subst (ren (+1)) <$> Γ2) (subst (ren (+1)) <$> ξ)).
    repeat rewrite fmap_app.
    asimpl in IHtyped2. asimpl. rewrite ?map_length in IHtyped2. apply IHtyped2.
    by repeat rewrite fmap_app.
198 199
Qed.

200 201 202 203 204 205 206
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.