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_refl ⇒ eq_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_refl ⇒ conj 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_refl ⇒ conj (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 nil ⇒ True | y :: m ⇒ x = y ∧ l = m end with eq_refl ⇒ conj 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_refl ⇒ I 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 X ⇒ B | None ⇒ None 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 a ⇒ f 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.
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_refl ⇒ eq_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_refl ⇒ conj 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_refl ⇒ conj (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 nil ⇒ True | y :: m ⇒ x = y ∧ l = m end with eq_refl ⇒ conj 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_refl ⇒ I 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 X ⇒ B | None ⇒ None 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 a ⇒ f 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 :: lb ⇒ fold_left2_weak la lb (f acc a b)
| nil, _
| _, nil ⇒ acc
end.
Fixpoint fold_left2 (la: list A) (lb: list B) (acc: C) {struct la} : C :=
match la, lb with
| a :: la, b :: lb ⇒ fold_left2 la lb (f acc a b)
| nil, nil ⇒ acc
| la, nil ⇒ ka acc la
| nil, lb ⇒ kb acc lb
end.
End FOLD2.
(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 :: lb ⇒ fold_left2_weak la lb (f acc a b)
| nil, _
| _, nil ⇒ acc
end.
Fixpoint fold_left2 (la: list A) (lb: list B) (acc: C) {struct la} : C :=
match la, lb with
| a :: la, b :: lb ⇒ fold_left2 la lb (f acc a b)
| nil, nil ⇒ acc
| la, nil ⇒ ka acc la
| nil, lb ⇒ kb acc lb
end.
End FOLD2.