Built with Alectryon, running Coq+SerAPI v8.16.0+0.16.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
From Tealeaves Require Export
Classes.Monoid
Classes.Categorical.Applicative
Classes.Categorical.Monad
Classes.Categorical.ShapelyFunctor
Classes.Kleisli.TraversableFunctor
Functors.Early.Batch.From Tealeaves.Functors Require Import
Early.List
Constant
VectorRefinement.Import Early.Batch.Notations.Import Monoid.Notations.Import Applicative.Notations.Import Kleisli.TraversableFunctor.Notations.Import VectorRefinement.Notations.#[local] Generalizable Variablesψ ϕ W F G M A B C D X Y O.#[local] Arguments map F%function_scope {Map} {A B}%type_scope f%function_scope _.#[local] Arguments ret T%function_scope {Return} (A)%type_scope _.#[local] Arguments pure F%function_scope {Pure} {A}%type_scope _.#[local] Arguments mult F%function_scope {Mult} {A B}%type_scope _.(** * <<mapReduce>> Rewriting Lemmas *)(******************************************************************************)SectionBatch_mapReduce_rewriting.Context {ABC: Type}.
A, B, C: Type
forall (M : Type) (op : Monoid_op M)
(unit0 : Monoid_unit M),
Monoid M ->
forall (f : A -> M) (a : A)
(rest : Batch A B (B -> C)),
mapReduce f (rest ⧆ a) = mapReduce f rest ● f a
A, B, C: Type
forall (M : Type) (op : Monoid_op M)
(unit0 : Monoid_unit M),
Monoid M ->
forall (f : A -> M) (a : A)
(rest : Batch A B (B -> C)),
mapReduce f (rest ⧆ a) = mapReduce f rest ● f a
A, B, C, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M a: A rest: Batch A B (B -> C)
mapReduce f (rest ⧆ a) = mapReduce f rest ● f a
A, B, C, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M a: A rest: Batch A B (B -> C)
traverse f (rest ⧆ a) = traverse f rest ● f a
A, B, C, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M a: A rest: Batch A B (B -> C)
map (const M) Step (traverse f rest) <⋆> f a =
traverse f rest ● f a
reflexivity.Qed.EndBatch_mapReduce_rewriting.(** ** <<mapReduce>> Rewriting for << <⋆> >> *)(******************************************************************************)
A, B, C, C': Type
forall (M : Type) (op : Monoid_op M)
(unit0 : Monoid_unit M),
Monoid M ->
forall (f : A -> M) (g : C -> C') (b : Batch A B C),
mapReduce f b = mapReduce f (map (Batch A B) g b)
A, B, C, C': Type
forall (M : Type) (op : Monoid_op M)
(unit0 : Monoid_unit M),
Monoid M ->
forall (f : A -> M) (g : C -> C') (b : Batch A B C),
mapReduce f b = mapReduce f (map (Batch A B) g b)
A, B, C, C', M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M g: C -> C' b: Batch A B C
mapReduce f b = mapReduce f (map (Batch A B) g b)
A, B, C, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M b: Batch A B C
forall (C' : Type) (g : C -> C'),
mapReduce f b = mapReduce f (map (Batch A B) g b)
A, B, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M C: Type c: C C': Type g: C -> C'
mapReduce f (Done c) =
mapReduce f (map (Batch A B) g (Done c))
A, B, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M C: Type b: Batch A B (B -> C) a: A IHb: forall (C' : Type) (g : (B -> C) -> C'),
mapReduce f b =
mapReduce f (map (Batch A B) g b) C': Type g: C -> C'
mapReduce f (b ⧆ a) =
mapReduce f (map (Batch A B) g (b ⧆ a))
A, B, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M C: Type c: C C': Type g: C -> C'
mapReduce f (Done c) =
mapReduce f (map (Batch A B) g (Done c))
reflexivity.
A, B, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M C: Type b: Batch A B (B -> C) a: A IHb: forall (C' : Type) (g : (B -> C) -> C'),
mapReduce f b =
mapReduce f (map (Batch A B) g b) C': Type g: C -> C'
mapReduce f (b ⧆ a) =
mapReduce f (map (Batch A B) g (b ⧆ a))
A, B, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M C: Type b: Batch A B (B -> C) a: A IHb: forall (C' : Type) (g : (B -> C) -> C'),
mapReduce f b =
mapReduce f (map (Batch A B) g b) C': Type g: C -> C'
mapReduce f b ● f a =
mapReduce f (map (Batch A B) g (b ⧆ a))
A, B, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M C: Type b: Batch A B (B -> C) a: A IHb: forall (C' : Type) (g : (B -> C) -> C'),
mapReduce f b =
mapReduce f (map (Batch A B) g b) C': Type g: C -> C'
mapReduce f b ● f a =
mapReduce f (map (Batch A B) (compose g) b ⧆ a)
A, B, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M C: Type b: Batch A B (B -> C) a: A IHb: forall (C' : Type) (g : (B -> C) -> C'),
mapReduce f b =
mapReduce f (map (Batch A B) g b) C': Type g: C -> C'
mapReduce f b ● f a =
mapReduce f (map (Batch A B) (compose g) b) ● f a
A, B, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M C: Type b: Batch A B (B -> C) a: A C': Type g: C -> C' IHb: mapReduce f b =
mapReduce f (map (Batch A B) (compose g) b)
mapReduce f b ● f a =
mapReduce f (map (Batch A B) (compose g) b) ● f a
A, B, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M C: Type b: Batch A B (B -> C) a: A C': Type g: C -> C' IHb: mapReduce f b =
mapReduce f (map (Batch A B) (compose g) b)
mapReduce f (map (Batch A B) (compose g) b) ● f a =
mapReduce f (map (Batch A B) (compose g) b) ● f a
reflexivity.Qed.
A, B, C, D, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M
forall (c : C) (b2 : Batch A B D),
mapReduce f (Done c ⊗ b2) = mapReduce f b2
A, B, C, D, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M
forall (c : C) (b2 : Batch A B D),
mapReduce f (Done c ⊗ b2) = mapReduce f b2
A, B, C, D, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M c: C b2: Batch A B D
mapReduce f (Done c ⊗ b2) = mapReduce f b2
A, B, C, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M c: C C0: Type c0: C0
mapReduce f (Done c ⊗ Done c0) = mapReduce f (Done c0)
A, B, C, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M c: C C0: Type b2: Batch A B (B -> C0) a: A IHb2: mapReduce f (Done c ⊗ b2) = mapReduce f b2
mapReduce f (Done c ⊗ (b2 ⧆ a)) = mapReduce f (b2 ⧆ a)
A, B, C, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M c: C C0: Type c0: C0
mapReduce f (Done c ⊗ Done c0) = mapReduce f (Done c0)
reflexivity.
A, B, C, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M c: C C0: Type b2: Batch A B (B -> C0) a: A IHb2: mapReduce f (Done c ⊗ b2) = mapReduce f b2
mapReduce f (Done c ⊗ (b2 ⧆ a)) = mapReduce f (b2 ⧆ a)
A, B, C, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M c: C C0: Type b2: Batch A B (B -> C0) a: A IHb2: mapReduce f (Done c ⊗ b2) = mapReduce f b2
mapReduce f (Done c ⊗ (b2 ⧆ a)) = mapReduce f b2 ● f a
A, B, C, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M c: C C0: Type b2: Batch A B (B -> C0) a: A IHb2: mapReduce f (Done c ⊗ b2) = mapReduce f b2
mapReduce f (Done c ⊗ (b2 ⧆ a)) =
mapReduce f (Done c ⊗ b2) ● f a
A, B, C, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M c: C C0: Type b2: Batch A B (B -> C0) a: A IHb2: mapReduce f (Done c ⊗ b2) = mapReduce f b2
(pure (const M) Step
● Traverse_Batch1 B (B -> C * C0) (const M) Map_const
Pure_const Mult_const A False f
(map (Batch A B) strength_arrow
(mult_Batch (Done c) b2))) ● f a =
mapReduce f (mult_Batch (Done c) b2) ● f a
A, B, C, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M c: C C0: Type b2: Batch A B (B -> C0) a: A IHb2: mapReduce f (Done c ⊗ b2) = mapReduce f b2
(Ƶ
● Traverse_Batch1 B (B -> C * C0) (const M) Map_const
(fun (X : Type) (_ : X) => Ƶ) Mult_const A False
f
(map (Batch A B) strength_arrow
(mult_Batch (Done c) b2))) ● f a =
mapReduce f (mult_Batch (Done c) b2) ● f a
A, B, C, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M c: C C0: Type b2: Batch A B (B -> C0) a: A IHb2: mapReduce f (Done c ⊗ b2) = mapReduce f b2
Traverse_Batch1 B (B -> C * C0) (const M) Map_const
(fun (X : Type) (_ : X) => Ƶ) Mult_const A False f
(map (Batch A B) strength_arrow
(mult_Batch (Done c) b2)) ● f a =
mapReduce f (mult_Batch (Done c) b2) ● f a
A, B, C, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M c: C C0: Type b2: Batch A B (B -> C0) a: A IHb2: mapReduce f (Done c ⊗ b2) = mapReduce f b2
mapReduce f
(map (Batch A B) strength_arrow
(mult_Batch (Done c) b2)) ● f a =
mapReduce f (mult_Batch (Done c) b2) ● f a
A, B, C, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M c: C C0: Type b2: Batch A B (B -> C0) a: A IHb2: mapReduce f (Done c ⊗ b2) = mapReduce f b2
mapReduce f (mult_Batch (Done c) b2) ● f a =
mapReduce f (mult_Batch (Done c) b2) ● f a
reflexivity.Qed.
A, B, C, D, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M
forall (b1 : Batch A B C) (b2 : Batch A B D),
mapReduce f (b1 ⊗ b2) =
mapReduce f b1 ● mapReduce f b2
A, B, C, D, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M
forall (b1 : Batch A B C) (b2 : Batch A B D),
mapReduce f (b1 ⊗ b2) =
mapReduce f b1 ● mapReduce f b2
A, B, C, D, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M b1: Batch A B C b2: Batch A B D
mapReduce f (b1 ⊗ b2) =
mapReduce f b1 ● mapReduce f b2
A, B, C, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M b1: Batch A B C C0: Type c: C0
mapReduce f (b1 ⊗ Done c) =
mapReduce f b1 ● mapReduce f (Done c)
A, B, C, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M b1: Batch A B C C0: Type b2: Batch A B (B -> C0) a: A IHb2: mapReduce f (b1 ⊗ b2) =
mapReduce f b1 ● mapReduce f b2
mapReduce f (b1 ⊗ (b2 ⧆ a)) =
mapReduce f b1 ● mapReduce f (b2 ⧆ a)
A, B, C, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M b1: Batch A B C C0: Type c: C0
mapReduce f (b1 ⊗ Done c) =
mapReduce f b1 ● mapReduce f (Done c)
A, B, C, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M b1: Batch A B C C0: Type c: C0
mapReduce f
(map (Batch A B) (func0 : C => (c0, c)) b1) =
mapReduce f b1 ● pure (const M) (Done c)
A, B, C, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M b1: Batch A B C C0: Type c: C0
mapReduce f b1 =
mapReduce f b1 ● pure (const M) (Done c)
A, B, C, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M b1: Batch A B C C0: Type c: C0
mapReduce f b1 = mapReduce f b1 ● Ƶ
A, B, C, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M b1: Batch A B C C0: Type c: C0
mapReduce f b1 = mapReduce f b1
reflexivity.
A, B, C, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M b1: Batch A B C C0: Type b2: Batch A B (B -> C0) a: A IHb2: mapReduce f (b1 ⊗ b2) =
mapReduce f b1 ● mapReduce f b2
mapReduce f (b1 ⊗ (b2 ⧆ a)) =
mapReduce f b1 ● mapReduce f (b2 ⧆ a)
A, B, C, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M b1: Batch A B C C0: Type b2: Batch A B (B -> C0) a: A IHb2: mapReduce f (b1 ⊗ b2) =
mapReduce f b1 ● mapReduce f b2
mapReduce f (b1 ⊗ (b2 ⧆ a)) =
mapReduce f b1 ● (mapReduce f b2 ● f a)
A, B, C, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M b1: Batch A B C C0: Type b2: Batch A B (B -> C0) a: A IHb2: mapReduce f (b1 ⊗ b2) =
mapReduce f b1 ● mapReduce f b2
mapReduce f (b1 ⊗ (b2 ⧆ a)) =
(mapReduce f b1 ● mapReduce f b2) ● f a
A, B, C, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M b1: Batch A B C C0: Type b2: Batch A B (B -> C0) a: A
mapReduce f (b1 ⊗ (b2 ⧆ a)) =
mapReduce f (b1 ⊗ b2) ● f a
A, B, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M C: Type c: C C0: Type b2: Batch A B (B -> C0) a: A
mapReduce f (Done c ⊗ (b2 ⧆ a)) =
mapReduce f (Done c ⊗ b2) ● f a
A, B, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M C: Type b1: Batch A B (B -> C) a0: A C0: Type b2: Batch A B (B -> C0) a: A IHb1: mapReduce f (b1 ⊗ (b2 ⧆ a)) =
mapReduce f (b1 ⊗ b2) ● f a
mapReduce f ((b1 ⧆ a0) ⊗ (b2 ⧆ a)) =
mapReduce f ((b1 ⧆ a0) ⊗ b2) ● f a
A, B, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M C: Type c: C C0: Type b2: Batch A B (B -> C0) a: A
mapReduce f (Done c ⊗ (b2 ⧆ a)) =
mapReduce f (Done c ⊗ b2) ● f a
A, B, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M C: Type c: C C0: Type b2: Batch A B (B -> C0) a: A
mapReduce f (b2 ⧆ a) = mapReduce f (Done c ⊗ b2) ● f a
A, B, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M C: Type c: C C0: Type b2: Batch A B (B -> C0) a: A
mapReduce f (b2 ⧆ a) = mapReduce f b2 ● f a
A, B, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M C: Type c: C C0: Type b2: Batch A B (B -> C0) a: A
mapReduce f b2 ● f a = mapReduce f b2 ● f a
reflexivity.
A, B, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M C: Type b1: Batch A B (B -> C) a0: A C0: Type b2: Batch A B (B -> C0) a: A IHb1: mapReduce f (b1 ⊗ (b2 ⧆ a)) =
mapReduce f (b1 ⊗ b2) ● f a
mapReduce f ((b1 ⧆ a0) ⊗ (b2 ⧆ a)) =
mapReduce f ((b1 ⧆ a0) ⊗ b2) ● f a
A, B, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M C: Type b1: Batch A B (B -> C) a0: A C0: Type b2: Batch A B (B -> C0) a: A IHb1: mapReduce f (b1 ⊗ (b2 ⧆ a)) =
mapReduce f (b1 ⊗ b2) ● f a
(pure (const M) Step
● Traverse_Batch1 B (B -> C * C0) (const M) Map_const
Pure_const Mult_const A False f
(map (Batch A B) strength_arrow
(mult_Batch (b1 ⧆ a0) b2))) ● f a =
mapReduce f (mult_Batch (b1 ⧆ a0) b2) ● f a
A, B, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M C: Type b1: Batch A B (B -> C) a0: A C0: Type b2: Batch A B (B -> C0) a: A IHb1: mapReduce f (b1 ⊗ (b2 ⧆ a)) =
mapReduce f (b1 ⊗ b2) ● f a
(Ƶ
● Traverse_Batch1 B (B -> C * C0) (const M) Map_const
(fun (X : Type) (_ : X) => Ƶ) Mult_const A False
f
(map (Batch A B) strength_arrow
(mult_Batch (b1 ⧆ a0) b2))) ● f a =
mapReduce f (mult_Batch (b1 ⧆ a0) b2) ● f a
A, B, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M C: Type b1: Batch A B (B -> C) a0: A C0: Type b2: Batch A B (B -> C0) a: A IHb1: mapReduce f (b1 ⊗ (b2 ⧆ a)) =
mapReduce f (b1 ⊗ b2) ● f a
Traverse_Batch1 B (B -> C * C0) (const M) Map_const
(fun (X : Type) (_ : X) => Ƶ) Mult_const A False f
(map (Batch A B) strength_arrow
(mult_Batch (b1 ⧆ a0) b2)) ● f a =
mapReduce f (mult_Batch (b1 ⧆ a0) b2) ● f a
A, B, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M C: Type b1: Batch A B (B -> C) a0: A C0: Type b2: Batch A B (B -> C0) a: A IHb1: mapReduce f (b1 ⊗ (b2 ⧆ a)) =
mapReduce f (b1 ⊗ b2) ● f a
mapReduce f
(map (Batch A B) strength_arrow
(mult_Batch (b1 ⧆ a0) b2)) ● f a =
mapReduce f (mult_Batch (b1 ⧆ a0) b2) ● f a
A, B, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M C: Type b1: Batch A B (B -> C) a0: A C0: Type b2: Batch A B (B -> C0) a: A IHb1: mapReduce f (b1 ⊗ (b2 ⧆ a)) =
mapReduce f (b1 ⊗ b2) ● f a
mapReduce f (mult_Batch (b1 ⧆ a0) b2) ● f a =
mapReduce f (mult_Batch (b1 ⧆ a0) b2) ● f a
reflexivity.Qed.
A, B: Type
forall (M : Type) (op : Monoid_op M)
(unit0 : Monoid_unit M),
Monoid M ->
forall (f : A -> M) (XY : Type)
(lhs : Batch A B (X -> Y)) (rhs : Batch A B X),
mapReduce f (lhs <⋆> rhs) =
mapReduce f lhs ● mapReduce f rhs
A, B: Type
forall (M : Type) (op : Monoid_op M)
(unit0 : Monoid_unit M),
Monoid M ->
forall (f : A -> M) (XY : Type)
(lhs : Batch A B (X -> Y)) (rhs : Batch A B X),
mapReduce f (lhs <⋆> rhs) =
mapReduce f lhs ● mapReduce f rhs
A, B, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M X, Y: Type lhs: Batch A B (X -> Y) rhs: Batch A B X
mapReduce f (lhs <⋆> rhs) =
mapReduce f lhs ● mapReduce f rhs
A, B, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M X, Y: Type lhs: Batch A B (X -> Y) rhs: Batch A B X
mapReduce f
(map (Batch A B) (fun '(f, a) => f a) (lhs ⊗ rhs)) =
mapReduce f lhs ● mapReduce f rhs
A, B, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M X, Y: Type lhs: Batch A B (X -> Y) rhs: Batch A B X
mapReduce f (lhs ⊗ rhs) =
mapReduce f lhs ● mapReduce f rhs
A, B, M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M f: A -> M X, Y: Type lhs: Batch A B (X -> Y) rhs: Batch A B X
mapReduce f lhs ● mapReduce f rhs =
mapReduce f lhs ● mapReduce f rhs
forall (b : Batch A B (B -> C)) (aa' : A),
a' ∈ (b ⧆ a) = (a' ∈ b \/ a' = a)
A, B, C: Type
forall (b : Batch A B (B -> C)) (aa' : A),
a' ∈ (b ⧆ a) = (a' ∈ b \/ a' = a)
A, B, C: Type b: Batch A B (B -> C) a, a': A
a' ∈ (b ⧆ a) = (a' ∈ b \/ a' = a)
A, B, C: Type b: Batch A B (B -> C) a, a': A
mapReduce {{a'}} (b ⧆ a) = (a' ∈ b \/ a' = a)
A, B, C: Type b: Batch A B (B -> C) a, a': A
mapReduce {{a'}} (b ⧆ a) =
(mapReduce {{a'}} b \/ a' = a)
A, B, C: Type b: Batch A B (B -> C) a, a': A
mapReduce {{a'}} b ● {{a'}} a =
(mapReduce {{a'}} b \/ a' = a)
reflexivity.Qed.EndBatch_mapReduce_rewriting_derived.(** * Simultaneous Induction on Two <<Batch>>es of the Same Shape *)(******************************************************************************)Sectionshape_induction.Context
{A1A2BC : Type}
{b1: Batch A1 B C}
{b2: Batch A2 B C}
(Hshape: shape (F := BATCH1 B C) b1 = shape (F := BATCH1 B C) b2)
(P : forallC : Type,
Batch A1 B C ->
Batch A2 B C ->
Prop)
(IHdone:
forall (C : Type) (c : C), P C (Done c) (Done c))
(IHstep:
forall (C : Type)
(b1 : Batch A1 B (B -> C))
(b2 : Batch A2 B (B -> C)),
P (B -> C) b1 b2 ->
forall (a1 : A1) (a2: A2)
(Hshape: shape (F := BATCH1 B C) (Step b1 a1) =
shape (F := BATCH1 B C) (Step b2 a2)),
P C (Step b1 a1) (Step b2 a2)).
A1, A2, B, C: Type b1: Batch A1 B C b2: Batch A2 B C Hshape: shape b1 = shape b2 P: forallC : Type,
Batch A1 B C -> Batch A2 B C -> Prop IHdone: forall (C : Type) (c : C),
P C (Done c) (Done c) IHstep: forall (C : Type) (b1 : Batch A1 B (B -> C))
(b2 : Batch A2 B (B -> C)),
P (B -> C) b1 b2 ->
forall (a1 : A1) (a2 : A2),
shape (b1 ⧆ a1) = shape (b2 ⧆ a2) ->
P C (b1 ⧆ a1) (b2 ⧆ a2)
P C b1 b2
A1, A2, B, C: Type b1: Batch A1 B C b2: Batch A2 B C Hshape: shape b1 = shape b2 P: forallC : Type,
Batch A1 B C -> Batch A2 B C -> Prop IHdone: forall (C : Type) (c : C),
P C (Done c) (Done c) IHstep: forall (C : Type) (b1 : Batch A1 B (B -> C))
(b2 : Batch A2 B (B -> C)),
P (B -> C) b1 b2 ->
forall (a1 : A1) (a2 : A2),
shape (b1 ⧆ a1) = shape (b2 ⧆ a2) ->
P C (b1 ⧆ a1) (b2 ⧆ a2)
P C b1 b2
A1, A2, B, C: Type b1: Batch A1 B C b2: Batch A2 B C c: C Hshape: shape (Done c) = shape b2 P: forallC : Type,
Batch A1 B C -> Batch A2 B C -> Prop IHdone: forall (C : Type) (c : C),
P C (Done c) (Done c) IHstep: forall (C : Type) (b1 : Batch A1 B (B -> C))
(b2 : Batch A2 B (B -> C)),
P (B -> C) b1 b2 ->
forall (a1 : A1) (a2 : A2),
shape (b1 ⧆ a1) = shape (b2 ⧆ a2) ->
P C (b1 ⧆ a1) (b2 ⧆ a2)
P C (Done c) b2
A1, A2, B, C: Type b1: Batch A1 B C b2: Batch A2 B C rest: Batch A1 B (B -> C) a: A1 Hshape: shape (rest ⧆ a) = shape b2 P: forallC : Type,
Batch A1 B C -> Batch A2 B C -> Prop IHdone: forall (C : Type) (c : C),
P C (Done c) (Done c) IHstep: forall (C : Type) (b1 : Batch A1 B (B -> C))
(b2 : Batch A2 B (B -> C)),
P (B -> C) b1 b2 ->
forall (a1 : A1) (a2 : A2),
shape (b1 ⧆ a1) = shape (b2 ⧆ a2) ->
P C (b1 ⧆ a1) (b2 ⧆ a2) IHrest: Batch A1 B (B -> C) ->
forallb2 : Batch A2 B (B -> C),
shape rest = shape b2 -> P (B -> C) rest b2
P C (rest ⧆ a) b2
A1, A2, B, C: Type b1: Batch A1 B C b2: Batch A2 B C c: C Hshape: shape (Done c) = shape b2 P: forallC : Type,
Batch A1 B C -> Batch A2 B C -> Prop IHdone: forall (C : Type) (c : C),
P C (Done c) (Done c) IHstep: forall (C : Type) (b1 : Batch A1 B (B -> C))
(b2 : Batch A2 B (B -> C)),
P (B -> C) b1 b2 ->
forall (a1 : A1) (a2 : A2),
shape (b1 ⧆ a1) = shape (b2 ⧆ a2) ->
P C (b1 ⧆ a1) (b2 ⧆ a2)
P C (Done c) b2
A1, A2, B, C: Type b1: Batch A1 B C b2: Batch A2 B C c, c0: C Hshape: shape (Done c) = shape (Done c0) P: forallC : Type,
Batch A1 B C -> Batch A2 B C -> Prop IHdone: forall (C : Type) (c : C),
P C (Done c) (Done c) IHstep: forall (C : Type) (b1 : Batch A1 B (B -> C))
(b2 : Batch A2 B (B -> C)),
P (B -> C) b1 b2 ->
forall (a1 : A1) (a2 : A2),
shape (b1 ⧆ a1) = shape (b2 ⧆ a2) ->
P C (b1 ⧆ a1) (b2 ⧆ a2)
P C (Done c) (Done c0)
A1, A2, B, C: Type b1: Batch A1 B C b2: Batch A2 B C c: C b: Batch A2 B (B -> C) a: A2 Hshape: shape (Done c) = shape (b ⧆ a) P: forallC : Type,
Batch A1 B C -> Batch A2 B C -> Prop IHdone: forall (C : Type) (c : C),
P C (Done c) (Done c) IHstep: forall (C : Type) (b1 : Batch A1 B (B -> C))
(b2 : Batch A2 B (B -> C)),
P (B -> C) b1 b2 ->
forall (a1 : A1) (a2 : A2),
shape (b1 ⧆ a1) = shape (b2 ⧆ a2) ->
P C (b1 ⧆ a1) (b2 ⧆ a2)
P C (Done c) (b ⧆ a)
A1, A2, B, C: Type b1: Batch A1 B C b2: Batch A2 B C c, c0: C Hshape: shape (Done c) = shape (Done c0) P: forallC : Type,
Batch A1 B C -> Batch A2 B C -> Prop IHdone: forall (C : Type) (c : C),
P C (Done c) (Done c) IHstep: forall (C : Type) (b1 : Batch A1 B (B -> C))
(b2 : Batch A2 B (B -> C)),
P (B -> C) b1 b2 ->
forall (a1 : A1) (a2 : A2),
shape (b1 ⧆ a1) = shape (b2 ⧆ a2) ->
P C (b1 ⧆ a1) (b2 ⧆ a2)
P C (Done c) (Done c0)
nowinversion Hshape.
A1, A2, B, C: Type b1: Batch A1 B C b2: Batch A2 B C c: C b: Batch A2 B (B -> C) a: A2 Hshape: shape (Done c) = shape (b ⧆ a) P: forallC : Type,
Batch A1 B C -> Batch A2 B C -> Prop IHdone: forall (C : Type) (c : C),
P C (Done c) (Done c) IHstep: forall (C : Type) (b1 : Batch A1 B (B -> C))
(b2 : Batch A2 B (B -> C)),
P (B -> C) b1 b2 ->
forall (a1 : A1) (a2 : A2),
shape (b1 ⧆ a1) = shape (b2 ⧆ a2) ->
P C (b1 ⧆ a1) (b2 ⧆ a2)
P C (Done c) (b ⧆ a)
false.
A1, A2, B, C: Type b1: Batch A1 B C b2: Batch A2 B C rest: Batch A1 B (B -> C) a: A1 Hshape: shape (rest ⧆ a) = shape b2 P: forallC : Type,
Batch A1 B C -> Batch A2 B C -> Prop IHdone: forall (C : Type) (c : C),
P C (Done c) (Done c) IHstep: forall (C : Type) (b1 : Batch A1 B (B -> C))
(b2 : Batch A2 B (B -> C)),
P (B -> C) b1 b2 ->
forall (a1 : A1) (a2 : A2),
shape (b1 ⧆ a1) = shape (b2 ⧆ a2) ->
P C (b1 ⧆ a1) (b2 ⧆ a2) IHrest: Batch A1 B (B -> C) ->
forallb2 : Batch A2 B (B -> C),
shape rest = shape b2 -> P (B -> C) rest b2
P C (rest ⧆ a) b2
A1, A2, B, C: Type b1: Batch A1 B C b2: Batch A2 B C rest: Batch A1 B (B -> C) a: A1 c': C Hshape: shape (rest ⧆ a) = shape (Done c') P: forallC : Type,
Batch A1 B C -> Batch A2 B C -> Prop IHdone: forall (C : Type) (c : C),
P C (Done c) (Done c) IHstep: forall (C : Type) (b1 : Batch A1 B (B -> C))
(b2 : Batch A2 B (B -> C)),
P (B -> C) b1 b2 ->
forall (a1 : A1) (a2 : A2),
shape (b1 ⧆ a1) = shape (b2 ⧆ a2) ->
P C (b1 ⧆ a1) (b2 ⧆ a2) IHrest: Batch A1 B (B -> C) ->
forallb2 : Batch A2 B (B -> C),
shape rest = shape b2 -> P (B -> C) rest b2
P C (rest ⧆ a) (Done c')
A1, A2, B, C: Type b1: Batch A1 B C b2: Batch A2 B C rest: Batch A1 B (B -> C) a: A1 rest': Batch A2 B (B -> C) a': A2 Hshape: shape (rest ⧆ a) = shape (rest' ⧆ a') P: forallC : Type,
Batch A1 B C -> Batch A2 B C -> Prop IHdone: forall (C : Type) (c : C),
P C (Done c) (Done c) IHstep: forall (C : Type) (b1 : Batch A1 B (B -> C))
(b2 : Batch A2 B (B -> C)),
P (B -> C) b1 b2 ->
forall (a1 : A1) (a2 : A2),
shape (b1 ⧆ a1) = shape (b2 ⧆ a2) ->
P C (b1 ⧆ a1) (b2 ⧆ a2) IHrest: Batch A1 B (B -> C) ->
forallb2 : Batch A2 B (B -> C),
shape rest = shape b2 -> P (B -> C) rest b2
P C (rest ⧆ a) (rest' ⧆ a')
A1, A2, B, C: Type b1: Batch A1 B C b2: Batch A2 B C rest: Batch A1 B (B -> C) a: A1 c': C Hshape: shape (rest ⧆ a) = shape (Done c') P: forallC : Type,
Batch A1 B C -> Batch A2 B C -> Prop IHdone: forall (C : Type) (c : C),
P C (Done c) (Done c) IHstep: forall (C : Type) (b1 : Batch A1 B (B -> C))
(b2 : Batch A2 B (B -> C)),
P (B -> C) b1 b2 ->
forall (a1 : A1) (a2 : A2),
shape (b1 ⧆ a1) = shape (b2 ⧆ a2) ->
P C (b1 ⧆ a1) (b2 ⧆ a2) IHrest: Batch A1 B (B -> C) ->
forallb2 : Batch A2 B (B -> C),
shape rest = shape b2 -> P (B -> C) rest b2
P C (rest ⧆ a) (Done c')
false.
A1, A2, B, C: Type b1: Batch A1 B C b2: Batch A2 B C rest: Batch A1 B (B -> C) a: A1 rest': Batch A2 B (B -> C) a': A2 Hshape: shape (rest ⧆ a) = shape (rest' ⧆ a') P: forallC : Type,
Batch A1 B C -> Batch A2 B C -> Prop IHdone: forall (C : Type) (c : C),
P C (Done c) (Done c) IHstep: forall (C : Type) (b1 : Batch A1 B (B -> C))
(b2 : Batch A2 B (B -> C)),
P (B -> C) b1 b2 ->
forall (a1 : A1) (a2 : A2),
shape (b1 ⧆ a1) = shape (b2 ⧆ a2) ->
P C (b1 ⧆ a1) (b2 ⧆ a2) IHrest: Batch A1 B (B -> C) ->
forallb2 : Batch A2 B (B -> C),
shape rest = shape b2 -> P (B -> C) rest b2
P C (rest ⧆ a) (rest' ⧆ a')
A1, A2, B, C: Type b1: Batch A1 B C b2: Batch A2 B C rest: Batch A1 B (B -> C) a: A1 rest': Batch A2 B (B -> C) a': A2 Hshape: shape (rest ⧆ a) = shape (rest' ⧆ a') P: forallC : Type,
Batch A1 B C -> Batch A2 B C -> Prop IHdone: forall (C : Type) (c : C),
P C (Done c) (Done c) IHstep: forall (C : Type) (b1 : Batch A1 B (B -> C))
(b2 : Batch A2 B (B -> C)),
P (B -> C) b1 b2 ->
forall (a1 : A1) (a2 : A2),
shape (b1 ⧆ a1) = shape (b2 ⧆ a2) ->
P C (b1 ⧆ a1) (b2 ⧆ a2) IHrest: Batch A1 B (B -> C) ->
forallb2 : Batch A2 B (B -> C),
shape rest = shape b2 -> P (B -> C) rest b2
P (B -> C) rest rest'
A1, A2, B, C: Type b1: Batch A1 B C b2: Batch A2 B C rest: Batch A1 B (B -> C) a: A1 rest': Batch A2 B (B -> C) a': A2 Hshape: shape (rest ⧆ a) = shape (rest' ⧆ a') P: forallC : Type,
Batch A1 B C -> Batch A2 B C -> Prop IHdone: forall (C : Type) (c : C),
P C (Done c) (Done c) IHstep: forall (C : Type) (b1 : Batch A1 B (B -> C))
(b2 : Batch A2 B (B -> C)),
P (B -> C) b1 b2 ->
forall (a1 : A1) (a2 : A2),
shape (b1 ⧆ a1) = shape (b2 ⧆ a2) ->
P C (b1 ⧆ a1) (b2 ⧆ a2) IHrest: Batch A1 B (B -> C) ->
forallb2 : Batch A2 B (B -> C),
shape rest = shape b2 -> P (B -> C) rest b2
shape (rest ⧆ a) = shape (rest' ⧆ a')
A1, A2, B, C: Type b1: Batch A1 B C b2: Batch A2 B C rest: Batch A1 B (B -> C) a: A1 rest': Batch A2 B (B -> C) a': A2 Hshape: shape (rest ⧆ a) = shape (rest' ⧆ a') P: forallC : Type,
Batch A1 B C -> Batch A2 B C -> Prop IHdone: forall (C : Type) (c : C),
P C (Done c) (Done c) IHstep: forall (C : Type) (b1 : Batch A1 B (B -> C))
(b2 : Batch A2 B (B -> C)),
P (B -> C) b1 b2 ->
forall (a1 : A1) (a2 : A2),
shape (b1 ⧆ a1) = shape (b2 ⧆ a2) ->
P C (b1 ⧆ a1) (b2 ⧆ a2) IHrest: Batch A1 B (B -> C) ->
forallb2 : Batch A2 B (B -> C),
shape rest = shape b2 -> P (B -> C) rest b2
P (B -> C) rest rest'
A1, A2, B, C: Type b1: Batch A1 B C b2: Batch A2 B C rest: Batch A1 B (B -> C) a: A1 rest': Batch A2 B (B -> C) a': A2 Hshape: shape (rest ⧆ a) = shape (rest' ⧆ a') P: forallC : Type,
Batch A1 B C -> Batch A2 B C -> Prop IHdone: forall (C : Type) (c : C),
P C (Done c) (Done c) IHstep: forall (C : Type) (b1 : Batch A1 B (B -> C))
(b2 : Batch A2 B (B -> C)),
P (B -> C) b1 b2 ->
forall (a1 : A1) (a2 : A2),
shape (b1 ⧆ a1) = shape (b2 ⧆ a2) ->
P C (b1 ⧆ a1) (b2 ⧆ a2) IHrest: Batch A1 B (B -> C) ->
forallb2 : Batch A2 B (B -> C),
shape rest = shape b2 -> P (B -> C) rest b2
Batch A1 B (B -> C)
A1, A2, B, C: Type b1: Batch A1 B C b2: Batch A2 B C rest: Batch A1 B (B -> C) a: A1 rest': Batch A2 B (B -> C) a': A2 Hshape: shape (rest ⧆ a) = shape (rest' ⧆ a') P: forallC : Type,
Batch A1 B C -> Batch A2 B C -> Prop IHdone: forall (C : Type) (c : C),
P C (Done c) (Done c) IHstep: forall (C : Type) (b1 : Batch A1 B (B -> C))
(b2 : Batch A2 B (B -> C)),
P (B -> C) b1 b2 ->
forall (a1 : A1) (a2 : A2),
shape (b1 ⧆ a1) = shape (b2 ⧆ a2) ->
P C (b1 ⧆ a1) (b2 ⧆ a2) IHrest: Batch A1 B (B -> C) ->
forallb2 : Batch A2 B (B -> C),
shape rest = shape b2 -> P (B -> C) rest b2
shape rest = shape rest'
A1, A2, B, C: Type b1: Batch A1 B C b2: Batch A2 B C rest: Batch A1 B (B -> C) a: A1 rest': Batch A2 B (B -> C) a': A2 Hshape: shape (rest ⧆ a) = shape (rest' ⧆ a') P: forallC : Type,
Batch A1 B C -> Batch A2 B C -> Prop IHdone: forall (C : Type) (c : C),
P C (Done c) (Done c) IHstep: forall (C : Type) (b1 : Batch A1 B (B -> C))
(b2 : Batch A2 B (B -> C)),
P (B -> C) b1 b2 ->
forall (a1 : A1) (a2 : A2),
shape (b1 ⧆ a1) = shape (b2 ⧆ a2) ->
P C (b1 ⧆ a1) (b2 ⧆ a2) IHrest: Batch A1 B (B -> C) ->
forallb2 : Batch A2 B (B -> C),
shape rest = shape b2 -> P (B -> C) rest b2
shape rest = shape rest'
nowinversion Hshape.
A1, A2, B, C: Type b1: Batch A1 B C b2: Batch A2 B C rest: Batch A1 B (B -> C) a: A1 rest': Batch A2 B (B -> C) a': A2 Hshape: shape (rest ⧆ a) = shape (rest' ⧆ a') P: forallC : Type,
Batch A1 B C -> Batch A2 B C -> Prop IHdone: forall (C : Type) (c : C),
P C (Done c) (Done c) IHstep: forall (C : Type) (b1 : Batch A1 B (B -> C))
(b2 : Batch A2 B (B -> C)),
P (B -> C) b1 b2 ->
forall (a1 : A1) (a2 : A2),
shape (b1 ⧆ a1) = shape (b2 ⧆ a2) ->
P C (b1 ⧆ a1) (b2 ⧆ a2) IHrest: Batch A1 B (B -> C) ->
forallb2 : Batch A2 B (B -> C),
shape rest = shape b2 -> P (B -> C) rest b2
shape (rest ⧆ a) = shape (rest' ⧆ a')
apply Hshape.Qed.Endshape_induction.(*(** * Miscellaneous *)(******************************************************************************)Instance: forall B, Pure (BATCH1 B B).Proof. unfold Pure. intros B A. apply batch.Defined.Instance: forall B, Mult (BATCH1 B B).Proof. unfold Mult. intros B A A'. apply batch.Defined. *)(** * <<runBatch>> specialized to monoids *)(******************************************************************************)SectionrunBatch_monoid.Context
`{Monoid M}.FixpointrunBatch_monoid
{AB: Type} `(ϕ: A -> M) `(b: Batch A B C): M :=
match b with
| Done c => monoid_unit M
| Step rest a => runBatch_monoid (ϕ: A -> M) rest ● ϕ a
end.
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B: Type
forall (ϕ : A -> M) (C : Type) (b : Batch A B C),
runBatch_monoid ϕ b =
unconst (runBatch (mkConst ∘ ϕ) b)
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B: Type
forall (ϕ : A -> M) (C : Type) (b : Batch A B C),
runBatch_monoid ϕ b =
unconst (runBatch (mkConst ∘ ϕ) b)
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B: Type ϕ: A -> M C: Type b: Batch A B C
runBatch_monoid ϕ b =
unconst (runBatch (mkConst ∘ ϕ) b)
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B: Type ϕ: A -> M C: Type c: C
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B: Type ϕ: A -> M C: Type b: Batch A B (B -> C) a: A IHb: runBatch_monoid ϕ b =
unconst (runBatch (mkConst ∘ ϕ) b)
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B: Type ϕ: A -> M C: Type b: Batch A B (B -> C) a: A IHb: runBatch_monoid ϕ b =
unconst (runBatch (mkConst ∘ ϕ) b)
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B: Type ϕ: A -> M C: Type b: Batch A B (B -> C) a: A IHb: runBatch_monoid ϕ b =
unconst (runBatch (mkConst ∘ ϕ) b)
runBatch_monoid ϕ b ● ϕ a =
unconst (runBatch (mkConst ∘ ϕ) b) ● ϕ a
nowrewrite IHb.Qed.
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B: Type
forall (ϕ : A -> M) (C : Type) (b : Batch A B C),
runBatch_monoid ϕ b = runBatch (ϕ : A -> const M B) b
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B: Type
forall (ϕ : A -> M) (C : Type) (b : Batch A B C),
runBatch_monoid ϕ b = runBatch (ϕ : A -> const M B) b
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B: Type ϕ: A -> M C: Type b: Batch A B C
runBatch_monoid ϕ b = runBatch (ϕ : A -> const M B) b
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B: Type ϕ: A -> M C: Type c: C
runBatch_monoid ϕ (Done c) = runBatch ϕ (Done c)
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B: Type ϕ: A -> M C: Type b: Batch A B (B -> C) a: A IHb: runBatch_monoid ϕ b = runBatch ϕ b
runBatch_monoid ϕ (b ⧆ a) = runBatch ϕ (b ⧆ a)
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B: Type ϕ: A -> M C: Type c: C
runBatch_monoid ϕ (Done c) = runBatch ϕ (Done c)
easy.
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B: Type ϕ: A -> M C: Type b: Batch A B (B -> C) a: A IHb: runBatch_monoid ϕ b = runBatch ϕ b
runBatch_monoid ϕ (b ⧆ a) = runBatch ϕ (b ⧆ a)
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B: Type ϕ: A -> M C: Type b: Batch A B (B -> C) a: A IHb: runBatch_monoid ϕ b = runBatch ϕ b
runBatch_monoid ϕ b ● ϕ a = runBatch ϕ b ● ϕ a
nowrewrite IHb.Qed.
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B, C, C': Type
forall (ϕ : A -> M) (f : C -> C') (b : Batch A B C),
runBatch_monoid ϕ b =
runBatch_monoid ϕ (map (Batch A B) f b)
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B, C, C': Type
forall (ϕ : A -> M) (f : C -> C') (b : Batch A B C),
runBatch_monoid ϕ b =
runBatch_monoid ϕ (map (Batch A B) f b)
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B, C, C': Type ϕ: A -> M f: C -> C' b: Batch A B C
runBatch_monoid ϕ b =
runBatch_monoid ϕ (map (Batch A B) f b)
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B, C: Type ϕ: A -> M b: Batch A B C
forall (C' : Type) (f : C -> C'),
runBatch_monoid ϕ b =
runBatch_monoid ϕ (map (Batch A B) f b)
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B: Type ϕ: A -> M C: Type c: C C': Type f: C -> C'
runBatch_monoid ϕ (Done c) =
runBatch_monoid ϕ (map (Batch A B) f (Done c))
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B: Type ϕ: A -> M C: Type b: Batch A B (B -> C) a: A IHb: forall (C' : Type) (f : (B -> C) -> C'),
runBatch_monoid ϕ b =
runBatch_monoid ϕ (map (Batch A B) f b) C': Type f: C -> C'
runBatch_monoid ϕ (b ⧆ a) =
runBatch_monoid ϕ (map (Batch A B) f (b ⧆ a))
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B: Type ϕ: A -> M C: Type c: C C': Type f: C -> C'
runBatch_monoid ϕ (Done c) =
runBatch_monoid ϕ (map (Batch A B) f (Done c))
reflexivity.
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B: Type ϕ: A -> M C: Type b: Batch A B (B -> C) a: A IHb: forall (C' : Type) (f : (B -> C) -> C'),
runBatch_monoid ϕ b =
runBatch_monoid ϕ (map (Batch A B) f b) C': Type f: C -> C'
runBatch_monoid ϕ (b ⧆ a) =
runBatch_monoid ϕ (map (Batch A B) f (b ⧆ a))
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B: Type ϕ: A -> M C: Type b: Batch A B (B -> C) a: A IHb: forall (C' : Type) (f : (B -> C) -> C'),
runBatch_monoid ϕ b =
runBatch_monoid ϕ (map (Batch A B) f b) C': Type f: C -> C'
runBatch_monoid ϕ b ● ϕ a =
runBatch_monoid ϕ (map (Batch A B) (compose f) b)
● ϕ a
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B: Type ϕ: A -> M C: Type b: Batch A B (B -> C) a: A IHb: forall (C' : Type) (f : (B -> C) -> C'),
runBatch_monoid ϕ b =
runBatch_monoid ϕ (map (Batch A B) f b) C': Type f: C -> C'
runBatch_monoid ϕ b ● ϕ a = runBatch_monoid ϕ b ● ϕ a
reflexivity.Qed.
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B, B': Type
forall (ϕ : A -> M) (f : B' -> B) (C : Type)
(b : Batch A B C),
runBatch_monoid ϕ b =
runBatch_monoid ϕ (mapsnd_Batch f b)
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B, B': Type
forall (ϕ : A -> M) (f : B' -> B) (C : Type)
(b : Batch A B C),
runBatch_monoid ϕ b =
runBatch_monoid ϕ (mapsnd_Batch f b)
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B, B': Type ϕ: A -> M f: B' -> B C: Type b: Batch A B C
runBatch_monoid ϕ b =
runBatch_monoid ϕ (mapsnd_Batch f b)
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B, B': Type ϕ: A -> M f: B' -> B C: Type b: Batch A B C
runBatch ϕ b = runBatch_monoid ϕ (mapsnd_Batch f b)
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B, B': Type ϕ: A -> M f: B' -> B C: Type b: Batch A B C
runBatch ϕ b = runBatch ϕ (mapsnd_Batch f b)
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B, B': Type ϕ: A -> M f: B' -> B C: Type b: Batch A B C
runBatch ϕ b = runBatch (map (const M) f ∘ ϕ) b
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B, B': Type ϕ: A -> M f: B' -> B C: Type b: Batch A B C
runBatch ϕ b = runBatch (map (const M) f ∘ ϕ) b
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B, B': Type ϕ: A -> M f: B' -> B C: Type c: C
runBatch ϕ (Done c) =
runBatch (map (const M) f ∘ ϕ) (Done c)
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B, B': Type ϕ: A -> M f: B' -> B C: Type b: Batch A B (B -> C) a: A IHb: runBatch ϕ b = runBatch (map (const M) f ∘ ϕ) b
runBatch ϕ (b ⧆ a) =
runBatch (map (const M) f ∘ ϕ) (b ⧆ a)
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B, B': Type ϕ: A -> M f: B' -> B C: Type c: C
runBatch ϕ (Done c) =
runBatch (map (const M) f ∘ ϕ) (Done c)
easy.
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B, B': Type ϕ: A -> M f: B' -> B C: Type b: Batch A B (B -> C) a: A IHb: runBatch ϕ b = runBatch (map (const M) f ∘ ϕ) b
runBatch ϕ (b ⧆ a) =
runBatch (map (const M) f ∘ ϕ) (b ⧆ a)
M: Type op: Monoid_op M unit0: Monoid_unit M H: Monoid M A, B, B': Type ϕ: A -> M f: B' -> B C: Type b: Batch A B (B -> C) a: A IHb: runBatch ϕ b = runBatch (map (const M) f ∘ ϕ) b
runBatch ϕ b ● ϕ a =
runBatch (map (const M) f ∘ ϕ) b
● (map (const M) f ∘ ϕ) a
nowrewrite IHb.Qed.EndrunBatch_monoid.(** * The <<length_Batch>> Operation *)(** This function is introduced because using <<plength>> has less desirable simplification behavior, which makes programming functions like <<Batch_make>> difficult *)(******************************************************************************)From Tealeaves Require Import Misc.NaturalNumbers.Sectionlength.Fixpointlength_Batch {ABC: Type} (b: Batch A B C): nat :=
match b with
| Done _ => 0
| Step rest a => S (length_Batch (C := B -> C) rest)
end.
A, B, C: Type b: Batch A B C
length_Batch b = plength b
A, B, C: Type b: Batch A B C
length_Batch b = plength b
A, B, C: Type c: C
length_Batch (Done c) = plength (Done c)
A, B, C: Type b: Batch A B (B -> C) a: A IHb: length_Batch b = plength b
length_Batch (b ⧆ a) = plength (b ⧆ a)
A, B, C: Type c: C
length_Batch (Done c) = plength (Done c)
reflexivity.
A, B, C: Type b: Batch A B (B -> C) a: A IHb: length_Batch b = plength b
length_Batch (b ⧆ a) = plength (b ⧆ a)
A, B, C: Type b: Batch A B (B -> C) a: A IHb: length_Batch b = plength b
S (length_Batch b) =
Traverse_Batch1 B (B -> C) (const nat) Map_const
Pure_const Mult_const A False (fun_ : A => 1) b ● 1
A, B, C: Type b: Batch A B (B -> C) a: A IHb: length_Batch b = plength b
S (plength b) =
Traverse_Batch1 B (B -> C) (const nat) Map_const
Pure_const Mult_const A False (fun_ : A => 1) b ● 1
A, B, C: Type b: Batch A B (B -> C) a: A IHb: length_Batch b = plength b
S (plength b) =
(Traverse_Batch1 B (B -> C) (const nat) Map_const
Pure_const Mult_const A False (fun_ : A => 1) b +
1)%nat
A, B, C: Type b: Batch A B (B -> C) a: A IHb: length_Batch b = plength b
S (plength b) =
S
(Traverse_Batch1 B (B -> C) (const nat) Map_const
Pure_const Mult_const A False (fun_ : A => 1) b)
reflexivity.Qed.
A, B, C: Type b: Batch A B C
length_Batch b = runBatch (fun_ : A => 1) b
A, B, C: Type b: Batch A B C
length_Batch b = runBatch (fun_ : A => 1) b
A, B, C: Type b: Batch A B C
plength b = runBatch (fun_ : A => 1) b
A, B, C: Type c: C
plength (Done c) = runBatch (fun_ : A => 1) (Done c)
A, B, C: Type b: Batch A B (B -> C) a: A IHb: plength b = runBatch (fun_ : A => 1) b
plength (b ⧆ a) = runBatch (fun_ : A => 1) (b ⧆ a)
A, B, C: Type c: C
plength (Done c) = runBatch (fun_ : A => 1) (Done c)
reflexivity.
A, B, C: Type b: Batch A B (B -> C) a: A IHb: plength b = runBatch (fun_ : A => 1) b
plength (b ⧆ a) = runBatch (fun_ : A => 1) (b ⧆ a)
A, B, C: Type b: Batch A B (B -> C) a: A IHb: plength b = runBatch (fun_ : A => 1) b
Traverse_Batch1 B (B -> C) (const nat) Map_const
Pure_const Mult_const A False (fun_ : A => 1) b ● 1 =
runBatch (fun_ : A => 1) b ● 1
A, B, C: Type b: Batch A B (B -> C) a: A IHb: plength b = runBatch (fun_ : A => 1) b
Traverse_Batch1 B (B -> C) (const nat) Map_const
Pure_const Mult_const A False (fun_ : A => 1) b ● 1 =
plength b ● 1
reflexivity.Qed.(** ** Rewriting Rules *)(** TODO *)(******************************************************************************)
A, B, C: Type
forall (b : Batch A B (B -> C)) (a : A),
length_Batch (b ⧆ a) = S (length_Batch b)
A, B, C: Type
forall (b : Batch A B (B -> C)) (a : A),
length_Batch (b ⧆ a) = S (length_Batch b)
reflexivity.Qed.(** ** Length is the Same as the Underlying <<list>> *)(* The length of a <<Batch>> is the same as the length of the list we can extract from it *)(******************************************************************************)
forall (ABC : Type) (b : Batch A B C),
length_Batch b = length (runBatch (ret list A) b)
forall (ABC : Type) (b : Batch A B C),
length_Batch b = length (runBatch (ret list A) b)
A, B, C: Type b: Batch A B C
length_Batch b = length (runBatch (ret list A) b)
A, B, C: Type c: C
length_Batch (Done c) =
length (runBatch (ret list A) (Done c))
A, B, C: Type b: Batch A B (B -> C) a: A IHb: length_Batch b = length (runBatch (ret list A) b)
length_Batch (b ⧆ a) =
length (runBatch (ret list A) (b ⧆ a))
A, B, C: Type c: C
length_Batch (Done c) =
length (runBatch (ret list A) (Done c))
reflexivity.
A, B, C: Type b: Batch A B (B -> C) a: A IHb: length_Batch b = length (runBatch (ret list A) b)
length_Batch (b ⧆ a) =
length (runBatch (ret list A) (b ⧆ a))
A, B, C: Type b: Batch A B (B -> C) a: A IHb: length_Batch b = length (runBatch (ret list A) b)
S (length_Batch b) =
length (runBatch (ret list A) b ● ret list A a)
A, B, C: Type b: Batch A B (B -> C) a: A IHb: length_Batch b = length (runBatch (ret list A) b)
S (length (runBatch (ret list A) b)) =
length (runBatch (ret list A) b ● ret list A a)
A, B, C: Type b: Batch A B (B -> C) a: A IHb: length_Batch b = length (runBatch (ret list A) b)
S (length (runBatch (ret list A) b)) =
length (runBatch (ret list A) b ++ ret list A a)
A, B, C: Type b: Batch A B (B -> C) a: A IHb: length_Batch b = length (runBatch (ret list A) b)
S (length (runBatch (ret list A) b)) =
(length (runBatch (ret list A) b) +
length (ret list A a))%nat
A, B, C: Type b: Batch A B (B -> C) a: A IHb: length_Batch b = length (runBatch (ret list A) b)
S (length (runBatch (ret list A) b)) =
(length (runBatch (ret list A) b) + 1)%nat
lia.Qed.(** ** Length is Preserved By <<map>> *)(******************************************************************************)
forall (ABCC' : Type) (f : C -> C')
(b : Batch A B C),
length_Batch b = length_Batch (map (Batch A B) f b)
forall (ABCC' : Type) (f : C -> C')
(b : Batch A B C),
length_Batch b = length_Batch (map (Batch A B) f b)
A, B, C, C': Type f: C -> C' b: Batch A B C
length_Batch b = length_Batch (map (Batch A B) f b)
A, B, C: Type b: Batch A B C
forall (C' : Type) (f : C -> C'),
length_Batch b = length_Batch (map (Batch A B) f b)
A, B, C: Type c: C C': Type f: C -> C'
length_Batch (Done c) =
length_Batch (map (Batch A B) f (Done c))
A, B, C: Type b: Batch A B (B -> C) a: A IHb: forall (C' : Type) (f : (B -> C) -> C'),
length_Batch b = length_Batch (map (Batch A B) f b) C': Type f: C -> C'
length_Batch (b ⧆ a) =
length_Batch (map (Batch A B) f (b ⧆ a))
A, B, C: Type c: C C': Type f: C -> C'
length_Batch (Done c) =
length_Batch (map (Batch A B) f (Done c))
reflexivity.
A, B, C: Type b: Batch A B (B -> C) a: A IHb: forall (C' : Type) (f : (B -> C) -> C'),
length_Batch b = length_Batch (map (Batch A B) f b) C': Type f: C -> C'
length_Batch (b ⧆ a) =
length_Batch (map (Batch A B) f (b ⧆ a))
A, B, C: Type b: Batch A B (B -> C) a: A IHb: forall (C' : Type) (f : (B -> C) -> C'),
length_Batch b = length_Batch (map (Batch A B) f b) C': Type f: C -> C'
S (length_Batch b) =
S (length_Batch (map (Batch A B) (compose f) b))
A, B, C: Type b: Batch A B (B -> C) a: A IHb: forall (C' : Type) (f : (B -> C) -> C'),
length_Batch b = length_Batch (map (Batch A B) f b) C': Type f: C -> C'
length_Batch b =
length_Batch (map (Batch A B) (compose f) b)
A, B, C: Type b: Batch A B (B -> C) a: A C': Type f: C -> C' IHb: length_Batch b = length_Batch (map (Batch A B) (compose f) b)
length_Batch b =
length_Batch (map (Batch A B) (compose f) b)
auto.Qed.
forall (AA'BC : Type) (f : A -> A')
(b : Batch A B C),
length_Batch b = length_Batch (mapfst_Batch f b)
forall (AA'BC : Type) (f : A -> A')
(b : Batch A B C),
length_Batch b = length_Batch (mapfst_Batch f b)
A, A', B, C: Type f: A -> A' b: Batch A B C
length_Batch b = length_Batch (mapfst_Batch f b)
A, A', B: Type f: A -> A' C: Type c: C
length_Batch (Done c) =
length_Batch (mapfst_Batch f (Done c))
A, A', B: Type f: A -> A' C: Type b: Batch A B (B -> C) a: A IHb: length_Batch b = length_Batch (mapfst_Batch f b)
length_Batch (b ⧆ a) =
length_Batch (mapfst_Batch f (b ⧆ a))
A, A', B: Type f: A -> A' C: Type c: C
length_Batch (Done c) =
length_Batch (mapfst_Batch f (Done c))
reflexivity.
A, A', B: Type f: A -> A' C: Type b: Batch A B (B -> C) a: A IHb: length_Batch b = length_Batch (mapfst_Batch f b)
length_Batch (b ⧆ a) =
length_Batch (mapfst_Batch f (b ⧆ a))
A, A', B: Type f: A -> A' C: Type b: Batch A B (B -> C) a: A IHb: length_Batch b = length_Batch (mapfst_Batch f b)
S (length_Batch b) =
S (length_Batch (mapfst_Batch f b))
A, A', B: Type f: A -> A' C: Type b: Batch A B (B -> C) a: A IHb: length_Batch b = length_Batch (mapfst_Batch f b)
S (length_Batch (mapfst_Batch f b)) =
S (length_Batch (mapfst_Batch f b))
reflexivity.Qed.
forall (ABB'C : Type) (f : B' -> B)
(b : Batch A B C),
length_Batch b = length_Batch (mapsnd_Batch f b)
forall (ABB'C : Type) (f : B' -> B)
(b : Batch A B C),
length_Batch b = length_Batch (mapsnd_Batch f b)
A, B, B', C: Type f: B' -> B b: Batch A B C
length_Batch b = length_Batch (mapsnd_Batch f b)
A, B, B': Type f: B' -> B C: Type c: C
length_Batch (Done c) =
length_Batch (mapsnd_Batch f (Done c))
A, B, B': Type f: B' -> B C: Type b: Batch A B (B -> C) a: A IHb: length_Batch b = length_Batch (mapsnd_Batch f b)
length_Batch (b ⧆ a) =
length_Batch (mapsnd_Batch f (b ⧆ a))
A, B, B': Type f: B' -> B C: Type c: C
length_Batch (Done c) =
length_Batch (mapsnd_Batch f (Done c))
reflexivity.
A, B, B': Type f: B' -> B C: Type b: Batch A B (B -> C) a: A IHb: length_Batch b = length_Batch (mapsnd_Batch f b)
length_Batch (b ⧆ a) =
length_Batch (mapsnd_Batch f (b ⧆ a))
A, B, B': Type f: B' -> B C: Type b: Batch A B (B -> C) a: A IHb: length_Batch b = length_Batch (mapsnd_Batch f b)
S (length_Batch b) =
S
(length_Batch
(map (Batch A B') (precompose f)
(mapsnd_Batch f b)))
A, B, B': Type f: B' -> B C: Type b: Batch A B (B -> C) a: A IHb: length_Batch b = length_Batch (mapsnd_Batch f b)
length_Batch b =
length_Batch
(map (Batch A B') (precompose f) (mapsnd_Batch f b))
A, B, B': Type f: B' -> B C: Type b: Batch A B (B -> C) a: A IHb: length_Batch b = length_Batch (mapsnd_Batch f b)
length_Batch (mapsnd_Batch f b) =
length_Batch
(map (Batch A B') (precompose f) (mapsnd_Batch f b))
A, B, B': Type f: B' -> B C: Type b: Batch A B (B -> C) a: A IHb: length_Batch b = length_Batch (mapsnd_Batch f b)
length_Batch
(map (Batch A B') (precompose f) (mapsnd_Batch f b)) =
length_Batch
(map (Batch A B') (precompose f) (mapsnd_Batch f b))
reflexivity.Qed.(** ** Length is Preserved by <<cojoin_Batch>> *)(******************************************************************************)
forall (AA'BC : Type) (b : Batch A B C),
length_Batch b = length_Batch (cojoin_Batch b)
forall (AA'BC : Type) (b : Batch A B C),
length_Batch b = length_Batch (cojoin_Batch b)
A, A', B, C: Type c: C
length_Batch (Done c) =
length_Batch (cojoin_Batch (Done c))
A, A', B, C: Type b: Batch A B (B -> C) a: A IHb: length_Batch b = length_Batch (cojoin_Batch b)
length_Batch (b ⧆ a) =
length_Batch (cojoin_Batch (b ⧆ a))
A, A', B, C: Type c: C
length_Batch (Done c) =
length_Batch (cojoin_Batch (Done c))
reflexivity.
A, A', B, C: Type b: Batch A B (B -> C) a: A IHb: length_Batch b = length_Batch (cojoin_Batch b)
length_Batch (b ⧆ a) =
length_Batch (cojoin_Batch (b ⧆ a))
A, A', B, C: Type b: Batch A B (B -> C) a: A IHb: length_Batch b = length_Batch (cojoin_Batch b)
S (length_Batch b) =
S
(length_Batch
(map (Batch A A') Step (cojoin_Batch b)))
A, A', B, C: Type b: Batch A B (B -> C) a: A IHb: length_Batch b = length_Batch (cojoin_Batch b)
length_Batch b =
length_Batch (map (Batch A A') Step (cojoin_Batch b))
A, A', B, C: Type b: Batch A B (B -> C) a: A IHb: length_Batch b = length_Batch (cojoin_Batch b)
length_Batch (cojoin_Batch b) =
length_Batch (map (Batch A A') Step (cojoin_Batch b))
A, A', B, C: Type b: Batch A B (B -> C) a: A IHb: length_Batch b = length_Batch (cojoin_Batch b)
length_Batch (cojoin_Batch b) =
length_Batch (cojoin_Batch b)
reflexivity.Qed.(** ** Two Same-Shaped <<Batch>>es Have the Same Length*)(******************************************************************************)
forall (A1BC : Type) (b1 : Batch A1 B C) (A2 : Type)
(b2 : Batch A2 B C),
shape b1 = shape b2 ->
length_Batch b1 = length_Batch b2
forall (A1BC : Type) (b1 : Batch A1 B C) (A2 : Type)
(b2 : Batch A2 B C),
shape b1 = shape b2 ->
length_Batch b1 = length_Batch b2
A1, B, C: Type b1: Batch A1 B C A2: Type b2: Batch A2 B C Hshape: shape b1 = shape b2
length_Batch b1 = length_Batch b2
A1, B, C: Type c: C A2: Type b2: Batch A2 B C Hshape: shape (Done c) = shape b2
length_Batch (Done c) = length_Batch b2
A1, B, C: Type b1: Batch A1 B (B -> C) a: A1 A2: Type b2: Batch A2 B C Hshape: shape (b1 ⧆ a) = shape b2 IHb1: forallb2 : Batch A2 B (B -> C),
shape b1 = shape b2 ->
length_Batch b1 = length_Batch b2
length_Batch (b1 ⧆ a) = length_Batch b2
A1, B, C: Type c: C A2: Type b2: Batch A2 B C Hshape: shape (Done c) = shape b2
length_Batch (Done c) = length_Batch b2
A1, B, C: Type c: C A2: Type c0: C Hshape: shape (Done c) = shape (Done c0)
length_Batch (Done c) = length_Batch (Done c0)
A1, B, C: Type c: C A2: Type b2: Batch A2 B (B -> C) a: A2 Hshape: shape (Done c) = shape (b2 ⧆ a)
length_Batch (Done c) = length_Batch (b2 ⧆ a)
A1, B, C: Type c: C A2: Type c0: C Hshape: shape (Done c) = shape (Done c0)
length_Batch (Done c) = length_Batch (Done c0)
nowinversion Hshape.
A1, B, C: Type c: C A2: Type b2: Batch A2 B (B -> C) a: A2 Hshape: shape (Done c) = shape (b2 ⧆ a)
length_Batch (Done c) = length_Batch (b2 ⧆ a)
false.
A1, B, C: Type b1: Batch A1 B (B -> C) a: A1 A2: Type b2: Batch A2 B C Hshape: shape (b1 ⧆ a) = shape b2 IHb1: forallb2 : Batch A2 B (B -> C),
shape b1 = shape b2 ->
length_Batch b1 = length_Batch b2
length_Batch (b1 ⧆ a) = length_Batch b2
A1, B, C: Type b1: Batch A1 B (B -> C) a: A1 A2: Type c: C Hshape: shape (b1 ⧆ a) = shape (Done c) IHb1: forallb2 : Batch A2 B (B -> C),
shape b1 = shape b2 ->
length_Batch b1 = length_Batch b2
length_Batch (b1 ⧆ a) = length_Batch (Done c)
A1, B, C: Type b1: Batch A1 B (B -> C) a: A1 A2: Type b2: Batch A2 B (B -> C) a0: A2 Hshape: shape (b1 ⧆ a) = shape (b2 ⧆ a0) IHb1: forallb2 : Batch A2 B (B -> C),
shape b1 = shape b2 ->
length_Batch b1 = length_Batch b2
length_Batch (b1 ⧆ a) = length_Batch (b2 ⧆ a0)
A1, B, C: Type b1: Batch A1 B (B -> C) a: A1 A2: Type c: C Hshape: shape (b1 ⧆ a) = shape (Done c) IHb1: forallb2 : Batch A2 B (B -> C),
shape b1 = shape b2 ->
length_Batch b1 = length_Batch b2
length_Batch (b1 ⧆ a) = length_Batch (Done c)
false.
A1, B, C: Type b1: Batch A1 B (B -> C) a: A1 A2: Type b2: Batch A2 B (B -> C) a0: A2 Hshape: shape (b1 ⧆ a) = shape (b2 ⧆ a0) IHb1: forallb2 : Batch A2 B (B -> C),
shape b1 = shape b2 ->
length_Batch b1 = length_Batch b2
length_Batch (b1 ⧆ a) = length_Batch (b2 ⧆ a0)
A1, B, C: Type b1: Batch A1 B (B -> C) a: A1 A2: Type b2: Batch A2 B (B -> C) a0: A2 Hshape: shape (b1 ⧆ a) = shape (b2 ⧆ a0) IHb1: forallb2 : Batch A2 B (B -> C),
shape b1 = shape b2 ->
length_Batch b1 = length_Batch b2
S (length_Batch b1) = S (length_Batch b2)
A1, B, C: Type b1: Batch A1 B (B -> C) a: A1 A2: Type b2: Batch A2 B (B -> C) a0: A2 Hshape: shape (b1 ⧆ a) = shape (b2 ⧆ a0) IHb1: forallb2 : Batch A2 B (B -> C),
shape b1 = shape b2 ->
length_Batch b1 = length_Batch b2
length_Batch b1 = length_Batch b2
A1, B, C: Type b1: Batch A1 B (B -> C) a: A1 A2: Type b2: Batch A2 B (B -> C) a0: A2 Hshape: shape (b1 ⧆ a) = shape (b2 ⧆ a0) IHb1: forallb2 : Batch A2 B (B -> C),
shape b1 = shape b2 ->
length_Batch b1 = length_Batch b2
shape b1 = shape b2
nowinversion Hshape.Qed.Endlength.(** * Specification for <<traverse>> via <<runBatch>> *)(******************************************************************************)
G: Type -> Type H: Map G H0: Mult G H1: Pure G Applicative0: Applicative G A, A': Type ϕ: A -> G A' B, C: Type
traverse ϕ = runBatch (map G (batch A' B) ∘ ϕ)
G: Type -> Type H: Map G H0: Mult G H1: Pure G Applicative0: Applicative G A, A': Type ϕ: A -> G A' B, C: Type
traverse ϕ = runBatch (map G (batch A' B) ∘ ϕ)
G: Type -> Type H: Map G H0: Mult G H1: Pure G Applicative0: Applicative G A, A': Type ϕ: A -> G A' B, C: Type
traverse ϕ = runBatch (map G (batch A' B) ∘ ϕ)
G: Type -> Type H: Map G H0: Mult G H1: Pure G Applicative0: Applicative G A, A': Type ϕ: A -> G A' B, C: Type b: Batch A B C
traverse ϕ b = runBatch (map G (batch A' B) ∘ ϕ) b
G: Type -> Type H: Map G H0: Mult G H1: Pure G Applicative0: Applicative G A, A': Type ϕ: A -> G A' B, C: Type c: C
traverse ϕ (Done c) =
runBatch (map G (batch A' B) ∘ ϕ) (Done c)
G: Type -> Type H: Map G H0: Mult G H1: Pure G Applicative0: Applicative G A, A': Type ϕ: A -> G A' B, C: Type rest: Batch A B (B -> C) a: A IHrest: traverse ϕ rest =
runBatch (map G (batch A' B) ∘ ϕ) rest
traverse ϕ (rest ⧆ a) =
runBatch (map G (batch A' B) ∘ ϕ) (rest ⧆ a)
G: Type -> Type H: Map G H0: Mult G H1: Pure G Applicative0: Applicative G A, A': Type ϕ: A -> G A' B, C: Type c: C
traverse ϕ (Done c) =
runBatch (map G (batch A' B) ∘ ϕ) (Done c)
G: Type -> Type H: Map G H0: Mult G H1: Pure G Applicative0: Applicative G A, A': Type ϕ: A -> G A' B, C: Type c: C
traverse ϕ (Done c) = pure (G ∘ Batch A' B) c
G: Type -> Type H: Map G H0: Mult G H1: Pure G Applicative0: Applicative G A, A': Type ϕ: A -> G A' B, C: Type c: C
pure G (Done c) = pure (G ∘ Batch A' B) c
reflexivity.
G: Type -> Type H: Map G H0: Mult G H1: Pure G Applicative0: Applicative G A, A': Type ϕ: A -> G A' B, C: Type rest: Batch A B (B -> C) a: A IHrest: traverse ϕ rest =
runBatch (map G (batch A' B) ∘ ϕ) rest
traverse ϕ (rest ⧆ a) =
runBatch (map G (batch A' B) ∘ ϕ) (rest ⧆ a)
G: Type -> Type H: Map G H0: Mult G H1: Pure G Applicative0: Applicative G A, A': Type ϕ: A -> G A' B, C: Type rest: Batch A B (B -> C) a: A IHrest: traverse ϕ rest =
runBatch (map G (batch A' B) ∘ ϕ) rest
traverse ϕ (rest ⧆ a) =
runBatch (map G (batch A' B) ∘ ϕ) rest <⋆>
(map G (batch A' B) ∘ ϕ) a
G: Type -> Type H: Map G H0: Mult G H1: Pure G Applicative0: Applicative G A, A': Type ϕ: A -> G A' B, C: Type rest: Batch A B (B -> C) a: A IHrest: traverse ϕ rest =
runBatch (map G (batch A' B) ∘ ϕ) rest
map G Step (traverse ϕ rest) <⋆> ϕ a =
runBatch (map G (batch A' B) ∘ ϕ) rest <⋆>
(map G (batch A' B) ∘ ϕ) a
G: Type -> Type H: Map G H0: Mult G H1: Pure G Applicative0: Applicative G A, A': Type ϕ: A -> G A' B, C: Type rest: Batch A B (B -> C) a: A IHrest: traverse ϕ rest =
runBatch (map G (batch A' B) ∘ ϕ) rest
map G Step (runBatch (map G (batch A' B) ∘ ϕ) rest) <⋆>
ϕ a =
runBatch (map G (batch A' B) ∘ ϕ) rest <⋆>
(map G (batch A' B) ∘ ϕ) a
G: Type -> Type H: Map G H0: Mult G H1: Pure G Applicative0: Applicative G A, A': Type ϕ: A -> G A' B, C: Type rest: Batch A B (B -> C) a: A IHrest: traverse ϕ rest =
runBatch (map G (batch A' B) ∘ ϕ) rest
map G Step (runBatch (map G (batch A' B) ∘ ϕ) rest) <⋆>
ϕ a =
runBatch (map G (batch A' B) ∘ ϕ) rest <⋆>
map G (batch A' B) (ϕ a)
G: Type -> Type H: Map G H0: Mult G H1: Pure G Applicative0: Applicative G A, A': Type ϕ: A -> G A' B, C: Type rest: Batch A B (B -> C) a: A IHrest: traverse ϕ rest =
runBatch (map G (batch A' B) ∘ ϕ) rest
map G Step (runBatch (map G (batch A' B) ∘ ϕ) rest) <⋆>
ϕ a =
map G (ap (Batch A' B))
(runBatch (map G (batch A' B) ∘ ϕ) rest) <⋆>
map G (batch A' B) (ϕ a)
G: Type -> Type H: Map G H0: Mult G H1: Pure G Applicative0: Applicative G A, A': Type ϕ: A -> G A' B, C: Type rest: Batch A B (B -> C) a: A IHrest: traverse ϕ rest =
runBatch (map G (batch A' B) ∘ ϕ) rest
map G Step (runBatch (map G (batch A' B) ∘ ϕ) rest) <⋆>
ϕ a =
map G (precompose (batch A' B))
(map G (ap (Batch A' B))
(runBatch (map G (batch A' B) ∘ ϕ) rest)) <⋆>
ϕ a
G: Type -> Type H: Map G H0: Mult G H1: Pure G Applicative0: Applicative G A, A': Type ϕ: A -> G A' B, C: Type rest: Batch A B (B -> C) a: A IHrest: traverse ϕ rest =
runBatch (map G (batch A' B) ∘ ϕ) rest
map G Step (runBatch (map G (batch A' B) ∘ ϕ) rest) <⋆>
ϕ a =
(map G (precompose (batch A' B))
∘ map G (ap (Batch A' B)))
(runBatch (map G (batch A' B) ∘ ϕ) rest) <⋆> ϕ a
G: Type -> Type H: Map G H0: Mult G H1: Pure G Applicative0: Applicative G A, A': Type ϕ: A -> G A' B, C: Type rest: Batch A B (B -> C) a: A IHrest: traverse ϕ rest =
runBatch (map G (batch A' B) ∘ ϕ) rest
map G Step (runBatch (map G (batch A' B) ∘ ϕ) rest) <⋆>
ϕ a =
map G (precompose (batch A' B) ∘ ap (Batch A' B))
(runBatch (map G (batch A' B) ∘ ϕ) rest) <⋆> ϕ a
G: Type -> Type H: Map G H0: Mult G H1: Pure G Applicative0: Applicative G A, A': Type ϕ: A -> G A' B, C: Type rest: Batch A B (B -> C) a: A IHrest: traverse ϕ rest =
runBatch (map G (batch A' B) ∘ ϕ) rest
Step = precompose (batch A' B) ∘ ap (Batch A' B)
G: Type -> Type H: Map G H0: Mult G H1: Pure G Applicative0: Applicative G A, A': Type ϕ: A -> G A' B, C: Type rest: Batch A B (B -> C) a: A IHrest: traverse ϕ rest =
runBatch (map G (batch A' B) ∘ ϕ) rest b: Batch A' B (B -> C)
Step b = (precompose (batch A' B) ∘ ap (Batch A' B)) b
G: Type -> Type H: Map G H0: Mult G H1: Pure G Applicative0: Applicative G A, A': Type ϕ: A -> G A' B, C: Type rest: Batch A B (B -> C) a: A IHrest: traverse ϕ rest =
runBatch (map G (batch A' B) ∘ ϕ) rest b: Batch A' B (B -> C)
Step b =
(funX : A' =>
map (Batch A' B) (fun '(f, a) => f a)
(b ⊗ batch A' B X))
G: Type -> Type H: Map G H0: Mult G H1: Pure G Applicative0: Applicative G A, A': Type ϕ: A -> G A' B, C: Type rest: Batch A B (B -> C) a: A IHrest: traverse ϕ rest =
runBatch (map G (batch A' B) ∘ ϕ) rest b: Batch A' B (B -> C)
Step b =
(funX : A' =>
map (Batch A' B) (compose (fun '(f, a) => f a))
(map (Batch A' B) strength_arrow
(map (Batch A' B) (func : B -> C => (c, id)) b))
⧆ X)
G: Type -> Type H: Map G H0: Mult G H1: Pure G Applicative0: Applicative G A, A': Type ϕ: A -> G A' B, C: Type rest: Batch A B (B -> C) a: A IHrest: traverse ϕ rest =
runBatch (map G (batch A' B) ∘ ϕ) rest b: Batch A' B (B -> C)
Step b =
(funX : A' =>
map (Batch A' B) (compose (fun '(f, a) => f a))
((map (Batch A' B) strength_arrow
∘ map (Batch A' B) (func : B -> C => (c, id))) b)
⧆ X)
G: Type -> Type H: Map G H0: Mult G H1: Pure G Applicative0: Applicative G A, A': Type ϕ: A -> G A' B, C: Type rest: Batch A B (B -> C) a: A IHrest: traverse ϕ rest =
runBatch (map G (batch A' B) ∘ ϕ) rest b: Batch A' B (B -> C)
Step b =
(funX : A' =>
map (Batch A' B) (compose (fun '(f, a) => f a))
(map (Batch A' B)
(strength_arrow ∘ (func : B -> C => (c, id))) b)
⧆ X)
G: Type -> Type H: Map G H0: Mult G H1: Pure G Applicative0: Applicative G A, A': Type ϕ: A -> G A' B, C: Type rest: Batch A B (B -> C) a: A IHrest: traverse ϕ rest =
runBatch (map G (batch A' B) ∘ ϕ) rest b: Batch A' B (B -> C)
Step b =
(funX : A' =>
(map (Batch A' B) (compose (fun '(f, a) => f a))
∘ map (Batch A' B)
(strength_arrow ∘ (func : B -> C => (c, id))))
b ⧆ X)
G: Type -> Type H: Map G H0: Mult G H1: Pure G Applicative0: Applicative G A, A': Type ϕ: A -> G A' B, C: Type rest: Batch A B (B -> C) a: A IHrest: traverse ϕ rest =
runBatch (map G (batch A' B) ∘ ϕ) rest b: Batch A' B (B -> C)
Step b =
(funX : A' =>
map (Batch A' B)
(compose (fun '(f, a) => f a)
∘ (strength_arrow ∘ (func : B -> C => (c, id))))
b ⧆ X)
G: Type -> Type H: Map G H0: Mult G H1: Pure G Applicative0: Applicative G A, A': Type ϕ: A -> G A' B, C: Type rest: Batch A B (B -> C) a: A IHrest: traverse ϕ rest =
runBatch (map G (batch A' B) ∘ ϕ) rest b: Batch A' B (B -> C)
Step b =
(funX : A' =>
map (Batch A' B)
(fun (a : B -> C) (a0 : B) =>
let '(f, a1) := strength_arrow (a, id) a0 in f a1)
b ⧆ X)
G: Type -> Type H: Map G H0: Mult G H1: Pure G Applicative0: Applicative G A, A': Type ϕ: A -> G A' B, C: Type rest: Batch A B (B -> C) a: A IHrest: traverse ϕ rest =
runBatch (map G (batch A' B) ∘ ϕ) rest b: Batch A' B (B -> C)
Step b =
(funX : A' =>
map (Batch A' B) (funa : B -> C => a ○ id) b ⧆ X)
G: Type -> Type H: Map G H0: Mult G H1: Pure G Applicative0: Applicative G A, A': Type ϕ: A -> G A' B, C: Type rest: Batch A B (B -> C) a: A IHrest: traverse ϕ rest =
runBatch (map G (batch A' B) ∘ ϕ) rest b: Batch A' B (B -> C)
b = map (Batch A' B) (funa : B -> C => a ○ id) b
G: Type -> Type H: Map G H0: Mult G H1: Pure G Applicative0: Applicative G A, A': Type ϕ: A -> G A' B, C: Type rest: Batch A B (B -> C) a: A IHrest: traverse ϕ rest =
runBatch (map G (batch A' B) ∘ ϕ) rest b: Batch A' B (B -> C)
b = map (Batch A' B) (funa : B -> C => a) b
G: Type -> Type H: Map G H0: Mult G H1: Pure G Applicative0: Applicative G A, A': Type ϕ: A -> G A' B, C: Type rest: Batch A B (B -> C) a: A IHrest: traverse ϕ rest =
runBatch (map G (batch A' B) ∘ ϕ) rest b: Batch A' B (B -> C)
b = id b
reflexivity.Qed.(** * <<Batch _ B C>> is a traversable monad *)(******************************************************************************)(** ** Operation *)(******************************************************************************)Definitionbindt_Batch (BC: Type) (G: Type -> Type)
`{Map G} `{Pure G} `{Mult G} (A A': Type) (f: A -> G (Batch A' B B))
(b: Batch A B B): G (Batch A' B B) :=
map G join_Batch (traverse (T := BATCH1 B B) f b).(** ** Traversable Monad Laws *)(** TODO *)(** * Deconstructing <<Batch A B C>> into Shape and Contents *)(******************************************************************************)Sectiondeconstruction.#[local] Generalizable Variablesn v a.(** ** <<Batch_make>> and <<Batch_contents>> *)(******************************************************************************)(** Extract the contents of <<Batch>> as a vector *)FixpointBatch_contents `(b: Batch A B C):
Vector (length_Batch b) A :=
match b with
| Done c => vnil
| Step b a => vcons (length_Batch b) a (Batch_contents b)
end.(** Obtain the build function of <<Batch>>. Note that <<Batch_make b v>> in general has type <<C>>, not another <<Batch>>. That is, this is not <<make>> in the sense of <<put>> *)FixpointBatch_make `(b: Batch A B C):
Vector (length_Batch b) B -> C :=
match b return Vector (length_Batch b) B -> C with
| Done c => funv => c
| Step b a => funv =>
Batch_make b (Vector_tl v) (Vector_hd v)
end.(** ** <<Batch_replace_contents>> *)(** This is <<make>> in the sense of <<put>>. *)(******************************************************************************)FixpointBatch_replace_contents
`(b: Batch A B C)
`(v: Vector (length_Batch b) A')
: Batch A' B C :=
match b return (Vector (length_Batch b) A' -> Batch A' B C) with
| Done c =>
funv => Done c
| Step rest a =>
funv =>
Step (Batch_replace_contents rest (Vector_tl v))
(Vector_hd v)
end v.(** ** Rewriting rules *)(******************************************************************************)Sectionrw.Context {ABC: Type}.Implicit Types (a: A) (b: Batch A B (B -> C)) (c: C).
A, B, C: Type c: C
Batch_contents (Done c) = vnil
A, B, C: Type c: C
Batch_contents (Done c) = vnil
reflexivity.Qed.
A, B, C: Type b: Batch A B (B -> C) a: A
Batch_contents (b ⧆ a) =
vcons (length_Batch b) a (Batch_contents b)
A, B, C: Type b: Batch A B (B -> C) a: A
Batch_contents (b ⧆ a) =
vcons (length_Batch b) a (Batch_contents b)
reflexivity.Qed.
A, B, C: Type c: C
Batch_make (Done c) = const c
A, B, C: Type c: C
Batch_make (Done c) = const c
reflexivity.Qed.
A, B, C: Type b: Batch A B (B -> C) a: A
Batch_make (b ⧆ a) =
(funv : Vector (length_Batch (b ⧆ a)) B =>
Batch_make b (Vector_tl v) (Vector_hd v))
A, B, C: Type b: Batch A B (B -> C) a: A
Batch_make (b ⧆ a) =
(funv : Vector (length_Batch (b ⧆ a)) B =>
Batch_make b (Vector_tl v) (Vector_hd v))
reflexivity.Qed.
A, B, C: Type c: C A': Type v: Vector (length_Batch (Done c)) A'
Batch_replace_contents (Done c) v = Done c
A, B, C: Type c: C A': Type v: Vector (length_Batch (Done c)) A'
Batch_replace_contents (Done c) v = Done c
reflexivity.Qed.
A, B, C: Type b: Batch A B (B -> C) a: A A': Type v: Vector (length_Batch (b ⧆ a)) A'
Batch_replace_contents (b ⧆ a) v =
Batch_replace_contents b (Vector_tl v) ⧆ Vector_hd v
A, B, C: Type b: Batch A B (B -> C) a: A A': Type v: Vector (length_Batch (b ⧆ a)) A'
Batch_replace_contents (b ⧆ a) v =
Batch_replace_contents b (Vector_tl v) ⧆ Vector_hd v
reflexivity.Qed.Endrw.(** ** Relating <<tolist>> and <<Batch_contents>> *)(******************************************************************************)Ltachide_rhs :=
match goal with
| |- ?lhs = ?rhs =>
letname := fresh"rhs"inremember rhs as name
end.
A, B, C: Type
forallb : Batch A B C,
proj1_sig (Batch_contents b) = List.rev (tolist b)
A, B, C: Type
forallb : Batch A B C,
proj1_sig (Batch_contents b) = List.rev (tolist b)
A, B, C: Type b: Batch A B C
proj1_sig (Batch_contents b) = List.rev (tolist b)
A, B, X, Y: Type f: Batch A B (X -> Y) x: Batch A B X
List.rev (mapReduce (ret list A) (f <⋆> x)) =
proj1_sig
(Vector_append (Batch_contents x) (Batch_contents f))
A, B, X, Y: Type f: Batch A B (X -> Y) x: Batch A B X
List.rev (mapReduce (ret list A) (f <⋆> x)) =
proj1_sig (Batch_contents x) ++
proj1_sig (Batch_contents f)
A, B, X, Y: Type f: Batch A B (X -> Y) x: Batch A B X
List.rev
(mapReduce (ret list A) f ● mapReduce (ret list A) x) =
proj1_sig (Batch_contents x) ++
proj1_sig (Batch_contents f)
A, B, X, Y: Type f: Batch A B (X -> Y) x: Batch A B X
List.rev
(mapReduce (ret list A) f ++
mapReduce (ret list A) x) =
proj1_sig (Batch_contents x) ++
proj1_sig (Batch_contents f)
A, B, X, Y: Type f: Batch A B (X -> Y) x: Batch A B X
List.rev (mapReduce (ret list A) x) ++
List.rev (mapReduce (ret list A) f) =
proj1_sig (Batch_contents x) ++
proj1_sig (Batch_contents f)
A, B, X, Y: Type f: Batch A B (X -> Y) x: Batch A B X
List.rev (mapReduce (ret list A) x) ++
List.rev (mapReduce (ret list A) f) =
List.rev (tolist x) ++ proj1_sig (Batch_contents f)
A, B, X, Y: Type f: Batch A B (X -> Y) x: Batch A B X
List.rev (mapReduce (ret list A) x) ++
List.rev (mapReduce (ret list A) f) =
List.rev (tolist x) ++ List.rev (tolist f)
reflexivity.Qed.Endrewrite_Batch_contents.(** ** Same Shape Iff Same <<Batch_make>> *)(******************************************************************************)
forall (A1BC : Type) (b1 : Batch A1 B C) (A2 : Type)
(b2 : Batch A2 B C),
shape b1 = shape b2 -> Batch_make b1 ~!~ Batch_make b2
forall (A1BC : Type) (b1 : Batch A1 B C) (A2 : Type)
(b2 : Batch A2 B C),
shape b1 = shape b2 -> Batch_make b1 ~!~ Batch_make b2
A1, B, C: Type b1: Batch A1 B C A2: Type b2: Batch A2 B C Hshape: shape b1 = shape b2
Batch_make b1 ~!~ Batch_make b2
A1, B, C: Type b1: Batch A1 B C A2: Type b2: Batch A2 B C Hshape: shape b1 = shape b2
forall (C : Type) (c : C),
Batch_make (Done c) ~!~ Batch_make (Done c)
A1, B, C: Type b1: Batch A1 B C A2: Type b2: Batch A2 B C Hshape: shape b1 = shape b2
split; auto using Batch_make_shape,
Batch_make_shape_rev.Qed.(** ** Two Lemmas for <<shape>> and <<length_Batch>> *)(******************************************************************************)
forall (ABC : Type) (b : Batch A B C),
shape b =
Batch_replace_contents b (Vector_tt (length_Batch b))
forall (ABC : Type) (b : Batch A B C),
shape b =
Batch_replace_contents b (Vector_tt (length_Batch b))
A, B, C: Type b: Batch A B C
shape b =
Batch_replace_contents b (Vector_tt (length_Batch b))
A, B, C: Type c: C
shape (Done c) =
Batch_replace_contents (Done c)
(Vector_tt (length_Batch (Done c)))
A, B, C: Type b: Batch A B (B -> C) a: A IHb: shape b = Batch_replace_contents b (Vector_tt (length_Batch b))
shape (b ⧆ a) =
Batch_replace_contents (b ⧆ a)
(Vector_tt (length_Batch (b ⧆ a)))
A, B, C: Type c: C
shape (Done c) =
Batch_replace_contents (Done c)
(Vector_tt (length_Batch (Done c)))
reflexivity.
A, B, C: Type b: Batch A B (B -> C) a: A IHb: shape b = Batch_replace_contents b (Vector_tt (length_Batch b))
shape (b ⧆ a) =
Batch_replace_contents (b ⧆ a)
(Vector_tt (length_Batch (b ⧆ a)))
A, B, C: Type b: Batch A B (B -> C) a: A IHb: shape b = Batch_replace_contents b (Vector_tt (length_Batch b))
mapfst_Batch (const tt) b ⧆ const tt a =
Batch_replace_contents b
(Vector_tl
(vcons (length_Batch b) tt
(Vector_repeat (length_Batch b) tt)))
⧆ Vector_hd
(vcons (length_Batch b) tt
(Vector_repeat (length_Batch b) tt))
A, B, C: Type b: Batch A B (B -> C) a: A IHb: shape b = Batch_replace_contents b (Vector_tt (length_Batch b))
mapfst_Batch (const tt) b ⧆ const tt a =
Batch_replace_contents b
(Vector_repeat (length_Batch b) tt)
⧆ Vector_hd
(vcons (length_Batch b) tt
(Vector_repeat (length_Batch b) tt))
A, B, C: Type b: Batch A B (B -> C) a: A IHb: shape b = Batch_replace_contents b (Vector_tt (length_Batch b))
mapfst_Batch (const tt) b ⧆ const tt a =
Batch_replace_contents b
(Vector_repeat (length_Batch b) tt) ⧆ tt
A, B, C: Type b: Batch A B (B -> C) a: A IHb: shape b = Batch_replace_contents b (Vector_tt (length_Batch b))
mapfst_Batch (const tt) b =
Batch_replace_contents b
(Vector_repeat (length_Batch b) tt)
A1, B, C: Type b1: Batch A1 B C A2: Type b2: Batch A2 B C H: forallA' : Type,
Batch_replace_contents b1 ~!~
Batch_replace_contents b2
length_Batch b1 = length_Batch b2
A1, B, C: Type b1: Batch A1 B C A2: Type b2: Batch A2 B C H: forallA' : Type,
Batch_replace_contents b1 ~!~
Batch_replace_contents b2
?f ~!~ ?g
apply (H False).Qed.(** ** Same Shape Implies Same <<Batch_replace_contents>> *)(******************************************************************************)
reflexivity.Qed.(** ** Similarity Lemmas for <<Batch_make>> *)(******************************************************************************)
A, B, C: Type b: Batch A B C v1, v2: Vector (length_Batch b) B Hsim: v1 ~~ v2
Batch_make b v1 = Batch_make b v2
A, B, C: Type b: Batch A B C v1, v2: Vector (length_Batch b) B Hsim: v1 ~~ v2
Batch_make b v1 = Batch_make b v2
A, B, C: Type b: Batch A B C v1, v2: Vector (length_Batch b) B Hsim: v1 = v2
Batch_make b v1 = Batch_make b v2
nowsubst.Qed.(* This sort of lemma is very useful when the complexity of expression <<v1>> and <<v2>> obstructs tactics like <<rewrite>> *)
A, B, C: Type b1, b2: Batch A B C v1: Vector (length_Batch b1) B v2: Vector (length_Batch b2) B Heq: b1 = b2 Hsim: v1 ~~ v2
Batch_make b1 v1 = Batch_make b2 v2
A, B, C: Type b1, b2: Batch A B C v1: Vector (length_Batch b1) B v2: Vector (length_Batch b2) B Heq: b1 = b2 Hsim: v1 ~~ v2
Batch_make b1 v1 = Batch_make b2 v2
A, B, C: Type b2: Batch A B C v1, v2: Vector (length_Batch b2) B Hsim: v1 ~~ v2
Batch_make b2 v1 = Batch_make b2 v2
now (subst; apply Batch_make_sim1).Qed.
A1, B, C: Type b1: Batch A1 B C A2: Type b2: Batch A2 B C v1: Vector (length_Batch b1) B v2: Vector (length_Batch b2) B Heq: shape b1 = shape b2 Hsim: v1 ~~ v2
Batch_make b1 v1 = Batch_make b2 v2
A1, B, C: Type b1: Batch A1 B C A2: Type b2: Batch A2 B C v1: Vector (length_Batch b1) B v2: Vector (length_Batch b2) B Heq: shape b1 = shape b2 Hsim: v1 ~~ v2
Batch_make b1 v1 = Batch_make b2 v2
A1, B, C: Type b1: Batch A1 B C A2: Type b2: Batch A2 B C v1: Vector (length_Batch b1) B v2: Vector (length_Batch b2) B Heq: shape b1 = shape b2 Hsim: v1 ~~ v2
Batch_make b1 ~!~ Batch_make b2
A1, B, C: Type b1: Batch A1 B C A2: Type b2: Batch A2 B C v1: Vector (length_Batch b1) B v2: Vector (length_Batch b2) B Heq: shape b1 = shape b2 Hsim: v1 ~~ v2
v1 ~~ v2
A1, B, C: Type b1: Batch A1 B C A2: Type b2: Batch A2 B C v1: Vector (length_Batch b1) B v2: Vector (length_Batch b2) B Heq: shape b1 = shape b2 Hsim: v1 ~~ v2
shape b1 = shape b2
A1, B, C: Type b1: Batch A1 B C A2: Type b2: Batch A2 B C v1: Vector (length_Batch b1) B v2: Vector (length_Batch b2) B Heq: shape b1 = shape b2 Hsim: v1 ~~ v2
v1 ~~ v2
A1, B, C: Type b1: Batch A1 B C A2: Type b2: Batch A2 B C v1: Vector (length_Batch b1) B v2: Vector (length_Batch b2) B Heq: shape b1 = shape b2 Hsim: v1 ~~ v2
v1 ~~ v2
assumption.Qed.
A, B, C: Type b: Batch A B C v1: Vector (length_Batch b) B n: nat v2: Vector n B Heq: n = length_Batch b
v1 ~~ v2 ->
Batch_make b v1 = Batch_make b (coerce Heq in v2)
A, B, C: Type b: Batch A B C v1: Vector (length_Batch b) B n: nat v2: Vector n B Heq: n = length_Batch b
v1 ~~ v2 ->
Batch_make b v1 = Batch_make b (coerce Heq in v2)
A, B, C: Type b: Batch A B C v1, v2: Vector (length_Batch b) B
v1 ~~ v2 ->
Batch_make b v1 = Batch_make b (coerce eq_refl in v2)
A, B, C: Type b: Batch A B C v1, v2: Vector (length_Batch b) B H: v1 ~~ v2
Batch_make b v1 = Batch_make b (coerce eq_refl in v2)
A, B, C: Type b: Batch A B C v1, v2: Vector (length_Batch b) B H: v1 ~~ v2
Batch_make b v1 = Batch_make b v2
A, B, C: Type b: Batch A B C v1, v2: Vector (length_Batch b) B H: v1 ~~ v2
v1 ~~ v2
assumption.Qed.(** Rewrite the <<Batch>> argument to an equal one by coercing the length proof in the vector. *)
A, B, C: Type b1, b2: Batch A B C v: Vector (length_Batch b1) B Heq: b1 = b2
Batch_make b1 v =
Batch_make b2
(rew [funb : Batch A B C =>
Vector (length_Batch b) B] Heq in v)
A, B, C: Type b1, b2: Batch A B C v: Vector (length_Batch b1) B Heq: b1 = b2
Batch_make b1 v =
Batch_make b2
(rew [funb : Batch A B C =>
Vector (length_Batch b) B] Heq in v)
now (subst; apply Batch_make_sim1).Qed.
A, B, C: Type b1, b2: Batch A B C v: Vector (length_Batch b1) B Heq: b1 = b2
Batch_make b1 v =
Batch_make b2
(coerce eq_ind_r
(funz : Batch A B C =>
length_Batch z = length_Batch b2) eq_refl
Heq in v)
A, B, C: Type b1, b2: Batch A B C v: Vector (length_Batch b1) B Heq: b1 = b2
Batch_make b1 v =
Batch_make b2
(coerce eq_ind_r
(funz : Batch A B C =>
length_Batch z = length_Batch b2) eq_refl
Heq in v)
A, B, C: Type b2: Batch A B C v: Vector (length_Batch b2) B
Batch_make b2 v =
Batch_make b2
(coerce eq_ind_r
(funz : Batch A B C =>
length_Batch z = length_Batch b2) eq_refl
eq_refl in v)
A, B, C: Type b2: Batch A B C v: Vector (length_Batch b2) B
Batch_make b2 v = Batch_make b2 (coerce eq_refl in v)
nowrewrite coerce_Vector_eq_refl.Qed.(** ** Similarity Laws for <<Batch_replace_contents>> *)(******************************************************************************)
A, B, C: Type b: Batch A B C A': Type v1, v2: Vector (length_Batch b) A' Hsim: v1 ~~ v2
Batch_replace_contents b v1 =
Batch_replace_contents b v2
A, B, C: Type b: Batch A B C A': Type v1, v2: Vector (length_Batch b) A' Hsim: v1 ~~ v2
Batch_replace_contents b v1 =
Batch_replace_contents b v2
A, B, C: Type c: C A': Type v1, v2: Vector (length_Batch (Done c)) A' Hsim: v1 ~~ v2
Batch_replace_contents (Done c) v1 =
Batch_replace_contents (Done c) v2
A, B, C: Type b: Batch A B (B -> C) a: A A': Type v1, v2: Vector (length_Batch (b ⧆ a)) A' Hsim: v1 ~~ v2 IHb: forallv1v2 : Vector (length_Batch b) A',
v1 ~~ v2 ->
Batch_replace_contents b v1 =
Batch_replace_contents b v2
Batch_replace_contents (b ⧆ a) v1 =
Batch_replace_contents (b ⧆ a) v2
A, B, C: Type c: C A': Type v1, v2: Vector (length_Batch (Done c)) A' Hsim: v1 ~~ v2
Batch_replace_contents (Done c) v1 =
Batch_replace_contents (Done c) v2
reflexivity.
A, B, C: Type b: Batch A B (B -> C) a: A A': Type v1, v2: Vector (length_Batch (b ⧆ a)) A' Hsim: v1 ~~ v2 IHb: forallv1v2 : Vector (length_Batch b) A',
v1 ~~ v2 ->
Batch_replace_contents b v1 =
Batch_replace_contents b v2
Batch_replace_contents (b ⧆ a) v1 =
Batch_replace_contents (b ⧆ a) v2
A, B, C: Type b: Batch A B (B -> C) a: A A': Type v1, v2: Vector (length_Batch (b ⧆ a)) A' Hsim: v1 ~~ v2 IHb: forallv1v2 : Vector (length_Batch b) A',
v1 ~~ v2 ->
Batch_replace_contents b v1 =
Batch_replace_contents b v2
Batch_replace_contents b (Vector_tl v1) ⧆ Vector_hd v1 =
Batch_replace_contents b (Vector_tl v2) ⧆ Vector_hd v2
A, B, C: Type b: Batch A B (B -> C) a: A A': Type v1, v2: Vector (length_Batch (b ⧆ a)) A' Hsim: v1 ~~ v2 IHb: forallv1v2 : Vector (length_Batch b) A',
v1 ~~ v2 ->
Batch_replace_contents b v1 =
Batch_replace_contents b v2
Batch_replace_contents b (Vector_tl v2) ⧆ Vector_hd v1 =
Batch_replace_contents b (Vector_tl v2) ⧆ Vector_hd v2
A, B, C: Type b: Batch A B (B -> C) a: A A': Type v1, v2: Vector (length_Batch (b ⧆ a)) A' Hsim: v1 ~~ v2 IHb: forallv1v2 : Vector (length_Batch b) A',
v1 ~~ v2 ->
Batch_replace_contents b v1 =
Batch_replace_contents b v2
Batch_replace_contents b (Vector_tl v2) ⧆ Vector_hd v2 =
Batch_replace_contents b (Vector_tl v2) ⧆ Vector_hd v2
reflexivity.Qed.
A, B, C: Type b1, b2: Batch A B C A': Type v1: Vector (length_Batch b1) A' v2: Vector (length_Batch b2) A' Heq: b1 = b2 Hsim: v1 ~~ v2
A1, B, C: Type b1: Batch A1 B C A2: Type b2: Batch A2 B C A': Type v1: Vector (length_Batch b1) A' v2: Vector (length_Batch b2) A' Heq: shape b1 = shape b2 Hsim: v1 ~~ v2
A1, B, C: Type b1: Batch A1 B C A2: Type b2: Batch A2 B C A': Type v1: Vector (length_Batch b1) A' v2: Vector (length_Batch b2) A' Heq: shape b1 = shape b2 Hsim: v1 ~~ v2
A1, B, C: Type b1: Batch A1 B C A2: Type b2: Batch A2 B C A': Type v1: Vector (length_Batch b1) A' v2: Vector (length_Batch b2) A' Heq: shape b1 = shape b2 Hsim: v1 ~~ v2
nowapply Batch_replace_contents_shape_iff.Qed.(** ** Naturality of <<Batch_make>> *)(******************************************************************************)
A, B, C: Type b: Batch A B C D: Type f: C -> D v1: Vector (length_Batch b) B v2: Vector (length_Batch (map (Batch A B) f b)) B Hsim: v1 ~~ v2
f (Batch_make b v1) =
Batch_make (map (Batch A B) f b) v2
A, B, C: Type b: Batch A B C D: Type f: C -> D v1: Vector (length_Batch b) B v2: Vector (length_Batch (map (Batch A B) f b)) B Hsim: v1 ~~ v2
f (Batch_make b v1) =
Batch_make (map (Batch A B) f b) v2
A, B, C: Type b: Batch A B C D: Type f: C -> D v1: Vector (length_Batch b) B
forallv2 : Vector (length_Batch (map (Batch A B) f b)) B,
v1 ~~ v2 ->
f (Batch_make b v1) =
Batch_make (map (Batch A B) f b) v2
A, B, C: Type b: Batch A B C D: Type f: C -> D
forall (v1 : Vector (length_Batch b) B)
(v2 : Vector (length_Batch (map (Batch A B) f b)) B),
v1 ~~ v2 ->
f (Batch_make b v1) =
Batch_make (map (Batch A B) f b) v2
A, B, C: Type b: Batch A B C
forall (D : Type) (f : C -> D)
(v1 : Vector (length_Batch b) B)
(v2 : Vector (length_Batch (map (Batch A B) f b)) B),
v1 ~~ v2 ->
f (Batch_make b v1) =
Batch_make (map (Batch A B) f b) v2
A, B, C: Type c: C
forall (D : Type) (f : C -> D)
(v1 : Vector (length_Batch (Done c)) B)
(v2 : Vector
(length_Batch (map (Batch A B) f (Done c)))
B),
v1 ~~ v2 ->
f (Batch_make (Done c) v1) =
Batch_make (map (Batch A B) f (Done c)) v2
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: forall (D : Type) (f : (B -> C) -> D)
(v1 : Vector (length_Batch rest) B)
(v2 : Vector
(length_Batch
(map (Batch A B) f rest)) B),
v1 ~~ v2 ->
f (Batch_make rest v1) =
Batch_make (map (Batch A B) f rest) v2
forall (D : Type) (f : C -> D)
(v1 : Vector (length_Batch (rest ⧆ a)) B)
(v2 : Vector
(length_Batch (map (Batch A B) f (rest ⧆ a)))
B),
v1 ~~ v2 ->
f (Batch_make (rest ⧆ a) v1) =
Batch_make (map (Batch A B) f (rest ⧆ a)) v2
A, B, C: Type c: C
forall (D : Type) (f : C -> D)
(v1 : Vector (length_Batch (Done c)) B)
(v2 : Vector
(length_Batch (map (Batch A B) f (Done c)))
B),
v1 ~~ v2 ->
f (Batch_make (Done c) v1) =
Batch_make (map (Batch A B) f (Done c)) v2
reflexivity.
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: forall (D : Type) (f : (B -> C) -> D)
(v1 : Vector (length_Batch rest) B)
(v2 : Vector
(length_Batch
(map (Batch A B) f rest)) B),
v1 ~~ v2 ->
f (Batch_make rest v1) =
Batch_make (map (Batch A B) f rest) v2
forall (D : Type) (f : C -> D)
(v1 : Vector (length_Batch (rest ⧆ a)) B)
(v2 : Vector
(length_Batch (map (Batch A B) f (rest ⧆ a)))
B),
v1 ~~ v2 ->
f (Batch_make (rest ⧆ a) v1) =
Batch_make (map (Batch A B) f (rest ⧆ a)) v2
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: forall (D : Type) (f : (B -> C) -> D)
(v1 : Vector (length_Batch rest) B)
(v2 : Vector
(length_Batch
(map (Batch A B) f rest)) B),
v1 ~~ v2 ->
f (Batch_make rest v1) =
Batch_make (map (Batch A B) f rest) v2 D: Type f: C -> D v1: Vector (length_Batch (rest ⧆ a)) B v2: Vector
(length_Batch (map (Batch A B) f (rest ⧆ a))) B Hsim: v1 ~~ v2
f (Batch_make (rest ⧆ a) v1) =
Batch_make (map (Batch A B) f (rest ⧆ a)) v2
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: forall (D : Type) (f : (B -> C) -> D)
(v1 : Vector (length_Batch rest) B)
(v2 : Vector
(length_Batch
(map (Batch A B) f rest)) B),
v1 ~~ v2 ->
f (Batch_make rest v1) =
Batch_make (map (Batch A B) f rest) v2 D: Type f: C -> D v1: Vector (length_Batch (rest ⧆ a)) B v2: Vector
(length_Batch
(map (Batch A B) (compose f) rest ⧆ a)) B Hsim: v1 ~~ v2
f (Batch_make (rest ⧆ a) v1) =
Batch_make (map (Batch A B) (compose f) rest ⧆ a) v2
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: forall (D : Type) (f : (B -> C) -> D)
(v1 : Vector (length_Batch rest) B)
(v2 : Vector
(length_Batch
(map (Batch A B) f rest)) B),
v1 ~~ v2 ->
f (Batch_make rest v1) =
Batch_make (map (Batch A B) f rest) v2 D: Type f: C -> D v1: Vector (S (length_Batch rest)) B v2: Vector
(S
(length_Batch
(map (Batch A B) (compose f) rest))) B Hsim: v1 ~~ v2
f (Batch_make (rest ⧆ a) v1) =
Batch_make (map (Batch A B) (compose f) rest ⧆ a) v2
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: forall (D : Type) (f : (B -> C) -> D)
(v1 : Vector (length_Batch rest) B)
(v2 : Vector
(length_Batch
(map (Batch A B) f rest)) B),
v1 ~~ v2 ->
f (Batch_make rest v1) =
Batch_make (map (Batch A B) f rest) v2 D: Type f: C -> D v1: Vector (S (length_Batch rest)) B v2: Vector
(S
(length_Batch
(map (Batch A B) (compose f) rest))) B Hsim: v1 ~~ v2
f (Batch_make rest (Vector_tl v1) (Vector_hd v1)) =
Batch_make (map (Batch A B) (compose f) rest)
(Vector_tl v2) (Vector_hd v2)
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: forall (D : Type) (f : (B -> C) -> D)
(v1 : Vector (length_Batch rest) B)
(v2 : Vector
(length_Batch
(map (Batch A B) f rest)) B),
v1 ~~ v2 ->
f (Batch_make rest v1) =
Batch_make (map (Batch A B) f rest) v2 D: Type f: C -> D v1: Vector (S (length_Batch rest)) B v2: Vector
(S
(length_Batch
(map (Batch A B) (compose f) rest))) B Hsim: v1 ~~ v2
f (Batch_make rest (Vector_tl v1) (Vector_hd v1)) =
Batch_make (map (Batch A B) (compose f) rest)
(Vector_tl v2) (Vector_hd v1)
A, B, C: Type rest: Batch A B (B -> C) a: A IHrest: forall (D : Type) (f : (B -> C) -> D)
(v1 : Vector (length_Batch rest) B)
(v2 : Vector
(length_Batch
(map (Batch A B) f rest)) B),
v1 ~~ v2 ->
f (Batch_make rest v1) =
Batch_make (map (Batch A B) f rest) v2 D: Type f: C -> D v1: Vector (S (length_Batch rest)) B v2: Vector
(S
(length_Batch
(map (Batch A B) (compose f) rest))) B Hsim: v1 ~~ v2
A, B, C: Type rest: Batch A B (B -> C) a: A D: Type f: C -> D IHrest: forall (v1 : Vector (length_Batch rest) B)
(v2 : Vector
(length_Batch
(map (Batch A B)
(compose f) rest)) B),
v1 ~~ v2 ->
f ∘ Batch_make rest v1 =
Batch_make (map (Batch A B) (compose f) rest)
v2 v1: Vector (S (length_Batch rest)) B v2: Vector
(S
(length_Batch
(map (Batch A B) (compose f) rest))) B Hsim: v1 ~~ v2
A, B, C: Type rest: Batch A B (B -> C) a: A D: Type f: C -> D IHrest: forall (v1 : Vector (length_Batch rest) B)
(v2 : Vector
(length_Batch
(map (Batch A B)
(compose f) rest)) B),
v1 ~~ v2 ->
f ∘ Batch_make rest v1 =
Batch_make (map (Batch A B) (compose f) rest)
v2 v1: Vector (S (length_Batch rest)) B v2: Vector
(S
(length_Batch
(map (Batch A B) (compose f) rest))) B Hsim: v1 ~~ v2
Batch_make (map (Batch A B) (compose f) rest)
(Vector_tl v2) (Vector_hd v1) =
Batch_make (map (Batch A B) (compose f) rest)
(Vector_tl v2) (Vector_hd v1)
reflexivity.Qed.
A, B, C: Type b: Batch A B C D: Type f: C -> D v: Vector (length_Batch b) B
f (Batch_make b v) =
Batch_make (map (Batch A B) f b)
(coerce batch_length_map f b in v)
A, B, C: Type b: Batch A B C D: Type f: C -> D v: Vector (length_Batch b) B
f (Batch_make b v) =
Batch_make (map (Batch A B) f b)
(coerce batch_length_map f b in v)
nowrewrite (
Batch_make_natural
b f
(v1 := v)
(v2 :=coerce_Vector_length (batch_length_map _ _) v)
) by vector_sim.Qed.
A, B, C: Type b: Batch A B C D: Type f: C -> D v: Vector (length_Batch (map (Batch A B) f b)) B
Batch_make (map (Batch A B) f b) v =
f
(Batch_make b
(coerce eq_sym (batch_length_map f b) in v))
A, B, C: Type b: Batch A B C D: Type f: C -> D v: Vector (length_Batch (map (Batch A B) f b)) B
Batch_make (map (Batch A B) f b) v =
f
(Batch_make b
(coerce eq_sym (batch_length_map f b) in v))
A, B, C: Type b: Batch A B C D: Type f: C -> D v: Vector (length_Batch (map (Batch A B) f b)) B
Batch_make (map (Batch A B) f b) v =
Batch_make (map (Batch A B) f b)
(coerce batch_length_map f b
in coerce eq_sym (batch_length_map f b) in v)
A, B, C: Type b: Batch A B C D: Type f: C -> D v: Vector (length_Batch (map (Batch A B) f b)) B
v ~~
coerce batch_length_map f b
in coerce eq_sym (batch_length_map f b) in v
vector_sim.Qed.(** ** Naturality of <<Batch_contents>> *)(******************************************************************************)
forall (ABC : Type) (b : Batch A B C) (A' : Type)
(f : A -> A'),
map (Vector (length_Batch b)) f (Batch_contents b) ~~
Batch_contents (mapfst_Batch f b)
forall (ABC : Type) (b : Batch A B C) (A' : Type)
(f : A -> A'),
map (Vector (length_Batch b)) f (Batch_contents b) ~~
Batch_contents (mapfst_Batch f b)
A, B, C: Type b: Batch A B C A': Type f: A -> A'
map (Vector (length_Batch b)) f (Batch_contents b) ~~
Batch_contents (mapfst_Batch f b)
A, B, C: Type c: C A': Type f: A -> A'
map (Vector (length_Batch (Done c))) f
(Batch_contents (Done c)) ~~
Batch_contents (mapfst_Batch f (Done c))
A, B, C: Type b: Batch A B (B -> C) a: A A': Type f: A -> A' IHb: map (Vector (length_Batch b)) f (Batch_contents b) ~~
Batch_contents (mapfst_Batch f b)
map (Vector (length_Batch (b ⧆ a))) f
(Batch_contents (b ⧆ a)) ~~
Batch_contents (mapfst_Batch f (b ⧆ a))
A, B, C: Type c: C A': Type f: A -> A'
map (Vector (length_Batch (Done c))) f
(Batch_contents (Done c)) ~~
Batch_contents (mapfst_Batch f (Done c))
reflexivity.
A, B, C: Type b: Batch A B (B -> C) a: A A': Type f: A -> A' IHb: map (Vector (length_Batch b)) f (Batch_contents b) ~~
Batch_contents (mapfst_Batch f b)
map (Vector (length_Batch (b ⧆ a))) f
(Batch_contents (b ⧆ a)) ~~
Batch_contents (mapfst_Batch f (b ⧆ a))
A, B, C: Type b: Batch A B (B -> C) a: A A': Type f: A -> A' IHb: map (Vector (length_Batch b)) f (Batch_contents b) ~~
Batch_contents (mapfst_Batch f b)
map (Vector (S (length_Batch b))) f
(vcons (length_Batch b) a (Batch_contents b)) ~~
vcons (length_Batch (mapfst_Batch f b)) (f a)
(Batch_contents (mapfst_Batch f b))
A, B, C: Type b: Batch A B (B -> C) a: A A': Type f: A -> A' IHb: map (Vector (length_Batch b)) f (Batch_contents b) ~~
Batch_contents (mapfst_Batch f b)
vcons (length_Batch b) (f a)
(map (Vector (length_Batch b)) f (Batch_contents b)) ~~
vcons (length_Batch (mapfst_Batch f b)) (f a)
(Batch_contents (mapfst_Batch f b))
A, B, C: Type b: Batch A B (B -> C) a: A A': Type f: A -> A' IHb: map (Vector (length_Batch b)) f (Batch_contents b) ~~
Batch_contents (mapfst_Batch f b)
map (Vector (length_Batch b)) f (Batch_contents b) ~~
Batch_contents (mapfst_Batch f b)
assumption.Qed.(** ** Specification for <<Batch_replace_contents>> *)(*******************************************************************************)
A, A', B, C: Type
forallb : Batch A B C,
Batch_replace_contents b =
Batch_make (cojoin_Batch b)
○ coerce_Vector_length (length_cojoin_Batch b)
A, A', B, C: Type
forallb : Batch A B C,
Batch_replace_contents b =
Batch_make (cojoin_Batch b)
○ coerce_Vector_length (length_cojoin_Batch b)
A, A', B, C: Type b: Batch A B C
Batch_replace_contents b =
Batch_make (cojoin_Batch b)
○ coerce_Vector_length (length_cojoin_Batch b)
A, A', B, C: Type b: Batch A B C v: Vector (length_Batch b) A'
Batch_replace_contents b v =
Batch_make (cojoin_Batch b)
(coerce length_cojoin_Batch b in v)
A, A', B, C: Type b: Batch A B C v: Vector (length_Batch b) A'
foralle : length_Batch b = length_Batch (cojoin_Batch b),
Batch_replace_contents b v =
Batch_make (cojoin_Batch b) (coerce e in v)
A, A', B, C: Type b: Batch A B C v: Vector (length_Batch b) A' Heq: length_Batch b = length_Batch (cojoin_Batch b)
Batch_replace_contents b v =
Batch_make (cojoin_Batch b) (coerce Heq in v)
A, A', B, C: Type c: C v: Vector (length_Batch (Done c)) A' Heq: length_Batch (Done c) = length_Batch (cojoin_Batch (Done c))
Batch_replace_contents (Done c) v =
Batch_make (cojoin_Batch (Done c)) (coerce Heq in v)
A, A', B, C: Type b: Batch A B (B -> C) a: A v: Vector (length_Batch (b ⧆ a)) A' Heq: length_Batch (b ⧆ a) = length_Batch (cojoin_Batch (b ⧆ a)) IHb: forall (v : Vector (length_Batch b) A')
(Heq : length_Batch b = length_Batch (cojoin_Batch b)),
Batch_replace_contents b v = Batch_make (cojoin_Batch b) (coerce Heq in v)
Batch_replace_contents (b ⧆ a) v =
Batch_make (cojoin_Batch (b ⧆ a)) (coerce Heq in v)
A, A', B, C: Type c: C v: Vector (length_Batch (Done c)) A' Heq: length_Batch (Done c) = length_Batch (cojoin_Batch (Done c))
Batch_replace_contents (Done c) v =
Batch_make (cojoin_Batch (Done c)) (coerce Heq in v)
reflexivity.
A, A', B, C: Type b: Batch A B (B -> C) a: A v: Vector (length_Batch (b ⧆ a)) A' Heq: length_Batch (b ⧆ a) = length_Batch (cojoin_Batch (b ⧆ a)) IHb: forall (v : Vector (length_Batch b) A')
(Heq : length_Batch b = length_Batch (cojoin_Batch b)),
Batch_replace_contents b v = Batch_make (cojoin_Batch b) (coerce Heq in v)
Batch_replace_contents (b ⧆ a) v =
Batch_make (cojoin_Batch (b ⧆ a)) (coerce Heq in v)
A, A', B, C: Type b: Batch A B (B -> C) a: A v: Vector (length_Batch (b ⧆ a)) A' Heq: length_Batch (b ⧆ a) = length_Batch (cojoin_Batch (b ⧆ a)) IHb: forall (v : Vector (length_Batch b) A')
(Heq : length_Batch b = length_Batch (cojoin_Batch b)),
Batch_replace_contents b v = Batch_make (cojoin_Batch b) (coerce Heq in v)
Batch_replace_contents b (Vector_tl v) ⧆ Vector_hd v =
Batch_make (cojoin_Batch (b ⧆ a)) (coerce Heq in v)
A, A', B, C: Type b: Batch A B (B -> C) a: A v: Vector (length_Batch (b ⧆ a)) A' Heq: length_Batch (b ⧆ a) = length_Batch (cojoin_Batch (b ⧆ a)) IHb: forall (v : Vector (length_Batch b) A')
(Heq : length_Batch b = length_Batch (cojoin_Batch b)),
Batch_replace_contents b v = Batch_make (cojoin_Batch b) (coerce Heq in v)
Batch_replace_contents b (Vector_tl v) ⧆ Vector_hd v =
Batch_make (map (Batch A A') Step (cojoin_Batch b))
(Vector_tl (coerce Heq in v))
(Vector_hd (coerce Heq in v))
A, A', B, C: Type b: Batch A B (B -> C) a: A v: Vector (length_Batch (b ⧆ a)) A' Heq: length_Batch (b ⧆ a) = length_Batch (cojoin_Batch (b ⧆ a)) IHb: forall (v : Vector (length_Batch b) A')
(Heq : length_Batch b = length_Batch (cojoin_Batch b)),
Batch_replace_contents b v = Batch_make (cojoin_Batch b) (coerce Heq in v)
Batch_replace_contents b (Vector_tl v) ⧆ Vector_hd v =
Batch_make (cojoin_Batch b)
(coerce eq_sym
(batch_length_map Step (cojoin_Batch b))
in Vector_tl (coerce Heq in v))
⧆ Vector_hd (coerce Heq in v)
A, A', B, C: Type b: Batch A B (B -> C) a: A v: Vector (length_Batch (b ⧆ a)) A' Heq: length_Batch (b ⧆ a) = length_Batch (cojoin_Batch (b ⧆ a)) IHb: forall (v : Vector (length_Batch b) A')
(Heq : length_Batch b = length_Batch (cojoin_Batch b)),
Batch_replace_contents b v = Batch_make (cojoin_Batch b) (coerce Heq in v)
Batch_replace_contents b (Vector_tl v) ⧆ Vector_hd v =
Batch_make (cojoin_Batch b)
(coerce eq_sym
(batch_length_map Step (cojoin_Batch b))
in Vector_tl (coerce Heq in v)) ⧆ Vector_hd v
A, A', B, C: Type b: Batch A B (B -> C) a: A v: Vector (length_Batch (b ⧆ a)) A' Heq: length_Batch (b ⧆ a) = length_Batch (cojoin_Batch (b ⧆ a)) IHb: forall (v : Vector (length_Batch b) A')
(Heq : length_Batch b = length_Batch (cojoin_Batch b)),
Batch_replace_contents b v = Batch_make (cojoin_Batch b) (coerce Heq in v)
Batch_replace_contents b (Vector_tl v) =
Batch_make (cojoin_Batch b)
(coerce eq_sym
(batch_length_map Step (cojoin_Batch b))
in Vector_tl (coerce Heq in v))
A, A', B, C: Type b: Batch A B (B -> C) a: A v: Vector (length_Batch (b ⧆ a)) A' Heq: length_Batch (b ⧆ a) = length_Batch (cojoin_Batch (b ⧆ a)) IHb: Batch_replace_contents b (Vector_tl v) =
Batch_make (cojoin_Batch b) (coerce length_cojoin_Batch b in Vector_tl v)
Batch_replace_contents b (Vector_tl v) =
Batch_make (cojoin_Batch b)
(coerce eq_sym
(batch_length_map Step (cojoin_Batch b))
in Vector_tl (coerce Heq in v))
A, A', B, C: Type b: Batch A B (B -> C) a: A v: Vector (length_Batch (b ⧆ a)) A' Heq: length_Batch (b ⧆ a) = length_Batch (cojoin_Batch (b ⧆ a)) IHb: Batch_replace_contents b (Vector_tl v) =
Batch_make (cojoin_Batch b) (coerce length_cojoin_Batch b in Vector_tl v)
Batch_make (cojoin_Batch b)
(coerce length_cojoin_Batch b in Vector_tl v) =
Batch_make (cojoin_Batch b)
(coerce eq_sym
(batch_length_map Step (cojoin_Batch b))
in Vector_tl (coerce Heq in v))
A, A', B, C: Type b: Batch A B (B -> C) a: A v: Vector (length_Batch (b ⧆ a)) A' Heq: length_Batch (b ⧆ a) = length_Batch (cojoin_Batch (b ⧆ a)) IHb: Batch_replace_contents b (Vector_tl v) =
Batch_make (cojoin_Batch b) (coerce length_cojoin_Batch b in Vector_tl v)
coerce length_cojoin_Batch b in Vector_tl v ~~
coerce eq_sym (batch_length_map Step (cojoin_Batch b))
in Vector_tl (coerce Heq in v)
vector_sim.Qed.(** ** Replacing Contents Does Not Change <<length_Batch>>, <<shape>>, or <<Batch_make>> *)(*******************************************************************************)
forall (ABC : Type) (b : Batch A B C) (A' : Type)
(v : Vector (length_Batch b) A'),
length_Batch b =
length_Batch (Batch_replace_contents b v)
forall (ABC : Type) (b : Batch A B C) (A' : Type)
(v : Vector (length_Batch b) A'),
length_Batch b =
length_Batch (Batch_replace_contents b v)
A, B, C: Type b: Batch A B C A': Type v: Vector (length_Batch b) A'
length_Batch b =
length_Batch (Batch_replace_contents b v)
A, B, C: Type c: C A': Type v: Vector (length_Batch (Done c)) A'
length_Batch (Done c) =
length_Batch (Batch_replace_contents (Done c) v)
A, B, C: Type b: Batch A B (B -> C) a: A A': Type v: Vector (length_Batch (b ⧆ a)) A' IHb: forallv : Vector (length_Batch b) A',
length_Batch b = length_Batch (Batch_replace_contents b v)
length_Batch (b ⧆ a) =
length_Batch (Batch_replace_contents (b ⧆ a) v)
A, B, C: Type c: C A': Type v: Vector (length_Batch (Done c)) A'
length_Batch (Done c) =
length_Batch (Batch_replace_contents (Done c) v)
reflexivity.
A, B, C: Type b: Batch A B (B -> C) a: A A': Type v: Vector (length_Batch (b ⧆ a)) A' IHb: forallv : Vector (length_Batch b) A',
length_Batch b = length_Batch (Batch_replace_contents b v)
length_Batch (b ⧆ a) =
length_Batch (Batch_replace_contents (b ⧆ a) v)
A, B, C: Type b: Batch A B (B -> C) a: A A': Type v: Vector (length_Batch (b ⧆ a)) A' IHb: forallv : Vector (length_Batch b) A',
length_Batch b = length_Batch (Batch_replace_contents b v)
S (length_Batch b) =
S
(length_Batch
(Batch_replace_contents b (Vector_tl v)))
A, B, C: Type b: Batch A B (B -> C) a: A A': Type v: Vector (length_Batch (b ⧆ a)) A' IHb: forallv : Vector (length_Batch b) A',
length_Batch b = length_Batch (Batch_replace_contents b v)
length_Batch b =
length_Batch (Batch_replace_contents b (Vector_tl v))
apply (IHb (Vector_tl v)).Qed.
A, A', B, C: Type
forall (b : Batch A B C)
(v : Vector (length_Batch b) A'),
Batch_make (Batch_replace_contents b v) =
Batch_make b
○ coerce_Vector_length
(eq_sym (length_replace_contents b v))
A, A', B, C: Type
forall (b : Batch A B C)
(v : Vector (length_Batch b) A'),
Batch_make (Batch_replace_contents b v) =
Batch_make b
○ coerce_Vector_length
(eq_sym (length_replace_contents b v))
A, A', B, C: Type b: Batch A B C v: Vector (length_Batch b) A'
Batch_make (Batch_replace_contents b v) =
Batch_make b
○ coerce_Vector_length
(eq_sym (length_replace_contents b v))
A, A', B, C: Type b: Batch A B C v: Vector (length_Batch b) A' v': Vector
(length_Batch (Batch_replace_contents b v)) B
Batch_make (Batch_replace_contents b v) v' =
Batch_make b
(coerce eq_sym (length_replace_contents b v) in v')
A, A', B, C: Type b: Batch A B C v: Vector (length_Batch b) A' v': Vector
(length_Batch (Batch_replace_contents b v)) B
foralle : length_Batch (Batch_replace_contents b v) =
length_Batch b,
Batch_make (Batch_replace_contents b v) v' =
Batch_make b (coerce e in v')
A, A', B, C: Type b: Batch A B C v: Vector (length_Batch b) A' v': Vector
(length_Batch (Batch_replace_contents b v)) B e: length_Batch (Batch_replace_contents b v) =
length_Batch b
Batch_make (Batch_replace_contents b v) v' =
Batch_make b (coerce e in v')
A, A', B, C: Type c: C v: Vector (length_Batch (Done c)) A' v': Vector
(length_Batch
(Batch_replace_contents (Done c) v)) B e: length_Batch (Batch_replace_contents (Done c) v) =
length_Batch (Done c)
Batch_make (Batch_replace_contents (Done c) v) v' =
Batch_make (Done c) (coerce e in v')
A, A', B, C: Type b: Batch A B (B -> C) a: A v: Vector (length_Batch (b ⧆ a)) A' v': Vector
(length_Batch
(Batch_replace_contents (b ⧆ a) v)) B e: length_Batch (Batch_replace_contents (b ⧆ a) v) =
length_Batch (b ⧆ a) IHb: forall (v : Vector (length_Batch b) A')
(v' : Vector (length_Batch (Batch_replace_contents b v)) B)
(e : length_Batch (Batch_replace_contents b v) = length_Batch b),
Batch_make (Batch_replace_contents b v) v' = Batch_make b (coerce e in v')
Batch_make (Batch_replace_contents (b ⧆ a) v) v' =
Batch_make (b ⧆ a) (coerce e in v')
A, A', B, C: Type c: C v: Vector (length_Batch (Done c)) A' v': Vector
(length_Batch
(Batch_replace_contents (Done c) v)) B e: length_Batch (Batch_replace_contents (Done c) v) =
length_Batch (Done c)
Batch_make (Batch_replace_contents (Done c) v) v' =
Batch_make (Done c) (coerce e in v')
reflexivity.
A, A', B, C: Type b: Batch A B (B -> C) a: A v: Vector (length_Batch (b ⧆ a)) A' v': Vector
(length_Batch
(Batch_replace_contents (b ⧆ a) v)) B e: length_Batch (Batch_replace_contents (b ⧆ a) v) =
length_Batch (b ⧆ a) IHb: forall (v : Vector (length_Batch b) A')
(v' : Vector (length_Batch (Batch_replace_contents b v)) B)
(e : length_Batch (Batch_replace_contents b v) = length_Batch b),
Batch_make (Batch_replace_contents b v) v' = Batch_make b (coerce e in v')
Batch_make (Batch_replace_contents (b ⧆ a) v) v' =
Batch_make (b ⧆ a) (coerce e in v')
A, A', B, C: Type b: Batch A B (B -> C) a: A v: Vector (length_Batch (b ⧆ a)) A' v': Vector
(length_Batch
(Batch_replace_contents (b ⧆ a) v)) B e: length_Batch (Batch_replace_contents (b ⧆ a) v) =
length_Batch (b ⧆ a) IHb: forall (v : Vector (length_Batch b) A')
(v' : Vector (length_Batch (Batch_replace_contents b v)) B)
(e : length_Batch (Batch_replace_contents b v) = length_Batch b),
Batch_make (Batch_replace_contents b v) v' = Batch_make b (coerce e in v')
Batch_make (Batch_replace_contents b (Vector_tl v))
(Vector_tl v') (Vector_hd v') =
Batch_make b (Vector_tl (coerce e in v'))
(Vector_hd (coerce e in v'))
A, A', B, C: Type b: Batch A B (B -> C) a: A v: Vector (length_Batch (b ⧆ a)) A' v': Vector
(length_Batch
(Batch_replace_contents (b ⧆ a) v)) B e: length_Batch (Batch_replace_contents (b ⧆ a) v) =
length_Batch (b ⧆ a) IHb: foralle : length_Batch (Batch_replace_contents b (Vector_tl v)) = length_Batch b,
Batch_make (Batch_replace_contents b (Vector_tl v)) (Vector_tl v') =
Batch_make b (coerce e in Vector_tl v')
Batch_make (Batch_replace_contents b (Vector_tl v))
(Vector_tl v') (Vector_hd v') =
Batch_make b (Vector_tl (coerce e in v'))
(Vector_hd (coerce e in v'))
A, A', B, C: Type b: Batch A B (B -> C) a: A v: Vector (length_Batch (b ⧆ a)) A' v': Vector
(length_Batch
(Batch_replace_contents (b ⧆ a) v)) B e: length_Batch (Batch_replace_contents (b ⧆ a) v) =
length_Batch (b ⧆ a) IHb: Batch_make (Batch_replace_contents b (Vector_tl v)) (Vector_tl v') =
Batch_make b
(coerce eq_sym (length_replace_contents b (Vector_tl v)) in Vector_tl v')
Batch_make (Batch_replace_contents b (Vector_tl v))
(Vector_tl v') (Vector_hd v') =
Batch_make b (Vector_tl (coerce e in v'))
(Vector_hd (coerce e in v'))
A, A', B, C: Type b: Batch A B (B -> C) a: A v: Vector (length_Batch (b ⧆ a)) A' v': Vector
(length_Batch
(Batch_replace_contents (b ⧆ a) v)) B e: length_Batch (Batch_replace_contents (b ⧆ a) v) =
length_Batch (b ⧆ a) IHb: Batch_make (Batch_replace_contents b (Vector_tl v)) (Vector_tl v') =
Batch_make b
(coerce eq_sym (length_replace_contents b (Vector_tl v)) in Vector_tl v')
Batch_make (Batch_replace_contents b (Vector_tl v))
(Vector_tl v') (Vector_hd v') =
Batch_make b (Vector_tl (coerce e in v'))
(Vector_hd v')
A, A', B, C: Type b: Batch A B (B -> C) a: A v: Vector (length_Batch (b ⧆ a)) A' v': Vector
(length_Batch
(Batch_replace_contents (b ⧆ a) v)) B e: length_Batch (Batch_replace_contents (b ⧆ a) v) =
length_Batch (b ⧆ a) IHb: Batch_make (Batch_replace_contents b (Vector_tl v)) (Vector_tl v') =
Batch_make b
(coerce eq_sym (length_replace_contents b (Vector_tl v)) in Vector_tl v')
Vector_hd v' = Vector_hd (coerce e in v')
A, A', B, C: Type b: Batch A B (B -> C) a: A v: Vector (length_Batch (b ⧆ a)) A' v': Vector
(length_Batch
(Batch_replace_contents (b ⧆ a) v)) B e: length_Batch (Batch_replace_contents (b ⧆ a) v) =
length_Batch (b ⧆ a) IHb: Batch_make (Batch_replace_contents b (Vector_tl v)) (Vector_tl v') =
Batch_make b
(coerce eq_sym (length_replace_contents b (Vector_tl v)) in Vector_tl v')
Batch_make (Batch_replace_contents b (Vector_tl v))
(Vector_tl v') (Vector_hd v') =
Batch_make b (Vector_tl (coerce e in v'))
(Vector_hd v')
A, A', B, C: Type b: Batch A B (B -> C) a: A v: Vector (length_Batch (b ⧆ a)) A' v': Vector
(length_Batch
(Batch_replace_contents (b ⧆ a) v)) B e: length_Batch (Batch_replace_contents (b ⧆ a) v) =
length_Batch (b ⧆ a) IHb: Batch_make (Batch_replace_contents b (Vector_tl v)) (Vector_tl v') =
Batch_make b
(coerce eq_sym (length_replace_contents b (Vector_tl v)) in Vector_tl v')
Vector_hd v' = Vector_hd (coerce e in v')
A, A', B, C: Type b: Batch A B (B -> C) a: A v: Vector (length_Batch (b ⧆ a)) A' v': Vector
(length_Batch
(Batch_replace_contents (b ⧆ a) v)) B e: length_Batch (Batch_replace_contents (b ⧆ a) v) =
length_Batch (b ⧆ a) IHb: Batch_make (Batch_replace_contents b (Vector_tl v)) (Vector_tl v') =
Batch_make b
(coerce eq_sym (length_replace_contents b (Vector_tl v)) in Vector_tl v')
Batch_make b
(coerce eq_sym
(length_replace_contents b (Vector_tl v))
in Vector_tl v') (Vector_hd v') =
Batch_make b (Vector_tl (coerce e in v'))
(Vector_hd v')
A, A', B, C: Type b: Batch A B (B -> C) a: A v: Vector (length_Batch (b ⧆ a)) A' v': Vector
(length_Batch
(Batch_replace_contents (b ⧆ a) v)) B e: length_Batch (Batch_replace_contents (b ⧆ a) v) =
length_Batch (b ⧆ a) IHb: Batch_make (Batch_replace_contents b (Vector_tl v)) (Vector_tl v') =
Batch_make b
(coerce eq_sym (length_replace_contents b (Vector_tl v)) in Vector_tl v')
Vector_hd v' = Vector_hd (coerce e in v')
A, A', B, C: Type b: Batch A B (B -> C) a: A v: Vector (length_Batch (b ⧆ a)) A' v': Vector
(length_Batch
(Batch_replace_contents (b ⧆ a) v)) B e: length_Batch (Batch_replace_contents (b ⧆ a) v) =
length_Batch (b ⧆ a) IHb: Batch_make (Batch_replace_contents b (Vector_tl v)) (Vector_tl v') =
Batch_make b
(coerce eq_sym (length_replace_contents b (Vector_tl v)) in Vector_tl v')
Batch_make b
(coerce eq_sym
(length_replace_contents b (Vector_tl v))
in Vector_tl v') (Vector_hd v') =
Batch_make b (Vector_tl (coerce e in v'))
(Vector_hd v')
A, A', B, C: Type b: Batch A B (B -> C) a: A v: Vector (length_Batch (b ⧆ a)) A' v': Vector
(length_Batch
(Batch_replace_contents (b ⧆ a) v)) B e: length_Batch (Batch_replace_contents (b ⧆ a) v) =
length_Batch (b ⧆ a) IHb: Batch_make (Batch_replace_contents b (Vector_tl v)) (Vector_tl v') =
Batch_make b
(coerce eq_sym (length_replace_contents b (Vector_tl v)) in Vector_tl v')
Vector_hd v' = Vector_hd (coerce e in v')
A, A', B, C: Type b: Batch A B (B -> C) a: A v: Vector (length_Batch (b ⧆ a)) A' v': Vector
(length_Batch
(Batch_replace_contents (b ⧆ a) v)) B e: length_Batch (Batch_replace_contents (b ⧆ a) v) =
length_Batch (b ⧆ a) IHb: Batch_make (Batch_replace_contents b (Vector_tl v)) (Vector_tl v') =
Batch_make b
(coerce eq_sym (length_replace_contents b (Vector_tl v)) in Vector_tl v')
coerce eq_sym
(length_replace_contents b (Vector_tl v))
in Vector_tl v' = Vector_tl (coerce e in v')
A, A', B, C: Type b: Batch A B (B -> C) a: A v: Vector (length_Batch (b ⧆ a)) A' v': Vector
(length_Batch
(Batch_replace_contents (b ⧆ a) v)) B e: length_Batch (Batch_replace_contents (b ⧆ a) v) =
length_Batch (b ⧆ a) IHb: Batch_make (Batch_replace_contents b (Vector_tl v)) (Vector_tl v') =
Batch_make b
(coerce eq_sym (length_replace_contents b (Vector_tl v)) in Vector_tl v')
Vector_hd v' = Vector_hd (coerce e in v')
A, A', B, C: Type b: Batch A B (B -> C) a: A v: Vector (length_Batch (b ⧆ a)) A' v': Vector
(length_Batch
(Batch_replace_contents (b ⧆ a) v)) B e: length_Batch (Batch_replace_contents (b ⧆ a) v) =
length_Batch (b ⧆ a) IHb: Batch_make (Batch_replace_contents b (Vector_tl v)) (Vector_tl v') =
Batch_make b
(coerce eq_sym (length_replace_contents b (Vector_tl v)) in Vector_tl v')
coerce eq_sym
(length_replace_contents b (Vector_tl v))
in Vector_tl v' = Vector_tl (coerce e in v')
A, A', B, C: Type b: Batch A B (B -> C) a: A v: Vector (length_Batch (b ⧆ a)) A' v': Vector
(length_Batch
(Batch_replace_contents (b ⧆ a) v)) B e: length_Batch (Batch_replace_contents (b ⧆ a) v) =
length_Batch (b ⧆ a) IHb: Batch_make (Batch_replace_contents b (Vector_tl v)) (Vector_tl v') =
Batch_make b
(coerce eq_sym (length_replace_contents b (Vector_tl v)) in Vector_tl v')
proj1_sig
(coerce eq_sym
(length_replace_contents b (Vector_tl v))
in Vector_tl v') =
proj1_sig (Vector_tl (coerce e in v'))
A, A', B, C: Type b: Batch A B (B -> C) a: A v: Vector (length_Batch (b ⧆ a)) A' v': Vector
(length_Batch
(Batch_replace_contents (b ⧆ a) v)) B e: length_Batch (Batch_replace_contents (b ⧆ a) v) =
length_Batch (b ⧆ a) IHb: Batch_make (Batch_replace_contents b (Vector_tl v)) (Vector_tl v') =
Batch_make b
(coerce eq_sym (length_replace_contents b (Vector_tl v)) in Vector_tl v')
proj1_sig (Vector_tl v') =
proj1_sig (Vector_tl (coerce e in v'))
apply Vector_tl_coerce_sim.
A, A', B, C: Type b: Batch A B (B -> C) a: A v: Vector (length_Batch (b ⧆ a)) A' v': Vector
(length_Batch
(Batch_replace_contents (b ⧆ a) v)) B e: length_Batch (Batch_replace_contents (b ⧆ a) v) =
length_Batch (b ⧆ a) IHb: Batch_make (Batch_replace_contents b (Vector_tl v)) (Vector_tl v') =
Batch_make b
(coerce eq_sym (length_replace_contents b (Vector_tl v)) in Vector_tl v')
Vector_hd v' = Vector_hd (coerce e in v')
apply Vector_hd_coerce_eq.Qed.
forall (AA'BC : Type) (b : Batch A B C)
(v : Vector (length_Batch b) A'),
shape b = shape (Batch_replace_contents b v)
forall (AA'BC : Type) (b : Batch A B C)
(v : Vector (length_Batch b) A'),
shape b = shape (Batch_replace_contents b v)
A, A', B, C: Type b: Batch A B C v: Vector (length_Batch b) A'
shape b = shape (Batch_replace_contents b v)
A, A', B, C: Type c: C v: Vector (length_Batch (Done c)) A'
shape (Done c) =
shape (Batch_replace_contents (Done c) v)
A, A', B, C: Type b: Batch A B (B -> C) a: A v: Vector (length_Batch (b ⧆ a)) A' IHb: forallv : Vector (length_Batch b) A',
shape b = shape (Batch_replace_contents b v)
shape (b ⧆ a) =
shape (Batch_replace_contents (b ⧆ a) v)
A, A', B, C: Type c: C v: Vector (length_Batch (Done c)) A'
shape (Done c) =
shape (Batch_replace_contents (Done c) v)
reflexivity.
A, A', B, C: Type b: Batch A B (B -> C) a: A v: Vector (length_Batch (b ⧆ a)) A' IHb: forallv : Vector (length_Batch b) A',
shape b = shape (Batch_replace_contents b v)
shape (b ⧆ a) =
shape (Batch_replace_contents (b ⧆ a) v)
A, A', B, C: Type b: Batch A B (B -> C) a: A v: Vector (length_Batch (b ⧆ a)) A' IHb: forallv : Vector (length_Batch b) A',
shape b = shape (Batch_replace_contents b v)
mapfst_Batch (const tt) b ⧆ const tt a =
mapfst_Batch (const tt)
(Batch_replace_contents b (Vector_tl v))
⧆ const tt (Vector_hd v)
A, A', B, C: Type b: Batch A B (B -> C) a: A v: Vector (length_Batch (b ⧆ a)) A' IHb: forallv : Vector (length_Batch b) A',
shape b = shape (Batch_replace_contents b v)
mapfst_Batch (const tt) b =
mapfst_Batch (const tt)
(Batch_replace_contents b (Vector_tl v))
forallb : Batch A A C,
Batch_make b (Batch_contents b) = extract_Batch b
A, A', A'', B, C: Type
forallb : Batch A A C,
Batch_make b (Batch_contents b) = extract_Batch b
A, A', A'', B, C: Type b: Batch A A C
Batch_make b (Batch_contents b) = extract_Batch b
A, A', A'', B, C: Type c: C
Batch_make (Done c) (Batch_contents (Done c)) =
extract_Batch (Done c)
A, A', A'', B, C: Type b: Batch A A (A -> C) a: A IHb: Batch_make b (Batch_contents b) = extract_Batch b
Batch_make (b ⧆ a) (Batch_contents (b ⧆ a)) =
extract_Batch (b ⧆ a)
A, A', A'', B, C: Type c: C
Batch_make (Done c) (Batch_contents (Done c)) =
extract_Batch (Done c)
reflexivity.
A, A', A'', B, C: Type b: Batch A A (A -> C) a: A IHb: Batch_make b (Batch_contents b) = extract_Batch b
Batch_make (b ⧆ a) (Batch_contents (b ⧆ a)) =
extract_Batch (b ⧆ a)
A, A', A'', B, C: Type b: Batch A A (A -> C) a: A IHb: Batch_make b (Batch_contents b) = extract_Batch b
Batch_make b (Vector_tl (Batch_contents (b ⧆ a)))
(Vector_hd (Batch_contents (b ⧆ a))) =
extract_Batch (b ⧆ a)
A, A', A'', B, C: Type b: Batch A A (A -> C) a: A IHb: Batch_make b (Batch_contents b) = extract_Batch b
Batch_make b
(Vector_tl
(vcons (length_Batch b) a (Batch_contents b)))
(Vector_hd
(vcons (length_Batch b) a (Batch_contents b))) =
extract_Batch (b ⧆ a)
A, A', A'', B, C: Type b: Batch A A (A -> C) a: A IHb: Batch_make b (Batch_contents b) = extract_Batch b
Batch_make b (Batch_contents b)
(Vector_hd
(vcons (length_Batch b) a (Batch_contents b))) =
extract_Batch (b ⧆ a)
A, A', A'', B, C: Type b: Batch A A (A -> C) a: A IHb: Batch_make b (Batch_contents b) = extract_Batch b
Batch_make b (Batch_contents b) a =
extract_Batch (b ⧆ a)
A, A', A'', B, C: Type b: Batch A A (A -> C) a: A IHb: Batch_make b (Batch_contents b) = extract_Batch b
extract_Batch b a = extract_Batch (b ⧆ a)
reflexivity.Qed.
A, A', A'', B, C: Type
forallb : Batch A B C,
Batch_replace_contents b (Batch_contents b) = b
A, A', A'', B, C: Type
forallb : Batch A B C,
Batch_replace_contents b (Batch_contents b) = b
A, A', A'', B, C: Type b: Batch A B C
Batch_replace_contents b (Batch_contents b) = b
A, A', A'', B, C: Type c: C
Batch_replace_contents (Done c)
(Batch_contents (Done c)) = Done c
A, A', A'', B, C: Type b: Batch A B (B -> C) a: A IHb: Batch_replace_contents b (Batch_contents b) = b
Batch_replace_contents (b ⧆ a)
(Batch_contents (b ⧆ a)) = b ⧆ a
A, A', A'', B, C: Type c: C
Batch_replace_contents (Done c)
(Batch_contents (Done c)) = Done c
reflexivity.
A, A', A'', B, C: Type b: Batch A B (B -> C) a: A IHb: Batch_replace_contents b (Batch_contents b) = b
Batch_replace_contents (b ⧆ a)
(Batch_contents (b ⧆ a)) = b ⧆ a
A, A', A'', B, C: Type b: Batch A B (B -> C) a: A IHb: Batch_replace_contents b (Batch_contents b) = b
Batch_replace_contents b
(Vector_tl
(vcons (length_Batch b) a (Batch_contents b)))
⧆ Vector_hd
(vcons (length_Batch b) a (Batch_contents b)) =
b ⧆ a
A, A', A'', B, C: Type b: Batch A B (B -> C) a: A IHb: Batch_replace_contents b (Batch_contents b) = b
Batch_replace_contents b (Batch_contents b)
⧆ Vector_hd
(vcons (length_Batch b) a (Batch_contents b)) =
b ⧆ a
A, A', A'', B, C: Type b: Batch A B (B -> C) a: A IHb: Batch_replace_contents b (Batch_contents b) = b
Batch_replace_contents b (Batch_contents b) ⧆ a =
b ⧆ a
A, A', A'', B, C: Type b: Batch A B (B -> C) a: A IHb: Batch_replace_contents b (Batch_contents b) = b
b ⧆ a = b ⧆ a
reflexivity.Qed.
A, A', A'', B, C: Type
forall (b : Batch A B C)
(v : Vector (length_Batch b) A'),
Batch_contents (Batch_replace_contents b v) =
coerce length_replace_contents b v in v
A, A', A'', B, C: Type
forall (b : Batch A B C)
(v : Vector (length_Batch b) A'),
Batch_contents (Batch_replace_contents b v) =
coerce length_replace_contents b v in v
A, A', A'', B, C: Type b: Batch A B C v: Vector (length_Batch b) A'
Batch_contents (Batch_replace_contents b v) =
coerce length_replace_contents b v in v
A, A', A'', B, C: Type b: Batch A B C v: Vector (length_Batch b) A'
foralle : length_Batch b =
length_Batch (Batch_replace_contents b v),
Batch_contents (Batch_replace_contents b v) =
coerce e in v
A, A', A'', B, C: Type b: Batch A B C v: Vector (length_Batch b) A' Heq: length_Batch b = length_Batch (Batch_replace_contents b v)
Batch_contents (Batch_replace_contents b v) =
coerce Heq in v
A, A', A'', B, C: Type c: C v: Vector (length_Batch (Done c)) A' Heq: length_Batch (Done c) = length_Batch (Batch_replace_contents (Done c) v)
Batch_contents (Batch_replace_contents (Done c) v) =
coerce Heq in v
A, A', A'', B, C: Type b: Batch A B (B -> C) a: A v: Vector (length_Batch (b ⧆ a)) A' Heq: length_Batch (b ⧆ a) = length_Batch (Batch_replace_contents (b ⧆ a) v) IHb: forall (v : Vector (length_Batch b) A')
(Heq : length_Batch b = length_Batch (Batch_replace_contents b v)),
Batch_contents (Batch_replace_contents b v) = coerce Heq in v
Batch_contents (Batch_replace_contents (b ⧆ a) v) =
coerce Heq in v
A, A', A'', B, C: Type c: C v: Vector (length_Batch (Done c)) A' Heq: length_Batch (Done c) = length_Batch (Batch_replace_contents (Done c) v)
Batch_contents (Batch_replace_contents (Done c) v) =
coerce Heq in v
A, A', A'', B, C: Type c: C v: Vector (length_Batch (Done c)) A' Heq: length_Batch (Done c) = length_Batch (Batch_replace_contents (Done c) v)
vnil = coerce Heq in v
A, A', A'', B, C: Type c: C v: Vector (length_Batch (Done c)) A' Heq: length_Batch (Done c) = length_Batch (Batch_replace_contents (Done c) v)
coerce Heq in v = vnil
apply Vector_nil_eq.
A, A', A'', B, C: Type b: Batch A B (B -> C) a: A v: Vector (length_Batch (b ⧆ a)) A' Heq: length_Batch (b ⧆ a) = length_Batch (Batch_replace_contents (b ⧆ a) v) IHb: forall (v : Vector (length_Batch b) A')
(Heq : length_Batch b = length_Batch (Batch_replace_contents b v)),
Batch_contents (Batch_replace_contents b v) = coerce Heq in v
Batch_contents (Batch_replace_contents (b ⧆ a) v) =
coerce Heq in v
A, A', A'', B, C: Type b: Batch A B (B -> C) a: A v: Vector (S (length_Batch b)) A' Heq: S (length_Batch b) =
S (length_Batch (Batch_replace_contents b (Vector_tl v))) IHb: forall (v : Vector (length_Batch b) A')
(Heq : length_Batch b = length_Batch (Batch_replace_contents b v)),
Batch_contents (Batch_replace_contents b v) = coerce Heq in v
vcons
(length_Batch
(Batch_replace_contents b (Vector_tl v)))
(Vector_hd v)
(Batch_contents
(Batch_replace_contents b (Vector_tl v))) =
coerce Heq in v
A, A', A'', B, C: Type b: Batch A B (B -> C) a: A v: Vector (S (length_Batch b)) A' Heq: S (length_Batch b) =
S (length_Batch (Batch_replace_contents b (Vector_tl v))) IHb: forall (v : Vector (length_Batch b) A')
(Heq : length_Batch b = length_Batch (Batch_replace_contents b v)),
Batch_contents (Batch_replace_contents b v) = coerce Heq in v
vcons
(length_Batch
(Batch_replace_contents b (Vector_tl v)))
(Vector_hd v)
(Batch_contents
(Batch_replace_contents b (Vector_tl v))) =
vcons
(length_Batch
(Batch_replace_contents b (Vector_tl v)))
(Vector_hd (coerce Heq in v))
(Vector_tl (coerce Heq in v))
A, A', A'', B, C: Type b: Batch A B (B -> C) a: A v: Vector (S (length_Batch b)) A' Heq: S (length_Batch b) =
S (length_Batch (Batch_replace_contents b (Vector_tl v))) IHb: forall (v : Vector (length_Batch b) A')
(Heq : length_Batch b = length_Batch (Batch_replace_contents b v)),
Batch_contents (Batch_replace_contents b v) = coerce Heq in v
vcons
(length_Batch
(Batch_replace_contents b (Vector_tl v)))
(Vector_hd v)
(Batch_contents
(Batch_replace_contents b (Vector_tl v))) =
vcons
(length_Batch
(Batch_replace_contents b (Vector_tl v)))
(Vector_hd v) (Vector_tl (coerce Heq in v))
A, A', A'', B, C: Type b: Batch A B (B -> C) a: A v: Vector (S (length_Batch b)) A' Heq: S (length_Batch b) =
S (length_Batch (Batch_replace_contents b (Vector_tl v))) IHb: Batch_contents (Batch_replace_contents b (Vector_tl v)) =
coerce S_uncons Heq in Vector_tl v
vcons
(length_Batch
(Batch_replace_contents b (Vector_tl v)))
(Vector_hd v)
(Batch_contents
(Batch_replace_contents b (Vector_tl v))) =
vcons
(length_Batch
(Batch_replace_contents b (Vector_tl v)))
(Vector_hd v) (Vector_tl (coerce Heq in v))
A, A', A'', B, C: Type b: Batch A B (B -> C) a: A v: Vector (S (length_Batch b)) A' Heq: S (length_Batch b) =
S (length_Batch (Batch_replace_contents b (Vector_tl v))) IHb: Batch_contents (Batch_replace_contents b (Vector_tl v)) =
coerce S_uncons Heq in Vector_tl v
vcons
(length_Batch
(Batch_replace_contents b (Vector_tl v)))
(Vector_hd v)
(Batch_contents
(Batch_replace_contents b (Vector_tl v))) =
vcons
(length_Batch
(Batch_replace_contents b (Vector_tl v)))
(Vector_hd v) (Vector_tl (coerce Heq in v))
(* ^^ I have no idea why this got expanded but it blocks rewriting *)
A, A', A'', B, C: Type b: Batch A B (B -> C) a: A v: Vector (S (length_Batch b)) A' Heq: S (length_Batch b) =
S (length_Batch (Batch_replace_contents b (Vector_tl v))) IHb: Batch_contents (Batch_replace_contents b (Vector_tl v)) =
coerce S_uncons Heq in Vector_tl v
vcons
(length_Batch
(Batch_replace_contents b (Vector_tl v)))
(Vector_hd v) (coerce S_uncons Heq in Vector_tl v) =
vcons
(length_Batch
(Batch_replace_contents b (Vector_tl v)))
(Vector_hd v) (Vector_tl (coerce Heq in v))
A, A', A'', B, C: Type b: Batch A B (B -> C) a: A v: Vector (S (length_Batch b)) A' Heq: S (length_Batch b) =
S (length_Batch (Batch_replace_contents b (Vector_tl v))) IHb: Batch_contents (Batch_replace_contents b (Vector_tl v)) =
coerce S_uncons Heq in Vector_tl v
coerce S_uncons Heq in Vector_tl v =
Vector_tl (coerce Heq in v)
A, A', A'', B, C: Type b: Batch A B (B -> C) a: A v: Vector (S (length_Batch b)) A' Heq: S (length_Batch b) =
S (length_Batch (Batch_replace_contents b (Vector_tl v))) IHb: Batch_contents (Batch_replace_contents b (Vector_tl v)) =
coerce S_uncons Heq in Vector_tl v
coerce S_uncons Heq in Vector_tl v ~~
Vector_tl (coerce Heq in v)
vector_sim.Qed.
A, A', A'', B, C: Type
forall (b : Batch A B C)
(v1 : Vector (length_Batch b) A')
(v2 : Vector (length_Batch b) A''),
Batch_replace_contents (Batch_replace_contents b v1)
(coerce length_replace_contents b v1 in v2) =
Batch_replace_contents b v2
A, A', A'', B, C: Type
forall (b : Batch A B C)
(v1 : Vector (length_Batch b) A')
(v2 : Vector (length_Batch b) A''),
Batch_replace_contents (Batch_replace_contents b v1)
(coerce length_replace_contents b v1 in v2) =
Batch_replace_contents b v2
A, A', A'', B, C: Type b: Batch A B C v1: Vector (length_Batch b) A' v2: Vector (length_Batch b) A''
Batch_replace_contents (Batch_replace_contents b v1)
(coerce length_replace_contents b v1 in v2) =
Batch_replace_contents b v2
A, A', A'', B, C: Type b: Batch A B C v1: Vector (length_Batch b) A' v2: Vector (length_Batch b) A''
shape (Batch_replace_contents b v1) = shape b
A, A', A'', B, C: Type b: Batch A B C v1: Vector (length_Batch b) A' v2: Vector (length_Batch b) A''
coerce length_replace_contents b v1 in v2 ~~ v2
A, A', A'', B, C: Type b: Batch A B C v1: Vector (length_Batch b) A' v2: Vector (length_Batch b) A''
shape b = shape (Batch_replace_contents b v1)
A, A', A'', B, C: Type b: Batch A B C v1: Vector (length_Batch b) A' v2: Vector (length_Batch b) A''
coerce length_replace_contents b v1 in v2 ~~ v2
A, A', A'', B, C: Type b: Batch A B C v1: Vector (length_Batch b) A' v2: Vector (length_Batch b) A''
coerce length_replace_contents b v1 in v2 ~~ v2
vector_sim.Qed.Endlens_laws.(** ** Batch is Shapely *)(******************************************************************************)SectionBatch_shapely.Context {ABC: Type}.
A, B, C: Type b1, b2: Batch A B C Hshape: shape b1 = shape b2 X: Type b1', b2': Batch A B (B -> X) Heq: tolist b1' = tolist b2' -> b1' = b2' a1, a2: A Hshape': shape (b1' ⧆ a1) = shape (b2' ⧆ a2) Hlist: tolist (b1' ⧆ a1) = tolist (b2' ⧆ a2)
b1' ⧆ a1 = b2' ⧆ a2
A, B, C: Type b1, b2: Batch A B C Hshape: shape b1 = shape b2 X: Type b1', b2': Batch A B (B -> X) Heq: tolist b1' = tolist b2' -> b1' = b2' a1, a2: A Hshape': shape (b1' ⧆ a1) = shape (b2' ⧆ a2) Hlist: tolist b1' ++ a1 :: nil = tolist (b2' ⧆ a2)
b1' ⧆ a1 = b2' ⧆ a2
A, B, C: Type b1, b2: Batch A B C Hshape: shape b1 = shape b2 X: Type b1', b2': Batch A B (B -> X) Heq: tolist b1' = tolist b2' -> b1' = b2' a1, a2: A Hshape': shape (b1' ⧆ a1) = shape (b2' ⧆ a2) Hlist: tolist b1' ++ a1 :: nil =
tolist b2' ++ a2 :: nil
b1' ⧆ a1 = b2' ⧆ a2
A, B, C: Type b1, b2: Batch A B C Hshape: shape b1 = shape b2 X: Type b1', b2': Batch A B (B -> X) Heq: tolist b1' = tolist b2' -> b1' = b2' a1, a2: A Hshape': shape (b1' ⧆ a1) = shape (b2' ⧆ a2) Hlist: tolist b1' ++ ret list A a1 =
tolist b2' ++ ret list A a2
b1' ⧆ a1 = b2' ⧆ a2
A, B, C: Type b1, b2: Batch A B C Hshape: shape b1 = shape b2 X: Type b1', b2': Batch A B (B -> X) Heq: tolist b1' = tolist b2' -> b1' = b2' a1, a2: A Hshape': shape (b1' ⧆ a1) = shape (b2' ⧆ a2) Hlist: tolist b1' ++ ret list A a1 =
tolist b2' ++ ret list A a2
a1 = a2
A, B, C: Type b1, b2: Batch A B C Hshape: shape b1 = shape b2 X: Type b1', b2': Batch A B (B -> X) Heq: tolist b1' = tolist b2' -> b1' = b2' a1, a2: A Hshape': shape (b1' ⧆ a1) = shape (b2' ⧆ a2) Hlist: tolist b1' ++ ret list A a1 =
tolist b2' ++ ret list A a2 H: a1 = a2
b1' ⧆ a1 = b2' ⧆ a2
A, B, C: Type b1, b2: Batch A B C Hshape: shape b1 = shape b2 X: Type b1', b2': Batch A B (B -> X) Heq: tolist b1' = tolist b2' -> b1' = b2' a1, a2: A Hshape': shape (b1' ⧆ a1) = shape (b2' ⧆ a2) Hlist: tolist b1' ++ ret list A a1 =
tolist b2' ++ ret list A a2
a1 = a2
eapply list_app_inv_r2; eauto.
A, B, C: Type b1, b2: Batch A B C Hshape: shape b1 = shape b2 X: Type b1', b2': Batch A B (B -> X) Heq: tolist b1' = tolist b2' -> b1' = b2' a1, a2: A Hshape': shape (b1' ⧆ a1) = shape (b2' ⧆ a2) Hlist: tolist b1' ++ ret list A a1 =
tolist b2' ++ ret list A a2 H: a1 = a2
b1' ⧆ a1 = b2' ⧆ a2
A, B, C: Type b1, b2: Batch A B C Hshape: shape b1 = shape b2 X: Type b1', b2': Batch A B (B -> X) Heq: tolist b1' = tolist b2' -> b1' = b2' a1, a2: A Hshape': shape (b1' ⧆ a1) = shape (b2' ⧆ a2) Hlist: tolist b1' ++ ret list A a1 =
tolist b2' ++ ret list A a2 H: a1 = a2
b1' = b2'
A, B, C: Type b1, b2: Batch A B C Hshape: shape b1 = shape b2 X: Type b1', b2': Batch A B (B -> X) Heq: tolist b1' = tolist b2' -> b1' = b2' a1, a2: A Hshape': shape (b1' ⧆ a1) = shape (b2' ⧆ a2) Hlist: tolist b1' ++ ret list A a1 =
tolist b2' ++ ret list A a2 H: a1 = a2 H0: b1' = b2'
b1' ⧆ a1 = b2' ⧆ a2
A, B, C: Type b1, b2: Batch A B C Hshape: shape b1 = shape b2 X: Type b1', b2': Batch A B (B -> X) Heq: tolist b1' = tolist b2' -> b1' = b2' a1, a2: A Hshape': shape (b1' ⧆ a1) = shape (b2' ⧆ a2) Hlist: tolist b1' ++ ret list A a1 =
tolist b2' ++ ret list A a2 H: a1 = a2
b1' = b2'
A, B, C: Type b1, b2: Batch A B C Hshape: shape b1 = shape b2 X: Type b1', b2': Batch A B (B -> X) Heq: tolist b1' = tolist b2' -> b1' = b2' a1, a2: A Hshape': shape (b1' ⧆ a1) = shape (b2' ⧆ a2) Hlist: tolist b1' ++ ret list A a1 =
tolist b2' ++ ret list A a2 H: a1 = a2
tolist b1' = tolist b2'
A, B, C: Type b1, b2: Batch A B C Hshape: shape b1 = shape b2 X: Type b1', b2': Batch A B (B -> X) Heq: tolist b1' = tolist b2' -> b1' = b2' a1, a2: A Hshape': shape (b1' ⧆ a1) = shape (b2' ⧆ a2) Hlist: tolist b1' ++ ret list A a1 =
tolist b2' ++ ret list A a2 H: a1 = a2
tolist b1' ++ ret list A ?a1 =
tolist b2' ++ ret list A ?a2
eauto.
A, B, C: Type b1, b2: Batch A B C Hshape: shape b1 = shape b2 X: Type b1', b2': Batch A B (B -> X) Heq: tolist b1' = tolist b2' -> b1' = b2' a1, a2: A Hshape': shape (b1' ⧆ a1) = shape (b2' ⧆ a2) Hlist: tolist b1' ++ ret list A a1 =
tolist b2' ++ ret list A a2 H: a1 = a2 H0: b1' = b2'
b1' ⧆ a1 = b2' ⧆ a2
A, B, C: Type b1, b2: Batch A B C Hshape: shape b1 = shape b2 X: Type b2': Batch A B (B -> X) Heq: tolist b2' = tolist b2' -> b2' = b2' a2: A Hshape': shape (b2' ⧆ a2) = shape (b2' ⧆ a2) Hlist: tolist b2' ++ ret list A a2 =
tolist b2' ++ ret list A a2
b2' ⧆ a2 = b2' ⧆ a2
reflexivity.Qed.EndBatch_shapely.Enddeconstruction.(** * Theory About Batch *)(******************************************************************************)SectionBatch_theory.
forall (ABC'CD : Type) (b : Batch A B (C -> D))
(f : C' -> C) (v : Vector (length_Batch b) B)
(v' : Vector
(length_Batch
(map (Batch A B) (precompose f) b)) B),
v ~~ v' ->
forallc : C',
Batch_make (map (Batch A B) (precompose f) b) v' c =
Batch_make b v (f c)
forall (ABC'CD : Type) (b : Batch A B (C -> D))
(f : C' -> C) (v : Vector (length_Batch b) B)
(v' : Vector
(length_Batch
(map (Batch A B) (precompose f) b)) B),
v ~~ v' ->
forallc : C',
Batch_make (map (Batch A B) (precompose f) b) v' c =
Batch_make b v (f c)
A, B, C', C, D: Type b: Batch A B (C -> D) f: C' -> C v: Vector (length_Batch b) B v': Vector
(length_Batch
(map (Batch A B) (precompose f) b)) B Hsim: v ~~ v' c: C'
Batch_make (map (Batch A B) (precompose f) b) v' c =
Batch_make b v (f c)
A, B, C', C, D: Type b: Batch A B (C -> D) f: C' -> C v: Vector (length_Batch b) B v': Vector
(length_Batch
(map (Batch A B) (precompose f) b)) B Hsim: v ~~ v' c: C'
precompose f
(Batch_make b
(coerce eq_sym
(batch_length_map (precompose f) b)
in v')) c = Batch_make b v (f c)
A, B, C', C, D: Type b: Batch A B (C -> D) f: C' -> C v: Vector (length_Batch b) B v': Vector
(length_Batch
(map (Batch A B) (precompose f) b)) B Hsim: v ~~ v' c: C'
Batch_make b
(coerce eq_sym
(batch_length_map
(fung : C -> D => g ○ f) b) in v')
(f c) = Batch_make b v (f c)
A, B, C', C, D: Type b: Batch A B (C -> D) f: C' -> C v: Vector (length_Batch b) B v': Vector
(length_Batch
(map (Batch A B) (precompose f) b)) B Hsim: v ~~ v' c: C'
coerce eq_sym
(batch_length_map (fung : C -> D => g ○ f) b)
in v' = v
A, B, C', C, D: Type b: Batch A B (C -> D) f: C' -> C v: Vector (length_Batch b) B v': Vector
(length_Batch
(map (Batch A B) (precompose f) b)) B Hsim: v ~~ v' c: C'
coerce eq_sym
(batch_length_map (fung : C -> D => g ○ f) b)
in v' ~~ v
A, B, C', C, D: Type b: Batch A B (C -> D) f: C' -> C v: Vector (length_Batch b) B v': Vector
(length_Batch
(map (Batch A B) (precompose f) b)) B Hsim: v ~~ v' c: C'
v' ~~ v
A, B, C', C, D: Type b: Batch A B (C -> D) f: C' -> C v: Vector (length_Batch b) B v': Vector
(length_Batch
(map (Batch A B) (precompose f) b)) B Hsim: v ~~ v' c: C'
proj1_sig v = proj1_sig v'
assumption.Qed.
forall (ABC'CD : Type) (b : Batch A B (C -> D))
(f : C' -> C)
(v : Vector
(length_Batch
(map (Batch A B) (precompose f) b)) B)
(c : C'),
Batch_make (map (Batch A B) (precompose f) b) v c =
Batch_make b
(coerce eq_sym (batch_length_map (precompose f) b)
in v) (f c)
forall (ABC'CD : Type) (b : Batch A B (C -> D))
(f : C' -> C)
(v : Vector
(length_Batch
(map (Batch A B) (precompose f) b)) B)
(c : C'),
Batch_make (map (Batch A B) (precompose f) b) v c =
Batch_make b
(coerce eq_sym (batch_length_map (precompose f) b)
in v) (f c)
A, B, C', C, D: Type b: Batch A B (C -> D) f: C' -> C v: Vector
(length_Batch (map (Batch A B) (precompose f) b))
B c: C'
Batch_make (map (Batch A B) (precompose f) b) v c =
Batch_make b
(coerce eq_sym (batch_length_map (precompose f) b)
in v) (f c)
A, B, C', C, D: Type b: Batch A B (C -> D) f: C' -> C v: Vector
(length_Batch (map (Batch A B) (precompose f) b))
B c: C'
coerce eq_sym (batch_length_map (precompose f) b) in v ~~
v
apply Vector_coerce_sim_l.Qed.
forall (ABB'C : Type) (b : Batch A B' C)
(f : B -> B') (v : Vector (length_Batch b) B)
(v' : Vector (length_Batch (mapsnd_Batch f b)) B),
v ~~ v' ->
Batch_make b (map (Vector (length_Batch b)) f v) =
Batch_make (mapsnd_Batch f b) v'
forall (ABB'C : Type) (b : Batch A B' C)
(f : B -> B') (v : Vector (length_Batch b) B)
(v' : Vector (length_Batch (mapsnd_Batch f b)) B),
v ~~ v' ->
Batch_make b (map (Vector (length_Batch b)) f v) =
Batch_make (mapsnd_Batch f b) v'
A, B, B', C: Type b: Batch A B' C f: B -> B' v: Vector (length_Batch b) B v': Vector (length_Batch (mapsnd_Batch f b)) B Hsim: v ~~ v'
Batch_make b (map (Vector (length_Batch b)) f v) =
Batch_make (mapsnd_Batch f b) v'
A, B, B', C: Type c: C f: B -> B' v: Vector (length_Batch (Done c)) B v': Vector (length_Batch (mapsnd_Batch f (Done c))) B Hsim: v ~~ v'
Batch_make (Done c)
(map (Vector (length_Batch (Done c))) f v) =
Batch_make (mapsnd_Batch f (Done c)) v'
A, B, B', C: Type b: Batch A B' (B' -> C) a: A f: B -> B' v: Vector (length_Batch (b ⧆ a)) B v': Vector (length_Batch (mapsnd_Batch f (b ⧆ a))) B Hsim: v ~~ v' IHb: forall (v : Vector (length_Batch b) B)
(v' : Vector (length_Batch (mapsnd_Batch f b))
B),
v ~~ v' ->
Batch_make b (map (Vector (length_Batch b)) f v) =
Batch_make (mapsnd_Batch f b) v'
Batch_make (b ⧆ a)
(map (Vector (length_Batch (b ⧆ a))) f v) =
Batch_make (mapsnd_Batch f (b ⧆ a)) v'
A, B, B', C: Type c: C f: B -> B' v: Vector (length_Batch (Done c)) B v': Vector (length_Batch (mapsnd_Batch f (Done c))) B Hsim: v ~~ v'
Batch_make (Done c)
(map (Vector (length_Batch (Done c))) f v) =
Batch_make (mapsnd_Batch f (Done c)) v'
A, B, B', C: Type c: C f: B -> B' v, v': Vector 0 B Hsim: v ~~ v'
Batch_make (Done c)
(map (Vector (length_Batch (Done c))) f v) =
Batch_make (mapsnd_Batch f (Done c)) v'
A, B, B', C: Type c: C f: B -> B' v, v': Vector 0 B Hsim: v ~~ v'
Batch_make (Done c)
(map (Vector (length_Batch (Done c))) f vnil) =
Batch_make (mapsnd_Batch f (Done c)) v'
A, B, B', C: Type c: C f: B -> B' v, v': Vector 0 B Hsim: v ~~ v'
Batch_make (Done c)
(map (Vector (length_Batch (Done c))) f vnil) =
Batch_make (mapsnd_Batch f (Done c)) vnil
reflexivity.
A, B, B', C: Type b: Batch A B' (B' -> C) a: A f: B -> B' v: Vector (length_Batch (b ⧆ a)) B v': Vector (length_Batch (mapsnd_Batch f (b ⧆ a))) B Hsim: v ~~ v' IHb: forall (v : Vector (length_Batch b) B)
(v' : Vector (length_Batch (mapsnd_Batch f b))
B),
v ~~ v' ->
Batch_make b (map (Vector (length_Batch b)) f v) =
Batch_make (mapsnd_Batch f b) v'
Batch_make (b ⧆ a)
(map (Vector (length_Batch (b ⧆ a))) f v) =
Batch_make (mapsnd_Batch f (b ⧆ a)) v'
A, B, B', C: Type b: Batch A B' (B' -> C) a: A f: B -> B' v: Vector (S (length_Batch b)) B v': Vector
(S
(length_Batch
(map (Batch A B) (precompose f)
(mapsnd_Batch f b)))) B Hsim: v ~~ v' IHb: forall (v : Vector (length_Batch b) B)
(v' : Vector (length_Batch (mapsnd_Batch f b))
B),
v ~~ v' ->
Batch_make b (map (Vector (length_Batch b)) f v) =
Batch_make (mapsnd_Batch f b) v'
Batch_make (b ⧆ a)
(map (Vector (length_Batch (b ⧆ a))) f v) =
Batch_make (mapsnd_Batch f (b ⧆ a)) v'
(* LHS *)
A, B, B', C: Type b: Batch A B' (B' -> C) a: A f: B -> B' v: Vector (S (length_Batch b)) B v': Vector
(S
(length_Batch
(map (Batch A B) (precompose f)
(mapsnd_Batch f b)))) B Hsim: v ~~ v' IHb: forall (v : Vector (length_Batch b) B)
(v' : Vector (length_Batch (mapsnd_Batch f b))
B),
v ~~ v' ->
Batch_make b (map (Vector (length_Batch b)) f v) =
Batch_make (mapsnd_Batch f b) v'
Batch_make b
(Vector_tl (map (Vector (length_Batch (b ⧆ a))) f v))
(Vector_hd (map (Vector (length_Batch (b ⧆ a))) f v)) =
Batch_make (mapsnd_Batch f (b ⧆ a)) v'
A, B, B', C: Type b: Batch A B' (B' -> C) a: A f: B -> B' v: Vector (S (length_Batch b)) B v': Vector
(S
(length_Batch
(map (Batch A B) (precompose f)
(mapsnd_Batch f b)))) B Hsim: v ~~ v' IHb: forall (v : Vector (length_Batch b) B)
(v' : Vector (length_Batch (mapsnd_Batch f b))
B),
v ~~ v' ->
Batch_make b (map (Vector (length_Batch b)) f v) =
Batch_make (mapsnd_Batch f b) v'
Batch_make b
(Vector_tl
(map (Vector (length_Batch (b ⧆ a))) f
(vcons (length_Batch b) (Vector_hd v)
(Vector_tl v))))
(Vector_hd
(map (Vector (length_Batch (b ⧆ a))) f
(vcons (length_Batch b) (Vector_hd v)
(Vector_tl v)))) =
Batch_make (mapsnd_Batch f (b ⧆ a)) v'
A, B, B', C: Type b: Batch A B' (B' -> C) a: A f: B -> B' v: Vector (S (length_Batch b)) B v': Vector
(S
(length_Batch
(map (Batch A B) (precompose f)
(mapsnd_Batch f b)))) B Hsim: v ~~ v' IHb: forall (v : Vector (length_Batch b) B)
(v' : Vector (length_Batch (mapsnd_Batch f b))
B),
v ~~ v' ->
Batch_make b (map (Vector (length_Batch b)) f v) =
Batch_make (mapsnd_Batch f b) v'
Batch_make b
(Vector_tl
(vcons (length_Batch b) (f (Vector_hd v))
(map (Vector (length_Batch b)) f (Vector_tl v))))
(Vector_hd
(vcons (length_Batch b) (f (Vector_hd v))
(map (Vector (length_Batch b)) f (Vector_tl v)))) =
Batch_make (mapsnd_Batch f (b ⧆ a)) v'
A, B, B', C: Type b: Batch A B' (B' -> C) a: A f: B -> B' v: Vector (S (length_Batch b)) B v': Vector
(S
(length_Batch
(map (Batch A B) (precompose f)
(mapsnd_Batch f b)))) B Hsim: v ~~ v' IHb: forall (v : Vector (length_Batch b) B)
(v' : Vector (length_Batch (mapsnd_Batch f b))
B),
v ~~ v' ->
Batch_make b (map (Vector (length_Batch b)) f v) =
Batch_make (mapsnd_Batch f b) v'
Batch_make b
(map (Vector (length_Batch b)) f (Vector_tl v))
(Vector_hd
(vcons (length_Batch b) (f (Vector_hd v))
(map (Vector (length_Batch b)) f (Vector_tl v)))) =
Batch_make (mapsnd_Batch f (b ⧆ a)) v'
A, B, B', C: Type b: Batch A B' (B' -> C) a: A f: B -> B' v: Vector (S (length_Batch b)) B v': Vector
(S
(length_Batch
(map (Batch A B) (precompose f)
(mapsnd_Batch f b)))) B Hsim: v ~~ v' IHb: forall (v : Vector (length_Batch b) B)
(v' : Vector (length_Batch (mapsnd_Batch f b))
B),
v ~~ v' ->
Batch_make b (map (Vector (length_Batch b)) f v) =
Batch_make (mapsnd_Batch f b) v'
Batch_make b
(map (Vector (length_Batch b)) f (Vector_tl v))
(f (Vector_hd v)) =
Batch_make (mapsnd_Batch f (b ⧆ a)) v'
(* RHS *)
A, B, B', C: Type b: Batch A B' (B' -> C) a: A f: B -> B' v: Vector (S (length_Batch b)) B v': Vector
(S
(length_Batch
(map (Batch A B) (precompose f)
(mapsnd_Batch f b)))) B Hsim: v ~~ v' IHb: forall (v : Vector (length_Batch b) B)
(v' : Vector (length_Batch (mapsnd_Batch f b))
B),
v ~~ v' ->
Batch_make b (map (Vector (length_Batch b)) f v) =
Batch_make (mapsnd_Batch f b) v'
Batch_make b
(map (Vector (length_Batch b)) f (Vector_tl v))
(f (Vector_hd v)) =
Batch_make (mapsnd_Batch f (b ⧆ a)) v'
(* ^^^ fails for some reason *)
A, B, B', C: Type b: Batch A B' (B' -> C) a: A f: B -> B' v: Vector (S (length_Batch b)) B v': Vector
(S
(length_Batch
(map (Batch A B) (precompose f)
(mapsnd_Batch f b)))) B Hsim: v ~~ v' IHb: forall (v : Vector (length_Batch b) B)
(v' : Vector (length_Batch (mapsnd_Batch f b))
B),
v ~~ v' ->
Batch_make b (map (Vector (length_Batch b)) f v) =
Batch_make (mapsnd_Batch f b) v'
Batch_make b
(map (Vector (length_Batch b)) f (Vector_tl v))
(f (Vector_hd v)) =
Batch_make
(map (Batch A B) (precompose f) (mapsnd_Batch f b))
(Vector_tl v') (Vector_hd v')
A, B, B', C: Type b: Batch A B' (B' -> C) a: A f: B -> B' v: Vector (S (length_Batch b)) B v': Vector
(S
(length_Batch
(map (Batch A B) (precompose f)
(mapsnd_Batch f b)))) B Hsim: v ~~ v' IHb: forall (v : Vector (length_Batch b) B)
(v' : Vector (length_Batch (mapsnd_Batch f b))
B),
v ~~ v' ->
Batch_make b (map (Vector (length_Batch b)) f v) =
Batch_make (mapsnd_Batch f b) v'
Batch_make b
(map (Vector (length_Batch b)) f (Vector_tl v))
(f (Vector_hd v)) =
Batch_make (mapsnd_Batch f b)
(coerce eq_sym
(batch_length_map (precompose f)
(mapsnd_Batch f b)) in Vector_tl v')
(f (Vector_hd v'))
A, B, B', C: Type b: Batch A B' (B' -> C) a: A f: B -> B' v: Vector (S (length_Batch b)) B v': Vector
(S
(length_Batch
(map (Batch A B) (precompose f)
(mapsnd_Batch f b)))) B Hsim: v ~~ v' IHb: forall (v : Vector (length_Batch b) B)
(v' : Vector (length_Batch (mapsnd_Batch f b))
B),
v ~~ v' ->
Batch_make b (map (Vector (length_Batch b)) f v) =
Batch_make (mapsnd_Batch f b) v'
f (Vector_hd v) = f (Vector_hd v')
A, B, B', C: Type b: Batch A B' (B' -> C) a: A f: B -> B' v: Vector (S (length_Batch b)) B v': Vector
(S
(length_Batch
(map (Batch A B)
(precompose f)
(mapsnd_Batch f b)))) B Hsim: v ~~ v' IHb: forall (v : Vector (length_Batch b) B)
(v' : Vector (length_Batch (mapsnd_Batch f b))
B),
v ~~ v' ->
Batch_make b (map (Vector (length_Batch b)) f v) =
Batch_make (mapsnd_Batch f b) v' cut: f (Vector_hd v) = f (Vector_hd v')
Batch_make b
(map (Vector (length_Batch b)) f (Vector_tl v))
(f (Vector_hd v)) =
Batch_make (mapsnd_Batch f b)
(coerce eq_sym
(batch_length_map
(precompose f)
(mapsnd_Batch f b)) in
Vector_tl v') (f (Vector_hd v'))
A, B, B', C: Type b: Batch A B' (B' -> C) a: A f: B -> B' v: Vector (S (length_Batch b)) B v': Vector
(S
(length_Batch
(map (Batch A B) (precompose f)
(mapsnd_Batch f b)))) B Hsim: v ~~ v' IHb: forall (v : Vector (length_Batch b) B)
(v' : Vector (length_Batch (mapsnd_Batch f b))
B),
v ~~ v' ->
Batch_make b (map (Vector (length_Batch b)) f v) =
Batch_make (mapsnd_Batch f b) v'
f (Vector_hd v) = f (Vector_hd v')
A, B, B', C: Type b: Batch A B' (B' -> C) a: A f: B -> B' v: Vector (S (length_Batch b)) B v': Vector
(S
(length_Batch
(map (Batch A B) (precompose f)
(mapsnd_Batch f b)))) B Hsim: v ~~ v' IHb: forall (v : Vector (length_Batch b) B)
(v' : Vector (length_Batch (mapsnd_Batch f b))
B),
v ~~ v' ->
Batch_make b (map (Vector (length_Batch b)) f v) =
Batch_make (mapsnd_Batch f b) v' H0: proj1_sig v = proj1_sig v'
f (Vector_hd v) = f (Vector_hd v')
A, B, B', C: Type b: Batch A B' (B' -> C) a: A f: B -> B' v: Vector (S (length_Batch b)) B v': Vector
(S
(length_Batch
(map (Batch A B) (precompose f)
(mapsnd_Batch f b)))) B Hsim: v ~~ v' IHb: forall (v : Vector (length_Batch b) B)
(v' : Vector (length_Batch (mapsnd_Batch f b))
B),
v ~~ v' ->
Batch_make b (map (Vector (length_Batch b)) f v) =
Batch_make (mapsnd_Batch f b) v' H0: proj1_sig v = proj1_sig v'
Vector_hd v = Vector_hd v'
apply (Vector_hd_sim Hsim).
A, B, B', C: Type b: Batch A B' (B' -> C) a: A f: B -> B' v: Vector (S (length_Batch b)) B v': Vector
(S
(length_Batch
(map (Batch A B) (precompose f)
(mapsnd_Batch f b)))) B Hsim: v ~~ v' IHb: forall (v : Vector (length_Batch b) B)
(v' : Vector (length_Batch (mapsnd_Batch f b))
B),
v ~~ v' ->
Batch_make b (map (Vector (length_Batch b)) f v) =
Batch_make (mapsnd_Batch f b) v' cut: f (Vector_hd v) = f (Vector_hd v')
Batch_make b
(map (Vector (length_Batch b)) f (Vector_tl v))
(f (Vector_hd v)) =
Batch_make (mapsnd_Batch f b)
(coerce eq_sym
(batch_length_map (precompose f)
(mapsnd_Batch f b)) in Vector_tl v')
(f (Vector_hd v'))
A, B, B', C: Type b: Batch A B' (B' -> C) a: A f: B -> B' v: Vector (S (length_Batch b)) B v': Vector
(S
(length_Batch
(map (Batch A B) (precompose f)
(mapsnd_Batch f b)))) B Hsim: v ~~ v' IHb: forall (v : Vector (length_Batch b) B)
(v' : Vector (length_Batch (mapsnd_Batch f b))
B),
v ~~ v' ->
Batch_make b (map (Vector (length_Batch b)) f v) =
Batch_make (mapsnd_Batch f b) v' cut: f (Vector_hd v) = f (Vector_hd v')
Batch_make b
(map (Vector (length_Batch b)) f (Vector_tl v))
(f (Vector_hd v')) =
Batch_make (mapsnd_Batch f b)
(coerce eq_sym
(batch_length_map (precompose f)
(mapsnd_Batch f b)) in Vector_tl v')
(f (Vector_hd v'))
A, B, B', C: Type b: Batch A B' (B' -> C) a: A f: B -> B' v: Vector (S (length_Batch b)) B v': Vector
(S
(length_Batch
(map (Batch A B) (precompose f)
(mapsnd_Batch f b)))) B Hsim: v ~~ v' IHb: forallv' : Vector (length_Batch (mapsnd_Batch f b))
B,
Vector_tl v ~~ v' ->
Batch_make b
(map (Vector (length_Batch b)) f (Vector_tl v)) =
Batch_make (mapsnd_Batch f b) v' cut: f (Vector_hd v) = f (Vector_hd v')
Batch_make b
(map (Vector (length_Batch b)) f (Vector_tl v))
(f (Vector_hd v')) =
Batch_make (mapsnd_Batch f b)
(coerce eq_sym
(batch_length_map (precompose f)
(mapsnd_Batch f b)) in Vector_tl v')
(f (Vector_hd v'))
A, B, B', C: Type b: Batch A B' (B' -> C) a: A f: B -> B' v: Vector (S (length_Batch b)) B v': Vector
(S
(length_Batch
(map (Batch A B) (precompose f)
(mapsnd_Batch f b)))) B Hsim: v ~~ v' IHb: Vector_tl v ~~
coerce eq_sym
(batch_length_map
(precompose f)
(mapsnd_Batch f b)) in
Vector_tl v' ->
Batch_make b
(map (Vector (length_Batch b)) f (Vector_tl v)) =
Batch_make (mapsnd_Batch f b)
(coerce eq_sym
(batch_length_map
(precompose f)
(mapsnd_Batch f b))
in Vector_tl v') cut: f (Vector_hd v) = f (Vector_hd v')
Batch_make b
(map (Vector (length_Batch b)) f (Vector_tl v))
(f (Vector_hd v')) =
Batch_make (mapsnd_Batch f b)
(coerce eq_sym
(batch_length_map (precompose f)
(mapsnd_Batch f b)) in Vector_tl v')
(f (Vector_hd v'))
A, B, B', C: Type b: Batch A B' (B' -> C) a: A f: B -> B' v: Vector (S (length_Batch b)) B v': Vector
(S
(length_Batch
(map (Batch A B) (precompose f)
(mapsnd_Batch f b)))) B Hsim: v ~~ v' IHb: Vector_tl v ~~
coerce eq_sym
(batch_length_map
(precompose f)
(mapsnd_Batch f b)) in
Vector_tl v' ->
Batch_make b
(map (Vector (length_Batch b)) f (Vector_tl v)) =
Batch_make (mapsnd_Batch f b)
(coerce eq_sym
(batch_length_map
(precompose f)
(mapsnd_Batch f b))
in Vector_tl v') cut: f (Vector_hd v) = f (Vector_hd v')
Batch_make (mapsnd_Batch f b)
(coerce eq_sym
(batch_length_map (precompose f)
(mapsnd_Batch f b)) in Vector_tl v')
(f (Vector_hd v')) =
Batch_make (mapsnd_Batch f b)
(coerce eq_sym
(batch_length_map (precompose f)
(mapsnd_Batch f b)) in Vector_tl v')
(f (Vector_hd v'))
A, B, B', C: Type b: Batch A B' (B' -> C) a: A f: B -> B' v: Vector (S (length_Batch b)) B v': Vector
(S
(length_Batch
(map (Batch A B)
(precompose f)
(mapsnd_Batch f b)))) B Hsim: v ~~ v' IHb: Vector_tl v ~~
coerce eq_sym
(batch_length_map
(precompose f)
(mapsnd_Batch f b)) in
Vector_tl v' ->
Batch_make b
(map (Vector (length_Batch b)) f (Vector_tl v)) =
Batch_make (mapsnd_Batch f b)
(coerce eq_sym
(batch_length_map
(precompose f)
(mapsnd_Batch f b))
in Vector_tl v') cut: f (Vector_hd v) = f (Vector_hd v')
Vector_tl v ~~
coerce eq_sym
(batch_length_map
(precompose f)
(mapsnd_Batch f b)) in
Vector_tl v'
A, B, B', C: Type b: Batch A B' (B' -> C) a: A f: B -> B' v: Vector (S (length_Batch b)) B v': Vector
(S
(length_Batch
(map (Batch A B) (precompose f)
(mapsnd_Batch f b)))) B Hsim: v ~~ v' IHb: Vector_tl v ~~
coerce eq_sym
(batch_length_map
(precompose f)
(mapsnd_Batch f b)) in
Vector_tl v' ->
Batch_make b
(map (Vector (length_Batch b)) f (Vector_tl v)) =
Batch_make (mapsnd_Batch f b)
(coerce eq_sym
(batch_length_map
(precompose f)
(mapsnd_Batch f b))
in Vector_tl v') cut: f (Vector_hd v) = f (Vector_hd v')
Batch_make (mapsnd_Batch f b)
(coerce eq_sym
(batch_length_map (precompose f)
(mapsnd_Batch f b)) in Vector_tl v')
(f (Vector_hd v')) =
Batch_make (mapsnd_Batch f b)
(coerce eq_sym
(batch_length_map (precompose f)
(mapsnd_Batch f b)) in Vector_tl v')
(f (Vector_hd v'))
reflexivity.
A, B, B', C: Type b: Batch A B' (B' -> C) a: A f: B -> B' v: Vector (S (length_Batch b)) B v': Vector
(S
(length_Batch
(map (Batch A B) (precompose f)
(mapsnd_Batch f b)))) B Hsim: v ~~ v' IHb: Vector_tl v ~~
coerce eq_sym
(batch_length_map
(precompose f)
(mapsnd_Batch f b)) in
Vector_tl v' ->
Batch_make b
(map (Vector (length_Batch b)) f (Vector_tl v)) =
Batch_make (mapsnd_Batch f b)
(coerce eq_sym
(batch_length_map
(precompose f)
(mapsnd_Batch f b))
in Vector_tl v') cut: f (Vector_hd v) = f (Vector_hd v')
Vector_tl v ~~
coerce eq_sym
(batch_length_map (precompose f)
(mapsnd_Batch f b)) in Vector_tl v'
A, B, B', C: Type b: Batch A B' (B' -> C) a: A f: B -> B' v: Vector (S (length_Batch b)) B v': Vector
(S
(length_Batch
(map (Batch A B) (precompose f)
(mapsnd_Batch f b)))) B Hsim: v ~~ v' IHb: Vector_tl v ~~
coerce eq_sym
(batch_length_map
(precompose f)
(mapsnd_Batch f b)) in
Vector_tl v' ->
Batch_make b
(map (Vector (length_Batch b)) f (Vector_tl v)) =
Batch_make (mapsnd_Batch f b)
(coerce eq_sym
(batch_length_map
(precompose f)
(mapsnd_Batch f b))
in Vector_tl v') cut: f (Vector_hd v) = f (Vector_hd v')
Vector_tl v ~~ Vector_tl v'
A, B, B', C: Type b: Batch A B' (B' -> C) a: A f: B -> B' v: Vector (S (length_Batch b)) B v': Vector
(S
(length_Batch
(map (Batch A B) (precompose f)
(mapsnd_Batch f b)))) B Hsim: v ~~ v' IHb: Vector_tl v ~~
coerce eq_sym
(batch_length_map
(precompose f)
(mapsnd_Batch f b)) in
Vector_tl v' ->
Batch_make b
(map (Vector (length_Batch b)) f (Vector_tl v)) =
Batch_make (mapsnd_Batch f b)
(coerce eq_sym
(batch_length_map
(precompose f)
(mapsnd_Batch f b))
in Vector_tl v') cut: f (Vector_hd v) = f (Vector_hd v')
v ~~ v'
assumption.Qed.
forall (nm : nat) (Heq : n = m) (AB : Type)
(f : A -> B) (v : Vector n A),
coerce Heq in map (Vector n) f v =
map (Vector m) f (coerce Heq in v)
forall (nm : nat) (Heq : n = m) (AB : Type)
(f : A -> B) (v : Vector n A),
coerce Heq in map (Vector n) f v =
map (Vector m) f (coerce Heq in v)
n, m: nat Heq: n = m A, B: Type f: A -> B v: Vector n A
coerce Heq in map (Vector n) f v =
map (Vector m) f (coerce Heq in v)
n, m: nat Heq: n = m A, B: Type f: A -> B v: Vector n A
coerce Heq in map (Vector n) f v ~~
map (Vector m) f (coerce Heq in v)
n, m: nat Heq: n = m A, B: Type f: A -> B v: Vector n A
coerce Heq in map (Vector n) f v ~~ map (Vector n) f v
n, m: nat Heq: n = m A, B: Type f: A -> B v: Vector n A
map (Vector n) f v ~~
map (Vector m) f (coerce Heq in v)
n, m: nat Heq: n = m A, B: Type f: A -> B v: Vector n A
coerce Heq in map (Vector n) f v ~~ map (Vector n) f v
n, m: nat Heq: n = m A, B: Type f: A -> B v: Vector n A
map (Vector n) f v ~~ coerce Heq in map (Vector n) f v
apply Vector_coerce_sim_r.
n, m: nat Heq: n = m A, B: Type f: A -> B v: Vector n A
map (Vector n) f v ~~
map (Vector m) f (coerce Heq in v)
apply map_coerce_Vector.Qed.
forall (ABB'C : Type) (b : Batch A B' C)
(f : B -> B')
(v : Vector (length_Batch (mapsnd_Batch f b)) B),
Batch_make (mapsnd_Batch f b) v =
Batch_make b
(coerce eq_sym (batch_length_mapsnd f b)
in map (Vector (length_Batch (mapsnd_Batch f b))) f
v)
forall (ABB'C : Type) (b : Batch A B' C)
(f : B -> B')
(v : Vector (length_Batch (mapsnd_Batch f b)) B),
Batch_make (mapsnd_Batch f b) v =
Batch_make b
(coerce eq_sym (batch_length_mapsnd f b)
in map (Vector (length_Batch (mapsnd_Batch f b))) f
v)
A, B, B', C: Type b: Batch A B' C f: B -> B' v: Vector (length_Batch (mapsnd_Batch f b)) B
Batch_make (mapsnd_Batch f b) v =
Batch_make b
(coerce eq_sym (batch_length_mapsnd f b)
in map (Vector (length_Batch (mapsnd_Batch f b))) f
v)
A, B, B', C: Type b: Batch A B' C f: B -> B' v: Vector (length_Batch (mapsnd_Batch f b)) B
Batch_make b
(coerce eq_sym (batch_length_mapsnd f b)
in map (Vector (length_Batch (mapsnd_Batch f b))) f
v) = Batch_make (mapsnd_Batch f b) v
A, B, B', C: Type b: Batch A B' C f: B -> B' v: Vector (length_Batch (mapsnd_Batch f b)) B
Batch_make b
(map (Vector (length_Batch b)) f
(coerce eq_sym (batch_length_mapsnd f b) in v)) =
Batch_make (mapsnd_Batch f b) v
A, B, B', C: Type b: Batch A B' C f: B -> B' v: Vector (length_Batch (mapsnd_Batch f b)) B
forall (G : Type -> Type) (Map_G : Map G)
(Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall (ABC : Type) (b : Batch A B C) (x : G B)
(A' : Type) (v : Vector (length_Batch b) A'),
runBatch (const x) b =
runBatch (const x) (Batch_replace_contents b v)
forall (G : Type -> Type) (Map_G : Map G)
(Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall (ABC : Type) (b : Batch A B C) (x : G B)
(A' : Type) (v : Vector (length_Batch b) A'),
runBatch (const x) b =
runBatch (const x) (Batch_replace_contents b v)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B C x: G B A': Type v: Vector (length_Batch b) A'
runBatch (const x) b =
runBatch (const x) (Batch_replace_contents b v)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type c: C x: G B A': Type v: Vector (length_Batch (Done c)) A'
runBatch (const x) (Done c) =
runBatch (const x) (Batch_replace_contents (Done c) v)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B (B -> C) a: A x: G B A': Type v: Vector (length_Batch (b ⧆ a)) A' IHb: forallv : Vector (length_Batch b) A',
runBatch (const x) b =
runBatch (const x) (Batch_replace_contents b v)
runBatch (const x) (b ⧆ a) =
runBatch (const x) (Batch_replace_contents (b ⧆ a) v)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type c: C x: G B A': Type v: Vector (length_Batch (Done c)) A'
runBatch (const x) (Done c) =
runBatch (const x) (Batch_replace_contents (Done c) v)
reflexivity.
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B (B -> C) a: A x: G B A': Type v: Vector (length_Batch (b ⧆ a)) A' IHb: forallv : Vector (length_Batch b) A',
runBatch (const x) b =
runBatch (const x) (Batch_replace_contents b v)
runBatch (const x) (b ⧆ a) =
runBatch (const x) (Batch_replace_contents (b ⧆ a) v)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B (B -> C) a: A x: G B A': Type v: Vector (length_Batch (b ⧆ a)) A' IHb: forallv : Vector (length_Batch b) A',
runBatch (const x) b =
runBatch (const x) (Batch_replace_contents b v)
runBatch (const x) b <⋆> const x a =
runBatch (const x)
(Batch_replace_contents b (Vector_tl v)) <⋆>
const x (Vector_hd v)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B (B -> C) a: A x: G B A': Type v: Vector (length_Batch (b ⧆ a)) A' IHb: forallv : Vector (length_Batch b) A',
runBatch (const x) b =
runBatch (const x) (Batch_replace_contents b v)
runBatch (const x) b =
runBatch (const x)
(Batch_replace_contents b (Vector_tl v))
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G
forall (ABC : Type) (b : Batch A B C) (f : A -> G B),
map G (Batch_make b) (traverse f (Batch_contents b)) =
forwards (runBatch (mkBackwards ∘ f) b)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G
forall (ABC : Type) (b : Batch A B C) (f : A -> G B),
map G (Batch_make b) (traverse f (Batch_contents b)) =
forwards (runBatch (mkBackwards ∘ f) b)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B C f: A -> G B
map G (Batch_make b) (traverse f (Batch_contents b)) =
forwards (runBatch (mkBackwards ∘ f) b)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type c: C f: A -> G B
map G (Batch_make (Done c))
(traverse f (Batch_contents (Done c))) =
forwards (runBatch (mkBackwards ∘ f) (Done c))
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B (B -> C) a: A f: A -> G B IHb: map G (Batch_make b)
(traverse f (Batch_contents b)) =
forwards (runBatch (mkBackwards ∘ f) b)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type c: C f: A -> G B
map G (Batch_make (Done c))
(traverse f (Batch_contents (Done c))) =
forwards (runBatch (mkBackwards ∘ f) (Done c))
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type c: C f: A -> G B
map G (fun_ : Vector 0 B => c)
(pure G
(exist (funl : list B => length l = 0) nil
eq_refl)) = pure G c
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type c: C f: A -> G B
pure G c = pure G c
reflexivity.
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B (B -> C) a: A f: A -> G B IHb: map G (Batch_make b)
(traverse f (Batch_contents b)) =
forwards (runBatch (mkBackwards ∘ f) b)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B (B -> C) a: A f: A -> G B IHb: map G (Batch_make b)
(traverse f (Batch_contents b)) =
forwards (runBatch (mkBackwards ∘ f) b)
map G (Batch_make (b ⧆ a))
(traverse f
(vcons (length_Batch b) a (Batch_contents b))) =
forwards (runBatch (mkBackwards ∘ f) (b ⧆ a))
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B (B -> C) a: A f: A -> G B IHb: map G (Batch_make b)
(traverse f (Batch_contents b)) =
forwards (runBatch (mkBackwards ∘ f) b)
map G (Batch_make (b ⧆ a))
(traverse f
(vcons (length_Batch b) a (Batch_contents b))) =
forwards (runBatch (mkBackwards ∘ f) (b ⧆ a))
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B (B -> C) a: A f: A -> G B IHb: map G (Batch_make b)
(traverse f (Batch_contents b)) =
forwards (runBatch (mkBackwards ∘ f) b)
map G (Batch_make (b ⧆ a))
(pure G (vcons (length_Batch b)) <⋆> f a <⋆>
traverse f (Batch_contents b)) =
forwards (runBatch (mkBackwards ∘ f) (b ⧆ a))
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B (B -> C) a: A f: A -> G B IHb: map G (Batch_make b)
(traverse f (Batch_contents b)) =
forwards (runBatch (mkBackwards ∘ f) b)
map G (Batch_make (b ⧆ a))
(pure G (vcons (length_Batch b)) <⋆> f a <⋆>
traverse f (Batch_contents b)) =
forwards
(runBatch (mkBackwards ∘ f) b <⋆>
(mkBackwards ∘ f) a)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B (B -> C) a: A f: A -> G B IHb: map G (Batch_make b)
(traverse f (Batch_contents b)) =
forwards (runBatch (mkBackwards ∘ f) b)
map G (Batch_make (b ⧆ a))
(pure G (vcons (length_Batch b)) <⋆> f a <⋆>
traverse f (Batch_contents b)) =
map G evalAt (forwards ((mkBackwards ∘ f) a)) <⋆>
forwards (runBatch (mkBackwards ∘ f) b)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B (B -> C) a: A f: A -> G B IHb: map G (Batch_make b)
(traverse f (Batch_contents b)) =
forwards (runBatch (mkBackwards ∘ f) b)
map G (compose (Batch_make (b ⧆ a)))
(pure G (vcons (length_Batch b)) <⋆> f a) <⋆>
traverse f (Batch_contents b) =
map G evalAt (forwards ((mkBackwards ∘ f) a)) <⋆>
forwards (runBatch (mkBackwards ∘ f) b)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B (B -> C) a: A f: A -> G B IHb: map G (Batch_make b)
(traverse f (Batch_contents b)) =
forwards (runBatch (mkBackwards ∘ f) b)
map G (compose (compose (Batch_make (b ⧆ a))))
(pure G (vcons (length_Batch b))) <⋆> f a <⋆>
traverse f (Batch_contents b) =
map G evalAt (forwards ((mkBackwards ∘ f) a)) <⋆>
forwards (runBatch (mkBackwards ∘ f) b)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B (B -> C) a: A f: A -> G B IHb: map G (Batch_make b)
(traverse f (Batch_contents b)) =
forwards (runBatch (mkBackwards ∘ f) b)
pure G
(compose (Batch_make (b ⧆ a))
∘ vcons (length_Batch b)) <⋆> f a <⋆>
traverse f (Batch_contents b) =
map G evalAt (forwards ((mkBackwards ∘ f) a)) <⋆>
forwards (runBatch (mkBackwards ∘ f) b)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B (B -> C) a: A f: A -> G B IHb: map G (Batch_make b)
(traverse f (Batch_contents b)) =
forwards (runBatch (mkBackwards ∘ f) b)
pure G
(compose (Batch_make (b ⧆ a))
∘ vcons (length_Batch b)) <⋆> f a <⋆>
traverse f (Batch_contents b) =
map G evalAt (forwards ((mkBackwards ∘ f) a)) <⋆>
map G (Batch_make b) (traverse f (Batch_contents b))
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B (B -> C) a: A f: A -> G B IHb: map G (Batch_make b)
(traverse f (Batch_contents b)) =
forwards (runBatch (mkBackwards ∘ f) b)
pure G
(compose (Batch_make (b ⧆ a))
∘ vcons (length_Batch b)) <⋆> f a <⋆>
traverse f (Batch_contents b) =
pure G evalAt <⋆> forwards ((mkBackwards ∘ f) a) <⋆>
map G (Batch_make b) (traverse f (Batch_contents b))
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B (B -> C) a: A f: A -> G B IHb: map G (Batch_make b)
(traverse f (Batch_contents b)) =
forwards (runBatch (mkBackwards ∘ f) b)
pure G
(compose (Batch_make (b ⧆ a))
∘ vcons (length_Batch b)) <⋆> f a <⋆>
traverse f (Batch_contents b) =
map G (precompose (Batch_make b))
(pure G evalAt <⋆> forwards ((mkBackwards ∘ f) a)) <⋆>
traverse f (Batch_contents b)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B (B -> C) a: A f: A -> G B IHb: map G (Batch_make b)
(traverse f (Batch_contents b)) =
forwards (runBatch (mkBackwards ∘ f) b)
pure G
(compose (Batch_make (b ⧆ a))
∘ vcons (length_Batch b)) <⋆> f a <⋆>
traverse f (Batch_contents b) =
map G (compose (precompose (Batch_make b)))
(pure G evalAt) <⋆> forwards ((mkBackwards ∘ f) a) <⋆>
traverse f (Batch_contents b)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B (B -> C) a: A f: A -> G B IHb: map G (Batch_make b)
(traverse f (Batch_contents b)) =
forwards (runBatch (mkBackwards ∘ f) b)
pure G
(compose (Batch_make (b ⧆ a))
∘ vcons (length_Batch b)) <⋆> f a <⋆>
traverse f (Batch_contents b) =
pure G (precompose (Batch_make b) ∘ evalAt) <⋆>
forwards ((mkBackwards ∘ f) a) <⋆>
traverse f (Batch_contents b)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B (B -> C) a: A f: A -> G B IHb: map G (Batch_make b)
(traverse f (Batch_contents b)) =
forwards (runBatch (mkBackwards ∘ f) b)
pure G
(compose (Batch_make (b ⧆ a))
∘ vcons (length_Batch b)) <⋆> f a =
pure G (precompose (Batch_make b) ∘ evalAt) <⋆>
forwards ((mkBackwards ∘ f) a)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B (B -> C) a: A f: A -> G B IHb: map G (Batch_make b)
(traverse f (Batch_contents b)) =
forwards (runBatch (mkBackwards ∘ f) b)
pure G
(compose (Batch_make (b ⧆ a))
∘ vcons (length_Batch b)) =
pure G (precompose (Batch_make b) ∘ evalAt)
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B (B -> C) a: A f: A -> G B IHb: map G (Batch_make b)
(traverse f (Batch_contents b)) =
forwards (runBatch (mkBackwards ∘ f) b)
compose (Batch_make (b ⧆ a)) ∘ vcons (length_Batch b) =
precompose (Batch_make b) ∘ evalAt
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B (B -> C) a: A f: A -> G B IHb: map G (Batch_make b)
(traverse f (Batch_contents b)) =
forwards (runBatch (mkBackwards ∘ f) b) b': B v': Vector (length_Batch b) B
(compose (Batch_make (b ⧆ a)) ∘ vcons (length_Batch b))
b' v' = (precompose (Batch_make b) ∘ evalAt) b' v'
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B (B -> C) a: A f: A -> G B IHb: map G (Batch_make b)
(traverse f (Batch_contents b)) =
forwards (runBatch (mkBackwards ∘ f) b) b': B v': Vector (length_Batch b) B
Batch_make (b ⧆ a) (vcons (length_Batch b) b' v') =
Batch_make b v' b'
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B (B -> C) a: A f: A -> G B IHb: map G (Batch_make b)
(traverse f (Batch_contents b)) =
forwards (runBatch (mkBackwards ∘ f) b) b': B v': Vector (length_Batch b) B
Batch_make b
(Vector_tl (vcons (length_Batch b) b' v'))
(Vector_hd (vcons (length_Batch b) b' v')) =
Batch_make b v' b'
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B (B -> C) a: A f: A -> G B IHb: map G (Batch_make b)
(traverse f (Batch_contents b)) =
forwards (runBatch (mkBackwards ∘ f) b) b': B v': Vector (length_Batch b) B
Batch_make b v'
(Vector_hd (vcons (length_Batch b) b' v')) =
Batch_make b v' b'
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B (B -> C) a: A f: A -> G B IHb: map G (Batch_make b)
(traverse f (Batch_contents b)) =
forwards (runBatch (mkBackwards ∘ f) b) b': B v': Vector (length_Batch b) B
Batch_make b v' b' = Batch_make b v' b'
reflexivity.Qed.
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G
forall (ABC : Type) (b : Batch A B C) (f : A -> G B),
runBatch f b =
map G (Batch_make b)
(forwards
(traverse (mkBackwards ∘ f) (Batch_contents b)))
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G
forall (ABC : Type) (b : Batch A B C) (f : A -> G B),
runBatch f b =
map G (Batch_make b)
(forwards
(traverse (mkBackwards ∘ f) (Batch_contents b)))
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B C f: A -> G B
runBatch f b =
map G (Batch_make b)
(forwards
(traverse (mkBackwards ∘ f) (Batch_contents b)))
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B C f: A -> G B
map G (Batch_make b)
(forwards
(traverse (mkBackwards ∘ f) (Batch_contents b))) =
runBatch f b
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B C f: A -> G B
forwards
(map (Backwards G) (Batch_make b)
(traverse (mkBackwards ∘ f) (Batch_contents b))) =
runBatch f b
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B C f: A -> G B
forwards
(forwards
(runBatch (mkBackwards ∘ (mkBackwards ∘ f)) b)) =
runBatch f b
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B C f: A -> G B
forwards
(forwards
((map (Backwards (Backwards G)) extract_Batch
∘ traverse (mkBackwards ∘ (mkBackwards ∘ f))) b)) =
runBatch f b
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B C f: A -> G B
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B C f: A -> G B
map G extract_Batch
(forwards
(forwards
(traverse (mkBackwards ∘ (mkBackwards ∘ f)) b))) =
(map G extract_Batch ∘ traverse f) b
G: Type -> Type Map_G: Map G Pure_G: Pure G Mult_G: Mult G H: Applicative G A, B, C: Type b: Batch A B C f: A -> G B
map G extract_Batch (traverse f b) =
(map G extract_Batch ∘ traverse f) b
reflexivity.Qed.(** * Annotating <<Batch>> with Proofs of Occurrence *)(******************************************************************************)Require Import ContainerFunctor.Import ContainerFunctor.Notations.Import Applicative.Notations.Import Functors.Early.Subset.Import Subset.Notations.Sectionannotate_Batch_elements.(** ** Lemmas regarding <<tosubset>> *)(******************************************************************************)
A, B, C: Type
forall (a' : A) (rest : Batch A B (B -> C)) (a : A),
tosubset rest a -> tosubset (rest ⧆ a') a
A, B, C: Type
forall (a' : A) (rest : Batch A B (B -> C)) (a : A),
tosubset rest a -> tosubset (rest ⧆ a') a
A, B, C: Type a': A rest: Batch A B (B -> C) a: A
tosubset rest a -> tosubset (rest ⧆ a') a
A, B, C: Type a': A rest: Batch A B (B -> C) a: A
tosubset rest a -> (tosubset rest ∪ {{a'}}) a
A, B, C: Type a': A rest: Batch A B (B -> C) a: A
tosubset rest a -> tosubset rest a \/ a' = a
tauto.Defined.
A, B, C: Type
forall (rest : Batch A B (B -> C)) (a : A),
tosubset (rest ⧆ a) a
A, B, C: Type
forall (rest : Batch A B (B -> C)) (a : A),
tosubset (rest ⧆ a) a
A, B, C: Type rest: Batch A B (B -> C) a: A
tosubset (rest ⧆ a) a
A, B, C: Type rest: Batch A B (B -> C) a: A
(tosubset rest ∪ {{a}}) a
A, B, C: Type rest: Batch A B (B -> C) a: A
tosubset rest a \/ a = a
tauto.Qed.
A, B, C: Type
forall (a' : A) (rest : Batch A B (B -> C)) (a : A),
a ∈ rest -> a ∈ (rest ⧆ a')
A, B, C: Type
forall (a' : A) (rest : Batch A B (B -> C)) (a : A),
a ∈ rest -> a ∈ (rest ⧆ a')
A, B, C: Type a': A rest: Batch A B (B -> C) a: A
a ∈ rest -> a ∈ (rest ⧆ a')
A, B, C: Type a': A rest: Batch A B (B -> C) a: A
a ∈ rest -> a ∈ rest \/ a = a'
tauto.Defined.
A, B, C: Type
forall (rest : Batch A B (B -> C)) (a : A),
a ∈ (rest ⧆ a)
A, B, C: Type
forall (rest : Batch A B (B -> C)) (a : A),
a ∈ (rest ⧆ a)
A, B, C: Type rest: Batch A B (B -> C) a: A
a ∈ (rest ⧆ a)
A, B, C: Type rest: Batch A B (B -> C) a: A
a ∈ rest \/ a = a
tauto.Qed.(** ** Annotation Operation *)(******************************************************************************)DefinitionsigMap {A: Type} (PQ: A -> Prop) (Himpl: foralla, P a -> Q a):
sig P -> sig Q :=
funσ => match σ with
| exist _ a h => exist Q a (Himpl a h)
end.
A, B, C: Type
forall (a : A) (b_orig : Batch A B (B -> C)),
Batch {a' : A | a' ∈ b_orig} B (B -> C) ->
Batch {a' : A | a' ∈ (b_orig ⧆ a)} B (B -> C)
A, B, C: Type
forall (a : A) (b_orig : Batch A B (B -> C)),
Batch {a' : A | a' ∈ b_orig} B (B -> C) ->
Batch {a' : A | a' ∈ (b_orig ⧆ a)} B (B -> C)
A, B, C: Type a: A b_orig: Batch A B (B -> C) b_recc: Batch {a' : A | a' ∈ b_orig} B (B -> C)
Batch {a' : A | a' ∈ (b_orig ⧆ a)} B (B -> C)
apply (map (BATCH1 B (B -> C))
(sigMap (funa0 : A => a0 ∈ b_orig)
(funa0 : A => a0 ∈ (b_orig ⧆ a))
(element_of_Step1 a b_orig)) b_recc).Defined.Fixpointannotate_occurrence
{ABC: Type}
(b: Batch A B C):
Batch {a| element_of (F := BATCH1 B C) a b} B C :=
match b with
| Done c => Done c
| Step rest a =>
Step (annotate_occurrence_helper a rest (annotate_occurrence rest))
(exist (tosubset (rest ⧆ a))
a (element_of_Step2 rest a))
end.(** * <<runBatch>> Assuming Proofs of Occurrence *)(******************************************************************************)DefinitionrunBatch_with_occurrence
{ABC} (G: Type -> Type)
`{Applicative G}:
forall (b: Batch A B C)
`(f: {a | element_of (F := BATCH1 B C) a b} -> G B), G C :=
funbf => runBatch f (annotate_occurrence b).Endannotate_Batch_elements.