### 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