
Require Import General.
Require Export Relations.

Unset Standard Proposition Elimination Names.

Section SortsOfV6.

  (* Definition des composantes du calcul *)

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

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

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

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

  Inductive univ_v6 : srt_v6 -> srt_v6 -> Prop :=
    | univ_prop : forall (c : calc) (n : nat), univ_v6 (Sprop c) (Stype n)
    | univ_type : forall n m : nat, n <= m -> univ_v6 (Stype n) (Stype m).

  Definition univ : srt_v6 -> srt_v6 -> Prop := clos_refl_trans _ univ_v6.

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

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

  Let univ_trans : forall x y z : srt_v6, univ x y -> univ y z -> univ x z.
Proof rt_trans srt_v6 univ_v6.


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

  Hint Resolve iu_prop iu_pr_ty iu_type: pts.


  Lemma inv_univ_trans :
   forall x y z : srt_v6, inv_univ x y -> inv_univ y z -> inv_univ x z.
(* Goal: forall (s1 s2 s3 : srt_v6) (_ : rules_v6 s1 s2 s3) (_ : univ (Sprop c) s1) (_ : univ x2 s2), univ x2 s3 *)
(* Goal: forall (s1 s2 s3 : srt_v6) (_ : rules_v6 s1 s2 s3) (_ : univ (Stype n) s1) (_ : univ (Sprop c') s2), univ (Sprop c') s3 *)
(* Goal: rules_v6 (Stype n) (Stype n') (Stype (max_nat n n')) *)
(* Goal: forall (s1 s2 s3 : srt_v6) (_ : rules_v6 s1 s2 s3) (_ : univ (Stype n) s1) (_ : univ (Stype n') s2), univ (Stype (max_nat n n')) s3 *)
simple induction 1; intros; auto with arith pts.
(* Goal: @eq calc c c' *)
(* Goal: univ (Sprop c) (Stype n) *)
(* Goal: not (univ (Stype n) (Sprop c)) *)
(* Goal: decide (univ (Stype n) (Stype n')) *)
inversion_clear H0; auto with arith pts.

(* Goal: inv_univ (Stype n) z *)
inversion_clear H1.
(* Goal: inv_univ (Stype n) (Stype 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_v6,
   univ s s' -> forall P : Prop, (inv_univ s s' -> P) -> P.
(* Goal: forall (s s' : srt_v6) (_ : univ s s') (P : Prop) (_ : forall _ : inv_univ s s', P), P *)
simple induction 1.
(* Goal: forall (x y : srt_v6) (_ : univ_v6 x y) (P : Prop) (_ : forall _ : inv_univ x y, P), P *)
(* Goal: forall (x : srt_v6) (P : Prop) (_ : forall _ : inv_univ x x, P), P *)
(* Goal: forall (x y z : srt_v6) (_ : clos_refl_trans srt_v6 univ_v6 x y) (_ : forall (P : Prop) (_ : forall _ : inv_univ x y, P), P) (_ : clos_refl_trans srt_v6 univ_v6 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_v6) (P : Prop) (_ : forall _ : inv_univ x x, P), P *)
(* Goal: forall (x y z : srt_v6) (_ : clos_refl_trans srt_v6 univ_v6 x y) (_ : forall (P : Prop) (_ : forall _ : inv_univ x y, P), P) (_ : clos_refl_trans srt_v6 univ_v6 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_v6) (_ : rules_v6 s1 s2 s3) (_ : univ (Stype n) s1) (_ : univ (Stype n') s2), univ (Stype (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';
 (right; discriminate) || auto with arith pts.
Qed.


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

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

(* Goal: forall (s1 s2 s3 : srt_v6) (_ : rules_v6 s1 s2 s3) (_ : univ (Stype n) s1) (_ : univ (Stype n') s2), univ (Stype (max_nat n n')) s3 *)
elim eq_nat_dec with n n0; intros.
(* Goal: decide (@eq srt_v6 (Stype n) (Stype n0)) *)
(* Goal: decide (@eq srt_v6 (Stype n) (Stype n0)) *)
left; elim a; auto with arith pts.

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


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

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

(* Goal: univ (Stype n) (Stype n') *)
(* Goal: not (univ (Stype n) (Stype n')) *)
auto with pts.

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

(* Goal: decide (univ (Stype n) (Stype n')) *)
case (le_gt_dec n n'); [ left | right ].
(* Goal: univ (Stype n) (Stype n') *)
(* Goal: not (univ (Stype n) (Stype n')) *)
auto with pts.

(* Goal: forall (s1 s2 s3 : srt_v6) (_ : rules_v6 s1 s2 s3) (_ : univ (Stype n) s1) (_ : univ (Stype n') s2), univ (Stype (max_nat n n')) s3 *)
red in |- *; intros.
(* Goal: False *)
apply univ_inv with (Stype n) (Stype n'); intros; auto with arith pts.
(* Goal: False *)
inversion_clear H0.
(* Goal: False *)
absurd (n <= n'); auto with arith pts.
Qed.


  (* Inference des axiomes et regles *)

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

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


  Lemma v6_inf_rule :
   forall x1 x2 : srt_v6,
   {x3 : srt_v6 | rules_v6 x1 x2 x3 & 
   forall s1 s2 s3 : srt_v6,
   rules_v6 s1 s2 s3 -> univ x1 s1 -> univ x2 s2 -> univ x3 s3}.
refine
 (fun x1 x2 : srt_v6 =>
  match
    x1, x2
    return
      {x3 : srt_v6 | rules_v6 x1 x2 x3 & 
      forall s1 s2 s3 : srt_v6,
      rules_v6 s1 s2 s3 -> univ x1 s1 -> univ x2 s2 -> univ x3 s3}
  with
  | Sprop c, _ => exist2 _ _ x2 _ _
  | Stype n, Sprop c' => exist2 _ _ (Sprop c') _ _
  | Stype n, Stype n' => exist2 _ _ (Stype (max_nat n n')) _ _
(* Goal: univ (Stype n) (Stype n') *)
(* Goal: not (univ (Stype n) (Stype n')) *)
  end); auto with pts.
(* Goal: forall (s1 s2 s3 : srt_v6) (_ : rules_v6 s1 s2 s3) (_ : univ (Sprop c) s1) (_ : univ x2 s2), univ x2 s3 *)
(* Goal: forall (s1 s2 s3 : srt_v6) (_ : rules_v6 s1 s2 s3) (_ : univ (Stype n) s1) (_ : univ (Sprop c') s2), univ (Sprop c') s3 *)
(* Goal: rules_v6 (Stype n) (Stype n') (Stype (max_nat n n')) *)
(* Goal: forall (s1 s2 s3 : srt_v6) (_ : rules_v6 s1 s2 s3) (_ : univ (Stype n) s1) (_ : univ (Stype n') s2), univ (Stype (max_nat n n')) s3 *)
simple induction 1; intros; auto with arith pts.
(* Goal: univ x2 (Stype p) *)
(* Goal: forall (s1 s2 s3 : srt_v6) (_ : rules_v6 s1 s2 s3) (_ : univ (Stype n) s1) (_ : univ (Sprop c') s2), univ (Sprop c') s3 *)
(* Goal: rules_v6 (Stype n) (Stype n') (Stype (max_nat n n')) *)
(* Goal: forall (s1 s2 s3 : srt_v6) (_ : rules_v6 s1 s2 s3) (_ : univ (Stype n) s1) (_ : univ (Stype n') s2), univ (Stype (max_nat n n')) s3 *)
apply univ_trans with (Stype m); auto with arith pts.

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

(* Goal: univ (Sprop c') s3 *)
(* Goal: rules_v6 (Stype n) (Stype n') (Stype (max_nat n n')) *)
(* Goal: forall (s1 s2 s3 : srt_v6) (_ : rules_v6 s1 s2 s3) (_ : univ (Stype n) s1) (_ : univ (Stype n') s2), univ (Stype (max_nat n n')) s3 *)
apply univ_inv with (Sprop c') s2; intros; auto with arith pts.
(* Goal: univ (Stype (max_nat n n')) s3 *)
generalize H.
(* Goal: forall _ : rules_v6 s1 s2 s3, univ (Sprop c') s3 *)
(* Goal: rules_v6 (Stype n) (Stype n') (Stype (max_nat n n')) *)
(* Goal: forall (s1 s2 s3 : srt_v6) (_ : rules_v6 s1 s2 s3) (_ : univ (Stype n) s1) (_ : univ (Stype n') s2), univ (Stype (max_nat n n')) s3 *)
inversion_clear H3; intros; auto with arith pts.
(* Goal: univ (Sprop c') s3 *)
(* Goal: rules_v6 (Stype n) (Stype n') (Stype (max_nat n n')) *)
(* Goal: forall (s1 s2 s3 : srt_v6) (_ : rules_v6 s1 s2 s3) (_ : univ (Stype n) s1) (_ : univ (Stype n') s2), univ (Stype (max_nat n n')) s3 *)
inversion_clear H3; auto with arith pts.

(* Goal: univ (Sprop c') s3 *)
(* Goal: rules_v6 (Stype n) (Stype n') (Stype (max_nat n n')) *)
(* Goal: forall (s1 s2 s3 : srt_v6) (_ : rules_v6 s1 s2 s3) (_ : univ (Stype n) s1) (_ : univ (Stype n') s2), univ (Stype (max_nat n n')) s3 *)
inversion_clear H3; auto with arith pts.

(* Goal: rules_v6 (Stype n) (Stype n') (Stype (max_nat n n')) *)
(* Goal: forall (s1 s2 s3 : srt_v6) (_ : rules_v6 s1 s2 s3) (_ : univ (Stype n) s1) (_ : univ (Stype n') s2), univ (Stype (max_nat n n')) s3 *)
unfold max_nat in |- *.
(* Goal: rules_v6 (Stype n) (Stype n') (Stype (if le_gt_dec n n' then n' else n)) *)
(* Goal: forall (s1 s2 s3 : srt_v6) (_ : rules_v6 s1 s2 s3) (_ : univ (Stype n) s1) (_ : univ (Stype n') s2), univ (Stype (max_nat n n')) s3 *)
elim (le_gt_dec n n'); auto with arith pts.

(* Goal: forall (s1 s2 s3 : srt_v6) (_ : rules_v6 s1 s2 s3) (_ : univ (Stype n) s1) (_ : univ (Stype n') s2), univ (Stype (max_nat n n')) s3 *)
intros.
(* Goal: univ (Stype (max_nat n n')) s3 *)
apply univ_inv with (Stype n) s1; intros; auto with arith pts.
(* Goal: univ (Stype (max_nat n n')) s3 *)
apply univ_inv with (Stype n') s2; intros; auto with arith pts.
(* Goal: univ (Stype (max_nat n n')) s3 *)
generalize H.
(* Goal: forall _ : rules_v6 s1 s2 s3, univ (Stype (max_nat n n')) s3 *)
inversion_clear H2.
(* Goal: forall (s1 s2 s3 : srt_v6) (_ : rules_v6 s1 s2 s3) (_ : univ (Stype n) s1) (_ : univ (Stype n') s2), univ (Stype (max_nat n n')) s3 *)
inversion_clear H3; intros.
(* Goal: univ (Stype (max_nat n n')) s3 *)
inversion_clear H3.
(* Goal: univ (Stype (max_nat n n')) (Stype p) *)
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: le n' p *)
apply le_trans with m0; auto with arith pts.
Qed.


End SortsOfV6.


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

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

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