Require Import List.

Lemma well_foundation1:
  forall (A: Set) (R: A -> A -> Prop) (x: A),
    (Acc R x) ->
    forall (y: A),
      (R x y) ->
      (R y x) -> False.

Lemma well_foundation2:
  forall (A: Set) (R: A -> A -> Prop),
    (well_founded R) ->
    forall (x y: A),
      (R x y) ->
      (R y x) -> False.

Definition fun_extension (A B: Set) (f: A -> B) (R: B -> B -> Prop) (x y: A): Prop :=
  (R (f x) (f y))
.

Lemma well_foundation3:
  forall (A B: Set) (f: A -> B) (R: B -> B -> Prop),
    forall (x: B),
      (Acc R x) ->
      forall (x': A),
        (x = (f x')) ->
        (Acc (fun_extension A B f R) x')
.

Lemma well_foundation4:
  forall (A B: Set) (f: A -> B) (R: B -> B -> Prop),
    (well_founded R) ->
    (well_founded (fun_extension A B f R))
.



Section List_forall_section.

Variable A: Set.

Inductive List_forall (P: A -> Prop): (list A) -> Prop :=

  | List_forall_nil:
    (List_forall P nil)

  | List_forall_cons:
    forall (x: A) (xs: (list A)),
      (P x) ->
      (List_forall P xs) ->
      (List_forall P (x :: xs))
.

Lemma forall_implies_forall:
  forall (P: A -> Prop),
    (forall (x: A), (P x)) ->
    forall (xs: (list A)),
      (List_forall P xs)
.



Lemma List_forall3:
  forall (P: A -> Prop) (x y z: A),
    (P x) -> (P y) -> (P z) ->
    (List_forall P (x :: y :: z :: nil))
.




End List_forall_section.

Implicit Arguments List_forall [A].


Section SequenceExtension.

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

Inductive RList: (list A) -> (list A) -> Prop :=

  | RList_head:
    forall (x y: A) (xs: (list A)),
      (R x y) ->
      (RList (x :: xs) (y :: xs))

  | RList_tail:
    forall (x: A) (xs ys: (list A)),
      (RList xs ys) ->
      (RList (x :: xs) (x :: ys))
.

Lemma sequence_extension_preserves_accessibility_aux:
  forall (x: A) (xs: (list A)),
    (Acc R x) ->
    (Acc (RList) xs) ->
    (Acc (RList) (x :: xs))
.







Lemma sequence_extension_preserves_accessibility:
  forall (xs: (list A)),
    (List_forall (Acc R) xs) ->
    (Acc (RList) xs)
.



Lemma sequence_extension_preserves_well_foundedness:
  (well_founded R) ->
  (well_founded RList)
.



Lemma RTriple1:
  forall (x x' y z: A),
    (R x x') ->
    (RList (x :: y :: z :: nil) (x' :: y :: z :: nil))
.


Lemma RTriple2:
  forall (x y y' z: A),
    (R y y') ->
    (RList (x :: y :: z :: nil) (x :: y' :: z :: nil))
.


Lemma RTriple3:
  forall (x y z z': A),
    (R z z') ->
    (RList (x :: y :: z :: nil) (x :: y :: z' :: nil))
.


End SequenceExtension.


Section LexicographicExtension.

Variable A1: Set.
Variable R1: A1 -> A1 -> Prop.
Variable A2: Set.
Variable R2: A2 -> A2 -> Prop.

Inductive RPair: (A1 * A2) -> (A1 * A2) -> Prop :=

  | RPair_fst:
    forall (x1 y1: A1) (x2 y2: A2),
      (R1 x1 y1) ->
      (RPair (x1, x2) (y1, y2))

  | RPair_snd:
    forall (x1: A1) (x2 y2: A2),
      (R2 x2 y2) ->
      (RPair (x1, x2) (x1, y2))
.

Lemma lexicographic_extension_preserves_well_foundedness:
  (well_founded R1) ->
  (well_founded R2) ->
  (well_founded RPair)
.









End LexicographicExtension.