Documentation

@[implicit_reducible]

instance Pointer.instLE {m : ℕ} :

LE (Pointer m)

Equations

Pointer.instLE = { le := Pointer.le }

@[implicit_reducible]

instance Pointer.instDecidableLe {m : ℕ} :

DecidableLE (Pointer m)

Equations

(Pointer.terminal a).instDecidableLe (Pointer.terminal a_1) = match a.instDecidableLe a_1 with | isTrue ht => isTrue ⋯ | isFalse hf => isFalse ⋯
(Pointer.terminal a).instDecidableLe (Pointer.node a_1) = isTrue ⋯
(Pointer.node a).instDecidableLe (Pointer.terminal a_1) = isFalse ⋯
(Pointer.node a).instDecidableLe (Pointer.node a_1) = match a.decLe a_1 with | isTrue ht => isTrue ⋯ | isFalse hf => isFalse ⋯

structure Node (n m : ℕ) :

BDD node

var : Fin n
low : Pointer m
high : Pointer m

Instances For

@[implicit_reducible]

instance instDecidableEqNode {n✝ m✝ : ℕ} :

DecidableEq (Node n✝ m✝)

Equations

instDecidableEqNode = instDecidableEqNode.decEq

def instDecidableEqNode.decEq {n✝ m✝ : ℕ} (x✝ x✝¹ : Node n✝ m✝) :

Decidable (x✝ = x✝¹)

Equations

One or more equations did not get rendered due to their size.

Instances For

def instReprNode.repr {n✝ m✝ : ℕ} :

Node n✝ m✝ → ℕ → Std.Format

Equations

One or more equations did not get rendered due to their size.

Instances For

@[implicit_reducible]

instance instReprNode {n✝ m✝ : ℕ} :

Repr (Node n✝ m✝)

Equations

instReprNode = { reprPrec := instReprNode.repr }

@[implicit_reducible]

instance Node.instToString {n m : ℕ} :

ToString (Node n m)

Equations

Node.instToString = { toString := fun (N : Node n m) => "⟨" ++ toString N.var ++ ", " ++ toString N.low ++ ", " ++ toString N.high ++ "⟩" }

structure Bdd (n m : ℕ) :

Raw BDD

heap : Vector (Node n m) m
root : Pointer m

Instances For

def instDecidableEqBdd.decEq {n✝ m✝ : ℕ} (x✝ x✝¹ : Bdd n✝ m✝) :

Decidable (x✝ = x✝¹)

Equations

instDecidableEqBdd.decEq { heap := a, root := a_1 } { heap := b, root := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

Instances For

@[implicit_reducible]

instance instDecidableEqBdd {n✝ m✝ : ℕ} :

DecidableEq (Bdd n✝ m✝)

Equations

instDecidableEqBdd = instDecidableEqBdd.decEq

@[implicit_reducible]

instance Bdd.instToString {n m : ℕ} :

ToString (Bdd n m)

Equations

Bdd.instToString = { toString := fun (B : Bdd n m) => "⟨" ++ toString B.heap ++ ", " ++ toString B.root ++ "⟩" }

inductive Edge {n m : ℕ} (M : Vector (Node n m) m) :

Pointer m → Pointer m → Prop

low {n m : ℕ} {M : Vector (Node n m) m} {j : Fin m} : Edge M (Pointer.node j) M[j].low
high {n m : ℕ} {M : Vector (Node n m) m} {j : Fin m} : Edge M (Pointer.node j) M[j].high

Instances For

theorem edge_iff {n m : ℕ} {M : Vector (Node n m) m} {p q : Pointer m} :

Edge M p q ↔ ∃ (j : Fin m), p = Pointer.node j ∧ (q = M[j].low ∨ q = M[j].high)

theorem not_terminal_edge {n✝ n✝¹ : ℕ} {w : Vector (Node n✝ n✝¹) n✝¹} {b : Bool} {q : Pointer n✝¹} :

¬Edge w (Pointer.terminal b) q

Terminals have no outgoing edges.

def Pointer.toVar {n m : ℕ} (M : Vector (Node n m) m) :

Pointer m → Fin n.succ

Equations

Pointer.toVar M (Pointer.terminal a) = Fin.last n
Pointer.toVar M (Pointer.node a) = ⟨↑M[a].var, ⋯⟩

Instances For

@[simp]

theorem Pointer.toVar_terminal_eq {b : Bool} {n m : ℕ} (w : Vector (Node n m) m) :

toVar w (terminal b) = ⟨n, ⋯⟩

@[simp]

theorem Pointer.toVar_node_eq {n m : ℕ} (w : Vector (Node n m) m) {j : Fin m} :

↑(toVar w (node j)) = ↑w[j].var

theorem Pointer.toVar_heap_set {n n✝ : ℕ} {M : Vector (Node n✝ n) n} {N : Node n✝ n} {i j : Fin n} :

i ≠ j → ↑(toVar (M.set (↑i) N ⋯) (node j)) = ↑(toVar M (node j))

theorem Pointer.toVar_heap_set' {n n✝ : ℕ} {M : Vector (Node n✝ n) n} {N : Node n✝ n} {i j : Fin n} :

i ≠ j → toVar (M.set (↑i) N ⋯) (node j) = toVar M (node j)

def Pointer.MayPrecede {n m : ℕ} (M : Vector (Node n m) m) (p q : Pointer m) :

Equations

Pointer.MayPrecede M p q = (Pointer.toVar M p < Pointer.toVar M q)

Instances For

theorem Pointer.not_terminal_MayPrecede {n✝ n✝¹ : ℕ} {M : Vector (Node n✝ n✝¹) n✝¹} {b : Bool} {p : Pointer n✝¹} :

¬MayPrecede M (terminal b) p

Terminals must not precede other pointers.

theorem Pointer.MayPrecede_node_terminal {b : Bool} {n m : ℕ} (w : Vector (Node n m) m) {j : Fin m} :

MayPrecede w (node j) (terminal b)

Non-terminals may precede terminals.

def Pointer.Reachable {n m : ℕ} (w : Vector (Node n m) m) (a : Pointer m) :

Pointer m → Prop

Equations

Pointer.Reachable w = Relation.ReflTransGen (Edge w)

Instances For

theorem Pointer.Reachable.trans {n✝ n✝¹ : ℕ} {v : Vector (Node n✝ n✝¹) n✝¹} {a b c : Pointer n✝¹} (hab : Reachable v a b) (hbc : Reachable v b c) :

Reachable v a c

@[reducible, inline]

abbrev Bdd.RelevantPointer {n m : ℕ} (B : Bdd n m) :

B.RelevantPointer is the subtype of pointers reachable from B.root.

Equations

B.RelevantPointer = { q : Pointer m // Pointer.Reachable B.heap B.root q }

Instances For

@[implicit_reducible]

instance Bdd.instDecidableEqRelevantPointer {n✝ m✝ : ℕ} {B : Bdd n✝ m✝} :

DecidableEq B.RelevantPointer

Equations

Bdd.instDecidableEqRelevantPointer x✝¹ x✝ = decidable_of_iff (↑x✝¹ = ↑x✝) ⋯

def Bdd.toRelevantPointer {n m : ℕ} (B : Bdd n m) :

B.RelevantPointer

Equations

B.toRelevantPointer = ⟨B.root, ⋯⟩

Instances For

@[reducible, inline]

abbrev Bdd.RelevantEdge {n m : ℕ} (B : Bdd n m) (p q : B.RelevantPointer) :

The Edge relation lifted to RelevantPointers.

Equations

B.RelevantEdge p q = Edge B.heap ↑p ↑q

Instances For

theorem Bdd.relevantEdge_of_edge_of_reachable {n m : ℕ} {p q : Pointer m} {B : Bdd n m} (e : Edge B.heap p q) (hp : Pointer.Reachable B.heap B.root p) :

B.RelevantEdge ⟨p, hp⟩ ⟨q, ⋯⟩

def Bdd.RelevantMayPrecede {n m : ℕ} (B : Bdd n m) (p q : B.RelevantPointer) :

The MayPrecede relation lifted to RelevantPointers.

Equations

B.RelevantMayPrecede p q = Pointer.MayPrecede B.heap ↑p ↑q

Instances For

def Bdd.Ordered {n m : ℕ} (B : Bdd n m) :

A BDD is Ordered if all edges relevant from the root respect the variable ordering.

Equations

B.Ordered = Subrelation B.RelevantEdge B.RelevantMayPrecede

Instances For

theorem Bdd.Ordered_of_terminal {n✝ n✝¹ : ℕ} {M : Vector (Node n✝ n✝¹) n✝¹} {b : Bool} :

{ heap := M, root := Pointer.terminal b }.Ordered

Terminals induce Ordered BDDs.

theorem Bdd.Ordered_of_terminal' {n m : ℕ} {b : Bool} {B : Bdd n m} :

B.root = Pointer.terminal b → B.Ordered

def OBdd (n m : ℕ) :

Equations

OBdd n m = { B : Bdd n m // B.Ordered }

Instances For

def OEdge {n m : ℕ} (O U : OBdd n m) :

Equations

OEdge O U = ((↑O).heap = (↑U).heap ∧ Edge (↑O).heap (↑O).root (↑U).root)

Instances For

def Bdd.var {n m : ℕ} (B : Bdd n m) :

Fin n.succ

Equations

B.var = Pointer.toVar B.heap B.root

Instances For

def OBdd.var {n m : ℕ} (O : OBdd n m) :

Equations

O.var = ↑(↑O).var

Instances For

def OBdd.rav {n m : ℕ} (B : OBdd n m) :

Equations

B.rav = n - B.var

Instances For

theorem OEdge.wellFounded {n m : ℕ} :

WellFounded OEdge

The OEdge relation between Ordered BDDs is well-founded.

theorem OEdge.flip_wellFounded {n m : ℕ} :

WellFounded (flip OEdge)

The OEdge relation between Ordered BDDs is converse well-founded.

@[implicit_reducible]

instance OEdge.instWellFoundedRelation {n m : ℕ} :

WellFoundedRelation (OBdd n m)

Equations

OEdge.instWellFoundedRelation = { rel := flip OEdge, wf := ⋯ }

theorem Bdd.ordered_of_reachable' {n m : ℕ} {p : Pointer m} {B : Bdd n m} :

B.Ordered → Pointer.Reachable B.heap B.root p → { heap := B.heap, root := p }.Ordered

theorem Bdd.ordered_of_reachable {n m : ℕ} {p : Pointer m} {O : OBdd n m} :

Pointer.Reachable (↑O).heap (↑O).root p → { heap := (↑O).heap, root := p }.Ordered

theorem Bdd.ordered_of_relevant {n m : ℕ} (O : OBdd n m) (S : (↑O).RelevantPointer) :

{ heap := (↑O).heap, root := ↑S }.Ordered

All BDDs in the graph of an Ordered BDD are Ordered.

def Bdd.low {n m : ℕ} {j : Fin m} (B : Bdd n m) :

B.root = Pointer.node j → Bdd n m

Equations

B.low x = { heap := B.heap, root := B.heap[j].low }

Instances For

theorem Bdd.edge_of_low {n m : ℕ} {j : Fin m} (B : Bdd n m) {h : B.root = Pointer.node j} :

Edge B.heap B.root (B.low h).root

def Bdd.high {n m : ℕ} {j : Fin m} (B : Bdd n m) :

B.root = Pointer.node j → Bdd n m

Equations

B.high x = { heap := B.heap, root := B.heap[j].high }

Instances For

theorem Bdd.edge_of_high {n m : ℕ} {j : Fin m} (B : Bdd n m) {h : B.root = Pointer.node j} :

Edge B.heap B.root (B.high h).root

theorem Bdd.reachable_of_edge {n✝ n✝¹ : ℕ} {M : Vector (Node n✝ n✝¹) n✝¹} {p q : Pointer n✝¹} :

Edge M p q → Pointer.Reachable M p q

theorem Bdd.ordered_of_relevant' {n m : ℕ} {v : Vector (Node n m) m} {q p : Pointer m} {B : Bdd n m} {h : B.heap = v} {r : B.root = q} :

B.Ordered → Pointer.Reachable v q p → { heap := v, root := p }.Ordered

theorem Bdd.ordered_of_edge {n m : ℕ} {p : Pointer m} {B : Bdd n m} :

B.Ordered → Edge B.heap B.root p → { heap := B.heap, root := p }.Ordered

theorem Bdd.high_ordered {n m : ℕ} {j : Fin m} {B : Bdd n m} (h : B.root = Pointer.node j) :

B.Ordered → (B.high h).Ordered

theorem Bdd.low_ordered {n m : ℕ} {j : Fin m} {B : Bdd n m} (h : B.root = Pointer.node j) :

B.Ordered → (B.low h).Ordered

theorem Bdd.low_heap_eq_heap {n m : ℕ} {j : Fin m} {B : Bdd n m} {h : B.root = Pointer.node j} :

(B.low h).heap = B.heap

theorem Bdd.low_root_eq_low {n m : ℕ} {j : Fin m} {B : Bdd n m} {h : B.root = Pointer.node j} :

(B.low h).root = B.heap[j].low

theorem Bdd.high_heap_eq_heap {n m : ℕ} {j : Fin m} {B : Bdd n m} {h : B.root = Pointer.node j} :

(B.high h).heap = B.heap

theorem Bdd.high_root_eq_high {n m : ℕ} {j : Fin m} {B : Bdd n m} {h : B.root = Pointer.node j} :

(B.high h).root = B.heap[j].high

def OBdd.high {n m : ℕ} {j : Fin m} (O : OBdd n m) :

(↑O).root = Pointer.node j → OBdd n m

Equations

O.high x✝ = ⟨(↑O).high x✝, ⋯⟩

Instances For

def OBdd.low {n m : ℕ} {j : Fin m} (O : OBdd n m) :

(↑O).root = Pointer.node j → OBdd n m

Equations

O.low x✝ = ⟨(↑O).low x✝, ⋯⟩

Instances For

@[simp]

theorem OBdd.low_heap_eq_heap {n m : ℕ} {j : Fin m} {O : OBdd n m} {h : (↑O).root = Pointer.node j} :

(↑(O.low h)).heap = (↑O).heap

theorem OBdd.low_root_eq_low {n m : ℕ} {j : Fin m} {O : OBdd n m} {h : (↑O).root = Pointer.node j} :

(↑(O.low h)).root = (↑O).heap[j].low

@[simp]

theorem OBdd.high_heap_eq_heap {n m : ℕ} {j : Fin m} {O : OBdd n m} {h : (↑O).root = Pointer.node j} :

(↑(O.high h)).heap = (↑O).heap

theorem OBdd.high_root_eq_high {n m : ℕ} {j : Fin m} {O : OBdd n m} {h : (↑O).root = Pointer.node j} :

(↑(O.high h)).root = (↑O).heap[j].high

theorem oedge_of_low {n✝ m✝ : ℕ} {O : OBdd n✝ m✝} {j : Fin m✝} {h : (↑O).root = Pointer.node j} :

OEdge O (O.low h)

theorem oedge_of_high {n✝ m✝ : ℕ} {O : OBdd n✝ m✝} {j : Fin m✝} {h : (↑O).root = Pointer.node j} :

OEdge O (O.high h)

@[irreducible]

def OBdd.toTree {n m : ℕ} (O : OBdd n m) :

DecisionTree n

Equations

O.toTree = match h : (↑O).root with | Pointer.terminal b => DecisionTree.leaf b | Pointer.node j => DecisionTree.branch (↑O).heap[j].var (O.low h).toTree (O.high h).toTree

Instances For

def OBdd.evaluate {n m : ℕ} :

OBdd n m → Vector Bool n → Bool

Equations

OBdd.evaluate = DecisionTree.evaluate ∘ OBdd.toTree

Instances For

theorem OBdd.evaluate_cast {n m n' : ℕ} {I : Vector Bool n'} {O : OBdd n m} (h : n = n') :

(h ▸ O).evaluate I = O.evaluate (⋯ ▸ I)

def OBdd.HSimilar {n m m' : ℕ} (O : OBdd n m) (U : OBdd n m') :

Equations

O.HSimilar U = (O.toTree = U.toTree)

Instances For

def OBdd.Similar {n m : ℕ} :

OBdd n m → OBdd n m → Prop

Equations

OBdd.Similar = OBdd.HSimilar

Instances For

@[implicit_reducible]

instance OBdd.instDecidableSimilar {n m : ℕ} :

DecidableRel Similar

Similarity of Ordered BDDs is decidable.

Equations

O.instDecidableSimilar U = decidable_of_decidable_of_iff ⋯

@[implicit_reducible]

instance OBdd.instDecidableHSimilar {n m m' : ℕ} (O : OBdd n m) (U : OBdd n m') :

Decidable (O.HSimilar U)

Equations

O.instDecidableHSimilar U = decidable_of_decidable_of_iff ⋯

def OBdd.SimilarRP {n m : ℕ} (O : OBdd n m) (p q : (↑O).RelevantPointer) :

Equations

O.SimilarRP p q = OBdd.Similar ⟨{ heap := (↑O).heap, root := ↑p }, ⋯⟩ ⟨{ heap := (↑O).heap, root := ↑q }, ⋯⟩

Instances For

@[implicit_reducible]

instance OBdd.instDecidableSimilarRP {n✝ m✝ : ℕ} {O : OBdd n✝ m✝} {l r : (↑O).RelevantPointer} :

Decidable (O.SimilarRP l r)

Equations

OBdd.instDecidableSimilarRP = id inferInstance

theorem OBdd.Similar.instEquivalence {n m : ℕ} :

Equivalence Similar

Isomorphism of Ordered BDDs is an equivalence relation.

inductive Pointer.Redundant {n m : ℕ} (M : Vector (Node n m) m) :

Pointer m → Prop

A pointer is redundant if it point to node N with N.low = N.high.

red {n m : ℕ} {M : Vector (Node n m) m} {j : Fin m} : M[j].low = M[j].high → Redundant M (node j)

Instances For

@[implicit_reducible]

instance Pointer.Redundant.instDecidable {n m : ℕ} (w : Vector (Node n m) m) :

DecidablePred (Redundant w)

Equations

One or more equations did not get rendered due to their size.

def Bdd.NoRedundancy {n m : ℕ} (B : Bdd n m) :

Equations

B.NoRedundancy = ∀ (p : B.RelevantPointer), ¬Pointer.Redundant B.heap ↑p

Instances For

def OBdd.Reduced {n m : ℕ} (O : OBdd n m) :

A BDD is Reduced if its graph does not contain redundant nodes or distinct similar subgraphs.

Equations

O.Reduced = ((↑O).NoRedundancy ∧ Subrelation O.SimilarRP (InvImage Eq Subtype.val))

Instances For

theorem transGen_iff_single_and_reflTransGen {α✝ : Type u_1} {r : α✝ → α✝ → Prop} {a b : α✝} :

Relation.TransGen r a b ↔ ∃ (c : α✝), r a c ∧ Relation.ReflTransGen r c b

def RelevantPointer.var {n m : ℕ} {B : Bdd n m} (p : B.RelevantPointer) :

Equations

RelevantPointer.var p = ↑(Pointer.toVar B.heap ↑p)

Instances For

def RelevantPointer.gap {n m : ℕ} {B : Bdd n m} (p : B.RelevantPointer) :

Equations

RelevantPointer.gap p = n - RelevantPointer.var p

Instances For

theorem RelevantEdge.flip_wellFounded {n✝ m✝ : ℕ} {B : Bdd n✝ m✝} (o : B.Ordered) :

WellFounded (flip B.RelevantEdge)

@[implicit_reducible]

instance RelevantEdge.instWellFoundedRelation {n m : ℕ} (O : OBdd n m) :

WellFoundedRelation (↑O).RelevantPointer

Equations

RelevantEdge.instWellFoundedRelation O = { rel := flip (↑O).RelevantEdge, wf := ⋯ }

@[implicit_reducible]

instance OBdd.instDecidableReflTransGen {n m : ℕ} (O : OBdd n m) (p : (↑O).RelevantPointer) (q : Pointer m) :

Decidable (Relation.ReflTransGen (Edge (↑O).heap) (↑p) q)

Equations

O.instDecidableReflTransGen p q = ⋯.mpr (decidable_of_iff (q = ↑p ∨ Relation.TransGen (Edge (↑O).heap) (↑p) q) ⋯)

@[implicit_reducible]

instance Pointer.instDecidableReachable {n m : ℕ} (O : OBdd n m) :

DecidablePred (Reachable (↑O).heap (↑O).root)

Equations

Pointer.instDecidableReachable O = O.instDecidableReflTransGen ⟨(↑O).root, ⋯⟩

def OBdd.size {n m : ℕ} (O : OBdd n m) :

Equations

O.size = Fintype.card { j : Fin m // Pointer.Reachable (↑O).heap (↑O).root (Pointer.node j) }

Instances For

@[implicit_reducible]

instance OBdd.instFintypeRelevantPointer {n m : ℕ} (O : OBdd n m) :

Fintype (↑O).RelevantPointer

Equations

O.instFintypeRelevantPointer = ⋯.mpr (Subtype.fintype (Pointer.Reachable (↑O).heap (↑O).root))

@[implicit_reducible]

def Pointer.decidableEitherReachable {n m : ℕ} (O U : OBdd n m) (h : (↑O).heap = (↑U).heap) :

DecidablePred fun (q : Pointer m) => Reachable (↑O).heap (↑O).root q ∨ Reachable (↑O).heap (↑U).root q

Equations

One or more equations did not get rendered due to their size.

Instances For

@[implicit_reducible]

def OBdd.fintypeEitherRelevantPointer {n m : ℕ} (O U : OBdd n m) (h : (↑O).heap = (↑U).heap) :

Fintype { q : Pointer m // Pointer.Reachable (↑O).heap (↑O).root q ∨ Pointer.Reachable (↑O).heap (↑U).root q }

Equations

O.fintypeEitherRelevantPointer U h = ⋯.mpr (Subtype.fintype fun (q : Pointer m) => Pointer.Reachable (↑O).heap (↑O).root q ∨ Pointer.Reachable (↑O).heap (↑U).root q)

Instances For

@[implicit_reducible]

instance OBdd.instReducedDecidable {n m : ℕ} :

DecidablePred Reduced

Reduced is decidable.

Equations

x✝.instReducedDecidable = instDecidableAnd

theorem eq_of_constant_eq {α : Sort u_1} {β : Sort u_2} {c c' : β} [Inhabited α] :

Function.const α c = Function.const α c' → c = c'

The output of equal constant functions with inhabited domain is equal.

theorem Bdd.terminal_or_node {n m : ℕ} (B : Bdd n m) :

(∃ (b : Bool), B.root = Pointer.terminal b ∧ B = { heap := B.heap, root := Pointer.terminal b }) ∨ ∃ (j : Fin m), B.root = Pointer.node j ∧ B = { heap := B.heap, root := Pointer.node j }

theorem OBdd.init_inductionOn {n m : ℕ} (t : OBdd n m) {motive : OBdd n m → Prop} (base : ∀ (b : Bool), motive ⟨{ heap := (↑t).heap, root := Pointer.terminal b }, ⋯⟩) (step : ∀ (j : Fin m) (hl : { heap := (↑t).heap, root := (↑t).heap[j].low }.Ordered), motive ⟨{ heap := (↑t).heap, root := (↑t).heap[j].low }, ⋯⟩ → ∀ (hh : { heap := (↑t).heap, root := (↑t).heap[j].high }.Ordered), motive ⟨{ heap := (↑t).heap, root := (↑t).heap[j].high }, ⋯⟩ → ∀ (h : { heap := (↑t).heap, root := Pointer.node j }.Ordered), motive ⟨{ heap := (↑t).heap, root := Pointer.node j }, ⋯⟩) :

motive t

def OBdd.isTerminal {n m : ℕ} (O : OBdd n m) :

Equations

O.isTerminal = ∃ (b : Bool), (↑O).root = Pointer.terminal b

Instances For

theorem not_OEdge_of_isTerminal {n m : ℕ} {U O : OBdd n m} :

O.isTerminal → ¬OEdge O U

theorem Bdd.terminal_relevant_iff {b : Bool} {n m : ℕ} {B : Bdd n m} (h : B.root = Pointer.terminal b) (S : B.RelevantPointer) {motive : Pointer m → Prop} :

motive ↑S ↔ motive (Pointer.terminal b)

The graph induced by a terminal BDD consists of a sole terminal pointer.

theorem Bdd.eq_terminal_of_relevant {b : Bool} {n m : ℕ} {v : Vector (Node n m) m} {B : Bdd n m} (h : B = { heap := v, root := Pointer.terminal b }) (S : B.RelevantPointer) :

↑S = Pointer.terminal b

theorem OBdd.reduced_of_terminal {n m : ℕ} {O : OBdd n m} :

O.isTerminal → O.Reduced

Terminal BDDs are reduced.

theorem Bdd.reduced_of_terminal {n✝ n✝¹ : ℕ} {M : Vector (Node n✝ n✝¹) n✝¹} {b : Bool} {o : { heap := M, root := Pointer.terminal b }.Ordered} :

OBdd.Reduced ⟨{ heap := M, root := Pointer.terminal b }, o⟩

theorem OBdd.reduced_of_relevant {n m : ℕ} {O : OBdd n m} (S : (↑O).RelevantPointer) :

O.Reduced → Reduced ⟨{ heap := (↑O).heap, root := ↑S }, ⋯⟩

Sub-BDDs of a reduced BDD are reduced.

theorem OBdd.reachable_of_edge {n✝ n✝¹ : ℕ} {w : Vector (Node n✝ n✝¹) n✝¹} {p q : Pointer n✝¹} :

Edge w p q → Pointer.Reachable w p q

theorem OBdd.ordered_of_edge {n m : ℕ} {v : Vector (Node n m) m} {q : Pointer m} {O : OBdd n m} {h : (↑O).heap = v} {r : (↑O).root = q} (p : Pointer m) :

Edge v q p → { heap := v, root := p }.Ordered

theorem OBdd.ordered_of_low_edge {n n✝ : ℕ} {v : Vector (Node n✝ n) n} {j : Fin n} :

{ heap := v, root := Pointer.node j }.Ordered → { heap := v, root := v[j].low }.Ordered

theorem OBdd.ordered_of_high_edge {n n✝ : ℕ} {v : Vector (Node n✝ n) n} {j : Fin n} :

{ heap := v, root := Pointer.node j }.Ordered → { heap := v, root := v[j].high }.Ordered

@[simp]

theorem OBdd.evaluate_node {n m : ℕ} {v : Vector (Node n m) m} {I : Vector Bool n} {j : Fin m} {h : { heap := v, root := Pointer.node j }.Ordered} :

evaluate ⟨{ heap := v, root := Pointer.node j }, h⟩ I = if I[v[j].var] = true then evaluate ⟨{ heap := v, root := v[j].high }, ⋯⟩ I else evaluate ⟨{ heap := v, root := v[j].low }, ⋯⟩ I

Spell out OBdd.evaluate for non-terminals.

theorem OBdd.evaluate_node' {n m : ℕ} {v : Vector (Node n m) m} {j : Fin m} {h : { heap := v, root := Pointer.node j }.Ordered} :

evaluate ⟨{ heap := v, root := Pointer.node j }, h⟩ = fun (I : Vector Bool n) => if I[v[j].var] = true then evaluate ⟨{ heap := v, root := v[j].high }, ⋯⟩ I else evaluate ⟨{ heap := v, root := v[j].low }, ⋯⟩ I

@[simp]

theorem OBdd.evaluate_terminal {b : Bool} {n m : ℕ} {v : Vector (Node n m) m} {h : { heap := v, root := Pointer.terminal b }.Ordered} :

evaluate ⟨{ heap := v, root := Pointer.terminal b }, h⟩ = Function.const (Vector Bool n) b

Spell out OBdd.evaluate for terminals.

theorem OBdd.evaluate_terminal' {b : Bool} {n m : ℕ} {O : OBdd n m} :

(↑O).root = Pointer.terminal b → O.evaluate = Function.const (Vector Bool n) b

@[simp]

theorem OBdd.toTree_terminal {b : Bool} {n m : ℕ} {v : Vector (Node n m) m} {h : { heap := v, root := Pointer.terminal b }.Ordered} :

toTree ⟨{ heap := v, root := Pointer.terminal b }, h⟩ = DecisionTree.leaf b

theorem OBdd.toTree_terminal' {b : Bool} {n m : ℕ} {O : OBdd n m} :

(↑O).root = Pointer.terminal b → O.toTree = DecisionTree.leaf b

theorem OBdd.HSimilar_of_terminal {n m m' : ℕ} {b : Bool} {O : OBdd n m} {U : OBdd n m'} :

(↑O).root = Pointer.terminal b → (↑U).root = Pointer.terminal b → O.HSimilar U

theorem OBdd.toTree_node {n m : ℕ} {O : OBdd n m} {j : Fin m} (h : (↑O).root = Pointer.node j) :

O.toTree = DecisionTree.branch (↑O).heap[j].var (O.low h).toTree (O.high h).toTree

theorem OBdd.evaluate_node'' {n m : ℕ} {O : OBdd n m} {j : Fin m} (h : (↑O).root = Pointer.node j) :

O.evaluate = fun (I : Vector Bool n) => if I[(↑O).heap[j].var] = true then (O.high h).evaluate I else (O.low h).evaluate I

theorem OBdd.var_lt_high_var {n m : ℕ} {j : Fin m} {O : OBdd n m} {h : (↑O).root = Pointer.node j} :

O.var < (O.high h).var

theorem OBdd.var_lt_low_var {n m : ℕ} {j : Fin m} {O : OBdd n m} {h : (↑O).root = Pointer.node j} :

O.var < (O.low h).var

theorem OBdd.independentOf_lt_root {n m : ℕ} (O : OBdd n m) (i : Fin O.var) :

Nary.IndependentOf O.evaluate ⟨↑i, ⋯⟩

def OBdd.size' {n m : ℕ} :

OBdd n m → ℕ

Equations

OBdd.size' = DecisionTree.size ∘ OBdd.toTree

Instances For

theorem OBdd.size_zero_of_terminal {n✝ m✝ : ℕ} {O : OBdd n✝ m✝} :

O.isTerminal → O.size' = 0

theorem OBdd.high_reduced {n m : ℕ} {O : OBdd n m} {j : Fin m} {h : (↑O).root = Pointer.node j} :

O.Reduced → (O.high h).Reduced

theorem OBdd.low_reduced {n m : ℕ} {O : OBdd n m} {j : Fin m} {h : (↑O).root = Pointer.node j} :

O.Reduced → (O.low h).Reduced

theorem OBdd.size_node {n m : ℕ} {O : OBdd n m} {j : Fin m} (h : (↑O).root = Pointer.node j) :

O.size' = 1 + (O.low h).size' + (O.high h).size'

theorem OBdd.evaluate_high_eq_evaluate_low_of_independentOf_root {n m : ℕ} {O : OBdd n m} {j : Fin m} {h : (↑O).root = Pointer.node j} :

Nary.IndependentOf O.evaluate (↑O).heap[j].var → (O.high h).evaluate = (O.low h).evaluate

theorem OBdd.evaluate_high_eq_evaluate_set_true {n m : ℕ} {O : OBdd n m} {j : Fin m} {h : (↑O).root = Pointer.node j} :

(O.high h).evaluate = O.evaluate ∘ fun (I : Vector Bool n) => I.set (↑(↑O).heap[j].var) true ⋯

theorem OBdd.evaluate_low_eq_evaluate_set_false {n m : ℕ} {O : OBdd n m} {j : Fin m} {h : (↑O).root = Pointer.node j} :

(O.low h).evaluate = O.evaluate ∘ fun (I : Vector Bool n) => I.set (↑(↑O).heap[j].var) false ⋯

theorem OBdd.evaluate_high_eq_of_evaluate_eq_and_var_eq' {n m m' : ℕ} {O : OBdd n m} {U : OBdd n m'} {j : Fin m} {i : Fin m'} {ho : (↑O).root = Pointer.node j} {hu : (↑U).root = Pointer.node i} :

O.evaluate = U.evaluate → (↑O).heap[j].var = (↑U).heap[i].var → (O.high ho).evaluate = (U.high hu).evaluate

theorem OBdd.evaluate_high_eq_of_evaluate_eq_and_var_eq {n m : ℕ} {O U : OBdd n m} {j i : Fin m} {ho : (↑O).root = Pointer.node j} {hu : (↑U).root = Pointer.node i} :

O.evaluate = U.evaluate → (↑O).heap[j].var = (↑U).heap[i].var → (O.high ho).evaluate = (U.high hu).evaluate

theorem OBdd.evaluate_low_eq_of_evaluate_eq_and_var_eq' {n m m' : ℕ} {O : OBdd n m} {U : OBdd n m'} {j : Fin m} {i : Fin m'} {ho : (↑O).root = Pointer.node j} {hu : (↑U).root = Pointer.node i} :

O.evaluate = U.evaluate → (↑O).heap[j].var = (↑U).heap[i].var → (O.low ho).evaluate = (U.low hu).evaluate

theorem OBdd.evaluate_low_eq_of_evaluate_eq_and_var_eq {n m : ℕ} {O U : OBdd n m} {j i : Fin m} {ho : (↑O).root = Pointer.node j} {hu : (↑U).root = Pointer.node i} :

O.evaluate = U.evaluate → (↑O).heap[j].var = (↑U).heap[i].var → (O.low ho).evaluate = (U.low hu).evaluate

theorem OBdd.not_reduced_of_sim_high_low {n m : ℕ} {O : OBdd n m} {j : Fin m} (h : (↑O).root = Pointer.node j) :

(O.high h).Similar (O.low h) → ¬O.Reduced

def OBdd.HIsomorphism {n m n' m' : ℕ} (O : OBdd n m) (U : OBdd n' m') :

Equations

One or more equations did not get rendered due to their size.

Instances For

def OBdd.Isomorphism {n m : ℕ} :

OBdd n m → OBdd n m → Prop

Equations

OBdd.Isomorphism = OBdd.HIsomorphism

Instances For

def OBdd.RelevantIsomorphism {n m : ℕ} (O : OBdd n m) (p q : (↑O).RelevantPointer) :

Equations

O.RelevantIsomorphism p q = OBdd.Isomorphism ⟨{ heap := (↑O).heap, root := ↑p }, ⋯⟩ ⟨{ heap := (↑O).heap, root := ↑q }, ⋯⟩

Instances For

def OBdd.Reduced' {n m : ℕ} (O : OBdd n m) :

Equations

O.Reduced' = ((↑O).NoRedundancy ∧ Subrelation O.RelevantIsomorphism (InvImage Eq Subtype.val))

Instances For

theorem OBdd.Canonicity {n m m' : ℕ} {O : OBdd n m} {U : OBdd n m'} (ho : O.Reduced) (hu : U.Reduced) :

O.evaluate = U.evaluate → O.HSimilar U

Reduced OBDDs are canonical.

theorem OBdd.terminal_of_constant {n m : ℕ} {b : Bool} (O : OBdd n m) :

O.Reduced → (O.evaluate = fun (x : Vector Bool n) => b) → (↑O).root = Pointer.terminal b

The only reduced BDD that denotes a constant function is the terminal BDD.

theorem OBdd.Canonicity_reverse {n m m' : ℕ} {O : OBdd n m} {U : OBdd n m'} :

O.HSimilar U → O.evaluate = U.evaluate

theorem OBdd.not_oedge_reachable {n m : ℕ} {O U : OBdd n m} :

OEdge O U → ¬Pointer.Reachable (↑O).heap (↑U).root (↑O).root

An acyclicity lemma: an edge from O to U implies that O is not reachable from U.

theorem Pointer.Reachable_iff {n m : ℕ} {r p : Pointer m} {M : Vector (Node n m) m} :

Reachable M r p ↔ r = p ∨ ∃ (j : Fin m), r = node j ∧ (Reachable M M[j].low p ∨ Reachable M M[j].high p)

theorem OBdd.reachable_or_eq_low_high {n m : ℕ} {p : Pointer m} {O : OBdd n m} :

Pointer.Reachable (↑O).heap (↑O).root p → (↑O).root = p ∨ ∃ (j : Fin m) (h : (↑O).root = Pointer.node j), Pointer.Reachable (↑O).heap (↑(O.low h)).root p ∨ Pointer.Reachable (↑O).heap (↑(O.high h)).root p

theorem not_isTerminal_of_root_eq_node {n m : ℕ} {j : Fin m} {O : OBdd n m} (h : (↑O).root = Pointer.node j) :

¬O.isTerminal

def OBdd.OReachable {n m : ℕ} (a : OBdd n m) :

OBdd n m → Prop

Equations

OBdd.OReachable = Relation.ReflTransGen OEdge

Instances For

theorem OBdd.low_oreachable {n m : ℕ} {j : Fin m} {O U : OBdd n m} {U_root_def : (↑U).root = Pointer.node j} :

O.OReachable U → O.OReachable (U.low U_root_def)

theorem OBdd.high_oreachable {n m : ℕ} {j : Fin m} {O U : OBdd n m} {U_root_def : (↑U).root = Pointer.node j} :

O.OReachable U → O.OReachable (U.high U_root_def)

theorem OBdd.card_RelevantPointer_le {n m : ℕ} {O : OBdd n m} :

Fintype.card (↑O).RelevantPointer ≤ m + 2

theorem OBdd.card_relevantPointer_eq_one_of_isTerminal {n m : ℕ} {O : OBdd n m} :

O.isTerminal → Fintype.card (↑O).RelevantPointer = 1

theorem OBdd.reachable_node_iff {n m : ℕ} {j : Fin m} {O : OBdd n m} (h : (↑O).root = Pointer.node j) :

@[implicit_reducible]

instance OBdd.instFintypeReachableFromNode {n m : ℕ} {j : Fin m} (O : OBdd n m) (h : (↑O).root = Pointer.node j) :

Fintype { q : Pointer m // q = (↑O).root ∨ Pointer.Reachable (↑O).heap (↑(O.low h)).root q ∨ Pointer.Reachable (↑O).heap (↑(O.high h)).root q }

Equations

One or more equations did not get rendered due to their size.

theorem OBdd.reachable_from_node_iff' {n m : ℕ} {j : Fin m} {p : Pointer m} {O : OBdd n m} (h : (↑O).root = Pointer.node j) :

Pointer.Reachable (↑O).heap (↑O).root p ↔ p = (↑O).root ∨ Pointer.Reachable (↑O).heap (↑(O.low h)).root p ∨ Pointer.Reachable (↑O).heap (↑(O.high h)).root p

theorem OBdd.card_reachable_node' {n m : ℕ} {j : Fin m} {O : OBdd n m} (h : (↑O).root = Pointer.node j) :

Fintype.card { p : Pointer m // Pointer.Reachable (↑O).heap (↑O).root p } = Fintype.card { p : Pointer m // p = (↑O).root ∨ Pointer.Reachable (↑O).heap (↑(O.low h)).root p ∨ Pointer.Reachable (↑O).heap (↑(O.high h)).root p }

theorem OBdd.eq_root_disjoint_reachable_low_or_high {n m : ℕ} {j : Fin m} {O : OBdd n m} (h : (↑O).root = Pointer.node j) :

Disjoint (fun (x : Pointer m) => x = (↑O).root) fun (p : Pointer m) => Pointer.Reachable (↑O).heap (↑(O.low h)).root p ∨ Pointer.Reachable (↑O).heap (↑(O.high h)).root p

theorem OBdd.card_reachable_node {n m : ℕ} {j : Fin m} {O : OBdd n m} (h : (↑O).root = Pointer.node j) :

Fintype.card { q : Pointer m // Pointer.Reachable (↑O).heap (↑O).root q } = 1 + Fintype.card { q : Pointer m // Pointer.Reachable (↑(O.low h)).heap (↑(O.low h)).root q ∨ Pointer.Reachable (↑(O.high h)).heap (↑(O.high h)).root q }

theorem Bdd.ordered_of_low_high_ordered {n m : ℕ} {j : Fin m} {B : Bdd n m} (h : B.root = Pointer.node j) :

(B.low h).Ordered → B.var < (B.low h).var → (B.high h).Ordered → B.var < (B.high h).var → B.Ordered

theorem Bdd.ordered_of_ordered_heap_not_reachable_set {n m : ℕ} (O : OBdd n m) (i : Fin m) (N : Node n m) :

¬Pointer.Reachable (↑O).heap (↑O).root (Pointer.node i) → { heap := (↑O).heap.set (↑i) N ⋯, root := (↑O).root }.Ordered

theorem Pointer.mayPrecede_of_reachable {n m : ℕ} {p : Pointer m} {B : Bdd n m} :

B.Ordered → Reachable B.heap B.root p → toVar B.heap B.root ≤ toVar B.heap p

theorem OBdd.reduced_var_dependent {n m : ℕ} {O : OBdd n m} {p : Fin n} :

O.Reduced → (∀ (i : Fin ↑p), Nary.IndependentOf O.evaluate ⟨↑i, ⋯⟩) → ↑p ≤ ↑(↑O).var

def Bdd.usesVar {n m : ℕ} (B : Bdd n m) (i : Fin n) :

Equations

B.usesVar i = ∃ (j : Fin m), Pointer.Reachable B.heap B.root (Pointer.node j) ∧ B.heap[j].var = i

Instances For

theorem Bdd.usesVar_of_high_usesVar {n m : ℕ} {j : Fin m} {i : Fin n} {B : Bdd n m} {h : B.root = Pointer.node j} :

(B.high h).usesVar i → B.usesVar i

theorem Bdd.usesVar_of_low_usesVar {n m : ℕ} {j : Fin m} {i : Fin n} {B : Bdd n m} {h : B.root = Pointer.node j} :

(B.low h).usesVar i → B.usesVar i

theorem OBdd.usesVar_of_high_usesVar {n m : ℕ} {j : Fin m} {i : Fin n} {O : OBdd n m} {h : (↑O).root = Pointer.node j} :

(↑(O.high h)).usesVar i → (↑O).usesVar i

theorem OBdd.usesVar_of_low_usesVar {n m : ℕ} {j : Fin m} {i : Fin n} {O : OBdd n m} {h : (↑O).root = Pointer.node j} :

(↑(O.low h)).usesVar i → (↑O).usesVar i

theorem OBdd.dependsOn_of_usesVar_of_reduced {n m : ℕ} {j : Fin m} {i : Fin n} {O : OBdd n m} :

O.Reduced → Pointer.Reachable (↑O).heap (↑O).root (Pointer.node j) → (↑O).heap[j].var = i → ∃ (v : Vector Bool n), O.evaluate v ≠ O.evaluate (v.set (↑i) true ⋯)

theorem OBdd.usesVar_of_dependsOn {n m : ℕ} {v : Vector Bool n} {b : Bool} {O : OBdd n m} {i : Fin n} :

O.evaluate v ≠ O.evaluate (v.set (↑i) b ⋯) → (↑O).usesVar i

theorem OBdd.usesVar_iff_dependsOn_of_reduced {n m : ℕ} {i : Fin n} {O : OBdd n m} :

O.Reduced → ((↑O).usesVar i ↔ Nary.DependsOn O.evaluate i)

theorem OBdd.usesVar_iff {n m : ℕ} (i : Fin n) (O : OBdd n m) :

(↑O).usesVar i ↔ ∃ (j : Fin m) (hj : (↑O).root = Pointer.node j), (↑O).heap[j].var = i ∨ (↑(O.low hj)).usesVar i ∨ (↑(O.high hj)).usesVar i

theorem OBdd.toTree_usesVar {n m : ℕ} {i : Fin n} {O : OBdd n m} :

(↑O).usesVar i ↔ DecisionTree.usesVar i O.toTree

theorem OBdd.evaluate_eq_of_forall_usesVar {n m : ℕ} {O : OBdd n m} {I J : Vector Bool n} :

(∀ (i : Fin n), (↑O).usesVar i → I[i] = J[i]) → O.evaluate I = O.evaluate J

theorem Pointer.eq_terminal_of_reachable {n✝ n✝¹ : ℕ} {w : Vector (Node n✝ n✝¹) n✝¹} {b : Bool} {p : Pointer n✝¹} :

Reachable w (terminal b) p → p = terminal b

theorem Bdd.not_usesVar_of_terminal {n✝ n✝¹ : ℕ} {M : Vector (Node n✝ n✝¹) n✝¹} {b : Bool} {i : Fin n✝} :

¬{ heap := M, root := Pointer.terminal b }.usesVar i

theorem Bdd.not_usesVar_of_var_gt {n m : ℕ} {i : Fin n} {M : Vector (Node n m) m} {j : Fin m} :

{ heap := M, root := Pointer.node j }.Ordered → M[j].var > i → ¬{ heap := M, root := Pointer.node j }.usesVar i

@[implicit_reducible]

instance OBdd.instDecidableUsesVar {n m : ℕ} {O : OBdd n m} :

DecidablePred (↑O).usesVar

Equations

OBdd.instDecidableUsesVar i = (usesVar_helper✝ O i (↑O).root ⋯ ⟨Std.HashSet.emptyWithCapacity, ⋯⟩).1

theorem Bdd.terminal_of_zero_vars {n m : ℕ} {B : Bdd n m} :

n = 0 → ∃ (b : Bool), B.root = Pointer.terminal b

theorem Bdd.terminal_of_zero_heap {n m : ℕ} {B : Bdd n m} :

m = 0 → ∃ (b : Bool), B.root = Pointer.terminal b

theorem Pointer.toVar_lt_of_trans_edge_of_ordered {n✝ n✝¹ : ℕ} {M : Vector (Node n✝ n✝¹) n✝¹} {x y : Pointer n✝¹} :

{ heap := M, root := x }.Ordered → Relation.TransGen (Edge M) x y → toVar M x < toVar M y

def Pointer.equiv {m m' : ℕ} (p : Pointer m) (p' : Pointer m') :

Equations

p.equiv p' = ((∀ (b : Bool), p = Pointer.terminal b → p' = Pointer.terminal b) ∧ ∀ (j : Fin m), p = Pointer.node j → ∃ (j' : Fin m'), p' = Pointer.node j' ∧ ↑j = ↑j')

Instances For

theorem Pointer.equiv_refl {m : ℕ} (p : Pointer m) :

p.equiv p

theorem Pointer.equiv_symm {m m✝ : ℕ} {q : Pointer m✝} {p : Pointer m} :

p.equiv q → q.equiv p

def Node.equiv {n m n' m' : ℕ} (N : Node n m) (N' : Node n' m') :

Equations

N.equiv N' = (↑N.var = ↑N'.var ∧ N.low.equiv N'.low ∧ N.high.equiv N'.high)

Instances For

theorem Node.equiv_refl {n m : ℕ} (N : Node n m) :

N.equiv N

theorem Node.equiv_symm {n✝ m✝ : ℕ} {N : Node n✝ m✝} {n✝¹ m✝¹ : ℕ} {M : Node n✝¹ m✝¹} :

N.equiv M → M.equiv N

theorem Bdd.ordered_of_ordered_heap_all_reachable_eq {n m m' : ℕ} (O : OBdd n m) (B : Bdd n m') :

(∀ (j : Fin m'), Pointer.Reachable B.heap B.root (Pointer.node j) → ∃ (hj : ↑j < m), (↑O).heap[↑j].equiv B.heap[j]) → (∀ (j : Fin m'), B.root = Pointer.node j → ∃ (hj : ↑j < m), (↑O).root = Pointer.node ⟨↑j, hj⟩) → B.Ordered

theorem OBdd.toTree_eq_toTree_of_ordered_heap_all_reachable_eq {n m m' : ℕ} (O : OBdd n m) (U : OBdd n m') :

(∀ (j : Fin m'), Pointer.Reachable (↑U).heap (↑U).root (Pointer.node j) → ∃ (hj : ↑j < m), (↑O).heap[↑j].equiv (↑U).heap[j]) → (↑U).root.equiv (↑O).root → O.toTree = U.toTree

theorem OBdd.evaluate_eq_evaluate_of_ordered_heap_all_reachable_eq {n m m' : ℕ} (O : OBdd n m) (U : OBdd n m') :

(∀ (j : Fin m'), Pointer.Reachable (↑U).heap (↑U).root (Pointer.node j) → ∃ (hj : ↑j < m), (↑O).heap[↑j].equiv (↑U).heap[j]) → (↑U).root.equiv (↑O).root → O.evaluate = U.evaluate

def RawBdd.RawPointer :

Equations

RawBdd.RawPointer = (Bool ⊕ ℕ)

Instances For

structure RawBdd.RawNode (n : ℕ) :

va : Fin n
lo : RawPointer
hi : RawPointer

Instances For

def RawBdd.RawPointer.Bounded (m : ℕ) (p : RawPointer) :

Equations

RawBdd.RawPointer.Bounded m p = ∀ {i : ℕ}, p = Sum.inr i → i < m

Instances For

theorem RawBdd.RawPointer.bounded_of_le {m m' : ℕ} {p : RawPointer} (hm : Bounded m p) (h : m ≤ m') :

Bounded m' p

def RawBdd.RawPointer.cook {m : ℕ} (p : RawPointer) (h : Bounded m p) :

Pointer m

Equations

RawBdd.RawPointer.cook (Sum.inl b) h_2 = Pointer.terminal b
RawBdd.RawPointer.cook (Sum.inr i) h_2 = Pointer.node ⟨i, ⋯⟩

Instances For

theorem RawBdd.RawPointer.cook_equiv {m1 : ℕ} {p : RawPointer} {m2 : ℕ} {h1 : Bounded m1 p} {h2 : Bounded m2 p} :

(p.cook ⋯).equiv (p.cook ⋯)

theorem RawBdd.RawPointer.cook_eq {m : ℕ} {p : RawPointer} {h1 h2 : Bounded m p} :

p.cook ⋯ = p.cook ⋯

cook ignores the Bounded witness: the bound is a Prop, so two cooks of the same raw pointer at the same heap size are equal.

def RawBdd.RawPointer.fromPointer {m : ℕ} :

Pointer m → RawPointer

Equations

RawBdd.RawPointer.fromPointer (Pointer.terminal a) = Sum.inl a
RawBdd.RawPointer.fromPointer (Pointer.node a) = Sum.inr ↑a

Instances For

def RawBdd.RawNode.Bounded {n : ℕ} (m : ℕ) (N : RawNode n) :

Equations

RawBdd.RawNode.Bounded m N = (RawBdd.RawPointer.Bounded m N.lo ∧ RawBdd.RawPointer.Bounded m N.hi)

Instances For

theorem RawBdd.RawNode.bounded_of_le {n m m' : ℕ} {N : RawNode n} (hm : Bounded m N) (h : m ≤ m') :

Bounded m' N

def RawBdd.RawNode.cook {n m : ℕ} (N : RawNode n) (h : Bounded m N) :

Node n m

Equations

N.cook h = { var := N.va, low := N.lo.cook ⋯, high := N.hi.cook ⋯ }

Instances For

theorem RawBdd.RawNode.cook_equiv {n✝ : ℕ} {N : RawNode n✝} {m✝ : ℕ} {h1 : Bounded m✝ N} {m✝¹ : ℕ} {h2 : Bounded m✝¹ N} :

(N.cook h1).equiv (N.cook h2)

def RawBdd.cook_heap {n c : ℕ} (v : Vector (RawNode n) c) (hh : ∀ (i : Fin c), RawNode.Bounded (↑i) v[i]) :

Vector (Node n c) c

Equations

RawBdd.cook_heap v hh = Vector.ofFn fun (i : Fin c) => v[i].cook ⋯

Instances For

def RawBdd.toVar_or {n m : ℕ} (M : Vector (Node n m) m) :

Pointer m → ℕ → ℕ

Equations

RawBdd.toVar_or M (Pointer.terminal a) x✝ = x✝
RawBdd.toVar_or M (Pointer.node j) x✝ = ↑M[j].var

Instances For

@[simp]

theorem RawBdd.toVar_or_terminal_eq {b : Bool} {i n m : ℕ} (w : Vector (Node n m) m) :

toVar_or w (Pointer.terminal b) i = i

@[simp]

theorem RawBdd.toVar_or_node_eq {i n m : ℕ} (w : Vector (Node n m) m) {j : Fin m} :

toVar_or w (Pointer.node j) i = ↑w[j].var

theorem RawBdd.cook_low {n m : ℕ} {rn : RawNode n} {h1 : RawPointer.Bounded m rn.lo} {h2 : RawNode.Bounded m rn} :

rn.lo.cook h1 = (rn.cook h2).low

theorem RawBdd.cook_high {n m : ℕ} {rn : RawNode n} {h1 : RawPointer.Bounded m rn.hi} {h2 : RawNode.Bounded m rn} :

rn.hi.cook h1 = (rn.cook h2).high

theorem RawBdd.cook_inj {m : ℕ} {p q : RawPointer} {hp : RawPointer.Bounded m p} {hq : RawPointer.Bounded m q} :

p.cook hp = q.cook hq → p = q

theorem RawBdd.cook_aux {n✝ : ℕ} {j : Fin n✝} {a✝ : ℕ} {hj : ↑j < a✝} {p : RawPointer} {h1 : RawPointer.Bounded n✝ p} {h2 : RawPointer.Bounded a✝ p} :

p.cook h1 = Pointer.node j → p.cook h2 = Pointer.node ⟨↑j, hj⟩

theorem RawBdd.push_ordered {n✝ n✝¹ : ℕ} {v : Vector (RawNode n✝) n✝¹} {h0 : ∀ (i : Fin n✝¹), RawNode.Bounded (↑i) v[i]} {p : RawPointer} {h1 : RawPointer.Bounded n✝¹ p} {N : RawNode n✝} {h2 : ∀ (i : Fin (n✝¹ + 1)), RawNode.Bounded (↑i) (v.push N)[i]} {h3 : RawPointer.Bounded (n✝¹ + 1) p} :

{ heap := cook_heap v h0, root := p.cook h1 }.Ordered → { heap := cook_heap (v.push N) h2, root := p.cook h3 }.Ordered