Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-17 11:03 3f4b154a

View on Github →

feat(tactic/omega): tactic for linear integer & natural number arithmetic (#827)

  • feat(tactic/omega): tactic for discharging linear integer and natural number arithmetic goals
  • refactor(tactic/omega): clean up namespace and notations
  • Update src/data/list/func.lean Co-Authored-By: skbaek seulkeebaek@gmail.com
  • Add changed files
  • Refactor val_between_map_div
  • Use default inhabitants for list.func

Estimated changes

added theorem int.add_div_of_dvd
added theorem int.default_eq_zero
modified theorem list.Ico.filter_ge
added theorem list.func.add_nil
added theorem list.func.eq_of_equiv
added theorem list.func.equiv_of_eq
added theorem list.func.equiv_refl
added theorem list.func.equiv_symm
added theorem list.func.equiv_trans
added theorem list.func.get_add
added theorem list.func.get_map'
added theorem list.func.get_map
added theorem list.func.get_neg
added theorem list.func.get_nil
added theorem list.func.get_set
added theorem list.func.get_sub
added theorem list.func.length_add
added theorem list.func.length_neg
added theorem list.func.length_set
added theorem list.func.length_sub
added theorem list.func.map_add_map
added theorem list.func.nil_add
added theorem list.func.nil_sub
added theorem list.func.sub_nil
added def list.func.add
added def list.func.equiv
added def list.func.get
added def list.func.neg
added def list.func.set
added def list.func.sub
added theorem nat.lt_iff_add_one_le
added theorem nat.max_succ_succ
added theorem nat.zero_max
added def omega.clause.sat
added def omega.clause
added theorem omega.coeffs.dvd_val
added def omega.coeffs.val
added theorem omega.coeffs.val_add
added theorem omega.coeffs.val_neg
added theorem omega.coeffs.val_nil
added theorem omega.coeffs.val_sub
added def omega.cancel
added def omega.ee.repr
added inductive omega.ee
added def omega.eq_elim
added theorem omega.mul_symdiv_eq
added def omega.rhs
added theorem omega.rhs_correct
added theorem omega.rhs_correct_aux
added theorem omega.sat_empty
added theorem omega.sat_eq_elim
added def omega.sgm
added def omega.subst
added theorem omega.subst_correct
added def omega.sym_sym
added def omega.symdiv
added def omega.symmod
added theorem omega.symmod_eq
added def omega.gcd
added def omega.int.dnf
added def omega.int.is_nnf
added theorem omega.int.is_nnf_nnf
added def omega.int.nnf
added theorem omega.int.nnf_equiv
added theorem omega.int.form.sat_or
added inductive omega.int.form
added inductive omega.int.preterm
added theorem omega.int.val_canonize
added def omega.lin_comb
added theorem omega.lin_comb_holds
added theorem omega.fun_mono_2
added theorem omega.pred_mono_2'
added theorem omega.pred_mono_2
added def omega.update
added theorem omega.update_eq
added theorem omega.update_eq_of_ne
added def omega.nat.dnf
added theorem omega.nat.form.sat_or
added inductive omega.nat.form
added def omega.nat.is_nnf
added theorem omega.nat.is_nnf_nnf
added def omega.nat.nnf
added theorem omega.nat.nnf_equiv
added inductive omega.nat.preterm
added theorem omega.nat.val_canonize
added theorem omega.nat.sat_sub_elim
added def omega.term.add
added def omega.term.div
added def omega.term.mul
added def omega.term.neg
added def omega.term.sub
added def omega.term.val
added theorem omega.term.val_add
added theorem omega.term.val_div
added theorem omega.term.val_mul
added theorem omega.term.val_neg
added theorem omega.term.val_sub
added def omega.term