mathlib docs: tactic.omega.int.form

source

meta inductive omega.int.exprform :

Type

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

Intermediate shadow syntax for LNA formulas that includes unreified exprs

source

inductive omega.int.preform :

Type

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

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

source

@[instance]

def omega.int.preform.inhabited :

inhabited omega.int.preform

source

@[instance]

meta def omega.int.preform.has_reflect :

has_reflect omega.int.preform

source

@[simp]

def omega.int.preform.holds :

(ℕ → ℤ) → omega.int.preform → Prop

Evaluate a preform into prop using the valuation v.

Equations

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

source

@[simp]

def omega.int.univ_close :

omega.int.preform → (ℕ → ℤ) → ℕ → Prop

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

Equations

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

source

def omega.int.preform.fresh_index :

omega.int.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.int.preform.le t s).fresh_index = max t.fresh_index s.fresh_index
(omega.int.preform.eq t s).fresh_index = max t.fresh_index s.fresh_index

source

def omega.int.preform.valid :

omega.int.preform → Prop

All valuations satisfy argument

Equations

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

source

def omega.int.preform.sat :

omega.int.preform → Prop

There exists some valuation that satisfies argument

Equations

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

source

def omega.int.preform.implies :

omega.int.preform → omega.int.preform → Prop

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

Equations

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

source

def omega.int.preform.equiv :

omega.int.preform → omega.int.preform → Prop

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

Equations

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

source

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

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

source

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

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

source

def omega.int.preform.unsat :

omega.int.preform → Prop

There does not exist any valuation that satisfies argument

Equations

p.unsat = ¬p.sat

source

def omega.int.preform.repr :

omega.int.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.int.preform.le t s).repr = "(" ++ t.repr ++ " ≤ " ++ s.repr ++ ")"
(omega.int.preform.eq t s).repr = "(" ++ t.repr ++ " = " ++ s.repr ++ ")"

source

@[instance]

def omega.int.preform.has_repr :

has_repr omega.int.preform

Equations

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

source

@[instance]

meta def omega.int.preform.has_to_format :

has_to_format omega.int.preform

source

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

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

source

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

p.not.unsat → p.valid

source

meta def omega.int.preform.induce :

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

Tactic for setting up proof by induction over preforms.

mathlib documentation

tactic.omega.int.form

General documentation

Additional documentation

Library

mathlib documentation

tactic.​omega.​int.​form

General documentation

Additional documentation

Library

tactic.omega.int.form