SortECC.v

Require General.
Require Export Relations.

Section SortsOfECC.

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

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

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

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

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

  Definition univ: (relation srt_ecc) := (clos_refl_trans ? univ_ecc).

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

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

  Local univ_trans: (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: (c:calc)(inv_univ (Sprop c) (Sprop c))
  | iu_type: (c:calc)(n,m:nat)(le n m)->(inv_univ (Stype c n) (Stype c m)).

  Hints Resolve iu_prop iu_type : pts.

  Lemma inv_univ_trans: (x,y,z:srt_ecc)(inv_univ x y)->(inv_univ y z)
                            ->(inv_univ x z).
(Induction 1; Intros; Auto with arith pts).
Inversion_clear H1.
Apply iu_type.
(Apply le_trans with m; Auto with arith pts).
Save.

  Lemma univ_inv: (s,s':srt_ecc)(univ s s')
                    ->(P:Prop)((inv_univ s s')->P)->P.
Induction 1.
(Induction 1; Auto with arith pts).

(Destruct x; Auto with arith pts).

Intros.
Apply H4.
Apply inv_univ_trans with y.
(Apply H1; Auto with arith pts).

(Apply H3; Auto with arith pts).
Save.

  Lemma calc_dec: (c,c':calc)(decide c=c').
Destruct c;Destruct c';(Right;Discriminate) Orelse Auto with arith pts.
Save.

  Lemma ecc_sort_dec: (s,s':srt_ecc)(decide s=s').
(Destruct s; Destruct s'; Intros; Try (Right; Discriminate)).
(Elim calc_dec with c c0; Intros).
(Left; Elim y; Auto with arith pts).

(Right; Red; Intros H; Apply y; Injection H; Auto with arith pts).

(Elim eq_nat_dec with n n0; Intros).
(Elim calc_dec with c c0; Intros).
(Left; Elim y; Elim y0; Auto with arith pts).

(Right; Red; Intros H; Apply y0; Injection H; Auto with arith pts).

(Right; Red; Intros H; Apply y; Injection H; Auto with arith pts).
Save.

  Lemma univ_ecc_dec: (s,s':srt_ecc)(decide (univ s s')).
Realizer [s,s':srt_ecc]
  Cases s s' of
    (Sprop c) (Sprop c') => (calc_dec c c')
  | (Stype c n) (Stype c' n') => (andb (calc_dec c c') (le_gt_dec n n'))
  | _ _ => false
  end.
Program_all.
(Elim e; Auto with arith pts).

(Red; Intro; Apply n).
(Apply univ_inv with (Sprop c) (Sprop c'); Intros; Auto with arith pts).
(Inversion_clear H0; Auto with arith pts).

(Red; Intros).
(Apply univ_inv with (Sprop c) (Stype t0 t); Intros; Auto with arith pts).

Inversion_clear H0.

(Red; Intros).
(Apply univ_inv with (Stype c n) (Sprop t); Intros; Auto with arith pts).
Inversion_clear H0.

(Elim e; Auto with arith pts).

(Red; Intros).
(Apply univ_inv with (Stype c n) (Stype c' n'); Intros; Auto with arith pts).
Inversion_clear H0.
(Absurd (le n n'); Auto with arith pts).

(Red; Intros; Apply n0).
(Apply univ_inv with (Stype c n) (Stype c' n'); Intros; Auto with arith pts).
Inversion_clear H0;Auto with arith pts.
Save.

  (* Inference des axiomes et regles *)

  Lemma ecc_inf_axiom: (s:srt_ecc)
      { sp:srt_ecc | (ppal (axiom_ecc s) univ sp) }.
Realizer [s:srt_ecc]
  Cases s of
    (Sprop c) => (Stype c O)
  | (Stype c n) => (Stype c (S n))
  end.
Program_all.
(Split; Intros; Auto with arith pts).
(Inversion_clear H; Auto with arith pts).

(Split; Intros; Auto with arith pts).
(Inversion_clear H; Auto with arith pts).
Save.

  Lemma ecc_inf_rule: (x1,x2:srt_ecc)
       { x3:srt_ecc | (rules_ecc x1 x2 x3) &
                         (s1,s2,s3:srt_ecc)(rules_ecc s1 s2 s3)
                            ->(univ x1 s1)->(univ x2 s2)->(univ x3 s3) }.
Realizer [x1,x2:srt_ecc]
  Cases x1 x2 of
    (Sprop c) _ => x2
  | (Stype c n) (Sprop c') => (Sprop c')
  | (Stype c n) (Stype c' n') => (Stype c' (max_nat n n'))
  end.
Program_all.
(Induction 1; Intros; Auto with arith pts).
(Apply univ_trans with (Stype c2 m); Auto with arith pts).

Intros.
(Apply univ_inv with (Sprop c') s2; Intros).
Auto with arith pts.

Generalize H .
(Inversion_clear H2; Intros).
(Inversion_clear H2; Auto with arith pts).

Unfold max_nat .
(Elim (le_gt_dec n n'); Auto with arith pts).

Intros.
(Apply univ_inv with (Stype c n) s1; Intros; Auto with arith pts).
(Apply univ_inv with (Stype c' n') s2; Intros; Auto with arith pts).
Generalize H .
Inversion_clear H2.
(Inversion_clear H3; Intros).
Inversion_clear H3.
(Cut (le (max_nat n n') p); Auto with arith pts).
Apply least_upper_bound_max_nat.
(Apply le_trans with m; Auto with arith pts).

(Apply le_trans with m0; Auto with arith pts).
Save.

End SortsOfECC.

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

  Definition sort_of_gen: gen_sort -> (Exc srt_ecc) :=
    [gs]Cases gs of
          Gprop => (value ? (Sprop Neg))
        | Gset => (value ? (Sprop Pos))
        | (Gtype n) => (value ? (Stype Neg n))
        | (Gtypeset n) => (value ? (Stype Pos n))
        | _ => (error ?)
        end.

  Definition gen_of_sort: srt_ecc -> gen_sort :=
    [s]Cases s of
         (Sprop Neg) => Gprop
       | (Sprop Pos) => Gset
       | (Stype Neg n) => (Gtype n)
       | (Stype Pos n) => (Gtypeset n)
       end.

23/12/98, 14:30