mathlib documentation

tactic.omega.nat.main

meta def simp_attr.sugar_nat :

(user_attribute simp_lemmas)

meta def omega.nat.desugar :

theorem omega.nat.univ_close_of_unsat_neg_elim_not (m : ℕ) (p : omega.nat.preform) :

(omega.nat.neg_elim (¬* p)).unsat → omega.nat.univ_close p (λ (_x : ℕ), 0) m

meta def omega.nat.preterm.prove_sub_free :

omega.nat.preterm → tactic expr

Return expr of proof that argument is free of subtractions

meta def omega.nat.prove_neg_free :

omega.nat.preform → tactic expr

Return expr of proof that argument is free of negations

meta def omega.nat.prove_sub_free :

omega.nat.preform → tactic expr

Return expr of proof that argument is free of subtractions

meta def omega.nat.prove_unsat_sub_free (p : omega.nat.preform) :

Given a p : preform, return the expr of a term t : p.unsat, where p is subtraction- and negation-free.

meta def omega.nat.prove_unsat_neg_free :

omega.nat.preform → tactic expr

Given a p : preform, return the expr of a term t : p.unsat, where p is negation-free.

meta def omega.nat.prove_univ_close (m : ℕ) (p : omega.nat.preform) :

Given a (m : nat) and (p : preform), return the expr of (t : univ_close m p).

meta def omega.nat.to_exprterm :

expr → tactic omega.nat.exprterm

Reification to imtermediate shadow syntax that retains exprs

meta def omega.nat.to_exprform :

expr → tactic omega.nat.exprform

Reification to imtermediate shadow syntax that retains exprs

meta def omega.nat.exprterm.exprs :

omega.nat.exprterm → list expr

List of all unreified exprs

meta def omega.nat.exprform.exprs :

omega.nat.exprform → list expr

List of all unreified exprs

meta def omega.nat.exprterm.to_preterm (xs : list expr) :

omega.nat.exprterm → tactic omega.nat.preterm

Reification to an intermediate shadow syntax which eliminates exprs, but still includes non-canonical terms

meta def omega.nat.exprform.to_preform (xs : list expr) :

omega.nat.exprform → tactic omega.nat.preform

Reification to an intermediate shadow syntax which eliminates exprs, but still includes non-canonical terms

meta def omega.nat.to_preform (x : expr) :

tactic (omega.nat.preform × ℕ)

Reification to an intermediate shadow syntax which eliminates exprs, but still includes non-canonical terms.

meta def omega.nat.prove :

Return expr of proof of current LNA goal

meta def omega.nat.eq_nat (x : expr) :

Succeed iff argument is expr of ℕ

meta def omega.nat.wff :

expr → tactic unit

Check whether argument is expr of a well-formed formula of LNA

meta def omega.nat.wfx (x : expr) :

Succeed iff argument is expr of term whose type is wff

meta def omega.nat.intro_nats_core :

Intro all universal quantifiers over nat

meta def omega.nat.intro_nats :

meta def omega.nat.preprocess :

If the goal has universal quantifiers over natural, introduce all of them. Otherwise, revert all hypotheses that are formulas of linear natural number arithmetic.

meta def omega_nat (is_manual : bool) :

The core omega tactic for natural numbers.