KStore.v

From Tealeaves Require Export
  Functors.Early.Batch
  Functors.Vector.

#[local] Generalizable Variables G ϕ.

Import Applicative.Notations.

(** * The [KStore] functor *)
(******************************************************************************)
Inductive KStore A B C :=
  { length : nat;
    contents : VEC length A;
    build : VEC length B -> C;
  }.

Definition kstore {A B : Type}: A -> KStore A B B :=
  fun a => Build_KStore A B B 1 (Vector.cons A a 0 (Vector.nil A)) unone.

(** ** Functor instance *)
(******************************************************************************)
Section map.

  Context
    {A B : Type}.

  Definition map_KStore : forall (C D : Type) (f : C -> D),
      KStore A B C -> KStore A B D.A, B: Type
forall C D : Type,
(C -> D) -> KStore A B C -> KStore A B D
  Proof.A, B: Type
forall C D : Type,
(C -> D) -> KStore A B C -> KStore A B D
    intros.A, B, C, D: Type
f: C -> D
X: KStore A B C
KStore A B D destruct X.A, B, C, D: Type
f: C -> D
length0: nat
contents0: Vector.t A length0
build0: Vector.t B length0 -> C
KStore A B D
    econstructor.A, B, C, D: Type
f: C -> D
length0: nat
contents0: Vector.t A length0
build0: Vector.t B length0 -> C
Vector.t A ?length
A, B, C, D: Type
f: C -> D
length0: nat
contents0: Vector.t A length0
build0: Vector.t B length0 -> C
Vector.t B ?length -> D eassumption.A, B, C, D: Type
f: C -> D
length0: nat
contents0: Vector.t A length0
build0: Vector.t B length0 -> C
Vector.t B length0 -> D
    intros.A, B, C, D: Type
f: C -> D
length0: nat
contents0: Vector.t A length0
build0: Vector.t B length0 -> C
X: Vector.t B length0
D apply f.A, B, C, D: Type
f: C -> D
length0: nat
contents0: Vector.t A length0
build0: Vector.t B length0 -> C
X: Vector.t B length0
C auto.
  Defined.

  #[export] Instance Map_KStore : Map (KStore A B) := map_KStore.

  Lemma map_id_KStore : forall (C : Type),
      map (F := KStore A B) (@id C) = @id (KStore A B C).A, B: Type
forall C : Type, map id = id
  Proof.A, B: Type
forall C : Type, map id = id
    intros.A, B, C: Type
map id = id ext k.A, B, C: Type
k: KStore A B C
map id k = id k destruct k as [len contents make].A, B, C: Type
len: nat
contents: Vector.t A len
make: Vector.t B len -> C
map id
  {|
    length := len; contents := contents; build := make
  |} =
id
  {|
    length := len; contents := contents; build := make
  |}
    reflexivity.

  Qed.
  Lemma map_map_KStore : forall (C D E : Type) (f : C -> D) (g : D -> E),
      map (F := KStore A B) g ∘ map (F := KStore A B) f = map (F := KStore A B) (g ∘ f).A, B: Type
forall (C D E : Type) (f : C -> D) (g : D -> E),
map g ∘ map f = map (g ∘ f)
  Proof.A, B: Type
forall (C D E : Type) (f : C -> D) (g : D -> E),
map g ∘ map f = map (g ∘ f)
    intros.A, B, C, D, E: Type
f: C -> D
g: D -> E
map g ∘ map f = map (g ∘ f) ext k.A, B, C, D, E: Type
f: C -> D
g: D -> E
k: KStore A B C
(map g ∘ map f) k = map (g ∘ f) k destruct k as [len contents make].A, B, C, D, E: Type
f: C -> D
g: D -> E
len: nat
contents: Vector.t A len
make: Vector.t B len -> C
(map g ∘ map f)
  {|
    length := len; contents := contents; build := make
  |} =
map (g ∘ f)
  {|
    length := len; contents := contents; build := make
  |}
    reflexivity.
  Qed.

  #[export] Instance Functor_KStore : Functor (KStore A B) :=
    {| fun_map_id := @map_id_KStore;
      fun_map_map := @map_map_KStore;
    |}.

End map.

(** ** Applicative instance *)
(******************************************************************************)
Definition pure_KStore: forall (A B C : Type), C -> KStore A B C.forall A B C : Type, C -> KStore A B C
Proof.forall A B C : Type, C -> KStore A B C
  intros.A, B, C: Type
X: C
KStore A B C
  apply (Build_KStore _ _ _ 0).A, B, C: Type
X: C
Vector.t A 0
A, B, C: Type
X: C
Vector.t B 0 -> C
  apply Vector.nil.A, B, C: Type
X: C
Vector.t B 0 -> C
  intros _; apply X.
Defined.

#[export] Instance Pure_KStore (A B : Type): Pure (KStore A B) :=
  pure_KStore A B.

Definition mult_KStore: forall (A B C D : Type),
    KStore A B C * KStore A B D -> KStore A B (C * D).forall A B C D : Type,
KStore A B C * KStore A B D -> KStore A B (C * D)
Proof.forall A B C D : Type,
KStore A B C * KStore A B D -> KStore A B (C * D)
  introv [k1 k2].A, B, C, D: Type
k1: KStore A B C
k2: KStore A B D
KStore A B (C * D)
  destruct k1.A, B, C, D: Type
length0: nat
contents0: Vector.t A length0
build0: Vector.t B length0 -> C
k2: KStore A B D
KStore A B (C * D)
  destruct k2.A, B, C, D: Type
length0: nat
contents0: Vector.t A length0
build0: Vector.t B length0 -> C
length1: nat
contents1: Vector.t A length1
build1: Vector.t B length1 -> D
KStore A B (C * D)
  apply (Build_KStore A B (C * D) (length0 + length1)).A, B, C, D: Type
length0: nat
contents0: Vector.t A length0
build0: Vector.t B length0 -> C
length1: nat
contents1: Vector.t A length1
build1: Vector.t B length1 -> D
Vector.t A (length0 + length1)
A, B, C, D: Type
length0: nat
contents0: Vector.t A length0
build0: Vector.t B length0 -> C
length1: nat
contents1: Vector.t A length1
build1: Vector.t B length1 -> D
Vector.t B (length0 + length1) -> C * D
  apply Vector.append; eauto.A, B, C, D: Type
length0: nat
contents0: Vector.t A length0
build0: Vector.t B length0 -> C
length1: nat
contents1: Vector.t A length1
build1: Vector.t B length1 -> D
Vector.t B (length0 + length1) -> C * D
  intro t.A, B, C, D: Type
length0: nat
contents0: Vector.t A length0
build0: Vector.t B length0 -> C
length1: nat
contents1: Vector.t A length1
build1: Vector.t B length1 -> D
t: Vector.t B (length0 + length1)
C * D
  apply (VectorDef.splitat length0) in t.A, B, C, D: Type
length0: nat
contents0: Vector.t A length0
build0: Vector.t B length0 -> C
length1: nat
contents1: Vector.t A length1
build1: Vector.t B length1 -> D
t: VectorDef.t B length0 * VectorDef.t B length1
C * D
  destruct t as [tc td].A, B, C, D: Type
length0: nat
contents0: Vector.t A length0
build0: Vector.t B length0 -> C
length1: nat
contents1: Vector.t A length1
build1: Vector.t B length1 -> D
tc: VectorDef.t B length0
td: VectorDef.t B length1
C * D
  split; auto.
Defined.

#[export] Instance Mult_KStore (A B : Type):
  Mult (KStore A B) := mult_KStore A B.

#[export] Instance Applicative_KStore:
  forall (A B : Type), Applicative (KStore A B).forall A B : Type, Applicative (KStore A B)
Proof.forall A B : Type, Applicative (KStore A B)
  intros.A, B: Type
Applicative (KStore A B) constructor.A, B: Type
Functor (KStore A B)
A, B: Type
forall (A0 B0 : Type) (f : A0 -> B0) (x : A0),
map f (pure x) = pure (f x)
A, B: Type
forall (A0 B0 C D : Type) (f : A0 -> C) (g : B0 -> D)
  (x : KStore A B A0) (y : KStore A B B0),
map f x ⊗ map g y = map (map_tensor f g) (x ⊗ y)
A, B: Type
forall (A0 B0 C : Type) (x : KStore A B A0)
  (y : KStore A B B0) (z : KStore A B C),
map associator (x ⊗ y ⊗ z) = x ⊗ (y ⊗ z)
A, B: Type
forall (A0 : Type) (x : KStore A B A0),
map left_unitor (pure tt ⊗ x) = x
A, B: Type
forall (A0 : Type) (x : KStore A B A0),
map right_unitor (x ⊗ pure tt) = x
A, B: Type
forall (A0 B0 : Type) (a : A0) (b : B0),
pure a ⊗ pure b = pure (a, b)
  -A, B: Type
Functor (KStore A B) typeclasses eauto.
  -A, B: Type
forall (A0 B0 : Type) (f : A0 -> B0) (x : A0),
map f (pure x) = pure (f x) intros.A, B, A0, B0: Type
f: A0 -> B0
x: A0
map f (pure x) = pure (f x)
    reflexivity.
  -A, B: Type
forall (A0 B0 C D : Type) (f : A0 -> C) (g : B0 -> D)
  (x : KStore A B A0) (y : KStore A B B0),
map f x ⊗ map g y = map (map_tensor f g) (x ⊗ y) intros.A, B, A0, B0, C, D: Type
f: A0 -> C
g: B0 -> D
x: KStore A B A0
y: KStore A B B0
map f x ⊗ map g y = map (map_tensor f g) (x ⊗ y)
    destruct x.A, B, A0, B0, C, D: Type
f: A0 -> C
g: B0 -> D
length0: nat
contents0: Vector.t A length0
build0: Vector.t B length0 -> A0
y: KStore A B B0
map f
  {|
    length := length0;
    contents := contents0;
    build := build0
  |} ⊗ map g y =
map (map_tensor f g)
  ({|
     length := length0;
     contents := contents0;
     build := build0
   |} ⊗ y)
    destruct y.A, B, A0, B0, C, D: Type
f: A0 -> C
g: B0 -> D
length0: nat
contents0: Vector.t A length0
build0: Vector.t B length0 -> A0
length1: nat
contents1: Vector.t A length1
build1: Vector.t B length1 -> B0
map f
  {|
    length := length0;
    contents := contents0;
    build := build0
  |}
⊗ map g
    {|
      length := length1;
      contents := contents1;
      build := build1
    |} =
map (map_tensor f g)
  ({|
     length := length0;
     contents := contents0;
     build := build0
   |}
   ⊗ {|
       length := length1;
       contents := contents1;
       build := build1
     |})
    cbn.A, B, A0, B0, C, D: Type
f: A0 -> C
g: B0 -> D
length0: nat
contents0: Vector.t A length0
build0: Vector.t B length0 -> A0
length1: nat
contents1: Vector.t A length1
build1: Vector.t B length1 -> B0
{|
  length := length0 + length1;
  contents := Vector.append contents0 contents1;
  build :=
    fun t : Vector.t B (length0 + length1) =>
    let (a, b) := VectorDef.splitat length0 t in
    (f (build0 a), g (build1 b))
|} =
{|
  length := length0 + length1;
  contents := Vector.append contents0 contents1;
  build :=
    fun X : Vector.t B (length0 + length1) =>
    map_tensor f g
      (let (a, b) := VectorDef.splitat length0 X in
       (build0 a, build1 b))
|}
    fequal.A, B, A0, B0, C, D: Type
f: A0 -> C
g: B0 -> D
length0: nat
contents0: Vector.t A length0
build0: Vector.t B length0 -> A0
length1: nat
contents1: Vector.t A length1
build1: Vector.t B length1 -> B0
(fun t : Vector.t B (length0 + length1) =>
 let (a, b) := VectorDef.splitat length0 t in
 (f (build0 a), g (build1 b))) =
(fun X : Vector.t B (length0 + length1) =>
 map_tensor f g
   (let (a, b) := VectorDef.splitat length0 X in
    (build0 a, build1 b)))
    ext t.A, B, A0, B0, C, D: Type
f: A0 -> C
g: B0 -> D
length0: nat
contents0: Vector.t A length0
build0: Vector.t B length0 -> A0
length1: nat
contents1: Vector.t A length1
build1: Vector.t B length1 -> B0
t: Vector.t B (length0 + length1)
(let (a, b) := VectorDef.splitat length0 t in
 (f (build0 a), g (build1 b))) =
map_tensor f g
  (let (a, b) := VectorDef.splitat length0 t in
   (build0 a, build1 b))
    destruct (VectorDef.splitat length0 t).A, B, A0, B0, C, D: Type
f: A0 -> C
g: B0 -> D
length0: nat
contents0: Vector.t A length0
build0: Vector.t B length0 -> A0
length1: nat
contents1: Vector.t A length1
build1: Vector.t B length1 -> B0
t: Vector.t B (length0 + length1)
t0: VectorDef.t B length0
t1: VectorDef.t B length1
(f (build0 t0), g (build1 t1)) =
map_tensor f g (build0 t0, build1 t1)
    reflexivity.
  -A, B: Type
forall (A0 B0 C : Type) 
  (x : KStore A B A0) (y : KStore A B B0)
  (z : KStore A B C),
map associator (x ⊗ y ⊗ z) = x ⊗ (y ⊗ z) intros.A, B, A0, B0, C: Type
x: KStore A B A0
y: KStore A B B0
z: KStore A B C
map associator (x ⊗ y ⊗ z) = x ⊗ (y ⊗ z)
    destruct x, y, z.A, B, A0, B0, C: Type
length0: nat
contents0: Vector.t A length0
build0: Vector.t B length0 -> A0
length1: nat
contents1: Vector.t A length1
build1: Vector.t B length1 -> B0
length2: nat
contents2: Vector.t A length2
build2: Vector.t B length2 -> C
map associator
  ({|
     length := length0;
     contents := contents0;
     build := build0
   |}
   ⊗ {|
       length := length1;
       contents := contents1;
       build := build1
     |}
   ⊗ {|
       length := length2;
       contents := contents2;
       build := build2
     |}) =
{|
  length := length0;
  contents := contents0;
  build := build0
|}
⊗ ({|
     length := length1;
     contents := contents1;
     build := build1
   |}
   ⊗ {|
       length := length2;
       contents := contents2;
       build := build2
     |})
    cbn.A, B, A0, B0, C: Type
length0: nat
contents0: Vector.t A length0
build0: Vector.t B length0 -> A0
length1: nat
contents1: Vector.t A length1
build1: Vector.t B length1 -> B0
length2: nat
contents2: Vector.t A length2
build2: Vector.t B length2 -> C
{|
  length := length0 + length1 + length2;
  contents :=
    Vector.append (Vector.append contents0 contents1)
      contents2;
  build :=
    fun X : Vector.t B (length0 + length1 + length2)
    =>
    associator
      (let (a, b) :=
         VectorDef.splitat (length0 + length1) X in
       (let (a0, b0) := VectorDef.splitat length0 a in
        (build0 a0, build1 b0), 
        build2 b))
|} =
{|
  length := length0 + (length1 + length2);
  contents :=
    Vector.append contents0
      (Vector.append contents1 contents2);
  build :=
    fun t : Vector.t B (length0 + (length1 + length2))
    =>
    let (a, b) := VectorDef.splitat length0 t in
    (build0 a,
     let (a0, b0) := VectorDef.splitat length1 b in
     (build1 a0, build2 b0))
|}
    assert (length0 + length1 + length2 =
              length0 + (length1 + length2))%nat.A, B, A0, B0, C: Type
length0: nat
contents0: Vector.t A length0
build0: Vector.t B length0 -> A0
length1: nat
contents1: Vector.t A length1
build1: Vector.t B length1 -> B0
length2: nat
contents2: Vector.t A length2
build2: Vector.t B length2 -> C
(length0 + length1 + length2)%nat =
(length0 + (length1 + length2))%nat
A, B, A0, B0, C: Type
length0: nat
contents0: Vector.t A length0
build0: Vector.t B length0 -> A0
length1: nat
contents1: Vector.t A length1
build1: Vector.t B length1 -> B0
length2: nat
contents2: Vector.t A length2
build2: Vector.t B length2 -> C
H: (length0 + length1 + length2)%nat =
(length0 + (length1 + length2))%nat
{|
  length := length0 + length1 + length2;
  contents :=
    Vector.append (Vector.append contents0 contents1)
      contents2;
  build :=
    fun X : Vector.t B (length0 + length1 + length2)
    =>
    associator
      (let (a, b) :=
         VectorDef.splitat (length0 + length1) X in
       (let (a0, b0) := VectorDef.splitat length0 a in
        (build0 a0, build1 b0), 
        build2 b))
|} =
{|
  length := length0 + (length1 + length2);
  contents :=
    Vector.append contents0
      (Vector.append contents1 contents2);
  build :=
    fun t : Vector.t B (length0 + (length1 + length2))
    =>
    let (a, b) := VectorDef.splitat length0 t in
    (build0 a,
     let (a0, b0) := VectorDef.splitat length1 b in
     (build1 a0, build2 b0))
|}
    lia.A, B, A0, B0, C: Type
length0: nat
contents0: Vector.t A length0
build0: Vector.t B length0 -> A0
length1: nat
contents1: Vector.t A length1
build1: Vector.t B length1 -> B0
length2: nat
contents2: Vector.t A length2
build2: Vector.t B length2 -> C
H: (length0 + length1 + length2)%nat =
(length0 + (length1 + length2))%nat
{|
  length := length0 + length1 + length2;
  contents :=
    Vector.append (Vector.append contents0 contents1)
      contents2;
  build :=
    fun X : Vector.t B (length0 + length1 + length2)
    =>
    associator
      (let (a, b) :=
         VectorDef.splitat (length0 + length1) X in
       (let (a0, b0) := VectorDef.splitat length0 a in
        (build0 a0, build1 b0), 
        build2 b))
|} =
{|
  length := length0 + (length1 + length2);
  contents :=
    Vector.append contents0
      (Vector.append contents1 contents2);
  build :=
    fun t : Vector.t B (length0 + (length1 + length2))
    =>
    let (a, b) := VectorDef.splitat length0 t in
    (build0 a,
     let (a0, b0) := VectorDef.splitat length1 b in
     (build1 a0, build2 b0))
|}
Abort.

(*
(** * Cata for <<KStore>> *)
(******************************************************************************)
Section cata.

  Context
    (A B : Type).

  Definition cata `{Mult G} `{Map G} `{Pure G}:
    forall (f : A -> G B) C, KStore A B C -> G C.
  Proof.
    intros f C [len contents make].
    pose (x := traverse (T := VEC len) (G := G) f contents).
    apply (map (F := G) make x).
  Defined.

  #[local] Instance Natural_cata:
    forall `{Applicative G} (f : A -> G B),
      Natural (cata f).
  Proof.
    constructor; try typeclasses eauto.
    intros. ext k.
    unfold compose. destruct k.
    cbn. compose near ((traverse (T := VEC length0) f contents0)) on left.
    rewrite (fun_map_map (F := G)).
    reflexivity.
  Qed.

  Lemma traverse_Vector_KStore: forall len kstore contents,
      traverse (T := VEC len)
               (G := KStore A B) kstore contents =
        {| length := len; contents := contents; build := (@id _) |}.
  Proof.
    intros len kstore contents.
    induction contents.
    - cbn.
      unfold_ops @Pure_KStore.
      unfold pure_KStore.
      fequal.
      ext b. rewrite toNil. reflexivity.
    - cbn.
      change_left (pure (F := KStore A B)
                        (Basics.flip (fun a : B => Vector.cons B a n))
                   <⋆> traverse (T := VEC n) (G := KStore A B) kstore contents0
                   <⋆> kstore h).
      rename h into a.
      rewrite IHcontents.
  Abort.

  Lemma cata_kstore : forall C, cata kstore C = @id (KStore A B C).
  Proof.
    intros C. ext k. destruct k as [len contents make].
    unfold id.
    unfold cata.
    Fail (now rewrite traverse_Vector_KStore).
  Abort.

  Lemma cata_appmor
  `{ApplicativeMorphism G1 G2 ϕ}:
    forall (f : A -> G1 B) C, ϕ C ∘ cata f C = cata (ϕ B ∘ f) C.
  Proof.
    intros. ext k.
    inversion H5. unfold compose. induction k.
    cbn. rewrite appmor_natural.
    compose near (contents0).
    rewrite (trf_traverse_morphism (T := VEC length0)).
    reflexivity.
  Qed.

End cata.
*)