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

Inductive type :=
  | TUnit : type
  | TProd : type  type  type
  | TSum : type  type  type
  | TArrow : type  type  type.

Reserved Notation "Γ ⊢ₜ e : τ" (at level 74, e, τ at next level).

Inductive typed (Γ : list type) : expr  type  Prop :=
  | Var_typedx 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
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 ( s1 s2 x, (x  0  s1 (pred x) = s2 (pred x))  up s1 x = up s2 x).
Robbert Krebbers's avatar
Robbert Krebbers committed
33 34
  { 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
35 36
Qed.

Amin Timany's avatar
Amin Timany committed
37 38 39 40 41
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
42

Amin Timany's avatar
Amin Timany committed
43 44
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
45
Proof.
Amin Timany's avatar
Amin Timany committed
46 47 48 49 50 51
  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.