apply suggestion

Author: staroperator

Mathlib/ModelTheory/Arithmetic/Presburger/Definability.lean

@@ -9,10 +9,7 @@ public import Mathlib.ModelTheory.Arithmetic.Presburger.Basic
 public import Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
 public import Mathlib.ModelTheory.Definability
 
-import Mathlib.Algebra.GCDMonoid.Finset
-import Mathlib.Algebra.GCDMonoid.Nat
 import Mathlib.Algebra.Group.Submonoid.Finsupp
-import Mathlib.LinearAlgebra.Dimension.Basic
 import Mathlib.LinearAlgebra.Matrix.Notation
 
 /-!
@@ -39,13 +36,13 @@ definable.
 * [Samuel Eilenberg and M. P. Schützenberger, *Rational Sets in Commutative Monoids*][eilenberg1969]
 -/
 
-@[expose] public section
+public section
 
-variable {α : Type*} [Fintype α] {s : Set (α → ℕ)} {A : Set ℕ}
+variable {α : Type*} {s : Set (α → ℕ)} {A : Set ℕ}
 
-open Set Submodule FirstOrder Language
+open Set FirstOrder Language
 
-theorem IsLinearSet.definable (hs : IsLinearSet s) : A.Definable presburger s := by
+theorem IsLinearSet.definable [Finite α] (hs : IsLinearSet s) : A.Definable presburger s := by
   rw [isLinearSet_iff] at hs
   rcases hs with ⟨v, t, rfl⟩
   refine ⟨Formula.iExs t (Formula.iInf fun i : α =>
@@ -64,7 +61,8 @@ theorem IsLinearSet.definable (hs : IsLinearSet s) : A.Definable presburger s :=
   congr! 1 with i
   simp
 
-theorem IsSemilinearSet.definable (hs : IsSemilinearSet s) : A.Definable presburger s := by
+theorem IsSemilinearSet.definable [Finite α] (hs : IsSemilinearSet s) :
+    A.Definable presburger s := by
   rw [isSemilinearSet_iff] at hs
   rcases hs with ⟨S, hS, rfl⟩
   choose φ hφ using fun s : S => (hS s.1 s.2).definable
@@ -76,13 +74,12 @@ theorem IsSemilinearSet.definable (hs : IsSemilinearSet s) : A.Definable presbur
 
 namespace FirstOrder.Language.presburger
 
-lemma term_realize_eq_add_dotProduct (t : presburger[[A]].Term α) :
+lemma term_realize_eq_add_dotProduct [Fintype α] (t : presburger[[A]].Term α) :
     ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), t.realize v = k + u ⬝ᵥ v := by
   classical
   induction t with simp only [Term.realize]
   | var i =>
-    refine ⟨0, Pi.single i 1, ?_⟩
-    simp
+    exact ⟨0, Pi.single i 1, by simp⟩
   | @func l f ts ih =>
     cases f with
     | inl f =>
@@ -105,13 +102,15 @@ lemma term_realize_eq_add_dotProduct (t : presburger[[A]].Term α) :
       cases l with
       | zero =>
         refine ⟨f, 0, fun v => ?_⟩
-        rw [withConstants_funMap_sumInr]
-        simp only [constantsOn_Functions, constantsOnFunc.eq_1, coe_con, zero_dotProduct, add_zero]
+        rw [withConstants_funMap_sumInr, zero_dotProduct, add_zero]
         rfl
       | succ => nomatch f
 
+variable [Finite α]
+
 lemma isSemilinearSet_boundedFormula_realize {n} (φ : presburger[[A]].BoundedFormula α n) :
     IsSemilinearSet {v : α ⊕ Fin n → ℕ | φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)} := by
+  haveI := Fintype.ofFinite α
   induction φ with simp only [BoundedFormula.Realize]
   | equal t₁ t₂ =>
     rcases term_realize_eq_add_dotProduct t₁ with ⟨k₁, u₁, ht₁⟩
@@ -156,109 +155,16 @@ theorem definable₁_iff_ultimately_periodic {s : Set ℕ} :
   rw [Definable₁, definable_iff_isSemilinearSet,
     ← isSemilinearSet_image_iff (LinearEquiv.funUnique (Fin 1) ℕ ℕ), ← preimage_setOf_eq]
   simp only [LinearEquiv.funUnique_apply, Function.eval, Fin.default_eq_zero, setOf_mem_eq]
-  rw [image_preimage_eq s fun x => ⟨![x], rfl⟩]
-  constructor
-  · intro hs
-    apply IsSemilinearSet.isProperSemilinearSet at hs
-    rw [isProperSemilinearSet_iff] at hs
-    rcases hs with ⟨S, hS, rfl⟩
-    replace hS : ∀ t ∈ S, ∃ k, ∃ p > 0, ∀ x ≥ k, x ∈ t ↔ x + p ∈ t := by
-      intro t ht
-      apply hS at ht
-      rw [isProperLinearSet_iff] at ht
-      rcases ht with ⟨a, t, ht, rfl⟩
-      have hcard : t.card ≤ 1 := by simpa [CommSemiring.rank_self] using ht.cardinal_le_rank
-      simp_rw [Finset.card_le_one_iff_subset_singleton, Finset.subset_singleton_iff] at hcard
-      rcases hcard with ⟨b, (rfl | rfl)⟩
-      · refine ⟨a + 1, 1, zero_lt_one, fun x hx => ?_⟩
-        simp [(Nat.lt_of_succ_le hx).ne', (Nat.lt_of_succ_le (Nat.le_succ_of_le hx)).ne']
-      · have hb : b ≠ 0 := by simpa [ne_comm] using ht.zero_notMem_image
-        rw [Nat.ne_zero_iff_zero_lt] at hb
-        refine ⟨a, b, hb, fun x hx => ?_⟩
-        simp only [Finset.coe_singleton, mem_vadd_set, SetLike.mem_coe,
-          AddSubmonoid.mem_closure_singleton, smul_eq_mul, vadd_eq_add, exists_exists_eq_and]
-        constructor
-        · rintro ⟨x, rfl⟩
-          refine ⟨x + 1, ?_⟩
-          simp [add_one_mul, add_assoc]
-        · rintro ⟨y, heq⟩
-          cases y with
-          | zero =>
-            rw [zero_mul, add_zero] at heq
-            simp only [heq, ge_iff_le, add_le_iff_nonpos_right, nonpos_iff_eq_zero] at hx
-            simp [hx] at hb
-          | succ y =>
-            rw [add_one_mul, ← add_assoc, add_right_cancel_iff] at heq
-            exact ⟨y, heq⟩
-    choose! k p hS hS' using hS
-    refine ⟨S.sup k, S.lcm p, ?_, fun x hx => ?_⟩
-    · rw [gt_iff_lt, Nat.pos_iff_ne_zero, ne_eq]
-      simpa [Finset.lcm_eq_zero_iff, ← Nat.pos_iff_ne_zero]
-    · simp only [ge_iff_le, Finset.sup_le_iff] at hx
-      refine exists_congr fun t => and_congr_right fun ht => ?_
-      have hpt : p t ∣ S.lcm p := Finset.dvd_lcm ht
-      rw [dvd_iff_exists_eq_mul_left] at hpt
-      rcases hpt with ⟨m, hpt⟩
-      rw [hpt]
-      clear hpt
-      induction m with
-      | zero => simp
-      | succ m ih =>
-        simp [← ih, Nat.succ_mul, ← add_assoc,
-          ← hS' t ht (x + m * p t) (le_add_of_le_left (hx t ht))]
-  · intro ⟨k, p, hp, hs⟩
-    have h₁ : {x ∈ s | x < k}.Finite := (Set.finite_lt_nat k).subset (sep_subset_setOf _ _)
-    have h₂ : {x ∈ s | k ≤ x ∧ x < k + p}.Finite :=
-      (Set.finite_Ico k (k + p)).subset (sep_subset_setOf _ _)
-    convert (IsSemilinearSet.of_finite h₁).union (.add (.of_finite h₂) (.closure_finset {p}))
-    ext x
-    simp only [sep_and, Finset.coe_singleton, mem_union, mem_setOf_eq, mem_add, mem_inter_iff,
-      SetLike.mem_coe, AddSubmonoid.mem_closure_singleton, smul_eq_mul, exists_exists_eq_and]
-    constructor
-    · intro hx
-      by_cases hx' : x < k
-      · exact Or.inl ⟨hx, hx'⟩
-      · rw [not_lt] at hx'
-        refine Or.inr ⟨k + (x - k) % p, ⟨⟨?_1, ?_2⟩, ?_1, ?_3⟩, (x - k) / p, ?_4⟩
-        · rw [← add_tsub_cancel_of_le hx', ← Nat.mod_add_div' (x - k) p, ← add_assoc] at hx
-          generalize (x - k) / p = m at hx
-          induction m with
-          | zero => simpa using hx
-          | succ m ih =>
-            refine ih ?_
-            rwa [hs _ (Nat.le_add_right_of_le (Nat.le_add_right _ _)), add_assoc, ← Nat.add_one_mul]
-        · apply Nat.le_add_right
-        · apply Nat.add_lt_add_left (Nat.mod_lt _ hp)
-        · rw [add_assoc, Nat.mod_add_div', add_tsub_cancel_of_le hx']
-    · rintro (⟨hx, hx'⟩ | ⟨x, ⟨⟨hx, hx'⟩, _⟩, m, rfl⟩)
-      · exact hx
-      · induction m with
-        | zero => simpa
-        | succ m ih =>
-          rw [hs _ (le_add_right hx')] at ih
-          rwa [Nat.add_one_mul, ← add_assoc]
+  rw [image_preimage_eq s fun x => ⟨![x], rfl⟩, Nat.isSemilinearSet_iff_ultimately_periodic]
 
 /-- The graph of multiplication is not Presburger definable in `ℕ`. -/
-theorem mul_not_definable :
-    ¬ A.Definable presburger {v : Fin 3 → ℕ | v 0 = v 1 * v 2} := by
+theorem mul_not_definable : ¬ A.Definable presburger {v : Fin 3 → ℕ | v 0 = v 1 * v 2} := by
   intro hmul
   have hsqr : A.Definable₁ presburger {x * x | x : ℕ} := by
-    rcases hmul with ⟨φ, hφ⟩
-    exists Formula.iExs (Fin 1) (φ.subst ![Term.var (.inl 0), Term.var (.inr 0), Term.var (.inr 0)])
-    simp only [setOf] at hφ
-    ext x
-    simp only [Fin.isValue, mem_setOf_eq, Formula.Realize, BoundedFormula.realize_iExs,
-      BoundedFormula.realize_subst]
-    constructor
-    · intro ⟨y, h⟩
-      refine ⟨![y], ?_⟩
-      rw [← Formula.Realize, ← hφ]
-      simp [h]
-    · intro ⟨v, h⟩
-      rw [← Formula.Realize, ← hφ] at h
-      simp only [Fin.isValue, Matrix.cons_val_zero, Term.realize_var, Sum.elim_inl,
-        Matrix.cons_val_one, Sum.elim_inr, Matrix.cons_val] at h
-      exact ⟨v 0, h.symm⟩
+    rw [Definable₁]
+    convert (hmul.preimage_comp (β := Fin 2) ![0, 1, 1]).image_comp ![0]
+    ext
+    simpa [funext_iff, Fin.exists_fin_succ_pi] using exists_congr fun _ => Eq.comm
   rw [definable₁_iff_ultimately_periodic] at hsqr
   rcases hsqr with ⟨k, p, hp, h⟩
   specialize h ((max k p) * (max k p)) ((Nat.le_mul_self _).trans' (le_max_left _ _))

Mathlib/ModelTheory/Arithmetic/Presburger/Semilinear/Defs.lean

@@ -8,6 +8,10 @@ module
 public import Mathlib.GroupTheory.Finiteness
 public import Mathlib.LinearAlgebra.LinearIndependent.Defs
 
+import Mathlib.Algebra.GCDMonoid.Finset
+import Mathlib.Algebra.GCDMonoid.Nat
+import Mathlib.LinearAlgebra.Dimension.Basic
+
 /-!
 # Linear and semilinear sets
 
@@ -31,6 +35,8 @@ which are linear sets with linearly independent submonoid generators (periods).
 - `IsSemilinearSet` is closed under union, projection, set addition and additive closure.
 - `IsSemilinearSet.isProperSemilinearSet`: every semilinear set is a finite union of proper linear
   sets.
+- `Nat.isSemilinearSet_iff_ultimately_periodic`: A set of `ℕ` is semilinear if and only if it is
+  ultimately periodic, i.e. periodic after some number `k`.
 
 ## Naming convention
 
@@ -379,3 +385,71 @@ theorem IsSemilinearSet.isProperSemilinearSet [IsCancelAdd M] (hs : IsSemilinear
   rcases hs with ⟨S, hS, hS', rfl⟩
   simp_rw [sUnion_eq_biUnion]
   exact IsProperSemilinearSet.biUnion hS fun s hs => (hS' s hs).isProperSemilinearSet
+
+
+
+/-- A set of `ℕ` is semilinear if and only if it is ultimately periodic, i.e. periodic after some
+number `k`. -/
+theorem Nat.isSemilinearSet_iff_ultimately_periodic {s : Set ℕ} :
+    IsSemilinearSet s ↔ ∃ k, ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s := by
+  constructor
+  · intro hs
+    apply IsSemilinearSet.isProperSemilinearSet at hs
+    rw [isProperSemilinearSet_iff] at hs
+    rcases hs with ⟨S, hS, rfl⟩
+    replace hS : ∀ t ∈ S, ∃ k, ∃ p > 0, ∀ x ≥ k, x ∈ t ↔ x + p ∈ t := by
+      intro t ht
+      apply hS at ht
+      rw [isProperLinearSet_iff] at ht
+      rcases ht with ⟨a, t, ht, rfl⟩
+      have hcard : t.card ≤ 1 := by simpa [CommSemiring.rank_self] using ht.cardinal_le_rank
+      simp_rw [Finset.card_le_one_iff_subset_singleton, Finset.subset_singleton_iff] at hcard
+      rcases hcard with ⟨b, (rfl | rfl)⟩
+      · refine ⟨a + 1, 1, zero_lt_one, fun x hx => ?_⟩
+        simp [(by grind : x ≠ a), (by grind : x + 1 ≠ a)]
+      · have hb : b ≠ 0 := by simpa [ne_comm] using ht.zero_notMem_image
+        rw [Nat.ne_zero_iff_zero_lt] at hb
+        refine ⟨a, b, hb, fun x hx => ?_⟩
+        simp only [Finset.coe_singleton, mem_vadd_set, SetLike.mem_coe,
+          AddSubmonoid.mem_closure_singleton, smul_eq_mul, vadd_eq_add, exists_exists_eq_and]
+        constructor
+        · rintro ⟨x, rfl⟩
+          exact ⟨x + 1, by grind⟩
+        · rintro ⟨y, heq⟩
+          cases y with
+          | zero => exact ⟨0, by grind⟩
+          | succ y => exact ⟨y, by grind⟩
+    choose! k p hS hS' using hS
+    refine ⟨S.sup k, S.lcm p, ?_, fun x hx => ?_⟩
+    · grind [Finset.lcm_eq_zero_iff]
+    · simp only [mem_sUnion, SetLike.mem_coe]
+      refine exists_congr fun t => and_congr_right fun ht => ?_
+      have hpt : p t ∣ S.lcm p := Finset.dvd_lcm ht
+      rw [dvd_iff_exists_eq_mul_left] at hpt
+      rcases hpt with ⟨m, hpt⟩
+      rw [hpt]
+      clear hpt
+      induction m with grind [Finset.sup_le_iff]
+  · intro ⟨k, p, hp, hs⟩
+    have h₁ : {x ∈ s | x < k}.Finite := (Set.finite_lt_nat k).subset (sep_subset_setOf _ _)
+    have h₂ : {x ∈ s | k ≤ x ∧ x < k + p}.Finite :=
+      (Set.finite_Ico k (k + p)).subset (sep_subset_setOf _ _)
+    convert (IsSemilinearSet.of_finite h₁).union (.add (.of_finite h₂) (.closure_finset {p}))
+    ext x
+    simp only [sep_and, Finset.coe_singleton, mem_union, mem_setOf_eq, mem_add, mem_inter_iff,
+      SetLike.mem_coe, AddSubmonoid.mem_closure_singleton, smul_eq_mul, exists_exists_eq_and]
+    constructor
+    · intro hx
+      by_cases hx' : x < k
+      · exact Or.inl ⟨hx, hx'⟩
+      · rw [not_lt] at hx'
+        refine Or.inr ⟨k + (x - k) % p, ⟨⟨?_1, ?_2⟩, ?_1, ?_3⟩, (x - k) / p, ?_4⟩
+        · rw [← add_tsub_cancel_of_le hx', ← Nat.mod_add_div' (x - k) p, ← add_assoc] at hx
+          generalize (x - k) / p = m at hx
+          induction m with grind
+        · grind
+        · exact Nat.add_lt_add_left (Nat.mod_lt _ hp) _
+        · rw [add_assoc, Nat.mod_add_div', add_tsub_cancel_of_le hx']
+    · rintro (⟨hx, hx'⟩ | ⟨x, ⟨⟨hx, hx'⟩, _⟩, m, rfl⟩)
+      · exact hx
+      · induction m with grind