### General.v

Require Export Bool.
Require Export Arith.
Require Export Compare_dec.
Require Export Peano_dec.
Require Export MyList.
Require Export MyRelations.

Definition max_nat :=
[n,m:nat]<nat>Case (le_gt_dec n m) of
[_:(le n m)]m
[_:(gt n m)]n
end.

Lemma
least_upper_bound_max_nat: (n,m,p:nat)(le n p)->(le m p)
->(le (
max_nat n m) p).
Intros.
Unfold max_nat .
(Elim (le_gt_dec n m); Auto with arith).
Save.

Require Export Relation_Definitions.

Definition decide := [P:Prop]{P}+{~P}.

Hints Unfold
decide : core.

Inductive Acc3 [A,B,C:Set;R:(relation A*B*C)] : A->B->C->Prop :=
Acc3_intro : (x:A)(x0:B)(x1:C)
((y:A)(y0:B)(y1:C)(R (y,(y0,y1)) (x,(x0,x1)))->(
Acc3 A B C R y y0 y1))
->(Acc3 A B C R x x0 x1).

Lemma Acc3_rec: (A,B,C:Set)(R:(relation A*B*C))
(P:A->B->C->Set)((x:A)(x0:B)(x1:C)
((y:A)(y0:B)(y1:C)(R (y,(y0,y1)) (x,(x0,x1)))->(P y y0 y1))
->(P x x0 x1))
->(x:A)(x0:B)(x1:C)(
Acc3 A B C R x x0 x1)->(P x x0 x1).
Do 6 Intro.
Fix F 4.
Intros.
Apply H; Intros.
Apply F.
Generalize H1.
Case H0; Intros.
Apply H2.
Exact H3.
Save.

Lemma Acc_Acc3: (A,B,C:Set)(R:(relation A*B*C))(x:A)(y:B)(z:C)
(Acc A*B*C R (x,(y,z)))->(
Acc3 A B C R x y z).
Intros.
Change ([p:A*B*C]
<Prop>Case p of
[x2:A]
[p0:B*C]
<Prop>Case p0 of [x3:B][x4:C](Acc3 A B C R x2 x3 x4)
end
end (x,(y,z))).
Elim H.
Destruct x.
(Destruct p; Intros).
(Apply Acc3_intro; Intros).
(Apply (H1 (y0,(y1,y2))); Auto).
Save.

Implicit Arguments On.

Section Principal.

Variable A: Set; P: A->Prop; R: A->A->Prop.

Record ppal [x:A]: Prop := Pp_intro {
pp_ok: (P x);
pp_least: (y:A)(P y)->(R x y)
}.

Definition
ppal_dec: Set :=
{ x:A | (
ppal x)} + { (x:A)~(P x) }.

End Principal.

23/12/98, 14:36