Weakening

Set Implicit Arguments.

Require Import Definitions.

Weakening Lemma

Weakening states that typing is preserved in extended environments.

, ⊢ t: T
ok(, , )
――――――――――――――――――――
, , ⊢ t: T

and

, ⊢ d: D
ok(, , )
――――――――――――――――――――
, , ⊢ d: D

and

, ⊢ ds :: T
ok(, , )
――――――――――――――――――――
, , ⊢ ds :: T

and

, ⊢ T <: U
ok(, , )
――――――――――――――――――――
, , ⊢ T <: U

The proof is by mutual induction on term typing, definition typing, and subtyping.

Lemma weaken_rules:
  (forall t T, ⊢ t : T forall ,
     = &
    ok ( & & )
     & & ⊢ t : T)
  (forall d D, /- d : D forall ,
     = &
    ok ( & & )
     & & /- d : D)
  (forall ds T, /- ds :: T forall ,
     = &
    ok ( & & )
     & & /- ds :: T)
  (forall T U, ⊢ T <: U forall ,
     = &
    ok ( & & )
     & & ⊢ T <: U).
Proof.
  apply rules_mutind; intros; subst;
  eauto 4 using binds_weaken;
  fresh_constructor;
    match goal with
    | [ H: forall z, z \notin ?L forall , _,
        Hok: ok (? & ? & ?)
        |- context [?z ~ ?T] ]
      assert (zL : z \notin L) by auto;
      specialize (H z zL ( & z ~ T));
      rewrite? concat_assoc in H;
      apply~ H
    end.
Qed.

Ltac weaken_specialize :=
  intros;
  match goal with
  | [ Hok: ok (? & ?) |- _ ]
    assert ( & = & & empty) as EqG by rewrite~ concat_empty_r;
    rewrite EqG; apply~ weaken_rules;
    (rewrite concat_empty_r || rewrite EqG); assumption
  end.

Weakening lemma specialized to term typing.

Lemma weaken_ty_trm: forall t T,
     ⊢ t : T
    ok ( & )
     & ⊢ t : T.
Proof.
  weaken_specialize.
Qed.

Weakening lemma specialized to subtyping.

Lemma weaken_subtyp: forall S U,
   ⊢ S <: U
  ok ( & )
   & ⊢ S <: U.
Proof.
  weaken_specialize.
Qed.