Inductive t {A} : sort → Type :=
| const : A → t 𝟙
| concat {s1 s2} : t s1 → t s2 → t (s1 ∐ s2).

Arguments t : clear implicits.

Bind Scope concrete_scope with t.
Infix "++" := function.concat : concrete_scope.
Notation "s ~> A" := (t A s) (at level 99, right associativity) : concrete_scope.

Fixpoint constant {A} (x : A) {s} : s ~> A :=
  match s with
  | 𝟙 ⇒ const x
  | s1 ∐ s2 ⇒ constant x ++ constant x
  end.


Fixpoint map {A B : Type}(f : A → B) {s} (fA : s ~> A) : s ~> B:=
  match fA with
  | const a ⇒ const (f a)
  | fA1 ++ fA2 ⇒ map f fA1 ++ map f fA2
  end%con.

Lemma map_compose {A B C : Type}(f : B → C) (g : A → B){s}
  : map (s:=s) f \o map g =1 map (f \o g).
  elim ⇒ [|s1 s2 u1 IH1 u2 IH2].
  - move ⇒ a; rewrite //=.
  - by rewrite //= -IH1 -IH2 //=.
Qed.

Lemma map_eqfun {A B : Type}(f g : A → B): f =1 g → ∀ s (u : s ~> A), map f u = map g u.
  move ⇒ H s.
  elim ⇒ [|s1 s2 u1 IH1 u2 IH2 ].
  - move ⇒ a; by rewrite //= H.
  - by rewrite //= IH1 IH2.
Qed.

Definition unconst {A}(f : 𝟙 ~> A) : A :=
  match f with
  | const a ⇒ a
  end.

Definition unsum {A s1 s2}(v : s1 ∐ s2 ~> A) : (s1 ~> A) × (s2 ~> A) :=
  match v with
  | v1 ++ v2 ⇒ (v1 , v2)
  end.

Lemma unconst_const {A} : ∀ u : 𝟙 ~> A, const (unconst u) = u.
  move ⇒ u.
  dependent destruction u; rewrite //=.
Qed.

Lemma unsum_sum {A s1 s2} : ∀ u : (s1 ∐ s2) ~> A, ∃ u1 u2 , u1 ++ u2 = u.
  move ⇒ u.
  dependent destruction u; by ∃ u1; ∃ u2.
Qed.

Fixpoint zipWith {A B C}(f : A → B → C) {s} : (s ~> A) → (s ~> B) → s ~> C :=
  match s with
  | 𝟙 ⇒ fun a b ⇒ const (f (unconst a) (unconst b))
  | s1 ∐ s2 ⇒ fun v1 v2 ⇒ let (v11, v12) := unsum v1 in
                        let (v21, v22) := unsum v2 in
                        (zipWith f v11 v21) ++ (zipWith f v12 v22)
  end.

Definition zipWith3 {A B C D}(f : A → B → C → D) {s} (u : s ~> A)(v : s ~> B) : (s ~> C) → s ~> D :=
  zipWith (fun f x ⇒ f x) (zipWith f u v).

Definition zipWith4 {A B C D E}(f : A → B → C → D → E) {s}
  (u : s ~> A)(v : s ~> B)(w : s ~> C) : (s ~> D) → s ~> E :=
  zipWith (fun f x ⇒ f x) (zipWith3 f u v w).


Fixpoint fold {A} (f : A → A → A) {s} (v : s ~> A) : A :=
  match v with
  | const x ⇒ x
  | v1 ++ v2 ⇒ f (fold f v1) (fold f v2)
  end.

Section FoldMap.
  Context {A B}(conv : A → B).
  Context (f : A → A → A)(g : B → B → B).
  Context (Hconv : ∀ a1 a2, conv (f a1 a2) = g (conv a1) (conv a2)).

  Lemma fold_map {s} : ∀ u : s ~> A, fold g (map conv u) = conv (fold f u).
    elim ⇒ [|s1 s2 u1 IH1 u2 IH2].
    - by rewrite //=.
    - by rewrite //= IH1 IH2 Hconv.
  Qed.

End FoldMap.

Fixpoint transpose {A r c} : (r ~> c ~> A) → c ~> r ~> A :=
  match r as r0 return (r0 ~> c ~> A) → (c ~> r0 ~> A) with
  | 𝟙 ⇒ map const \o unconst
  | r1 ∐ r2 ⇒ fun v ⇒ let (v1 , v2) := unsum v in
                    zipWith concat (transpose v1) (transpose v2)
  end.

Fixpoint to {A s} (func : s ~> A) : s → A :=
  match func with
  | const a ⇒ fun _ ⇒ a
  | func1 ++ func2 ⇒ fun x ⇒ match x with
                            | inl x1 ⇒ to func1 x1
                            | inr x2 ⇒ to func2 x2
                            end
  end.

Definition denote {s A} (func : s ~> A) : {ffun universe.denote s → A} := finfun (to func).


Fixpoint from {A}{s : sort}: (s → A) → (s ~> A) :=
  match s as s0 return (s0 → A) → s0 ~> A with
  | 𝟙 ⇒ fun func ⇒ const (func tt)
  | s1 ∐ s2 ⇒ (fun func ⇒ from (func \o inl) ++ from (func \o inr))
  end.

Lemma denoteE {s A}(func : s ~> A) : ∀ x, denote func x = func x.
  move ⇒ x; by rewrite ffunE.
Qed.

Lemma constantE {s A}(a : A) : ∀ x, constant (s:=s) a x = a.
  induction s.
  - rewrite //=.
  - move ⇒ x; by case x.
Qed.

Lemma fromeq {A}{s : sort} (f g : s → A) (Hfext : f =1 g) : from f = from g.
  induction s as [|s1 IH1 s2 IH2].
  - by rewrite //= Hfext.
  - rewrite //=.
    have HL : f \o inl =1 g \o inl by [move ⇒ x; rewrite /comp Hfext].
    have HR : f \o inr =1 g \o inr by [move ⇒ x; rewrite /comp Hfext].
    by rewrite (IH1 _ _ HL) (IH2 _ _ HR).
Qed.

Lemma to_from {A} {s : sort} (f : s → A) : from f =1 f.
  move ⇒ x.
  induction s as [| s1 IH1 s2 IH2];
    destruct x; by rewrite //= ?IH1 ?IH2.
Qed.

Lemma from_to {A s}(v : s ~> A) : from (to v) = v.
  induction v as[| s1 s2 v1 IH1 v2 IH2]; by rewrite //= IH1 IH2.
Qed.

Lemma extensionality {A s} (v1 v2 : A ~> s) (Hexteq : v1 =1 v2) : v1 = v2.
  rewrite -(from_to v1) -(from_to v2); by apply fromeq.
Qed.

Lemma to_plus_1 {A s1 s2}(v1 : s1 ~> A) (v2 : s2 ~> A) : ∀ x, v1 x = (v1 ++ v2) (inl x).
  move ⇒ x; rewrite //=.
Qed.
Lemma to_plus_2 {A s1 s2}(v1 : s1 ~> A) (v2 : s2 ~> A) : ∀ x, v2 x = (v1 ++ v2) (inr x).
  move ⇒ x; rewrite //=.
Qed.

Lemma to_map {A B s} (f : A → B) (v : s ~> A) : ∀ x : s, map f v x = f (v x).
  move ⇒ x.
  induction v.
  - by destruct x.
  - destruct x; rewrite //=.
Qed.

Definition proj1 {A s1 s2}(v : s1 ∐ s2 ~> A) : s1 ~> A :=
  match v with
  | v1 ++ _ ⇒ v1
  end%con.

Definition proj2 {A s1 s2}(v : s1 ∐ s2 ~> A) : s2 ~> A :=
  match v with
  | _ ++ v2 ⇒ v2
  end%con.

Notation "p '.1'" := (function.proj1 p) (format "p .1") : concrete_scope.
Notation "p '.2'" := (function.proj2 p) (format "p .2") : concrete_scope.

Lemma sum_proj {A s1 s2} : ∀ x : s1 ∐ s2 ~> A , (x.1 ++ x.2 = x).
  move ⇒ x.
  dependent destruction x.
  rewrite //=.
Qed.

Lemma proj_sum_1 {A s1 s2} : ∀ (x : s1 ~> A) (y : s2 ~> A), ((x ++ y).1 = x).
  trivial.
Qed.

Lemma proj_sum_2 {A s1 s2} : ∀ (x : s1 ~> A) (y : s2 ~> A), ((x ++ y).2 = y).
  trivial.
Qed.

Lemma to_proj1 {A s1 s2} (v : s1 ∐ s2 ~> A) (x : s1) : (v.1 x = v (inl x)).
  by dependent destruction v; rewrite //=.
Qed.

Lemma to_proj2 {A s1 s2} (v : s1 ∐ s2 ~> A ) (x : s2) : (v.2 x = v (inr x)).
  by dependent destruction v; rewrite //=.
Qed.

Lemma zip_pointwise {A B C}(f : A → B → C) {s} (va : s ~> A )(vb : s ~> B) (x : s)
  : zipWith f va vb x = f (va x) (vb x).
  induction va; dependent destruction vb; destruct x; by [rewrite //=].
Qed.

Lemma zip_pointwise3 {A B C D}(f : A → B → C → D) {s} (va : s ~> A )(vb : s ~> B) (vc : s ~> C) (x : s)
  : zipWith3 f va vb vc x = f (va x) (vb x) (vc x).
  by rewrite /zipWith3 ?zip_pointwise.
Qed.

Lemma zip_pointwise4 {A B C D E}(f : A → B → C → D → E) {s}
  (va : s ~> A )(vb : s ~> B) (vc : s ~> C) (vd : s ~> D) (x : s)
  : zipWith4 f va vb vc vd x = f (va x) (vb x) (vc x) (vd x).
  by rewrite /zipWith3 ?zip_pointwise.
Qed.

Section ZipWithMap.
  Context {A B C : Type}(f : A → B → C).

  Section Right.
    Context {Bp Cp : Type}.
    Context (fp : A → Bp → Cp).
    Context (convB : B → Bp)(convC : C → Cp).
    Context (Hconv : ∀ (a : A)(b : B), convC (f a b) = fp a (convB b)).
    Lemma zipWith_mapR {s}(u : s ~> A)(v : s ~> B) : map convC (zipWith f u v) = zipWith fp u (map convB v).
      apply extensionality ⇒ x; by rewrite to_map ?zip_pointwise to_map Hconv.
    Qed.

  End Right.

End ZipWithMap.

Lemma transpose_spec {A r c}(v : r ~> c ~> A) x y : transpose v y x = v x y.
  induction v.
  - case: x; by rewrite /comp to_map //=.
  - case: x; by rewrite zip_pointwise //=.
Qed.

Fixpoint ifeq {A} (th el : A) {s : sort} : s → s ~> A :=
  match s with
  | 𝟙 ⇒ fun _ ⇒ const th
  | s1 ∐ s2 ⇒ fun x ⇒ match x with
                    | inl x1 ⇒ ifeq th el x1 ++ constant el
                    | inr x2 ⇒ constant el ++ ifeq th el x2
                    end
  end.

Lemma ifeq_spec {A}(th el : A) {s : sort} : ∀ (x y : s), ifeq th el x y = if y == x then th else el.
  elim s ⇒ [|s1 IH1 s2 IH2]; move ⇒ x y; case x; case y; rewrite //=; move ⇒ z u; by rewrite //= constantE.
Qed.