SortV6.v

Require General.
Require Export Relations.

Section SortsOfV6.

  (* Definition des composantes du calcul *)

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

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

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

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

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

  Definition univ: srt_v6->srt_v6->Prop := (clos_refl_trans ? univ_v6).

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

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

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

  Hints Resolve iu_prop iu_pr_ty iu_type : pts.

  Lemma inv_univ_trans: (x,y,z:srt_v6)(inv_univ x y)->(inv_univ y z)
                            ->(inv_univ x z).
(Induction 1; Intros; Auto with arith pts).
(Inversion_clear H0; 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_v6)(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 v6_sort_dec: (s,s':srt_v6)(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).
(Left; Elim y; Auto with arith pts).

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

  Lemma univ_v6_dec: (s,s':srt_v6)(decide (univ s s')).
Realizer [s,s':srt_v6]
  Cases s s' of
    (Sprop c) (Sprop c') => (calc_dec c c')
  | (Sprop _) (Stype _) => true
  | (Stype n) (Stype n') => (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 (Stype n) (Sprop t); Intros; Auto with arith pts).
Inversion_clear H0.

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

  (* Inference des axiomes et regles *)

  Lemma v6_inf_axiom: (s:srt_v6)
      { sp:srt_v6 | (ppal (axiom_v6 s) univ sp) }.
Realizer [s:srt_v6]
  Cases s of
    (Sprop c) => (Stype O)
  | (Stype n) => (Stype (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 v6_inf_rule: (x1,x2:srt_v6)
       { x3:srt_v6 | (rules_v6 x1 x2 x3) &
                         (s1,s2,s3:srt_v6)(rules_v6 s1 s2 s3)
                            ->(univ x1 s1)->(univ x2 s2)->(univ x3 s3) }.
Realizer [x1,x2:srt_v6]
  Cases x1 x2 of
    (Sprop c) _ => x2
  | (Stype n) (Sprop c') => (Sprop c')
  | (Stype n) (Stype n') => (Stype (max_nat n n'))
  end.
Program_all.
(Induction 1; Intros; Auto with arith pts).
(Apply univ_trans with (Stype 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).

(Apply univ_inv with (Sprop c') s2; Intros; Auto with arith pts).
Generalize H.
(Inversion_clear H3; Intros; Auto with arith pts).
(Inversion_clear H3; Auto with arith pts).

(Inversion_clear H3; Auto with arith pts).

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

Intros.
(Apply univ_inv with (Stype n) s1; Intros; Auto with arith pts).
(Apply univ_inv with (Stype 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 SortsOfV6.

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

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

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

23/12/98, 14:30