Documentation

Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic

This module contains the definition of a generic boolean substructure for SMT problems with BoolExpr. For verification purposes BoolExpr.Sat and BoolExpr.Unsat are provided.

inductive Std.Tactic.BVDecide.Gate :

Instances For

Lean.Elab.Tactic.BVDecide.Frontend.instToExprGate

def Std.Tactic.BVDecide.Gate.toString :

Std.Tactic.BVDecide.Gate → String

Equations

Std.Tactic.BVDecide.Gate.and.toString = "&&"
Std.Tactic.BVDecide.Gate.xor.toString = "^^"
Std.Tactic.BVDecide.Gate.beq.toString = "=="

def Std.Tactic.BVDecide.Gate.eval :

Std.Tactic.BVDecide.Gate → Bool → Bool → Bool

Equations

Std.Tactic.BVDecide.Gate.and.eval = fun (x1 x2 : Bool) => x1 && x2
Std.Tactic.BVDecide.Gate.xor.eval = fun (x1 x2 : Bool) => x1 ^^ x2
Std.Tactic.BVDecide.Gate.beq.eval = fun (x1 x2 : Bool) => x1 == x2

inductive Std.Tactic.BVDecide.BoolExpr (α : Type) :

literal: {α : Type} → α → Std.Tactic.BVDecide.BoolExpr α
const: {α : Type} → Bool → Std.Tactic.BVDecide.BoolExpr α
not: {α : Type} → Std.Tactic.BVDecide.BoolExpr α → Std.Tactic.BVDecide.BoolExpr α
gate: {α : Type} → Std.Tactic.BVDecide.Gate → Std.Tactic.BVDecide.BoolExpr α → Std.Tactic.BVDecide.BoolExpr α → Std.Tactic.BVDecide.BoolExpr α

Instances For

def Std.Tactic.BVDecide.BoolExpr.toString {α : Type} [ToString α] :

Std.Tactic.BVDecide.BoolExpr α → String

Equations

(Std.Tactic.BVDecide.BoolExpr.literal a).toString = toString a
(Std.Tactic.BVDecide.BoolExpr.const b).toString = toString b
x_1.not.toString = "!" ++ x_1.toString
(Std.Tactic.BVDecide.BoolExpr.gate g x_1 y).toString = "(" ++ x_1.toString ++ " " ++ g.toString ++ " " ++ y.toString ++ ")"

instance Std.Tactic.BVDecide.BoolExpr.instToString {α : Type} [ToString α] :

ToString (Std.Tactic.BVDecide.BoolExpr α)

Equations

Std.Tactic.BVDecide.BoolExpr.instToString = { toString := Std.Tactic.BVDecide.BoolExpr.toString }

def Std.Tactic.BVDecide.BoolExpr.size {α : Type} :

Std.Tactic.BVDecide.BoolExpr α → Nat

Equations

(Std.Tactic.BVDecide.BoolExpr.literal a).size = 1
(Std.Tactic.BVDecide.BoolExpr.const b).size = 1
x_1.not.size = x_1.size + 1
(Std.Tactic.BVDecide.BoolExpr.gate g x_1 y).size = x_1.size + y.size + 1

theorem Std.Tactic.BVDecide.BoolExpr.size_pos {α : Type} (x : Std.Tactic.BVDecide.BoolExpr α) :

0 < x.size

def Std.Tactic.BVDecide.BoolExpr.eval {α : Type} (a : α → Bool) :

Std.Tactic.BVDecide.BoolExpr α → Bool

Equations

Std.Tactic.BVDecide.BoolExpr.eval a (Std.Tactic.BVDecide.BoolExpr.literal a_1) = a a_1
Std.Tactic.BVDecide.BoolExpr.eval a (Std.Tactic.BVDecide.BoolExpr.const b) = b
Std.Tactic.BVDecide.BoolExpr.eval a x_1.not = !Std.Tactic.BVDecide.BoolExpr.eval a x_1
Std.Tactic.BVDecide.BoolExpr.eval a (Std.Tactic.BVDecide.BoolExpr.gate g x_1 y) = g.eval (Std.Tactic.BVDecide.BoolExpr.eval a x_1) (Std.Tactic.BVDecide.BoolExpr.eval a y)

@[simp]

theorem Std.Tactic.BVDecide.BoolExpr.eval_literal :

∀ {α : Type} {a : α → Bool} {l : α}, Std.Tactic.BVDecide.BoolExpr.eval a (Std.Tactic.BVDecide.BoolExpr.literal l) = a l

@[simp]

theorem Std.Tactic.BVDecide.BoolExpr.eval_const :

∀ {α : Type} {a : α → Bool} {b : Bool}, Std.Tactic.BVDecide.BoolExpr.eval a (Std.Tactic.BVDecide.BoolExpr.const b) = b

@[simp]

theorem Std.Tactic.BVDecide.BoolExpr.eval_not :

∀ {α : Type} {a : α → Bool} {x : Std.Tactic.BVDecide.BoolExpr α}, Std.Tactic.BVDecide.BoolExpr.eval a x.not = !Std.Tactic.BVDecide.BoolExpr.eval a x

@[simp]

theorem Std.Tactic.BVDecide.BoolExpr.eval_gate :

∀ {α : Type} {a : α → Bool} {g : Std.Tactic.BVDecide.Gate} {x y : Std.Tactic.BVDecide.BoolExpr α}, Std.Tactic.BVDecide.BoolExpr.eval a (Std.Tactic.BVDecide.BoolExpr.gate g x y) = g.eval (Std.Tactic.BVDecide.BoolExpr.eval a x) (Std.Tactic.BVDecide.BoolExpr.eval a y)

def Std.Tactic.BVDecide.BoolExpr.Sat {α : Type} (a : α → Bool) (x : Std.Tactic.BVDecide.BoolExpr α) :

Equations

Std.Tactic.BVDecide.BoolExpr.Sat a x = (Std.Tactic.BVDecide.BoolExpr.eval a x = true)

def Std.Tactic.BVDecide.BoolExpr.Unsat {α : Type} (x : Std.Tactic.BVDecide.BoolExpr α) :

Equations

x.Unsat = ∀ (f : α → Bool), Std.Tactic.BVDecide.BoolExpr.eval f x = false

theorem Std.Tactic.BVDecide.BoolExpr.sat_and {α : Type} {x : Std.Tactic.BVDecide.BoolExpr α} {y : Std.Tactic.BVDecide.BoolExpr α} {a : α → Bool} (hx : Std.Tactic.BVDecide.BoolExpr.Sat a x) (hy : Std.Tactic.BVDecide.BoolExpr.Sat a y) :

Std.Tactic.BVDecide.BoolExpr.Sat a (Std.Tactic.BVDecide.BoolExpr.gate Std.Tactic.BVDecide.Gate.and x y)

theorem Std.Tactic.BVDecide.BoolExpr.sat_true {α : Type} {a : α → Bool} :

Std.Tactic.BVDecide.BoolExpr.Sat a (Std.Tactic.BVDecide.BoolExpr.const true)