Lvc.Infra.MoreList
Lemma app_nil_eq X (L:list X) xl
: L = xl ++ L → xl = nil.
Lemma cons_app X (x:X) xl
: x::xl = (x::nil)++xl.
Fixpoint tabulate X (x:X) n : list X :=
match n with
| 0 ⇒ nil
| S n ⇒ x::tabulate x n
end.
Section ParametricZip.
Variables X Y Z : Type.
Hypothesis f : X → Y → Z : Type.
Fixpoint zip (L:list X) (L´:list Y) : list Z :=
match L, L´ with
| x::L, y::L´ ⇒ f x y::zip L L´
| _, _ ⇒ nil
end.
Lemma zip_get L L´ n (x:X) (y:Y)
: get L n x → get L´ n y → get (zip L L´) n (f x y).
Lemma get_zip L L´ n (z:Z)
: get (zip L L´) n z
→ { x : X & {y : Y | get L n x ∧ get L´ n y ∧ f x y = z } } .
Lemma zip_tl L L´
: tl (zip L L´) = zip (tl L) (tl L´).
End ParametricZip.
Lemma map_zip X Y Z (f: X → Y → Z) W (g: Z → W) L L´
: map g (zip f L L´) = zip (fun x y ⇒ g (f x y)) L L´.
Lemma zip_map_l X Y Z (f: X → Y → Z) W (g: W → X) L L´
: zip f (map g L) L´ = zip (fun x y ⇒ f (g x) y) L L´.
Lemma zip_map_r X Y Z (f: X → Y → Z) W (g: W → Y) L L´
: zip f L (map g L´) = zip (fun x y ⇒ f x (g y)) L L´.
Lemma zip_ext X Y Z (f f´:X → Y → Z) L L´
: (∀ x y, f x y = f´ x y) → zip f L L´ = zip f´ L L´.
Lemma zip_length X Y Z (f:X→Y→Z) L L´
: length (zip f L L´) = min (length L) (length L´).
Lemma zip_length2 {X Y Z} {f:X→Y→Z} DL ZL
: length DL = length ZL
→ length (zip f DL ZL) = length DL.
Section ParametricMapIndex.
Variables X Y : Type.
Hypothesis f : nat → X → Y : Type.
Fixpoint mapi_impl (n:nat) (L:list X) : list Y :=
match L with
| x::L ⇒ f n x::mapi_impl (S n) L
| _ ⇒ nil
end.
Definition mapi := mapi_impl 0.
Lemma mapi_get_impl L i y n
: getT (mapi_impl i L) n y → { x : X & (getT L n x × (f (n+i) x = y))%type }.
Lemma mapi_get L n y
: get (mapi L) n y → { x : X | get L n x ∧ f n x = y }.
Lemma mapi_length L {n}
: length (mapi_impl n L) = length L.
End ParametricMapIndex.
Lemma map_impl_mapi X Y Z L {n} (f:nat→X→Y) (g:Y→Z)
: List.map g (mapi_impl f n L) = mapi_impl (fun n x ⇒ g (f n x)) n L.
Lemma map_mapi X Y Z L (f:nat→X→Y) (g:Y→Z)
: List.map g (mapi f L) = mapi (fun n x ⇒ g (f n x)) L.
Lemma mapi_map_ext X Y L (f:nat→X→Y) (g:X→Y) n
: (∀ x n, g x = f n x)
→ List.map g L = mapi_impl f n L.
Lemma map_ext_get_eq X Y L (f:X→Y) (g:X→Y)
: (∀ x n, get L n x → g x = f x)
→ List.map g L = List.map f L.
Lemma map_ext_get X Y (R:Y → Y → Prop) L (f:X→Y) (g:X→Y)
: (∀ x n, get L n x → R (g x) (f x))
→ PIR2 R (List.map g L) (List.map f L).
Ltac list_eqs :=
match goal with
| [ H´ : ?x :: ?L = ?L´ ++ ?L |- _ ] ⇒
rewrite cons_app in H´; eapply app_inv_tail in H´
| [ H : ?L = ?L´ ++ ?L |- _ ] ⇒
let A := fresh "A" in
eapply app_nil_eq in H
| _ ⇒ fail "no matching assumptions"
end.
Ltac inv_map H :=
match type of H with
| get (List.map ?f ?L) ?n ?x ⇒
match goal with
| [H´ : get ?L ?n ?y |- _ ] ⇒
let EQ := fresh "EQ" in pose proof (map_get f H´ H) as EQ; invc EQ
| _ ⇒ let X := fresh "X" in let EQ := fresh "EQ" in
pose proof (map_get_4 _ f H) as X; destruct X as [? [? EQ]]; invc EQ
end
end.
Lemma list_eq_get {X:Type} (L L´:list X) eqA n x
: list_eq eqA L L´ → get L n x → ∃ x´, get L´ n x´ ∧ eqA x x´.
Instance list_R_dec A (R:A→A→Prop)
`{∀ a b, Computable (R a b)} (L:list A) (L´:list A) :
Computable (∀ n a b, get L n a → get L´ n b → R a b).
Instance list_eq_computable X (R:X → X→ Prop) `{∀ x y, Computable (R x y)}
: ∀ (L L´:list X), Computable (list_eq R L L´).
Ltac inv_mapi H :=
match type of H with
| get (mapi ?f ?L) ?n ?x ⇒
match goal with
| [H´ : get ?L ?n ?y |- _ ] ⇒
let EQ := fresh "EQ" in pose proof (mapi_get f H´ H) as EQ; invc EQ
| _ ⇒ let X := fresh "X" in let EQ := fresh "EQ" in
pose proof (mapi_get f _ H) as X; destruct X as [? [? EQ]]; invc EQ;
clear_trivial_eqs
end
end.
Instance list_get_computable X (Y:list X) (R:X→Prop) `{∀ (x:X), Computable (R x)}
: Computable (∀ n y, get Y n y → R y).