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

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}).

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 τ/]
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
47 48
  { 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
49 50
Qed.

Amin Timany's avatar
Amin Timany committed
51 52 53 54 55
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
56

Amin Timany's avatar
Amin Timany committed
57 58
Lemma env_subst_lookup vs x v :
  vs !! x = Some v  env_subst vs x = of_val v.
Amin Timany's avatar
Amin Timany committed
59
Proof.
Amin Timany's avatar
Amin Timany committed
60 61 62 63 64 65
  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.