# Library Util

Require Import Utf8 List.
Require Import DLib.

Set Implicit Arguments.

Section INV.

Variables A B C : Type.

Definition some_eq_inv (x y: A) :
Some x = Some y x = y :=
λ H, match H with eq_refleq_refl _ end.

Lemma None_not_Some (v: A) :
None = Some v X : Prop, X.

Lemma false_eq_true_False : false true.

Lemma false_not_true : false = true P : Prop, P.

Definition pair_eq_inv (x:A) (y:B) z w :
(x,y) = (z,w) x = z y = w :=
λ H, match H with eq_reflconj eq_refl eq_refl end.

Definition triple_eq_inv (x: A) (y: B) (z: C) x' y' z' :
(x,y,z) = (x',y',z') (x = x' y = y') z = z' :=
λ H, match H with eq_reflconj (pair_eq_inv eq_refl) eq_refl end.

Definition cons_eq_inv (x x': A) (l l': list A) :
x :: l = x' :: l' x = x' l = l' :=
λ H, match H in _ = a return match a with nilTrue | y :: mx = y l = m end with eq_reflconj eq_refl eq_refl end.

Definition cons_nil_inv (x : A) (l: list A) :
x :: l = nil P : Prop, P :=
λ H, match H in _ = a return match a with nil P, P | _True end with eq_reflI end.

Definition eq_dec_of_beq (beq: A A bool) (beq_correct: a b : A, beq a b = true a = b)
(x y: A) : { x = y } + { x y } :=
(if beq x y as b return (b = true x = y) { x = y } + { x y }
then λ H, left (proj1 H eq_refl)
else λ H, right (λ K, false_eq_true_False (proj2 H K)))
(beq_correct x y).

End INV.

Ltac eq_some_inv :=
repeat match goal with
| H : @None _ = Some _ |- _
exact (None_not_Some H _)
| H : Some _ = @None _ |- _
exact (None_not_Some (eq_sym H) _)
| H : Some ?a = Some ?b |- _
apply (@some_eq_inv _ a b) in H
| H : _ :: _ = @nil _ |- _
exact (cons_nil_inv H _)
| H : @nil = _ :: _ |- _
exact (cons_nil_inv (eq_sym H) _)
| H : false = true |- _
exact (false_not_true H _)
| H : true = false |- _
exact (false_not_true (eq_sym H) _)
| H : (_, _) = (_, _) |- _
destruct (pair_eq_inv H); clear H
end.

Notation "'do_opt' X <- A ; B" :=
(match A with Some XB | NoneNone end)
(at level 200, X ident, A at level 100, B at level 200).

Definition option_bind A B (a: option A) (f: A option B) : option B :=
match a with Some af a | _None end.

Lemma fold_left_ext_m {A B} (f g: A B A) :
( u v, f u v = g u v)
l z, fold_left f l z = fold_left g l z.

Section MAPS.

Variables A B C D : Type.

Variable e : A B.
Variable f : A B C.
Variable g : A B C D.

Definition rev_map_app (l: list A) (acc: list B) : list B :=
fold_left (λ acc a, e a :: acc) l acc.

Definition rev_map (l: list A) : list B :=
rev_map_app l nil.

Lemma rev_map_app_correct : l l', rev_map_app l l' = rev (map e l) ++ l'.

Lemma rev_map_correct : l, rev_map l = rev (map e l).

Lemma rev_nil : l : list A, rev l = nil l = nil.

Definition map' (l: list A) : list B :=
rev' (fold_left (λ acc a, e a :: acc) l nil).

Lemma map'_correct : l, map' l = map e l.

Definition map2 (l: list A) (m: list B) : list C :=
fold_left (λ acc a, fold_left (λ acc b, f a b :: acc) m acc) l nil.

Definition map2_spec (l: list A) (m: list B) : list C :=
rev (flat_map (λ a, map (f a) m) l).

Lemma map2_correct : l m, map2 l m = map2_spec l m.

Corollary in_map2 l m a b :
In a l In b m In (f a b) (map2 l m).

Lemma map_cons_inv l b b' :
map e l = b :: b'
a a', l = a :: a' b = e a map e a' = b'.

Lemma map_nil_inv l :
map e l = nil l = nil.

End MAPS.

Lemma map2_nil_inv A B C (f: A B C) l m :
map2 f l m = nil l = nil m = nil.

Section FOLD2.
Fold on two lists. The weak version ignores trailing elements of the longest list.
Context (A B C: Type)
(f: C A B C)
(ka: C list A C)
(kb: C list B C).

Fixpoint fold_left2_weak (la: list A) (lb: list B) (acc: C) {struct la} : C :=
match la, lb with
| a :: la, b :: lbfold_left2_weak la lb (f acc a b)
| nil, _
| _, nilacc
end.

Fixpoint fold_left2 (la: list A) (lb: list B) (acc: C) {struct la} : C :=
match la, lb with
| a :: la, b :: lbfold_left2 la lb (f acc a b)
| nil, nilacc
| la, nilka acc la
| nil, lbkb acc lb
end.

End FOLD2.