tactic.omega.nat.sub_elim

source

def omega.nat.preterm.sub_terms :

omega.nat.preterm → option (omega.nat.preterm × omega.nat.preterm)

Find subtraction inside preterm and return its operands

Equations

(t -* s).sub_terms = (t.sub_terms <|> s.sub_terms <|> some (t, s))
(t +* s).sub_terms = (t.sub_terms <|> s.sub_terms)
(i ** n).sub_terms = none
(&i).sub_terms = none

source

def omega.nat.preterm.sub_subst (t s : omega.nat.preterm) (k : ℕ) :

omega.nat.preterm → omega.nat.preterm

Find (t - s) inside a preterm and replace it with variable k

Equations

t.sub_subst s k (x -* y) = ite (x = t ∧ y = s) (1 ** k) (t.sub_subst s k x -* t.sub_subst s k y)
t.sub_subst s k (x +* y) = (t.sub_subst s k x +* t.sub_subst s k y)
t.sub_subst s k (m ** n) = m ** n
t.sub_subst s k (&m) = &m

source

theorem omega.nat.preterm.val_sub_subst {k : ℕ} {x y : omega.nat.preterm} {v : ℕ → ℕ} {t : omega.nat.preterm} :

t.fresh_index ≤ k → omega.nat.preterm.val v ⟨k ↦ omega.nat.preterm.val v x - omega.nat.preterm.val v y⟩ (x.sub_subst y k t) = omega.nat.preterm.val v t

source

def omega.nat.preform.sub_terms :

omega.nat.preform → option (omega.nat.preterm × omega.nat.preterm)

Find subtraction inside preform and return its operands

Equations

(p ∧* q).sub_terms = (p.sub_terms <|> q.sub_terms)
(p ∨* q).sub_terms = (p.sub_terms <|> q.sub_terms)
(¬* p).sub_terms = p.sub_terms
(t ≤* s).sub_terms = (t.sub_terms <|> s.sub_terms)
(t =* s).sub_terms = (t.sub_terms <|> s.sub_terms)

source

@[simp]

def omega.nat.preform.sub_subst (x y : omega.nat.preterm) (k : ℕ) :

omega.nat.preform → omega.nat.preform

Find (t - s) inside a preform and replace it with variable k

Equations

omega.nat.preform.sub_subst x y k (p ∧* q) = (omega.nat.preform.sub_subst x y k p ∧* omega.nat.preform.sub_subst x y k q)
omega.nat.preform.sub_subst x y k (p ∨* q) = (omega.nat.preform.sub_subst x y k p ∨* omega.nat.preform.sub_subst x y k q)
omega.nat.preform.sub_subst x y k (¬* p) = ¬* omega.nat.preform.sub_subst x y k p
omega.nat.preform.sub_subst x y k (t ≤* s) = (x.sub_subst y k t ≤* x.sub_subst y k s)
omega.nat.preform.sub_subst x y k (t =* s) = (x.sub_subst y k t =* x.sub_subst y k s)

source

def omega.nat.is_diff (t s : omega.nat.preterm) (k : ℕ) :

omega.nat.preform

Preform which asserts that the value of variable k is the truncated difference between preterms t and s

Equations

omega.nat.is_diff t s k = (t =* (s +* 1 ** k) ∨* (t ≤* s ∧* (1 ** k =* &0)))

source

theorem omega.nat.holds_is_diff {t s : omega.nat.preterm} {k : ℕ} {v : ℕ → ℕ} :

v k = omega.nat.preterm.val v t - omega.nat.preterm.val v s → omega.nat.preform.holds v (omega.nat.is_diff t s k)

source

def omega.nat.sub_elim_core (t s : omega.nat.preterm) (k : ℕ) (p : omega.nat.preform) :

omega.nat.preform

Helper function for sub_elim

Equations

omega.nat.sub_elim_core t s k p = (omega.nat.preform.sub_subst t s k p ∧* omega.nat.is_diff t s k)

source

def omega.nat.sub_fresh_index (t s : omega.nat.preterm) (p : omega.nat.preform) :

ℕ

Return de Brujin index of fresh variable that does not occur in any of the arguments

Equations

omega.nat.sub_fresh_index t s p = max p.fresh_index (max t.fresh_index s.fresh_index)

source

def omega.nat.sub_elim (t s : omega.nat.preterm) (p : omega.nat.preform) :

omega.nat.preform

Return a new preform with all subtractions eliminated

Equations

omega.nat.sub_elim t s p = omega.nat.sub_elim_core t s (omega.nat.sub_fresh_index t s p) p

source

theorem omega.nat.sub_subst_equiv {k : ℕ} {x y : omega.nat.preterm} {v : ℕ → ℕ} (p : omega.nat.preform) :

p.fresh_index ≤ k → (omega.nat.preform.holds v ⟨k ↦ omega.nat.preterm.val v x - omega.nat.preterm.val v y⟩ (omega.nat.preform.sub_subst x y k p) ↔ omega.nat.preform.holds v p)

source

theorem omega.nat.sat_sub_elim {t s : omega.nat.preterm} {p : omega.nat.preform} :

p.sat → (omega.nat.sub_elim t s p).sat

source

theorem omega.nat.unsat_of_unsat_sub_elim (t s : omega.nat.preterm) (p : omega.nat.preform) :

(omega.nat.sub_elim t s p).unsat → p.unsat