From 97452e67b05248c229305b7a3a30fcc38e8b2242 Mon Sep 17 00:00:00 2001 From: Ching-Tsun Chou Date: Wed, 24 Dec 2025 15:43:34 -0800 Subject: [PATCH 1/2] feat: prove that regular languages are closed under concatenation --- Cslib.lean | 1 + Cslib/Computability/Automata/NA/Concat.lean | 74 ++++++++++-- Cslib/Computability/Automata/NA/Total.lean | 61 ++++++++++ .../Languages/RegularLanguage.lean | 22 ++++ Cslib/Foundations/Semantics/LTS/Basic.lean | 111 +++++++++++++++++- 5 files changed, 254 insertions(+), 15 deletions(-) create mode 100644 Cslib/Computability/Automata/NA/Total.lean diff --git a/Cslib.lean b/Cslib.lean index 249bd723..e87cc1a6 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -16,6 +16,7 @@ import Cslib.Computability.Automata.NA.Hist import Cslib.Computability.Automata.NA.Prod import Cslib.Computability.Automata.NA.Sum import Cslib.Computability.Automata.NA.ToDA +import Cslib.Computability.Automata.NA.Total import Cslib.Computability.Languages.ExampleEventuallyZero import Cslib.Computability.Languages.Language import Cslib.Computability.Languages.OmegaLanguage diff --git a/Cslib/Computability/Automata/NA/Concat.lean b/Cslib/Computability/Automata/NA/Concat.lean index 3a1b29d6..b4aec46b 100644 --- a/Cslib/Computability/Automata/NA/Concat.lean +++ b/Cslib/Computability/Automata/NA/Concat.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Ching-Tsun Chou -/ -import Cslib.Computability.Automata.NA.Basic +import Cslib.Computability.Automata.NA.Total import Cslib.Foundations.Data.OmegaSequence.Temporal /-! # Concatenation of nondeterministic automata. -/ @@ -74,17 +74,19 @@ lemma concat_run_right {xs : ωSequence Symbol} {ss : ωSequence (State1 ⊕ Sta /-- A run of `concat na1 na2` containing at least one `na2` state is the concatenation of an accepting finite run of `na1` followed by a run of `na2`. -/ -theorem concat_run_proj {xs : ωSequence Symbol} {ss : ωSequence (State1 ⊕ State2)} - (hc : (concat na1 na2).Run xs ss) (hr : ∃ k, (ss k).isRight) : - ∃ n, xs.take n ∈ language na1 ∧ ∃ ss2, na2.Run (xs.drop n) ss2 ∧ ss.drop n = ss2.map inr := by - let n := Nat.find hr - have hl (k) (h_k : k < n) := not_isRight.mp <| Nat.find_min hr h_k - refine ⟨n, ?_, ?_⟩ +theorem concat_run_proj {xs : ωSequence Symbol} {ss : ωSequence (State1 ⊕ State2)} {k : ℕ} + (hc : (concat na1 na2).Run xs ss) (hr : (ss k).isRight) : + ∃ n, n ≤ k ∧ xs.take n ∈ language na1 ∧ + ∃ ss2, na2.Run (xs.drop n) ss2 ∧ ss.drop n = ss2.map inr := by + have hr' : ∃ k, (ss k).isRight := by grind + let n := Nat.find hr' + have hl (k) (h_k : k < n) := not_isRight.mp <| Nat.find_min hr' h_k + refine ⟨n, by grind, ?_, ?_⟩ · by_cases h_n : n = 0 · grind [concat_start_right] · grind [concat_run_left_right] - · have hr : (ss n).isRight := Nat.find_spec hr - grind [concat_run_right hc n hl hr] + · have hr'' : (ss n).isRight := Nat.find_spec hr' + grind [concat_run_right hc n hl hr''] /-- Given an accepting finite run of `na1` and a run of `na2`, there exists a run of `concat na1 na2` that is the concatenation of the two runs. -/ @@ -117,8 +119,8 @@ theorem concat_language_eq {acc2 : Set State2} : ext xs constructor · rintro ⟨ss, h_run, h_acc⟩ - have h_ex2 : ∃ k, (ss k).isRight := by grind [Frequently.exists h_acc] - obtain ⟨n, h_acc1, ss2, h_run2, h_map2⟩ := concat_run_proj h_run h_ex2 + obtain ⟨k, h_k⟩ : ∃ k, (ss k).isRight := by grind [Frequently.exists h_acc] + obtain ⟨n, _, h_acc1, ss2, h_run2, h_map2⟩ := concat_run_proj h_run h_k use xs.take n, h_acc1, xs.drop n, ?_, by simp use ss2, h_run2 grind [(drop_frequently_iff_frequently n).mpr h_acc] @@ -130,4 +132,54 @@ theorem concat_language_eq {acc2 : Set State2} : end Buchi +namespace FinAcc + +/-- `finConcat na1 na2` is the concatenation of the "totalized" versions of `na1` and `na2`. -/ +def finConcat (na1 : FinAcc State1 Symbol) (na2 : FinAcc State2 Symbol) + : NA ((State1 ⊕ Unit) ⊕ (State2 ⊕ Unit)) Symbol := + concat ⟨na1.totalize, inl '' na1.accept⟩ na2.totalize + +variable {na1 : FinAcc State1 Symbol} {na2 : FinAcc State2 Symbol} + +/-- `finConcat na1 na2` is total. -/ +def finConcat_total : (finConcat na1 na2).Total where + next s x := match s with + | inl s1 => inl (inr ()) + | inr s2 => inr (inr ()) + total s x := by + cases s <;> simp [finConcat, concat, NA.totalize, LTS.totalize] + +/-- `finConcat na1 na2` accepts the concatenation of the languages of `na1` and `na2`. -/ +theorem finConcat_language_eq [Inhabited Symbol] : + language (FinAcc.mk (finConcat na1 na2) (inr '' (inl '' na2.accept))) = + language na1 * language na2 := by + ext xl + constructor + · rintro ⟨s, _, t, h_acc, h_mtr⟩ + obtain ⟨xs, ss, h_ωtr, rfl, rfl⟩ := LTS.Total.mTr_ωTr finConcat_total h_mtr + have hc : (finConcat na1 na2).Run (xl ++ω xs) ss := by grind [Run.mk] + have hr : (ss xl.length).isRight := by grind + obtain ⟨n, _, _, ss2, h_run2, _⟩ := concat_run_proj hc hr + refine ⟨xl.take n, ?_, xl.drop n, ?_, by simp⟩ + · grind [totalize_language_eq, take_append_of_le_length] + · have : ss xl.length = (ss.drop n) (xl.length - n) := by grind + have : ss xl.length = inr (ss2 (xl.length - n)) := by grind + have hl : (ss2 (xl.length - n)).isLeft := by grind + obtain ⟨s2, t2, h_mtr2, _, _, _⟩ := totalize_run_mtr h_run2 hl + refine ⟨s2, ?_, t2, ?_, ?_⟩ <;> grind [drop_append_of_le_length, take_append_of_le_length] + · rintro ⟨xl1, h_xl1, xl2, h_xl2, rfl⟩ + rw [← totalize_language_eq] at h_xl1 + obtain ⟨s2, h_s2, t2, h_t2, h_mtr2⟩ := h_xl2 + obtain ⟨xs2, ss2, h_run2, _, _⟩ := totalize_mtr_run h_s2 h_mtr2 + obtain ⟨ss, ⟨h_start, h_ωtr⟩, _⟩ := concat_run_exists h_xl1 h_run2 + have h_mtr := LTS.ωTr_mTr h_ωtr (zero_le (xl1.length + xl2.length)) + simp [← append_append_ωSequence, extract_eq_drop_take, + take_append_of_le_length, ← List.length_append] at h_mtr + have : ss (xl1.length + xl2.length) = (ss.drop xl1.length) xl2.length := by grind + have : ss (xl1.length + xl2.length) = inr (ss2 xl2.length) := by grind + refine ⟨ss 0, ?_, ss (xl1.length + xl2.length), ?_, ?_⟩ <;> + grind [finConcat, List.length_append] + +end FinAcc + end Cslib.Automata.NA diff --git a/Cslib/Computability/Automata/NA/Total.lean b/Cslib/Computability/Automata/NA/Total.lean new file mode 100644 index 00000000..76bdb7da --- /dev/null +++ b/Cslib/Computability/Automata/NA/Total.lean @@ -0,0 +1,61 @@ +/- +Copyright (c) 2025 Ching-Tsun Chou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Ching-Tsun Chou +-/ + +import Cslib.Computability.Automata.NA.Basic + +/-! # Making a nondeterministic automaton total. +-/ + +namespace Cslib.Automata.NA + +open Sum ωSequence Acceptor + +variable {Symbol State : Type*} + +/-- `NA.totalize` makes the original NA total by replacing its LTS with `LTS.totalize` +and its starting states with their lifted non-sink versions. -/ +def totalize (na : NA State Symbol) : NA (State ⊕ Unit) Symbol where + toLTS := na.toLTS.totalize + start := inl '' na.start + +variable {na : NA State Symbol} + +/-- In an infinite execution of `NA.totalize`, as long as the NA stays in a non-sink state, +the execution so far corresponds to a finite execution of the original NA. -/ +theorem totalize_run_mtr {xs : ωSequence Symbol} {ss : ωSequence (State ⊕ Unit)} {n : ℕ} + (h : na.totalize.Run xs ss) (hl : (ss n).isLeft) : + ∃ s t, na.MTr s (xs.take n) t ∧ s ∈ na.start ∧ ss 0 = inl s ∧ ss n = inl t := by + obtain ⟨s, _, _⟩ := h.start + obtain ⟨t, _⟩ := isLeft_iff.mp hl + use s, t + refine ⟨?_, by grind⟩ + rw [← LTS.totalize.mtr_left_iff, ← extract_eq_take] + have := LTS.ωTr_mTr h.trans (show 0 ≤ n by grind) + simp_all only + assumption + +/-- Any finite execution of the original NA can be extended to an infinite execution of +`NA.totalize`, provided that the alphabet is inbabited. -/ +theorem totalize_mtr_run [Inhabited Symbol] {xl : List Symbol} {s t : State} + (hs : s ∈ na.start) (hm : na.MTr s xl t) : + ∃ xs ss, na.totalize.Run (xl ++ω xs) ss ∧ ss 0 = inl s ∧ ss xl.length = inl t := by + obtain ⟨xs, ss, _⟩ := LTS.Total.mTr_ωTr + (LTS.totalize.total na.toLTS) (LTS.totalize.mtr_left_iff.mpr hm) + use xs, ss + grind [totalize, Run.mk] + +namespace FinAcc + +/-- `NA.totalize` and the original NA accept the same language of finite words, +as long as the accepting states are also lifted in the obvious way. -/ +theorem totalize_language_eq {na : FinAcc State Symbol} : + language (FinAcc.mk na.totalize (inl '' na.accept)) = language na := by + ext xl + simp [totalize] + +end FinAcc + +end Cslib.Automata.NA diff --git a/Cslib/Computability/Languages/RegularLanguage.lean b/Cslib/Computability/Languages/RegularLanguage.lean index c7d01175..18d9ae20 100644 --- a/Cslib/Computability/Languages/RegularLanguage.lean +++ b/Cslib/Computability/Languages/RegularLanguage.lean @@ -6,8 +6,10 @@ Authors: Ching-Tsun Chou import Cslib.Computability.Automata.DA.Prod import Cslib.Computability.Automata.DA.ToNA +import Cslib.Computability.Automata.NA.Concat import Cslib.Computability.Automata.NA.ToDA import Mathlib.Computability.DFA +import Mathlib.Data.Finite.Sum import Mathlib.Data.Set.Card import Mathlib.Tactic.Common @@ -49,12 +51,14 @@ theorem IsRegular.iff_nfa {l : Language Symbol} : use Set State, inferInstance, na.toDAFinAcc grind +/-- The complementation of a regular language is regular. -/ theorem IsRegular.compl {l : Language Symbol} (h : l.IsRegular) : (lᶜ).IsRegular := by rw [IsRegular.iff_dfa] at h ⊢ obtain ⟨State, _, ⟨da, acc⟩, rfl⟩ := h use State, inferInstance, ⟨da, accᶜ⟩ grind +/-- The empty language is regular. -/ @[simp] theorem IsRegular.zero : (0 : Language Symbol).IsRegular := by rw [IsRegular.iff_dfa] @@ -62,6 +66,7 @@ theorem IsRegular.zero : (0 : Language Symbol).IsRegular := by use Unit, inferInstance, ⟨DA.mk flts (), ∅⟩ grind +/-- The language containing only the empty word is regular. -/ @[simp] theorem IsRegular.one : (1 : Language Symbol).IsRegular := by rw [IsRegular.iff_dfa] @@ -73,11 +78,13 @@ theorem IsRegular.one : (1 : Language Symbol).IsRegular := by grind · grind [Language.mem_one] +/-- The language of all finite words is regular. -/ @[simp] theorem IsRegular.top : (⊤ : Language Symbol).IsRegular := by have : (⊥ᶜ : Language Symbol).IsRegular := IsRegular.compl <| IsRegular.zero rwa [← compl_bot] +/-- The intersection of two regular languages is regular. -/ @[simp] theorem IsRegular.inf {l1 l2 : Language Symbol} (h1 : l1.IsRegular) (h2 : l2.IsRegular) : (l1 ⊓ l2).IsRegular := by @@ -87,6 +94,7 @@ theorem IsRegular.inf {l1 l2 : Language Symbol} use State1 × State2, inferInstance, ⟨da1.prod da2, fst ⁻¹' acc1 ∩ snd ⁻¹' acc2⟩ ext; grind [Language.mem_inf] +/-- The union of two regular languages is regular. -/ @[simp] theorem IsRegular.add {l1 l2 : Language Symbol} (h1 : l1.IsRegular) (h2 : l2.IsRegular) : (l1 + l2).IsRegular := by @@ -96,6 +104,7 @@ theorem IsRegular.add {l1 l2 : Language Symbol} use State1 × State2, inferInstance, ⟨da1.prod da2, fst ⁻¹' acc1 ∪ snd ⁻¹' acc2⟩ ext; grind [Language.mem_add] +/-- The intersection of any finite number of regular languages is regular. -/ @[simp] theorem IsRegular.iInf {I : Type*} [Finite I] {s : Set I} {l : I → Language Symbol} (h : ∀ i ∈ s, (l i).IsRegular) : (⨅ i ∈ s, l i).IsRegular := by @@ -107,6 +116,7 @@ theorem IsRegular.iInf {I : Type*} [Finite I] {s : Set I} {l : I → Language Sy rw [iInf_insert] grind [IsRegular.inf] +/-- The union of any finite number of regular languages is regular. -/ @[simp] theorem IsRegular.iSup {I : Type*} [Finite I] {s : Set I} {l : I → Language Symbol} (h : ∀ i ∈ s, (l i).IsRegular) : (⨆ i ∈ s, l i).IsRegular := by @@ -121,4 +131,16 @@ theorem IsRegular.iSup {I : Type*} [Finite I] {s : Set I} {l : I → Language Sy rw [iSup_insert] apply IsRegular.add <;> grind +open NA.FinAcc Sum in +/-- The concatenation of two regular languages is regular. -/ +@[simp] +theorem IsRegular.mul [Inhabited Symbol] {l1 l2 : Language Symbol} + (h1 : l1.IsRegular) (h2 : l2.IsRegular) : (l1 * l2).IsRegular := by + rw [IsRegular.iff_nfa] at h1 h2 ⊢ + obtain ⟨State1, h_fin1, nfa1, rfl⟩ := h1 + obtain ⟨State2, h_fin1, nfa2, rfl⟩ := h2 + use (State1 ⊕ Unit) ⊕ (State2 ⊕ Unit), inferInstance, + ⟨finConcat nfa1 nfa2, inr '' (inl '' nfa2.accept)⟩ + rw [finConcat_language_eq] + end Cslib.Language diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean index e29c98c8..a05bed75 100644 --- a/Cslib/Foundations/Semantics/LTS/Basic.lean +++ b/Cslib/Foundations/Semantics/LTS/Basic.lean @@ -239,7 +239,7 @@ variable {lts : LTS State Label} open scoped ωSequence in /-- Any finite execution extracted from an infinite execution is valid. -/ -theorem LTS.ωTr_mTr {n m : ℕ} {hnm : n ≤ m} (h : lts.ωTr ss μs) : +theorem LTS.ωTr_mTr (h : lts.ωTr ss μs) {n m : ℕ} (hnm : n ≤ m) : lts.MTr (ss n) (μs.extract n m) (ss m) := by by_cases heq : n = m case pos => grind @@ -250,16 +250,119 @@ theorem LTS.ωTr_mTr {n m : ℕ} {hnm : n ≤ m} (h : lts.ωTr ss μs) : have : lts.MTr (ss n) (μs.extract n m) (ss m) := ωTr_mTr (hnm := by grind) h grind [MTr.comp] -open scoped ωSequence +open ωSequence /-- Prepends an infinite execution with a transition. -/ -theorem LTS.ωTr.cons (hmtr : lts.Tr s1 μ s2) (hωtr : lts.ωTr ss μs) (hm : ss 0 = s2) : - lts.ωTr (s1 ::ω ss) (μ ::ω μs) := by +theorem LTS.ωTr.cons (htr : lts.Tr s μ t) (hωtr : lts.ωTr ss μs) (hm : ss 0 = t) : + lts.ωTr (s ::ω ss) (μ ::ω μs) := by intro i induction i <;> grind +/-- Prepends an infinite execution with a finite execution. -/ +theorem LTS.ωTr.append (hmtr : lts.MTr s μl t) (hωtr : lts.ωTr ss μs) + (hm : ss 0 = t) : ∃ ss', lts.ωTr ss' (μl ++ω μs) ∧ ss' 0 = s ∧ ss' μl.length = t := by + obtain ⟨sl, _, _, _, _⟩ := LTS.MTr.exists_states hmtr + refine ⟨sl ++ω ss.drop 1, ?_, by grind [get_append_left], by grind [get_append_left]⟩ + intro n + by_cases n < μl.length + · grind [get_append_left] + · by_cases n = μl.length + · grind [get_append_left] + · grind [get_append_right', hωtr (n - μl.length - 1)] + end ωMultiStep +section Total + +/-! ## Total LTS + +A LTS is total iff every state has a transition for every label. +-/ + +open Sum ωSequence + +variable {State Label : Type*} {lts : LTS State Label} + +/-- `LTS.Total` provides a witness that the LTS is total. -/ +structure LTS.Total (lts : LTS State Label) where + /-- `next` rovides a next state for any given starting state and label. -/ + next : State → Label → State + /-- A proof that the state provided by `next` indeed forms a legal transition. -/ + total s μ : lts.Tr s μ (next s μ) + +/-- `LTS.makeωTr` builds an infinite execution of a total LTS from any starting state and +any infinite sequence of labels. -/ +def LTS.makeωTr (lts : LTS State Label) (h : lts.Total) + (s : State) (μs : ωSequence Label) : ℕ → State + | 0 => s + | n + 1 => h.next (lts.makeωTr h s μs n) (μs n) + +/-- If a LTS is total, then there exists an infinite execution from any starting state and +over any infinite sequence of labels. -/ +theorem LTS.Total.ωTr_exists (h : lts.Total) (s : State) (μs : ωSequence Label) : + ∃ ss, lts.ωTr ss μs ∧ ss 0 = s := by + use lts.makeωTr h s μs + grind [LTS.makeωTr, h.total] + +/-- If a LTS is total, then any finite execution can be extended to an infinite execution, +provided that the label type is inbabited. -/ +theorem LTS.Total.mTr_ωTr [Inhabited Label] (ht : lts.Total) {μl : List Label} {s t : State} + (hm : lts.MTr s μl t) : ∃ μs ss, lts.ωTr ss (μl ++ω μs) ∧ ss 0 = s ∧ ss μl.length = t := by + let μs : ωSequence Label := .const default + obtain ⟨ss', ho, h0⟩ := LTS.Total.ωTr_exists ht t μs + refine ⟨μs, LTS.ωTr.append hm ho h0⟩ + +/-- `LTS.totalize` constructs a total LTS from any given LTS by adding a sink state. -/ +def LTS.totalize (lts : LTS State Label) : LTS (State ⊕ Unit) Label where + Tr s' μ t' := match s', t' with + | inl s, inl t => lts.Tr s μ t + | _, inr () => True + | inr (), inl _ => False + +/-- The LTS constructed by `LTS.totalize` is indeed total. -/ +def LTS.totalize.total (lts : LTS State Label) : lts.totalize.Total where + next _ _ := inr () + total _ _ := by simp [LTS.totalize] + +/-- In `LTS.totalize`, there is no finite execution from the sink state to any non-sink state. -/ +theorem LTS.totalize.not_right_left {μs : List Label} {t : State} : + ¬ lts.totalize.MTr (inr ()) μs (inl t) := by + intro h + generalize h_s : (inr () : State ⊕ Unit) = s' + generalize h_t : (inl t : State ⊕ Unit) = t' + rw [h_s, h_t] at h + induction h <;> grind [LTS.totalize] + +/-- In `LTS.totalize`, the transitions between non-sink states correspond exactly to +the transitions in the original LTS. -/ +@[simp] +theorem LTS.totalize.tr_left_iff {μ : Label} {s t : State} : + lts.totalize.Tr (inl s) μ (inl t) ↔ lts.Tr s μ t := by + simp [LTS.totalize] + +/-- In `LTS.totalize`, the multistep transitions between non-sink states correspond exactly to +the multistep transitions in the original LTS. -/ +@[simp] +theorem LTS.totalize.mtr_left_iff {μs : List Label} {s t : State} : + lts.totalize.MTr (inl s) μs (inl t) ↔ lts.MTr s μs t := by + constructor <;> intro h + · generalize h_s : (inl s : State ⊕ Unit) = s' + generalize h_t : (inl t : State ⊕ Unit) = t' + rw [h_s, h_t] at h + induction h generalizing s + case refl _ => grind [LTS.MTr] + case stepL t1' μ t2' μs t3' h_tr h_mtr h_ind => + obtain ⟨rfl⟩ := h_s + cases t2' + case inl t2 => grind [LTS.MTr, totalize.tr_left_iff.mp h_tr] + case inr t2 => grind [totalize.not_right_left] + · induction h + case refl _ => grind [LTS.MTr] + case stepL t1 μ t2 μs t3 h_tr h_mtr h_ind => + grind [LTS.MTr, totalize.tr_left_iff.mpr h_tr] + +end Total + section Termination /-! ## Definitions about termination -/ From e2074b2ee9853c531f322cb09b0c26db9ddd31c3 Mon Sep 17 00:00:00 2001 From: Ching-Tsun Chou Date: Sun, 28 Dec 2025 13:59:26 -0800 Subject: [PATCH 2/2] incorporate Chris Henson's comments --- Cslib/Computability/Automata/NA/Concat.lean | 36 ++++++++----------- Cslib/Computability/Automata/NA/Total.lean | 16 ++++----- .../Languages/RegularLanguage.lean | 2 +- 3 files changed, 22 insertions(+), 32 deletions(-) diff --git a/Cslib/Computability/Automata/NA/Concat.lean b/Cslib/Computability/Automata/NA/Concat.lean index b4aec46b..e677a81d 100644 --- a/Cslib/Computability/Automata/NA/Concat.lean +++ b/Cslib/Computability/Automata/NA/Concat.lean @@ -85,8 +85,7 @@ theorem concat_run_proj {xs : ωSequence Symbol} {ss : ωSequence (State1 ⊕ St · by_cases h_n : n = 0 · grind [concat_start_right] · grind [concat_run_left_right] - · have hr'' : (ss n).isRight := Nat.find_spec hr' - grind [concat_run_right hc n hl hr''] + · exact concat_run_right hc n hl (Nat.find_spec hr') /-- Given an accepting finite run of `na1` and a run of `na2`, there exists a run of `concat na1 na2` that is the concatenation of the two runs. -/ @@ -146,8 +145,7 @@ def finConcat_total : (finConcat na1 na2).Total where next s x := match s with | inl s1 => inl (inr ()) | inr s2 => inr (inr ()) - total s x := by - cases s <;> simp [finConcat, concat, NA.totalize, LTS.totalize] + total s x := by grind [finConcat, concat, NA.totalize, LTS.totalize] /-- `finConcat na1 na2` accepts the concatenation of the languages of `na1` and `na2`. -/ theorem finConcat_language_eq [Inhabited Symbol] : @@ -157,28 +155,24 @@ theorem finConcat_language_eq [Inhabited Symbol] : constructor · rintro ⟨s, _, t, h_acc, h_mtr⟩ obtain ⟨xs, ss, h_ωtr, rfl, rfl⟩ := LTS.Total.mTr_ωTr finConcat_total h_mtr - have hc : (finConcat na1 na2).Run (xl ++ω xs) ss := by grind [Run.mk] + have hc : (finConcat na1 na2).Run (xl ++ω xs) ss := by grind [Run] have hr : (ss xl.length).isRight := by grind - obtain ⟨n, _, _, ss2, h_run2, _⟩ := concat_run_proj hc hr - refine ⟨xl.take n, ?_, xl.drop n, ?_, by simp⟩ + obtain ⟨n, _⟩ := concat_run_proj hc hr + refine ⟨xl.take n, ?_, xl.drop n, ?_, ?_⟩ · grind [totalize_language_eq, take_append_of_le_length] · have : ss xl.length = (ss.drop n) (xl.length - n) := by grind - have : ss xl.length = inr (ss2 (xl.length - n)) := by grind - have hl : (ss2 (xl.length - n)).isLeft := by grind - obtain ⟨s2, t2, h_mtr2, _, _, _⟩ := totalize_run_mtr h_run2 hl - refine ⟨s2, ?_, t2, ?_, ?_⟩ <;> grind [drop_append_of_le_length, take_append_of_le_length] + grind [drop_append_of_le_length, take_append_of_le_length, totalize_run_mtr] + · exact xl.take_append_drop n · rintro ⟨xl1, h_xl1, xl2, h_xl2, rfl⟩ rw [← totalize_language_eq] at h_xl1 - obtain ⟨s2, h_s2, t2, h_t2, h_mtr2⟩ := h_xl2 - obtain ⟨xs2, ss2, h_run2, _, _⟩ := totalize_mtr_run h_s2 h_mtr2 - obtain ⟨ss, ⟨h_start, h_ωtr⟩, _⟩ := concat_run_exists h_xl1 h_run2 - have h_mtr := LTS.ωTr_mTr h_ωtr (zero_le (xl1.length + xl2.length)) - simp [← append_append_ωSequence, extract_eq_drop_take, - take_append_of_le_length, ← List.length_append] at h_mtr - have : ss (xl1.length + xl2.length) = (ss.drop xl1.length) xl2.length := by grind - have : ss (xl1.length + xl2.length) = inr (ss2 xl2.length) := by grind - refine ⟨ss 0, ?_, ss (xl1.length + xl2.length), ?_, ?_⟩ <;> - grind [finConcat, List.length_append] + obtain ⟨_, h_s2, _, _, h_mtr2⟩ := h_xl2 + obtain ⟨_, _, h_run2, _, _⟩ := totalize_mtr_run h_s2 h_mtr2 + obtain ⟨ss, ⟨_, h_ωtr⟩, _⟩ := concat_run_exists h_xl1 h_run2 + grind [ + finConcat, List.length_append, take_append_of_le_length, + extract_eq_drop_take, =_ append_append_ωSequence, get_drop xl2.length xl1.length ss, + LTS.ωTr_mTr h_ωtr (zero_le (xl1.length + xl2.length)) + ] end FinAcc diff --git a/Cslib/Computability/Automata/NA/Total.lean b/Cslib/Computability/Automata/NA/Total.lean index 76bdb7da..95e90f60 100644 --- a/Cslib/Computability/Automata/NA/Total.lean +++ b/Cslib/Computability/Automata/NA/Total.lean @@ -28,24 +28,20 @@ the execution so far corresponds to a finite execution of the original NA. -/ theorem totalize_run_mtr {xs : ωSequence Symbol} {ss : ωSequence (State ⊕ Unit)} {n : ℕ} (h : na.totalize.Run xs ss) (hl : (ss n).isLeft) : ∃ s t, na.MTr s (xs.take n) t ∧ s ∈ na.start ∧ ss 0 = inl s ∧ ss n = inl t := by - obtain ⟨s, _, _⟩ := h.start - obtain ⟨t, _⟩ := isLeft_iff.mp hl + obtain ⟨s, _, eq₁⟩ := h.start + obtain ⟨t, eq₂⟩ := isLeft_iff.mp hl use s, t refine ⟨?_, by grind⟩ - rw [← LTS.totalize.mtr_left_iff, ← extract_eq_take] - have := LTS.ωTr_mTr h.trans (show 0 ≤ n by grind) - simp_all only - assumption + -- TODO: `grind` does not use congruence relations with `na.totalize.MTr` + rw [← LTS.totalize.mtr_left_iff, ← extract_eq_take, eq₁, ← eq₂] + exact LTS.ωTr_mTr h.trans (by grind) /-- Any finite execution of the original NA can be extended to an infinite execution of `NA.totalize`, provided that the alphabet is inbabited. -/ theorem totalize_mtr_run [Inhabited Symbol] {xl : List Symbol} {s t : State} (hs : s ∈ na.start) (hm : na.MTr s xl t) : ∃ xs ss, na.totalize.Run (xl ++ω xs) ss ∧ ss 0 = inl s ∧ ss xl.length = inl t := by - obtain ⟨xs, ss, _⟩ := LTS.Total.mTr_ωTr - (LTS.totalize.total na.toLTS) (LTS.totalize.mtr_left_iff.mpr hm) - use xs, ss - grind [totalize, Run.mk] + grind [totalize, Run, (LTS.totalize.total na.toLTS).mTr_ωTr, =_ LTS.totalize.mtr_left_iff] namespace FinAcc diff --git a/Cslib/Computability/Languages/RegularLanguage.lean b/Cslib/Computability/Languages/RegularLanguage.lean index 18d9ae20..11de7c0d 100644 --- a/Cslib/Computability/Languages/RegularLanguage.lean +++ b/Cslib/Computability/Languages/RegularLanguage.lean @@ -141,6 +141,6 @@ theorem IsRegular.mul [Inhabited Symbol] {l1 l2 : Language Symbol} obtain ⟨State2, h_fin1, nfa2, rfl⟩ := h2 use (State1 ⊕ Unit) ⊕ (State2 ⊕ Unit), inferInstance, ⟨finConcat nfa1 nfa2, inr '' (inl '' nfa2.accept)⟩ - rw [finConcat_language_eq] + exact finConcat_language_eq end Cslib.Language