Weakening

Weakening Lemma

Set Implicit Arguments.

Require Import Definitions.

Weakening states that typing is preserved in extended environments.

G1, G3 |- t: T
ok(G1, G2, G3)
――――――――――――――――――――
G1, G2, G3 |- t: T

and

G1, G3 |- d: D
ok(G1, G2, G3)
――――――――――――――――――――
G1, G2, G3 |- d: D

and

G1, G3 |- ds :: T
ok(G1, G2, G3)
――――――――――――――――――――
G1, G2, G3 |- ds :: T

and

G1, G3 |- T <: U
ok(G1, G2, G3)
――――――――――――――――――――
G1, G2, G3 |- T <: U

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

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

Ltac weaken_specialize :=
  intros;
  match goal with
  | [ Hok: ok (?G1 & ?G2) |- _ ] ⇒
    assert (G1 & G2 = G1 & G2 & 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: ∀ G1 G2 t T,
    G1 ⊢ t : T →
    ok (G1 & G2) →
    G1 & G2 ⊢ t : T.
Proof.
  weaken_specialize.
Qed.

Weakening lemma specialized to subtyping.

Lemma weaken_subtyp: ∀ G1 G2 S U,
  G1 ⊢ S <: U →
  ok (G1 & G2) →
  G1 & G2 ⊢ S <: U.
Proof.
  weaken_specialize.
Qed.

Weakening lemma specialized to definition-typing

Lemma weaken_ty_defs: ∀ G1 G2 z bs ds T,
    z ; bs ; G1 ⊢ ds :: T →
    ok (G1 & G2) →
    z ; bs ; G1 & G2 ⊢ ds :: T.
Proof.
  weaken_specialize.
Qed.