Library Stalmarck.OrderedListEq

Require Import Arith.
Require Export List.
Require Import Lexicographic_Exponentiation.
Require Export Relation_Definitions.
Require Export Relation_Operators.
Require Export Option.
Require Export sTactic.
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.
Casec Test; intros Test; auto.
right.
red in |- *; intros H'; absurd (eqA b a); auto.
Qed.
Hypothesis eqADec' : a b : A, {eqA a b} + {¬ eqA a b}.

Inductive Olist : list A Prop :=
| OlistNil : Olist nil
| OlistOne : a : A, Olist (a :: nil)
| OlistCons :
(a b : A) (L : list A),
Olist (b :: L) ltA a b Olist (a :: b :: L).
Hint Resolve OlistNil OlistOne OlistCons.

Theorem OlistInv : (a : A) (L : list A), Olist (a :: L) Olist L.
intros a L H'; inversion H'; auto.
Qed.

Theorem OlistSkip :
(a b : A) (L : list A), Olist (a :: b :: L) Olist (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 (a :: L) b : A, In b L ltA a b.
intros a L; elim L; simpl in |- *; auto.
intros H' b H'0; elim H'0.
intros a0 l H' H'0 b H'1; Elimc H'1; intros H'1; [ rewrite <- H'1 | idtac ];
auto.
inversion H'0; auto.
apply H'; auto.
apply OlistSkip with (b := a0); auto.
Qed.

Theorem OlistUnique :
(L : list A) (a b : A), Olist (a :: L) eqA a b ¬ In b L.
intros L a b H' H'0; red in |- *; 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 in |- *; auto.
intros a b H'; elim H'; auto.
intros a l H' a0 b H'0; Elimc H'0; intros H'0; [ rewrite <- H'0 | idtac ].
intros H'1; Casec 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; Elimc 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.

Inductive InEq : A list A Prop :=
| InEqHead : (a b : A) (L : list A), eqA a b InEq a (b :: L)
| InEqSkip : (a b : A) (L : list A), InEq a L InEq a (b :: L).

Definition InEqDec :
(a : A) (L1 : list A), {InEq a L1} + {¬ InEq a L1}.
fix 2.
intros a L1; case L1.
right; red in |- *; intros H'; inversion H'; auto.
intros a0 l; case (eqADec' a a0); intros Eqaa0.
left; auto.
case (InEqDec a l); intros REc.
left; auto.
right; red in |- *; 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 in |- *; auto.
intros H'; elim H'.
intros a0 l H' H'0; Elimc H'0; intros H'0; [ rewrite <- H'0 | idtac ]; auto.
Qed.

Theorem OlistSupEq :
(a : A) (L : list A),
Olist (a :: L) b : A, InEq b L ltA a b.
intros a L; elim L; simpl in |- *; 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 := a0 :: l); simpl in |- *; auto.
apply H'; auto.
apply OlistSkip with (b := a0); auto.
Qed.

Theorem OlistUniqueEq :
(L : list A) (a b : A), Olist (a :: L) eqA a b ¬ InEq b L.
intros L a b H' H'0; red in |- *; 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 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 in |- *; intros H'1; case H'; auto.
apply InEqComp with (a := b); auto.
Qed.

Inductive InclEq : list A list A Prop :=
InclEqDef :
L1 L2 : list A,
( a : A, InEq a L1 InEq a L2) InclEq L1 L2.
Hint 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 := 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.
Hint Resolve InclEqNil.

Theorem InclEqRef : L : list A, InclEq L L.
intros L.
apply InclEqDef; auto.
Qed.
Hint Resolve InclEqRef.

Theorem InclEqTrans : transitive (list A) InclEq.
red in |- ×.
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 (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.
Hint Resolve InclEqCons.

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 (a :: L1) (b :: L2).
Hint 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 eqATrans with (y := a0); auto.
Qed.

Theorem EqLRef : L : list A, EqL L L.
intros L; elim L; auto.
Qed.
Hint Resolve EqLRef.

Theorem EqLTrans : L : list A, transitive (list A) EqL.
intros L; red in |- ×.
intros x y z H'; generalize z; Elimc H'; clear 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 (a :: L1)
Olist (b :: L2) InclEq (a :: L1) (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 :=
fun L2 : list A
match L1 with
| nilNone _
| a :: L'1
match InEqDec a L2 with
| 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 in |- *; 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 in |- *; 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 in |- *; 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 (diffElem L1 L2) at -1 in |- *; case (diffElem L1 L2);
auto.
intros x H'2; 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 (diffElem L2 L1) at -1 in |- *; case (diffElem L2 L1);
auto.
intros x H'2; 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.

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 in |- *; intros H'2; absurd (InEq a L4); auto.
Qed.

Theorem DisjointInv1 :
(a : A) (L1 L2 : list A), Disjoint L1 (a :: L2) Disjoint L1 L2.
intros a L1 L2 H'; inversion H'; apply DisjointDef.
intros a0 H'0; red in |- *; intros H'1.
lapply (H a0); [ intros H'3; apply H'3 | idtac ]; auto.
Qed.

Theorem DisjointInv2 :
(a : A) (L1 L2 : list A), Disjoint (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 (b :: L2).
intros a L1 L2 H' H'0; inversion_clear H'.
apply DisjointDef; simpl in |- *; auto.
intros b H'1; red in |- *; 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 (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.

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 (a :: L1) (b :: L2) (a :: L3)
| appendLtA1 :
(a b : A) (L1 L2 L3 : list A),
ltA a b
append L1 (b :: L2) L3 append (a :: L1) (b :: L2) (a :: L3)
| appendLtA2 :
(a b : A) (L1 L2 L3 : list A),
ltA b a
append (a :: L1) L2 L3 append (a :: L1) (b :: L2) (b :: L3).
Hint 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 (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 in |- *; 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 in |- *; 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 in |- *; 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 in |- *; auto.
intros a b L4 L5 L6 H'0 H'1 H'2 m H'3; Elimc H'3; intros H'3;
[ rewrite <- H'3 | 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; Elimc H'3; intros H'3; 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; Elimc H'3; intros H'3; 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 in |- *; 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 in |- *; auto;
intros a b L4 L5 L6 H'0 H'1 H'2 a0 H'3 H'4 b0 H'5;
(Elimc H'5; intros H'5; [ rewrite <- H'5 | idtac ]);
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 := 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 in |- *; 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 := b :: L5) (L3 := a0 :: l); auto.
intros b0 H'5.
apply OlistSup with (L := L4); auto.
intros b0 H'5.
apply OlistSup with (L := b :: L5); auto.
simpl in |- *; 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 := a :: L4) (L2 := L5) (L3 := a0 :: l); auto.
intros b0 H'5.
apply OlistSup with (L := a :: L4); auto.
intros b0 H'5.
apply OlistSup with (L := L5); auto.
simpl in |- *; auto.
Qed.

Definition appendf :=
(fix aux1 (l1 l2 : list A) {struct l1} : list A :=
match l1, l2 with
| a :: t1, b :: t2
| inleft (left _) ⇒ a :: aux1 t1 (b :: t2)
| inleft (right _) ⇒
(fix aux2 (l3 : list A) : list A :=
match l3 with
| c :: t3
| inleft (left _) ⇒ a :: aux1 t1 (c :: t3)
| inleft (right _) ⇒ c :: aux2 t3
| inright _a :: aux1 t1 t3
end
| nila :: t1
end) (b :: t2)
| inright _a :: aux1 t1 t2
end
| nil, _l2
| _, nill1
end).

Theorem appendfAppend : L1 L2 : list A, append L1 L2 (appendf L1 L2).
intros L1; elim L1; simpl in |- ×.
intros L2; case L2; simpl in |- *; auto with datatypes.
intros a l H' L2; case L2; simpl in |- *; auto with datatypes.
intros a0 l0.
case (ltADec a a0); intros s; auto.
Casec s; intros s; auto.
apply appendLtA2; auto.
elim l0; auto.
intros a1 l1 H'0.
case (ltADec a a1); intros s1; auto.
Casec s1; intros s1; auto.
Qed.
Hint 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 in |- *; 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 in |- *; 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 in |- *; auto.
intros H'0.
apply DisjointDef; simpl in |- *; auto.
intros a l H'0 H'1.
apply DisjointCons1; auto.
apply H'0; auto.
intros a0 H'2; red in |- *; intros H'3.
lapply (H'1 a0); [ intros H'5; case H'5 | idtac ]; auto.
red in |- *; intros H'2.
lapply (H'1 (f a)); [ intros H'5; case H'5 | idtac ]; auto.
Qed.

Definition fappendf :=
(fix aux1 (l1 l2 : list A) {struct l1} : list A :=
match l1, l2 with
| a :: t1, b :: t2
| inleft (left _) ⇒ a :: aux1 t1 (b :: t2)
| inleft (right _) ⇒
(fix aux2 (l3 : list A) : list A :=
match l3 with
| c :: t3
| inleft (left _) ⇒ a :: aux1 t1 (c :: t3)
| inleft (right _) ⇒ f c :: aux2 t3
| inright _a :: aux1 t1 t3
end
| nila :: t1
end) (b :: t2)
| inright _a :: aux1 t1 t2
end
| nil, _map f l2
| _, nill1
end).

Theorem fappendfAppend :
L1 L2 : list A, append L1 (map f L2) (fappendf L1 L2).
intros L1; elim L1; simpl in |- ×.
intros L2; case L2; simpl in |- *; auto with datatypes.
intros a l H' L2; case L2; simpl in |- *; auto with datatypes.
intros a0 l0.
case (ltADec a a0); intros s; auto.
Casec s; intros s; auto.
apply appendLtA1; auto.
apply ltAeqAComp with (a := a) (b := a0); auto.
generalize (H' (a0 :: l0)); simpl in |- *; auto.
apply appendLtA2; auto.
apply ltAeqAComp with (a := a0) (b := a); auto.
elim l0; auto.
intros a1 l1 H'0.
case (ltADec a a1); intros s1; auto.
Casec s1; intros s1; auto.
simpl in |- ×.
apply appendLtA1; auto.
apply ltAeqAComp with (a := a) (b := a1); auto.
generalize (H' (a1 :: l1)); simpl in |- *; auto.
simpl in |- *; auto.
apply appendLtA2; auto.
apply ltAeqAComp with (a := a1) (b := a); auto.
simpl in |- ×.
apply appendEqA; auto.
apply eqATrans with a1; auto.
apply appendEqA; auto.
apply eqATrans with a0; auto.
Qed.
Hint 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.

Definition getMin :=
(fix aux1 (l1 l2 : list A) {struct l1} : Option A :=
match l1, l2 with
| a :: t1, b :: t2
| inleft (left _) ⇒ aux1 t1 (b :: t2)
| inleft (right _) ⇒
(fix aux2 (l3 : list A) : Option A :=
match l3 with
| c :: t3
| inleft (left _) ⇒ aux1 t1 (c :: t3)
| inleft (right _) ⇒ aux2 t3
| inright H
match testDec a c H with
| left _Some A a
| right __aux2 t3
end
end
| nilNone A
end) (b :: t2)
| inright H
match testDec a b H with
| left _Some A a
| right _aux1 t1 t2
end
end
| nil, _None A
| _, nilNone A
end).

Theorem geMinIn :
(L1 L2 : list A) (a : A),
Olist L1 Olist L2 getMin L1 L2 = Some _ a In a L1.
intros L1; elim L1; simpl in |- ×.
intros L2; case L2; simpl in |- *; auto with datatypes.
intros a H' H'0 H'1; discriminate.
intros a l a0 H' H'0 H'1; discriminate.
intros a l H' L2; case L2; simpl in |- *; auto with datatypes.
intros a0 H'0 H'1 H'2; discriminate.
intros a0 l0 a1 H'0 H'1.
case (ltADec a a0); intros s; auto.
Casec s; intros s; auto.
intros H'2; right.
apply (H' (a0 :: l0)); auto.
apply OlistInv with (a := a); auto.
generalize H'1; elim l0; auto.
intros H'2 H'3; discriminate.
intros a2 l1 H'2 H'3.
case (ltADec a a2); intros s1; auto.
Casec s1; intros s1; auto.
intros H'4; right.
apply (H' (a2 :: l1)); auto.
apply OlistInv with (a := a); auto.
apply OlistInv with (a := a0); auto.
intros H'4; case H'2; auto.
apply OlistSkip with (b := a2); auto.
case (testDec a a2 s1); auto.
intros H'4 H'5; inversion H'5; auto.
intros H'4 H'5; case H'2; auto.
apply OlistSkip with (b := a2); auto.
case (testDec a a0 s); auto.
intros H'2 H'3; inversion H'3; auto.
intros H'2 H'3; right.
apply (H' l0); auto.
apply OlistInv with (a := a); auto.
apply OlistInv with (a := a0); auto.
Qed.

Theorem getMinComp :
(L1 L2 : list A) (a : A),
Olist L1
Olist L2 getMin L1 L2 = Some _ a b : A, test a b In b L2.
intros L1; elim L1; simpl in |- ×.
intros L2; case L2; simpl in |- *; auto with datatypes.
intros a H' H'0 H'1; discriminate.
intros a l a0 H' H'0 H'1; discriminate.
intros a l H' L2; case L2; simpl in |- *; auto with datatypes.
intros a0 H'0 H'1 H'2; discriminate.
intros a0 l0 a1 H'0 H'1.
case (ltADec a a0); intros s; auto.
Casec s; intros s; auto.
intros H'2; case (H' (a0 :: l0) a1); auto.
apply OlistInv with (a := a); auto.
intros x H'3; elim H'3; intros H'4 H'5; x; auto.
generalize H'1; elim l0; auto.
intros H'2 H'3; discriminate.
intros a2 l1 H'2 H'3.
case (ltADec a a2); intros s1; auto.
Casec s1; intros s1; auto.
intros H'4; case (H' (a2 :: l1) a1); auto.
apply OlistInv with (a := a); auto.
apply OlistInv with (a := a0); auto.
intros x H'5; elim H'5; intros H'6 H'7; x; auto.
intros H'4; case H'2; auto.
apply OlistSkip with (b := a2); auto.
intros x H'5; elim H'5; intros H'6 H'7; x; intuition.
case (testDec a a2 s1); auto.
intros H'4 H'5; inversion H'5; auto.
a2; split; auto with datatypes.
rewrite <- H0; auto.
intros H'4 H'5; case H'2; auto.
apply OlistSkip with (b := a2); auto.
intros x H'6; elim H'6; intros H'7 H'8; x; split; auto with datatypes;
case H'8; auto with datatypes.
case (testDec a a0 s); auto.
intros H'2 H'3; inversion H'3; auto.
a0; split; auto with datatypes.
rewrite <- H0; auto.
intros H'2 H'3; case (H' l0 a1); auto.
apply OlistInv with (a := a); auto.
apply OlistInv with (a := a0); auto.
intros x H'4; elim H'4; intros H'5 H'6; x; auto.
Qed.

Theorem getMinMin :
(L1 L2 : list A) (a : 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 L1; elim L1; simpl in |- ×.
intros L2; case L2; simpl in |- *; auto with datatypes.
intros a l H' L2; case L2; simpl in |- *; auto with datatypes.
intros a0 l0 a1 H'0 H'1.
case (ltADec a a0); intros s; auto.
Casec s; intros s; auto.
intros H'2 b c H'3 H'4 H'5; Casec H'4; intros H'4; auto.
rewrite <- H'4; auto.
red in |- *; intros H'6; absurd (In c (a0 :: l0)); auto.
apply OlistUnique with (a := a); auto.
apply (H' (a0 :: l0) a1); auto.
apply OlistInv with (a := a); auto.
generalize H'1; elim l0; auto.
intros H'2 H'3; discriminate.
intros a2 l1 H'2 H'3.
case (ltADec a a2); intros s1; auto.
Casec s1; intros s1; auto.
intros H'4 b c H'5 H'6 H'7; Casec H'6; intros H'6; auto.
rewrite <- H'6; auto.
Elimc H'7; intros H'7; [ rewrite <- H'7 | idtac ]; auto.
red in |- *; intros H'8; absurd (eqA a0 a); auto.
red in |- *; intros H'8; absurd (In c (a2 :: l1)); auto.
apply OlistUnique with (a := a); auto.
apply OlistCons; auto.
apply OlistInv with (a := a0); auto.
Elimc H'7; intros H'7; [ rewrite <- H'7 | idtac ]; auto.
red in |- *; intros H'8; Contradict H'6; auto.
apply OlistUnique with (a := a0); auto.
apply OlistSkip with (b := a); auto.
apply (H' (a2 :: l1) a1); auto.
apply OlistInv with (a := a); auto.
apply OlistInv with (a := a0); auto.
simpl in |- *; intros H'4 b c H'5 H'6 H'7; auto.
Casec H'7; intros H'7; auto.
apply (H'2 (OlistSkip _ _ _ H'3) H'4); auto.
Casec H'7; intros H'7; auto.
rewrite <- H'7.
Elimc H'6; intros H'6; [ rewrite <- H'6 | idtac ]; auto.
red in |- *; intros H'8; absurd (eqA a2 a); auto.
apply OlistUnique with (a := a2); auto.
apply OlistSkip with (b := a); auto.
apply (H'2 (OlistSkip _ _ _ H'3) H'4); auto.
case (testDec a a2 s1); auto.
intros H'4 H'5; inversion H'5; auto.
rewrite <- H0.
intros b c H'6 H'7 H'8; absurd (In b (a :: l)); auto.
apply OlistUnique with (a := b); auto.
intros H'4 H'5 b c H'6 H'7 H'8.
Elimc H'8; simpl in |- *; intros H'8.
apply (H'2 (OlistSkip _ _ _ H'3) H'5); auto.
Elimc H'8; simpl in |- *; intros H'8.
rewrite <- H'8.
Elimc H'7; intros H'7; [ rewrite <- H'7 | idtac ]; auto.
apply OlistUnique with (a := a); auto.
apply eqATrans with a2; auto.
apply (H'2 (OlistSkip _ _ _ H'3) H'5); auto.
case (testDec a a0 s); auto.
intros H'2 H'3; inversion H'3.
intros b c H'4 H'5 H'6.
Elimc H'5; intros H'5; [ rewrite <- H'5 in H'4; Contradict H'4 | idtac ];
auto.
Elimc H'6; intros H'6; [ rewrite <- H'6 | idtac ]; auto.
apply OlistUnique with (a := a); auto.
apply eqATrans with a0; auto.
apply OlistUnique with (a := b); auto.
apply OlistSkip with (b := a1); auto.
apply OlistCons; auto.
rewrite <- H0; auto.
intros H'2 H'3 b c H'4 H'5 H'6.
Elimc H'6; intros H'6; [ rewrite <- H'6 | idtac ]; auto.
Elimc H'5; intros H'5; [ rewrite <- H'5 | idtac ]; auto.
apply OlistUnique with (a := a); auto.
apply eqATrans with a0; auto.
Elimc H'5; intros H'5; [ rewrite <- H'5 | idtac ]; auto.
apply OlistUnique with (a := a0); auto.
apply eqATrans with a; auto.
apply (H' l0 a1); auto.
apply OlistInv with (a := a); auto.
apply OlistInv with (a := a0); auto.
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; elim L1; simpl in |- ×.
intros L2; case L2; simpl in |- *; auto with datatypes.
intros a l H' L2; case L2; simpl in |- *; auto with datatypes.
intros a0 l0 a1 H'0.
case (ltADec a a0); intros s; auto.
Casec s; intros s; auto.
intros H'1 a2 b H'2; Elimc H'2; intros H'2; [ rewrite <- H'2 | idtac ]; auto.
intros H'3; red in |- *; intros H'4; absurd (In b (a0 :: l0)); auto.
apply OlistUnique with (a := a); auto.
intros H'3; apply (H' (a0 :: l0)); auto.
apply OlistInv with (a := a); auto.
generalize H'0; elim l0; auto.
intros H'1 H'2 a2 b H'3 H'4; Elimc H'4; intros H'4;
[ rewrite <- H'4 | idtac ]; auto.
Elimc H'3; intros H'3; [ rewrite <- H'3 | idtac ].
red in |- *; intros H'5; absurd (eqA a0 a); auto.
apply OlistUnique with (a := a0); auto.
apply OlistSkip with (b := a); auto.
intros a2 l1 H'1 H'2.
case (ltADec a a2); intros s1; auto.
Casec s1; intros s1; auto.
intros H'3 a3 b H'4; Elimc H'4; intros H'4; [ rewrite <- H'4 | idtac ]; auto.
intros H'5; Elimc H'5; intros H'5; [ rewrite <- H'5 | idtac ]; auto.
red in |- *; intros H'6; absurd (eqA a0 a); auto.
apply OlistUnique with (a := a); auto.
apply OlistCons; auto.
apply OlistInv with (a := a0); auto.
intros H'5; Elimc H'5; intros H'5; [ rewrite <- H'5 | idtac ].
apply OlistUnique with (a := a0); auto.
apply OlistSkip with (b := a); auto.
apply (H' (a2 :: l1)); auto.
apply OlistInv with (a := a); auto.
apply OlistInv with (a := a0); auto.
intros H'3 a3 b H'4 H'5.
Elimc H'5; simpl in |- *; intros H'5; [ rewrite <- H'5 | idtac ]; auto.
apply H'1; auto.
apply OlistSkip with (b := a2); auto.
Elimc H'5; intros H'5; [ rewrite <- H'5 | idtac ]; auto.
Elimc H'4; intros H'4; [ rewrite <- H'4 | idtac ].
red in |- *; intros H'6; absurd (eqA a2 a); auto.
apply OlistUnique with (a := a2); auto.
apply OlistSkip with (b := a); auto.
apply H'1; auto.
apply OlistSkip with (b := a2); auto.
case (testDec a a2 s1); auto.
intros H'3 H'4; discriminate.
intros H'3 H'4 a3 b H'5 H'6.
Elimc H'6; simpl in |- *; intros H'6; [ rewrite <- H'6 | idtac ].
Elimc H'5; intros H'5; [ rewrite <- H'5 | idtac ].
red in |- *; intros H'7; absurd (eqA a0 a); auto.
apply OlistUnique with (a := a0); auto.
apply OlistSkip with (b := a); auto.
Elimc H'6; intros H'6; [ rewrite <- H'6 | idtac ].
Elimc H'5; intros H'5; [ rewrite <- H'5 | idtac ]; auto.
apply OlistUnique with (a := a); auto.
apply eqATrans with a2; auto.
apply H'1; auto.
apply OlistSkip with (b := a2); auto.
case (testDec a a0 s); auto.
intros H'1 H'2; discriminate.
intros H'1 H'2 a2 b H'3; Elimc H'3; intros H'3; [ rewrite <- H'3 | idtac ];
auto.
intros H'4; Elimc H'4; intros H'4; [ rewrite <- H'4 | idtac ]; auto.
apply OlistUnique with (a := a0); auto.
apply eqATrans with a; auto.
intros H'4; Elimc H'4; intros H'4; [ rewrite <- H'4 | idtac ].
apply OlistUnique with (a := a); auto.
apply eqATrans with a0; auto.
apply (H' l0); auto.
apply OlistInv with (a := a); auto.
apply OlistInv with (a := a0); auto.
Qed.

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 (a :: L1) (b :: L2) (a :: L3)
| interLtA1 :
(a b : A) (L1 L2 L3 : list A),
ltA a b inter L1 (b :: L2) L3 inter (a :: L1) (b :: L2) L3
| interLtA2 :
(a b : A) (L1 L2 L3 : list A),
ltA b a inter (a :: L1) L2 L3 inter (a :: L1) (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 in |- *; auto;
intros a b L4 L5 L6 H'0 H'1 H'2 a0 H'3 H'4 b0 H'5;
(Elimc H'5; intros H'5; [ rewrite <- H'5 | idtac ]);
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 := 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 in |- *; 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 (a :: L).
intros a L; elim L; auto.
intros H'; inversion H'; auto.
intros a0 l H' H'0; inversion H'0; auto.
red in |- *; intros H'1; inversion H'1; auto.
absurd (eqA a a0); auto.
red in |- *; 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 (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 := 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 (a :: L1) (b :: L2)
Olist (a :: L1)
Olist (b :: L2) InclEq (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.
Casec Eqab; intros Eqab.
absurd (Olist (a :: 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 (a0 :: 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.
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 (a0 :: 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 (a0 :: 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 interf :=
(fix aux1 (l1 l2 : list A) {struct l1} : list A :=
match l1, l2 with
| a :: t1, b :: t2
| inleft (left _) ⇒ aux1 t1 (b :: t2)
| inleft (right _) ⇒
(fix aux2 (l3 : list A) : list A :=
match l3 with
| c :: t3
| inleft (left _) ⇒ aux1 t1 (c :: t3)
| inleft (right _) ⇒ aux2 t3
| inright _a :: aux1 t1 t3
end
| nilnil
end) (b :: t2)
| inright _a :: aux1 t1 t2
end
| nil, _nil
| _, nilnil
end).

Theorem interfProp1 : L1 L2 : list A, inter L1 L2 (interf L1 L2).
intros L1; elim L1; simpl in |- ×.
intros L2; case L2; simpl in |- *; intros; apply interNil2; auto.
intros a l H' L2; case L2; simpl in |- *; auto with datatypes.
apply interNil1; auto.
intros a0 l0.
case (ltADec a a0); intros s; [ Casec s; intros s | idtac ].
apply interLtA1; auto.
apply interLtA2; auto.
elim l0; auto.
apply interNil1; auto.
intros a1 l1 H'0.
case (ltADec a a1); intros s1; [ Casec s1; intros s1 | idtac ].
apply interLtA1; auto.
apply interLtA2; auto.
apply interEqA; auto.
apply interEqA; auto.
Qed.
Hint 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.