Prove derive_commutes

Katydid/Regex/SmartRegex.lean

@@ -422,8 +422,94 @@ 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
+  cases r with
+  | emptyset =>
+    funext xs
+    simp [derive, denote]
+  | emptystr =>
+    funext xs
+    simp [derive, denote]
+  | pred p =>
+    funext xs
+    simp [derive, denote]
+    rw [onlyif', Language.pred]
+    split_ifs with h
+    · rw [denote]
+      simp only [Language.emptystr, cons.injEq]
+      apply Iff.intro
+      · intro hxs
+        use x
+      · intro ⟨w, hxs, hp⟩
+        exact hxs.right
+    · rw [denote]
+      simp
+      intro _ h'
+      contradiction
+  | or r₁ r₂ =>
+    funext xs
+    simp [derive, denote]
+    rw [←smartOr_is_or, denote, Language.or]
+    rw [derive_commutes, derive_commutes]
+    rfl
+  | concat r₁ r₂ =>
+    funext xs
+    simp [derive, denote]
+    rw [←smartOr_is_or, denote, Language.or]
+    rw [←smartConcat_is_concat]
+    simp only [denote, Language.concat, exists_and_left]
+    apply Iff.intro
+    · intro h
+      match h with
+      | Or.inl ⟨ys, h, zs, h', hxs⟩ =>
+        rw [derive_commutes] at h
+        rw [Language.derive, Language.derives, singleton_append] at h
+        refine ⟨x::ys, h, zs, h', ?_⟩
+        rw [hxs, cons_append]
+      | Or.inr h =>
+        rw [onlyif] at h
+        split_ifs at h with hn
+        · rw [null_commutes, Language.null] at hn
+          rw [derive_commutes] at h
+          rw [Language.derive, Language.derives, singleton_append] at h
+          refine ⟨[], hn, x::xs, h, ?_⟩
+          rw [nil_append]
+        · simp only [denote, Language.emptyset] at h
+    · intro ⟨ys, h, zs, h', hxs⟩
+      rw [derive_commutes]
+      simp only [Language.derive, Language.derives, singleton_append]
+      cases ys with
+      | nil =>
+        rw [nil_append] at hxs
+        rw [onlyif]
+        split_ifs with hn
+        · rw [derive_commutes]
+          rw [Language.derive, Language.derives, singleton_append, hxs]
+          exact Or.inr h'
+        · rw [null_commutes, Language.null] at hn
+          contradiction
+      | cons w ws =>
+        rw [cons_append, cons.injEq] at hxs
+        rw [hxs.left]
+        exact Or.inl ⟨ws, h, zs, h', hxs.right⟩
+  | star r =>
+    funext xs
+    simp [derive, denote]
+    rw [←smartConcat_is_concat]
+    simp only [denote, Language.concat, exists_and_left]
+    apply Iff.intro
+    · intro ⟨ys, h, zs, h', hxs⟩
+      rw [derive_commutes] at h
+      rw [Language.derive, Language.derives, singleton_append] at h
+      apply Language.star.more x ys zs
+      rw [hxs, cons_append]
+      exact h
+      exact h'
+    · intro h
+      cases h with
+      | more y ys zs _ hxs h h'  =>
+        rw [cons_append, cons.injEq] at hxs
+        rw [derive_commutes, hxs.left]
+        exact ⟨ys, h, zs, h', hxs.right⟩
 
 def derives (r: Regex α) (xs: List α): Regex α :=
   (List.foldl derive r) xs