Commit 2022-11-01 00:14 50ba914c

View on Github →

feat: port abel1 (#509) This is a quick and dirty port of abel1, just a direct translation of what is in Lean 3, with minimal modifications to use the new norm_num. (This PR depends on #507, integer operations for norm_num.) Recall abel1 is the tactic that solves equations; I haven't done the normalizer tactic abel yet, but hopefully it's straightforward from here.

Estimated changes

added theorem ofNat_zsmul
added theorem zero_zsmul
deleted theorem zpow_coe_nat
modified theorem zpow_eq_pow
added theorem zpow_negSucc
deleted theorem zpow_neg_succ_of_nat
added theorem zpow_ofNat
deleted theorem zpow_of_nat
modified theorem zpow_zero
added theorem zsmul_eq_smul
added theorem add_nsmul
added theorem nsmul_zero
added theorem one_nsmul
added theorem one_pow
added theorem coe_nat_zsmul
added theorem zpow_coe_nat
added def Lean.Expr.ofInt
added def Lean.Expr.ofNat
added structure Tactic.Abel.Context
added inductive Tactic.Abel.NormalExpr
added def Tactic.Abel.smul
added def Tactic.Abel.term
added theorem Tactic.Abel.term_atom
added theorem Tactic.Abel.term_atomg
added theorem Tactic.Abel.term_neg
added theorem Tactic.Abel.term_smul
added theorem Tactic.Abel.term_smulg
added theorem Tactic.Abel.unfold_sub
added theorem Tactic.Abel.zero_smul
added theorem Tactic.Abel.zero_smulg
added theorem Tactic.Abel.zero_term
added theorem Tactic.Abel.zero_termg
added def Tactic.abel1Impl
added def id'