feat: prove CNFA.{isEmpty, isUniversal} (#900)

SSA/Experimental/Bits/AutoStructs/Basic.lean

@@ -65,6 +65,49 @@ structure RawCNFA.Simul (m : RawCNFA A) (M : NFA A Q) (R : Rel State Q) (D : Set
   trans_match₁ {s s' a q} : R s q → s' ∈ m.tr s a → ∃ q', q' ∈ M.step q a ∧ R s' q'
   trans_match₂ {s a q q'} : R s q → q' ∈ M.step q a → q ∈ D → (q, a, q') ∉ T → ∃ s', s' ∈ m.tr s a ∧ R s' q'
 
+@[simp]
+lemma RawCNFA.Simul.initial {m : RawCNFA A} {M : NFA A Q} (hsim : m.Simul M R ⊤ ∅) :
+    R.set_eq m.initials.toSet M.start := by
+  constructor
+  · rintro s h; exact hsim.initial₁ h
+  · rintro q h; exact hsim.initial₂ h
+
+lemma RawCNFA.Simul.rel_preserved_letter {m : RawCNFA A} {M : NFA A Q} (hsim : m.Simul M R ⊤ ∅) :
+    R.set_eq S₁ Q₁ → ∃ S₂, R.set_eq S₂ (M.stepSet Q₁ a) := by
+  rintro hR
+  use {s' | ∃ s ∈ S₁, s' ∈ m.tr s a }
+  constructor
+  · rintro s' ⟨s, hs, htr⟩
+    obtain ⟨q₁, hq₁, hR₁⟩ := hR.1 hs
+    obtain ⟨q₂, hst, hR₂⟩ := hsim.trans_match₁ hR₁ htr
+    use q₂
+    simp_all only [Set.top_eq_univ, NFA.stepSet, Set.mem_iUnion, exists_prop, and_true]
+    use q₁, hq₁
+  · rintro q₂ ⟨Q₂, ⟨q₁, rfl⟩, Q, ⟨hq₁, rfl⟩, hst⟩
+    obtain ⟨s₁, hs₁, hR₁⟩ := hR.2 hq₁
+    obtain ⟨s₂, htr, hR₂⟩ := hsim.trans_match₂ hR₁ hst (by simp) (by simp)
+    use s₂, ⟨s₁, by tauto⟩
+
+lemma RawCNFA.Simul.rel_preserved_word {m : RawCNFA A} {M : NFA A Q} (hsim : m.Simul M R ⊤ ∅) :
+    R.set_eq S₁ Q₁ → ∃ S₂, R.set_eq S₂ (M.evalFrom Q₁ w) := by
+  induction w using List.list_reverse_induction
+  case base => rintro h; use S₁; simp [h]
+  case ind w a ih =>
+    rintro h; obtain ⟨S₂, hR⟩ := ih h; clear ih
+    simp only [NFA.evalFrom_append_singleton]
+    exact hsim.rel_preserved_letter hR
+
+lemma RawCNFA.Simul.eval_set_eq {m : RawCNFA A} {M : NFA A Q} (hsim : m.Simul M R ⊤ ∅) :
+    ∃ S, R.set_eq S (M.eval w) :=
+  hsim.rel_preserved_word (hsim.initial)
+
+lemma RawCNFA.Simul.rel_eval {m : RawCNFA A} {M : NFA A Q} (hsim : m.Simul M R ⊤ ∅) :
+    q ∈ M.eval w → ∃ s, R s q := by
+  rintro h
+  obtain ⟨S, heq⟩ := hsim.eval_set_eq
+  obtain ⟨s, hs, hR⟩ := heq.2 h
+  exact ⟨s, hR⟩
+
 /--
 Similarity is the greatest simulation
 -/

SSA/Experimental/Bits/AutoStructs/Constructions.lean

@@ -674,11 +674,24 @@ variable {A : Type} [BEq A] [LawfulBEq A] [Hashable A] [DecidableEq A] [FinEnum
 
 def CNFA.isEmpty (m : CNFA n) : Bool := m.m.finals.isEmpty
 
+theorem CNFA.isEmpty_spec {m : CNFA n} {M : NFA' n} :
+    m.Sim M → m.isEmpty → M.accepts = ∅ := by
+  rintro ⟨R, hsim⟩ hemp
+  apply Set.eq_empty_of_forall_not_mem
+  rintro w ⟨w', ⟨q, ha, he⟩, ww⟩
+  obtain ⟨s, hR⟩ := hsim.rel_eval he
+  obtain hfin := hsim.accept hR |>.mpr ha
+  exact Std.HashSet.isEmpty_iff_forall_not_mem.mp hemp _ hfin
+
 def CNFA.isUniversal (m : CNFA n) : Bool := m.neg.isEmpty
 
 theorem CNFA.isUniversal_spec {m : CNFA n} {M : NFA' n} :
     m.Sim M → m.isUniversal → M.accepts = ⊤ := by
-  sorry
+  rintro hsim huniv
+  simp [isUniversal] at huniv
+  have hsim' : m.neg.Sim M.neg := neg_spec m hsim
+  have _ := isEmpty_spec hsim' huniv
+  simp_all
 
 /-- Recognizes the empty word -/
 def RawCNFA.emptyWord : RawCNFA A :=