tactic.omega.nat.form - mathlib docs

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

@[protected, instance]

def omega.nat.preform.inhabited :

inhabited omega.nat.preform

source

@[protected, instance]

meta def omega.nat.preform.has_reflect :

has_reflect omega.nat.preform

source

@[simp]

def omega.nat.preform.holds (v : ℕ → ℕ) :

omega.nat.preform → Prop

Evaluate a preform into prop using the valuation v.

Equations

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

source

@[simp]

def omega.nat.univ_close (p : 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 ∧* q).neg_free = (p.neg_free ∧ q.neg_free)
(p ∨* q).neg_free = (p.neg_free ∧ q.neg_free)
(¬* ᾰ).neg_free = false
(t ≤* s).neg_free = true
(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 ∧* q).sub_free = (p.sub_free ∧ q.sub_free)
(p ∨* q).sub_free = (p.sub_free ∧ q.sub_free)
(¬* p).sub_free = p.sub_free
(t ≤* s).sub_free = (t.sub_free ∧ s.sub_free)
(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 ∧* 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

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 (p : omega.nat.preform) :

Prop

All valuations satisfy argument

Equations

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

source

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

source

def omega.nat.preform.unsat (p : 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 ∧* 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.nat.preform.has_repr :

has_repr omega.nat.preform

Equations

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

source

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

source

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

tactic unit

Tactic for setting up proof by induction over preforms.