From 4ec021944a896966fcbc75c065b409c99afc0fe5 Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Fri, 17 Jul 2026 16:13:53 -0400 Subject: [PATCH 1/8] feat(StackTape): add scan simp lemmas for mapSome/cons and the empty tape Add simp lemmas describing how `mapSome` and `cons` interact with `head`/`tail` and the empty tape, used for reasoning about a left-to-right tape scan: `mapSome_head`, `mapSome_tail`, `cons_some_mapSome`, `cons_head?_mapSome`, `cons_none_empty`, `mapSome_nil`, `empty_head`, `empty_tail`. Co-Authored-By: Claude Fable 5 --- Cslib/Foundations/Data/StackTape.lean | 29 +++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) diff --git a/Cslib/Foundations/Data/StackTape.lean b/Cslib/Foundations/Data/StackTape.lean index 2cd556ecf..254f23249 100644 --- a/Cslib/Foundations/Data/StackTape.lean +++ b/Cslib/Foundations/Data/StackTape.lean @@ -141,6 +141,35 @@ lemma cons_head_tail (l : StackTape Symbol) : @[scoped grind] def mapSome (l : List Symbol) : StackTape Symbol := ⟨l.map some, by simp⟩ +@[simp] +lemma mapSome_head (l : List Symbol) : (mapSome l).head = l.head? := by + cases l <;> rfl + +@[simp] +lemma mapSome_tail (l : List Symbol) : (mapSome l).tail = mapSome l.tail := by + cases l <;> rfl + +@[simp] +lemma cons_some_mapSome (a : Symbol) (l : List Symbol) : + cons (some a) (mapSome l) = mapSome (a :: l) := rfl + +@[simp] +lemma cons_head?_mapSome (l : List Symbol) : + cons l.head? (mapSome l.tail) = mapSome l := by + cases l <;> rfl + +@[simp] +lemma cons_none_empty : cons none (∅ : StackTape Symbol) = ∅ := rfl + +@[simp] +lemma mapSome_nil : mapSome ([] : List Symbol) = ∅ := rfl + +@[simp] +lemma empty_head : (∅ : StackTape Symbol).head = none := rfl + +@[simp] +lemma empty_tail : (∅ : StackTape Symbol).tail = ∅ := rfl + section Length /-- The length of the `StackTape` is the number of elements up to the last non-`none` element -/ From d009e93a3bf9b0a26fdc5469b19a59321ba0cad1 Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Fri, 17 Jul 2026 16:23:20 -0400 Subject: [PATCH 2/8] sectioning and scope --- Cslib/Foundations/Data/StackTape.lean | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/Cslib/Foundations/Data/StackTape.lean b/Cslib/Foundations/Data/StackTape.lean index 254f23249..7b47ad2a1 100644 --- a/Cslib/Foundations/Data/StackTape.lean +++ b/Cslib/Foundations/Data/StackTape.lean @@ -137,6 +137,8 @@ lemma cons_head_tail (l : StackTape Symbol) : rw [eq_iff] simp +section mapSome + /-- Create a `StackTape` from a list by mapping all elements to `some` -/ @[scoped grind] def mapSome (l : List Symbol) : StackTape Symbol := ⟨l.map some, by simp⟩ @@ -158,17 +160,10 @@ lemma cons_head?_mapSome (l : List Symbol) : cons l.head? (mapSome l.tail) = mapSome l := by cases l <;> rfl -@[simp] -lemma cons_none_empty : cons none (∅ : StackTape Symbol) = ∅ := rfl - @[simp] lemma mapSome_nil : mapSome ([] : List Symbol) = ∅ := rfl -@[simp] -lemma empty_head : (∅ : StackTape Symbol).head = none := rfl - -@[simp] -lemma empty_tail : (∅ : StackTape Symbol).tail = ∅ := rfl +end mapSome section Length From 3a06bc52f351195e105356d1ccdabb635ca39613 Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Fri, 17 Jul 2026 16:35:05 -0400 Subject: [PATCH 3/8] simp choice --- Cslib/Foundations/Data/StackTape.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Cslib/Foundations/Data/StackTape.lean b/Cslib/Foundations/Data/StackTape.lean index 7b47ad2a1..c28d72b25 100644 --- a/Cslib/Foundations/Data/StackTape.lean +++ b/Cslib/Foundations/Data/StackTape.lean @@ -151,7 +151,6 @@ lemma mapSome_head (l : List Symbol) : (mapSome l).head = l.head? := by lemma mapSome_tail (l : List Symbol) : (mapSome l).tail = mapSome l.tail := by cases l <;> rfl -@[simp] lemma cons_some_mapSome (a : Symbol) (l : List Symbol) : cons (some a) (mapSome l) = mapSome (a :: l) := rfl From 6ed5072c5b191ecde59f2f7919ab5c3a96f9b0b8 Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Sat, 1 Aug 2026 18:45:53 -0700 Subject: [PATCH 4/8] simp normal form --- Cslib/Foundations/Data/StackTape.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cslib/Foundations/Data/StackTape.lean b/Cslib/Foundations/Data/StackTape.lean index c28d72b25..3ba130175 100644 --- a/Cslib/Foundations/Data/StackTape.lean +++ b/Cslib/Foundations/Data/StackTape.lean @@ -160,7 +160,7 @@ lemma cons_head?_mapSome (l : List Symbol) : cases l <;> rfl @[simp] -lemma mapSome_nil : mapSome ([] : List Symbol) = ∅ := rfl +lemma mapSome_nil : mapSome ([] : List Symbol) = nil := rfl end mapSome From 567e02d9b09635a4934f08510f25302a51c17f9d Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Sat, 1 Aug 2026 19:54:23 -0700 Subject: [PATCH 5/8] reorg grind lemmas --- Cslib/Foundations/Data/StackTape.lean | 30 ++++++++++++++++++--------- 1 file changed, 20 insertions(+), 10 deletions(-) diff --git a/Cslib/Foundations/Data/StackTape.lean b/Cslib/Foundations/Data/StackTape.lean index 3ba130175..da4dd194c 100644 --- a/Cslib/Foundations/Data/StackTape.lean +++ b/Cslib/Foundations/Data/StackTape.lean @@ -70,7 +70,7 @@ instance : Inhabited (StackTape Symbol) where instance : EmptyCollection (StackTape Symbol) := ⟨nil⟩ -@[simp] +@[simp, scoped grind =] lemma empty_eq_nil : (∅ : StackTape Symbol) = nil := rfl @[simp, scoped grind =] @@ -83,6 +83,9 @@ def cons (x : Option Symbol) (xs : StackTape Symbol) : StackTape Symbol := | none, ⟨hd :: tl, hl⟩ => ⟨none :: hd :: tl, by grind⟩ | some a, ⟨l, hl⟩ => ⟨some a :: l, by grind⟩ +@[simp, scoped grind =] +lemma cons_none_nil : cons none (nil : StackTape Symbol) = nil := rfl + @[simp, scoped grind =] lemma cons_none_nil_toList : (cons none (nil : StackTape Symbol)).toList = [] := by grind only [nil, cons] @@ -137,32 +140,39 @@ lemma cons_head_tail (l : StackTape Symbol) : rw [eq_iff] simp -section mapSome +section MapSome /-- Create a `StackTape` from a list by mapping all elements to `some` -/ -@[scoped grind] def mapSome (l : List Symbol) : StackTape Symbol := ⟨l.map some, by simp⟩ -@[simp] -lemma mapSome_head (l : List Symbol) : (mapSome l).head = l.head? := by +@[scoped grind =] +lemma toList_mapSome (l : List Symbol) : (mapSome l).toList = l.map some := rfl + +@[scoped grind =] +lemma head_mapSome (l : List Symbol) : (mapSome l).head = l.head? := by cases l <;> rfl -@[simp] -lemma mapSome_tail (l : List Symbol) : (mapSome l).tail = mapSome l.tail := by +@[scoped grind =] +lemma tail_mapSome (l : List Symbol) : (mapSome l).tail = mapSome l.tail := by cases l <;> rfl +@[scoped grind =] +lemma mapSome_cons (a : Symbol) (l : List Symbol) : + mapSome (a :: l) = cons (some a) (mapSome l) := rfl + +@[scoped grind =] lemma cons_some_mapSome (a : Symbol) (l : List Symbol) : cons (some a) (mapSome l) = mapSome (a :: l) := rfl -@[simp] +@[scoped grind =] lemma cons_head?_mapSome (l : List Symbol) : cons l.head? (mapSome l.tail) = mapSome l := by cases l <;> rfl -@[simp] +@[scoped grind =] lemma mapSome_nil : mapSome ([] : List Symbol) = nil := rfl -end mapSome +end MapSome section Length From 98acba6b64cc1b5e7ee8adeddb8665d1c64bdb28 Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Sat, 1 Aug 2026 20:21:24 -0700 Subject: [PATCH 6/8] remove redundant lemmas --- Cslib/Foundations/Data/StackTape.lean | 8 -------- 1 file changed, 8 deletions(-) diff --git a/Cslib/Foundations/Data/StackTape.lean b/Cslib/Foundations/Data/StackTape.lean index da4dd194c..be4476f74 100644 --- a/Cslib/Foundations/Data/StackTape.lean +++ b/Cslib/Foundations/Data/StackTape.lean @@ -86,10 +86,6 @@ def cons (x : Option Symbol) (xs : StackTape Symbol) : StackTape Symbol := @[simp, scoped grind =] lemma cons_none_nil : cons none (nil : StackTape Symbol) = nil := rfl -@[simp, scoped grind =] -lemma cons_none_nil_toList : (cons none (nil : StackTape Symbol)).toList = [] := by - grind only [nil, cons] - @[simp] lemma cons_some_toList (a : Symbol) (l : StackTape Symbol) : (cons (some a) l).toList = some a :: l.toList := by simp only [cons] @@ -160,10 +156,6 @@ lemma tail_mapSome (l : List Symbol) : (mapSome l).tail = mapSome l.tail := by lemma mapSome_cons (a : Symbol) (l : List Symbol) : mapSome (a :: l) = cons (some a) (mapSome l) := rfl -@[scoped grind =] -lemma cons_some_mapSome (a : Symbol) (l : List Symbol) : - cons (some a) (mapSome l) = mapSome (a :: l) := rfl - @[scoped grind =] lemma cons_head?_mapSome (l : List Symbol) : cons l.head? (mapSome l.tail) = mapSome l := by From 8056328608d79c27a397e1b8a6db6bb35ecc34cc Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Sat, 1 Aug 2026 20:43:08 -0700 Subject: [PATCH 7/8] readd simp lemmas --- Cslib/Foundations/Data/StackTape.lean | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/Cslib/Foundations/Data/StackTape.lean b/Cslib/Foundations/Data/StackTape.lean index be4476f74..a021ea617 100644 --- a/Cslib/Foundations/Data/StackTape.lean +++ b/Cslib/Foundations/Data/StackTape.lean @@ -86,6 +86,9 @@ def cons (x : Option Symbol) (xs : StackTape Symbol) : StackTape Symbol := @[simp, scoped grind =] lemma cons_none_nil : cons none (nil : StackTape Symbol) = nil := rfl +lemma cons_none_nil_toList : (cons none (nil : StackTape Symbol)).toList = [] := by + simp + @[simp] lemma cons_some_toList (a : Symbol) (l : StackTape Symbol) : (cons (some a) l).toList = some a :: l.toList := by simp only [cons] @@ -141,10 +144,10 @@ section MapSome /-- Create a `StackTape` from a list by mapping all elements to `some` -/ def mapSome (l : List Symbol) : StackTape Symbol := ⟨l.map some, by simp⟩ -@[scoped grind =] +@[simp, scoped grind =] lemma toList_mapSome (l : List Symbol) : (mapSome l).toList = l.map some := rfl -@[scoped grind =] +@[simp, scoped grind =] lemma head_mapSome (l : List Symbol) : (mapSome l).head = l.head? := by cases l <;> rfl @@ -156,7 +159,7 @@ lemma tail_mapSome (l : List Symbol) : (mapSome l).tail = mapSome l.tail := by lemma mapSome_cons (a : Symbol) (l : List Symbol) : mapSome (a :: l) = cons (some a) (mapSome l) := rfl -@[scoped grind =] +@[simp, scoped grind =] lemma cons_head?_mapSome (l : List Symbol) : cons l.head? (mapSome l.tail) = mapSome l := by cases l <;> rfl From 666c6612baef13c55de172b276ba93f2379937ab Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Sat, 1 Aug 2026 20:49:39 -0700 Subject: [PATCH 8/8] more material --- Cslib/Foundations/Data/StackTape.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Cslib/Foundations/Data/StackTape.lean b/Cslib/Foundations/Data/StackTape.lean index a021ea617..a9e8de88b 100644 --- a/Cslib/Foundations/Data/StackTape.lean +++ b/Cslib/Foundations/Data/StackTape.lean @@ -167,6 +167,10 @@ lemma cons_head?_mapSome (l : List Symbol) : @[scoped grind =] lemma mapSome_nil : mapSome ([] : List Symbol) = nil := rfl +@[simp, scoped grind =] +lemma mapSome_eq_nil_iff (l : List Symbol) : mapSome l = nil ↔ l = [] := by + cases l <;> simp [mapSome, nil] + end MapSome section Length