more

ECTate/Algebra/EllipticCurve/CubicRoots.lean

@@ -12,35 +12,6 @@ import Mathlib.Algebra.EuclideanDomain.Instances
 import Mathlib.Algebra.EuclideanDomain.Basic
 
 
-namespace Mathlib
-open Lean hiding Rat mkRat
-open Meta
-
-namespace Meta.NormNum
-open Qq
--- TODO move to mathlib next to mod
-
-theorem isNat_natDiv : {a b : ℕ} → {a' b' c : ℕ} →
-    IsNat a a' → IsNat b b' → Nat.div a' b' = c → IsNat (a / b) c
-  | _, _, _, _, _, ⟨rfl⟩, ⟨rfl⟩, rfl => ⟨by aesop⟩
-
-/-- The `norm_num` extension which identifies expressions of the form `Nat.div a b`,
-such that `norm_num` successfully recognises both `a` and `b`. -/
-@[norm_num (_ : ℕ) % _, HDiv.hDiv (_ : ℕ) _, Nat.div _ _] def evalNatDiv :
-    NormNumExt where eval {u α} e := do
-  let .app (.app f (a : Q(ℕ))) (b : Q(ℕ)) ← whnfR e | failure
-  -- We trust that the default instance for `HDiv` is `Nat.div` when the first parameter is `ℕ`.
-  guard <|← withNewMCtxDepth <| isDefEq f q(HDiv.hDiv (α := ℕ))
-  let sℕ : Q(AddMonoidWithOne ℕ) := q(instAddMonoidWithOneNat)
-  let ⟨na, pa⟩ ← deriveNat a sℕ; let ⟨nb, pb⟩ ← deriveNat b sℕ
-  have pa : Q(IsNat $a $na) := pa
-  have pb : Q(IsNat $b $nb) := pb
-  have nc : Q(ℕ) := mkRawNatLit (na.natLit! / nb.natLit!)
-  let r : Q(Nat.div $na $nb = $nc) := (q(Eq.refl $nc) : Expr)
-  return (.isNat sℕ nc q(isNat_natDiv $pa $pb $r) : Result q($a / $b))
-end Meta.NormNum
-end Mathlib
-
 
 namespace Field
 variable {K : Type u} [Field K]
@@ -106,6 +77,8 @@ by
     rw [← Nat.cast_ofNat (R := ℤ), ← Nat.mod_add_div 2 (ringChar K)]
     simp
     simp [heq] -- TODO why no nat mod self fires
+    -- change (a * b + c) ^ 2 = 0 at hd
+    -- simp at hd
     sorry
 
   . rename_i heq

ECTate/Tactic/FactorAs.lean

@@ -15,3 +15,5 @@ on the goal -a - b + a * b + 1
 example [CommRing R] (r : R) : r + r^2 + 1 = 0 :=
 by
   convert_to (r + 1) ^ 2 = 0
+  admit
+  admit

lake-manifest.json

@@ -2,9 +2,15 @@
  "packagesDir": "lake-packages",
  "packages":
  [{"git":
+   {"url": "https://github.com/EdAyers/ProofWidgets4",
+    "subDir?": null,
+    "rev": "3b157dc3f6162615de001a8ebe7e01d629c97448",
+    "name": "proofwidgets",
+    "inputRev?": "v0.0.10"}},
+  {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "331093523301e692e51c6de01319c299787efdd5",
+    "rev": "28f3fa38884fd766d4ba9f5813d7efdc994ed470",
     "name": "mathlib",
     "inputRev?": null}},
   {"git":
@@ -16,12 +22,12 @@
   {"git":
    {"url": "https://github.com/JLimperg/aesop",
     "subDir?": null,
-    "rev": "409f3b050034337664d21e41fe1cc1bf7f5daec0",
+    "rev": "ca73109cc40837bc61df8024c9016da4b4f99d4c",
     "name": "aesop",
     "inputRev?": "master"}},
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "3156cd5b375d1a932d590c918b7ad50e3be11947",
+    "rev": "6932c4ea52914dc6b0488944e367459ddc4d01a6",
     "name": "std",
     "inputRev?": "main"}}]}

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2023-05-16
+leanprover/lean4:nightly-2023-05-31

test/testspecialize.lean

@@ -15,7 +15,7 @@ def h (R : Type _) [Ring R] (l : List R) : R := match l with
 | [] => 0
 | a :: l => a + h R l
 
-set_option trace.compiler true
+-- set_option trace.compiler true
 @[specialize ℤ]
 def f := h
 

test/tet.lean

@@ -4,8 +4,8 @@ import Mathlib.Data.Nat.Basic
 
 #check List.replicate
 open List
-set_option trace.compiler true
-set_option trace.Compiler true
+-- set_option trace.compiler true
+-- set_option trace.Compiler true
 def f (n : ℕ) := List.sum $ List.replicate n (1 : ℤ)
 
 def g (R : Type _) [Ring R] (n : ℕ) : R := List.sum $ List.replicate n (1 : R)