Require Import base ord ars data.fintype ccomega.sorts
        ccomega.syntax ccomega.reduction ccomega.churchrosser.

Inductive sub1 {n} : tm n -> tm n -> Prop :=
| sub1_refl A : sub1 A A
| sub1_sort u v : u ≤ v -> sub1 (univ n u) (univ n v)
| sub1_prod A B1 B2 : @sub1 n.+1 B1 B2 -> sub1 (prod A B1) (prod A B2).

CoInductive sub {n} (A B : tm n) : Prop :=
| SubI A' B' : sub1 A' B' -> A === A' -> B' === B -> sub A B.
Infix "<:" := sub (at level 50, no associativity).

Lemma sub1_sub n (A B : tm n) : sub1 A B -> sub A B. move=> /SubI. exact. Qed.
Lemma sub1_conv n (B A C : tm n) : sub1 A B -> B === C -> A <: C. move=>/SubI. exact. Qed.
Lemma conv_sub1 n (B A C : tm n) : A === B -> sub1 B C -> A <: C. move=>c/SubI. exact. Qed.

Lemma conv_sub n (A B : tm n) : A === B -> A <: B.
Proof. move/conv_sub1. apply. exact: sub1_refl. Qed.

Lemma sub_refl n (A : tm n) : A <: A.
Proof. apply: sub1_sub. exact: sub1_refl. Qed.
Hint Resolve sub_refl.

Lemma sub_sort n u v : u ≤ v -> univ n u <: univ n v.
Proof. move=> leq. exact/sub1_sub/sub1_sort. Qed.

Lemma sub1_trans n (A B C D : tm n) :
  sub1 A B -> B === C -> sub1 C D -> A <: D.
Proof with eauto using @sub1, @sub1_sub, @sub1_conv, @conv_sub1.
  move=> sb. elim: sb C D => {n A B}
    [n A C D|n u v leq C D conv sb|n A B1 B2 sb1 ih C D conv sb2]...
  - inv sb...
    + apply: sub_sort. move: conv => /inj_sort eqn. subst.
      exact: le_trans leq _.
    + exfalso. exact: conv_prod_sort (conv_sym conv).
  - inv sb2...
    + exfalso. exact: conv_prod_sort conv.
    + move: conv => /inj_prod[conv1 conv2].
      move: (ih _ _ conv2 H) => {ih} sub. inv sub.
      eapply SubI. eapply sub1_prod... eapply conv_prod... exact: conv_prod.
Qed.

Lemma sub_trans n (B A C : tm n) :
  A <: B -> B <: C -> A <: C.
Proof.
  move=> [A' B' s1 c1 c2] [B'' C' s2 c3 c4]. move: (conv_trans _ c2 c3) => h.
  case: (sub1_trans s1 h s2) => A0 B0 s3 c5 c6. apply: (SubI s3).
  exact: conv_trans c5. exact: conv_trans c4.
Qed.

Lemma sub_prod_inv n (A1 A2 : tm n) B1 B2 :
  prod A1 B1 <: prod A2 B2 -> A1 === A2 /\ B1 <: B2.
Proof.
  move=> [A' B' []].
  - move=> C c1 c2. have{c1 c2}/inj_prod[c1 c2]: prod A1 B1 === prod A2 B2.
     exact: conv_trans c2.
    split=>//. exact: conv_sub.
  - by move=> u _ _ /conv_prod_sort[].
  - move=> A C1 C2 sb /inj_prod[c1 c2] /inj_prod[c3 c4]. split.
    exact: conv_trans c3. exact: SubI sb c2 c4.
Qed.

Lemma sub1_inst m n (sigma : subst m n) A B :
  sub1 A B -> sub1 (inst sigma A) (inst sigma B).
Proof. move=> s. elim: s n sigma => /=; eauto using @sub1. Qed.

Lemma sub_inst m n (sigma : subst m n) A B :
  A <: B -> inst sigma A <: inst sigma B.
Proof. move=> [A' B' /sub1_inst]; eauto using @sub, @conv_subst. Qed.