cool stuff

6 files changed, 152 insertions, 0 deletions

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..1824d0c
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,3 @@
+/build
+/lakefile.olean
+/lake-packages/*
diff --git a/Bananas.lean b/Bananas.lean
new file mode 100644
index 0000000..f003560
--- /dev/null
+++ b/Bananas.lean
@@ -0,0 +1,3 @@
+-- This module serves as the root of the `Bananas` library.
+-- Import modules here that should be built as part of the library.
+import «Bananas».Basic
\ No newline at end of file
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
diff --git a/Main.lean b/Main.lean
new file mode 100644
index 0000000..bcfff43
--- /dev/null
+++ b/Main.lean
@@ -0,0 +1,4 @@
+import «Bananas»
+
+def main : IO Unit :=
+  IO.println s!"Hello, {hello}!"
diff --git a/lakefile.lean b/lakefile.lean
new file mode 100644
index 0000000..a961071
--- /dev/null
+++ b/lakefile.lean
@@ -0,0 +1,16 @@
+import Lake
+open Lake DSL
+
+package «bananas» where
+  -- add package configuration options here
+
+lean_lib «Bananas» where
+  -- add library configuration options here
+
+@[default_target]
+lean_exe «bananas» where
+  root := `Main
+  -- Enables the use of the Lean interpreter by the executable (e.g.,
+  -- `runFrontend`) at the expense of increased binary size on Linux.
+  -- Remove this line if you do not need such functionality.
+  supportInterpreter := true
diff --git a/lean-toolchain b/lean-toolchain
new file mode 100644
index 0000000..54be3ff
--- /dev/null
+++ b/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:4.2.0