

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

Set Implicit Arguments.
Unset Strict Implicit.

  Definition max_nat (n m : nat) :=
    match le_gt_dec n m with
    | left _ => m
    | right _ => n
    end.

  Lemma least_upper_bound_max_nat :
   forall n m p : nat, n <= p -> m <= p -> max_nat n m <= p.
(* Goal: forall (A B C : Set) (R : relation (prod A (prod B C))) (x : A) (y : B) (z : C) (_ : @Acc (prod A (prod B C)) R (@pair A (prod B C) x (@pair B C y z))), @Acc3 A B C R x y z *)
intros.
(* Goal: le (max_nat n m) p *)
unfold max_nat in |- *.
(* Goal: le (if le_gt_dec n m then m else n) p *)
elim (le_gt_dec n m); auto with arith.
Qed.





Require Export Relation_Definitions.

  Definition decide (P : Prop) := {P} + {~ P}.

  Hint Unfold decide: core.



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


  Lemma Acc3_rec :
   forall (A B C : Set) (R : relation (A * (B * C))) (P : A -> B -> C -> Set),
   (forall (x : A) (x0 : B) (x1 : C),
    (forall (y : A) (y0 : B) (y1 : C),
     R (y, (y0, y1)) (x, (x0, x1)) -> P y y0 y1) -> 
    P x x0 x1) ->
   forall (x : A) (x0 : B) (x1 : C), Acc3 R x x0 x1 -> P x x0 x1.
Proof.
(* Goal: forall (A B C : Set) (R : relation (prod A (prod B C))) (P : forall (_ : A) (_ : B) (_ : C), Set) (_ : forall (x : A) (x0 : B) (x1 : C) (_ : forall (y : A) (y0 : B) (y1 : C) (_ : R (@pair A (prod B C) y (@pair B C y0 y1)) (@pair A (prod B C) x (@pair B C 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.
(* Goal: forall (x : A) (x0 : B) (x1 : C) (_ : @Acc3 A B C R x x0 x1), P x x0 x1 *)
fix F 4.
(* Goal: forall (A B C : Set) (R : relation (prod A (prod B C))) (x : A) (y : B) (z : C) (_ : @Acc (prod A (prod B C)) R (@pair A (prod B C) x (@pair B C y z))), @Acc3 A B C R x y z *)
intros.
(* Goal: forall (A B C : Set) (R : relation (prod A (prod B C))) (x : A) (y : B) (z : C) (_ : @Acc (prod A (prod B C)) R (@pair A (prod B C) x (@pair B C y z))), @Acc3 A B C R x y z *)
apply H; intros.
(* Goal: P y y0 y1 *)
apply F.
(* Goal: @Acc3 A B C R y y0 y1 *)
generalize H1.
(* Goal: forall (A B C : Set) (R : relation (prod A (prod B C))) (x : A) (y : B) (z : C) (_ : @Acc (prod A (prod B C)) R (@pair A (prod B C) x (@pair B C y z))), @Acc3 A B C R x y z *)
case H0; intros.
(* Goal: @Acc3 A B C R y y0 y1 *)
apply H2.
(* Goal: R (@pair A (prod B C) y (@pair B C y0 y1)) (@pair A (prod B C) x2 (@pair B C x3 x4)) *)
exact H3.
Qed.

  Lemma Acc_Acc3 :
   forall (A B C : Set) (R : relation (A * (B * C))) (x : A) (y : B) (z : C),
   Acc R (x, (y, z)) -> Acc3 R x y z. 
Proof.
(* Goal: forall (A B C : Set) (R : relation (prod A (prod B C))) (x : A) (y : B) (z : C) (_ : @Acc (prod A (prod B C)) R (@pair A (prod B C) x (@pair B C y z))), @Acc3 A B C R x y z *)
intros.
change
  ((fun p : A * (B * C) =>
    match p with
    | (x2, (x3, x4)) => Acc3 R x2 x3 x4
    end) (x, (y, z))) in |- *.
(* Goal: (fun p : prod A (prod B C) => let (x2, p0) := p in let (x3, x4) := p0 in @Acc3 A B C R x2 x3 x4) (@pair A (prod B C) x (@pair B C y z)) *)
elim H.
(* Goal: forall (x : prod A (prod B C)) (_ : forall (y : prod A (prod B C)) (_ : R y x), @Acc (prod A (prod B C)) R y) (_ : forall (y : prod A (prod B C)) (_ : R y x), let (x2, p) := y in let (x3, x4) := p in @Acc3 A B C R x2 x3 x4), let (x2, p) := x in let (x3, x4) := p in @Acc3 A B C R x2 x3 x4 *)
simple destruct x0.
(* Goal: forall (A B C : Set) (R : relation (prod A (prod B C))) (x : A) (y : B) (z : C) (_ : @Acc (prod A (prod B C)) R (@pair A (prod B C) x (@pair B C y z))), @Acc3 A B C R x y z *)
simple destruct p; intros.
(* Goal: forall (A B C : Set) (R : relation (prod A (prod B C))) (x : A) (y : B) (z : C) (_ : @Acc (prod A (prod B C)) R (@pair A (prod B C) x (@pair B C y z))), @Acc3 A B C R x y z *)
apply Acc3_intro; intros.
(* Goal: @Acc3 A B C R y0 y1 y2 *)
apply (H1 (y0, (y1, y2))); auto.
Qed.


Section Principal.

  Variables (A : Set) (P : A -> Prop) (R : A -> A -> Prop).

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

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

End Principal.

