mathlib docs: tactic.omega.nat.form

source

meta inductive omega.nat.exprform :

Type

eq : omega.nat.exprterm → omega.nat.exprterm → omega.nat.exprform
le : omega.nat.exprterm → omega.nat.exprterm → omega.nat.exprform
not : omega.nat.exprform → omega.nat.exprform
or : omega.nat.exprform → omega.nat.exprform → omega.nat.exprform
and : omega.nat.exprform → omega.nat.exprform → omega.nat.exprform

Intermediate shadow syntax for LNA formulas that includes unreified exprs

source

inductive omega.nat.preform :

Type

eq : omega.nat.preterm → omega.nat.preterm → omega.nat.preform
le : omega.nat.preterm → omega.nat.preterm → omega.nat.preform
not : omega.nat.preform → omega.nat.preform
or : omega.nat.preform → omega.nat.preform → omega.nat.preform
and : omega.nat.preform → omega.nat.preform → omega.nat.preform

Intermediate shadow syntax for LNA formulas that includes non-canonical terms

source

@[instance]

def omega.nat.preform.inhabited :

inhabited omega.nat.preform

source

@[instance]

meta def omega.nat.preform.has_reflect :

has_reflect omega.nat.preform

source

@[simp]

def omega.nat.preform.holds :

(ℕ → ℕ) → omega.nat.preform → Prop

Evaluate a preform into prop using the valuation v.

Equations

omega.nat.preform.holds v (p.and q) = (omega.nat.preform.holds v p ∧ omega.nat.preform.holds v q)
omega.nat.preform.holds v (p.or q) = (omega.nat.preform.holds v p ∨ omega.nat.preform.holds v q)
omega.nat.preform.holds v p.not = ¬omega.nat.preform.holds v p
omega.nat.preform.holds v (omega.nat.preform.le t s) = (omega.nat.preterm.val v t ≤ omega.nat.preterm.val v s)
omega.nat.preform.holds v (omega.nat.preform.eq t s) = (omega.nat.preterm.val v t = omega.nat.preterm.val v s)

source

@[simp]

def omega.nat.univ_close :

omega.nat.preform → (ℕ → ℕ) → ℕ → Prop

univ_close p n := p closed by prepending n universal quantifiers

Equations

omega.nat.univ_close p v (k + 1) = ∀ (i : ℕ), omega.nat.univ_close p (omega.update_zero i v) k
omega.nat.univ_close p v 0 = omega.nat.preform.holds v p

source

def omega.nat.preform.neg_free :

omega.nat.preform → Prop

Argument is free of negations

Equations

(p.and q).neg_free = (p.neg_free ∧ q.neg_free)
(p.or q).neg_free = (p.neg_free ∧ q.neg_free)
a.not.neg_free = false
(omega.nat.preform.le t s).neg_free = true
(omega.nat.preform.eq t s).neg_free = true

source

def omega.nat.preform.sub_free :

omega.nat.preform → Prop

Return expr of proof that argument is free of subtractions

Equations

(p.and q).sub_free = (p.sub_free ∧ q.sub_free)
(p.or q).sub_free = (p.sub_free ∧ q.sub_free)
p.not.sub_free = p.sub_free
(omega.nat.preform.le t s).sub_free = (t.sub_free ∧ s.sub_free)
(omega.nat.preform.eq t s).sub_free = (t.sub_free ∧ s.sub_free)

source

def omega.nat.preform.fresh_index :

omega.nat.preform → ℕ

Fresh de Brujin index not used by any variable in argument

Equations

(p.and q).fresh_index = max p.fresh_index q.fresh_index
(p.or q).fresh_index = max p.fresh_index q.fresh_index
p.not.fresh_index = p.fresh_index
(omega.nat.preform.le t s).fresh_index = max t.fresh_index s.fresh_index
(omega.nat.preform.eq t s).fresh_index = max t.fresh_index s.fresh_index

source

theorem omega.nat.preform.holds_constant {v w : ℕ → ℕ} (p : omega.nat.preform) :

(∀ (x : ℕ), x < p.fresh_index → v x = w x) → (omega.nat.preform.holds v p ↔ omega.nat.preform.holds w p)

source

def omega.nat.preform.valid :

omega.nat.preform → Prop

All valuations satisfy argument

Equations

p.valid = ∀ (v : ℕ → ℕ), omega.nat.preform.holds v p

source

def omega.nat.preform.sat :

omega.nat.preform → Prop

There exists some valuation that satisfies argument

Equations

p.sat = ∃ (v : ℕ → ℕ), omega.nat.preform.holds v p

source

def omega.nat.preform.implies :

omega.nat.preform → omega.nat.preform → Prop

implies p q := under any valuation, q holds if p holds

Equations

p.implies q = ∀ (v : ℕ → ℕ), omega.nat.preform.holds v p → omega.nat.preform.holds v q

source

def omega.nat.preform.equiv :

omega.nat.preform → omega.nat.preform → Prop

equiv p q := under any valuation, p holds iff q holds

Equations

p.equiv q = ∀ (v : ℕ → ℕ), omega.nat.preform.holds v p ↔ omega.nat.preform.holds v q

source

theorem omega.nat.preform.sat_of_implies_of_sat {p q : omega.nat.preform} :

p.implies q → p.sat → q.sat

source

theorem omega.nat.preform.sat_or {p q : omega.nat.preform} :

(p.or q).sat ↔ p.sat ∨ q.sat

source

def omega.nat.preform.unsat :

omega.nat.preform → Prop

There does not exist any valuation that satisfies argument

Equations

p.unsat = ¬p.sat

source

def omega.nat.preform.repr :

omega.nat.preform → string

Equations

(p.and q).repr = "(" ++ p.repr ++ " ∧ " ++ q.repr ++ ")"
(p.or q).repr = "(" ++ p.repr ++ " ∨ " ++ q.repr ++ ")"
p.not.repr = "¬" ++ p.repr
(omega.nat.preform.le t s).repr = "(" ++ t.repr ++ " ≤ " ++ s.repr ++ ")"
(omega.nat.preform.eq t s).repr = "(" ++ t.repr ++ " = " ++ s.repr ++ ")"

source

@[instance]

def omega.nat.preform.has_repr :

has_repr omega.nat.preform

Equations

omega.nat.preform.has_repr = {repr := omega.nat.preform.repr}

source

@[instance]

meta def omega.nat.preform.has_to_format :

has_to_format omega.nat.preform

source

theorem omega.nat.univ_close_of_valid {p : omega.nat.preform} {m : ℕ} {v : ℕ → ℕ} :

p.valid → omega.nat.univ_close p v m

source

theorem omega.nat.valid_of_unsat_not {p : omega.nat.preform} :

p.not.unsat → p.valid

source

meta def omega.nat.preform.induce :

(tactic unit := tactic.skip) → tactic unit

Tactic for setting up proof by induction over preforms.

mathlib documentation

tactic.omega.nat.form

General documentation

Additional documentation

Library

mathlib documentation

tactic.​omega.​nat.​form

General documentation

Additional documentation

Library

tactic.omega.nat.form