section catamorphism
  def cata {α β : Type} (b : β) (f : α → β → β) (x : List α) :=
    match x with
    | [] => b
    | a :: as => f a (cata b f as)

  notation:max "⦅" l:10 "," r:11 "⦆" => cata l r

  -- theorem cata_fusion (h : β → β) (b : β) (f : α → β → β) : h ∘ ⦅b, f⦆ = ⦅b, h ∘ f⦆ := by
    -- sorry

  section length
    def length := ⦅0, Function.const Nat Nat.succ⦆
    theorem length_empty : length [] = Nat.zero := by
      unfold length
      unfold cata
      rfl

    theorem length_cons : length (a :: as) = Nat.succ (length as) := by
      match as with
      | [] =>
        rw [length_empty]
        unfold length
        simp [cata]
      | b :: bs =>
        unfold length
        simp [cata]
    end length

  section filter
    def filter {α : Type} (p : α → Bool) := ⦅[],
    λ (a as) => if (p a) then (a :: as) else (as)⦆

    theorem filter_nil {α : Type} (p : α → Bool) : filter p [] = [] := by
      unfold filter
      simp [cata]

    theorem filter_cons_pos {α : Type} (p : α → Bool) {a : α} (l : List α) : p a → filter p (a :: l) = a :: (filter p l) := by
      intro hp
      unfold filter
      simp [cata]
      simp [hp]

    theorem filter_cons_neg {α : Type} (p : α → Bool) {a : α} (l : List α) : ¬p a → filter p (a :: l) = filter p l := by
      intro hp
      unfold filter
      simp [cata]
      simp [hp]
    end filter
end catamorphism

section anamorphism
  partial def ana {α β : Type} (g : β → α × β) (p : β → Bool) (b : β) :=
    match p b with
    | true => []
    | false => let t := g b
              t.fst :: ana g p t.snd

  notation:max "〖" l:10 "," r:11 "〗" => ana l r

  section zip
    def p (l : List α × List β) := match l with
      | ([], _) => true
      | (_, []) => true
      | _ => false

    def g [Inhabited α] [Inhabited β] (l : List α × List β) := match l with
      | (a :: as, b :: bs) => ((a,b),(as,bs))
      -- prove this cant happen, i dont wanna handle this case
      | _ => ((default,default), ([], []))


    def curry : (α × β → φ) → α → β → φ := fun f a b => f (a, b)
    def zip [Inhabited α] [Inhabited β] : List α → List β → List (α × β) := curry 〖g, p〗
    -- theorem zip_nil_left {α β : Type} [Inhabited β] [Inhabited α] {l1 : List α} {l2 : List β} : l1 = [] → zip l1 l2 = [] := by
    --   -- intro emp
    --   -- rw [emp]
    --   -- unfold zip
    --   sorry

    -- theorem zip_cons_cons {α β : Type} [Inhabited β] [Inhabited α] {l1 : List α} {l2 : List β} : l2 = [] → zip l1 l2 = [] := by
    --   intro emp
    --   rw [emp]

    --   sorry
    #eval zip ["hello"] ["world"]
  end zip

  -- def g {α : Type} (a : α) := (a, f a)
  -- def iterate {α β : Type} (f : α → β) := let g := fun a => (f a, a)
  --                  ana g (Function.const α  false)

  -- theorem iterate_nonempty {α β : Type} (f : α → β) (a : α) : iterate f a ≠ [] := by
  --   unfold iterate

  --   sorry
  -- example : List.head (iterate Nat.succ 0) = 1 := by
    -- sorry
  -- #eval List.head (iterate Nat.succ 0)
end anamorphism

section hylomorphism
  -- partial def hylo (c : φ) (f : β → φ → φ) (g : α → β × α) (p : α → Bool) (a : α) := match p a with
  --   | true => c
  --   | false => let t := g a
  --             f t.fst (hylo c f g p t.snd)

  def hylo (c : φ) (f : β → φ → φ) (g : α → β × α) (p : α → Bool) := ⦅c,f⦆ ∘ 〖g, p〗

  notation:max "⟦" "(" c:10 "," f:11 ")" "," "(" g:12 "," p:13 ")" "⟧" => hylo c f g p

  section factorial
    def g_1 (n : Nat) := match n with
      | Nat.succ k => (n, k)
      -- prove this cant happen, i dont wanna handle this case
      | 0 => default

    def fac := ⟦(1, Nat.mul), (g_1, λ n => n = 0)⟧

    #eval fac 6

  end factorial

end hylomorphism