# Library Sudoku.ListAux

Require Export List.
Require Export Arith.
Require Export Tactic.
Require Import Inverse_Image.
Require Import Wf_nat.

Section List.
Variables (A : Set) (B : Set) (C : Set).
Variable f : AB.

Theorem list_length_ind:
(P : list AProp),
( (l1 : list A),
( (l2 : list A), length l2 < length l1P l2) → P l1) →
(l : list A), P l.
intros P H l;
apply well_founded_ind with ( R := fun (x y : list A) ⇒ length x < length y );
auto.
apply wf_inverse_image with ( R := lt ); auto.
apply lt_wf.
Qed.

Definition list_length_induction:
(P : list ASet),
( (l1 : list A),
( (l2 : list A), length l2 < length l1P l2) → P l1) →
(l : list A), P l.
intros P H l;
apply well_founded_induction
with ( R := fun (x y : list A) ⇒ length x < length y ); auto.
apply wf_inverse_image with ( R := lt ); auto.
apply lt_wf.
Qed.

Theorem in_ex_app:
(a : A) (l : list A),
In a l → ( l1 : list A , l2 : list A , l = l1 ++ (a :: l2) ).
intros a l; elim l; clear l; simpl; auto.
intros H; case H.
intros a1 l H [H1|H1]; auto.
(nil (A:=A)); l; simpl; auto.
eq_tac; auto.
case H; auto; intros l1 [l2 Hl2]; (a1 :: l1); l2; simpl; auto.
eq_tac; auto.
Qed.

Theorem nth_nil: n (a: A), nth n nil a = a.
intros n; elim n; simpl; auto.
Qed.

Theorem in_ex_nth: (a b: A) l,
In a l n, n < length l a = nth n l b.
intros a b l; elim l; simpl; auto; clear l.
split; [intros H; case H | intros (k, (H, _))];
contradict H; auto with arith.
intros c l (Rec1, Rec2); split.
intros [H1 | H1]; subst.
0; auto with arith.
case Rec1; auto.
intros n (H2, H3); (S n); auto with arith.
intros tmp; case tmp; clear tmp.
intros n; case n; auto.
intros (H1, H2); auto.
intros n1 (H1, H2); right; apply Rec2.
n1; auto with arith.
Qed.

Theorem nth_app_l: i r (l1 l2: list A), i < length l1nth i (l1 ++ l2) r = nth i l1 r.
intros i r l1; generalize i; elim l1; simpl; auto; clear i l1.
intros i l2 H; contradict H; auto with arith.
intros a l Rec i; case i; simpl; auto with arith.
Qed.

Theorem nth_app_r: i r (l1 l2: list A), length l1 inth i (l1 ++ l2) r = nth (i - length l1) l2 r.
intros i r l1; generalize i; elim l1; simpl; auto; clear i l1.
intros; rewrite <- minus_n_O; auto.
intros a l Rec i; case i; simpl; auto with arith.
intros l2 HH; contradict HH; auto with arith.
Qed.

Theorem nth_default: i r (l: list A), length l inth i l r = r.
intros i r l; generalize i; elim l; clear i l; simpl; auto.
intros i; case i; auto.
intros a l Rec i; case i; auto with arith.
intros HH; contradict HH; auto with arith.
Qed.

Theorem list_nth_eq: (r: A) l1 l2,
length l1 = length l2
( n, nth n l1 r = nth n l2 r) → l1 = l2.
intros r l1; elim l1; simpl; auto; clear l1.
intros l2; case l2; clear l2; auto.
intros b l2 H; discriminate.
intros a l1 Rec l2; case l2; auto; clear l2.
intros H; discriminate.
intros b l2 H1 H2; eq_tac; auto; simpl in H1.
apply (H2 0); auto.
apply Rec; auto with arith.
intros n; generalize (H2 (S n)); simpl; auto.
Qed.

Theorem length_app:
(l1 l2 : list A), length (l1 ++ l2) = length l1 + length l2.
intros l1; elim l1; simpl; auto.
Qed.

(l1 l2 l3 : list A), l1 ++ l2 = l1 ++ l3l2 = l3.
intros l1; elim l1; simpl; auto.
intros a l H l2 l3 H0; apply H; injection H0; auto.
Qed.

Theorem app_inv_tail:
(l1 l2 l3 : list A), l2 ++ l1 = l3 ++ l1l2 = l3.
intros l1 l2; generalize l1; elim l2; clear l1 l2; simpl; auto.
intros l1 l3; case l3; auto.
intros b l H; absurd (length ((b :: l) ++ l1) length l1).
simpl; rewrite length_app; auto with arith.
rewrite <- H; auto with arith.
intros a l H l1 l3; case l3.
simpl; intros H1; absurd (length (a :: (l ++ l1)) length l1).
simpl; rewrite length_app; auto with arith.
rewrite H1; auto with arith.
simpl; intros b l0 H0; injection H0.
intros H1 H2; eq_tac; auto.
apply H with ( 1 := H1 ); auto.
Qed.

Theorem app_inv_app:
l1 l2 l3 l4 a,
l1 ++ l2 = l3 ++ (a :: l4)
( l5 : list A , l1 = l3 ++ (a :: l5) )
( l5 , l2 = l5 ++ (a :: l4) ).
intros l1; elim l1; simpl; auto.
intros l2 l3 l4 a H; right; l3; auto.
intros a l H l2 l3 l4 a0; case l3; simpl.
intros H0; left; l; eq_tac; injection H0; auto.
intros b l0 H0; case (H l2 l0 l4 a0); auto.
injection H0; auto.
intros [l5 H1].
left; l5; eq_tac; injection H0; auto.
Qed.

Theorem app_inv_app2:
l1 l2 l3 l4 a b,
l1 ++ l2 = l3 ++ (a :: (b :: l4))
( l5 : list A , l1 = l3 ++ (a :: (b :: l5)) )
(( l5 , l2 = l5 ++ (a :: (b :: l4)) )
l1 = l3 ++ (a :: nil) l2 = b :: l4).
intros l1; elim l1; simpl; auto.
intros l2 l3 l4 a b H; right; left; l3; auto.
intros a l H l2 l3 l4 a0 b; case l3; simpl.
case l; simpl.
intros H0; right; right; injection H0; split; auto.
eq_tac; auto.
intros b0 l0 H0; left; l0; injection H0; intros; (repeat eq_tac); auto.
intros b0 l0 H0; case (H l2 l0 l4 a0 b); auto.
injection H0; auto.
intros [l5 HH1]; left; l5; eq_tac; auto; injection H0; auto.
intros [H1|[H1 H2]]; auto.
right; right; split; auto; eq_tac; auto; injection H0; auto.
Qed.

Theorem same_length_ex:
(a : A) l1 l2 l3,
length (l1 ++ (a :: l2)) = length l3
( l4 ,
l5 ,
b : B ,
length l1 = length l4 (length l2 = length l5 l3 = l4 ++ (b :: l5)) ).
intros a l1; elim l1; simpl; auto.
intros l2 l3; case l3; simpl; (try (intros; discriminate)).
intros b l H; (nil (A:=B)); l; b; (repeat (split; auto)).
intros a0 l H l2 l3; case l3; simpl; (try (intros; discriminate)).
intros b l0 H0.
case (H l2 l0); auto.
intros l4 [l5 [b1 [HH1 [HH2 HH3]]]].
(b :: l4); l5; b1; (repeat (simpl; split; auto)).
eq_tac; auto.
Qed.

Theorem in_map_inv:
(b : B) (l : list A),
In b (map f l) → ( a : A , In a l b = f a ).
intros b l; elim l; simpl; auto.
intros tmp; case tmp.
intros a0 l0 H [H1|H1]; auto.
a0; auto.
case (H H1); intros a1 [H2 H3]; a1; auto.
Qed.

Theorem in_map_fst_inv:
a (l : list (B × C)),
In a (map (fst (B:=_)) l) → ( c , In (a, c) l ).
intros a l; elim l; simpl; auto.
intros H; case H.
intros a0 l0 H [H0|H0]; auto.
(snd a0); left; rewrite <- H0; case a0; simpl; auto.
case H; auto; intros l1 Hl1; l1; auto.
Qed.

Theorem length_map: l, length (map f l) = length l.
intros l; elim l; simpl; auto.
Qed.

Theorem map_app: l1 l2, map f (l1 ++ l2) = map f l1 ++ map f l2.
intros l; elim l; simpl; auto.
intros a l0 H l2; eq_tac; auto.
Qed.

Theorem map_length_decompose:
l1 l2 l3 l4,
length l1 = length l2
map f (app l1 l3) = app l2 l4map f l1 = l2 map f l3 = l4.
intros l1; elim l1; simpl; auto; clear l1.
intros l2; case l2; simpl; auto.
intros; discriminate.
intros a l1 Rec l2; case l2; simpl; clear l2; auto.
intros; discriminate.
intros b l2 l3 l4 H1 H2.
injection H2; clear H2; intros H2 H3.
case (Rec l2 l3 l4); auto.
intros H4 H5; split; auto.
eq_tac; auto.
Qed.

Theorem in_flat_map:
(l : list B) (f : Blist C) a b,
In a (f b) → In b lIn a (flat_map f l).
intros l g; elim l; simpl; auto.
intros a l0 H a0 b H0 [H1|H1]; apply in_or_app; auto.
left; rewrite H1; auto.
right; apply H with ( b := b ); auto.
Qed.

Theorem in_flat_map_ex:
(l : list B) (f : Blist C) a,
In a (flat_map f l) → ( b , In b l In a (f b) ).
intros l g; elim l; simpl; auto.
intros a H; case H.
intros a l0 H a0 H0; case in_app_or with ( 1 := H0 ); simpl; auto.
intros H1; a; auto.
intros H1; case H with ( 1 := H1 ).
intros b [H2 H3]; b; simpl; auto.
Qed.

End List.

Theorem length_list_prod:
(A : Set) (l1 l2 : list A),
length (list_prod l1 l2) = length l1 × length l2.
intros A l1 l2; elim l1; simpl; auto.
intros a l H; rewrite length_app; rewrite length_map; rewrite H; auto.
Qed.

Theorem in_list_prod_inv:
(A B : Set) a l1 l2,
In a (list_prod l1 l2) →
( b : A , c : B , a = (b, c) (In b l1 In c l2) ).
intros A B a l1 l2; elim l1; simpl; auto; clear l1.
intros H; case H.
intros a1 l1 H1 H2.
case in_app_or with ( 1 := H2 ); intros H3; auto.
case in_map_inv with ( 1 := H3 ); intros b1 [Hb1 Hb2]; auto.
a1; b1; split; auto.
case H1; auto; intros b1 [c1 [Hb1 [Hb2 Hb3]]].
b1; c1; split; auto.
Qed.

Definition list_eq_dec: A : Set,
( x y : A, {x = y} + {x y}) →
x y : list A, {x = y} + {x y}.
intros A dec; fix 2; intros x y; case x; case y.
left; auto.
intros; right; discriminate.
intros; right; discriminate.
intros b y1 a x1.
case (dec a b); intros H.
case (list_eq_dec x1 y1); intros H1.
left; apply f_equal2 with (f := @cons A); auto.
intros; right; contradict H1; injection H1; auto.
intros; right; contradict H; injection H; auto.
Defined.

Implicit Arguments list_eq_dec [A].

Definition In_dec:
A : Set,
( x y : A, {x = y} + {x y}) →
(a : A) (l : list A), {In a l} + {¬ In a l}.
intros A dec; fix 2; intros a l; case l.
right; simpl; intros H; case H.
intros b l1.
case (In_dec a l1); intros H1.
left; auto with datatypes.
case (dec a b); intros H2.
left; subst; auto with datatypes.
right; simpl; intros [H3|H3]; auto.
Defined.

Implicit Arguments In_dec [A].

Definition In_dec1:
(A: Set), ( x y : A, {x = y} + {x y}) →
(a : A) (l : list A),
{ll : list A × list A| l = fst ll ++ (a :: snd ll)} + {¬ In a l}.
intros A dec; fix 2; intros a l; case l.
right; simpl; intros tmp; case tmp.
intros b l1; case (In_dec1 a l1); intros H.
left; case H; intros ll HH; ((b :: fst ll), snd ll).
rewrite HH; auto with datatypes.
case (dec a b); intros H1.
left; (@nil A, l1); subst; auto.
right; simpl; intros [H2 | H2]; auto.
Defined.

Implicit Arguments In_dec1 [A].

Theorem in_fold_map: (A: Set) (f: natnatA) p l1 l2,
In p
(fold_right
(fun x l
map (f x) l1 ++ l) nil l2)
( x, ( y , In x l2 In y l1 p = f x y)).
intros A f p l1 l2; elim l2; simpl; auto; clear l2.
split; auto.
intros H; case H.
intros (x, (y, (H, _))); auto.
intros a l2 (Rec1, Rec2); split; intros H.
case in_app_or with (1 := H); clear H; intros H.
case (in_map_inv _ _ (f a) p l1); auto.
intros y (H1, H2).
a; y; repeat split; auto.
case Rec1; auto; clear Rec1 Rec2.
intros x (y, (U1, (U2, U3))); x; y; repeat split;
auto with arith.
case H; intros x (y, ([U1 | U1], (U2, U3))); subst; auto; clear H.
apply in_or_app; left; auto.
apply in_map; auto.
apply in_or_app; right; auto.
apply Rec2; auto; clear Rec1 Rec2.
x; y; repeat split; auto with arith.
Qed.