Avoid tactic based defs in PowersetConstruction

knowsys · Sep 28, 2024 · 89c1b1d · 89c1b1d
1 parent b71aed4
commit 89c1b1d
Showing 1 changed file with 8 additions and 14 deletions.
diff --git a/FormalSystems/Chomsky/Regular/PowersetConstruction.lean b/FormalSystems/Chomsky/Regular/PowersetConstruction.lean
@@ -17,20 +17,14 @@ variable [DecidableEq α] [DecidableEq qs] { M: NFA α qs }
 def DFA.fromNFA.RunFromRestricted { qs: _ }
   (r: (DFA.fromNFA M).Run q w)
   (h: q.val ⊆ qs.val):
-  (DFA.fromNFA M).Run qs w := by
-  cases r
-  apply NFA.Run.final
-  assumption
-  case step x _ =>
-    apply NFA.Run.step
-    dsimp [toNFA, fromNFA]; simp
-    rfl
-    apply RunFromRestricted
-    assumption
-    dsimp [toNFA, fromNFA] at x; simp at x
-    simp_rw [x]
-    apply Finset.fold_union_subs
-    repeat { assumption }
+  (DFA.fromNFA M).Run qs w :=
+  match r with
+  | .final _ h => .final qs h
+  | .step _ hq' r hw => .step
+    qs
+    (by unfold toNFA; unfold fromNFA; simp; rfl)
+    (RunFromRestricted r (by unfold toNFA at hq'; unfold fromNFA at hq'; simp at hq'; simp [hq']; apply Finset.fold_union_subs; exact h))
+    hw
 
 theorem DFA.fromNFA.RunFromRestricted_final
   (h: r.last ∈ (DFA.fromNFA M).F):