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