From 42e1c0b81f997ebd0f377eb5f14a24b657363ea3 Mon Sep 17 00:00:00 2001
From: tzlil <tzlils@protonmail.com>
Date: Fri, 15 Mar 2024 23:51:51 +0200
Subject: improve hylo and ana morphisms

---
 Bananas/Basic.lean | 83 +++++++++++++++++++++++-------------------------------
 1 file changed, 36 insertions(+), 47 deletions(-)

(limited to 'Bananas')

diff --git a/Bananas/Basic.lean b/Bananas/Basic.lean
index 121d563..b972e86 100644
--- a/Bananas/Basic.lean
+++ b/Bananas/Basic.lean
@@ -1,3 +1,4 @@
+import Std.Data.List.Basic
 
 section catamorphism
   def cata {α β : Type} (b : β) (f : α → β → β) (x : List α) :=
@@ -26,6 +27,8 @@ section catamorphism
       | b :: bs =>
         unfold length
         simp [cata]
+
+    #eval length [1,2,3,4,5,6,7,8,9]
     end length
 
   section filter
@@ -47,76 +50,62 @@ section catamorphism
       unfold filter
       simp [cata]
       simp [hp]
+
+    #eval filter (·>5) [1,2,3,4,5,6,7,8,9]
     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
+  partial def ana {α β : Type} (p : β → Bool) (b : β) (g : ∀ (b : β) (_ : ¬p b), α × β) := by
+    cases h : (p b)
+    have hp := ne_true_of_eq_false h
+    let t := g b hp
+    exact t.fst :: ana p t.snd g
+    exact []
 
-  notation:max "〖" l:10 "," r:11 "〗" => ana l r
+  notation:max "〖" l:10 "," r:11 "〗" => λ b => ana r b l
 
   section zip
-    def p (l : List α × List β) := match l with
-      | ([], _) => true
-      | (_, []) => true
-      | _ => false
+    def p (l : List α × List β) : Bool := (List.length l.1) = 0 || (List.length l.2 = 0)
 
-    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), ([], []))
+    -- this si fucking ugly!!!!!!
+    def g (l : List α × List β) (hp : ¬p l) := by
+      unfold p at hp
+      simp at hp
+      rw [not_or] at hp
 
+      have left := And.left hp
+      rw [List.length_eq_zero] at left
+      have right := And.right hp
+      rw [List.length_eq_zero] at right
 
-    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
+      have lh := List.head l.fst left
+      have rh := List.head l.snd right
 
-  -- def g {α : Type} (a : α) := (a, f a)
-  -- def iterate {α β : Type} (f : α → β) := let g := fun a => (f a, a)
-  --                  ana g (Function.const α  false)
+      exact ((lh, rh), (List.tail l.fst, List.tail l.snd))
 
-  -- theorem iterate_nonempty {α β : Type} (f : α → β) (a : α) : iterate f a ≠ [] := by
-  --   unfold iterate
+    def curry : (α × β → φ) → α → β → φ := fun f a b => f (a, b)
+    def zip : List α → List β → List (α × β) := curry 〖g, p〗
 
-  --   sorry
-  -- example : List.head (iterate Nat.succ 0) = 1 := by
-    -- sorry
-  -- #eval List.head (iterate Nat.succ 0)
+    #eval zip [1] [2]
+  end zip
 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)
+    -- | 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〗
+  def hylo (c : φ) (f : β → φ → φ) (p : α → Bool) (g : (b : α) → ¬p b = true → β × α) := ⦅c,f⦆ ∘ 〖g, p〗
 
-  notation:max "⟦" "(" c:10 "," f:11 ")" "," "(" g:12 "," p:13 ")" "⟧" => hylo c f g p
+  notation:max "⟦" "(" c:10 "," f:11 ")" "," "(" g:12 "," p:13 ")" "⟧" => hylo c f p g
 
   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 p_1 (n : Nat) := decide (n = 0)
+    def g_1 (b : Nat) (hp : ¬p_1 b = true) : Nat × Nat := (b, b-1)
 
-    def fac := ⟦(1, Nat.mul), (g_1, λ n => n = 0)⟧
+    def fac : Nat → Nat := ⟦(1, Nat.mul), (g_1, p_1)⟧
 
     #eval fac 6
 
-- 
cgit 1.4.1