Require Export SetIsType.

Require Import Arith.
Require Import List.
Require Import ListSet.
Require Import Omega.






Lemma length_of_append:
  forall (A: Set) (xs ys: (list A)),
    (length (xs ++ ys)) = (length xs) + (length ys)
.



Lemma app_inject:
  forall (A: Set) (xs2 ys2 xs1 ys1: (list A)),
    (xs1 ++ xs2) = (ys1 ++ ys2) ->
    (length xs1) = (length ys1) ->
    (xs1 = ys1) /\ (xs2 = ys2)
.









Lemma app_length_right:
  forall (A: Set) (xs1 xs2 ys1 ys2: (list A)),
    (length xs2) = (length ys2) ->
    (length (xs1 ++ xs2)) = (length (ys1 ++ ys2)) ->
    (length xs1) = (length ys1)
.



Lemma map_elim:
  forall (A B: Set) (f: A -> B) (xs: (list A)) (y: B),
    (In y (map f xs)) ->
    exists x: A, (In x xs) /\ y = (f x)
.









Lemma map_intro:
  forall (A B: Set) (f: A -> B) (x: A) (xs: (list A)),
    (In x xs) ->
    (In (f x) (map f xs))
.







Lemma length_of_map:
  forall (A B: Set) (f: A -> B) (xs: (list A)),
    (length (map f xs)) = (length xs)
.




Lemma map_of_append:
  forall (A B: Set) (f: A -> B) (xs ys: (list A)),
    (map f (xs ++ ys)) = (map f xs) ++ (map f ys)
.





Lemma cons_destruct:
    forall (A: Set) (x y: A) (xs ys: (list A)),
      (x = y) -> (xs = ys) -> (x :: xs) = (y :: ys)
.



Lemma plus_minus_assoc:
  forall (n m p: nat),
    (p <= m) ->
    n + m - p = n + (m - p)
.








Lemma myarith_1:
  forall (n m: nat),
    (m <= n) ->
    (n - m + m) = n
.

Lemma myarith_2:
  forall (n m p: nat),
    ((m + p) <= n) ->
    (n - m - p) = (n - (m + p))
.







Lemma empty_is_empty_1:
  forall (A: Set) (eqdec: forall (x y: A), { x = y } + { x <> y }),
    forall (x: A),
      ~(set_In x (empty_set A))
.


Lemma empty_is_empty_2:
  forall (A: Set) (eqdec: forall (x y: A), { x = y } + { x <> y }),
    forall (s: (set A)),
      (forall (x: A), ~(set_In x s)) ->
      (s = (empty_set A))
.



Lemma empty_union_left:
  forall (A: Set) (eqdec: forall (x y: A), { x = y } + { x <> y }),
    forall (s1 s2: (set A)),
    (set_union eqdec s1 s2) = (empty_set A) ->
    s1 = (empty_set A)
.




Lemma empty_union_right:
  forall (A: Set) (eqdec: forall (x y: A), { x = y } + { x <> y }),
    forall (s1 s2: (set A)),
    (set_union eqdec s1 s2) = (empty_set A) ->
    s2 = (empty_set A)
.

Definition snoc (A: Set) (xs: (list A)) (x: A): (list A) :=
   (xs ++ (x :: nil))
.
Implicit Arguments snoc [A].

Lemma snoc_of_append:
  forall (A: Set) (xs ys: (list A)) (z: A),
    (snoc (xs ++ ys) z) = (xs ++ (snoc ys z))
.


Lemma snoc_of_cons:
  forall (A: Set) (x y: A) (xs: (list A)),
    (snoc (x :: xs) y) = (x :: (snoc xs y))
.


Lemma length_of_snoc:
  forall (A: Set) (x: A) (xs: list A),
    (length (snoc xs x)) = (S (length xs))
.



Section SnocInd.

Variable A: Set.
Variable P: (list A) -> Prop.
Variable H_nil: (P nil).
Variable H_snoc: forall (x: A) (xs: (list A)), (P xs) -> (P (snoc xs x)).

Lemma snoc_ind_aux_1:
  forall (xs: (list A)),
    (length xs) = 0 ->
    xs = nil
.





Lemma snoc_ind_aux_2:
  forall (xs: (list A)),
    (length xs) > 0 ->
    exists ys: (list A), exists y: A, xs = y :: ys
.




Lemma snoc_ind_aux_3:
  forall (xs: (list A)) (x: A),
    (snoc xs x) <> nil
.



Lemma snoc_ind_aux_4:
  forall (xs: (list A)) (x: A),
    exists ys: (list A), exists y: A, x :: xs = (snoc ys y)
.





Lemma snoc_ind_aux_5:
  forall (xs: (list A)),
    (length xs) > 0 ->
    exists ys: (list A), exists y: A, xs = (snoc ys y)
.



Lemma snoc_ind_aux_6:
  forall (n: nat) (xs: (list A)),
    (length xs) = n ->
    (P xs)
.







Lemma snoc_ind:
  forall (xs: (list A)),
    (P xs)
.


End SnocInd.

Lemma snoc_inject:
  forall (A: Set) (x y: A) (xs ys: (list A)),
    (snoc xs x) = (snoc ys y) ->
    (xs = ys) /\ (x = y)
.





Lemma snoc_then_append:
  forall (A: Set) (x: A) (ys xs: (list A)),
    (snoc xs x) ++ ys = xs ++ (x :: ys)
.




Lemma snoc_nil:
  forall (A: Set) (x: A),
    (snoc nil x) = (x :: nil)
.




Require ListSet.
Require Peano_dec.

Definition natSet: Set := (ListSet.set nat).
Definition natSet_empty: natSet := (ListSet.empty_set nat).
Definition natSet_union: natSet -> natSet -> natSet :=
  fun x y => (ListSet.set_union Peano_dec.eq_nat_dec x y)
.
Definition natSet_add: nat -> natSet -> natSet :=
  fun x y => (ListSet.set_add Peano_dec.eq_nat_dec x y)
.
Definition natSet_in: nat -> natSet -> Prop :=
  fun x y => (ListSet.set_In x y)
.



Section Forall2_section.

Variable A: Set.
Variable B: Set.

Inductive Forall2 (P: A -> B -> Prop): (list A) -> (list B) -> Prop :=
  
  | Forall2_nil:
    (Forall2 P nil nil)

  | Forall2_cons:
    forall (xA: A) (xB: B) (xsA: (list A)) (xsB: (list B)),
      (P xA xB) ->
      (Forall2 P xsA xsB) ->
      (Forall2 P (xA :: xsA) (xB:: xsB))
.

Lemma Forall2_implies_same_length:
  forall (P: A -> B -> Prop) (xsA: (list A)) (xsB: (list B)),
    (Forall2 P xsA xsB) ->
    (length xsA) = (length xsB)
.



Lemma Forall2_implies:
  forall (P1: A -> B -> Prop) (P2: A -> B -> Prop)
         (xsA: (list A)) (xsB: (list B)),
         (forall (xA: A) (xB: B), (P1 xA xB) -> (P2 xA xB)) ->
         (Forall2 P1 xsA xsB) ->
         (Forall2 P2 xsA xsB)
.



End Forall2_section.

Implicit Arguments Forall2 [A B].


Inductive List_from (A: Set): (list A) -> nat -> A -> Prop :=

  | List_from_tail:
    forall (xs: (list A)) (x: A),
      (List_from A (snoc xs x) 0 x)

  | List_from_head:
    forall (xs: (list A)) (x y: A) (n : nat),
      (List_from A xs n y) ->
      (List_from A (snoc xs x) (S n) y)
.

Implicit Arguments List_from [A].

Lemma List_from_domain:
  forall (A: Set) (xs: (list A)) (i: nat),
    i < (length xs) ->
    exists x: A,
      (List_from xs i x)
.








Lemma List_from_is_a_partial_function:
  forall (A: Set) (xs: (list A)) (i: nat) (x: A),
    (List_from xs i x) ->
    forall (x': A),
      (List_from xs i x') ->
      (x = x')
.






Lemma List_from_lem1:
  forall (A: Set) (xs1 xs2: (list A)) (x: A) (k: nat),
    (List_from (xs1 ++ xs2) ((length xs2) + k) x) ->
    (List_from xs1 k x)
.







Lemma List_from_lem1_cor1:
  forall (A: Set) (xs1 xs2: (list A)) (x: A) (i: nat),
    i >= (length xs2) ->
    (List_from (xs1 ++ xs2) i x) ->
    (List_from xs1 (i - (length xs2)) x)
.


Lemma List_from_lem2:
  forall (A: Set) (xs1 xs2: (list A)) (x: A) (k: nat),
    (List_from xs1 k x) ->
    (List_from (xs1 ++ xs2) ((length xs2) + k) x)
.





Lemma List_from_lem3:
  forall (A: Set) (xs1 xs2: (list A)) (x: A) (k: nat),
    (List_from xs2 k x) ->
    (List_from (xs1 ++ xs2) k x)
.



Lemma List_from_lem4:
  forall (A: Set) (xs1 xs2: (list A)) (x: A) (k: nat),
    (List_from (xs1 ++ xs2) k x) ->
    (k < (length xs2)) ->
    (List_from xs2 k x)
.












Lemma by_omega1: forall (x: nat), (x > 0) -> (S (pred x)) = x.

Lemma Declaration_of_variable_1:
  forall (A: Set) (xs1 xs2: (list A)) (x x': A) (i: nat),
    i > (length xs2) ->
    (List_from (xs1 ++ (x :: xs2)) i x') ->
    (List_from (xs1 ++ xs2) (pred i) x')
.



Lemma Declaration_of_variable_2:
  forall (A: Set) (xs1 xs2: (list A)) (x x': A) (i: nat),
    i < (length xs2) ->
    (List_from (xs1 ++ (x :: xs2)) i x') ->
    (List_from (xs1 ++ xs2) i x')
.


Lemma List_from_lem6:
  forall (A: Set) (xs1 xs2: (list A)) (x: A),
    (List_from (xs1 ++ (x :: xs2)) (length xs2) x)
.






Inductive List_at (A: Set): (list A) -> nat -> A -> Prop :=

  | List_at_head:
    forall (xs: (list A)) (x: A),
      (List_at A (x :: xs) 0 x)

  | List_at_tail:
    forall (xs: (list A)) (x y: A) (n : nat),
      (List_at A xs n y) ->
      (List_at A (x :: xs) (S n) y)
.

Implicit Arguments List_at [A].

Lemma Forall2_and_ListAt:
  forall (A B: Set) (P: A -> B -> Prop) (xs: (list A)) (ys: (list B)) (i: nat) (x: A),
    (Forall2 P xs ys) ->
    (List_at xs i x) ->
    exists y: B,
      (List_at ys i y) /\
      (P x y)
.








Lemma List_at_snoc_tail:
  forall (A: Set) (xs: (list A)) (x: A),
    (List_at (snoc xs x) (length xs) x)
.




Lemma List_at_right_weakening:
  forall (A: Set) (xs ys: (list A)) (i: nat) (x: A),
    (List_at xs i x) ->
    (List_at (xs ++ ys) i x)
.




Lemma ListFrom_implies_ListAt:
  forall (A: Set) (xs: (list A)) (i: nat) (x: A),
    (List_from xs i x) ->
    (List_at xs ((length xs) - (S i)) x)
.





Lemma ListAt_implies_ListFrom:
  forall (A: Set) (xs: (list A)) (i: nat) (x: A),
    (List_at xs i x) ->
    (List_from xs ((length xs) - (S i)) x)
.





Lemma List_from_inversion_on_length:
  forall (A: Set) (xs: (list A)) (i: nat) (x: A),
    (List_from xs i x) ->
    i < (length xs)
.







Lemma Forall2_and_ListFrom:
  forall (A B: Set) (P: A -> B -> Prop) (xs: (list A)) (ys: (list B)) (i: nat) (x: A),
    (Forall2 P xs ys) ->
    (List_from xs i x) ->
    exists y: B,
      (List_from ys i y) /\
      (P x y)
.








Lemma Forall2_snoc:
  forall (A B: Set) (P: A -> B -> Prop) (xAs: (list A)) (xBs: (list B)) (xA: A) (xB: B),
    (Forall2 P xAs xBs) ->
    (P xA xB) ->
    (Forall2 P (snoc xAs xA) (snoc xBs xB))
.






Lemma Forall2_refl:
  forall (A: Set) (P: A -> A -> Prop),
    (forall (x: A), (P x x)) ->
    forall (xs: (list A)),
      (Forall2 P xs xs)
.


Lemma Forall2_trans:
  forall (A B C: Set) (P1: A -> B -> Prop) (P2: B -> C -> Prop) (P3: A -> C -> Prop)
         (xs: (list A)) (ys: (list B)) (zs: (list C)),
    (forall (x: A) (y: B) (z: C),
      (P1 x y) -> (P2 y z) -> (P3 x z)) ->
    (Forall2 P1 xs ys) ->
    (Forall2 P2 ys zs) ->
    (Forall2 P3 xs zs)
.






Definition symRel (A B: Set) (R: A -> B -> Prop) (y: B) (x: A) := (R x y).
Implicit Arguments symRel [A B].


Section Rplus_Section.

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

Inductive Rplus: A -> A -> Prop :=
  | tc_step: forall (x y: A), (R x y) -> (Rplus x y)
  | tc_trans: forall (x y z: A), (Rplus x y) -> (Rplus y z) -> (Rplus x z)
.

Inductive Rplus1: A -> A -> Prop :=
  | tc_step1: forall (x y: A), (R x y) -> (Rplus1 x y)
  | tc_trans1: forall (x y z: A), (R x y) -> (Rplus1 y z) -> (Rplus1 x z)
.

Lemma Rplus1_is_transitive:
  forall (x y z: A), (Rplus1 x y) -> (Rplus1 y z) -> (Rplus1 x z)
.




Lemma Rplus_is_transitive:
  forall (x y z: A), (R x y) -> (Rplus y z) -> (Rplus x z)
.


Lemma Rplus_implies_Rplus1:
  forall (x y: A),
    (Rplus x y) ->
    (Rplus1 x y)
.


Lemma Rplus1_implies_Rplus:
  forall (x y: A),
    (Rplus1 x y) ->
    (Rplus x y)
.


End Rplus_Section.
Implicit Arguments Rplus [A].
Implicit Arguments Rplus1 [A].

Definition subrel (A B: Set) (R1 R2: A -> B -> Prop): Prop :=
  forall (x: A) (y: B),
    (R1 x y) ->
    (R2 x y)
.
Implicit Arguments subrel [A B].

Lemma Accessibility_is_preserved_by_inclusion:
  forall (A: Set) (R1 R2: A -> A -> Prop),
    (subrel R2 R1) ->
    forall (x: A),
      (Acc R1 x) ->
      (Acc R2 x)
.



Lemma Rplus_of_symRel:
  forall (A: Set) (R: A -> A -> Prop),
  (subrel (Rplus (symRel R)) (symRel (Rplus R)))
.




Lemma symRel_of_Rplus:
  forall (A: Set) (R: A -> A -> Prop),
  (subrel (symRel (Rplus R)) (Rplus (symRel R)))
.




Lemma Rplus1_of_symRel:
  forall (A: Set) (R: A -> A -> Prop),
  (subrel (Rplus1 (symRel R)) (symRel (Rplus1 R)))
.






Lemma transitive_closure_well_founded:
  forall (A: Set) (R: A -> A -> Prop) (x: A),
    (Acc (symRel R) x) ->
    (Acc (symRel (Rplus R)) x)
.








Section Exists_Section.

Variable A: Set.
Variable B: Set.
Variable P: A -> B -> Prop.

Hypothesis existence: forall (x: A), { y: B | (P x y) }.

Definition get_witness (x: A): B := let (y, _) := (existence x) in y.

Lemma correct_witness: forall (x: A), (P x (get_witness x)).

End Exists_Section.
Implicit Arguments get_witness [A B].


Inductive List_forall (A: Set) (P: A -> Prop): (list A) -> Prop :=
  | List_forall_nil:
    (List_forall A P nil)
  | List_forall_cons:
    forall (x: A) (xs: (list A)),
      (P x) -> (List_forall A P xs) ->
      (List_forall A P (x :: xs))
.
Implicit Arguments List_forall [A].

Lemma List_forall_and_List_at:
  forall (A: Set) (P: A -> Prop) (xs: (list A)) (i: nat) (x: A),
    (List_forall P xs) ->
    (List_at xs i x) ->
    (P x)
.





Lemma List_forall_and_List_from:
  forall (A: Set) (P: A -> Prop) (xs: (list A)) (i: nat) (x: A),
    (List_forall P xs) ->
    (List_from xs i x) ->
    (P x)
.



Lemma List_forall_implies_forall:
  forall (A: Set) (P1 P2: A -> Prop) (xs: (list A)),
    (forall (x: A), (P1 x) -> (P2 x)) ->
    (List_forall P1 xs) ->
    (List_forall P2 xs)
.


Lemma List_forall_equal_maps:
  forall (A B: Set) (f g: A -> B) (xs: (list A)),
    (List_forall (fun x => (f x) = (g x)) xs) ->
    (map f xs) = (map g xs)
.




Lemma map_id_is_id:
  forall (A: Set) (xs: (list A)),
    (map (fun x => x) xs) = xs
.


Lemma List_forall_equal_maps_cor1:
  forall (A: Set) (f: A -> A) (xs: (list A)),
    (List_forall (fun x => (f x) = x) xs) ->
    (map f xs) = xs
.




Lemma List_forall_of_map:
  forall (A B: Set) (P: B -> Prop) (f: A -> B) (xs: (list A)),
    (List_forall (fun x => (P (f x))) xs) ->
    (List_forall P (map f xs))
.





Lemma List_forall_of_append_intro:
  forall (A: Set) (P: A -> Prop) (xs ys: (list A)),
    (List_forall P xs) ->
    (List_forall P ys) ->
    (List_forall P (xs ++ ys))
.




Lemma List_forall_of_append_elim:
  forall (A: Set) (P: A -> Prop) (xs ys: (list A)),
    (List_forall P (xs ++ ys)) ->
    (List_forall P xs) /\
    (List_forall P ys)
.





Lemma List_forall_of_append_cor1:
  forall (A: Set) (P: A -> Prop) (xs ys: (list A)) (x: A),
    (List_forall P (xs ++ x :: ys)) ->
    (List_forall P (xs ++ ys))
.


Lemma List_forall_implies_Forall2_right:
  forall (A B: Set) (P: B -> Prop) (xs: (list A)) (ys: (list B)),
    (List_forall P ys) ->
    (length xs) = (length ys) ->
    (Forall2 (fun x y => (P y)) xs ys)
.





Lemma List_forall_implies_map_id:
  forall (A: Set) (xs: (list A)) (f: A -> A),
    (List_forall (fun x => (f x) = x) xs) ->
    (map f xs) = xs
.




Lemma List_at_of_map:
  forall (A B: Set) (f: A -> B) (xs: (list A)) (i: nat) (x: A),
    (List_at xs i x) ->
    (List_at (map f xs) i (f x))
.




Lemma List_from_of_map:
  forall (A B: Set) (f: A -> B) (xs: (list A)) (i: nat) (x: A),
    (List_from xs i x) ->
    (List_from (map f xs) i (f x))
.





Lemma Forall2_of_map:
  forall (A1 B1 A2 B2: Set) (P1: A1 -> B1 -> Prop) (P2: A2 -> B2 -> Prop)
         (fA: A1 -> A2) (fB: B1 -> B2) (xs: (list A1)) (ys: (list B1)),
    (forall (x: A1) (y: B1), (P1 x y) -> (P2 (fA x) (fB y))) ->
    (Forall2 P1 xs ys) ->
    (Forall2 P2 (map fA xs) (map fB ys))
.




Lemma Forall2_of_map_cor1:
  forall (A : Set) (P : A -> A -> Prop) (f g: A -> A) (xs ys : list A),
    (Forall2 (fun x y => (P (f x) (g y))) xs ys) ->
    (Forall2 P (map f xs) (map g ys))
.

Lemma Forall2_of_map_cor2:
  forall (A : Set) (P : A -> A -> Prop) (f g: A -> A) (xs ys : list A),
    (Forall2 P (map f xs) (map g ys)) ->
    (Forall2 (fun x y => (P (f x) (g y))) xs ys)
.







Lemma Forall2_conj:
  forall (A B: Set) (P1: A -> B -> Prop) (P2: A -> B -> Prop)
         (xs: (list A)) (ys: (list B)),
    (Forall2 P1 xs ys) ->
    (Forall2 P2 xs ys) ->
    (Forall2 (fun x y => (P1 x y) /\ (P2 x y)) xs ys)
.




Lemma List_forall_implies_Forall2:
  forall (A B: Set) (P1: A -> Prop) (P2: B -> Prop)
         (xs: (list A)) (ys: (list B)),
    (List_forall P1 xs) ->
    (length xs) = (length ys) ->
    (List_forall P2 ys) ->
    (Forall2 (fun x y => (P1 x) /\ (P2 y)) xs ys)
.