typing.v 6.1 KB
Newer Older
Amin Timany's avatar
Amin Timany committed
1
From iris_examples.logrel.F_mu_ref 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

Inductive type :=
  | TUnit : 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.

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
  | 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 ρ :
     Γ  e0 : TSum τ1 τ2  τ1 :: Γ  e1 : ρ  τ2 :: Γ  e2 : ρ 
     Γ  Case e0 e1 e2 : ρ
  | Lam_typed e τ1 τ2 : τ1 :: Γ  e : τ2  Γ  Lam 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 τ/]
  | TAlloc e τ : Γ  e : τ  Γ  Alloc e : Tref τ
  | TLoad e τ : Γ  e : Tref τ  Γ  Load e : τ
  | TStore e e' τ : Γ  e : Tref τ  Γ  e' : τ  Γ  Store e e' : TUnit
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
53 54
  { 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
55 56 57 58 59 60 61 62 63 64 65
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
66 67
  - 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
68 69 70 71 72 73
  - unfold upn in *.
    change (e.[up (upn m (ren (+1)))]) with
    (e.[iter (S m) up (ren (+1))]) in *.
    apply (IHe (S m)).
    + inversion Hmc; match goal with H : _ |- _ => (by rewrite H) end.
    + intros [|[|x]] H2; [by cbv| |].
Robbert Krebbers's avatar
Robbert Krebbers committed
74 75
      asimpl; rewrite H1; auto with lia.
      asimpl; rewrite H1; auto with lia.
Amin Timany's avatar
Amin Timany committed
76 77 78 79 80
  - 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
81
      asimpl; rewrite H1; auto with lia.
Amin Timany's avatar
Amin Timany committed
82 83 84 85 86
  - 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
87
      asimpl; rewrite H1; auto with lia.
Amin Timany's avatar
Amin Timany committed
88 89
Qed.

Amin Timany's avatar
Amin Timany committed
90 91 92 93 94
Fixpoint env_subst (vs : list val) : var  expr :=
  match vs with
  | [] => ids
  | v :: vs' => #v .: env_subst vs'
  end.
Amin Timany's avatar
Amin Timany committed
95

Amin Timany's avatar
Amin Timany committed
96 97 98 99 100 101 102 103 104
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
105 106 107
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
108
  - apply lookup_lt_Some in H. rewrite iter_up. destruct lt_dec; auto with lia.
Amin Timany's avatar
Amin Timany committed
109 110 111 112 113 114 115 116 117 118 119 120 121
  - 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
122 123 124
    + 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
125
      match goal with
Robbert Krebbers's avatar
Robbert Krebbers committed
126
        |- _ !! ?A = _ => by replace A with (x - length Γ1) by lia
Amin Timany's avatar
Amin Timany committed
127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144
      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.