From 78a3f33d2d41dec531b274c5c267988c27a3f673 Mon Sep 17 00:00:00 2001
From: Walter Schulze <awalterschulze@gmail.com>
Date: Thu, 19 Dec 2024 10:11:48 +0000
Subject: [PATCH] add list splitat theorem

Also move extra Nat theorems into their own file
---
 Katydid.lean                |  1 +
 Katydid/Expr/Desc.lean      | 20 ++++----
 Katydid/Regex/Language.lean |  2 +-
 Katydid/Std/Lists.lean      | 97 +++++++------------------------------
 Katydid/Std/Nat.lean        | 81 +++++++++++++++++++++++++++++++
 5 files changed, 111 insertions(+), 90 deletions(-)
 create mode 100644 Katydid/Std/Nat.lean

diff --git a/Katydid.lean b/Katydid.lean
index e20527f..46a73c6 100644
--- a/Katydid.lean
+++ b/Katydid.lean
@@ -1,6 +1,7 @@
 import Katydid.Std.Ordering
 import Katydid.Std.Decidable
 import Katydid.Std.OrderingThunk
+import Katydid.Std.Nat
 import Katydid.Std.Lists
 import Katydid.Std.Ltac
 import Katydid.Std.Balistic
diff --git a/Katydid/Expr/Desc.lean b/Katydid/Expr/Desc.lean
index ef00188..03b391d 100644
--- a/Katydid/Expr/Desc.lean
+++ b/Katydid/Expr/Desc.lean
@@ -6,8 +6,6 @@ We want to represent some nested function calls for a very restricted language,
 We represent the description (including AST) of the expr, or as we call it the Descriptor here:
 -/
 
-namespace Desc
-
 inductive Desc where
   | intro
     (name: String)
@@ -16,11 +14,13 @@ inductive Desc where
     (reader: Bool)
   deriving Repr
 
-def Desc.name (desc: Desc): String :=
+namespace Desc
+
+def name (desc: Desc): String :=
   match desc with
   | ⟨ name, _, _, _ ⟩ => name
 
-def Desc.params (desc: Desc): List Desc :=
+def params (desc: Desc): List Desc :=
   match desc with
   | ⟨ _, params, _, _⟩ => params
 
@@ -30,13 +30,13 @@ The `hash` field is important, because it is used to efficiently compare functio
   * and(lt(3, 5), lt(3, 5)) => lt(3, 5)
   * or(and(lt(3, 5), contains("abcd", "bc")), and(contains("abcd", "bc"), lt(3, 5))) => and(contains("abcd", "bc"), lt(3, 5))
 -/
-def hash_list (innit: UInt64) (list: List UInt64): UInt64 :=
+private def hash_list (innit: UInt64) (list: List UInt64): UInt64 :=
   List.foldl (fun acc h => 31 * acc + h) innit list
 
-def hash_string (s: String): UInt64 :=
+private def hash_string (s: String): UInt64 :=
   hash_list 0 (List.map (Nat.toUInt64 ∘ Char.toNat) (String.toList s))
 
-def hash_desc (desc: Desc): UInt64 :=
+private def hash_desc (desc: Desc): UInt64 :=
   match desc with
   | ⟨ name, params, _, _⟩ => hash_list (31 * 17 + hash_string name) (hash_params params)
 where hash_params (params: List Desc): List UInt64 :=
@@ -44,10 +44,10 @@ where hash_params (params: List Desc): List UInt64 :=
   | [] => []
   | param::params => hash_desc param :: hash_params params
 
-def Desc.hash (desc: Desc): UInt64 :=
+def hash (desc: Desc): UInt64 :=
   hash_desc desc
 
-def any_reader (d: Desc): Bool :=
+private def any_reader (d: Desc): Bool :=
   match d with
   | ⟨ _, params, _, _⟩ => any_params params
 where any_params (params: List Desc): Bool :=
@@ -56,7 +56,7 @@ where any_params (params: List Desc): Bool :=
   | param::params => any_reader param || any_params params
 
 /- The reader field tells us whether the function has any variables or can be evaluated at compile time. -/
-def Desc.reader (desc: Desc): Bool :=
+def reader (desc: Desc): Bool :=
   any_reader desc
 
 inductive IsSmart : Desc → Prop
diff --git a/Katydid/Regex/Language.lean b/Katydid/Regex/Language.lean
index 0b2d4df..5541ee2 100644
--- a/Katydid/Regex/Language.lean
+++ b/Katydid/Regex/Language.lean
@@ -256,7 +256,7 @@ def derive_char {α: Type} [DecidableEq α] {a: α} {c: α}:
   funext
   rw [derive_iff_char]
 
-def derive_iff_pred {α: Type} {p: α -> Prop} [dp: DecidablePred p] {x: α} {xs: List α}:
+def derive_iff_pred {α: Type} {p: α -> Prop} {x: α} {xs: List α}:
   (derive (pred p) x) xs <-> (onlyif (p x) emptystr) xs := by
   simp only [derive, derives, singleton_append]
   simp only [onlyif, emptystr]
diff --git a/Katydid/Std/Lists.lean b/Katydid/Std/Lists.lean
index 693bcbd..a2af311 100644
--- a/Katydid/Std/Lists.lean
+++ b/Katydid/Std/Lists.lean
@@ -9,74 +9,11 @@
 
 import Mathlib.Tactic.Linarith
 
+import Katydid.Std.Nat
+
 open Nat
 open List
 
-theorem nat_succ_le_succ_iff (x y: Nat):
-  succ x ≤ succ y <-> x ≤ y := by
-  apply Iff.intro
-  case mp =>
-    apply Nat.le_of_succ_le_succ
-  case mpr =>
-    apply Nat.succ_le_succ
-
-theorem nat_succ_eq_plus_one : succ n = n + 1 := by
-  simp only
-
-theorem nat_pred_le_succ : {n m : Nat} -> Nat.le n (succ m) -> Nat.le (pred n) m
-  | zero, zero, _ => Nat.le.refl
-  | _, _, Nat.le.refl => Nat.le.refl
-  | zero, succ _, Nat.le.step h => h
-  | succ _, succ _, Nat.le.step h => Nat.le_trans (le_succ _) h
-
-theorem nat_pred_le_succ' : {n m : Nat} -> Nat.le n (succ m) -> Nat.le (pred n) m := by
-  intro n m h
-  cases h with
-  | refl =>
-    constructor
-  | step h =>
-    cases n with
-    | zero =>
-      dsimp only [zero_eq, Nat.pred_zero, le_eq]
-      exact h
-    | succ n =>
-      dsimp only [Nat.pred_succ, le_eq]
-      have h_n_le_succ_n := Nat.le_succ n
-      exact (Nat.le_trans h_n_le_succ_n h)
-
-
-theorem nat_min_zero {n: Nat}: min 0 n = 0 :=
-  Nat.min_eq_left (Nat.zero_le _)
-
-theorem nat_zero_min {n: Nat}: min n 0 = 0 :=
-  Nat.min_eq_right (Nat.zero_le _)
-
-theorem nat_add_succ_is_succ_add (n m: Nat): succ n + m = succ (n + m) := by
-  cases n with
-  | zero =>
-    rewrite [Nat.add_comm]
-    simp only [zero_eq, zero_add]
-  | succ n =>
-    rewrite [Nat.add_comm]
-    rewrite [Nat.add_comm (succ n)]
-    repeat rewrite [Nat.add_succ]
-    rfl
-
-theorem nat_pred_le_pred : {n m : Nat} → LE.le n m → LE.le (pred n) (pred m) := by
-  intro n m h
-  cases h with
-  | refl => constructor
-  | step h =>
-    rename_i m
-    cases n with
-    | zero =>
-      dsimp
-      exact h
-    | succ n =>
-      dsimp
-      have h_n_le_succ_n := Nat.le_succ n
-      exact (Nat.le_trans h_n_le_succ_n h)
-
 theorem list_cons_ne_nil (x : α) (xs : List α):
   x :: xs ≠ [] := by
   intro h'
@@ -648,20 +585,6 @@ theorem list_take_drop (n: Nat) (xs: List α):
       apply (congrArg (cons x))
       apply ih
 
-theorem nat_succ_gt_succ {n m: Nat}:
-  succ n > succ m -> n > m := by
-  intro h
-  cases h with
-  | refl =>
-    constructor
-  | step s =>
-    apply Nat.le_of_succ_le_succ
-    exact (Nat.le_succ_of_le s)
-
-theorem nat_succ_gt_succ' {n m: Nat}:
-  succ n > succ m -> n > m := by
-  apply Nat.le_of_succ_le_succ
-
 theorem list_take_large_length {n: Nat} {xs: List α}:
   n > length xs -> length (take n xs) = length xs := by
   revert xs
@@ -990,3 +913,19 @@ theorem list_split_flatten {α: Type} (zs: List α):
   | cons x ys => by
     exists [[x], ys]
     simp
+
+theorem list_splitAt_eq (n: Nat) (xs: List α):
+  splitAt n xs = (xs.take n, xs.drop n) :=
+  splitAt_eq n xs
+
+theorem list_splitAt_length {α: Type} (n: Nat) (xs: List α) (hn: n ≤ length xs):
+  ∃ xs1 xs2, (xs1, xs2) = splitAt n xs
+    /\ xs1.length = n
+    /\ xs2.length = xs.length - n := by
+  have h := splitAt_eq n xs
+  exists take n xs
+  exists drop n xs
+  split_ands
+  · exact (symm (list_splitAt_eq n xs))
+  · exact (list_take_length_le n xs hn)
+  · exact (list_drop_length n xs)
diff --git a/Katydid/Std/Nat.lean b/Katydid/Std/Nat.lean
new file mode 100644
index 0000000..0cabd15
--- /dev/null
+++ b/Katydid/Std/Nat.lean
@@ -0,0 +1,81 @@
+import Mathlib.Tactic.Linarith
+
+open Nat
+
+theorem nat_succ_le_succ_iff (x y: Nat):
+  succ x ≤ succ y <-> x ≤ y := by
+  apply Iff.intro
+  case mp =>
+    apply Nat.le_of_succ_le_succ
+  case mpr =>
+    apply Nat.succ_le_succ
+
+theorem nat_succ_eq_plus_one : succ n = n + 1 := by
+  simp only
+
+theorem nat_pred_le_succ : {n m : Nat} -> Nat.le n (succ m) -> Nat.le (pred n) m
+  | zero, zero, _ => Nat.le.refl
+  | _, _, Nat.le.refl => Nat.le.refl
+  | zero, succ _, Nat.le.step h => h
+  | succ _, succ _, Nat.le.step h => Nat.le_trans (le_succ _) h
+
+theorem nat_pred_le_succ' : {n m : Nat} -> Nat.le n (succ m) -> Nat.le (pred n) m := by
+  intro n m h
+  cases h with
+  | refl =>
+    constructor
+  | step h =>
+    cases n with
+    | zero =>
+      dsimp only [zero_eq, Nat.pred_zero, le_eq]
+      exact h
+    | succ n =>
+      dsimp only [Nat.pred_succ, le_eq]
+      have h_n_le_succ_n := Nat.le_succ n
+      exact (Nat.le_trans h_n_le_succ_n h)
+
+theorem nat_min_zero {n: Nat}: min 0 n = 0 :=
+  Nat.min_eq_left (Nat.zero_le _)
+
+theorem nat_zero_min {n: Nat}: min n 0 = 0 :=
+  Nat.min_eq_right (Nat.zero_le _)
+
+theorem nat_add_succ_is_succ_add (n m: Nat): succ n + m = succ (n + m) := by
+  cases n with
+  | zero =>
+    rewrite [Nat.add_comm]
+    simp only [zero_eq, zero_add]
+  | succ n =>
+    rewrite [Nat.add_comm]
+    rewrite [Nat.add_comm (succ n)]
+    repeat rewrite [Nat.add_succ]
+    rfl
+
+theorem nat_pred_le_pred : {n m : Nat} → LE.le n m → LE.le (pred n) (pred m) := by
+  intro n m h
+  cases h with
+  | refl => constructor
+  | step h =>
+    rename_i m
+    cases n with
+    | zero =>
+      dsimp
+      exact h
+    | succ n =>
+      dsimp
+      have h_n_le_succ_n := Nat.le_succ n
+      exact (Nat.le_trans h_n_le_succ_n h)
+
+theorem nat_succ_gt_succ {n m: Nat}:
+  succ n > succ m -> n > m := by
+  intro h
+  cases h with
+  | refl =>
+    constructor
+  | step s =>
+    apply Nat.le_of_succ_le_succ
+    exact (Nat.le_succ_of_le s)
+
+theorem nat_succ_gt_succ' {n m: Nat}:
+  succ n > succ m -> n > m := by
+  apply Nat.le_of_succ_le_succ