From 5965c0504b7985cd57230fc49dd7b41f842d8ac1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9o=20Stefanesco?= <leo.lveb@gmail.com>
Date: Wed, 13 Nov 2024 12:05:09 +0100
Subject: [PATCH] Lift NFA results to GoodNFA results

---
 .../Bits/AutoStructs/Constructions.lean       |  4 +--
 .../Bits/AutoStructs/ForMathlib.lean          | 33 ++++++++++++++-----
 .../Bits/AutoStructs/GoodNFA.lean             | 21 ++++++++----
 3 files changed, 42 insertions(+), 16 deletions(-)

diff --git a/SSA/Experimental/Bits/AutoStructs/Constructions.lean b/SSA/Experimental/Bits/AutoStructs/Constructions.lean
index a0603e91f..8518e3708 100644
--- a/SSA/Experimental/Bits/AutoStructs/Constructions.lean
+++ b/SSA/Experimental/Bits/AutoStructs/Constructions.lean
@@ -114,7 +114,7 @@ def GoodCNFA.inter_spec (m1 m2 : GoodCNFA n)
     m2.Sim M2 →
     (m1.inter m2).Sim (M1.inter M2) := by
   intros h1 h2
-  simp [GoodNFA.inter, GoodCNFA.inter]
+  simp [GoodNFA.inter_eq, GoodCNFA.inter]
   have heq : And = to_prop (fun x y => x && y) := by
     ext x y; simp [to_prop]
   simp [heq]
@@ -126,7 +126,7 @@ def GoodCNFA.union_spec (m1 m2 : GoodCNFA n)
     m2.Sim M2 →
     (m1.union m2).Sim (M1.union M2) := by
   intros h1 h2
-  simp [GoodNFA.union, GoodCNFA.union]
+  simp [GoodNFA.union_eq, GoodCNFA.union]
   have heq : Or = to_prop (fun x y => x || y) := by
     ext x y; simp [to_prop]
   simp [heq]
diff --git a/SSA/Experimental/Bits/AutoStructs/ForMathlib.lean b/SSA/Experimental/Bits/AutoStructs/ForMathlib.lean
index 3ca8ab92c..75ef13373 100644
--- a/SSA/Experimental/Bits/AutoStructs/ForMathlib.lean
+++ b/SSA/Experimental/Bits/AutoStructs/ForMathlib.lean
@@ -107,8 +107,9 @@ lemma helper_dec_enc (bvs : BitVecs n) (h : w' = bvs.w) i (j : Nat) :
     (bvs.bvs.get i)[j]?.getD false = (h ▸ bvs.bvs.get i)[j]?.getD false := by
   rcases h; simp
 
-lemma dec_enc (bvs : BitVecs n) : dec (enc bvs) = bvs := by
-  ext1; exact dec_enc_w bvs
+@[simp]
+lemma dec_enc : Function.RightInverse (α := BitVecs' n) enc dec := by
+  intros bvs; ext1; exact dec_enc_w bvs
   next i =>
     simp [enc, dec]
     ext j
@@ -124,8 +125,9 @@ lemma dec_enc (bvs : BitVecs n) : dec (enc bvs) = bvs := by
     apply (helper_dec_enc ⟨w, bvs⟩)
     simp
 
-lemma enc_dec (bvs' : BitVecs' n) : enc (dec bvs') = bvs' := by
-  simp [enc, dec]
+@[simp]
+lemma enc_dec : Function.LeftInverse (α := BitVecs' n) enc dec := by
+  intros bvs'; simp [enc, dec]
   ext1 k
   by_cases hin : k < (List.length bvs')
   · simp
@@ -138,6 +140,16 @@ lemma enc_dec (bvs' : BitVecs' n) : enc (dec bvs') = bvs' := by
   · simp
     repeat rw [List.getElem?_eq_none] <;> simp_all
 
+@[simp]
+def dec_bij {n : Nat} : Function.Bijective (dec (n := n)) := by
+  rw [Function.bijective_iff_has_inverse]; use enc; simp
+
+def dec_surj (n : Nat) : Function.Surjective (dec (n := n)) := by
+  exact Function.Bijective.surjective dec_bij
+
+def dec_inj {n : Nat} : Function.Injective (dec (n := n)) := by
+  exact Function.Bijective.injective dec_bij
+
 @[simp]
 def BitVecs.transport (f : Fin n → Fin m) (bvs : BitVecs m) : BitVecs n :=
   { w := bvs.w, bvs := bvs.bvs.transport f }
@@ -250,6 +262,8 @@ lemma reduce_spec (M : NFA α σ) : M.reduce.accepts = M.accepts := by
     · apply ha
     · simp_all [←reduce_eval q]
 
+-- TODO: M.reduce is reduced
+
 def closed_set (M : NFA α σ) (S : Set σ) := M.start ⊆ S ∧ ∀ a, M.stepSet S a ⊆ S
 
 theorem reachable_sub_closed_set (M : NFA α σ) (S : Set σ) (hcl: M.closed_set S) :
@@ -357,6 +371,7 @@ lemma product_eval {M : NFA α σ} {N : NFA α ς} {w} :
   case base => ext; simp [product]
   case ind w a ih => simp only [eval, evalFrom_append_singleton, product_stepSet, ih]
 
+@[simp]
 theorem inter_accepts (M : NFA α σ) (N : NFA α ς) :
     (M.inter N).accepts = M.accepts ∩ N.accepts:= by
   ext w; simp [accepts, inter]; constructor
@@ -396,12 +411,12 @@ theorem flipAccept_eval {M : NFA α σ} : M.flipAccept.eval w = M.eval w := by
 
 @[simp]
 theorem flipAccept_accepts (M : NFA α σ) (hc : M.Complete) (hdet : M.Deterministic) :
-    M.flipAccept.accepts = M.accepts.compl := by
-  ext w; constructor; simp [accepts, Set.compl]; rintro ⟨q, ha, he⟩
+    M.flipAccept.accepts = M.acceptsᶜ := by
+  ext w; constructor; simp [accepts, Language.eq_def, Set.compl_def]; rintro q ha he
   · intros q' ha' he'
     obtain rfl := deterministic_eval_subsingleton hdet w he he'
     simp_all [flipAccept, Set.compl]
-  · simp [accepts, Set.compl]
+  · simp [accepts, Language.eq_def, Set.compl_def]
     intros hw
     obtain ⟨qf, hqf⟩ := hc w
     have ha : ¬ qf ∈ M.accept := by by_contra; apply hw <;> assumption
@@ -422,7 +437,7 @@ lemma determinize_deternistic (M : NFA α σ) :
 
 @[simp]
 theorem neg_accepts (M : NFA α σ) :
-    M.neg.accepts = M.accepts.compl := by
+    M.neg.accepts = M.acceptsᶜ := by
   simp [neg]
 
 
@@ -450,6 +465,7 @@ lemma lift_eval (M : NFA (BitVec n) σ) (f : Fin n → Fin m) :
   case base => simp [lift, BitVecs'.transport]
   case ind w a ih => simp [BitVecs'.transport, ih]
 
+@[simp]
 lemma lift_accepts (M : NFA (BitVec n) σ) (f : Fin n → Fin m) :
     (M.lift f).accepts = BitVecs'.transport f ⁻¹' M.accepts := by
   simp [accepts]
@@ -505,6 +521,7 @@ lemma proj_eval (M : NFA (BitVec m) σ) (f : Fin n → Fin m) :
         use wa'.dropLast
         simp_all [BitVecs'.transport]
 
+@[simp]
 lemma proj_accepts (M : NFA (BitVec m) σ) (f : Fin n → Fin m) :
     (M.proj f).accepts = BitVecs'.transport f '' M.accepts := by
   ext w; simp [accepts]; constructor
diff --git a/SSA/Experimental/Bits/AutoStructs/GoodNFA.lean b/SSA/Experimental/Bits/AutoStructs/GoodNFA.lean
index 0e8f35163..37fbc570b 100644
--- a/SSA/Experimental/Bits/AutoStructs/GoodNFA.lean
+++ b/SSA/Experimental/Bits/AutoStructs/GoodNFA.lean
@@ -28,23 +28,30 @@ noncomputable def complete (M : GoodNFA n) : GoodNFA n where
   σ := _
   M := M.M.complete
 
+
 def product (final? : Prop → Prop → Prop) (M N : GoodNFA n) : GoodNFA n where
   σ := _
   M := M.M.product final? N.M
 
-def inter (M N : GoodNFA n) : GoodNFA n := GoodNFA.product And M N
+def inter (M N : GoodNFA n) : GoodNFA n := ⟨_, M.M.inter N.M⟩
+
+lemma inter_eq (M N : GoodNFA n) : M.inter N = GoodNFA.product And M N := by
+  simp [inter, product, NFA.inter]
 
 @[simp]
 lemma inter_accepts (M N : GoodNFA n) :
     (M.inter N).accepts = M.accepts ∩ N.accepts := by
-  sorry
+  simp [accepts, accepts', inter, Set.image_inter dec_inj]
 
-def union (M N : GoodNFA n) : GoodNFA n := GoodNFA.product Or M.complete N.complete
+def union (M N : GoodNFA n) : GoodNFA n := ⟨_, M.M.union N.M⟩
+
+lemma union_eq (M N : GoodNFA n) : M.union N = GoodNFA.product Or M.complete N.complete := by
+  simp [union, product, NFA.union, NFA.union', complete]
 
 @[simp]
 lemma union_accepts (M N : GoodNFA n) :
     (M.union N).accepts = M.accepts ∪ N.accepts := by
-  sorry
+  simp [accepts, accepts', union]; rw [Set.image_union]
 
 def neg (M : GoodNFA n) : GoodNFA n where
   σ := _
@@ -52,8 +59,8 @@ def neg (M : GoodNFA n) : GoodNFA n where
 
 @[simp]
 lemma neg_accepts (M : GoodNFA n) :
-    M.neg.accepts = M.accepts.compl := by
-  sorry
+    M.neg.accepts = M.acceptsᶜ:= by
+  simp [accepts, accepts', neg, Set.image_compl_eq (dec_bij)]
 
 def reduce (M : GoodNFA n) : GoodNFA n where
   σ := _
@@ -74,9 +81,11 @@ def proj (f : Fin m → Fin n) (M : GoodNFA n) : GoodNFA m where
 @[simp]
 lemma lift_accepts (M : GoodNFA n) (f : Fin n → Fin m) :
     (M.lift f).accepts = BitVecs.transport f ⁻¹' M.accepts := by
+  simp [accepts, accepts', lift]
   sorry
 
 @[simp]
 lemma proj_accepts (M : GoodNFA m) (f : Fin n → Fin m) :
     (M.proj f).accepts = BitVecs.transport f '' M.accepts := by
+  simp [accepts, accepts', proj]
   sorry