Require Import base ord.

Inductive sort :=
| prop
| type (n : nat).

Definition nat_le (m n : nat) : Prop := (m <= n)%bool.

Lemma nat_le_refl n : nat_le n n.
Proof. exact: leqnn. Qed.

Lemma nat_le_trans : transitive nat_le.
Proof. move=> x y z. exact: leq_trans. Qed.

Lemma nat_le_eq m n : nat_le m n -> nat_le n m -> m = n.
Proof.
  move=> le_m_n le_n_m. apply/eqP. by rewrite eqn_leq le_m_n le_n_m.
Qed.

Canonical nat_proMixin := ProMixin nat_le_refl nat_le_trans.
Canonical nat_proType := Eval hnf in ProType nat nat_proMixin.
Canonical nat_ordMixin := OrdMixin nat_le_eq.
Canonical nat_ordType := Eval hnf in OrdType nat nat_ordMixin.

Lemma nat_le_E (m n : nat) : (m ≤ n) = (m <= n).
Proof. by []. Qed.

Definition sort_le (m n : sort) : Prop :=
  match m, n with
  | prop, _ => True
  | _, prop => False
  | type m, type n => m ≤ n
  end.

Lemma sort_le_refl n : sort_le n n.
Proof. by case n=> /=. Qed.

Lemma sort_le_trans : transitive sort_le.
Proof. move=> []//m[]//=n[]//=k. exact: le_trans. Qed.

Lemma sort_le_eq m n : sort_le m n -> sort_le n m -> m = n.
Proof.
  destruct m, n => //= l1 l2. apply: ap. exact: le_eq.
Qed.

Canonical sort_proMixin := ProMixin sort_le_refl sort_le_trans.
Canonical sort_proType := Eval hnf in ProType sort sort_proMixin.
Canonical sort_ordMixin := OrdMixin sort_le_eq.
Canonical sort_ordType := Eval hnf in OrdType sort sort_ordMixin.

Definition sort_prod (m n : sort) : sort :=
  match m, n with
  | _, prop => prop
  | prop, _ => n
  | type m, type n => type (maxn m n)
  end.

Lemma sort_le_typeE m n :
  (type m ≤ type n) = (m <= n).
Proof. by []. Qed.

Global Instance sort_prod_proper :
  Proper (ord_op ++> ord_op ++> ord_op) sort_prod.
Proof.
  move=> [|m1] [|m2]//= l1 [|n1] [|n2] //= l2 /=.
  - apply: le_trans l2 _. rewrite sort_le_typeE. exact: leq_maxr.
  - rewrite sort_le_typeE geq_max. apply/andP; split.
    apply: leq_trans l1 _. exact: leq_maxl.
    apply: leq_trans l2 _. exact: leq_maxr.
Qed.

Definition sort_succ (m : sort) : sort :=
  match m with
  | prop => type 0
  | type m => type m.+1
  end.