From 04ce8b577e579bab2237d6482c9f440a529348dd Mon Sep 17 00:00:00 2001
From: Walter Schulze <awalterschulze@gmail.com>
Date: Mon, 23 Dec 2024 16:23:28 +0000
Subject: [PATCH] cleanup

---
 Katydid/Regex/IndexedRegex.lean |  3 +++
 Katydid/Regex/Language.lean     |  6 ++++++
 Katydid/Regex/SmartRegex.lean   |  3 +++
 Katydid/Std/Lists.lean          | 22 +++-------------------
 README.md                       |  1 +
 5 files changed, 16 insertions(+), 19 deletions(-)

diff --git a/Katydid/Regex/IndexedRegex.lean b/Katydid/Regex/IndexedRegex.lean
index 9904a54..3fa7590 100644
--- a/Katydid/Regex/IndexedRegex.lean
+++ b/Katydid/Regex/IndexedRegex.lean
@@ -43,6 +43,7 @@ def iso'' {P Q: Language.Lang α} (ifflang: ∀ {xs: List α}, P xs <-> Q xs) (r
 
 -- | scalar {s: Type u}: (Decidability.Dec s) -> Lang P -> Lang (Language.scalar s P)
 def onlyif {cond: Prop} (dcond: Decidable cond) (r: Regex α l): Regex α (Language.onlyif cond l) :=
+-- TODO
   sorry
 
 def derive (r: Regex α l) (a: α): Regex α (Language.derive l a) :=
@@ -51,11 +52,13 @@ def derive (r: Regex α l) (a: α): Regex α (Language.derive l a) :=
   | Regex.emptystr =>
     iso Language.derive_emptystr Regex.emptyset
   | Regex.pred p =>
+    -- TODO
     -- iso Language.derive_pred (onlyif p Regex.emptystr)
     sorry
   | Regex.or x y =>
     iso Language.derive_or (Regex.or (derive x a) (derive y a))
   | Regex.concat x y =>
+    -- TODO
     -- iso Language.derive_concat
     --   (Regex.or
     --     (onlyif (null x) (derive y a))
diff --git a/Katydid/Regex/Language.lean b/Katydid/Regex/Language.lean
index 18ced25..0b686a3 100644
--- a/Katydid/Regex/Language.lean
+++ b/Katydid/Regex/Language.lean
@@ -651,24 +651,28 @@ theorem simp_and_null_l_emptystr_is_l
     | And.intro hr hxs =>
     exact hr
   case mpr =>
+    -- TODO
     sorry
 
 theorem simp_and_emptystr_null_r_is_r
   (r: Lang α)
   (nullr: null r):
   and emptystr r = r := by
+  -- TODO
   sorry
 
 theorem simp_and_not_null_l_emptystr_is_emptyset
   (r: Lang α)
   (notnullr: Not (null r)):
   and r emptystr = emptyset := by
+  -- TODO
   sorry
 
 theorem simp_and_emptystr_not_null_r_is_emptyset
   (r: Lang α)
   (notnullr: Not (null r)):
   and emptystr r = emptyset := by
+  -- TODO
   sorry
 
 theorem simp_and_idemp (r: Lang α):
@@ -755,12 +759,14 @@ theorem simp_and_not_emptystr_l_not_null_r_is_r
   (r: Lang α)
   (notnullr: Not (null r)):
   and (not emptystr) r = r := by
+  -- TODO
   sorry
 
 theorem simp_and_not_null_l_not_emptystr_r_is_l
   (r: Lang α)
   (notnullr: Not (null r)):
   and r (not emptystr) = r := by
+  -- TODO
   sorry
 
 theorem simp_one_r_implies_star_r (r: Lang α) (xs: List α):
diff --git a/Katydid/Regex/SmartRegex.lean b/Katydid/Regex/SmartRegex.lean
index 6ae9e8a..a6abbcb 100644
--- a/Katydid/Regex/SmartRegex.lean
+++ b/Katydid/Regex/SmartRegex.lean
@@ -323,6 +323,7 @@ theorem orToList_is_orFromList (x: Regex α):
   orFromList (orToList x) = x := by
   induction x <;> (try simp [orToList, orFromList])
   · case or x1 x2 ih1 ih2 =>
+    -- TODO
     sorry
 
 -- 1. If x or y is emptyset then return the other (Language.simp_or_emptyset_r_is_l and Language.simp_or_emptyset_l_is_r)
@@ -352,6 +353,7 @@ def smartOr (x y: Regex α): Regex α :=
 
 theorem smartOr_is_or (x y: Regex α):
   denote (Regex.or x y) = denote (smartOr x y) := by
+  -- TODO
   sorry
 
 def derive (r: Regex α) (a: α): Regex α :=
@@ -370,6 +372,7 @@ def derive (r: Regex α) (a: α): Regex α :=
 
 theorem derive_commutes {α: Type} (r: Regex α) (x: α):
   denote (derive r x) = Language.derive (denote r) x := by
+  -- TODO
   sorry
 
 def derives (r: Regex α) (xs: List α): Regex α :=
diff --git a/Katydid/Std/Lists.lean b/Katydid/Std/Lists.lean
index a5c3bea..d62a97e 100644
--- a/Katydid/Std/Lists.lean
+++ b/Katydid/Std/Lists.lean
@@ -1,11 +1,7 @@
--- Lean Tactics
--- https://leanprover.github.io/theorem_proving_in_lean4/tactics.html
--- Lean List Proofs
--- https://github.com/leanprover/std4/blob/main/Std/Data/List/Lemmas.lean
--- Coq List Proofs
+-- This file is based on List Proofs originally done in Coq:
 -- https://github.com/katydid/proofs/blob/old-coq/src/CoqStock/List.v
--- List of Lean Tactics
--- https://github.com/leanprover/lean4/blob/master/src/Init/Tactics.lean
+-- Other Lean List Proofs can be found in:
+-- https://github.com/leanprover/std4/blob/main/Std/Data/List/Lemmas.lean
 
 import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.SplitIfs
@@ -1005,15 +1001,3 @@ theorem list_notin_cons (y: α) (x: α) (xs: List α):
     apply h
     apply Mem.tail
     exact yinxs
-
-theorem list_eraseReps_idemp {α: Type} [BEq α] (x: α) (xs: List α):
-  List.eraseReps (List.eraseReps xs) = List.eraseReps xs := by
-  sorry
-
-theorem list_eraseReps_erases_first_rep {α: Type} [BEq α] (x: α) (xs: List α):
-  List.eraseReps (x::(x::xs)) = List.eraseReps (x::xs) := by
-  sorry
-
-theorem list_eraseReps_does_not_erase_head (α: Type) [BEq α] [LawfulBEq α] (x: α) (xs: List α):
-  ∃ (xs': List α), (x::xs') = List.eraseReps (x::xs) := by
-  sorry
diff --git a/README.md b/README.md
index 044f801..527e176 100644
--- a/README.md
+++ b/README.md
@@ -70,6 +70,7 @@ Optionally the following will also be helpful, but this is not required:
     + [Coq Lean Tactic Cheat Sheet](https://github.com/katydid/coq-lean-cheatsheet/)
     + [Lean Standard Libary Documentation](https://leanprover-community.github.io/mathlib4_docs/Std/Data/HashMap/Basic.html#Std.HashMap)
     + [Lean4 Meta Programming Book](https://github.com/arthurpaulino/lean4-metaprogramming-book)
+    + [Tactic List](https://github.com/haruhisa-enomoto/mathlib4-all-tactics/blob/main/all-tactics.md)
 
 Questions about Lean4 can be asked on [proofassistants.stackexchange](https://proofassistants.stackexchange.com/) by tagging questions with `lean` and `lean4` or in the [Zulip Chat](https://leanprover.zulipchat.com/).