tactic.omega.int.form - mathlib docs

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

@[protected, instance]

meta def omega.int.preform.has_reflect :

has_reflect omega.int.preform

source

@[protected, instance]

def omega.int.preform.inhabited :

inhabited omega.int.preform

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

@[simp]

def omega.int.preform.holds (v : ℕ → ℤ) :

omega.int.preform → Prop

Evaluate a preform into prop using the valuation v.

Equations

omega.int.preform.holds v (p ∧* q) = (omega.int.preform.holds v p ∧ omega.int.preform.holds v q)
omega.int.preform.holds v (p ∨* q) = (omega.int.preform.holds v p ∨ omega.int.preform.holds v q)
omega.int.preform.holds v (¬* p) = ¬omega.int.preform.holds v p
omega.int.preform.holds v (t ≤* s) = (omega.int.preterm.val v t ≤ omega.int.preterm.val v s)
omega.int.preform.holds v (t =* s) = (omega.int.preterm.val v t = omega.int.preterm.val v s)

source

@[simp]

def omega.int.univ_close (p : 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 ∧* q).fresh_index = max p.fresh_index q.fresh_index
(p ∨* q).fresh_index = max p.fresh_index q.fresh_index
(¬* p).fresh_index = p.fresh_index
(t ≤* s).fresh_index = max t.fresh_index s.fresh_index
(t =* s).fresh_index = max t.fresh_index s.fresh_index

source

def omega.int.preform.valid (p : omega.int.preform) :

Prop

All valuations satisfy argument

Equations

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

source

def omega.int.preform.sat (p : 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 (p q : 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 (p q : 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 ∨* q).sat ↔ p.sat ∨ q.sat

source

def omega.int.preform.unsat (p : 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 ∧* q).repr = "(" ++ p.repr ++ " ∧ " ++ q.repr ++ ")"
(p ∨* q).repr = "(" ++ p.repr ++ " ∨ " ++ q.repr ++ ")"
(¬* p).repr = "¬" ++ p.repr
(t ≤* s).repr = "(" ++ t.repr ++ " ≤ " ++ s.repr ++ ")"
(t =* s).repr = "(" ++ t.repr ++ " = " ++ s.repr ++ ")"

source

@[protected, instance]

def omega.int.preform.has_repr :

has_repr omega.int.preform

Equations

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

source

@[protected, 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).unsat → p.valid

source

meta def omega.int.preform.induce (t : tactic unit := tactic.skip) :

tactic unit

Tactic for setting up proof by induction over preforms.