From 98eb18bc338c7292d58404f81b86cbc0fcc11c51 Mon Sep 17 00:00:00 2001
From: tzlil <tzlils@protonmail.com>
Date: Fri, 15 Mar 2024 17:20:40 +0200
Subject: cool stuff

---
 Bananas/Basic.lean | 125 +++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 125 insertions(+)
 create mode 100644 Bananas/Basic.lean

(limited to 'Bananas/Basic.lean')

diff --git a/Bananas/Basic.lean b/Bananas/Basic.lean
new file mode 100644
index 0000000..121d563
--- /dev/null
+++ b/Bananas/Basic.lean
@@ -0,0 +1,125 @@
+
+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
-- 
cgit 1.4.1