fix aesop_reconcile, now does not need arguments

Author: Ferinko

ArkLib/ProofSystem/Fri/Domain.lean

@@ -27,6 +27,11 @@ omit [Finite F] in
 private lemma op_der_eq : Monoid.toMulAction Fˣ = Units.mulAction' := by ext; rfl
 
 open Lean Elab in
+/--
+A variation on `rw [op_der_eq] at *`.
+
+Ensures that once `Fˣ` is fixed, we use `Monoid.toMulAction Fˣ`, not `Units.mulAction'`.
+-/
 private def reconcile (goal : MVarId) : MetaM (Option MVarId) := goal.withContext do
   let mut goal ← go goal
   for const in ←getLCtx do
@@ -43,46 +48,30 @@ private def reconcile (goal : MVarId) : MetaM (Option MVarId) := goal.withContex
     return goal'
 
 open Lean Elab Tactic in
-private def reconcile_tac : TacticM Unit := liftMetaTactic1 reconcile
+/--
+Reconciles `Monoid.toMulAction Fˣ = Units.mulAction'` across the goal.
+-/
+scoped elab "reconcile" : tactic => liftMetaTactic1 reconcile
 
 /--
 `reconcile`-aware `aesop` that deals with coset membership.
 
-- Optionally takes either side of `mem_leftCoset_iff` as a hint.
+Can be trivially extended to recognise more than just `mem_leftCoset_iff`.
 -/
-scoped syntax (name := reconcileStx) withPosition("aesop_reconcile" (colGt ident)?) : tactic
+scoped syntax (name := reconcileStx) "aesop_reconcile" : tactic
 
-open Lean Elab Tactic in
+set_option hygiene false in
+open Lean Elab Tactic PrettyPrinter Delaborator in
 @[tactic reconcileStx, inherit_doc reconcileStx]
-private def elabReconcileStx : Tactic := fun stx => do
+private def elabReconcileStx : Tactic := fun stx => withMainContext do
   match stx with
-  | `(tactic|aesop_reconcile $[$h]?) =>
-    let tac : TacticM _ :=
-      match h with
-      | .none => `(tactic|(try apply (mem_leftCoset_iff _).1
-                           aesop (add safe tactic reconcile_tac)))
-      | .some h => `(tactic| (try have := (mem_leftCoset_iff _).2 $h
-                              try apply (mem_leftCoset_iff _).1
-                              aesop (add safe tactic reconcile_tac)))
-    evalTactic (←tac)
+  | `(tactic|aesop_reconcile) =>  
+    evalTactic (←
+      `(tactic|(have := fun X₁ X₂ X₃ ↦ @mem_leftCoset_iff Fˣ _ X₁ X₂ X₃
+                reconcile
+                aesop)))
   | _ => throwError "Unsupported syntax."
 
-/--
-Reconciles `Monoid.toMulAction Fˣ = Units.mulAction'` across the goal.
--/
-scoped elab "reconcile" : tactic => reconcile_tac
-
--- open Lean Elab Tactic in
--- scoped elab "reconcile" h:(ident)? : tactic => do
---   let tac : TacticM _ :=
---     match h with
---     | .none => `(tactic|(try apply (mem_leftCoset_iff _).1
---                          aesop (add safe tactic (reconcile_tac))))
---     | .some h => `(tactic| (try have := (mem_leftCoset_iff _).2 $h
---                             try apply (mem_leftCoset_iff _).1
---                             aesop (add safe tactic (reconcile_tac))))
---   evalTactic (←tac)
-
 namespace Domain
 
 /-- Constructs the subgroups of `Fˣ` which we will use to construct
@@ -194,8 +183,10 @@ def domainEmb {i : ℕ} : evalDomain D i ↪ F :=
 
 /- Proof the first subgroup is `D`, the cyclic group generated by `DIsCyclicC.gen : Fˣ` -/
 omit [Finite F] in
-lemma D_def : D = evalDomain D 0 := by
+@[simp]
+lemma D_def : evalDomain D 0 = D := by
   unfold evalDomain
+  symm
   ext x
   rw [Subgroup.mem_zpowers_iff]
   simp only [pow_zero, pow_one]
@@ -360,8 +351,6 @@ namespace CosetDomain
 
 open Pointwise
 
-
-  
 /- Element of `Fˣ` we will use to define our coset -/
 variable (x : Fˣ)
 
@@ -373,21 +362,12 @@ def evalDomain (i : ℕ) : Set Fˣ :=
 abbrev evalDomainSigma (s : Fin (n + 1) → ℕ+) (i : ℕ) :=
   evalDomain D x (∑ j' ∈ finRangeTo i, s j') 
 
--- set_option pp.all true in
 /- Enumeration of the elements of the `i`th coset. -/
 def domain (n : ℕ) (i : ℕ) : Fin (2 ^ (n - i)) → evalDomain D x i :=
   fun j =>
     ⟨
       x ^ 2 ^ i * (DIsCyclicC.gen ^ (2 ^ i)) ^ j.1,
-      by
-        simp
-        rw [←Domain.evalDomain]
-        have h :
-            (x ^ 2 ^ i)⁻¹ * (x ^ 2 ^ i * (DIsCyclicC.gen.1 ^ 2 ^ i) ^ j.1) ∈
-              Domain.evalDomain D i := by
-          rw [←mul_assoc]
-          simp
-        aesop_reconcile h
+      by aesop_reconcile
     ⟩
 
 lemma domain_injective {i : ℕ} : i ≤ n → Function.Injective (domain D x n i) := by
@@ -422,9 +402,7 @@ noncomputable def domainToFin {i : Fin (n + 1)} : evalDomain D x i → Fin (2 ^
             g.1.1 = x.1 ^ (2 ^ i.1) * ((DIsCyclicC.gen.1 ^ (2 ^ i.1)) ^ ind.1) := by
       have h := g.2
       unfold evalDomain at h
-      have h' : (x ^ 2 ^ i.1)⁻¹ * ↑g ∈ ↑(Domain.evalDomain D ↑i) := by
-        apply (@mem_leftCoset_iff Fˣ _ (Domain.evalDomain D ↑i) g.1 (x ^ (2 ^ i.1))).mp
-        aesop_reconcile
+      have h' : (x ^ 2 ^ i.1)⁻¹ * ↑g ∈ ↑(Domain.evalDomain D ↑i) := by aesop_reconcile
       unfold Domain.evalDomain at h'
       rw [Subgroup.mem_zpowers_iff] at h'
       rcases h' with ⟨ind, h'⟩
@@ -480,7 +458,11 @@ def injectF {F : Type} [NonBinaryField F] {D : Subgroup Fˣ} [DIsCyclicC : IsCyc
 /- Helper lemmas for constructing operations on/lifting between domains. -/
 
 omit [Finite F] in
-lemma D_def : evalDomain D x 0 = x • D := by simp [Domain.D_def D]
+@[simp]
+lemma D_def : evalDomain D x 0 = x • D := by
+  unfold evalDomain
+  rw [Domain.D_def]
+  simp
 
 lemma pow_2_pow_i_mem_Di_of_mem_D {F : Type} [NonBinaryField F] [Finite F] {D : Subgroup Fˣ}
   [DIsCyclicC : IsCyclicWithGen ↥D] {x : Fˣ} :
@@ -489,19 +471,17 @@ lemma pow_2_pow_i_mem_Di_of_mem_D {F : Type} [NonBinaryField F] [Finite F] {D :
   unfold evalDomain
   intros a i h
   have h : x⁻¹ * a ∈ Domain.evalDomain D 0 := by aesop_reconcile
-  rw [←Domain.D_def] at h
   have : (x⁻¹ * a) ^ 2 ^ i = (x ^ (2 ^ i))⁻¹ * (a ^ (2 ^ i)) := by field_simp
-  have h := this ▸ Domain.pow_2_pow_i_mem_Di_of_mem_D D (i := i) h
-  aesop_reconcile h
+  simp only [Domain.D_def] at h
+  have := Domain.pow_2_pow_i_mem_Di_of_mem_D D (i := i) h
+  aesop_reconcile
 
 omit [Finite F] in
 lemma sqr_mem_D_succ_i_of_mem_D_i : ∀ {a : Fˣ} {i : ℕ},
     a ∈ evalDomain D x i → a ^ 2 ∈ evalDomain D x (i + 1) := by
   unfold evalDomain
   intros a i h
-  have h : (x ^ 2 ^ i)⁻¹ * a ∈ Domain.evalDomain D i := by
-    apply (mem_leftCoset_iff _).mp
-    aesop
+  have h : (x ^ 2 ^ i)⁻¹ * a ∈ Domain.evalDomain D i := by aesop_reconcile
   have : ((x ^ 2 ^ i)⁻¹ * a) ^ 2 = (x ^ 2 ^ (i + 1))⁻¹ * (a ^ 2) := by
     have : ((x ^ 2 ^ i)⁻¹ * a) ^ 2 = ((x ^ 2 ^ i) ^ 2)⁻¹ * (a ^ 2) := by field_simp
     rw [this]
@@ -510,8 +490,8 @@ lemma sqr_mem_D_succ_i_of_mem_D_i : ∀ {a : Fˣ} {i : ℕ},
       congr 1
       grind
     rw [this]
-  have h := this ▸ Domain.sqr_mem_D_succ_i_of_mem_D_i D h
-  aesop_reconcile h
+  have h := Domain.sqr_mem_D_succ_i_of_mem_D_i D h
+  aesop_reconcile
 
 omit [Finite F] in
 lemma pow_lift : ∀ {a : Fˣ} {i : ℕ} (s : ℕ),
@@ -533,17 +513,17 @@ lemma neg_mem_dom_of_mem_dom : ∀ {a : Fˣ} (i : Fin n),
   unfold evalDomain
   rintro a ⟨i, i_prop⟩ h
   have mem : (x ^ 2 ^ i)⁻¹ * a ∈ Domain.evalDomain D i := by
-    aesop_reconcile h
+    aesop_reconcile
   have : (x ^ 2 ^ i)⁻¹ * -a ∈ ↑(Domain.evalDomain D i) := by
     have : (x ^ 2 ^ i)⁻¹ * -a = ((x ^ 2 ^ i)⁻¹ * a) * (- 1) := by field_simp
     rw [this]
     exact
       (
         Subgroup.mul_mem_cancel_right
-          (Domain.evalDomain D i)
+          _
           (Domain.minus_one_in_doms D i_prop)
       ).mpr mem
-  aesop_reconcile this
+  aesop_reconcile
 
 omit [Finite F] in
 lemma mul_root_of_unity {x : Fˣ} :
@@ -553,21 +533,19 @@ lemma mul_root_of_unity {x : Fˣ} :
   intros a b i j i_le_j a_in b_in
   unfold evalDomain Domain.evalDomain at *
   have : (x ^ 2 ^ i)⁻¹ * a ∈ (Subgroup.zpowers (DIsCyclicC.gen.1 ^ 2 ^ i)) := by
-    apply (mem_leftCoset_iff _).mp
-    convert a_in
-    exact op_der_eq
+    aesop_reconcile
   have : (x ^ 2 ^ i)⁻¹ * (a * b) ∈ (Subgroup.zpowers (DIsCyclicC.gen.1 ^ 2 ^ i)) := by
     rw [Subgroup.mem_zpowers_iff] at b_in this
     rcases this with ⟨ka, a_in⟩
     rcases b_in with ⟨kb, b_in⟩
     apply Subgroup.mem_zpowers_iff.mpr
     exists (ka + (2 ^ (j - i)) * kb)
     rw [
-      ←@mul_assoc Fˣ _ _ a b, ←a_in, ←b_in, zpow_add,
-      Eq.symm (pow_mul_pow_sub 2 i_le_j), pow_mul, zpow_mul
+      ←@mul_assoc _ _ _ a b, ←a_in, ←b_in, zpow_add,
+      (pow_mul_pow_sub 2 i_le_j).symm, pow_mul, zpow_mul
     ]
     norm_cast
-  aesop_reconcile this
+  aesop_reconcile
 
 omit [Finite F] in
 lemma dom_n_eq_triv : evalDomain D x n = {x ^ (2 ^ n)} := by
@@ -577,15 +555,8 @@ lemma dom_n_eq_triv : evalDomain D x n = {x ^ (2 ^ n)} := by
 
 noncomputable local instance : Fintype F := Fintype.ofFinite _
 
-noncomputable instance : Nonempty ↑(CosetDomain.evalDomain D x 0) := by
-  apply Nonempty.intro
-  exact
-    ⟨x,
-    by
-      simp
-      have := (@mem_leftCoset_iff Fˣ _ (Subgroup.zpowers DIsCyclicC.gen.1) x x).mpr (by simp)
-      aesop
-    ⟩
+noncomputable instance : Nonempty ↑(CosetDomain.evalDomain D x 0) := 
+  ⟨x, by aesop_reconcile⟩
 
 noncomputable instance : Fintype ↑(CosetDomain.evalDomain D x 0) := inferInstance