
Require Import General.
Require Export Relations.

Unset Standard Proposition Elimination Names.

Section SortsOfECC.

  Inductive calc : Set :=
    | Pos : calc
    | Neg : calc.

  Inductive srt_ecc : Set :=
    | Sprop : calc -> srt_ecc
    | Stype : calc -> nat -> srt_ecc.

  Inductive axiom_ecc : srt_ecc -> srt_ecc -> Prop :=
    | ax_prop : forall (c : calc) (n : nat), axiom_ecc (Sprop c) (Stype c n)
    | ax_type :
        forall (c : calc) (n m : nat),
        n < m -> axiom_ecc (Stype c n) (Stype c m).

  Inductive rules_ecc : srt_ecc -> srt_ecc -> srt_ecc -> Prop :=
    | rule_prop_l : forall (c : calc) (s : srt_ecc), rules_ecc (Sprop c) s s
    | rule_prop_r :
        forall (c : calc) (s : srt_ecc), rules_ecc s (Sprop c) (Sprop c)
    | rule_type :
        forall (c1 c2 : calc) (n m p : nat),
        n <= p -> m <= p -> rules_ecc (Stype c1 n) (Stype c2 m) (Stype c2 p).

  Inductive univ_ecc : srt_ecc -> srt_ecc -> Prop :=
      univ_type :
        forall (c : calc) (n m : nat),
        n <= m -> univ_ecc (Stype c n) (Stype c m).

  Definition univ : relation srt_ecc := clos_refl_trans _ univ_ecc.

  Hint Resolve ax_prop ax_type rule_prop_l rule_prop_r rule_type univ_type:
    pts.
  Hint Unfold univ: pts.


  (* Inversion et Decidabilite de l'inclusion entre sortes *)

  Let univ_trans : forall x y z : srt_ecc, univ x y -> univ y z -> univ x z.
Proof rt_trans srt_ecc univ_ecc.


  Inductive inv_univ : srt_ecc -> srt_ecc -> Prop :=
    | iu_prop : forall c : calc, inv_univ (Sprop c) (Sprop c)
    | iu_type :
        forall (c : calc) (n m : nat),
        n <= m -> inv_univ (Stype c n) (Stype c m).

  Hint Resolve iu_prop iu_type: pts.


  Lemma inv_univ_trans :
   forall x y z : srt_ecc, inv_univ x y -> inv_univ y z -> inv_univ x z.
(* Goal: forall (s1 s2 s3 : srt_ecc) (_ : rules_ecc s1 s2 s3) (_ : univ (Sprop c) s1) (_ : univ x2 s2), univ x2 s3 *)
(* Goal: rules_ecc (Stype c n) (Sprop c') (Sprop c') *)
(* Goal: forall (s1 s2 s3 : srt_ecc) (_ : rules_ecc s1 s2 s3) (_ : univ (Stype c n) s1) (_ : univ (Sprop c') s2), univ (Sprop c') s3 *)
(* Goal: rules_ecc (Stype c n) (Stype c' n') (Stype c' (max_nat n n')) *)
(* Goal: forall (s1 s2 s3 : srt_ecc) (_ : rules_ecc s1 s2 s3) (_ : univ (Stype c n) s1) (_ : univ (Stype c' n') s2), univ (Stype c' (max_nat n n')) s3 *)
simple induction 1; intros; auto with arith pts.
(* Goal: inv_univ (Stype c n) z *)
inversion_clear H1.
(* Goal: inv_univ (Stype c n) (Stype c m0) *)
apply iu_type.
(* Goal: le n p *)
(* Goal: le n' p *)
apply le_trans with m; auto with arith pts.
Qed.


  Lemma univ_inv :
   forall s s' : srt_ecc,
   univ s s' -> forall P : Prop, (inv_univ s s' -> P) -> P.
(* Goal: forall (s s' : srt_ecc) (_ : univ s s') (P : Prop) (_ : forall _ : inv_univ s s', P), P *)
simple induction 1.
(* Goal: forall (x y : srt_ecc) (_ : univ_ecc x y) (P : Prop) (_ : forall _ : inv_univ x y, P), P *)
(* Goal: forall (x : srt_ecc) (P : Prop) (_ : forall _ : inv_univ x x, P), P *)
(* Goal: forall (x y z : srt_ecc) (_ : clos_refl_trans srt_ecc univ_ecc x y) (_ : forall (P : Prop) (_ : forall _ : inv_univ x y, P), P) (_ : clos_refl_trans srt_ecc univ_ecc y z) (_ : forall (P : Prop) (_ : forall _ : inv_univ y z, P), P) (P : Prop) (_ : forall _ : inv_univ x z, P), P *)
simple induction 1; auto with arith pts.

(* Goal: forall (x : srt_ecc) (P : Prop) (_ : forall _ : inv_univ x x, P), P *)
(* Goal: forall (x y z : srt_ecc) (_ : clos_refl_trans srt_ecc univ_ecc x y) (_ : forall (P : Prop) (_ : forall _ : inv_univ x y, P), P) (_ : clos_refl_trans srt_ecc univ_ecc y z) (_ : forall (P : Prop) (_ : forall _ : inv_univ y z, P), P) (P : Prop) (_ : forall _ : inv_univ x z, P), P *)
simple destruct x; auto with arith pts.

(* Goal: forall (s1 s2 s3 : srt_ecc) (_ : rules_ecc s1 s2 s3) (_ : univ (Stype c n) s1) (_ : univ (Stype c' n') s2), univ (Stype c' (max_nat n n')) s3 *)
intros.
(* Goal: P *)
apply H4.
(* Goal: inv_univ x z *)
apply inv_univ_trans with y.
(* Goal: inv_univ x y *)
(* Goal: inv_univ y z *)
apply H1; auto with arith pts.

(* Goal: inv_univ y z *)
apply H3; auto with arith pts.
Qed.



  Lemma calc_dec : forall c c' : calc, decide (c = c').
simple destruct c; simple destruct c';
(* Goal: univ (Sprop c') s2 *)
(* Goal: univ (Sprop c') s3 *)
(* Goal: rules_ecc (Stype c n) (Stype c' n') (Stype c' (max_nat n n')) *)
(* Goal: forall (s1 s2 s3 : srt_ecc) (_ : rules_ecc s1 s2 s3) (_ : univ (Stype c n) s1) (_ : univ (Stype c' n') s2), univ (Stype c' (max_nat n n')) s3 *)
 (right; discriminate) || auto with arith pts.
Qed.


  Lemma ecc_sort_dec : forall s s' : srt_ecc, decide (s = s').
(* Goal: forall s s' : srt_ecc, decide (@eq srt_ecc s s') *)
simple destruct s; simple destruct s'; intros; try (right; discriminate).
(* Goal: forall (s1 s2 s3 : srt_ecc) (_ : rules_ecc s1 s2 s3) (_ : univ (Stype c n) s1) (_ : univ (Stype c' n') s2), univ (Stype c' (max_nat n n')) s3 *)
elim calc_dec with c c0; intros.
(* Goal: decide (@eq srt_ecc (Sprop c) (Sprop c0)) *)
(* Goal: decide (@eq srt_ecc (Sprop c) (Sprop c0)) *)
(* Goal: decide (@eq srt_ecc (Stype c n) (Stype c0 n0)) *)
left; elim a; auto with arith pts.

(* Goal: decide (@eq srt_ecc (Stype c n) (Stype c0 n0)) *)
right; red in |- *; intros H; apply b; injection H; auto with arith pts.

(* Goal: forall (s1 s2 s3 : srt_ecc) (_ : rules_ecc s1 s2 s3) (_ : univ (Stype c n) s1) (_ : univ (Stype c' n') s2), univ (Stype c' (max_nat n n')) s3 *)
elim eq_nat_dec with n n0; intros.
(* Goal: forall (s1 s2 s3 : srt_ecc) (_ : rules_ecc s1 s2 s3) (_ : univ (Stype c n) s1) (_ : univ (Stype c' n') s2), univ (Stype c' (max_nat n n')) s3 *)
elim calc_dec with c c0; intros.
(* Goal: decide (@eq srt_ecc (Stype c n) (Stype c0 n0)) *)
(* Goal: decide (@eq srt_ecc (Stype c n) (Stype c0 n0)) *)
(* Goal: decide (@eq srt_ecc (Stype c n) (Stype c0 n0)) *)
left; elim a; elim a0; auto with arith pts.

(* Goal: decide (@eq srt_ecc (Stype c n) (Stype c0 n0)) *)
right; red in |- *; intros H; apply b; injection H; auto with arith pts.

(* Goal: decide (@eq srt_ecc (Stype c n) (Stype c0 n0)) *)
right; red in |- *; intros H; apply b; injection H; auto with arith pts.
Qed.


  Lemma univ_ecc_dec : forall s s' : srt_ecc, decide (univ s s').
refine
 (fun s s' : srt_ecc =>
  match s, s' return (decide (univ s s')) with
  | Sprop c, Sprop c' => _
  | Stype c n, Stype c' n' => _
  | Sprop c, Stype c0 n => right _ _
  | Stype c n, Sprop c0 => right _ _
  end).
(* Goal: decide (univ (Sprop c) (Sprop c')) *)
(* Goal: not (univ (Sprop c) (Stype c0 n)) *)
(* Goal: not (univ (Stype c n) (Sprop c0)) *)
(* Goal: decide (univ (Stype c n) (Stype c' n')) *)
case (calc_dec c c'); [ left | right ].
(* Goal: univ (Stype c n) (Stype c' n') *)
(* Goal: not (univ (Stype c n) (Stype c' n')) *)
(* Goal: decide (univ (Stype c n) (Stype c' n')) *)
elim e; auto with arith pts.

(* Goal: not (univ (Sprop c) (Sprop c')) *)
(* Goal: not (univ (Sprop c) (Stype c0 n)) *)
(* Goal: not (univ (Stype c n) (Sprop c0)) *)
(* Goal: decide (univ (Stype c n) (Stype c' n')) *)
red in |- *; intro; apply n.
(* Goal: @eq calc c c' *)
(* Goal: not (univ (Sprop c) (Stype c0 n)) *)
(* Goal: not (univ (Stype c n) (Sprop c0)) *)
(* Goal: decide (univ (Stype c n) (Stype c' n')) *)
apply univ_inv with (Sprop c) (Sprop c'); intros; auto with arith pts.
(* Goal: @eq calc c c' *)
inversion_clear H0; auto with arith pts.

(* Goal: forall (s1 s2 s3 : srt_ecc) (_ : rules_ecc s1 s2 s3) (_ : univ (Stype c n) s1) (_ : univ (Stype c' n') s2), univ (Stype c' (max_nat n n')) s3 *)
red in |- *; intros.
(* Goal: False *)
(* Goal: not (univ (Stype c n) (Sprop c0)) *)
(* Goal: decide (univ (Stype c n) (Stype c' n')) *)
apply univ_inv with (Sprop c) (Stype c0 n); intros; auto with arith pts.

(* Goal: False *)
(* Goal: decide (univ (Stype c n) (Stype c' n')) *)
inversion_clear H0.

(* Goal: forall (s1 s2 s3 : srt_ecc) (_ : rules_ecc s1 s2 s3) (_ : univ (Stype c n) s1) (_ : univ (Stype c' n') s2), univ (Stype c' (max_nat n n')) s3 *)
red in |- *; intros.
(* Goal: False *)
(* Goal: decide (univ (Stype c n) (Stype c' n')) *)
apply univ_inv with (Stype c n) (Sprop c0); intros; auto with arith pts.
(* Goal: False *)
(* Goal: decide (univ (Stype c n) (Stype c' n')) *)
inversion_clear H0.

(* Goal: forall (s1 s2 s3 : srt_ecc) (_ : rules_ecc s1 s2 s3) (_ : univ (Stype c n) s1) (_ : univ (Stype c' n') s2), univ (Stype c' (max_nat n n')) s3 *)
case (calc_dec c c'); intros.
(* Goal: decide (univ (Stype c n) (Stype c' n')) *)
(* Goal: decide (univ (Stype c n) (Stype c' n')) *)
case (le_gt_dec n n'); [ left | right ].
(* Goal: univ (Stype c n) (Stype c' n') *)
(* Goal: not (univ (Stype c n) (Stype c' n')) *)
(* Goal: decide (univ (Stype c n) (Stype c' n')) *)
elim e; auto with arith pts.

(* Goal: forall (s1 s2 s3 : srt_ecc) (_ : rules_ecc s1 s2 s3) (_ : univ (Stype c n) s1) (_ : univ (Stype c' n') s2), univ (Stype c' (max_nat n n')) s3 *)
red in |- *; intros.
(* Goal: @eq calc c c' *)
apply univ_inv with (Stype c n) (Stype c' n'); intros; auto with arith pts.
(* Goal: False *)
(* Goal: decide (univ (Stype c n) (Stype c' n')) *)
inversion_clear H0.
(* Goal: False *)
(* Goal: decide (univ (Stype c n) (Stype c' n')) *)
absurd (n <= n'); auto with arith pts.

(* Goal: decide (univ (Stype c n) (Stype c' n')) *)
right; red in |- *; intros; apply n0.
(* Goal: @eq calc c c' *)
apply univ_inv with (Stype c n) (Stype c' n'); intros; auto with arith pts.
(* Goal: @eq calc c c' *)
inversion_clear H0; auto with arith pts.
Qed.



  (* Inference des axiomes et regles *)

  Lemma ecc_inf_axiom :
   forall s : srt_ecc, {sp : srt_ecc | ppal (axiom_ecc s) univ sp}.
refine
 (fun s : srt_ecc =>
  match s return {sp : srt_ecc | ppal (axiom_ecc s) univ sp} with
  | Sprop c => exist _ (Stype c 0) _
  | Stype c n => exist _ (Stype c (S n)) _
  end).
(* Goal: @ppal srt_ecc (axiom_ecc (Stype c n)) univ (Stype c (S n)) *)
split; intros; auto with arith pts.
(* Goal: univ (Stype c (S n)) y *)
inversion_clear H; auto with arith pts.

(* Goal: @ppal srt_ecc (axiom_ecc (Stype c n)) univ (Stype c (S n)) *)
split; intros; auto with arith pts.
(* Goal: univ (Stype c (S n)) y *)
inversion_clear H; auto with arith pts.
Qed.


  Lemma ecc_inf_rule :
   forall x1 x2 : srt_ecc,
   {x3 : srt_ecc | rules_ecc x1 x2 x3 & 
   forall s1 s2 s3 : srt_ecc,
   rules_ecc s1 s2 s3 -> univ x1 s1 -> univ x2 s2 -> univ x3 s3}.
refine
 (fun x1 x2 : srt_ecc =>
  match
    x1, x2
    return
      {x3 : srt_ecc | rules_ecc x1 x2 x3 & 
      forall s1 s2 s3 : srt_ecc,
      rules_ecc s1 s2 s3 -> univ x1 s1 -> univ x2 s2 -> univ x3 s3}
  with
  | Sprop c, _ => exist2 _ _ x2 _ _
  | Stype c n, Sprop c' => exist2 _ _ (Sprop c') _ _
  | Stype c n, Stype c' n' => exist2 _ _ (Stype c' (max_nat n n')) _ _
  end).
(* Goal: rules_ecc (Stype c n) (Sprop c') (Sprop c') *)
(* Goal: forall (s1 s2 s3 : srt_ecc) (_ : rules_ecc s1 s2 s3) (_ : univ (Stype c n) s1) (_ : univ (Sprop c') s2), univ (Sprop c') s3 *)
(* Goal: rules_ecc (Stype c n) (Stype c' n') (Stype c' (max_nat n n')) *)
(* Goal: forall (s1 s2 s3 : srt_ecc) (_ : rules_ecc s1 s2 s3) (_ : univ (Stype c n) s1) (_ : univ (Stype c' n') s2), univ (Stype c' (max_nat n n')) s3 *)
auto with pts.

(* Goal: forall (s1 s2 s3 : srt_ecc) (_ : rules_ecc s1 s2 s3) (_ : univ (Sprop c) s1) (_ : univ x2 s2), univ x2 s3 *)
(* Goal: rules_ecc (Stype c n) (Sprop c') (Sprop c') *)
(* Goal: forall (s1 s2 s3 : srt_ecc) (_ : rules_ecc s1 s2 s3) (_ : univ (Stype c n) s1) (_ : univ (Sprop c') s2), univ (Sprop c') s3 *)
(* Goal: rules_ecc (Stype c n) (Stype c' n') (Stype c' (max_nat n n')) *)
(* Goal: forall (s1 s2 s3 : srt_ecc) (_ : rules_ecc s1 s2 s3) (_ : univ (Stype c n) s1) (_ : univ (Stype c' n') s2), univ (Stype c' (max_nat n n')) s3 *)
simple induction 1; intros; auto with arith pts.
(* Goal: univ x2 (Stype c2 p) *)
(* Goal: rules_ecc (Stype c n) (Sprop c') (Sprop c') *)
(* Goal: forall (s1 s2 s3 : srt_ecc) (_ : rules_ecc s1 s2 s3) (_ : univ (Stype c n) s1) (_ : univ (Sprop c') s2), univ (Sprop c') s3 *)
(* Goal: rules_ecc (Stype c n) (Stype c' n') (Stype c' (max_nat n n')) *)
(* Goal: forall (s1 s2 s3 : srt_ecc) (_ : rules_ecc s1 s2 s3) (_ : univ (Stype c n) s1) (_ : univ (Stype c' n') s2), univ (Stype c' (max_nat n n')) s3 *)
apply univ_trans with (Stype c2 m); auto with arith pts.

(* Goal: rules_ecc (Stype c n) (Sprop c') (Sprop c') *)
(* Goal: forall (s1 s2 s3 : srt_ecc) (_ : rules_ecc s1 s2 s3) (_ : univ (Stype c n) s1) (_ : univ (Sprop c') s2), univ (Sprop c') s3 *)
(* Goal: rules_ecc (Stype c n) (Stype c' n') (Stype c' (max_nat n n')) *)
(* Goal: forall (s1 s2 s3 : srt_ecc) (_ : rules_ecc s1 s2 s3) (_ : univ (Stype c n) s1) (_ : univ (Stype c' n') s2), univ (Stype c' (max_nat n n')) s3 *)
auto with pts.

(* Goal: forall (s1 s2 s3 : srt_ecc) (_ : rules_ecc s1 s2 s3) (_ : univ (Stype c n) s1) (_ : univ (Stype c' n') s2), univ (Stype c' (max_nat n n')) s3 *)
intros.
(* Goal: forall (s1 s2 s3 : srt_ecc) (_ : rules_ecc s1 s2 s3) (_ : univ (Stype c n) s1) (_ : univ (Stype c' n') s2), univ (Stype c' (max_nat n n')) s3 *)
apply univ_inv with (Sprop c') s2; intros.
(* Goal: univ (Sprop c') s2 *)
(* Goal: univ (Sprop c') s3 *)
(* Goal: rules_ecc (Stype c n) (Stype c' n') (Stype c' (max_nat n n')) *)
(* Goal: forall (s1 s2 s3 : srt_ecc) (_ : rules_ecc s1 s2 s3) (_ : univ (Stype c n) s1) (_ : univ (Stype c' n') s2), univ (Stype c' (max_nat n n')) s3 *)
auto with arith pts.

(* Goal: univ (Stype c' (max_nat n n')) s3 *)
generalize H.
(* Goal: forall (s1 s2 s3 : srt_ecc) (_ : rules_ecc s1 s2 s3) (_ : univ (Stype c n) s1) (_ : univ (Stype c' n') s2), univ (Stype c' (max_nat n n')) s3 *)
inversion_clear H2; intros.
(* Goal: univ (Sprop c') s2 *)
(* Goal: univ (Sprop c') s3 *)
(* Goal: rules_ecc (Stype c n) (Stype c' n') (Stype c' (max_nat n n')) *)
(* Goal: forall (s1 s2 s3 : srt_ecc) (_ : rules_ecc s1 s2 s3) (_ : univ (Stype c n) s1) (_ : univ (Stype c' n') s2), univ (Stype c' (max_nat n n')) s3 *)
inversion_clear H2; auto with arith pts.

(* Goal: rules_ecc (Stype c n) (Stype c' n') (Stype c' (max_nat n n')) *)
(* Goal: forall (s1 s2 s3 : srt_ecc) (_ : rules_ecc s1 s2 s3) (_ : univ (Stype c n) s1) (_ : univ (Stype c' n') s2), univ (Stype c' (max_nat n n')) s3 *)
unfold max_nat in |- *.
(* Goal: univ (Sprop c') s2 *)
(* Goal: univ (Sprop c') s3 *)
(* Goal: rules_ecc (Stype c n) (Stype c' n') (Stype c' (max_nat n n')) *)
(* Goal: forall (s1 s2 s3 : srt_ecc) (_ : rules_ecc s1 s2 s3) (_ : univ (Stype c n) s1) (_ : univ (Stype c' n') s2), univ (Stype c' (max_nat n n')) s3 *)
elim (le_gt_dec n n'); auto with arith pts.

(* Goal: forall (s1 s2 s3 : srt_ecc) (_ : rules_ecc s1 s2 s3) (_ : univ (Stype c n) s1) (_ : univ (Stype c' n') s2), univ (Stype c' (max_nat n n')) s3 *)
intros.
(* Goal: univ (Sprop c') s2 *)
(* Goal: univ (Sprop c') s3 *)
(* Goal: rules_ecc (Stype c n) (Stype c' n') (Stype c' (max_nat n n')) *)
(* Goal: forall (s1 s2 s3 : srt_ecc) (_ : rules_ecc s1 s2 s3) (_ : univ (Stype c n) s1) (_ : univ (Stype c' n') s2), univ (Stype c' (max_nat n n')) s3 *)
apply univ_inv with (Stype c n) s1; intros; auto with arith pts.
(* Goal: univ (Sprop c') s2 *)
(* Goal: univ (Sprop c') s3 *)
(* Goal: rules_ecc (Stype c n) (Stype c' n') (Stype c' (max_nat n n')) *)
(* Goal: forall (s1 s2 s3 : srt_ecc) (_ : rules_ecc s1 s2 s3) (_ : univ (Stype c n) s1) (_ : univ (Stype c' n') s2), univ (Stype c' (max_nat n n')) s3 *)
apply univ_inv with (Stype c' n') s2; intros; auto with arith pts.
(* Goal: univ (Stype c' (max_nat n n')) s3 *)
generalize H.
(* Goal: forall _ : rules_ecc s1 s2 s3, univ (Stype c' (max_nat n n')) s3 *)
inversion_clear H2.
(* Goal: forall (s1 s2 s3 : srt_ecc) (_ : rules_ecc s1 s2 s3) (_ : univ (Stype c n) s1) (_ : univ (Stype c' n') s2), univ (Stype c' (max_nat n n')) s3 *)
inversion_clear H3; intros.
(* Goal: univ (Stype c' (max_nat n n')) s3 *)
inversion_clear H3.
(* Goal: univ (Sprop c') s2 *)
(* Goal: univ (Sprop c') s3 *)
(* Goal: rules_ecc (Stype c n) (Stype c' n') (Stype c' (max_nat n n')) *)
(* Goal: forall (s1 s2 s3 : srt_ecc) (_ : rules_ecc s1 s2 s3) (_ : univ (Stype c n) s1) (_ : univ (Stype c' n') s2), univ (Stype c' (max_nat n n')) s3 *)
cut (max_nat n n' <= p); auto with arith pts.
(* Goal: le (max_nat n n') p *)
apply least_upper_bound_max_nat.
(* Goal: le n p *)
(* Goal: le n' p *)
apply le_trans with m; auto with arith pts.

(* Goal: univ (Sprop c') s2 *)
(* Goal: univ (Sprop c') s3 *)
(* Goal: rules_ecc (Stype c n) (Stype c' n') (Stype c' (max_nat n n')) *)
(* Goal: forall (s1 s2 s3 : srt_ecc) (_ : rules_ecc s1 s2 s3) (_ : univ (Stype c n) s1) (_ : univ (Stype c' n') s2), univ (Stype c' (max_nat n n')) s3 *)
apply le_trans with m0; auto with arith pts.
Qed.


End SortsOfECC.

(* Uniform interface of sorts *)
Require Export GenericSort.

  Definition sort_of_gen (gs : gen_sort) : Exc srt_ecc :=
    match gs with
    | Gprop => value (Sprop Neg)
    | Gset => value (Sprop Pos)
    | Gtype n => value (Stype Neg n)
    | Gtypeset n => value (Stype Pos n)
    end.

  Definition gen_of_sort (s : srt_ecc) : gen_sort :=
    match s with
    | Sprop Neg => Gprop
    | Sprop Pos => Gset
    | Stype Neg n => Gtype n
    | Stype Pos n => Gtypeset n
    end.
