OrderedListEq.v

(* A generic module to define concatenation on ordered list *)
Require Import Arith.
Require Export PolyList.
Require Import Lexicographic_Exponentiation.
Require Export Relation_Definitions.
Require Export Relation_Operators.
Require Export Option.
Section OrderedList.
Variable A:Set.
Variable ltA:A -> A ->Prop.
Variable eqA:A -> A ->Prop.
Hypothesis eqARefl:(reflexive A eqA).
Hypothesis eqASym:(symmetric A eqA).
Hypothesis eqATrans:(transitive A eqA).
Hypothesis ltADec:(a, b:A){(ltA a b)}+{(ltA b a)}+{(eqA a b)}.
Hypothesis ltATrans:(transitive A ltA).
Hypothesis ltAAnti:(a:A)~ (ltA a a).
Hypothesis ltAImpNotEqA:(a, b:A) (ltA a b) ->~ (eqA a b).
Hypothesis ltAntiSym:(a, b:A) (ltA a b) ->~ (ltA b a).
Variable f:A ->A.
Hypothesis feqA:(a:A)(eqA (f a) a).
Hypothesis ltAeqAComp:
           (a, b, c, d:A) (ltA a b) -> (eqA a c) -> (eqA b d) ->(ltA c d).

Definition eqADec: (a, b:A){(eqA a b)}+{~ (eqA a b)}.
Intros a b; Case (ltADec a b); Intros Test; Auto.
Case Test; Clear Test; Intros Test; Auto.
Right.
Red; Intros H'; Absurd (eqA b a); Auto.
Qed.
Hypothesis eqADec':(a, b:A){(eqA a b)}+{~ (eqA a b)}.

Mutual Inductive Olist: (list A) ->Prop :=
     OlistNil: (Olist (nil ?))
    | OlistOne: (a:A)(Olist (cons a (nil ?)))
    | OlistCons:
        (a, b:A) (L:(list A)) (Olist (cons b L)) -> (ltA a b) ->
        (Olist (cons a (cons b L))) .
Hints Resolve OlistNil OlistOne OlistCons.

Theorem OlistInv: (a:A) (L:(list A)) (Olist (cons a L)) ->(Olist L).
Intros a L H'; Inversion H'; Auto.
Qed.

Theorem OlistSkip:
  (a, b:A) (L:(list A)) (Olist (cons a (cons b L))) ->(Olist (cons a L)).
Intros a b L; Case L.
Intros H'.
Apply OlistOne; Auto.
Intros a0 l; Case l.
Intros H'.
Apply OlistCons; Auto.
Apply ltATrans with y := b; Auto.
Inversion H'; Auto.
Inversion H'; Auto.
Inversion H1; Auto.
Intros a1 l0 H'; Inversion H'; Inversion H1.
Apply OlistCons; Auto.
Apply ltATrans with y := b; Auto.
Qed.

Theorem OlistSup:
  (a:A) (L:(list A)) (Olist (cons a L)) ->(b:A) (In b L) ->(ltA a b).
Intros a L; Elim L; Simpl; Auto.
Intros H' b H'0; Elim H'0.
Intros a0 l H' H'0 b H'1; Elim H'1;
[Intros H'2; Rewrite <- H'2; Clear H'1 | Intros H'2; Clear H'1]; Auto.
Inversion H'0; Auto.
Apply H'; Auto.
Apply OlistSkip with b := a0; Auto.
Qed.

Theorem OlistUnique:
  (L:(list A)) (a, b:A) (Olist (cons a L)) -> (eqA a b) ->~ (In b L).
Intros L a b H' H'0; Red; Intros H'1; Absurd (eqA a b); Auto.
Apply ltAImpNotEqA; Auto.
Apply OlistSup with L := L; Auto.
Qed.

Theorem OlistIn:
  (L:(list A)) (a, b:A) (In a L) -> (In b L) -> (Olist L) -> (eqA a b) ->a=b.
Intros L; Elim L; Simpl; Auto.
Intros a b H'; Elim H'; Auto.
Intros a l H' a0 b H'0; Elim H'0; Clear H'0; Intros H'0;
[Rewrite <- H'0 | Idtac].
Intros H'1; Case H'1; Clear H'1; Intros H'1; Auto.
Intros H'2 H'3; Absurd (eqA a b); Auto.
Apply ltAImpNotEqA; Auto.
Apply OlistSup with L := l; Auto.
Intros H'1; Elim H'1; Clear H'1; Intros H'1; [Rewrite <- H'1 | Idtac];
Intros H'2 H'3.
Absurd (eqA a a0); Auto.
Apply ltAImpNotEqA; Auto.
Apply OlistSup with L := l; Auto.
Apply H'; Auto.
Apply OlistInv with a := a; Auto.
Qed.

Mutual Inductive InEq: A -> (list A) ->Prop :=
     InEqHead: (a, b:A) (L:(list A)) (eqA a b) ->(InEq a (cons b L))
    | InEqSkip: (a, b:A) (L:(list A)) (InEq a L) ->(InEq a (cons b L)) .
Hints Resolve InEqHead InEqSkip.

Definition InEqDec: (a:A) (L1:(list A)){(InEq a L1)}+{~ (InEq a L1)}.
Intros a L1; Elim L1; Auto.
Right; Red; Intros H'; Inversion H'; Auto.
Intros a0 l H'; Case (eqADec' a a0); Intros Eqaa0; Auto.
Case H'; Intros REc; Auto.
Right; Red; Intros H'0; Inversion H'0; Auto.
Defined.

Theorem inImpInEq: (a:A) (L:(list A)) (In a L) ->(InEq a L).
Intros a L; Elim L; Simpl; Auto.
Intros H'; Elim H'.
Intros a0 l H' H'0; Elim H'0;
[Intros H'1; Rewrite <- H'1; Clear H'0 | Intros H'1; Clear H'0]; Auto.
Qed.

Theorem OlistSupEq:
  (a:A) (L:(list A)) (Olist (cons a L)) ->(b:A) (InEq b L) ->(ltA a b).
Intros a L; Elim L; Simpl; Auto.
Intros H' b H'0; Inversion H'0.
Intros a0 l H' H'0 b H'1; Inversion_clear H'1.
Apply ltAeqAComp with a := a b := a0; Auto.
Apply OlistSup with L := (cons a0 l); Simpl; Auto.
Apply H'; Auto.
Apply OlistSkip with b := a0; Auto.
Qed.

Theorem OlistUniqueEq:
  (L:(list A)) (a, b:A) (Olist (cons a L)) -> (eqA a b) ->~ (InEq b L).
Intros L a b H' H'0; Red; Intros H'1; Absurd (eqA a b); Auto.
Apply ltAImpNotEqA; Auto.
Apply OlistSupEq with L := L; Auto.
Qed.

Theorem InEqComp: (a, b:A) (L:(list A)) (InEq a L) -> (eqA a b) ->(InEq b L).
Intros a b L H'; Generalize b; Clear b; Elim H'; Auto.
Intros a0 b L0 H'0 b0 H'1.
Apply InEqHead; Auto.
Apply eqATrans with y := a0; Auto.
Qed.

Theorem NotInEqComp:
  (a, b:A) (L:(list A)) ~ (InEq a L) -> (eqA a b) ->~ (InEq b L).
Intros a b L H' H'0; Red; Intros H'1; Case H'; Auto.
Apply InEqComp with a := b; Auto.
Qed.

Mutual Inductive InclEq: (list A) -> (list A) ->Prop :=
     InclEqDef:
       (L1, L2:(list A)) ((a:A) (InEq a L1) ->(InEq a L2)) ->(InclEq L1 L2) .
Hints Resolve InclEqDef.

Theorem inclImpImplEq: (L1, L2:(list A)) (incl L1 L2) ->(InclEq L1 L2).
Intros L1 L2 H'; Apply InclEqDef.
Intros a H'0; Generalize H'; Elim H'0; Auto.
Intros a0 b L H'1 H'2.
Apply InEqComp with a := b; Auto.
Apply inImpInEq; Auto with datatypes.
Intros a0 b L H'1 H'2 H'3.
Apply H'2; Auto.
Apply incl_tran with A := A m := (cons b L); Auto with datatypes.
Qed.

Theorem InclEqNil: (L:(list A))(InclEq (nil ?) L).
Intros L.
Apply InclEqDef; Auto.
Intros a H'; Inversion H'.
Qed.
Hints Resolve InclEqNil.

Theorem InclEqRef: (L:(list A))(InclEq L L).
Intros L.
Apply InclEqDef; Auto.
Qed.
Hints Resolve InclEqRef.

Theorem InclEqTrans: (transitive (list A) InclEq).
Red.
Intros x y z H' H'0; Inversion_clear H'; Inversion_clear H'0; Auto.
Qed.

Theorem InclEqCons:
  (a:A) (L1, L2:(list A)) (InEq a L2) -> (InclEq L1 L2) ->
  (InclEq (cons a L1) L2).
Intros a L1 L2 H' H'0; Inversion H'0; Auto.
Apply InclEqDef; Auto.
Intros a0 H'1; Inversion H'1; Auto.
Apply InEqComp with a := a; Auto.
Qed.
Hints Resolve InclEqCons.

Mutual Inductive EqL: (list A) -> (list A) ->Prop :=
     EqLNil: (EqL (nil ?) (nil ?))
    | EqLCons:
        (a, b:A) (L1, L2:(list A)) (eqA a b) -> (EqL L1 L2) ->
        (EqL (cons a L1) (cons b L2)) .
Hints Resolve EqLNil EqLCons.

Theorem EqLInv:
  (L1, L2:(list A)) (a:A) (EqL L1 L2) -> (InEq a L1) ->(InEq a L2).
Intros L1 L2 a H'; Elim H'; Auto.
Intros a0 b L3 L4 H'0 H'1 H'2 H'3; Inversion H'3; Auto.
Apply InEqHead; Auto.
Apply eqATrans with y := a0; Auto.
Qed.

Theorem EqLRef: (L:(list A))(EqL L L).
Intros L; Elim L; Auto.
Qed.
Hints Resolve EqLRef.

Theorem EqLTrans: (L:(list A))(transitive (list A) EqL).
Intros L; Red.
Intros x y z H'; Generalize z; Elim H'; Clear H' z; Auto.
Intros a b L1 L2 H' H'0 H'1 z H'2; Inversion H'2; Auto.
Apply EqLCons; Auto.
Apply eqATrans with y := b; Auto.
Qed.

Theorem InclEqOlist:
  (L1, L2:(list A))
  (a, b:A)
  (Olist (cons a L1)) ->
  (Olist (cons b L2)) -> (InclEq (cons a L1) (cons b L2)) ->(InclEq L1 L2).
Intros L1 L2 a b H' H'0 H'1.
Apply InclEqDef; Auto.
Intros a0 H'2.
Inversion H'1.
LApply (H a0); [Intros H'4; Inversion H'4 | Try Assumption]; Auto.
Cut (ltA a a0); Auto.
2:Apply OlistSupEq with L := L1; Auto.
Intros H'3.
LApply (H a); [Intros H'6; Inversion H'6 | Idtac]; Auto.
Absurd (eqA a b); Auto.
Apply ltAImpNotEqA; Auto.
Apply ltAeqAComp with a := a b := a0; Auto.
Absurd (ltA b a); Auto.
Apply ltAntiSym; Auto.
Apply ltAeqAComp with a := a b := a0; Auto.
Apply OlistSupEq with L := L2; Auto.
Qed.

Theorem EqLOlist:
  (L1, L2:(list A))
  (Olist L1) -> (Olist L2) -> (InclEq L1 L2) -> (InclEq L2 L1) ->(EqL L1 L2).
Intros L1; Elim L1; Auto.
Intros L2; Case L2; Auto.
Intros a l H' H'0 H'1 H'2; Inversion H'2.
LApply (H a); [Intros H'4; Inversion H'4 | Idtac]; Auto.
Intros a l H' L2; Case L2; Auto.
Intros H'0 H'1 H'2; Inversion H'2.
LApply (H a); [Intros H'4; Inversion H'4 | Idtac]; Auto.
Intros a0 l0 H'0 H'1 H'2 H'3; Auto.
Apply EqLCons; Auto.
2:Apply H'; Auto.
2:Apply OlistInv with a := a; Auto.
2:Apply OlistInv with a := a0; Auto.
2:Apply InclEqOlist with a := a b := a0; Auto.
2:Apply InclEqOlist with a := a0 b := a; Auto.
Inversion H'3.
LApply (H a0); [Intros H'5; Inversion H'5 | Idtac]; Auto.
Inversion H'2; Auto.
LApply (H6 a); [Intros H'6; Inversion H'6 | Idtac]; Auto.
Absurd (ltA a0 a); Auto.
Apply ltAntiSym; Auto.
Apply OlistSupEq with L := l; Auto.
Apply OlistSupEq with L := l0; Auto.
Qed.

Fixpoint diffElem[L1:(list A)]: (list A) ->(Option A) :=
   [L2:(list A)]
      Cases L1 of
          nil => (None ?)
         | (cons a L'1) => Cases (InEqDec a L2) of
                               (left _) => (diffElem L'1 L2)
                              | (right _) => (Some ? a)
                           end
      end.

Theorem diffElemNone:
  (L1, L2:(list A)) (diffElem L1 L2)=(None ?) ->(InclEq L1 L2).
Intros L1; Elim L1; Simpl; Auto.
Intros a l H' L2.
Case (InEqDec a L2); Auto.
Intros H'0 H'1; Discriminate.
Qed.

Theorem diffElemSomeIn:
  (L1, L2:(list A)) (a:A) (diffElem L1 L2)=(Some ? a) ->(InEq a L1).
Intros L1; Elim L1; Simpl; Auto.
Intros H' a H'0; Discriminate.
Intros a l H' L2 a0.
Case (InEqDec a L2); Intros InEq0 Eq0; Auto.
Apply InEqSkip; Auto.
Apply H' with L2 := L2; Auto.
Inversion Eq0; Auto.
Qed.

Theorem diffElemSomeNIn:
  (L1, L2:(list A)) (a:A) (diffElem L1 L2)=(Some ? a) ->~ (InEq a L2).
Intros L1; Elim L1; Simpl; Auto.
Intros H' a H'0; Discriminate.
Intros a l H' L2 a0.
Case (InEqDec a L2); Intros InEq0 Eq0; Auto.
Inversion Eq0; Auto.
Rewrite <- H0; Auto.
Qed.

Definition olistDiff:
  (L1, L2:(list A)) (Olist L1) -> (Olist L2) -> ~ (EqL L1 L2) ->
  {a:A | (InEq a L1) /\ ~ (InEq a L2) \/ ~ (InEq a L1) /\ (InEq a L2)}.
Intros L1 L2 H' H'0 H'1.
Generalize (refl_equal ? (diffElem L1 L2)); Pattern -1 (diffElem L1 L2);
Case (diffElem L1 L2); Auto.
Intros x H'2; Exists x; Left; Split; Auto.
Apply diffElemSomeIn with 1 := H'2; Auto.
Apply diffElemSomeNIn with 1 := H'2; Auto.
Intros Eq1.
Generalize (refl_equal ? (diffElem L2 L1)); Pattern -1 (diffElem L2 L1);
Case (diffElem L2 L1); Auto.
Intros x H'2; Exists x; Right; Split; Auto.
Apply diffElemSomeNIn with 1 := H'2; Auto.
Apply diffElemSomeIn with 1 := H'2; Auto.
Intros Eq2; Absurd (EqL L1 L2); Auto.
Apply EqLOlist; Auto.
Apply diffElemNone; Auto.
Apply diffElemNone; Auto.
Defined.

Mutual Inductive Disjoint: (list A) -> (list A) ->Prop :=
     DisjointDef:
       (L1, L2:(list A)) ((a:A) (InEq a L1) ->~ (InEq a L2)) ->(Disjoint L1 L2) .

Theorem DisjointCom: (L1, L2:(list A)) (Disjoint L1 L2) ->(Disjoint L2 L1).
Intros L1 L2 H'; Elim H'; Auto.
Intros L3 L4 H'0.
Apply DisjointDef.
Intros a H'1; Red; Intros H'2; Absurd (InEq a L4); Auto.
Qed.

Theorem DisjointInv1:
  (a:A) (L1, L2:(list A)) (Disjoint L1 (cons a L2)) ->(Disjoint L1 L2).
Intros a L1 L2 H'; Inversion H'; Apply DisjointDef.
Intros a0 H'0; Red; Intros H'1.
LApply (H a0); [Intros H'3; Apply H'3 | Idtac]; Auto.
Qed.

Theorem DisjointInv2:
  (a:A) (L1, L2:(list A)) (Disjoint (cons a L1) L2) ->(Disjoint L1 L2).
Intros a L1 L2 H'.
Apply DisjointCom.
Apply DisjointInv1 with a := a; Auto.
Apply DisjointCom; Auto.
Qed.

Theorem DisjointCons1:
  (b:A) (L1, L2:(list A)) (Disjoint L1 L2) -> ~ (InEq b L1) ->
  (Disjoint L1 (cons b L2)).
Intros a L1 L2 H' H'0; Inversion_clear H'.
Apply DisjointDef; Simpl; Auto.
Intros b H'1; Red; Intros H'2; Inversion_clear H'2; Auto.
Case H'0; Apply InEqComp with a := b; Auto.
Absurd (InEq b L2); Auto.
Qed.

Theorem DisjointCons2:
  (a:A) (L1, L2:(list A)) (Disjoint L1 L2) -> ~ (InEq a L2) ->
  (Disjoint (cons a L1) L2).
Intros a L1 L2 H' H'0; Apply DisjointCom; Auto.
Apply DisjointCons1; Auto.
Apply DisjointCom; Auto.
Qed.

Theorem DisjointInclL:
  (L1, L2, L3:(list A)) (Disjoint L1 L2) -> (InclEq L3 L1) ->(Disjoint L3 L2).
Intros L1 L2 L3 H' H'0.
Apply DisjointDef; Auto.
Intros a H'1; Inversion H'.
Apply H; Auto.
Inversion H'0; Auto.
Qed.

Theorem DisjointInclR:
  (L1, L2, L3:(list A)) (Disjoint L1 L2) -> (InclEq L3 L2) ->(Disjoint L1 L3).
Intros L1 L2 L3 H' H'0.
Apply DisjointCom.
Apply DisjointInclL with L1 := L2; Auto.
Apply DisjointCom; Auto.
Qed.

Theorem DisjointIncl:
  (L1, L2, L3, L4:(list A))
  (Disjoint L1 L2) -> (InclEq L3 L1) -> (InclEq L4 L2) ->(Disjoint L3 L4).
Intros L1 L2 L3 L4 H' H'0 H'1.
Apply DisjointInclR with L2 := L2; Auto.
Apply DisjointInclL with L1 := L1; Auto.
Qed.

Mutual Inductive append: (list A) -> (list A) -> (list A) ->Prop :=
     appendNil1: (L1:(list A))(append L1 (nil ?) L1)
    | appendNil2: (L2:(list A))(append (nil ?) L2 L2)
    | appendEqA:
        (a, b:A) (L1, L2, L3:(list A)) (eqA a b) -> (append L1 L2 L3) ->
        (append (cons a L1) (cons b L2) (cons a L3))
    | appendLtA1:
        (a, b:A)
        (L1, L2, L3:(list A)) (ltA a b) -> (append L1 (cons b L2) L3) ->
        (append (cons a L1) (cons b L2) (cons a L3))
    | appendLtA2:
        (a, b:A)
        (L1, L2, L3:(list A)) (ltA b a) -> (append (cons a L1) L2 L3) ->
        (append (cons a L1) (cons b L2) (cons b L3)) .
Hints Resolve appendNil1 appendNil2 appendEqA appendLtA1 appendLtA2.

Theorem appendCom:
  (L1, L2, L3:(list A)) (append L1 L2 L3) -> (Disjoint L1 L2) ->
  (append L2 L1 L3).
Intros L1 L2 L3 H'; Elim H'; Auto.
Intros a b L4 L5 L6 H'0 H'1 H'2 H'3; Inversion_clear H'3.
Absurd (InEq a (cons b L5)); Auto.
Intros a b L4 L5 L6 H'0 H'1 H'2 H'3.
Apply appendLtA2; Auto.
Apply H'2; Auto.
Apply DisjointInv2 with a := a; Auto.
Intros a b L4 L5 L6 H'0 H'1 H'2 H'3; Apply appendLtA1; Auto.
Apply H'2; Auto.
Apply DisjointInv1 with a := b; Auto.
Qed.

Theorem appendIncl1: (L1, L2, L3:(list A)) (append L1 L2 L3) ->(InclEq L1 L3).
Intros L1 L2 L3 H'; Elim H'; Auto with datatypes.
Intros a b L4 L5 L6 H'0 H'1 H'2.
Apply InclEqDef; Auto.
Intros a0 H'3; Inversion_clear H'3; Auto.
Inversion_clear H'2; Auto.
Intros a b L4 L5 L6 H'0 H'1 H'2; Apply InclEqDef; Auto.
Intros a0 H'3; Inversion_clear H'2; Inversion_clear H'3; Auto.
Intros a b L4 L5 L6 H'0 H'1 H'2; Apply InclEqDef; Auto.
Intros a0 H'3; Inversion_clear H'2; Inversion_clear H'3; Auto.
Qed.

Theorem appendDisjIncl1:
  (L1, L2, L3:(list A)) (append L1 L2 L3) -> (Disjoint L1 L2) ->(incl L1 L3).
Intros L1 L2 L3 H'; Elim H'; Auto with datatypes.
Intros L4 H'0; Red; Intros a H'1; Inversion H'1.
Intros a b L4 L5 L6 H'0 H'1 H'2 H'3; Inversion_clear H'3.
LApply (H a); [Intros H'4; Case H'4 | Idtac]; Auto.
Intros a b L4 L5 L6 H'0 H'1 H'2 H'3; Apply incl_cons with A := A;
Auto with datatypes; Apply incl_tran with m := L6; Auto with datatypes.
Apply H'2; Apply DisjointInv2 with a := a; Auto.
Intros a b L4 L5 L6 H'0 H'1 H'2 H'3; Apply incl_tran with m := L6; Simpl;
Auto with datatypes.
Apply H'2; Apply DisjointInv1 with a := b; Auto.
Qed.

Theorem appendIncl2: (L1, L2, L3:(list A)) (append L1 L2 L3) ->(InclEq L2 L3).
Intros L1 L2 L3 H'; Elim H'; Auto with datatypes.
Intros a b L4 L5 L6 H'0 H'1 H'2; Apply InclEqDef.
Intros a0 H'3; Inversion_clear H'2; Inversion_clear H'3; Auto.
Apply InEqComp with a := b; Auto.
Intros a b L4 L5 L6 H'0 H'1 H'2; Apply InclEqDef; Auto.
Intros a0 H'3; Inversion_clear H'2; Inversion_clear H'3; Auto.
Intros a b L4 L5 L6 H'0 H'1 H'2; Apply InclEqDef; Auto.
Intros a0 H'3; Inversion_clear H'2; Inversion_clear H'3; Auto.
Qed.

Theorem appendDisjIncl2:
  (L1, L2, L3:(list A)) (append L1 L2 L3) -> (Disjoint L1 L2) ->(incl L2 L3).
Intros L1 L2 L3 H'; Elim H'; Auto with datatypes.
Intros L4 H'0; Red; Intros a H'1; Inversion H'1.
Intros a b L4 L5 L6 H'0 H'1 H'2 H'3; Inversion_clear H'3.
LApply (H a); [Intros H'4; Case H'4 | Idtac]; Auto.
Intros a b L4 L5 L6 H'0 H'1 H'2 H'3; Apply incl_tran with m := L6;
Auto with datatypes.
Apply H'2; Auto.
Apply DisjointInv2 with a := a; Auto.
Intros a b L4 L5 L6 H'0 H'1 H'2 H'3; Apply incl_cons with A := A;
Auto with datatypes; Apply incl_tran with m := L6; Auto with datatypes.
Apply H'2; Apply DisjointInv1 with a := b; Auto.
Qed.

Theorem appendInv:
  (L1, L2, L3:(list A)) (append L1 L2 L3) ->
  (m:A) (In m L3) ->(In m L1) \/ (In m L2).
Intros L1 L2 L3 H'; Elim H'; Simpl; Auto.
Intros a b L4 L5 L6 H'0 H'1 H'2 m H'3; Elim H'3; Clear H'3; Intros H'4;
[Rewrite <- H'4 | Idtac]; Auto.
Elim (H'2 m); [Intros H'6 | Intros H'6 | Idtac]; Auto.
Intros a b L4 L5 L6 H'0 H'1 H'2 m H'3; Elim H'3; Clear H'3; Intros H'4; Auto.
Elim (H'2 m); [Intros H'6 | Intros H'6 | Idtac]; Auto.
Intros a b L4 L5 L6 H'0 H'1 H'2 m H'3; Elim H'3; Clear H'3; Intros H'4; Auto.
Elim (H'2 m); [Intros H'6 | Intros H'6 | Idtac]; Auto.
Qed.

Theorem appendEqInv:
  (L1, L2, L3:(list A)) (append L1 L2 L3) ->
  (m:A) (InEq m L3) ->(InEq m L1) \/ (InEq m L2).
Intros L1 L2 L3 H'; Elim H'; Simpl; Auto.
Intros a b L4 L5 L6 H'0 H'1 H'2 m H'3; Inversion_clear H'3; Auto.
Case (H'2 m H); Intros H'5; Auto.
Intros a b L4 L5 L6 H'0 H'1 H'2 m H'3; Inversion_clear H'3; Auto.
Case (H'2 m H); Intros H'5; Auto.
Intros a b L4 L5 L6 H'0 H'1 H'2 m H'3; Inversion_clear H'3; Auto.
Case (H'2 m H); Intros H'5; Auto.
Qed.

Theorem appendDisjoint:
  (L1, L2, L3:(list A)) (append L1 L2 L3) ->
  (L4:(list A)) (Disjoint L1 L4) -> (Disjoint L2 L4) ->(Disjoint L3 L4).
Intros L1 L2 L3 H'; Elim H'; Auto.
Intros a b L4 L5 L6 H'0 H'1 H'2 L7 H'3 H'4.
Apply DisjointCons2; Auto.
Apply H'2; Auto.
Apply DisjointInv2 with a := a; Auto.
Apply DisjointInv2 with a := b; Auto.
Inversion_clear H'3; Auto.
Intros a b L4 L5 L6 H'0 H'1 H'2 L7 H'3 H'4; Apply DisjointCons2; Auto.
Apply H'2; Auto.
Apply DisjointInv2 with a := a; Auto.
Inversion_clear H'3; Auto.
Intros a b L4 L5 L6 H'0 H'1 H'2 L7 H'3 H'4; Apply DisjointCons2; Auto.
Apply H'2; Auto.
Apply DisjointInv2 with a := b; Auto.
Inversion_clear H'4; Auto.
Qed.

Theorem appendSup:
  (L1, L2, L3:(list A)) (append L1 L2 L3) ->
  (a:A) ((b:A) (In b L1) ->(ltA a b)) -> ((b:A) (In b L2) ->(ltA a b)) ->
  (b:A) (In b L3) ->(ltA a b).
Intros L1 L2 L3 H'; Elim H'; Simpl; Auto;
Intros a b L4 L5 L6 H'0 H'1 H'2 a0 H'3 H'4 b0 H'5;
(Elim H'5; [Intros H'6; Rewrite <- H'6; Clear H'5 | Intros H'6; Clear H'5]);
Auto.
Qed.

Theorem appendOlist:
  (L1, L2, L3:(list A)) (append L1 L2 L3) -> (Olist L1) -> (Olist L2) ->
  (Olist L3).
Intros L1 L2 L3 H'; Elim H'; Auto.
Intros a b L4 L5 L6; Case L6; Auto.
Intros a0 l H'0 H'1 H'2 H'3 H'4.
Apply OlistCons; Auto.
Apply H'2; Auto.
Apply OlistInv with a := a; Auto.
Apply OlistInv with a := b; Auto.
Apply appendSup with L1 := L4 L2 := L5 L3 := (cons a0 l); Auto.
Intros b0 H'5.
Apply OlistSup with L := L4; Auto.
Intros b0 H'5.
Apply ltAeqAComp with a := b b := b0; Auto.
Apply OlistSup with L := L5; Auto.
Simpl; Auto.
Intros a b L4 L5 L6; Case L6; Auto.
Intros a0 l H'0 H'1 H'2 H'3 H'4.
Apply OlistCons; Auto.
Apply H'2; Auto.
Apply OlistInv with a := a; Auto.
Apply appendSup with L1 := L4 L2 := (cons b L5) L3 := (cons a0 l); Auto.
Intros b0 H'5.
Apply OlistSup with L := L4; Auto.
Intros b0 H'5.
Apply OlistSup with L := (cons b L5); Auto.
Simpl; Auto.
Intros a b L4 L5 L6; Case L6; Auto.
Intros a0 l H'0 H'1 H'2 H'3 H'4.
Apply OlistCons; Auto.
Apply H'2; Auto.
Apply OlistInv with a := b; Auto.
Apply appendSup with L1 := (cons a L4) L2 := L5 L3 := (cons a0 l); Auto.
Intros b0 H'5.
Apply OlistSup with L := (cons a L4); Auto.
Intros b0 H'5.
Apply OlistSup with L := L5; Auto.
Simpl; Auto.
Qed.

Definition size := (!length A).

Definition sizel :=
   [m:(list A) * (list A)]
      Cases m of
          (pair l1 l2) => (plus (size l1) (size l2))
      end.

Definition lessP := [m1, m2:(list A) * (list A)](lt (sizel m1) (sizel m2)).

Lemma wf_lessP: (well_founded (list A) * (list A) lessP).
Red.
Cut (n:nat) (a:(list A) * (list A)) (lt (sizel a) n) ->
    (Acc (list A) * (list A) lessP a).
Intros H' a.
Apply H' with n := (S (sizel a)); Auto.
Intros n; Elim n; Clear n.
Intros a H; Inversion H.
Intros n H' a H'0; Try Assumption.
Apply Acc_intro.
Intros y H'1; Try Assumption.
Apply H'.
Unfold lessP in H'1.
Apply lt_le_trans with (sizel a); Auto with arith.
Qed.

Definition appendfAux:
  (L:(list A) * (list A)){M:(list A) | (append (Fst L) (Snd L) M)}.
Intros L; Pattern L.
Apply well_founded_induction with A := (list A) * (list A) R := lessP; Auto.
Exact wf_lessP.
Intros x; Case x; Simpl.
Intros L1 L2; Case L1.
Intros Rec; Exists L2; Auto.
Intros m1 L'1; Case L2; Simpl.
Intros Rec; Exists (cons m1 L'1); Auto.
Intros m2 L'2 Rec.
Case (ltADec m1 m2); [Intros tmp; Case tmp; Clear tmp | Idtac]; Intros lt0.
Cut (lessP (L'1, (cons m2 L'2)) ((cons m1 L'1), (cons m2 L'2)));
[Intros less0 | Red; Simpl]; Auto.
Case (Rec (L'1, (cons m2 L'2)) less0); Simpl.
Intros L3 HL3; Exists (cons m1 L3); Auto.
Cut (lessP ((cons m1 L'1), L'2) ((cons m1 L'1), (cons m2 L'2)));
[Intros less0 | Red; Simpl; Auto with arith].
Case (Rec ((cons m1 L'1), L'2) less0); Simpl.
Intros L3 HL3; Exists (cons m2 L3); Auto.
Cut (lessP (L'1, L'2) ((cons m1 L'1), (cons m2 L'2)));
[Intros less0 | Red; Simpl; Auto with arith].
Case (Rec (L'1, L'2) less0); Simpl.
Intros L3 HL3; Exists (cons m1 L3); Auto.
Defined.

Definition appendf: (L1, L2:(list A))(list A).
Intros L1 L2; Case (appendfAux (L1, L2)).
Intros L3 H'0; Exact L3.
Defined.

Theorem appendfAppend: (L1, L2:(list A))(append L1 L2 (appendf L1 L2)).
Intros L1 L2; Unfold appendf; Case (appendfAux (L1, L2)); Simpl; Auto.
Qed.
Hints Resolve appendfAppend.

Theorem appendfIncl1:
  (L1, L2:(list A)) (Disjoint L1 L2) ->(incl L1 (appendf L1 L2)).
Intros L1 L2 HL1L2.
Apply appendDisjIncl1 with L2 := L2; Auto.
Qed.

Theorem appendfIncl2:
  (L1, L2:(list A)) (Disjoint L1 L2) ->(incl L2 (appendf L1 L2)).
Intros L1 L2 HL1L2.
Apply appendDisjIncl2 with L1 := L1; Auto.
Qed.

Theorem appendfInv:
  (L1, L2:(list A)) (m:A) (In m (appendf L1 L2)) ->(In m L1) \/ (In m L2).
Intros L1 L2 m H'.
Apply appendInv with L3 := (appendf L1 L2); Auto.
Qed.

Theorem appendfInclEq1: (L1, L2:(list A))(InclEq L1 (appendf L1 L2)).
Intros L1 L2.
Apply appendIncl1 with L2 := L2; Auto.
Qed.

Theorem appendfInclEq2: (L1, L2:(list A))(InclEq L2 (appendf L1 L2)).
Intros L1 L2.
Apply appendIncl2 with L1 := L1; Auto.
Qed.

Theorem appendfInvEq:
  (L1, L2:(list A)) (m:A) (InEq m (appendf L1 L2)) ->(InEq m L1) \/ (InEq m L2).
Intros L1 L2 m H'.
Apply appendEqInv with L3 := (appendf L1 L2); Auto.
Qed.

Theorem NotInAppendf:
  (L1, L2:(list A)) (m:A) ~ (InEq m L1) -> ~ (InEq m L2) ->
  ~ (InEq m (appendf L1 L2)).
Intros L1 L2 m H' H'0; Red; Intros H'1.
Case (appendfInvEq L1 L2 m H'1); Auto.
Qed.

Theorem appendfDisjoint:
  (L1, L2:(list A)) (Disjoint L1 L2) ->
  (L3:(list A)) (Disjoint L1 L3) -> (Disjoint L2 L3) ->
  (Disjoint (appendf L1 L2) L3).
Intros L1 L2 HL1L2 L3 H' H'0.
Apply appendDisjoint with L1 := L1 L2 := L2; Auto.
Qed.

Theorem appendfOlist:
  (L1, L2:(list A)) (Olist L1) -> (Olist L2) ->(Olist (appendf L1 L2)).
Intros L1 L2 H' H'0.
Apply appendOlist with L1 := L1 L2 := L2; Auto.
Qed.

Theorem Olistf: (L:(list A)) (Olist L) ->(Olist (map f L)).
Intros L H'; Elim H'; Simpl; Auto.
Intros a b L0 H'0 H'1 H'2.
Apply OlistCons; Auto.
Apply ltAeqAComp with a := a b := b; Auto.
Qed.

Theorem Disjointf:
  (L1, L2:(list A)) (Disjoint L1 L2) ->(Disjoint L1 (map f L2)).
Intros L1 L2 H'; Elim H'; Auto.
Intros L3 L4; Elim L4; Simpl; Auto.
Intros H'0.
Apply DisjointDef; Simpl; Auto.
Intros a l H'0 H'1.
Apply DisjointCons1; Auto.
Apply H'0; Auto.
Intros a0 H'2; Red; Intros H'3.
LApply (H'1 a0); [Intros H'5; Case H'5 | Idtac]; Auto.
Red; Intros H'2.
LApply (H'1 (f a)); [Intros H'5; Case H'5 | Idtac]; Auto.
Qed.

Definition fappendfAux:
  (L:(list A) * (list A)){M:(list A) | (append (Fst L) (map f (Snd L)) M)}.
Intros L; Pattern L.
Apply well_founded_induction with A := (list A) * (list A) R := lessP; Auto.
Exact wf_lessP.
Intros x; Case x; Simpl.
Intros L1 L2; Case L1.
Intros Rec; Exists (map f L2); Auto.
Intros m1 L'1; Case L2; Simpl.
Intros Rec; Exists (cons m1 L'1); Auto.
Intros m2 L'2 Rec.
Case (ltADec m1 m2); [Intros tmp; Case tmp; Clear tmp | Idtac]; Intros lt0.
Cut (lessP (L'1, (cons m2 L'2)) ((cons m1 L'1), (cons m2 L'2)));
[Intros less0 | Red; Simpl]; Auto.
Case (Rec (L'1, (cons m2 L'2)) less0); Simpl.
Intros L3 HL3; Exists (cons m1 L3); Auto.
Apply appendLtA1; Auto.
Apply ltAeqAComp with a := m1 b := m2; Auto.
Cut (lessP ((cons m1 L'1), L'2) ((cons m1 L'1), (cons m2 L'2)));
[Intros less0 | Red; Simpl; Auto with arith].
Case (Rec ((cons m1 L'1), L'2) less0); Simpl.
Intros L3 HL3; Exists (cons (f m2) L3); Auto.
Apply appendLtA2; Auto.
Apply ltAeqAComp with a := m2 b := m1; Auto.
Cut (lessP (L'1, L'2) ((cons m1 L'1), (cons m2 L'2)));
[Intros less0 | Red; Simpl; Auto with arith].
Case (Rec (L'1, L'2) less0); Simpl.
Intros L3 HL3; Exists (cons m1 L3); Auto.
Apply appendEqA; Auto.
Apply eqATrans with y := m2; Auto.
Defined.

Definition fappendf: (L1, L2:(list A))(list A).
Intros L1 L2; Case (fappendfAux (L1, L2)).
Intros L3 H'0; Exact L3.
Defined.

Theorem fappendfAppend:
  (L1, L2:(list A))(append L1 (map f L2) (fappendf L1 L2)).
Intros L1 L2; Unfold fappendf; Case (fappendfAux (L1, L2)); Simpl; Auto.
Qed.
Hints Resolve fappendfAppend.

Theorem fappendfIncl1:
  (L1, L2:(list A)) (HL1L2:(Disjoint L1 L2))(incl L1 (fappendf L1 L2)).
Intros L1 L2 HL1L2.
Apply appendDisjIncl1 with L2 := (map f L2); Auto.
Apply Disjointf; Auto.
Qed.

Theorem fappendfIncl2:
  (L1, L2:(list A)) (HL1L2:(Disjoint L1 L2))(incl (map f L2) (fappendf L1 L2)).
Intros L1 L2 HL1L2.
Apply appendDisjIncl2 with L1 := L1; Auto.
Apply Disjointf; Auto.
Qed.

Theorem fappendfInv:
  (L1, L2:(list A)) (m:A) (In m (fappendf L1 L2)) ->
  (In m L1) \/ (In m (map f L2)).
Intros L1 L2 m H'.
Apply appendInv with L3 := (fappendf L1 L2); Auto.
Qed.

Theorem fappendfInclEq1: (L1, L2:(list A))(InclEq L1 (fappendf L1 L2)).
Intros L1 L2.
Apply appendIncl1 with L2 := (map f L2); Auto.
Qed.

Theorem fappendfInclEq2: (L1, L2:(list A))(InclEq (map f L2) (fappendf L1 L2)).
Intros L1 L2.
Apply appendIncl2 with L1 := L1; Auto.
Qed.

Theorem fappendfInvEq:
  (L1, L2:(list A)) (m:A) (InEq m (fappendf L1 L2)) ->
  (InEq m L1) \/ (InEq m (map f L2)).
Intros L1 L2 m H'.
Apply appendEqInv with L3 := (fappendf L1 L2); Auto.
Qed.

Theorem fappendfDisjoint:
  (L1, L2:(list A))
  (HL1L2:(Disjoint L1 L2)) (L3:(list A)) (Disjoint L1 L3) -> (Disjoint L2 L3) ->
  (Disjoint (fappendf L1 L2) L3).
Intros L1 L2 HL1L2 L3 H' H'0.
Apply appendDisjoint with L1 := L1 L2 := (map f L2); Auto.
Apply DisjointCom.
Apply Disjointf.
Apply DisjointCom; Auto.
Qed.

Theorem fappendfOlist:
  (L1, L2:(list A)) (Olist L1) -> (Olist L2) ->(Olist (fappendf L1 L2)).
Intros L1 L2 H' H'0.
Apply appendOlist with L1 := L1 L2 := (map f L2); Auto.
Apply Olistf; Auto.
Qed.
Variable test:A -> A ->Prop.
Variable testDec:(a, b:A) (eqA a b) ->{(test a b)}+{~ (test a b)}.
Variable testEq:(a, b:A) (test a b) ->(eqA a b).

Mutual Inductive minProp: (list A) -> (list A) -> A ->Prop :=
     minDef:
       (a, b:A)
       (L1, L2:(list A))
       (In a L1) ->
       (In b L2) ->
       (test a b) ->
       ((c, d:A) (In c L1) -> (In d L2) -> (test c d) ->~ (ltA c a)) ->
       (minProp L1 L2 a) .

Definition getMinAux: (L:(list A) * (list A)){a:(Option A) | Cases a of
                                                                 (Some b) =>
                                                                   (Olist
                                                                      (Fst L)) ->
                                                                   (Olist
                                                                      (Snd L)) ->
                                                                   (minProp
                                                                      (Fst L)
                                                                      (Snd L) b)
                                                                | None =>
                                                                    (Olist
                                                                       (Fst L)) ->
                                                                    (Olist
                                                                       (Snd L)) ->
                                                                    (a, b:A)
                                                                    (In
                                                                       a (Fst L)) ->
                                                                    (In
                                                                       b (Snd L)) ->
                                                                    ~ (test a b)
                                                             end}.
Intros L; Pattern L.
Apply well_founded_induction with A := (list A) * (list A) R := lessP; Auto.
Exact wf_lessP.
Intros x; Case x; Simpl.
Intros L1 L2; Case L1.
Intros H'; Exists (None A); Auto.
Intros a L'1; Case L2; Simpl.
Intros H'; Exists (None A); Auto.
Intros b L'2 Rec.
Generalize (OlistInv a); Intros OL1.
Generalize (OlistInv b); Intros OL2.
Case (ltADec a b); [Intros tmp; Case tmp; Clear tmp | Idtac]; Intros lt0.
Cut (lessP (L'1, (cons b L'2)) ((cons a L'1), (cons b L'2)));
[Intros less0 | Red; Simpl]; Auto.
Case (Rec (L'1, (cons b L'2)) less0); Simpl; Auto.
Intros x0 H'; Exists x0; Auto.
Generalize H'; Clear H'; Case x0; Auto.
Intros x1 H'0 H'1 H'2.
Generalize (H'0 (OL1 ? H'1) H'2); Clear H'0; Intros min1; Inversion min1.
Apply minDef with b := b0; Auto with datatypes.
Intros c d H'0; Simpl in H'0; Case H'0; Auto.
Intros H'3; Rewrite <- H'3; Auto.
Intros H'5 H'6; Red; Intros H'7; Absurd (eqA a d); Auto.
Apply ltAImpNotEqA; Auto.
Simpl in H'5.
Elim H'5; [Intros H'8; Rewrite <- H'8; Clear H'5 | Intros H'8; Clear H'5]; Auto.
Apply ltATrans with y := b; Auto.
Apply OlistSup with L := L'2; Auto.
Intros H'3 H'5 H'6.
Apply H2 with d := d; Auto.
Intros H' H'0 H'1 a0 b0 H'2; Elim H'2; Clear H'2; Intros H'2;
[Rewrite <- H'2 | Idtac]; Intros H'3; Auto.
Red; Intros H'4; Absurd (eqA a b0); Auto.
Apply ltAImpNotEqA; Auto.
Elim H'3; Clear H'3; Intros H'3; [Rewrite <- H'3 | Idtac]; Auto.
Apply ltATrans with y := b; Auto.
Apply OlistSup with L := L'2; Auto.
Cut (lessP ((cons a L'1), L'2) ((cons a L'1), (cons b L'2)));
[Intros less0 | Red; Simpl]; Auto.
Case (Rec ((cons a L'1), L'2) less0); Simpl; Auto.
Intros x0 H'; Exists x0; Auto.
Generalize H'; Case x0; Auto.
Intros x1 H'0 H'1 H'2.
Generalize (H'0 H'1 (OL2 ? H'2)); Clear H'0; Intros min1; Inversion min1.
Apply minDef with b := b0; Auto with datatypes.
Intros c d H'0 H'3; Simpl in H'3; Case H'3; Auto.
Intros H'5; Rewrite <- H'5; Auto.
Intros H'6; Red; Intros H'7; Absurd (eqA b c); Auto.
Apply ltAImpNotEqA; Auto.
Simpl in H'0.
Elim H'0; [Intros H'8; Rewrite <- H'8; Clear H'0 | Intros H'8; Clear H'0]; Auto.
Apply ltATrans with y := a; Auto.
Apply OlistSup with L := L'1; Auto.
Intros H'5 H'6.
Apply H2 with d := d; Auto.
Intros H'0 H'1 H'2 a0 b0 H'3 H'4; Elim H'4; Clear H'4; Intros H'4;
[Rewrite <- H'4 | Idtac]; Auto.
Red; Intros H'5; Absurd (eqA b a0); Auto.
Apply ltAImpNotEqA.
Elim H'3; Clear H'3; Intros H'3; [Rewrite <- H'3 | Idtac]; Auto.
Apply ltATrans with y := a; Auto.
Apply OlistSup with L := L'1; Auto.
Rewrite (plus_sym (size L'1) (S (size L'2))); Simpl;
Rewrite (plus_sym (size L'2) (size L'1)); Auto.
Case (testDec a b lt0); Intros test1.
Exists (Some ? a); Auto.
Intros H' H'0.
Apply minDef with b := b; Auto with datatypes.
Intros c d H'1; Simpl in H'1; Case H'1; Auto.
Intros H'2; Rewrite <- H'2; Auto.
Intros H'2 H'3 H'4; Red; Intros H'5; Absurd (ltA c c); Auto.
Apply ltATrans with y := a; Auto.
Apply OlistSup with L := L'1; Auto.
Cut (lessP (L'1, L'2) ((cons a L'1), (cons b L'2)));
[Intros less0 | Red; Simpl]; Auto.
Case (Rec (L'1, L'2) less0); Simpl; Auto.
Intros x0 H'; Exists x0; Auto.
Generalize H'; Case x0; Auto.
Intros x1 H'0 H'1 H'2.
Generalize (H'0 (OL1 ? H'1) (OL2 ? H'2)); Clear H'0; Intros min1; Inversion min1.
Apply minDef with b := b0; Auto with datatypes.
Intros c d H'0; Simpl in H'0; Case H'0; Auto.
Intros H'3; Rewrite <- H'3; Auto.
Intros H'5; Simpl in H'5; Auto.
Elim H'5; [Intros H'8; Rewrite <- H'8; Clear H'5 | Intros H'8; Clear H'5]; Auto.
Intros H'5; Red; Intros H'6; Absurd (eqA a d); Auto.
Apply ltAImpNotEqA; Auto.
Apply ltAeqAComp with a := b b := d; Auto.
Apply OlistSup with L := L'2; Auto.
Intros H'3 H'5; Simpl in H'5; Case H'5.
Intros H'6; Rewrite <- H'6; Auto.
Intros H'7; Red; Intros H'8; Absurd (eqA b c); Auto.
Apply ltAImpNotEqA; Auto.
Apply ltAeqAComp with a := a b := c; Auto.
Apply OlistSup with L := L'1; Auto.
Intros H'6 H'7.
Apply H2 with d := d; Auto.
Intros H'0 H'1 H'2 a0 b0 H'3; Elim H'3; Clear H'3; Intros H'3;
[Rewrite <- H'3 | Idtac]; Auto.
Intros H'4; Elim H'4; Clear H'4; Intros H'4; [Rewrite <- H'4 | Idtac]; Auto.
Red; Intros H'5; Absurd (eqA a b0); Auto.
Apply ltAImpNotEqA; Auto.
Apply ltAeqAComp with a := b b := b0; Auto.
Apply OlistSup with L := L'2; Auto.
Intros H'4; Elim H'4; Clear H'4; Intros H'4; [Rewrite <- H'4 | Idtac]; Auto.
Red; Intros H'5; Absurd (eqA b a0); Auto.
Apply ltAImpNotEqA; Auto.
Apply ltAeqAComp with a := a b := a0; Auto.
Apply OlistSup with L := L'1; Auto.
Rewrite (plus_sym (size L'1) (S (size L'2))); Simpl;
Rewrite (plus_sym (size L'2) (size L'1)); Auto.
Defined.

Definition getMin: (L1, L2:(list A))(Option A).
Intros L1 L2; Case (getMinAux (L1, L2)).
Intros x H'1; Exact x.
Defined.

Theorem MinPropIn: (a:A) (L1, L2:(list A)) (minProp L1 L2 a) ->(In a L1).
Intros a L1 L2 H'; Elim H'; Auto.
Qed.

Theorem getMinIn:
  (a:A)
  (L1, L2:(list A)) (Olist L1) -> (Olist L2) -> (getMin L1 L2)=(Some ? a) ->
  (In a L1).
Intros a L1 L2 H' H'0; Unfold getMin; Case (getMinAux (L1, L2)); Auto.
Intros x; Case x; Simpl.
Intros x0 H'1 H'2; Inversion H'2; Auto.
Apply MinPropIn with L2 := L2; Auto.
Rewrite <- H0; Auto.
Intros H'1 H'2; Discriminate.
Qed.

Theorem MinPropComp:
  (a:A) (L1, L2:(list A)) (minProp L1 L2 a) ->(Ex [b:A] (test a b) /\ (In b L2)).
Intros a L1 L2 H'; Elim H'; Auto.
Intros a0 b L3 L4 H'0 H'1 H'2 H'3; Exists b; Split; Auto.
Qed.

Theorem getMinComp:
  (a:A)
  (L1, L2:(list A)) (Olist L1) -> (Olist L2) -> (getMin L1 L2)=(Some ? a) ->
  (Ex [b:A] (test a b) /\ (In b L2)).
Intros a L1 L2 H' H'0; Unfold getMin; Case (getMinAux (L1, L2)); Auto.
Intros x; Case x; Simpl.
Intros x0 H'1 H'2; Inversion H'2; Auto.
Apply MinPropComp with L1 := L1; Auto.
Rewrite <- H0; Auto.
Intros H'1 H'2; Discriminate.
Qed.

Theorem getMinMin:
  (a:A)
  (L1, L2:(list A)) (Olist L1) -> (Olist L2) -> (getMin L1 L2)=(Some ? a) ->
  (b, c:A) (ltA b a) -> (In b L1) -> (In c L2) ->~ (test b c).
Intros a L1 L2 H' H'0; Unfold getMin; Case (getMinAux (L1, L2)); Auto.
Intros x; Case x; Simpl.
Intros x0 H'1 H'2; Inversion H'2; Auto.
Generalize (H'1 H' H'0); Intros H'3; Inversion H'3.
Intros b0 c H'4 H'5 H'6; Red; Intros H'7.
Absurd (ltA b0 a); Auto.
Rewrite <- H0.
Apply H3 with d := c; Auto.
Intros H'1 H'2; Discriminate.
Qed.

Theorem getMinNone:
  (L1, L2:(list A)) (Olist L1) -> (Olist L2) -> (getMin L1 L2)=(None ?) ->
  (a, b:A) (In a L1) -> (In b L2) ->~ (test a b).
Intros L1 L2 H' H'0; Unfold getMin; Case (getMinAux (L1, L2)); Auto.
Intros x; Case x; Simpl; Auto.
Intros x0 H'1 H'2; Discriminate.
Qed.

Mutual Inductive inter: (list A) -> (list A) -> (list A) ->Prop :=
     interNil1: (L1:(list A))(inter L1 (nil ?) (nil ?))
    | interNil2: (L2:(list A))(inter (nil ?) L2 (nil ?))
    | interEqA:
        (a, b:A) (L1, L2, L3:(list A)) (eqA a b) -> (inter L1 L2 L3) ->
        (inter (cons a L1) (cons b L2) (cons a L3))
    | interLtA1:
        (a, b:A) (L1, L2, L3:(list A)) (ltA a b) -> (inter L1 (cons b L2) L3) ->
        (inter (cons a L1) (cons b L2) L3)
    | interLtA2:
        (a, b:A) (L1, L2, L3:(list A)) (ltA b a) -> (inter (cons a L1) L2 L3) ->
        (inter (cons a L1) (cons b L2) L3) .

Theorem interIncl1: (L1, L2, L3:(list A)) (inter L1 L2 L3) ->(InclEq L3 L1).
Intros L1 L2 L3 H'; Elim H'; Auto with datatypes.
Intros a b L4 L5 L6 H'0 H'1 H'2.
Apply InclEqCons; Auto.
Apply InclEqTrans with y := L4; Auto.
Intros a b L4 L5 L6 H'0 H'1 H'2.
Apply InclEqTrans with y := L4; Auto.
Qed.

Theorem interIncl2: (L1, L2, L3:(list A)) (inter L1 L2 L3) ->(InclEq L3 L2).
Intros L1 L2 L3 H'; Elim H'; Auto with datatypes.
Intros a b L4 L5 L6 H'0 H'1 H'2.
Apply InclEqCons; Auto.
Apply InclEqTrans with y := L5; Auto.
Intros a b L4 L5 L6 H'0 H'1 H'2.
Apply InclEqTrans with y := L5; Auto.
Qed.

Theorem interSup:
  (L1, L2, L3:(list A)) (inter L1 L2 L3) ->
  (a:A) ((b:A) (In b L1) ->(ltA a b)) -> ((b:A) (In b L2) ->(ltA a b)) ->
  (b:A) (In b L3) ->(ltA a b).
Intros L1 L2 L3 H'; Elim H'; Simpl; Auto;
Intros a b L4 L5 L6 H'0 H'1 H'2 a0 H'3 H'4 b0 H'5;
(Elim H'5; [Intros H'6; Rewrite <- H'6; Clear H'5 | Intros H'6; Clear H'5]);
Auto.
Qed.

Theorem interOlist:
  (L1, L2, L3:(list A)) (inter L1 L2 L3) -> (Olist L1) -> (Olist L2) ->
  (Olist L3).
Intros L1 L2 L3 H'; Elim H'; Auto.
Intros a b L4 L5 L6; Case L6; Auto.
Intros a0 l H'0 H'1 H'2 H'3 H'4.
Apply OlistCons; Auto.
Apply H'2; Auto.
Apply OlistInv with a := a; Auto.
Apply OlistInv with a := b; Auto.
Apply interSup with L1 := L4 L2 := L5 L3 := (cons a0 l); Auto.
Intros b0 H'5.
Apply OlistSup with L := L4; Auto.
Intros b0 H'5.
Apply ltAeqAComp with a := b b := b0; Auto.
Apply OlistSup with L := L5; Auto.
Simpl; Auto.
Intros a b L4 L5 L6 H'0 H'1 H'2 H'3 H'4.
Apply H'2; Auto.
Apply OlistInv with a := a; Auto.
Intros a b L4 L5 L6 H'0 H'1 H'2 H'3 H'4.
Apply H'2; Auto.
Apply OlistInv with a := b; Auto.
Qed.

Theorem InEqNList: (a:A) (L:(list A)) (InEq a L) ->~ (Olist (cons a L)).
Intros a L; Elim L; Auto.
Intros H'; Inversion H'; Auto.
Intros a0 l H' H'0; Inversion H'0; Auto.
Red; Intros H'1; Inversion H'1; Auto.
Absurd (eqA a a0); Auto.
Red; Intros H'1; Case H'; Auto.
Apply OlistSkip with b := a0; Auto.
Qed.

Theorem InEqSup:
  (a, b:A) (L:(list A)) (InEq a L) -> (Olist (cons b L)) ->(ltA b a).
Intros a b L; Elim L; Auto.
Intros H'; Inversion H'; Auto.
Intros a0 l H' H'0 H'1; Inversion H'0; Auto.
Apply ltAeqAComp with a := b b := a0; Auto.
Apply OlistSup with L := (cons a0 l); Auto with datatypes.
Apply H'; Auto.
Apply OlistSkip with b := a0; Auto.
Qed.

Theorem InEqOlistInv:
  (a, b:A)
  (L1, L2:(list A))
  (InclEq (cons a L1) (cons b L2)) ->
  (Olist (cons a L1)) -> (Olist (cons b L2)) ->
  (InclEq (cons a L1) L2) \/ (eqA a b) /\ (InclEq L1 L2).
Intros a b L1 L2 H' H'0 H'1.
Case (ltADec a b); Intros Eqab.
Case Eqab; Clear Eqab; Intros Eqab.
Absurd (Olist (cons a (cons b L2))); Auto.
Apply InEqNList; Auto.
Inversion H'; Auto.
Left.
Inversion H'; Auto.
Apply InclEqDef; Auto.
Intros a0 H'2.
LApply (H a0); [Intros H'4 | Idtac]; Auto.
Inversion H'4; Auto.
Absurd (Olist (cons a0 (cons a L1))); Auto.
Apply InEqNList; Auto.
Apply OlistCons; Auto.
Apply ltAeqAComp with a := b b := a; Auto.
Right; Split; Auto.
Apply InclEqDef; Auto.
Intros a0 H'2.
Inversion H'.
LApply (H a0); [Intros H'4 | Idtac]; Auto.
Inversion H'4; Auto.
Absurd (eqA a a0); Auto.
Apply ltAImpNotEqA; Auto.
Apply InEqSup with L := L1; Auto.
Apply eqATrans with y := b; Auto.
Qed.

Theorem interMin:
  (L1, L2, L3, L4:(list A))
  (inter L1 L2 L3) ->
  (Olist L1) ->
  (Olist L2) -> (Olist L3) -> (Olist L4) -> (InclEq L4 L1) -> (InclEq L4 L2) ->
  (InclEq L4 L3).
Intros L1 L2 L3 L4 H'; Generalize L4; Clear L4; Elim H'; Auto.
Intros a b L4 L5 L6 H'0 H'1 H'2 L7; Case L7; Auto.
Intros a0 l H'3 H'4 H'5 H'6 H'7 H'8.
Case (eqADec a0 a); Auto.
Intros H'9.
Apply InclEqCons; Auto.
Apply InclEqTrans with y := L6; Auto.
Apply H'2; Auto.
Apply OlistInv with a := a; Auto.
Apply OlistInv with a := b; Auto.
Apply OlistInv with a := a; Auto.
Apply OlistInv with a := a0; Auto.
Apply InclEqOlist with a := a0 b := a; Auto.
Apply InclEqOlist with a := a0 b := b; Auto.
Intros H'9.
Apply InclEqTrans with y := L6; Auto.
Apply H'2; Auto.
Apply OlistInv with a := a; Auto.
Apply OlistInv with a := b; Auto.
Apply OlistInv with a := a; Auto.
Elim (InEqOlistInv a0 a l L4);
[Intros H'17; Apply H'17 | Intros H'17; Elim H'17; Intros H'18 | Idtac |
   Idtac | Idtac]; Auto.
Case H'9; Auto.
Elim (InEqOlistInv a0 b l L5);
[Intros H'17; Apply H'17 | Intros H'17; Elim H'17; Intros H'18 | Idtac |
   Idtac | Idtac]; Auto.
Case H'9; Auto.
Apply eqATrans with y := b; Auto.
Intros a b L4 L5 L6 H'0 H'1 H'2 L7; Case L7; Auto.
Intros a0 l H'3 H'4 H'5 H'6 H'7 H'8.
Apply H'2; Auto.
Apply OlistInv with a := a; Auto.
Elim (InEqOlistInv a0 a l L4);
[Intros H'17; Apply H'17 | Intros H'17; Elim H'17; Intros H'18 | Idtac |
   Idtac | Idtac]; Auto.
Absurd (Olist (cons a0 (cons b L5))); Auto.
Apply InEqNList; Auto.
Inversion H'8; Auto.
Apply OlistCons; Auto.
Apply ltAeqAComp with a := a b := b; Auto.
Intros a b L4 L5 L6 H'0 H'1 H'2 L7; Case L7; Auto.
Intros a0 l H'3 H'4 H'5 H'6 H'7 H'8.
Apply H'2; Auto.
Apply OlistInv with a := b; Auto.
Elim (InEqOlistInv a0 b l L5);
[Intros H'17; Apply H'17 | Intros H'17; Elim H'17; Intros H'18 | Idtac |
   Idtac | Idtac]; Auto.
Absurd (Olist (cons a0 (cons a L4))); Auto.
Apply InEqNList; Auto.
Inversion H'7; Auto.
Apply OlistCons; Auto.
Apply ltAeqAComp with a := b b := a; Auto.
Qed.

Theorem interCom:
  (L1, L2, L3, L4:(list A))
  (inter L1 L2 L3) ->
  (inter L2 L1 L4) -> (Olist L1) -> (Olist L2) -> (Olist L3) -> (Olist L4) ->
  (EqL L3 L4).
Intros L1 L2 L3 L4 H' H'0 H'1 H'2 H'3 H'4.
Apply EqLOlist; Auto.
Apply interMin with L1 := L2 L2 := L1; Auto.
Apply interIncl2 with L1 := L1; Auto.
Apply interIncl1 with L2 := L2; Auto.
Apply interMin with L1 := L1 L2 := L2; Auto.
Apply interIncl2 with L1 := L2; Auto.
Apply interIncl1 with L2 := L1; Auto.
Qed.

Definition interAux: (L1, L2:(list A)){L3:(list A) | (inter L1 L2 L3)}.
Intros L1; Elim L1; Auto.
Intros L2; Exists (nil A); Auto.
Apply interNil2; Auto.
Intros a l H' L2; Elim L2; Auto.
Exists (nil A); Apply interNil1; Auto.
Intros a0 l0 H'0.
Case (ltADec a a0); Intros s.
Case s; Clear s; Intros s.
Case (H' (cons a0 l0)); Intros L3 HL3.
Exists L3; Auto.
Apply interLtA1; Auto.
Case H'0; Intros L3 HL3.
Exists L3; Auto.
Apply interLtA2; Auto.
Case (H' l0); Intros L3 HL3.
Exists (cons a L3); Auto.
Apply interEqA; Auto.
Defined.

Definition interf: (list A) -> (list A) ->(list A) :=
   [L1, L2:(list A)]
      Cases (interAux L1 L2) of
          (exist L3 _) => L3
      end.

Theorem interfProp1: (L1, L2:(list A))(inter L1 L2 (interf L1 L2)).
Intros L1 L2; Unfold interf; Case (interAux L1 L2); Auto.
Qed.
Hints Resolve interfProp1.

Theorem interfIncl1: (L1, L2:(list A))(InclEq (interf L1 L2) L1).
Intros L1 L2.
Apply interIncl1 with L2 := L2; Auto.
Qed.

Theorem interfIncl2: (L1, L2:(list A))(InclEq (interf L1 L2) L2).
Intros L1 L2.
Apply interIncl2 with L1 := L1; Auto.
Qed.

Theorem interfOlist:
  (L1, L2:(list A)) (Olist L1) -> (Olist L2) ->(Olist (interf L1 L2)).
Intros L1 L2 H' H'0.
Apply interOlist with L1 := L1 L2 := L2; Auto.
Qed.

Theorem interfMin:
  (L1, L2, L3:(list A))
  (Olist L1) -> (Olist L2) -> (Olist L3) -> (InclEq L3 L1) -> (InclEq L3 L2) ->
  (InclEq L3 (interf L1 L2)).
Intros L1 L2 L3 H' H'0 H'1 H'2 H'3.
Apply interMin with L1 := L1 L2 := L2; Auto.
Apply interfOlist; Auto.
Qed.

Theorem interfCom:
  (L1, L2:(list A)) (Olist L1) -> (Olist L2) ->
  (EqL (interf L1 L2) (interf L2 L1)).
Intros L1 L2 H' H'0.
Apply interCom with L1 := L1 L2 := L2; Auto.
Apply interfOlist; Auto.
Apply interfOlist; Auto.
Qed.
End OrderedList.

05/07/100, 11:37