Require Import basics.
Require Import poplmark1a.

(**********************************************************************)
(* transitivity of subtyping                                          *)
(**********************************************************************)

Section tn_sec.

Let trans_stmt(Q:tp) := 
  (forall (G:ctxt) (S T : tp), 
      G |- S <:: Q -> 
      G |- Q <:: T -> 
      G |- S <:: T).

Let narrow_stmt(Q:tp) :=
  (forall (G:ctxt) (M N : tp),
                   G |- M <:: N ->
                   forall (G1 G2 : ctxt) (P : tp),
                   G = G1 ~:: bound Q ~++ G2 -> 
                   G1 |- P <:: Q -> 
                   G1 ~:: bound P ~++ G2 |- M <:: N).

(* The lemmas are structured here following Vouillon's development. *)

Lemma transitivity_case: forall Q:tp,
                         (forall Q':tp, size Q' < size Q -> trans_stmt(Q')) ->
                         (forall Q':tp, size Q' < size Q -> narrow_stmt(Q')) ->
                         trans_stmt(Q).
Proof.
intros Q TransH NarrowH; unfold trans_stmt in |- *; intros G S T D1 D2;
 induction D1.
 inversion D2.
   apply sa_top; try tauto.
 assumption.
 apply sa_trans_tvar with (U := U); try tauto.
 inversion D2.
  apply sa_top; unfold is_ground in |- *; simpl in |- *; try tauto; split.
   apply subtp_consts_bounded2 with (S := T1); assumption.
   apply subtp_consts_bounded1 with (T := T2); assumption.
   fold (is_ground Q1) in |- *.
     apply subtp_ground2 with (G := G) (S := T1); assumption.
   fold (is_ground Q2) in |- *; apply subtp_ground1 with (G := G) (T := T2);
    assumption.
  unfold trans_stmt in TransH; apply sa_arrow;
   [ apply TransH with (Q' := T1) | apply TransH with (Q' := T2) ]; 
   try tauto; simpl in |- *; omega.
 inversion D2.
  apply sa_top; try assumption; unfold is_ground in |- *; simpl in |- *;
   split.
   apply subtp_consts_bounded2 with (S := T1) (G := G); assumption.
   assert
    (consts_bounded (length (G ~:: bound T1))
       (graft_tp (const (length G)) x1 Q2)).
    apply subtp_consts_bounded1 with (T := graft_tp (const (length G)) x2 T2);
     assumption.
    simpl in H8.
      apply consts_bounded_step with (x := x1); assumption.
   fold (is_ground Q1) in |- *; apply subtp_ground2 with (G := G) (S := T1);
    assumption.
   fold (nil ~:: x1 ~++ nil) in |- *;
    apply is_ground_h_extend with (c := length G); 
    simpl in |- *.
     apply
      subtp_ground1
       with (G := G ~:: bound T1) (T := graft_tp (const (length G)) x2 T2);
      assumption.
  clear H5 G0 H1 x0 H2 Q0 H3 Q3.
    rename x2 into y.
    rename x3 into x2.
    rename T1 into S1.
    rename T0 into T1.
    rename T2 into S2.
    rename T3 into T2.
    apply sa_all; try tauto.
   unfold trans_stmt in TransH; apply TransH with (Q' := S1); try assumption;
    simpl in |- *; omega.
   unfold narrow_stmt in NarrowH.
     assert
      (G ~:: bound T1 |- graft_tp (const (length G)) x1 Q2 <::
       graft_tp (const (length G)) y S2).
    fold (G ~:: bound T1 ~++ nil) in |- *;
     apply NarrowH with (Q' := S1) (G := G ~:: bound S1 ~++ nil);
     try assumption; simpl in |- *; reflexivity || omega.
    unfold trans_stmt in TransH;
     apply TransH with (Q' := graft_tp (const (length G)) y S2);
     try assumption.
      rewrite size_graft_const; simpl in |- *; omega.
Qed.

Lemma narrow_case: forall Q : tp,
                   (forall Q' : tp, size Q' = size Q -> trans_stmt Q') ->
                   narrow_stmt(Q).
intros Q TransH G M N D1; induction D1; intros G1 G2 P E; subst G; intro D2.
 apply sa_top; try assumption.
  lain H; simpl in H; la; simpl in |- *; assumption.
  apply ctxt_consts_bounded_change with (Q := Q); try assumption.
    apply subtp_consts_bounded1 with (T := Q); assumption.
  apply ctxt_is_ground_change with (Q := Q); try assumption.
    apply subtp_ground1 with (G := G1) (T := Q); assumption.
 apply sa_refl_tvar;
  [ apply ctxt_consts_bounded_change with (Q := Q);
     [ assumption | apply subtp_consts_bounded1 with (T := Q); assumption ]
  | apply ctxt_is_ground_change with (Q := Q);
     [ assumption | apply subtp_ground1 with (G := G1) (T := Q); assumption ]
  | lain H1; simpl in H1; la; simpl in |- *; omega ].
 assert (x = length G1 \/ x < length G1 \/ x > length G1); try omega.
   elim H1; clear H1; intro H1.
  subst x.
    clear H0.
    assert
     (lookup (length (G1 ~:: bound Q ~++ G2) - 1 - length G1)
        (G1 ~:: bound Q ~++ G2) Q).
   la; simpl in |- *.
     assert (length G2 + S (length G1) - 1 - length G1 = length G2);
      try omega.
     rewrite H0.
     apply lookup_skip.
   assert (U = Q).
    exact
     (lookup_functional (G1 ~:: bound Q ~++ G2) U Q
        (length (G1 ~:: bound Q ~++ G2) - 1 - length G1) H H0).
    subst U.
      apply sa_trans_tvar with (U := P).
     assert (length (G1 ~:: bound P ~++ G2) - 1 - length G1 = length G2);
      try (la; simpl in |- *; omega).
       rewrite H1.
       apply lookup_skip.
     la; simpl in |- *; omega.
     assert (G1 ~:: bound P ~++ G2 |- Q <:: T).
      apply IHD1; tauto.
      assert (G1 ~:: bound P ~++ G2 |- P <:: Q).
       apply multi_weaken_subtp.
        apply weaken_subtp.
         apply subtp_ground1 with (G := G1) (T := Q); assumption.
         assumption.
         apply subtp_consts_bounded1 with (T := Q); assumption.
        assert (ctxt_is_ground (G1 ~:: bound P ~++ G2)).
         apply (subtp_ctxt_is_ground (G1 ~:: bound P ~++ G2) Q T H1).
         exact (proj2 (ctxt_is_ground_split (G1 ~:: bound P) G2 H2)).
        apply subtp_ctxt_consts_bounded with (T := Q) (U := T).
          assumption.
       unfold trans_stmt in TransH.
         apply TransH with (Q' := Q); omega || tauto.
  lain H; lain H0; simpl in *; elim H1; clear H1; intro H1;
   (apply sa_trans_tvar with (U := U);
     [ idtac
     | la; simpl in |- *; omega
     | apply IHD1; try assumption || trivial ]); la; 
   simpl in |- *.
   assert
    (length G2 + S (length G1) - 1 - x = length G2 + (S (length G1) - 1 - x)).
    clear H0; omega.
    rewrite H2.
      apply lookup_skip1.
      clear H2.
      assert (exists z : nat, S (length G1) - S x = S z).
     apply lt_to_S.
       omega.
     elim H2; clear H2; intros z H2.
       assert (S (length G1) - 1 - x = S (length G1) - S x).
      omega.
      rewrite H3; clear H3.
        rewrite H2; apply lookup_n.
        apply lookup_skip2 with (G2 := nil ~:: bound Q ~++ G2).
        la; simpl in |- *.
        assert (length G2 + 1 + z = length G2 + S z); try omega.
        rewrite H3.
        rewrite <- H2.
        assert
         (length G2 + (S (length G1) - S x) =
          length G2 + S (length G1) - 1 - x).
       omega.
       rewrite H4.
         assert (G1 ~++ (nil ~:: bound Q ~++ G2) = G1 ~:: bound Q ~++ G2).
        rewrite app_ass.
          simpl in |- *.
          trivial.
        rewrite H5.
          assumption.
   apply lookup_start2.
    omega.
    apply lookup_start1 with (G1 := G1 ~:: bound Q).
     omega.
     assumption.
 apply sa_arrow; [ apply IHD1_1 | apply IHD1_2 ]; try tauto.
 apply sa_all.
  apply IHD1_1; tauto.
  lain H; simpl in H; la; simpl in |- *; assumption.
  lain H0; simpl in H0; la; simpl in |- *; assumption.
  assert (length (G1 ~:: bound P ~++ G2) = length (G1 ~:: bound Q ~++ G2));
   try (la; simpl in |- *; reflexivity).
    assert
     (G1 ~:: bound P ~++ G2 ~:: bound T1 =
      G1 ~:: bound P ~++ (G2 ~:: bound T1)).
   simpl in |- *; reflexivity.
   rewrite H1; rewrite H2; apply IHD1_2; simpl in |- *; tauto.
Qed.

Lemma both_at_once : forall (n : nat) (Q : tp),
                     size Q <= n -> 
                     trans_stmt Q /\ narrow_stmt Q.
Proof.
intro n; induction n; intros Q sQ.
 assert (size Q > 0); [ apply size_non_zero | elimtype False; omega ].
 split.
  apply transitivity_case; intros; assert (trans_stmt Q' /\ narrow_stmt Q');
   try tauto; apply IHn; omega.
  apply narrow_case.
    intros.
    apply transitivity_case; intros Q1 sQ1;
     assert (trans_stmt Q1 /\ narrow_stmt Q1); try tauto; 
     apply IHn; omega.
Qed.

Lemma subtp_trans : forall (G : ctxt) (S Q T : tp),
                    G |- S <:: Q -> 
                    G |- Q <:: T -> 
                    G |- S <:: T.
Proof.
intros G S Q; generalize G S; clear G S.
refine (proj1 (both_at_once (size Q) Q _)); omega.
Qed.

End tn_sec.