Subenvironments

Set Implicit Arguments.

Require Import Definitions.
Require Import Coq.Program.Equality.

Subenvironments G1 ⪯ G2

G1 is a subenvironment of G2, denoted G1 ⪯ G2, if dom(G1) = dom(G2) and for each x, G1 ⊢ G1(x) <: G2(x).

Reserved Notation "G1 ⪯ G2" (at level 35).

Inductive subenv: ctx -> ctx -> Prop :=
| subenv_empty : empty ⪯ empty
| subenv_grow: forall G G' x T T',
    G ⪯ G' ->
    ok (G & x ~ T) ->
    G ⊢ T <: T' ->
    G & x ~ T ⪯ G' & x ~ T'
where "G1 ⪯ G2" := (subenv G1 G2).

Hint Constructors subenv.

If ok G, then G ⪯ G. Note: ok(G) means that G's domain consists of distinct variables. ok is defined in TLC.LibEnv.v

Lemma subenv_refl : forall G, ok G -> G ⪯ G.
Proof.
intros G H. induction H; auto.
Qed.
Hint Resolve subenv_refl.

G' subG G
ok(G', x: T)
―――――――――――――――――――――――――――――
G', x: T subG G, x: T

Lemma subenv_push : forall G1 G2 x T,
    G1 ⪯ G2 ->
    ok (G1 & x ~ T) -> ok (G2 & x ~ T) ->
    (G1 & x ~ T ) ⪯ (G2 & x ~ T ).
Proof.
  intros. induction H; intros; auto.
Qed.
Hint Resolve subenv_push.

G ⊢ S <: U
ok(G, x: S) (see subenv_push)
――――――――――――――――――――――――――――――――――
G', x: T subG G, x: T

Lemma subenv_last: forall G x S U,
  G ⊢ S <: U ->
  ok (G & x ~ S) ->
  (G & x ~ S ) ⪯ (G & x ~ U ).
Proof.
  intros.
  inversion H0;
  match goal with
  | [ H : empty = _ |- _ ] => destruct (empty_push_inv H2)
  | [ H : _ & _ ~ _ = _ & _ ~ _ |- _ ] =>
    apply eq_push_inv in H; destruct_all; subst
  end;
  auto.
Qed.
Hint Resolve subenv_last.

Lemma subenv_ok_fresh : forall G G',
    G ⪯ G' ->
    ok G' /\ (forall x, x # G -> x # G').
Proof.
  introv H.
  induction H;
    destruct_all;
    match goal with
    | [H : ok (?G & ?x ~ _) |- _] =>
      pose proof (ok_push_inv H0) as [? ?]; split; auto
    | _ => split; auto
    end.
Qed.

Lemma subenv_ok_l : forall G1 G2,
    G1 ⪯ G2 -> ok G1.
Proof.
  introv H. induction H; auto.
Qed.
Hint Resolve subenv_ok_l.

Lemma subenv_ok_r: forall G1 G2,
    G1 ⪯ G2 -> ok G2.
Proof.
  apply subenv_ok_fresh.
Qed.
Hint Resolve subenv_ok_r.