Tealeaves.Theory.TraversableFunctor
From Tealeaves Require Export
Classes.Kleisli.TraversableFunctor
Classes.Kleisli.Theory.TraversableFunctor
Classes.Categorical.ContainerFunctor
Classes.Categorical.ShapelyFunctor
Classes.Categorical.ApplicativeCommutativeIdempotent
Adapters.KleisliToCoalgebraic.TraversableFunctor
Functors.Batch
Functors.List
Functors.VectorRefinement.
Import Coalgebraic.TraversableFunctor (ToBatch, toBatch).
Import KleisliToCoalgebraic.TraversableFunctor.DerivedInstances.
Import Subset.Notations.
Import Applicative.Notations.
Import ContainerFunctor.Notations.
Import ProductFunctor.Notations.
Import Kleisli.TraversableFunctor.Notations.
Import Batch.Notations.
Import Monoid.Notations.
Import VectorRefinement.Notations.
#[local] Generalizable Variables F T G A B C M ϕ.
#[local] Arguments mapfst_Batch {B C A1 A2}%type_scope
f%function_scope b.
#[local] Arguments mapsnd_Batch {A B1 B2 C}%type_scope
f%function_scope b.
Classes.Kleisli.TraversableFunctor
Classes.Kleisli.Theory.TraversableFunctor
Classes.Categorical.ContainerFunctor
Classes.Categorical.ShapelyFunctor
Classes.Categorical.ApplicativeCommutativeIdempotent
Adapters.KleisliToCoalgebraic.TraversableFunctor
Functors.Batch
Functors.List
Functors.VectorRefinement.
Import Coalgebraic.TraversableFunctor (ToBatch, toBatch).
Import KleisliToCoalgebraic.TraversableFunctor.DerivedInstances.
Import Subset.Notations.
Import Applicative.Notations.
Import ContainerFunctor.Notations.
Import ProductFunctor.Notations.
Import Kleisli.TraversableFunctor.Notations.
Import Batch.Notations.
Import Monoid.Notations.
Import VectorRefinement.Notations.
#[local] Generalizable Variables F T G A B C M ϕ.
#[local] Arguments mapfst_Batch {B C A1 A2}%type_scope
f%function_scope b.
#[local] Arguments mapsnd_Batch {A B1 B2 C}%type_scope
f%function_scope b.
Section stuff.
Import Adapters.KleisliToCoalgebraic.TraversableFunctor.
Context
`{Kleisli.TraversableFunctor.TraversableFunctor T}
`{Map T}
`{ToBatch T}
`{! Compat_Map_Traverse T}
`{! Compat_ToBatch_Traverse T}.
Import Adapters.KleisliToCoalgebraic.TraversableFunctor.
Context
`{Kleisli.TraversableFunctor.TraversableFunctor T}
`{Map T}
`{ToBatch T}
`{! Compat_Map_Traverse T}
`{! Compat_ToBatch_Traverse T}.
Lemma Batch_contents_tolist:
∀ {A B} (t: T A),
proj1_sig (Batch_contents (toBatch (A' := B) t)) =
List.rev (tolist t).
Proof.
intros.
rewrite tolist_Batch_contents.
rewrite <- tolist_through_toBatch.
reflexivity.
Qed.
∀ {A B} (t: T A),
proj1_sig (Batch_contents (toBatch (A' := B) t)) =
List.rev (tolist t).
Proof.
intros.
rewrite tolist_Batch_contents.
rewrite <- tolist_through_toBatch.
reflexivity.
Qed.
Corollary shape_natural_toBatch {A A'}: ∀ (t: T A),
toBatch (A' := A') (shape t) =
shape (F := BATCH1 A' (T A')) (toBatch (A' := A') t).
Proof.
intros. unfold shape. compose near t.
now rewrite toBatch_mapfst.
Qed.
Corollary shape_toBatch_spec {A}: ∀ (t: T A),
shape t = runBatch (G := fun A ⇒ A) (const tt)
(toBatch (A' := unit) (T := T) t).
Proof.
intros.
unfold shape.
rewrite map_through_runBatch.
reflexivity.
Qed.
(* This statement holds without a A' universally quantified
inside the iff, but this is harder to prove. *)
Lemma toBatch_injective_univ {A}: ∀ (t u: T A),
(∀ (A': Type), toBatch (A' := A') t = toBatch u) ↔ t = u.
Proof.
intros. split.
- intro HBatch.
change (id t = id u).
rewrite id_through_runBatch.
unfold compose.
rewrite HBatch.
reflexivity.
- intro; now subst.
Qed.
toBatch (A' := A') (shape t) =
shape (F := BATCH1 A' (T A')) (toBatch (A' := A') t).
Proof.
intros. unfold shape. compose near t.
now rewrite toBatch_mapfst.
Qed.
Corollary shape_toBatch_spec {A}: ∀ (t: T A),
shape t = runBatch (G := fun A ⇒ A) (const tt)
(toBatch (A' := unit) (T := T) t).
Proof.
intros.
unfold shape.
rewrite map_through_runBatch.
reflexivity.
Qed.
(* This statement holds without a A' universally quantified
inside the iff, but this is harder to prove. *)
Lemma toBatch_injective_univ {A}: ∀ (t u: T A),
(∀ (A': Type), toBatch (A' := A') t = toBatch u) ↔ t = u.
Proof.
intros. split.
- intro HBatch.
change (id t = id u).
rewrite id_through_runBatch.
unfold compose.
rewrite HBatch.
reflexivity.
- intro; now subst.
Qed.
Lemma Batch_contents_toBatch_sim:
∀ {A B B': Type} (t: T A),
Batch_contents (toBatch (A' := B) t)
~~ Batch_contents (toBatch (A' := B') t).
Proof.
intros.
unfold Vector_sim.
rewrite Batch_contents_tolist.
rewrite Batch_contents_tolist.
reflexivity.
Qed.
∀ {A B B': Type} (t: T A),
Batch_contents (toBatch (A' := B) t)
~~ Batch_contents (toBatch (A' := B') t).
Proof.
intros.
unfold Vector_sim.
rewrite Batch_contents_tolist.
rewrite Batch_contents_tolist.
reflexivity.
Qed.
Lemma same_shape_toBatch:
∀ {A' B} `(t1: T A) (t2: T A'),
shape t1 = shape t2 →
shape (F := BATCH1 B (T B))
(toBatch (A' := B) t1) =
shape (F := BATCH1 B (T B))
(toBatch (A' := B) t2).
Proof.
introv Hshape.
rewrite <- shape_natural_toBatch.
rewrite <- shape_natural_toBatch.
rewrite Hshape.
reflexivity.
Qed.
∀ {A' B} `(t1: T A) (t2: T A'),
shape t1 = shape t2 →
shape (F := BATCH1 B (T B))
(toBatch (A' := B) t1) =
shape (F := BATCH1 B (T B))
(toBatch (A' := B) t2).
Proof.
introv Hshape.
rewrite <- shape_natural_toBatch.
rewrite <- shape_natural_toBatch.
rewrite Hshape.
reflexivity.
Qed.
Lemma same_tolist_toBatch:
∀ {B1 B2: Type} `(t1: T A) (t2: T A),
tolist t1 = tolist t2 →
tolist (toBatch (A' := B1) t1) =
tolist (toBatch (A' := B2) t2).
Proof.
introv Hshape.
rewrite (tolist_through_toBatch B1) in Hshape.
rewrite (tolist_through_toBatch (T := T) B2) in Hshape.
assumption.
Qed.
∀ {B1 B2: Type} `(t1: T A) (t2: T A),
tolist t1 = tolist t2 →
tolist (toBatch (A' := B1) t1) =
tolist (toBatch (A' := B2) t2).
Proof.
introv Hshape.
rewrite (tolist_through_toBatch B1) in Hshape.
rewrite (tolist_through_toBatch (T := T) B2) in Hshape.
assumption.
Qed.
Lemma toBatch_injective_tolist:
∀ {A B} `(t1: T A) (t2: T A),
(toBatch (A' := B) t1) =
(toBatch (A' := B) t2) →
tolist t1 = tolist t2.
Proof.
introv Heq.
rewrite (tolist_through_toBatch B).
rewrite (tolist_through_toBatch (T := T) B).
rewrite Heq.
reflexivity.
Qed.
∀ {A B} `(t1: T A) (t2: T A),
(toBatch (A' := B) t1) =
(toBatch (A' := B) t2) →
tolist t1 = tolist t2.
Proof.
introv Heq.
rewrite (tolist_through_toBatch B).
rewrite (tolist_through_toBatch (T := T) B).
rewrite Heq.
reflexivity.
Qed.
Lemma toBatch_shape_inv:
∀ {A' B} `(t1: T A) (t2: T A'),
shape (F := BATCH1 B (T B))
(toBatch (A' := B) t1) =
shape (F := BATCH1 B (T B))
(toBatch (A' := B) t2) →
shape t1 = shape t2.
Proof.
introv.
intro HBatch.
rewrite <- shape_natural_toBatch in HBatch.
rewrite <- shape_natural_toBatch in HBatch.
unfold shape.
Abort.
Lemma toBatch_injective_shape:
∀ {A B} `(t1: T A) (t2: T A),
(toBatch (A' := B) t1) =
(toBatch (A' := B) t2) →
shape t1 = shape t2.
Proof.
introv Heq.
unfold shape at 1 2.
Abort.
Lemma toBatch_injective_tolist2:
∀ {A B} `(t1: T A) (t2: T A),
(toBatch (A' := B) t1) =
(toBatch (A' := B) t2) ↔
tolist t1 = tolist t2.
Proof.
intros. split.
- apply toBatch_injective_tolist.
- rewrite (tolist_through_toBatch B).
rewrite (tolist_through_toBatch (T := T) B).
Abort.
Lemma toBatch_injective:
∀ {A B} `(t1: T A) (t2: T A),
(toBatch (A' := B) t1) =
(toBatch (A' := B) t2) →
t1 = t2.
Proof.
introv Heq.
change (id t1 = id t2).
rewrite id_through_runBatch.
unfold compose.
Abort.
End stuff.
∀ {A' B} `(t1: T A) (t2: T A'),
shape (F := BATCH1 B (T B))
(toBatch (A' := B) t1) =
shape (F := BATCH1 B (T B))
(toBatch (A' := B) t2) →
shape t1 = shape t2.
Proof.
introv.
intro HBatch.
rewrite <- shape_natural_toBatch in HBatch.
rewrite <- shape_natural_toBatch in HBatch.
unfold shape.
Abort.
Lemma toBatch_injective_shape:
∀ {A B} `(t1: T A) (t2: T A),
(toBatch (A' := B) t1) =
(toBatch (A' := B) t2) →
shape t1 = shape t2.
Proof.
introv Heq.
unfold shape at 1 2.
Abort.
Lemma toBatch_injective_tolist2:
∀ {A B} `(t1: T A) (t2: T A),
(toBatch (A' := B) t1) =
(toBatch (A' := B) t2) ↔
tolist t1 = tolist t2.
Proof.
intros. split.
- apply toBatch_injective_tolist.
- rewrite (tolist_through_toBatch B).
rewrite (tolist_through_toBatch (T := T) B).
Abort.
Lemma toBatch_injective:
∀ {A B} `(t1: T A) (t2: T A),
(toBatch (A' := B) t1) =
(toBatch (A' := B) t2) →
t1 = t2.
Proof.
introv Heq.
change (id t1 = id t2).
rewrite id_through_runBatch.
unfold compose.
Abort.
End stuff.
Lemma length_Batch_independent
`{TraversableFunctor T}
`{ToBatch T}
`{Map T}
`{! Compat_Map_Traverse T}
`{! Compat_ToBatch_Traverse T}
: ∀ `(t: T A) B C,
length_Batch (toBatch (A' := B) t) =
length_Batch (toBatch (A' := C) t).
Proof.
Abort.
`{TraversableFunctor T}
`{ToBatch T}
`{Map T}
`{! Compat_Map_Traverse T}
`{! Compat_ToBatch_Traverse T}
: ∀ `(t: T A) B C,
length_Batch (toBatch (A' := B) t) =
length_Batch (toBatch (A' := C) t).
Proof.
Abort.
Section shapeliness.
Context
`{TraversableFunctor T}
`{Map T}
`{ToBatch T}
`{! Compat_Map_Traverse T}
`{! Compat_ToBatch_Traverse T}
`{! ToSubset T} `{! Functor T}
`{! Compat_ToSubset_Traverse T}.
Theorem Traversable_shapeliness: ∀ A (t1 t2: T A),
shape t1 = shape t2 ∧ tolist t1 = tolist t2 →
t1 = t2.
Proof.
introv [hyp1 hyp2].
change (id t1 = id t2).
rewrite id_through_runBatch.
unfold compose.
enough (cut: toBatch (A' := A) t1 = toBatch t2)
by now rewrite cut.
specialize (same_shape_toBatch (B := A) t1 t2 hyp1).
specialize (same_tolist_toBatch (B1 := A) (B2 := A) t1 t2 hyp2).
intros. apply Batch_shapeliness; assumption.
Qed.
Lemma map_tolist_equal_iff: ∀ `(f1: A → B) `(f2: A → B) (t: T A),
map f1 (tolist t) = map f2 (tolist t) ↔
(∀ a: A, a ∈ t → f1 a = f2 a).
Proof.
intros.
setoid_rewrite in_iff_in_tolist.
induction (tolist t).
- cbn. tauto.
- cbn. split.
+ introv Hyp.
inversion Hyp.
intros a' [Case1 | Case2].
× subst. assumption.
× apply IHl.
assumption.
assumption.
+ intros X.
assert (cut: f1 a = f2 a).
{ apply X. now left. }
{ rewrite cut.
fequal. apply IHl.
firstorder. }
Qed.
Lemma map_equal_iff `{! Functor T}: ∀ `(f1: A → B) `(f2: A → B) (t: T A),
map f1 t = map f2 t ↔ map f1 (tolist t) = map f2 (tolist t).
Proof.
intros.
compose near t on right. split.
- introv Hmapeq.
rewrite (natural (ϕ := @tolist T _)).
rewrite (natural (ϕ := @tolist T _)).
unfold compose.
rewrite Hmapeq.
reflexivity.
- introv Hyp.
specialize (Traversable_shapeliness _ (map f1 t) (map f2 t)).
intros X. apply X. split.
+ rewrite shape_map.
rewrite shape_map.
reflexivity.
+ compose near t.
rewrite <- (natural (ϕ := @tolist T _)).
rewrite <- (natural (ϕ := @tolist T _)).
assumption.
Qed.
Lemma map_respectful_iff `{! Functor T}: ∀ `(f1: A → B) `(f2: A → B) (t: T A),
(∀ a: A, a ∈ t → f1 a = f2 a) ↔ map f1 t = map f2 t.
Proof.
intros.
rewrite map_equal_iff.
rewrite map_tolist_equal_iff.
tauto.
Qed.
End shapeliness.
Context
`{TraversableFunctor T}
`{Map T}
`{ToBatch T}
`{! Compat_Map_Traverse T}
`{! Compat_ToBatch_Traverse T}
`{! ToSubset T} `{! Functor T}
`{! Compat_ToSubset_Traverse T}.
Theorem Traversable_shapeliness: ∀ A (t1 t2: T A),
shape t1 = shape t2 ∧ tolist t1 = tolist t2 →
t1 = t2.
Proof.
introv [hyp1 hyp2].
change (id t1 = id t2).
rewrite id_through_runBatch.
unfold compose.
enough (cut: toBatch (A' := A) t1 = toBatch t2)
by now rewrite cut.
specialize (same_shape_toBatch (B := A) t1 t2 hyp1).
specialize (same_tolist_toBatch (B1 := A) (B2 := A) t1 t2 hyp2).
intros. apply Batch_shapeliness; assumption.
Qed.
Lemma map_tolist_equal_iff: ∀ `(f1: A → B) `(f2: A → B) (t: T A),
map f1 (tolist t) = map f2 (tolist t) ↔
(∀ a: A, a ∈ t → f1 a = f2 a).
Proof.
intros.
setoid_rewrite in_iff_in_tolist.
induction (tolist t).
- cbn. tauto.
- cbn. split.
+ introv Hyp.
inversion Hyp.
intros a' [Case1 | Case2].
× subst. assumption.
× apply IHl.
assumption.
assumption.
+ intros X.
assert (cut: f1 a = f2 a).
{ apply X. now left. }
{ rewrite cut.
fequal. apply IHl.
firstorder. }
Qed.
Lemma map_equal_iff `{! Functor T}: ∀ `(f1: A → B) `(f2: A → B) (t: T A),
map f1 t = map f2 t ↔ map f1 (tolist t) = map f2 (tolist t).
Proof.
intros.
compose near t on right. split.
- introv Hmapeq.
rewrite (natural (ϕ := @tolist T _)).
rewrite (natural (ϕ := @tolist T _)).
unfold compose.
rewrite Hmapeq.
reflexivity.
- introv Hyp.
specialize (Traversable_shapeliness _ (map f1 t) (map f2 t)).
intros X. apply X. split.
+ rewrite shape_map.
rewrite shape_map.
reflexivity.
+ compose near t.
rewrite <- (natural (ϕ := @tolist T _)).
rewrite <- (natural (ϕ := @tolist T _)).
assumption.
Qed.
Lemma map_respectful_iff `{! Functor T}: ∀ `(f1: A → B) `(f2: A → B) (t: T A),
(∀ a: A, a ∈ t → f1 a = f2 a) ↔ map f1 t = map f2 t.
Proof.
intros.
rewrite map_equal_iff.
rewrite map_tolist_equal_iff.
tauto.
Qed.
End shapeliness.
Section pointwise.
Context
`{Classes.Kleisli.TraversableFunctor.TraversableFunctor T}
`{ToMap_inst: Map T}
`{ToSubset_inst: ToSubset T}
`{ToBatch_inst: ToBatch T}
`{! Compat_Map_Traverse T}
`{! Compat_ToSubset_Traverse T}
`{! Compat_ToBatch_Traverse T}.
Lemma traverse_respectful:
∀ `{Applicative G} `(f1: A → G B) `(f2: A → G B) (t: T A),
(∀ (a: A), a ∈ t → f1 a = f2 a) → traverse f1 t = traverse f2 t.
Proof.
introv ? hyp.
do 2 rewrite traverse_through_runBatch.
unfold element_of in hyp.
rewrite (tosubset_through_runBatch2 A B) in hyp.
unfold compose in ×.
unfold ret in ×.
induction (toBatch t).
- reflexivity.
- cbn. fequal.
+ apply IHb. intros.
apply hyp. now left.
+ apply hyp. now right.
Qed.
Context
`{Classes.Kleisli.TraversableFunctor.TraversableFunctor T}
`{ToMap_inst: Map T}
`{ToSubset_inst: ToSubset T}
`{ToBatch_inst: ToBatch T}
`{! Compat_Map_Traverse T}
`{! Compat_ToSubset_Traverse T}
`{! Compat_ToBatch_Traverse T}.
Lemma traverse_respectful:
∀ `{Applicative G} `(f1: A → G B) `(f2: A → G B) (t: T A),
(∀ (a: A), a ∈ t → f1 a = f2 a) → traverse f1 t = traverse f2 t.
Proof.
introv ? hyp.
do 2 rewrite traverse_through_runBatch.
unfold element_of in hyp.
rewrite (tosubset_through_runBatch2 A B) in hyp.
unfold compose in ×.
unfold ret in ×.
induction (toBatch t).
- reflexivity.
- cbn. fequal.
+ apply IHb. intros.
apply hyp. now left.
+ apply hyp. now right.
Qed.
Corollary traverse_respectful_pure:
∀ `{Applicative G} `(f1: A → G A) (t: T A),
(∀ (a: A), a ∈ t → f1 a = pure a) → traverse f1 t = pure t.
Proof.
intros.
rewrite <- traverse_purity1.
now apply traverse_respectful.
Qed.
Corollary traverse_respectful_map {A B}:
∀ `{Applicative G} (t: T A) (f: A → G B) (g: A → B),
(∀ a, a ∈ t → f a = pure (g a)) → traverse f t = pure (map g t).
Proof.
intros. rewrite <- (traverse_purity1 (G := G)).
compose near t on right.
rewrite traverse_map.
apply traverse_respectful.
assumption.
Qed.
Corollary traverse_respectful_id {A}:
∀ (t: T A) (f: A → A),
(∀ a, a ∈ t → f a = id a) → traverse (G := fun A ⇒ A) f t = t.
Proof.
intros.
change t with (pure (F := fun A ⇒ A) t) at 2.
apply (traverse_respectful_pure (G := fun A ⇒ A)).
assumption.
Qed.
Corollary map_respectful: ∀ `(f1: A → B) `(f2: A → B) (t: T A),
(∀ (a: A), a ∈ t → f1 a = f2 a) → map f1 t = map f2 t.
Proof.
introv hyp.
rewrite map_to_traverse.
rewrite map_to_traverse.
apply (traverse_respectful (G := fun A ⇒ A)).
assumption.
Qed.
∀ `{Applicative G} `(f1: A → G A) (t: T A),
(∀ (a: A), a ∈ t → f1 a = pure a) → traverse f1 t = pure t.
Proof.
intros.
rewrite <- traverse_purity1.
now apply traverse_respectful.
Qed.
Corollary traverse_respectful_map {A B}:
∀ `{Applicative G} (t: T A) (f: A → G B) (g: A → B),
(∀ a, a ∈ t → f a = pure (g a)) → traverse f t = pure (map g t).
Proof.
intros. rewrite <- (traverse_purity1 (G := G)).
compose near t on right.
rewrite traverse_map.
apply traverse_respectful.
assumption.
Qed.
Corollary traverse_respectful_id {A}:
∀ (t: T A) (f: A → A),
(∀ a, a ∈ t → f a = id a) → traverse (G := fun A ⇒ A) f t = t.
Proof.
intros.
change t with (pure (F := fun A ⇒ A) t) at 2.
apply (traverse_respectful_pure (G := fun A ⇒ A)).
assumption.
Qed.
Corollary map_respectful: ∀ `(f1: A → B) `(f2: A → B) (t: T A),
(∀ (a: A), a ∈ t → f1 a = f2 a) → map f1 t = map f2 t.
Proof.
introv hyp.
rewrite map_to_traverse.
rewrite map_to_traverse.
apply (traverse_respectful (G := fun A ⇒ A)).
assumption.
Qed.
#[export] Instance ContainerFunctor_Traverse:
ContainerFunctor T.
Proof.
constructor.
- rewrite compat_tosubset_traverse.
typeclasses eauto.
- apply DerivedInstances.Functor_TraversableFunctor.
- intros. now apply map_respectful.
Qed.
#[export] Instance ShapelyFunctor_Traverse:
ShapelyFunctor T.
Proof.
constructor.
- typeclasses eauto.
- typeclasses eauto.
- unfold shapeliness.
apply Traversable_shapeliness.
Qed.
End pointwise.
ContainerFunctor T.
Proof.
constructor.
- rewrite compat_tosubset_traverse.
typeclasses eauto.
- apply DerivedInstances.Functor_TraversableFunctor.
- intros. now apply map_respectful.
Qed.
#[export] Instance ShapelyFunctor_Traverse:
ShapelyFunctor T.
Proof.
constructor.
- typeclasses eauto.
- typeclasses eauto.
- unfold shapeliness.
apply Traversable_shapeliness.
Qed.
End pointwise.
Section length.
Context
`{Map T}
`{ToBatch T}
`{Traverse T}
`{! TraversableFunctor T}
`{! Compat_Map_Traverse T}
`{! Compat_ToBatch_Traverse T}.
Lemma plength_eq_length:
∀ {A} {B} (t: T A),
length_Batch (toBatch (A' := B) t) = plength t.
Proof.
intros.
unfold plength.
rewrite (mapReduce_through_runBatch2 A B).
unfold compose.
induction (toBatch t).
- reflexivity.
- cbn.
rewrite IHb.
unfold_ops @NaturalNumbers.Monoid_op_plus.
lia.
Qed.
Lemma plength_eq_length': ∀ {A} (t: T A),
plength t = length_Batch (toBatch (A' := False) t).
Proof.
intros.
symmetry.
apply plength_eq_length.
Qed.
End length.
Context
`{Map T}
`{ToBatch T}
`{Traverse T}
`{! TraversableFunctor T}
`{! Compat_Map_Traverse T}
`{! Compat_ToBatch_Traverse T}.
Lemma plength_eq_length:
∀ {A} {B} (t: T A),
length_Batch (toBatch (A' := B) t) = plength t.
Proof.
intros.
unfold plength.
rewrite (mapReduce_through_runBatch2 A B).
unfold compose.
induction (toBatch t).
- reflexivity.
- cbn.
rewrite IHb.
unfold_ops @NaturalNumbers.Monoid_op_plus.
lia.
Qed.
Lemma plength_eq_length': ∀ {A} (t: T A),
plength t = length_Batch (toBatch (A' := False) t).
Proof.
intros.
symmetry.
apply plength_eq_length.
Qed.
End length.
Section deconstruction.
Definition trav_contents
{T: Type → Type} {toBatch_T: ToBatch T} {traverse_T: Traverse T} {map_T: Map T}
{cmt: Compat_Map_Traverse T}
{cbt: Compat_ToBatch_Traverse T}
{Trav_T: TraversableFunctor T}
{A} (t: T A): Vector (plength t) A :=
let v: Vector
(length_Batch (toBatch (ToBatch := toBatch_T) (A' := False) t)) A
:= Batch_contents (toBatch t)
in coerce_Vector_length (plength_eq_length t) v.
Definition trav_make
{T: Type → Type}
{map_T: Map T}
{traverse_T: Traverse T}
{toBatch_T: ToBatch T}
{cmt: Compat_Map_Traverse T}
{cmt: Compat_ToBatch_Traverse T}
{Trav_T: TraversableFunctor T}
{A B: Type} (t: T A):
Vector (plength t) B → T B :=
(fun v ⇒
let v' := coerce_Vector_length (eq_sym (plength_eq_length t)) v
in Batch_make (toBatch t) v').
Context
`{Traverse T}
`{Map T}
`{ToBatch T}
`{! TraversableFunctor T}
`{! Compat_Map_Traverse T}
`{! Compat_ToBatch_Traverse T}.
#[local] Generalizable Variables v.
Definition trav_contents
{T: Type → Type} {toBatch_T: ToBatch T} {traverse_T: Traverse T} {map_T: Map T}
{cmt: Compat_Map_Traverse T}
{cbt: Compat_ToBatch_Traverse T}
{Trav_T: TraversableFunctor T}
{A} (t: T A): Vector (plength t) A :=
let v: Vector
(length_Batch (toBatch (ToBatch := toBatch_T) (A' := False) t)) A
:= Batch_contents (toBatch t)
in coerce_Vector_length (plength_eq_length t) v.
Definition trav_make
{T: Type → Type}
{map_T: Map T}
{traverse_T: Traverse T}
{toBatch_T: ToBatch T}
{cmt: Compat_Map_Traverse T}
{cmt: Compat_ToBatch_Traverse T}
{Trav_T: TraversableFunctor T}
{A B: Type} (t: T A):
Vector (plength t) B → T B :=
(fun v ⇒
let v' := coerce_Vector_length (eq_sym (plength_eq_length t)) v
in Batch_make (toBatch t) v').
Context
`{Traverse T}
`{Map T}
`{ToBatch T}
`{! TraversableFunctor T}
`{! Compat_Map_Traverse T}
`{! Compat_ToBatch_Traverse T}.
#[local] Generalizable Variables v.
Section traverse_vector.
Lemma trav_contents_Vector {n: nat} {A: Type}:
∀ (v: Vector n A),
trav_contents v ~~ reverse_Vector v.
Proof.
intros.
unfold Vector_sim.
unfold trav_contents.
rewrite <- coerce_Vector_contents.
induction v using Vector_induction.
- reflexivity.
- rewrite toBatch_to_traverse.
rewrite traverse_Vector_vcons.
rewrite Batch_contents_rw_app.
rewrite proj_Vector_append.
rewrite Batch_contents_rw_app.
rewrite proj_Vector_append.
rewrite Batch_contents_rw_pure.
rewrite proj_reverse_Vector.
rewrite proj_vcons.
cbn.
rewrite <- proj_reverse_Vector.
rewrite <- IHv.
reflexivity.
Qed.
Lemma trav_make_Vector {n: nat} {A B: Type}:
∀ (v1: Vector n A) (v2: Vector (plength v1) B),
(trav_make (B := B) v1 v2) ~~ v2.
Proof.
intros.
induction v1 using Vector_induction.
- assert (Hey: v2 = vnil).
{ apply Vector_nil_eq. }
rewrite Hey.
reflexivity.
- cbn in v2.
unfold trav_make.
pose (toBatch_to_traverse (T := Vector (S m)) A B).
Abort.
End traverse_vector.
Lemma trav_contents_Vector {n: nat} {A: Type}:
∀ (v: Vector n A),
trav_contents v ~~ reverse_Vector v.
Proof.
intros.
unfold Vector_sim.
unfold trav_contents.
rewrite <- coerce_Vector_contents.
induction v using Vector_induction.
- reflexivity.
- rewrite toBatch_to_traverse.
rewrite traverse_Vector_vcons.
rewrite Batch_contents_rw_app.
rewrite proj_Vector_append.
rewrite Batch_contents_rw_app.
rewrite proj_Vector_append.
rewrite Batch_contents_rw_pure.
rewrite proj_reverse_Vector.
rewrite proj_vcons.
cbn.
rewrite <- proj_reverse_Vector.
rewrite <- IHv.
reflexivity.
Qed.
Lemma trav_make_Vector {n: nat} {A B: Type}:
∀ (v1: Vector n A) (v2: Vector (plength v1) B),
(trav_make (B := B) v1 v2) ~~ v2.
Proof.
intros.
induction v1 using Vector_induction.
- assert (Hey: v2 = vnil).
{ apply Vector_nil_eq. }
rewrite Hey.
reflexivity.
- cbn in v2.
unfold trav_make.
pose (toBatch_to_traverse (T := Vector (S m)) A B).
Abort.
End traverse_vector.
Section trav_make_lemmas.
Context
{A B: Type}.
Lemma trav_make_sim_refl:
∀ (t: T A), trav_make (B := B) t ~!~ trav_make t.
Proof.
intros.
unfold trav_make.
unfold Vector_fun_sim. split.
- reflexivity.
- intros.
apply Batch_make_sim1.
apply Vector_coerce_sim_l'.
apply Vector_coerce_sim_r'.
assumption.
Qed.
Lemma toBatch_trav_make_to_replace_contents
{A'} {t: T A} {v: Vector (plength t) B}:
toBatch (A' := A') (trav_make t v) =
Batch_replace_contents (toBatch (A' := A') t)
(coerce eq_sym (plength_eq_length t) in v).
Proof.
unfold trav_make.
rewrite Batch_make_natural_rw1.
rewrite Batch_replace_contents_spec.
apply Batch_make_sim2.
- compose near t.
rewrite (TraversableFunctor.trf_duplicate (T := T)).
rewrite compat_toBatch_traverse.
reflexivity.
- vector_sim.
Qed.
Context
{A B: Type}.
Lemma trav_make_sim_refl:
∀ (t: T A), trav_make (B := B) t ~!~ trav_make t.
Proof.
intros.
unfold trav_make.
unfold Vector_fun_sim. split.
- reflexivity.
- intros.
apply Batch_make_sim1.
apply Vector_coerce_sim_l'.
apply Vector_coerce_sim_r'.
assumption.
Qed.
Lemma toBatch_trav_make_to_replace_contents
{A'} {t: T A} {v: Vector (plength t) B}:
toBatch (A' := A') (trav_make t v) =
Batch_replace_contents (toBatch (A' := A') t)
(coerce eq_sym (plength_eq_length t) in v).
Proof.
unfold trav_make.
rewrite Batch_make_natural_rw1.
rewrite Batch_replace_contents_spec.
apply Batch_make_sim2.
- compose near t.
rewrite (TraversableFunctor.trf_duplicate (T := T)).
rewrite compat_toBatch_traverse.
reflexivity.
- vector_sim.
Qed.
Lemma trav_contents_natural:
∀ (A B: Type) (t: T A) (f: A → B),
trav_contents (map f t) ~~ map f (trav_contents t).
Proof.
intros.
unfold Vector_sim.
unfold trav_contents.
rewrite <- coerce_Vector_contents.
rewrite <- map_coerce_Vector.
compose near t on left.
rewrite toBatch_mapfst.
unfold compose at 2.
rewrite Batch_contents_natural.
reflexivity.
Qed.
Lemma trav_make_natural:
∀ (A B C: Type) (t: T A) (f: B → C) (v: Vector (plength t) B),
trav_make t (map f v) = map f (trav_make t v).
Proof.
intros.
unfold trav_make.
rewrite (Batch_make_natural_rw1 (toBatch t) (map f)).
assert (cut: map (map f) (toBatch t) =
mapsnd_Batch f (toBatch t)).
{ compose near t.
now rewrite (toBatch_mapsnd). }
rewrite (Batch_make_rw
(map (map f) (toBatch t))
(mapsnd_Batch f (toBatch t))
cut).
rewrite coerce_Vector_compose.
rewrite coerce_Vector_compose.
rewrite Batch_make_natural2.
apply Batch_make_sim1.
apply Vector_coerce_sim_r'.
apply Vector_coerce_sim_l'.
apply map_coerce_Vector.
Qed.
End trav_make_lemmas.
∀ (A B: Type) (t: T A) (f: A → B),
trav_contents (map f t) ~~ map f (trav_contents t).
Proof.
intros.
unfold Vector_sim.
unfold trav_contents.
rewrite <- coerce_Vector_contents.
rewrite <- map_coerce_Vector.
compose near t on left.
rewrite toBatch_mapfst.
unfold compose at 2.
rewrite Batch_contents_natural.
reflexivity.
Qed.
Lemma trav_make_natural:
∀ (A B C: Type) (t: T A) (f: B → C) (v: Vector (plength t) B),
trav_make t (map f v) = map f (trav_make t v).
Proof.
intros.
unfold trav_make.
rewrite (Batch_make_natural_rw1 (toBatch t) (map f)).
assert (cut: map (map f) (toBatch t) =
mapsnd_Batch f (toBatch t)).
{ compose near t.
now rewrite (toBatch_mapsnd). }
rewrite (Batch_make_rw
(map (map f) (toBatch t))
(mapsnd_Batch f (toBatch t))
cut).
rewrite coerce_Vector_compose.
rewrite coerce_Vector_compose.
rewrite Batch_make_natural2.
apply Batch_make_sim1.
apply Vector_coerce_sim_r'.
apply Vector_coerce_sim_l'.
apply map_coerce_Vector.
Qed.
End trav_make_lemmas.
Lemma tolist_trav_contents `{t: T A}:
Vector_to_list A (trav_contents t) = List.rev (tolist t).
Proof.
intros.
unfold Vector_to_list.
unfold trav_contents.
rewrite <- coerce_Vector_contents.
rewrite tolist_Batch_contents.
rewrite <- tolist_through_toBatch.
reflexivity.
Qed.
Vector_to_list A (trav_contents t) = List.rev (tolist t).
Proof.
intros.
unfold Vector_to_list.
unfold trav_contents.
rewrite <- coerce_Vector_contents.
rewrite tolist_Batch_contents.
rewrite <- tolist_through_toBatch.
reflexivity.
Qed.
Lemma trav_get_put `{t: T A}:
trav_make t (trav_contents t) = t.
Proof.
unfold trav_make, trav_contents.
rewrite coerce_Vector_compose.
hide_lhs;
change t with (id t);
rewrite <- TraversableFunctor.trf_extract;
rewrite Heqlhs; clear Heqlhs lhs;
unfold compose at 1.
rewrite <- Batch_make_contents.
apply Batch_make_sim1.
vector_sim.
apply Batch_contents_toBatch_sim.
Qed.
trav_make t (trav_contents t) = t.
Proof.
unfold trav_make, trav_contents.
rewrite coerce_Vector_compose.
hide_lhs;
change t with (id t);
rewrite <- TraversableFunctor.trf_extract;
rewrite Heqlhs; clear Heqlhs lhs;
unfold compose at 1.
rewrite <- Batch_make_contents.
apply Batch_make_sim1.
vector_sim.
apply Batch_contents_toBatch_sim.
Qed.
Lemma trav_contents_make {A B} {t: T A} {v: Vector (plength t) B}:
trav_contents (trav_make t v) ~~ v.
Proof.
unfold trav_contents.
vector_sim.
rewrite toBatch_trav_make_to_replace_contents.
rewrite Batch_put_get.
vector_sim.
Qed.
trav_contents (trav_make t v) ~~ v.
Proof.
unfold trav_contents.
vector_sim.
rewrite toBatch_trav_make_to_replace_contents.
rewrite Batch_put_get.
vector_sim.
Qed.
Lemma trav_make_make_
`(t: T A) `(v: Vector (plength t) B)
`(v1: Vector (plength (trav_make t v)) B')
(v2: Vector (plength t) B')
(pf: v1 ~~ v2):
trav_make (trav_make t v) v1 =
trav_make t v2.
Proof.
unfold trav_make at 1.
unfold trav_make at 7.
apply Batch_make_sim3.
- symmetry.
rewrite toBatch_trav_make_to_replace_contents.
apply Batch_shape_replace_contents.
- vector_sim.
Qed.
Lemma plength_trav_make: ∀ `(t: T A) `(v: Vector _ B),
plength t = plength (trav_make t v).
Proof.
intros.
unfold plength at 1 2.
do 2 change (fun (x:?X) ⇒ 1) with (const (A := X) 1).
do 2 rewrite (mapReduce_through_runBatch2 _ B).
unfold compose.
rewrite (@toBatch_trav_make_to_replace_contents A B B t v).
rewrite <- (runBatch_const_contents (G := @const Type Type nat)).
reflexivity.
Qed.
Lemma trav_make_make:
∀ `(t: T A) `(v: Vector (plength t) B) (C: Type),
trav_make (B := C) (trav_make t v) ~!~
trav_make t.
Proof.
intros.
unfold Vector_fun_sim. split.
- rewrite <- plength_trav_make.
reflexivity.
- intros.
now rewrite (trav_make_make_ t v v1 v2).
Qed.
`(t: T A) `(v: Vector (plength t) B)
`(v1: Vector (plength (trav_make t v)) B')
(v2: Vector (plength t) B')
(pf: v1 ~~ v2):
trav_make (trav_make t v) v1 =
trav_make t v2.
Proof.
unfold trav_make at 1.
unfold trav_make at 7.
apply Batch_make_sim3.
- symmetry.
rewrite toBatch_trav_make_to_replace_contents.
apply Batch_shape_replace_contents.
- vector_sim.
Qed.
Lemma plength_trav_make: ∀ `(t: T A) `(v: Vector _ B),
plength t = plength (trav_make t v).
Proof.
intros.
unfold plength at 1 2.
do 2 change (fun (x:?X) ⇒ 1) with (const (A := X) 1).
do 2 rewrite (mapReduce_through_runBatch2 _ B).
unfold compose.
rewrite (@toBatch_trav_make_to_replace_contents A B B t v).
rewrite <- (runBatch_const_contents (G := @const Type Type nat)).
reflexivity.
Qed.
Lemma trav_make_make:
∀ `(t: T A) `(v: Vector (plength t) B) (C: Type),
trav_make (B := C) (trav_make t v) ~!~
trav_make t.
Proof.
intros.
unfold Vector_fun_sim. split.
- rewrite <- plength_trav_make.
reflexivity.
- intros.
now rewrite (trav_make_make_ t v v1 v2).
Qed.
Lemma trav_same_shape {A1 A2: Type}
{t1: T A1} {t2: T A2}:
shape t1 = shape t2 →
∀ B, trav_make (B := B) t1 ~!~ trav_make t2.
Proof.
intros.
unfold trav_make.
apply Vector_coerce_fun_sim_l'.
apply Vector_coerce_fun_sim_r'.
apply Batch_make_shape.
apply same_shape_toBatch.
assumption.
Qed.
{t1: T A1} {t2: T A2}:
shape t1 = shape t2 →
∀ B, trav_make (B := B) t1 ~!~ trav_make t2.
Proof.
intros.
unfold trav_make.
apply Vector_coerce_fun_sim_l'.
apply Vector_coerce_fun_sim_r'.
apply Batch_make_shape.
apply same_shape_toBatch.
assumption.
Qed.
Section trav_make_lemmas.
Context
{A B: Type}.
Lemma trav_make_sim1:
∀ (t: T A) `{v1 ~~ v2},
trav_make (B := B) t v1 = trav_make t v2.
Proof.
intros.
unfold trav_make.
apply Batch_make_sim1.
vector_sim.
Qed.
Lemma trav_make_sim2:
∀ `(t1: T A) (t2: T A)
`(v1: Vector (plength t1) B)
`(v2: Vector (plength t2) B),
t1 = t2 →
Vector_sim v1 v2 →
trav_make t1 v1 = trav_make t2 v2.
Proof.
intros.
subst.
now apply trav_make_sim1.
Qed.
End trav_make_lemmas.
End lens_laws.
Context
{A B: Type}.
Lemma trav_make_sim1:
∀ (t: T A) `{v1 ~~ v2},
trav_make (B := B) t v1 = trav_make t v2.
Proof.
intros.
unfold trav_make.
apply Batch_make_sim1.
vector_sim.
Qed.
Lemma trav_make_sim2:
∀ `(t1: T A) (t2: T A)
`(v1: Vector (plength t1) B)
`(v2: Vector (plength t2) B),
t1 = t2 →
Vector_sim v1 v2 →
trav_make t1 v1 = trav_make t2 v2.
Proof.
intros.
subst.
now apply trav_make_sim1.
Qed.
End trav_make_lemmas.
End lens_laws.
Lemma traverse_repr:
∀ `{Applicative G} (A B: Type) (t: T A) (f: A → G B),
traverse f t =
map (trav_make t) (forwards (traverse (mkBackwards ∘ f) (trav_contents t))).
Proof.
intros.
rewrite traverse_through_runBatch.
unfold compose at 1.
rewrite runBatch_repr2.
unfold trav_make, trav_contents.
rewrite (traverse_Vector_coerce _ _ _ (plength_eq_length t)).
change_left (
map (Batch_make (toBatch t))
(map
(fun v: Vector (plength t) B ⇒
coerce eq_sym (plength_eq_length (B := B) t) in v)
(forwards
(traverse (mkBackwards ∘ f)
(coerce (plength_eq_length (B := B) t) in
Batch_contents (toBatch t)))))).
compose near ((forwards
(traverse (mkBackwards ∘ f)
(coerce (plength_eq_length (B := B) t)
in Batch_contents (toBatch t))))).
rewrite (fun_map_map).
fequal.
fequal.
fequal.
apply Vector_eq.
apply Vector_coerce_sim_l'.
apply Vector_coerce_sim_r'.
eapply Batch_contents_toBatch_sim.
Qed.
∀ `{Applicative G} (A B: Type) (t: T A) (f: A → G B),
traverse f t =
map (trav_make t) (forwards (traverse (mkBackwards ∘ f) (trav_contents t))).
Proof.
intros.
rewrite traverse_through_runBatch.
unfold compose at 1.
rewrite runBatch_repr2.
unfold trav_make, trav_contents.
rewrite (traverse_Vector_coerce _ _ _ (plength_eq_length t)).
change_left (
map (Batch_make (toBatch t))
(map
(fun v: Vector (plength t) B ⇒
coerce eq_sym (plength_eq_length (B := B) t) in v)
(forwards
(traverse (mkBackwards ∘ f)
(coerce (plength_eq_length (B := B) t) in
Batch_contents (toBatch t)))))).
compose near ((forwards
(traverse (mkBackwards ∘ f)
(coerce (plength_eq_length (B := B) t)
in Batch_contents (toBatch t))))).
rewrite (fun_map_map).
fequal.
fequal.
fequal.
apply Vector_eq.
apply Vector_coerce_sim_l'.
apply Vector_coerce_sim_r'.
eapply Batch_contents_toBatch_sim.
Qed.
Corollary traverse_trav_make:
∀ `{Applicative G} (X A B: Type)
(t: T X) (f: A → G B) (v: Vector (plength t) A),
traverse (T := T) f (trav_make t v) =
map (trav_make t) (forwards (traverse (mkBackwards ∘ f) v)).
Proof.
intros.
rewrite traverse_repr.
assert (Hlen: plength (trav_make t v) = plength t).
{ now rewrite <- plength_trav_make. }
rewrite (map_sim_function B (T B) _ _ (trav_make (trav_make t v))
(trav_make t (B := B)) Hlen).
2: { apply trav_make_make. }
change (?f ○ ?pre) with (f ∘ pre).
rewrite <- (fun_map_map).
unfold compose at 1.
fequal.
compose near (traverse (mkBackwards ∘ f) (trav_contents (trav_make t v))).
rewrite (natural (Natural := Natural_forwards)).
unfold compose.
fequal.
apply map_sim_function_traverse_Vector.
apply trav_contents_make.
Qed.
Lemma mapReduce_opposite_traverse {A}:
∀ `{Monoid M} `{TraversableFunctor T'}
`{ToBatch T'} `{! Compat_ToBatch_Traverse T'} (t: T' A) (f: A → M),
mapReduce (op := Monoid_op_Opposite op) f t =
forwards (traverse (B := False) (T := T') (G := Backwards (const M)) (mkBackwards ∘ f) t).
Proof.
intros.
rewrite mapReduce_to_traverse1.
rewrite traverse_through_runBatch.
rewrite traverse_through_runBatch.
unfold compose.
induction (@toBatch T' _ A False t).
- reflexivity.
- rewrite runBatch_rw2.
rewrite IHb.
rewrite runBatch_rw2.
reflexivity.
Qed.
Corollary mapReduce_trav_make:
∀ `{Monoid M} (X A: Type)
(t: T X) (f: A → M) (v: Vector (plength t) A),
mapReduce (T := T) f (trav_make t v) =
mapReduce (op := Monoid_op_Opposite op) f v.
Proof.
intros.
unfold mapReduce.
rewrite traverse_trav_make.
unfold_ops @Map_const.
setoid_rewrite <- (mapReduce_opposite_traverse (T' := Vector (plength t))).
reflexivity.
Qed.
∀ `{Applicative G} (X A B: Type)
(t: T X) (f: A → G B) (v: Vector (plength t) A),
traverse (T := T) f (trav_make t v) =
map (trav_make t) (forwards (traverse (mkBackwards ∘ f) v)).
Proof.
intros.
rewrite traverse_repr.
assert (Hlen: plength (trav_make t v) = plength t).
{ now rewrite <- plength_trav_make. }
rewrite (map_sim_function B (T B) _ _ (trav_make (trav_make t v))
(trav_make t (B := B)) Hlen).
2: { apply trav_make_make. }
change (?f ○ ?pre) with (f ∘ pre).
rewrite <- (fun_map_map).
unfold compose at 1.
fequal.
compose near (traverse (mkBackwards ∘ f) (trav_contents (trav_make t v))).
rewrite (natural (Natural := Natural_forwards)).
unfold compose.
fequal.
apply map_sim_function_traverse_Vector.
apply trav_contents_make.
Qed.
Lemma mapReduce_opposite_traverse {A}:
∀ `{Monoid M} `{TraversableFunctor T'}
`{ToBatch T'} `{! Compat_ToBatch_Traverse T'} (t: T' A) (f: A → M),
mapReduce (op := Monoid_op_Opposite op) f t =
forwards (traverse (B := False) (T := T') (G := Backwards (const M)) (mkBackwards ∘ f) t).
Proof.
intros.
rewrite mapReduce_to_traverse1.
rewrite traverse_through_runBatch.
rewrite traverse_through_runBatch.
unfold compose.
induction (@toBatch T' _ A False t).
- reflexivity.
- rewrite runBatch_rw2.
rewrite IHb.
rewrite runBatch_rw2.
reflexivity.
Qed.
Corollary mapReduce_trav_make:
∀ `{Monoid M} (X A: Type)
(t: T X) (f: A → M) (v: Vector (plength t) A),
mapReduce (T := T) f (trav_make t v) =
mapReduce (op := Monoid_op_Opposite op) f v.
Proof.
intros.
unfold mapReduce.
rewrite traverse_trav_make.
unfold_ops @Map_const.
setoid_rewrite <- (mapReduce_opposite_traverse (T' := Vector (plength t))).
reflexivity.
Qed.
Lemma id_spec:
∀ (A: Type) (t: T A),
id t = trav_make t (trav_contents t).
Proof.
intros.
rewrite trav_get_put.
reflexivity.
Qed.
Lemma map_spec:
∀ (A B: Type) (t: T A) (f: A → B),
map f t = trav_make t (map f (trav_contents t)).
Proof.
intros A B t f.
rewrite <- trav_get_put at 1.
apply Vector_fun_sim_eq.
- apply trav_same_shape.
rewrite shape_map.
reflexivity.
- apply trav_contents_natural.
Qed.
∀ (A: Type) (t: T A),
id t = trav_make t (trav_contents t).
Proof.
intros.
rewrite trav_get_put.
reflexivity.
Qed.
Lemma map_spec:
∀ (A B: Type) (t: T A) (f: A → B),
map f t = trav_make t (map f (trav_contents t)).
Proof.
intros A B t f.
rewrite <- trav_get_put at 1.
apply Vector_fun_sim_eq.
- apply trav_same_shape.
rewrite shape_map.
reflexivity.
- apply trav_contents_natural.
Qed.
Lemma trav_contents_shape:
∀ (A: Type) (t: T A),
trav_contents (shape t) ~~ Vector_tt (plength t).
Proof.
intros.
(* LHS *)
unfold trav_contents.
apply Vector_coerce_sim_l'.
unfold shape.
replace (toBatch (A' := False) (map (const tt) t))
with (mapfst_Batch (B := False) (const tt) (toBatch t)).
2:{ compose near t.
now rewrite toBatch_mapfst. }
unfold Vector_tt.
unfold plength.
rewrite mapReduce_through_runBatch1.
unfold compose.
induction (toBatch t).
- reflexivity.
- cbn.
unfold_ops @NaturalNumbers.Monoid_op_plus.
rewrite PeanoNat.Nat.add_1_r.
cbn.
apply vcons_sim.
assumption.
Qed.
Lemma shape_spec:
∀ (A: Type) (t: T A),
shape t = trav_make (B := unit) t (Vector_tt (plength t)).
Proof.
intros A t.
unfold shape.
rewrite map_spec.
fequal.
apply Vector_sim_eq.
unfold Vector_sim.
rewrite <- (trav_contents_natural A unit t (const tt)).
change (map (const tt) t) with (shape t).
rewrite trav_contents_shape.
reflexivity.
Qed.
Lemma trav_same_shape_rev {A1 A2: Type}
{t1: T A1} {t2: T A2}:
(∀ B, trav_make (B := B) t1 ~!~ trav_make t2) →
shape t1 = shape t2.
Proof.
introv Hmake.
rewrite shape_spec.
rewrite shape_spec.
destruct (Hmake unit) as
[Hlen Hmake'].
apply Vector_fun_sim_eq.
- apply Hmake.
- now inversion Hlen.
Qed.
Lemma trav_same_shape_iff {A1 A2: Type}
{t1: T A1} {t2: T A2}:
shape t1 = shape t2 ↔
(∀ B, trav_make (B := B) t1 ~!~ trav_make t2).
Proof.
split.
- apply trav_same_shape.
- apply trav_same_shape_rev.
Qed.
Corollary trav_make_sim_map:
∀ `(t: T A)
`(f: A → B) (C: Type),
trav_make (B := C) t ~!~
(trav_make (B := C) (map (F := T) f t)).
Proof.
intros.
apply trav_same_shape_iff.
rewrite shape_map.
reflexivity.
Qed.
∀ (A: Type) (t: T A),
trav_contents (shape t) ~~ Vector_tt (plength t).
Proof.
intros.
(* LHS *)
unfold trav_contents.
apply Vector_coerce_sim_l'.
unfold shape.
replace (toBatch (A' := False) (map (const tt) t))
with (mapfst_Batch (B := False) (const tt) (toBatch t)).
2:{ compose near t.
now rewrite toBatch_mapfst. }
unfold Vector_tt.
unfold plength.
rewrite mapReduce_through_runBatch1.
unfold compose.
induction (toBatch t).
- reflexivity.
- cbn.
unfold_ops @NaturalNumbers.Monoid_op_plus.
rewrite PeanoNat.Nat.add_1_r.
cbn.
apply vcons_sim.
assumption.
Qed.
Lemma shape_spec:
∀ (A: Type) (t: T A),
shape t = trav_make (B := unit) t (Vector_tt (plength t)).
Proof.
intros A t.
unfold shape.
rewrite map_spec.
fequal.
apply Vector_sim_eq.
unfold Vector_sim.
rewrite <- (trav_contents_natural A unit t (const tt)).
change (map (const tt) t) with (shape t).
rewrite trav_contents_shape.
reflexivity.
Qed.
Lemma trav_same_shape_rev {A1 A2: Type}
{t1: T A1} {t2: T A2}:
(∀ B, trav_make (B := B) t1 ~!~ trav_make t2) →
shape t1 = shape t2.
Proof.
introv Hmake.
rewrite shape_spec.
rewrite shape_spec.
destruct (Hmake unit) as
[Hlen Hmake'].
apply Vector_fun_sim_eq.
- apply Hmake.
- now inversion Hlen.
Qed.
Lemma trav_same_shape_iff {A1 A2: Type}
{t1: T A1} {t2: T A2}:
shape t1 = shape t2 ↔
(∀ B, trav_make (B := B) t1 ~!~ trav_make t2).
Proof.
split.
- apply trav_same_shape.
- apply trav_same_shape_rev.
Qed.
Corollary trav_make_sim_map:
∀ `(t: T A)
`(f: A → B) (C: Type),
trav_make (B := C) t ~!~
(trav_make (B := C) (map (F := T) f t)).
Proof.
intros.
apply trav_same_shape_iff.
rewrite shape_map.
reflexivity.
Qed.
Lemma trav_make_shape_spec {A B: Type}: ∀ (t: T A),
trav_make (B := B) t ~!~ trav_make (B := B) (shape t).
Proof.
intros t.
apply trav_same_shape.
rewrite shape_shape.
reflexivity.
Qed.
trav_make (B := B) t ~!~ trav_make (B := B) (shape t).
Proof.
intros t.
apply trav_same_shape.
rewrite shape_shape.
reflexivity.
Qed.
Lemma tosubset_spec `{ToSubset T} `{! Compat_ToSubset_Traverse T}:
∀ (A: Type) (t: T A),
tosubset t = tosubset (trav_contents t).
Proof.
intros A t.
rewrite tosubset_through_tolist.
unfold compose at 1.
rewrite (tosubset_through_tolist (T := Vector (plength t))).
unfold compose at 1.
rewrite <- Vector_to_list_tolist.
rewrite tolist_trav_contents.
rewrite tosubset_to_mapReduce.
apply mapReduce_comm_list.
Qed.
End deconstruction.
∀ (A: Type) (t: T A),
tosubset t = tosubset (trav_contents t).
Proof.
intros A t.
rewrite tosubset_through_tolist.
unfold compose at 1.
rewrite (tosubset_through_tolist (T := Vector (plength t))).
unfold compose at 1.
rewrite <- Vector_to_list_tolist.
rewrite tolist_trav_contents.
rewrite tosubset_to_mapReduce.
apply mapReduce_comm_list.
Qed.
End deconstruction.
Section misc.
Context
`{Classes.Kleisli.TraversableFunctor.TraversableFunctor T}
`{ToMap_inst: Map T}
`{ToSubset_inst: ToSubset T}
`{ToBatch_inst: ToBatch T}
`{! Compat_Map_Traverse T}
`{! Compat_ToSubset_Traverse T}
`{! Compat_ToBatch_Traverse T}.
(*
(** ** Same <<shape>> Implies Same <<trav_make>> *)
(********************************************************************)
Lemma same_shape_implies_make_sim:
forall (A B C: Type) (t: T A) (u: T B),
shape t = shape u ->
trav_make (B := C) t ~!~ trav_make u.
Proof.
intros. apply trav_same_shape.
assumption.
introv Hshape.
eapply (transitive_Vector_fun_sim).
apply (trav_make_shape_spec t).
rewrite Hshape.
apply symmetric_Vector_fun_sim.
apply (trav_make_shape_spec u).
Qed.
*)
Context
`{Classes.Kleisli.TraversableFunctor.TraversableFunctor T}
`{ToMap_inst: Map T}
`{ToSubset_inst: ToSubset T}
`{ToBatch_inst: ToBatch T}
`{! Compat_Map_Traverse T}
`{! Compat_ToSubset_Traverse T}
`{! Compat_ToBatch_Traverse T}.
(*
(** ** Same <<shape>> Implies Same <<trav_make>> *)
(********************************************************************)
Lemma same_shape_implies_make_sim:
forall (A B C: Type) (t: T A) (u: T B),
shape t = shape u ->
trav_make (B := C) t ~!~ trav_make u.
Proof.
intros. apply trav_same_shape.
assumption.
introv Hshape.
eapply (transitive_Vector_fun_sim).
apply (trav_make_shape_spec t).
rewrite Hshape.
apply symmetric_Vector_fun_sim.
apply (trav_make_shape_spec u).
Qed.
*)
Lemma same_shape_implies_other_make:
∀ (A B: Type) (t: T A) (u: T B)
(Hshape: shape t = shape u),
t = trav_make u
(coerce (same_shape_implies_plength t u Hshape)
in (trav_contents t)).
Proof.
intros.
change t with (id t) at 1.
rewrite id_spec.
pose (cut := trav_same_shape Hshape A).
destruct cut as [Hlen H_make_eq].
apply H_make_eq.
vector_sim.
Qed.
End misc.
∀ (A B: Type) (t: T A) (u: T B)
(Hshape: shape t = shape u),
t = trav_make u
(coerce (same_shape_implies_plength t u Hshape)
in (trav_contents t)).
Proof.
intros.
change t with (id t) at 1.
rewrite id_spec.
pose (cut := trav_same_shape Hshape A).
destruct cut as [Hlen H_make_eq].
apply H_make_eq.
vector_sim.
Qed.
End misc.
From Tealeaves Require Import Functors.Pair.
Section traversable_functors_zipping.
Context
`{Classes.Kleisli.TraversableFunctor.TraversableFunctor T}
`{ToMap_inst: Map T}
`{ToSubset_inst: ToSubset T}
`{ToBatch_inst: ToBatch T}
`{! Compat_Map_Traverse T}
`{! Compat_ToSubset_Traverse T}
`{! Compat_ToBatch_Traverse T}.
Section traversable_functors_zipping.
Context
`{Classes.Kleisli.TraversableFunctor.TraversableFunctor T}
`{ToMap_inst: Map T}
`{ToSubset_inst: ToSubset T}
`{ToBatch_inst: ToBatch T}
`{! Compat_Map_Traverse T}
`{! Compat_ToSubset_Traverse T}
`{! Compat_ToBatch_Traverse T}.
Definition same_shape_zip_contents
(A B: Type) (t: T A) (u: T B)
(Hshape: shape t = shape u):
Vector (plength t) (A × B) :=
Vector_zip A B (plength t) (plength u) (trav_contents t) (trav_contents u)
(same_shape_implies_plength t u Hshape).
#[global] Arguments same_shape_zip_contents {A B}%type_scope t u Hshape.
(A B: Type) (t: T A) (u: T B)
(Hshape: shape t = shape u):
Vector (plength t) (A × B) :=
Vector_zip A B (plength t) (plength u) (trav_contents t) (trav_contents u)
(same_shape_implies_plength t u Hshape).
#[global] Arguments same_shape_zip_contents {A B}%type_scope t u Hshape.
Lemma same_shape_zip_contents_proof_irrelevance:
∀ (A B: Type) (t: T A) (u: T B)
(Hshape1: shape t = shape u)
(Hshape2: shape t = shape u),
same_shape_zip_contents t u Hshape1 =
same_shape_zip_contents t u Hshape2.
Proof.
intros.
unfold same_shape_zip_contents.
fequal.
apply proof_irrelevance.
Qed.
(* useful when <<u>> can't be rewritten due to Hshape proofs *)
Lemma same_shape_zip_contents_proof_irrelevance2:
∀ (A B: Type)
(t: T A) (u: T B) (u': T B)
(Hshape1: shape t = shape u)
(Hshape2: shape t = shape u'),
u = u' →
same_shape_zip_contents t u Hshape1 =
same_shape_zip_contents t u' Hshape2.
Proof.
introv Heq.
subst.
apply same_shape_zip_contents_proof_irrelevance.
Qed.
(* useful when <<u>> can't be rewritten due to Hshape proofs *)
Lemma same_shape_zip_contents_proof_irrelevance3:
∀ (A B: Type)
(t: T A) (t': T A) (u: T B) (u': T B)
(Hshape1: shape t = shape u)
(Hshape2: shape t' = shape u'),
t = t' →
u = u' →
(same_shape_zip_contents t u Hshape1 ~~
same_shape_zip_contents t' u' Hshape2).
Proof.
introv Heqt Hequ.
subst.
erewrite same_shape_zip_contents_proof_irrelevance.
reflexivity.
Qed.
∀ (A B: Type) (t: T A) (u: T B)
(Hshape1: shape t = shape u)
(Hshape2: shape t = shape u),
same_shape_zip_contents t u Hshape1 =
same_shape_zip_contents t u Hshape2.
Proof.
intros.
unfold same_shape_zip_contents.
fequal.
apply proof_irrelevance.
Qed.
(* useful when <<u>> can't be rewritten due to Hshape proofs *)
Lemma same_shape_zip_contents_proof_irrelevance2:
∀ (A B: Type)
(t: T A) (u: T B) (u': T B)
(Hshape1: shape t = shape u)
(Hshape2: shape t = shape u'),
u = u' →
same_shape_zip_contents t u Hshape1 =
same_shape_zip_contents t u' Hshape2.
Proof.
introv Heq.
subst.
apply same_shape_zip_contents_proof_irrelevance.
Qed.
(* useful when <<u>> can't be rewritten due to Hshape proofs *)
Lemma same_shape_zip_contents_proof_irrelevance3:
∀ (A B: Type)
(t: T A) (t': T A) (u: T B) (u': T B)
(Hshape1: shape t = shape u)
(Hshape2: shape t' = shape u'),
t = t' →
u = u' →
(same_shape_zip_contents t u Hshape1 ~~
same_shape_zip_contents t' u' Hshape2).
Proof.
introv Heqt Hequ.
subst.
erewrite same_shape_zip_contents_proof_irrelevance.
reflexivity.
Qed.
Lemma same_shape_zip_contents_fst
(A B: Type) (t: T A) (u: T B)
(Hshape: shape t = shape u):
map fst (same_shape_zip_contents t u Hshape) = trav_contents t.
Proof.
unfold same_shape_zip_contents.
rewrite Vector_zip_fst.
reflexivity.
Qed.
Lemma same_shape_zip_contents_snd
(A B: Type) (t: T A) (u: T B)
(Hshape: shape t = shape u):
map snd (same_shape_zip_contents t u Hshape) ~~ trav_contents u.
Proof.
unfold same_shape_zip_contents.
apply (Vector_zip_snd A B
(plength t) (plength u)
(trav_contents t) (trav_contents u)
(same_shape_implies_plength t u Hshape)).
Qed.
(A B: Type) (t: T A) (u: T B)
(Hshape: shape t = shape u):
map fst (same_shape_zip_contents t u Hshape) = trav_contents t.
Proof.
unfold same_shape_zip_contents.
rewrite Vector_zip_fst.
reflexivity.
Qed.
Lemma same_shape_zip_contents_snd
(A B: Type) (t: T A) (u: T B)
(Hshape: shape t = shape u):
map snd (same_shape_zip_contents t u Hshape) ~~ trav_contents u.
Proof.
unfold same_shape_zip_contents.
apply (Vector_zip_snd A B
(plength t) (plength u)
(trav_contents t) (trav_contents u)
(same_shape_implies_plength t u Hshape)).
Qed.
Lemma same_shape_map {A1 A2 B1 B2}:
∀ (t: T A1) (u: T B1) (Hshape: shape t = shape u)
(f: A1 → A2) (g: B1 → B2),
shape (map f t) = shape (map g u).
Proof.
intros.
rewrite (shape_map).
rewrite (shape_map).
assumption.
Qed.
Lemma same_shape_map_l {A1 A2 B}:
∀ (t: T A1) (u: T B) (Hshape: shape t = shape u)
(f: A1 → A2),
shape (map f t) = shape u.
Proof.
intros.
rewrite (shape_map).
assumption.
Qed.
Lemma same_shape_map_r {A B1 B2}:
∀ (t: T A) (u: T B1) (Hshape: shape t = shape u)
(g: B1 → B2),
shape t = shape (map g u).
Proof.
intros.
rewrite (shape_map).
assumption.
Qed.
Lemma same_shape_map_rev {A1 A2 B1 B2}:
∀ (t: T A1) (u: T B1)
(f: A1 → A2) (g: B1 → B2)
(Hshape: shape (map f t) = shape (map g u)),
shape t = shape u.
Proof.
introv.
rewrite (shape_map).
rewrite (shape_map).
easy.
Qed.
Lemma same_shape_map_rev_l {A1 A2 B}:
∀ (t: T A1) (u: T B)
(f: A1 → A2)
(Hshape: shape (map f t) = shape u),
shape t = shape u.
Proof.
introv.
rewrite (shape_map).
easy.
Qed.
Lemma same_shape_map_rev_r {A B1 B2}:
∀ (t: T A) (u: T B1)
(g: B1 → B2)
(Hshape: shape t = shape (map g u)),
shape t = shape u.
Proof.
introv.
rewrite (shape_map).
easy.
Qed.
Lemma natural_same_shape_zip_contents
{A1 A2 B1 B2: Type}:
∀ (t: T A1) (u: T B1) (Hshape: shape t = shape u)
(f: A1 → A2) (g: B1 → B2),
map (map_pair f g) (same_shape_zip_contents t u Hshape)=
coerce (natural_plength f t) in
same_shape_zip_contents (map f t) (map g u) (same_shape_map t u Hshape _ _).
Proof.
intros.
apply Vector_sim_eq.
vector_sim.
unfold same_shape_zip_contents.
unfold Vector_zip.
rewrite natural_Vector_zip_eq.
apply Vector_zip_eq_sim_poly_both.
- apply symmetric_Vector_sim.
apply trav_contents_natural.
- vector_sim.
apply symmetric_Vector_sim.
apply trav_contents_natural.
Qed.
Lemma natural_same_shape_zip_contents_op
{A1 A2 B1 B2: Type}:
∀ (t: T A1) (u: T B1)
(f: A1 → A2) (g: B1 → B2)
(Hshape: shape (map f t) = shape (map g u)),
same_shape_zip_contents (map f t) (map g u) Hshape =
coerce (eq_sym (natural_plength f t)) in
map (map_pair f g) (same_shape_zip_contents t u (same_shape_map_rev t u _ _ Hshape)).
Proof.
intros.
rewrite natural_same_shape_zip_contents.
apply Vector_sim_eq.
vector_sim.
vector_sim.
fequal.
fequal.
apply proof_irrelevance.
Qed.
Corollary natural_fst_same_shape_zip_contents
{A1 A2 B: Type}:
∀ (t: T A1) (u: T B) (Hshape: shape t = shape u)
(f: A1 → A2),
map (map_fst f) (same_shape_zip_contents t u Hshape) =
coerce (natural_plength f t) in
same_shape_zip_contents (map f t) u (same_shape_map_l t u Hshape f).
Proof.
intros.
rewrite map_fst_to_pair.
rewrite natural_same_shape_zip_contents.
apply Vector_sim_eq.
vector_sim.
fequal.
apply same_shape_zip_contents_proof_irrelevance2.
rewrite fun_map_id.
reflexivity.
Qed.
Corollary natural_fst_same_shape_zip_contents_rev
{A1 A2 B: Type}:
∀ (t: T A1) (u: T B)
(f: A1 → A2)
(Hshape: shape (map f t) = shape u),
same_shape_zip_contents (map f t) u Hshape =
coerce (eq_sym (natural_plength f t)) in
map (map_fst f) (same_shape_zip_contents t u (same_shape_map_rev_l _ _ _ Hshape)).
Proof.
intros.
rewrite map_fst_to_pair.
rewrite natural_same_shape_zip_contents.
apply Vector_sim_eq.
vector_sim.
fequal.
apply same_shape_zip_contents_proof_irrelevance2.
rewrite fun_map_id.
reflexivity.
Qed.
Corollary natural_snd_same_shape_zip_contents
{A B1 B2: Type}:
∀ (t: T A) (u: T B1) (Hshape: shape t = shape u)
(g: B1 → B2),
map (map_snd g) (same_shape_zip_contents t u Hshape) =
same_shape_zip_contents t (map g u) (same_shape_map_r t u Hshape g).
Proof.
intros.
rewrite map_snd_to_pair.
rewrite natural_same_shape_zip_contents.
apply Vector_sim_eq.
vector_sim.
apply same_shape_zip_contents_proof_irrelevance3.
rewrite fun_map_id.
reflexivity.
reflexivity.
Qed.
Corollary natural_snd_same_shape_zip_contents_rev
{A B1 B2: Type}:
∀ (t: T A) (u: T B1)
(g: B1 → B2)
(Hshape: shape t = shape (map g u)),
same_shape_zip_contents t (map g u) Hshape =
map (map_snd g) (same_shape_zip_contents t u (same_shape_map_rev_r _ _ _ Hshape)).
Proof.
intros.
rewrite map_snd_to_pair.
rewrite natural_same_shape_zip_contents.
apply Vector_sim_eq.
vector_sim.
apply same_shape_zip_contents_proof_irrelevance3.
rewrite fun_map_id.
reflexivity.
reflexivity.
Qed.
∀ (t: T A1) (u: T B1) (Hshape: shape t = shape u)
(f: A1 → A2) (g: B1 → B2),
shape (map f t) = shape (map g u).
Proof.
intros.
rewrite (shape_map).
rewrite (shape_map).
assumption.
Qed.
Lemma same_shape_map_l {A1 A2 B}:
∀ (t: T A1) (u: T B) (Hshape: shape t = shape u)
(f: A1 → A2),
shape (map f t) = shape u.
Proof.
intros.
rewrite (shape_map).
assumption.
Qed.
Lemma same_shape_map_r {A B1 B2}:
∀ (t: T A) (u: T B1) (Hshape: shape t = shape u)
(g: B1 → B2),
shape t = shape (map g u).
Proof.
intros.
rewrite (shape_map).
assumption.
Qed.
Lemma same_shape_map_rev {A1 A2 B1 B2}:
∀ (t: T A1) (u: T B1)
(f: A1 → A2) (g: B1 → B2)
(Hshape: shape (map f t) = shape (map g u)),
shape t = shape u.
Proof.
introv.
rewrite (shape_map).
rewrite (shape_map).
easy.
Qed.
Lemma same_shape_map_rev_l {A1 A2 B}:
∀ (t: T A1) (u: T B)
(f: A1 → A2)
(Hshape: shape (map f t) = shape u),
shape t = shape u.
Proof.
introv.
rewrite (shape_map).
easy.
Qed.
Lemma same_shape_map_rev_r {A B1 B2}:
∀ (t: T A) (u: T B1)
(g: B1 → B2)
(Hshape: shape t = shape (map g u)),
shape t = shape u.
Proof.
introv.
rewrite (shape_map).
easy.
Qed.
Lemma natural_same_shape_zip_contents
{A1 A2 B1 B2: Type}:
∀ (t: T A1) (u: T B1) (Hshape: shape t = shape u)
(f: A1 → A2) (g: B1 → B2),
map (map_pair f g) (same_shape_zip_contents t u Hshape)=
coerce (natural_plength f t) in
same_shape_zip_contents (map f t) (map g u) (same_shape_map t u Hshape _ _).
Proof.
intros.
apply Vector_sim_eq.
vector_sim.
unfold same_shape_zip_contents.
unfold Vector_zip.
rewrite natural_Vector_zip_eq.
apply Vector_zip_eq_sim_poly_both.
- apply symmetric_Vector_sim.
apply trav_contents_natural.
- vector_sim.
apply symmetric_Vector_sim.
apply trav_contents_natural.
Qed.
Lemma natural_same_shape_zip_contents_op
{A1 A2 B1 B2: Type}:
∀ (t: T A1) (u: T B1)
(f: A1 → A2) (g: B1 → B2)
(Hshape: shape (map f t) = shape (map g u)),
same_shape_zip_contents (map f t) (map g u) Hshape =
coerce (eq_sym (natural_plength f t)) in
map (map_pair f g) (same_shape_zip_contents t u (same_shape_map_rev t u _ _ Hshape)).
Proof.
intros.
rewrite natural_same_shape_zip_contents.
apply Vector_sim_eq.
vector_sim.
vector_sim.
fequal.
fequal.
apply proof_irrelevance.
Qed.
Corollary natural_fst_same_shape_zip_contents
{A1 A2 B: Type}:
∀ (t: T A1) (u: T B) (Hshape: shape t = shape u)
(f: A1 → A2),
map (map_fst f) (same_shape_zip_contents t u Hshape) =
coerce (natural_plength f t) in
same_shape_zip_contents (map f t) u (same_shape_map_l t u Hshape f).
Proof.
intros.
rewrite map_fst_to_pair.
rewrite natural_same_shape_zip_contents.
apply Vector_sim_eq.
vector_sim.
fequal.
apply same_shape_zip_contents_proof_irrelevance2.
rewrite fun_map_id.
reflexivity.
Qed.
Corollary natural_fst_same_shape_zip_contents_rev
{A1 A2 B: Type}:
∀ (t: T A1) (u: T B)
(f: A1 → A2)
(Hshape: shape (map f t) = shape u),
same_shape_zip_contents (map f t) u Hshape =
coerce (eq_sym (natural_plength f t)) in
map (map_fst f) (same_shape_zip_contents t u (same_shape_map_rev_l _ _ _ Hshape)).
Proof.
intros.
rewrite map_fst_to_pair.
rewrite natural_same_shape_zip_contents.
apply Vector_sim_eq.
vector_sim.
fequal.
apply same_shape_zip_contents_proof_irrelevance2.
rewrite fun_map_id.
reflexivity.
Qed.
Corollary natural_snd_same_shape_zip_contents
{A B1 B2: Type}:
∀ (t: T A) (u: T B1) (Hshape: shape t = shape u)
(g: B1 → B2),
map (map_snd g) (same_shape_zip_contents t u Hshape) =
same_shape_zip_contents t (map g u) (same_shape_map_r t u Hshape g).
Proof.
intros.
rewrite map_snd_to_pair.
rewrite natural_same_shape_zip_contents.
apply Vector_sim_eq.
vector_sim.
apply same_shape_zip_contents_proof_irrelevance3.
rewrite fun_map_id.
reflexivity.
reflexivity.
Qed.
Corollary natural_snd_same_shape_zip_contents_rev
{A B1 B2: Type}:
∀ (t: T A) (u: T B1)
(g: B1 → B2)
(Hshape: shape t = shape (map g u)),
same_shape_zip_contents t (map g u) Hshape =
map (map_snd g) (same_shape_zip_contents t u (same_shape_map_rev_r _ _ _ Hshape)).
Proof.
intros.
rewrite map_snd_to_pair.
rewrite natural_same_shape_zip_contents.
apply Vector_sim_eq.
vector_sim.
apply same_shape_zip_contents_proof_irrelevance3.
rewrite fun_map_id.
reflexivity.
reflexivity.
Qed.
Definition same_shape_zip
(A B: Type) (t: T A) (u: T B)
(Hshape: shape t = shape u):
T (A × B) :=
trav_make t (same_shape_zip_contents t u Hshape).
#[global] Arguments same_shape_zip {A B}%type_scope t u Hshape.
Lemma same_shape_zip_fst
(A B: Type) (t: T A) (u: T B)
(Hshape: shape t = shape u):
map fst (same_shape_zip t u Hshape) = t.
Proof.
unfold same_shape_zip.
rewrite <- (trav_make_natural A (A × B) A t (@fst A B)
(same_shape_zip_contents t u Hshape)).
rewrite same_shape_zip_contents_fst.
rewrite trav_get_put.
reflexivity.
Qed.
Lemma same_shape_zip_snd
(A B: Type) (t: T A) (u: T B)
(Hshape: shape t = shape u):
map snd (same_shape_zip t u Hshape) = u.
Proof.
unfold same_shape_zip.
rewrite <- (trav_make_natural A (A × B) B t (@snd A B)
(same_shape_zip_contents t u Hshape)).
change u with (id u) at 2.
rewrite id_spec.
apply Vector_fun_sim_eq.
- apply trav_same_shape.
assumption.
- apply same_shape_zip_contents_snd.
Qed.
(A B: Type) (t: T A) (u: T B)
(Hshape: shape t = shape u):
T (A × B) :=
trav_make t (same_shape_zip_contents t u Hshape).
#[global] Arguments same_shape_zip {A B}%type_scope t u Hshape.
Lemma same_shape_zip_fst
(A B: Type) (t: T A) (u: T B)
(Hshape: shape t = shape u):
map fst (same_shape_zip t u Hshape) = t.
Proof.
unfold same_shape_zip.
rewrite <- (trav_make_natural A (A × B) A t (@fst A B)
(same_shape_zip_contents t u Hshape)).
rewrite same_shape_zip_contents_fst.
rewrite trav_get_put.
reflexivity.
Qed.
Lemma same_shape_zip_snd
(A B: Type) (t: T A) (u: T B)
(Hshape: shape t = shape u):
map snd (same_shape_zip t u Hshape) = u.
Proof.
unfold same_shape_zip.
rewrite <- (trav_make_natural A (A × B) B t (@snd A B)
(same_shape_zip_contents t u Hshape)).
change u with (id u) at 2.
rewrite id_spec.
apply Vector_fun_sim_eq.
- apply trav_same_shape.
assumption.
- apply same_shape_zip_contents_snd.
Qed.
(* useful when <<u>> can't be rewritten due to Hshape proofs *)
Lemma same_shape_zip_proof_irrelevance:
∀ (A B: Type)
(t: T A) (t': T A) (u: T B) (u': T B)
(Hshape1: shape t = shape u)
(Hshape2: shape t' = shape u'),
t = t' →
u = u' →
same_shape_zip t u Hshape1 =
same_shape_zip t' u' Hshape2.
Proof.
introv Heqt Hequ.
subst.
fequal.
apply proof_irrelevance.
Qed.
Lemma same_shape_zip_proof_irrelevance:
∀ (A B: Type)
(t: T A) (t': T A) (u: T B) (u': T B)
(Hshape1: shape t = shape u)
(Hshape2: shape t' = shape u'),
t = t' →
u = u' →
same_shape_zip t u Hshape1 =
same_shape_zip t' u' Hshape2.
Proof.
introv Heqt Hequ.
subst.
fequal.
apply proof_irrelevance.
Qed.
Lemma natural_same_shape_zip
{A1 A2 B1 B2: Type}:
∀ (t: T A1) (u: T B1) (Hshape: shape t = shape u)
(f: A1 → A2) (g: B1 → B2),
map (map_pair f g) (same_shape_zip t u Hshape) =
same_shape_zip (map f t) (map g u) (same_shape_map t u Hshape _ _).
Proof.
intros.
unfold same_shape_zip.
rewrite <- trav_make_natural.
rewrite natural_same_shape_zip_contents.
apply Vector_fun_sim_eq.
- apply trav_same_shape.
rewrite shape_map.
reflexivity.
- vector_sim.
Qed.
Corollary natural_fst_same_shape_zip
{A1 A2 B: Type}:
∀ (t: T A1) (u: T B) (Hshape: shape t = shape u)
(f: A1 → A2),
map (map_fst f) (same_shape_zip t u Hshape) =
same_shape_zip (map f t) u (same_shape_map_l t u Hshape f).
Proof.
intros.
rewrite map_fst_to_pair.
rewrite natural_same_shape_zip.
apply same_shape_zip_proof_irrelevance.
- reflexivity.
- now rewrite fun_map_id.
Qed.
Corollary natural_snd_same_shape_zip
{A B1 B2: Type}:
∀ (t: T A) (u: T B1) (Hshape: shape t = shape u)
(g: B1 → B2),
map (map_snd g) (same_shape_zip t u Hshape) =
same_shape_zip t (map g u) (same_shape_map_r t u Hshape g).
Proof.
intros.
rewrite map_snd_to_pair.
rewrite natural_same_shape_zip.
apply same_shape_zip_proof_irrelevance.
- rewrite fun_map_id.
reflexivity.
- reflexivity.
Qed.
Lemma same_shape_zip_same_shape {A B}:
∀ (t: T A) (u: T B)
(Hshape: shape t = shape u),
shape (same_shape_zip t u Hshape) = shape t.
Proof.
intros.
apply (same_shape_map_rev _ _ fst id).
rewrite fun_map_id.
rewrite same_shape_zip_fst.
reflexivity.
Qed.
{A1 A2 B1 B2: Type}:
∀ (t: T A1) (u: T B1) (Hshape: shape t = shape u)
(f: A1 → A2) (g: B1 → B2),
map (map_pair f g) (same_shape_zip t u Hshape) =
same_shape_zip (map f t) (map g u) (same_shape_map t u Hshape _ _).
Proof.
intros.
unfold same_shape_zip.
rewrite <- trav_make_natural.
rewrite natural_same_shape_zip_contents.
apply Vector_fun_sim_eq.
- apply trav_same_shape.
rewrite shape_map.
reflexivity.
- vector_sim.
Qed.
Corollary natural_fst_same_shape_zip
{A1 A2 B: Type}:
∀ (t: T A1) (u: T B) (Hshape: shape t = shape u)
(f: A1 → A2),
map (map_fst f) (same_shape_zip t u Hshape) =
same_shape_zip (map f t) u (same_shape_map_l t u Hshape f).
Proof.
intros.
rewrite map_fst_to_pair.
rewrite natural_same_shape_zip.
apply same_shape_zip_proof_irrelevance.
- reflexivity.
- now rewrite fun_map_id.
Qed.
Corollary natural_snd_same_shape_zip
{A B1 B2: Type}:
∀ (t: T A) (u: T B1) (Hshape: shape t = shape u)
(g: B1 → B2),
map (map_snd g) (same_shape_zip t u Hshape) =
same_shape_zip t (map g u) (same_shape_map_r t u Hshape g).
Proof.
intros.
rewrite map_snd_to_pair.
rewrite natural_same_shape_zip.
apply same_shape_zip_proof_irrelevance.
- rewrite fun_map_id.
reflexivity.
- reflexivity.
Qed.
Lemma same_shape_zip_same_shape {A B}:
∀ (t: T A) (u: T B)
(Hshape: shape t = shape u),
shape (same_shape_zip t u Hshape) = shape t.
Proof.
intros.
apply (same_shape_map_rev _ _ fst id).
rewrite fun_map_id.
rewrite same_shape_zip_fst.
reflexivity.
Qed.
Lemma map_sim_fns:
∀ (n m: nat) (A B C: Type) `{Applicative G}
(mk1: Vector n B → C) (v1: Vector n A)
(mk2: Vector m B → C) (v2: Vector m A)
(f: A → G B),
mk1 ~!~ mk2 →
v1 ~~ v2 →
map (F := G) mk1 (traverse (G := G) (T := Vector n) f v1) = map (F := G) mk2 (traverse (T := Vector m) f v2).
Proof.
intros.
assert (Heq: n = m) by (now apply Vector_sim_length in H2).
generalize dependent v2.
generalize dependent m.
induction n; intros; subst.
- rewrite (Vector_nil_eq v1).
rewrite (Vector_nil_eq v2).
rewrite traverse_Vector_vnil.
fequal. ext v.
apply Vector_fun_sim_eq.
assumption. reflexivity.
- rewrite (Vector_surjective_pairing2 (v := v2)) in ×.
rewrite (Vector_surjective_pairing2 (v := v1)) in ×.
rewrite traverse_Vector_vcons.
rewrite traverse_Vector_vcons.
inversion H2.
do 2 rewrite proj_vcons in H4.
inversion H4.
fequal.
{ ext v. apply Vector_fun_sim_eq.
assumption. reflexivity. }
fequal.
fequal.
apply Vector_sim_eq.
apply H6.
Qed.
Definition traverse_same_shape_zip
`{Applicative G}
(A B C: Type) (t: T A) (u: T B)
(f: A × B → G C)
(Hshape: shape t = shape u)
:
traverse (T := T) f (same_shape_zip t u Hshape) =
map (F := G) (trav_make t)
(forwards (traverse (T := Vector (plength t)) (mkBackwards ∘ f) (same_shape_zip_contents t u Hshape))).
Proof.
assert (trav_make (B := C) (same_shape_zip t u Hshape) ~!~ trav_make t).
{ apply trav_same_shape.
apply same_shape_zip_same_shape.
}
rewrite traverse_repr.
assert (trav_contents (same_shape_zip t u Hshape) ~~
(same_shape_zip_contents t u Hshape)).
{ unfold same_shape_zip.
unfold Vector_sim.
rewrite trav_contents_make.
reflexivity. }
{ compose near (traverse (mkBackwards ∘ f) (trav_contents (same_shape_zip t u Hshape))).
compose near (traverse (mkBackwards ∘ f) (same_shape_zip_contents t u Hshape)).
rewrite natural.
rewrite natural.
unfold compose.
fequal.
apply map_sim_fns; auto.
typeclasses eauto.
}
Qed.
Instance ApplicativeMorphism_const_op `{op: Monoid_op M} `{unit: Monoid_unit M} `{! Monoid M}:
@ApplicativeMorphism (@const Type Type M) (Backwards (@const Type Type M))
(@Map_const M) (@Mult_const M (@Monoid_op_Opposite M op)) (@Pure_const M unit)
(@Map_Backwards (const M) _) (@Mult_Backwards (const M) (@Map_const M) (@Mult_const M op))
(@Pure_Backwards (const M) (@Pure_const M unit)) (@mkBackwards (const M)).
Proof.
constructor; try typeclasses eauto.
- reflexivity.
- reflexivity.
- reflexivity.
Qed.
Instance ApplicativeMorphism_const_op_inv `{op: Monoid_op M} `{unit: Monoid_unit M} `{! Monoid M}:
@ApplicativeMorphism (Backwards (@const Type Type M))(@const Type Type M)
(@Map_Backwards (const M) _) (@Mult_Backwards (const M) (@Map_const M) (@Mult_const M op))
(@Pure_Backwards (const M) (@Pure_const M unit))
(@Map_const M) (@Mult_const M (@Monoid_op_Opposite M op)) (@Pure_const M unit)
(@forwards (const M)).
Proof.
constructor; try typeclasses eauto.
- reflexivity.
- reflexivity.
- reflexivity.
Qed.
Definition foldmap_same_shape_zip
`{Monoid M}
(A B C: Type) (t: T A) (u: T B)
(f: A × B → M)
(Hshape: shape t = shape u)
:
mapReduce f (same_shape_zip t u Hshape) =
mapReduce (op := Monoid_op_Opposite op) f (same_shape_zip_contents t u Hshape).
Proof.
intros.
rewrite mapReduce_to_traverse1.
rewrite traverse_same_shape_zip.
rewrite mapReduce_to_traverse1.
unfold_ops @Map_const.
compose near (same_shape_zip_contents t u Hshape) on left.
change ((fun (X Y : Type) (_ : X → Y) (t0 : @const Type Type M X) ⇒ t0))
with (@Map_const M).
rewrite (trf_traverse_morphism (T := Vector (@plength T Traverse_T A t))
(morphism := ApplicativeMorphism_const_op_inv (M := M))).
reflexivity.
Qed.
(*
Lemma traverse_const_opposite `{Monoid M} {A B: Type} (f: A -> M):
traverse (T := T) (G := const M)
(@Mult_const M (@Monoid_op_Opposite M op))
Search traverse same_shape_zip_contents.
rewrite t
.
unfold mapReduce.
rewrite traverse_same_shape_zip.
rewrite <- traverse_repr.
rewrite traverse_same_shape_zip.
reflexivity.
Qed.
*)
End traversable_functors_zipping.
∀ (n m: nat) (A B C: Type) `{Applicative G}
(mk1: Vector n B → C) (v1: Vector n A)
(mk2: Vector m B → C) (v2: Vector m A)
(f: A → G B),
mk1 ~!~ mk2 →
v1 ~~ v2 →
map (F := G) mk1 (traverse (G := G) (T := Vector n) f v1) = map (F := G) mk2 (traverse (T := Vector m) f v2).
Proof.
intros.
assert (Heq: n = m) by (now apply Vector_sim_length in H2).
generalize dependent v2.
generalize dependent m.
induction n; intros; subst.
- rewrite (Vector_nil_eq v1).
rewrite (Vector_nil_eq v2).
rewrite traverse_Vector_vnil.
fequal. ext v.
apply Vector_fun_sim_eq.
assumption. reflexivity.
- rewrite (Vector_surjective_pairing2 (v := v2)) in ×.
rewrite (Vector_surjective_pairing2 (v := v1)) in ×.
rewrite traverse_Vector_vcons.
rewrite traverse_Vector_vcons.
inversion H2.
do 2 rewrite proj_vcons in H4.
inversion H4.
fequal.
{ ext v. apply Vector_fun_sim_eq.
assumption. reflexivity. }
fequal.
fequal.
apply Vector_sim_eq.
apply H6.
Qed.
Definition traverse_same_shape_zip
`{Applicative G}
(A B C: Type) (t: T A) (u: T B)
(f: A × B → G C)
(Hshape: shape t = shape u)
:
traverse (T := T) f (same_shape_zip t u Hshape) =
map (F := G) (trav_make t)
(forwards (traverse (T := Vector (plength t)) (mkBackwards ∘ f) (same_shape_zip_contents t u Hshape))).
Proof.
assert (trav_make (B := C) (same_shape_zip t u Hshape) ~!~ trav_make t).
{ apply trav_same_shape.
apply same_shape_zip_same_shape.
}
rewrite traverse_repr.
assert (trav_contents (same_shape_zip t u Hshape) ~~
(same_shape_zip_contents t u Hshape)).
{ unfold same_shape_zip.
unfold Vector_sim.
rewrite trav_contents_make.
reflexivity. }
{ compose near (traverse (mkBackwards ∘ f) (trav_contents (same_shape_zip t u Hshape))).
compose near (traverse (mkBackwards ∘ f) (same_shape_zip_contents t u Hshape)).
rewrite natural.
rewrite natural.
unfold compose.
fequal.
apply map_sim_fns; auto.
typeclasses eauto.
}
Qed.
Instance ApplicativeMorphism_const_op `{op: Monoid_op M} `{unit: Monoid_unit M} `{! Monoid M}:
@ApplicativeMorphism (@const Type Type M) (Backwards (@const Type Type M))
(@Map_const M) (@Mult_const M (@Monoid_op_Opposite M op)) (@Pure_const M unit)
(@Map_Backwards (const M) _) (@Mult_Backwards (const M) (@Map_const M) (@Mult_const M op))
(@Pure_Backwards (const M) (@Pure_const M unit)) (@mkBackwards (const M)).
Proof.
constructor; try typeclasses eauto.
- reflexivity.
- reflexivity.
- reflexivity.
Qed.
Instance ApplicativeMorphism_const_op_inv `{op: Monoid_op M} `{unit: Monoid_unit M} `{! Monoid M}:
@ApplicativeMorphism (Backwards (@const Type Type M))(@const Type Type M)
(@Map_Backwards (const M) _) (@Mult_Backwards (const M) (@Map_const M) (@Mult_const M op))
(@Pure_Backwards (const M) (@Pure_const M unit))
(@Map_const M) (@Mult_const M (@Monoid_op_Opposite M op)) (@Pure_const M unit)
(@forwards (const M)).
Proof.
constructor; try typeclasses eauto.
- reflexivity.
- reflexivity.
- reflexivity.
Qed.
Definition foldmap_same_shape_zip
`{Monoid M}
(A B C: Type) (t: T A) (u: T B)
(f: A × B → M)
(Hshape: shape t = shape u)
:
mapReduce f (same_shape_zip t u Hshape) =
mapReduce (op := Monoid_op_Opposite op) f (same_shape_zip_contents t u Hshape).
Proof.
intros.
rewrite mapReduce_to_traverse1.
rewrite traverse_same_shape_zip.
rewrite mapReduce_to_traverse1.
unfold_ops @Map_const.
compose near (same_shape_zip_contents t u Hshape) on left.
change ((fun (X Y : Type) (_ : X → Y) (t0 : @const Type Type M X) ⇒ t0))
with (@Map_const M).
rewrite (trf_traverse_morphism (T := Vector (@plength T Traverse_T A t))
(morphism := ApplicativeMorphism_const_op_inv (M := M))).
reflexivity.
Qed.
(*
Lemma traverse_const_opposite `{Monoid M} {A B: Type} (f: A -> M):
traverse (T := T) (G := const M)
(@Mult_const M (@Monoid_op_Opposite M op))
Search traverse same_shape_zip_contents.
rewrite t
.
unfold mapReduce.
rewrite traverse_same_shape_zip.
rewrite <- traverse_repr.
rewrite traverse_same_shape_zip.
reflexivity.
Qed.
*)
End traversable_functors_zipping.
Section fold_over_vector_pairs.
Context {A B A0 B0: Type} `{Monoid M} `(f: A × B → M).
Lemma mapReduce_vector_pair_natural:
∀ (fl: A0 → A) (fr: B0 → B),
∀ (n: nat) (v: Vector n (A0 × B0)),
mapReduce (T := Vector n) f (map (F := Vector n) (map_tensor fl fr) v) =
mapReduce (T := Vector n) (f ∘ map_tensor fl fr) v.
Proof.
intros.
compose near v on left.
rewrite mapReduce_map.
reflexivity.
Qed.
Lemma mapReduce_vector_pair_natural_l:
∀ (fl: A0 → A) (n: nat) (v: Vector n (A0 × B)),
mapReduce (T := Vector n) f (map (F := Vector n) (map_fst fl) v) =
mapReduce (T := Vector n) (f ∘ map_fst fl) v.
Proof.
intros.
compose near v on left.
rewrite mapReduce_map.
reflexivity.
Qed.
Lemma mapReduce_vector_pair_natural_r:
∀ (fr: B0 → B) (n: nat) (v: Vector n (A × B0)),
mapReduce (T := Vector n) f (map (F := Vector n) (map_snd fr) v) =
mapReduce (T := Vector n) (f ∘ map_snd fr) v.
Proof.
intros.
compose near v on left.
rewrite mapReduce_map.
reflexivity.
Qed.
End fold_over_vector_pairs.
Context {A B A0 B0: Type} `{Monoid M} `(f: A × B → M).
Lemma mapReduce_vector_pair_natural:
∀ (fl: A0 → A) (fr: B0 → B),
∀ (n: nat) (v: Vector n (A0 × B0)),
mapReduce (T := Vector n) f (map (F := Vector n) (map_tensor fl fr) v) =
mapReduce (T := Vector n) (f ∘ map_tensor fl fr) v.
Proof.
intros.
compose near v on left.
rewrite mapReduce_map.
reflexivity.
Qed.
Lemma mapReduce_vector_pair_natural_l:
∀ (fl: A0 → A) (n: nat) (v: Vector n (A0 × B)),
mapReduce (T := Vector n) f (map (F := Vector n) (map_fst fl) v) =
mapReduce (T := Vector n) (f ∘ map_fst fl) v.
Proof.
intros.
compose near v on left.
rewrite mapReduce_map.
reflexivity.
Qed.
Lemma mapReduce_vector_pair_natural_r:
∀ (fr: B0 → B) (n: nat) (v: Vector n (A × B0)),
mapReduce (T := Vector n) f (map (F := Vector n) (map_snd fr) v) =
mapReduce (T := Vector n) (f ∘ map_snd fr) v.
Proof.
intros.
compose near v on left.
rewrite mapReduce_map.
reflexivity.
Qed.
End fold_over_vector_pairs.
Section uniqueness_lemmas.
Context {A B: Type}.
Context
`{Classes.Kleisli.TraversableFunctor.TraversableFunctor T}
`{ToMap_inst: Map T}
`{ToBatch_inst: ToBatch T}
`{! Compat_Map_Traverse T}
`{! Compat_ToBatch_Traverse T}.
Lemma trav_contents_unique:
∀ (t: T A) (u: T B) (v: Vector (plength t) B),
trav_make t v = u → v ~~ trav_contents u.
Proof.
introv Hmake.
rewrite <- Hmake.
unfold Vector_sim.
rewrite trav_contents_make.
reflexivity.
Qed.
Lemma trav_make_unique:
∀ (t: T A) (u: T B) (v: Vector (plength t) B),
trav_make t v = u →
∀ (C: Type), trav_make (B := C) t ~!~ trav_make u.
Proof.
introv Hmake. intro C.
rewrite <- Hmake.
rewrite symmetric_Vector_fun_sim.
apply trav_make_make.
Qed.
Corollary trav_decomposition_unique:
∀ (t: T A) (u: T B) (v: Vector (plength t) B),
trav_make t v = u →
(∀ C, trav_make (B := C) t ~!~ trav_make u) ∧
v ~~ trav_contents u.
Proof.
introv Hmake; split.
eauto using trav_make_unique.
auto using trav_contents_unique.
Qed.
Corollary trav_decomposition_unique_iff:
∀ (t: T A) (u: T B) (v: Vector (plength t) B),
trav_make t v = u ↔
(∀ C, trav_make (B := C) t ~!~ trav_make u) ∧
v ~~ trav_contents u.
Proof.
intros. split.
- apply trav_decomposition_unique.
- intros [Hmake Hcontents].
rewrite <- (trav_get_put (t := u)).
apply Vector_fun_sim_eq; auto.
Qed.
Corollary trav_decomposition_same_shape:
∀ (t: T A) (u: T B) (v: Vector (plength t) B),
trav_make t v = u →
shape t = shape u.
Proof.
introv Hmake.
apply trav_same_shape_rev.
eapply trav_make_unique.
eassumption.
Qed.
Corollary trav_decomposition_same_length:
∀ (t: T A) (u: T B) (v: Vector (plength t) B),
trav_make t v = u →
plength t = plength u.
Proof.
introv Hmake.
apply same_shape_implies_plength.
eapply trav_decomposition_same_shape.
eassumption.
Qed.
End uniqueness_lemmas.