From Tealeaves Require Export
  Functors.Batch
  Functors.KStore.

Import Batch.Notations.
Import Applicative.Notations.

#[local] Arguments length_Batch {A B C}%type_scope b.

(** * Batch to KStore *)
(******************************************************************************)

Section batch_to.

  Definition Batch_to_KStore {A B C}: Batch A B C -> KStore A B C.
A, B, C: Type
Batch A B C -> KStore A B C
  Proof.
A, B, C: Type
Batch A B C -> KStore A B C
    eapply (runBatch (G := KStore A B) kstore).
  Defined.

  Definition KStore_length: forall A B C,
      KStore A B C -> nat.
forall A B C : Type, KStore A B C -> nat
    intros.
A, B, C: Type
X: KStore A B C
nat destruct X.
A, B, C: Type
length: nat
contents: Vector.t A length
build: Vector.t B length -> C
nat
    assumption.
  Defined.

  Generalizable All Variables.

  Lemma length_Batch_KStore : forall `(b : Batch A B C),
      length_Batch b = KStore.length A B C (Batch_to_KStore b).
forall (A B C : Type) (b : Batch A B C),
length_Batch b = length A B C (Batch_to_KStore b)
    intros.
A, B, C: Type
b: Batch A B C
length_Batch b = length A B C (Batch_to_KStore b)
    induction b.
A, B, C: Type
c: C
length_Batch (Done c) =
length A B C (Batch_to_KStore (Done c))
A, B, C: Type
b: Batch A B (B -> C)
a: A
IHb: length_Batch b = length A B (B -> C) (Batch_to_KStore b)
length_Batch (b ⧆ a) =
length A B C (Batch_to_KStore (b ⧆ a))
    -
A, B, C: Type
c: C
length_Batch (Done c) =
length A B C (Batch_to_KStore (Done c)) reflexivity.
    -
A, B, C: Type
b: Batch A B (B -> C)
a: A
IHb: length_Batch b = length A B (B -> C) (Batch_to_KStore b)
length_Batch (b ⧆ a) =
length A B C (Batch_to_KStore (b ⧆ a)) cbn.
A, B, C: Type
b: Batch A B (B -> C)
a: A
IHb: length_Batch b = length A B (B -> C) (Batch_to_KStore b)
S (length_Batch b) =
length A B C (runBatch kstore b <⋆> kstore a)
      unfold ap.
A, B, C: Type
b: Batch A B (B -> C)
a: A
IHb: length_Batch b = length A B (B -> C) (Batch_to_KStore b)
S (length_Batch b) =
length A B C
  (map (fun '(f, a) => f a)
     (runBatch kstore b ⊗ kstore a))
      unfold length.
A, B, C: Type
b: Batch A B (B -> C)
a: A
IHb: length_Batch b = length A B (B -> C) (Batch_to_KStore b)
S (length_Batch b) =
(let (length, _, _) :=
   map (fun '(f, a) => f a)
     (runBatch kstore b ⊗ kstore a) in
 length)
      rewrite IHb.
A, B, C: Type
b: Batch A B (B -> C)
a: A
IHb: length_Batch b = length A B (B -> C) (Batch_to_KStore b)
S (length A B (B -> C) (Batch_to_KStore b)) =
(let (length, _, _) :=
   map (fun '(f, a) => f a)
     (runBatch kstore b ⊗ kstore a) in
 length)
  Abort.

  Context (A B C: Type).

  Definition Batch_to_Vector:
    Batch A B C -> @sigT nat (Vector.t A).
A, B, C: Type
Batch A B C -> {x : nat & Vector.t A x}
  Proof.
A, B, C: Type
Batch A B C -> {x : nat & Vector.t A x}
    intros b.
A, B, C: Type
b: Batch A B C
{x : nat & Vector.t A x}
    induction b.
A, B, C: Type
c: C
{x : nat & Vector.t A x}
A, B, C: Type
b: Batch A B (B -> C)
a: A
IHb: {x : nat & Vector.t A x}
{x : nat & Vector.t A x}
    -
A, B, C: Type
c: C
{x : nat & Vector.t A x} exists 0.
A, B, C: Type
c: C
Vector.t A 0 apply Vector.nil.
    -
A, B, C: Type
b: Batch A B (B -> C)
a: A
IHb: {x : nat & Vector.t A x}
{x : nat & Vector.t A x} destruct IHb as [n contents].
A, B, C: Type
b: Batch A B (B -> C)
a: A
n: nat
contents: Vector.t A n
{x : nat & Vector.t A x}
      exists (S n).
A, B, C: Type
b: Batch A B (B -> C)
a: A
n: nat
contents: Vector.t A n
Vector.t A (S n) apply Vector.cons.
A, B, C: Type
b: Batch A B (B -> C)
a: A
n: nat
contents: Vector.t A n
A
A, B, C: Type
b: Batch A B (B -> C)
a: A
n: nat
contents: Vector.t A n
Vector.t A n assumption.
A, B, C: Type
b: Batch A B (B -> C)
a: A
n: nat
contents: Vector.t A n
Vector.t A n
      assumption.
  Defined.

  Definition Batch_toMakeFn:
    Batch A B C -> @sigT nat (fun n => Vector.t B n -> C).
A, B, C: Type
Batch A B C -> {n : nat & Vector.t B n -> C}
  Proof.
A, B, C: Type
Batch A B C -> {n : nat & Vector.t B n -> C}
    intros b.
A, B, C: Type
b: Batch A B C
{n : nat & Vector.t B n -> C}
    induction b.
A, B, C: Type
c: C
{n : nat & Vector.t B n -> C}
A, B, C: Type
b: Batch A B (B -> C)
a: A
IHb: {n : nat & Vector.t B n -> B -> C}
{n : nat & Vector.t B n -> C}
    -
A, B, C: Type
c: C
{n : nat & Vector.t B n -> C} exists 0.
A, B, C: Type
c: C
Vector.t B 0 -> C intros _.
A, B, C: Type
c: C
C assumption.
    -
A, B, C: Type
b: Batch A B (B -> C)
a: A
IHb: {n : nat & Vector.t B n -> B -> C}
{n : nat & Vector.t B n -> C} destruct IHb as [n mk].
A, B, C: Type
b: Batch A B (B -> C)
a: A
n: nat
mk: Vector.t B n -> B -> C
{n : nat & Vector.t B n -> C}
      exists (S n).
A, B, C: Type
b: Batch A B (B -> C)
a: A
n: nat
mk: Vector.t B n -> B -> C
Vector.t B (S n) -> C intro v.
A, B, C: Type
b: Batch A B (B -> C)
a: A
n: nat
mk: Vector.t B n -> B -> C
v: Vector.t B (S n)
C
      remember (S n).
A, B, C: Type
b: Batch A B (B -> C)
a: A
n: nat
mk: Vector.t B n -> B -> C
n0: nat
Heqn0: n0 = S n
v: Vector.t B n0
C destruct v.
A, B, C: Type
b: Batch A B (B -> C)
a: A
n: nat
mk: Vector.t B n -> B -> C
Heqn0: 0 = S n
C
A, B, C: Type
b: Batch A B (B -> C)
a: A
n: nat
mk: Vector.t B n -> B -> C
n0: nat
Heqn0: S n0 = S n
h: B
v: Vector.t B n0
C
      +
A, B, C: Type
b: Batch A B (B -> C)
a: A
n: nat
mk: Vector.t B n -> B -> C
Heqn0: 0 = S n
C inversion Heqn0.
      +
A, B, C: Type
b: Batch A B (B -> C)
a: A
n: nat
mk: Vector.t B n -> B -> C
n0: nat
Heqn0: S n0 = S n
h: B
v: Vector.t B n0
C inversion Heqn0; subst.
A, B, C: Type
b: Batch A B (B -> C)
a: A
n: nat
mk: Vector.t B n -> B -> C
Heqn0: S n = S n
h: B
v: Vector.t B n
C
        apply mk.
A, B, C: Type
b: Batch A B (B -> C)
a: A
n: nat
mk: Vector.t B n -> B -> C
Heqn0: S n = S n
h: B
v: Vector.t B n
Vector.t B n
A, B, C: Type
b: Batch A B (B -> C)
a: A
n: nat
mk: Vector.t B n -> B -> C
Heqn0: S n = S n
h: B
v: Vector.t B n
B
        assumption.
A, B, C: Type
b: Batch A B (B -> C)
a: A
n: nat
mk: Vector.t B n -> B -> C
Heqn0: S n = S n
h: B
v: Vector.t B n
B
        assumption.
  Defined.

  Definition Batch_deconstructed:
    Batch A B C -> @sigT nat (fun n => VEC n A * (VEC n B -> C)).
A, B, C: Type
Batch A B C -> {n : nat & VEC n A * (VEC n B -> C)}
  Proof.
A, B, C: Type
Batch A B C -> {n : nat & VEC n A * (VEC n B -> C)}
    intros b.
A, B, C: Type
b: Batch A B C
{n : nat & VEC n A * (VEC n B -> C)}
    induction b.
A, B, C: Type
c: C
{n : nat & Vector.t A n * (Vector.t B n -> C)}
A, B, C: Type
b: Batch A B (B -> C)
a: A
IHb: {n : nat & Vector.t A n * (Vector.t B n -> B -> C)}
{n : nat & Vector.t A n * (Vector.t B n -> C)}
    -
A, B, C: Type
c: C
{n : nat & Vector.t A n * (Vector.t B n -> C)} exists 0.
A, B, C: Type
c: C
Vector.t A 0 * (Vector.t B 0 -> C) split.
A, B, C: Type
c: C
Vector.t A 0
A, B, C: Type
c: C
Vector.t B 0 -> C apply Vector.nil.
A, B, C: Type
c: C
Vector.t B 0 -> C auto.
    -
A, B, C: Type
b: Batch A B (B -> C)
a: A
IHb: {n : nat & Vector.t A n * (Vector.t B n -> B -> C)}
{n : nat & Vector.t A n * (Vector.t B n -> C)} destruct IHb as [n [contents mk]].
A, B, C: Type
b: Batch A B (B -> C)
a: A
n: nat
contents: Vector.t A n
mk: Vector.t B n -> B -> C
{n : nat & Vector.t A n * (Vector.t B n -> C)}
      exists (S n).
A, B, C: Type
b: Batch A B (B -> C)
a: A
n: nat
contents: Vector.t A n
mk: Vector.t B n -> B -> C
Vector.t A (S n) * (Vector.t B (S n) -> C) split.
A, B, C: Type
b: Batch A B (B -> C)
a: A
n: nat
contents: Vector.t A n
mk: Vector.t B n -> B -> C
Vector.t A (S n)
A, B, C: Type
b: Batch A B (B -> C)
a: A
n: nat
contents: Vector.t A n
mk: Vector.t B n -> B -> C
Vector.t B (S n) -> C
      +
A, B, C: Type
b: Batch A B (B -> C)
a: A
n: nat
contents: Vector.t A n
mk: Vector.t B n -> B -> C
Vector.t A (S n) apply Vector.cons.
A, B, C: Type
b: Batch A B (B -> C)
a: A
n: nat
contents: Vector.t A n
mk: Vector.t B n -> B -> C
A
A, B, C: Type
b: Batch A B (B -> C)
a: A
n: nat
contents: Vector.t A n
mk: Vector.t B n -> B -> C
Vector.t A n assumption.
A, B, C: Type
b: Batch A B (B -> C)
a: A
n: nat
contents: Vector.t A n
mk: Vector.t B n -> B -> C
Vector.t A n assumption.
      +
A, B, C: Type
b: Batch A B (B -> C)
a: A
n: nat
contents: Vector.t A n
mk: Vector.t B n -> B -> C
Vector.t B (S n) -> C intro v.
A, B, C: Type
b: Batch A B (B -> C)
a: A
n: nat
contents: Vector.t A n
mk: Vector.t B n -> B -> C
v: Vector.t B (S n)
C apply Vector.uncons in v.
A, B, C: Type
b: Batch A B (B -> C)
a: A
n: nat
contents: Vector.t A n
mk: Vector.t B n -> B -> C
v: B * Vector.t B n
C destruct v.
A, B, C: Type
b: Batch A B (B -> C)
a: A
n: nat
contents: Vector.t A n
mk: Vector.t B n -> B -> C
b0: B
t: Vector.t B n
C
        apply mk; auto.
  Defined.

  Definition Batch_to_KStore2: Batch A B C -> KStore A B C.
A, B, C: Type
Batch A B C -> KStore A B C
  Proof.
A, B, C: Type
Batch A B C -> KStore A B C
    intros b.
A, B, C: Type
b: Batch A B C
KStore A B C
    destruct (Batch_deconstructed b) as [len [contents mk]].
A, B, C: Type
b: Batch A B C
len: nat
contents: Vector.t A len
mk: Vector.t B len -> C
KStore A B C
    econstructor; eassumption.
  Defined.

End batch_to.

(*
(** ** <<KStore>> to <<Batch>> *)
(******************************************************************************)
Section toBatch.

  Context {A B C: Type}.

  Definition KStore_to_Batch: KStore A B C -> Batch A B C
    := cata A B (batch A B) C.

  (* induction on the length *)
  Definition KStore_to_Batch2: KStore A B C -> Batch A B C.
  Proof.
    intros k.
    destruct k as [len contents make].
    generalize dependent C.
    clear C.
    induction len.
    - intros C make.
      pose (c := make (Vector.nil B)).
      exact (Done c).
    - intros.
      apply Vector.uncons in contents.
      destruct contents as [a rest].
      specialize (IHlen rest (B -> C)).
      apply Step.
      + apply IHlen.
        intros. apply make. constructor; assumption.
      + assumption.
  Defined.

  (* induction on the contents themselves *)
  Definition KStore_to_Batch3: KStore A B C -> Batch A B C.
    intros k.
    destruct k as [len contents make].
    generalize dependent C.
    clear C.
    induction contents as [| a n rest IHrest].
    - intros C make.
      exact (Done (make (Vector.nil B))).
    - intros C make.
      apply Step.
      apply IHrest.
      intros restB b.
      apply make.
      apply Vector.cons.
      assumption.
      assumption.
      assumption.
  Defined.

End toBatch.

(* ISOS *)
Section isos.

  Context (A B C : Type).

  Lemma KStore_Batch_iso1: forall (k : KStore A B C),
      k = Batch_to_KStore (KStore_to_Batch k).
  Proof.
    intros.
    unfold KStore_to_Batch.
    unfold Batch_to_KStore.
    compose near k.
    (*
    Fail rewrite (cata_appmor _ _ (G1 := Batch A B) (G2 := KStore A B)).
    rewrite runBatch_batch.
    rewrite cata_kstore.
    reflexivity.
    typeclasses eauto.
    *)
  Abort.

  Lemma KStore_Batch_iso2: forall (b : Batch A B C),
      b = KStore_to_Batch (Batch_to_KStore b).
  Proof.
    intros.
    unfold KStore_to_Batch.
    unfold Batch_to_KStore.
    compose near b.
    enough (ApplicativeMorphism (KStore A B) (Batch A B)
                   (cata A B (batch A B))).
    rewrite (runBatch_morphism'(G := Batch A B) (F := KStore A B)).
  Abort.

End isos.
*)