typing.v 2.98 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 51 52 53 54 55 56 57 58 59
Qed.

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

Lemma typed_subst_head_simpl Δ τ e w ws :
  Δ  e : τ  length Δ = S (length ws) 
  e.[# w .: env_subst ws] = e.[env_subst (w :: ws)].
Proof.
  intros H1 H2. rewrite /env_subst.
  eapply typed_subst_invariant; eauto=> /= -[|x] ? //=.
Robbert Krebbers's avatar
Robbert Krebbers committed
60
  destruct (lookup_lt_is_Some_2 ws x) as [v' ?]; first lia.
Amin Timany's avatar
Amin Timany committed
61 62 63 64 65
  by simplify_option_eq.
Qed.

Lemma empty_env_subst e : e.[env_subst []] = e.
Proof. change (env_subst []) with (@ids expr _). by asimpl. Qed.