internlm/Lean-Github huggingface dataset:
Theorem: AIG.denote_mkConst
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
⊢ ⟦aig.mkConst val, assign⟧ = val
Tactic:
unfold denote denote.go
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
⊢ (match elem : (aig.mkConst val).aig.decls[(aig.mkConst val).ref.gate] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := denote.go lhs (aig.mkConst val).aig.decls assign ⋯ ⋯;
      let rval := denote.go rhs (aig.mkConst val).aig.decls assign ⋯ ⋯;
      xor lval linv && xor rval rinv) =
    val
Theorem: AIG.denote_mkConst
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
⊢ (match elem : (aig.mkConst val).aig.decls[(aig.mkConst val).ref.gate] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := denote.go lhs (aig.mkConst val).aig.decls assign ⋯ ⋯;
      let rval := denote.go rhs (aig.mkConst val).aig.decls assign ⋯ ⋯;
      xor lval linv && xor rval rinv) =
    val
Tactic:
split
Proof state after:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
b✝ : Bool
heq✝ : (aig.mkConst val).aig.decls[(aig.mkConst val).ref.gate] = Decl.const b✝
⊢ b✝ = val

case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
idx✝ : α
heq✝ : (aig.mkConst val).aig.decls[(aig.mkConst val).ref.gate] = Decl.atom idx✝
⊢ assign idx✝ = val

case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : (aig.mkConst val).aig.decls[(aig.mkConst val).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ (aig.mkConst val).aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ (aig.mkConst val).aig.decls assign ⋯ ⋯;
    xor lval linv✝ && xor rval rinv✝) =
    val
Theorem: AIG.denote_mkConst
Proof state before:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
b✝ : Bool
heq✝ : (aig.mkConst val).aig.decls[(aig.mkConst val).ref.gate] = Decl.const b✝
⊢ b✝ = val

case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
idx✝ : α
heq✝ : (aig.mkConst val).aig.decls[(aig.mkConst val).ref.gate] = Decl.atom idx✝
⊢ assign idx✝ = val

case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : (aig.mkConst val).aig.decls[(aig.mkConst val).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ (aig.mkConst val).aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ (aig.mkConst val).aig.decls assign ⋯ ⋯;
    xor lval linv✝ && xor rval rinv✝) =
    val
Tactic:
. next heq =>
  rw [mkConst, Array.get_push_size] at heq
  injection heq with heq
  rw [heq]
Proof state after:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
idx✝ : α
heq✝ : (aig.mkConst val).aig.decls[(aig.mkConst val).ref.gate] = Decl.atom idx✝
⊢ assign idx✝ = val

case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : (aig.mkConst val).aig.decls[(aig.mkConst val).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ (aig.mkConst val).aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ (aig.mkConst val).aig.decls assign ⋯ ⋯;
    xor lval linv✝ && xor rval rinv✝) =
    val
Theorem: AIG.denote_mkConst
Proof state before:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
idx✝ : α
heq✝ : (aig.mkConst val).aig.decls[(aig.mkConst val).ref.gate] = Decl.atom idx✝
⊢ assign idx✝ = val

case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : (aig.mkConst val).aig.decls[(aig.mkConst val).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ (aig.mkConst val).aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ (aig.mkConst val).aig.decls assign ⋯ ⋯;
    xor lval linv✝ && xor rval rinv✝) =
    val
Tactic:
. next heq =>
  rw [mkConst, Array.get_push_size] at heq
  contradiction
Proof state after:
case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : (aig.mkConst val).aig.decls[(aig.mkConst val).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ (aig.mkConst val).aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ (aig.mkConst val).aig.decls assign ⋯ ⋯;
    xor lval linv✝ && xor rval rinv✝) =
    val
Theorem: AIG.denote_mkConst
Proof state before:
case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : (aig.mkConst val).aig.decls[(aig.mkConst val).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ (aig.mkConst val).aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ (aig.mkConst val).aig.decls assign ⋯ ⋯;
    xor lval linv✝ && xor rval rinv✝) =
    val
Tactic:
. next heq =>
  rw [mkConst, Array.get_push_size] at heq
  contradiction
Proof state after:
no goals
Theorem: AIG.denote_mkConst
Proof state before:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
b✝ : Bool
heq✝ : (aig.mkConst val).aig.decls[(aig.mkConst val).ref.gate] = Decl.const b✝
⊢ b✝ = val
Tactic:
next heq =>
rw [mkConst, Array.get_push_size] at heq
injection heq with heq
rw [heq]
Proof state after:
no goals
Theorem: AIG.denote_mkConst
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
b✝ : Bool
heq : (aig.mkConst val).aig.decls[(aig.mkConst val).ref.gate] = Decl.const b✝
⊢ b✝ = val
Tactic:
rw [mkConst, Array.get_push_size] at heq
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
b✝ : Bool
heq : Decl.const val = Decl.const b✝
⊢ b✝ = val
Theorem: AIG.denote_mkConst
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
b✝ : Bool
heq : Decl.const val = Decl.const b✝
⊢ b✝ = val
Tactic:
injection heq with heq
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
b✝ : Bool
heq : val = b✝
⊢ b✝ = val
Theorem: AIG.denote_mkConst
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
b✝ : Bool
heq : val = b✝
⊢ b✝ = val
Tactic:
rw [heq]
Proof state after:
no goals
Theorem: AIG.denote_mkConst
Proof state before:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
idx✝ : α
heq✝ : (aig.mkConst val).aig.decls[(aig.mkConst val).ref.gate] = Decl.atom idx✝
⊢ assign idx✝ = val
Tactic:
next heq =>
rw [mkConst, Array.get_push_size] at heq
contradiction
Proof state after:
no goals
Theorem: AIG.denote_mkConst
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
idx✝ : α
heq : (aig.mkConst val).aig.decls[(aig.mkConst val).ref.gate] = Decl.atom idx✝
⊢ assign idx✝ = val
Tactic:
rw [mkConst, Array.get_push_size] at heq
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
idx✝ : α
heq : Decl.const val = Decl.atom idx✝
⊢ assign idx✝ = val
Theorem: AIG.denote_mkConst
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
idx✝ : α
heq : Decl.const val = Decl.atom idx✝
⊢ assign idx✝ = val
Tactic:
contradiction
Proof state after:
no goals
Theorem: AIG.denote_mkConst
Proof state before:
case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : (aig.mkConst val).aig.decls[(aig.mkConst val).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ (aig.mkConst val).aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ (aig.mkConst val).aig.decls assign ⋯ ⋯;
    xor lval linv✝ && xor rval rinv✝) =
    val
Tactic:
next heq =>
rw [mkConst, Array.get_push_size] at heq
contradiction
Proof state after:
no goals
Theorem: AIG.denote_mkConst
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkConst val).aig.decls[(aig.mkConst val).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ (aig.mkConst val).aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ (aig.mkConst val).aig.decls assign ⋯ ⋯;
    xor lval linv✝ && xor rval rinv✝) =
    val
Tactic:
rw [mkConst, Array.get_push_size] at heq
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : (aig.mkConst val).aig.decls[(aig.mkConst val).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq : Decl.const val = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ (aig.mkConst val).aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ (aig.mkConst val).aig.decls assign ⋯ ⋯;
    xor lval linv✝ && xor rval rinv✝) =
    val
Theorem: AIG.denote_mkConst
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : (aig.mkConst val).aig.decls[(aig.mkConst val).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq : Decl.const val = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ (aig.mkConst val).aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ (aig.mkConst val).aig.decls assign ⋯ ⋯;
    xor lval linv✝ && xor rval rinv✝) =
    val
Tactic:
contradiction
Proof state after:
no goals
Theorem: AIG.denote_idx_const
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
b : Bool
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.const b
⊢ ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = b
Tactic:
unfold denote denote.go
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
b : Bool
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.const b
⊢ (match elem :
      { aig := aig,
              ref :=
                { gate := start,
                  hgate := hstart } }.aig.decls[{ aig := aig, ref := { gate := start, hgate := hstart } }.ref.gate] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := denote.go lhs { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
      let rval := denote.go rhs { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
      xor lval linv && xor rval rinv) =
    b
Theorem: AIG.denote_idx_const
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
b : Bool
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.const b
⊢ (match elem :
      { aig := aig,
              ref :=
                { gate := start,
                  hgate := hstart } }.aig.decls[{ aig := aig, ref := { gate := start, hgate := hstart } }.ref.gate] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := denote.go lhs { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
      let rval := denote.go rhs { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
      xor lval linv && xor rval rinv) =
    b
Tactic:
split <;> simp_all
Proof state after:
no goals
Theorem: AIG.denote_idx_atom
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
a : α
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.atom a
⊢ ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = assign a
Tactic:
unfold denote denote.go
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
a : α
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.atom a
⊢ (match elem :
      { aig := aig,
              ref :=
                { gate := start,
                  hgate := hstart } }.aig.decls[{ aig := aig, ref := { gate := start, hgate := hstart } }.ref.gate] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := denote.go lhs { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
      let rval := denote.go rhs { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
      xor lval linv && xor rval rinv) =
    assign a
Theorem: AIG.denote_idx_atom
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
a : α
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.atom a
⊢ (match elem :
      { aig := aig,
              ref :=
                { gate := start,
                  hgate := hstart } }.aig.decls[{ aig := aig, ref := { gate := start, hgate := hstart } }.ref.gate] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := denote.go lhs { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
      let rval := denote.go rhs { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
      xor lval linv && xor rval rinv) =
    assign a
Tactic:
split <;> simp_all
Proof state after:
no goals
Theorem: AIG.denote_idx_gate
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
lhs : Nat
linv : Bool
rhs : Nat
rinv : Bool
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ lhs < aig.decls.size
Tactic:
have := aig.inv start lhs rhs linv rinv hstart h
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
lhs : Nat
linv : Bool
rhs : Nat
rinv : Bool
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
this : lhs < start ∧ rhs < start
⊢ lhs < aig.decls.size
Theorem: AIG.denote_idx_gate
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
lhs : Nat
linv : Bool
rhs : Nat
rinv : Bool
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
this : lhs < start ∧ rhs < start
⊢ lhs < aig.decls.size
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.denote_idx_gate
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
lhs : Nat
linv : Bool
rhs : Nat
rinv : Bool
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ rhs < aig.decls.size
Tactic:
have := aig.inv start lhs rhs linv rinv hstart h
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
lhs : Nat
linv : Bool
rhs : Nat
rinv : Bool
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
this : lhs < start ∧ rhs < start
⊢ rhs < aig.decls.size
Theorem: AIG.denote_idx_gate
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
lhs : Nat
linv : Bool
rhs : Nat
rinv : Bool
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
this : lhs < start ∧ rhs < start
⊢ rhs < aig.decls.size
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.denote_idx_gate
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
lhs : Nat
linv : Bool
rhs : Nat
rinv : Bool
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ =
    (xor ⟦{ aig := aig, ref := { gate := lhs, hgate := ⋯ } }, assign⟧ linv &&
      xor ⟦{ aig := aig, ref := { gate := rhs, hgate := ⋯ } }, assign⟧ rinv)
Tactic:
unfold denote
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
lhs : Nat
linv : Bool
rhs : Nat
rinv : Bool
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ denote.go { aig := aig, ref := { gate := start, hgate := hstart } }.ref.gate
      { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯ =
    (xor
        (denote.go { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯)
        linv &&
      xor
        (denote.go { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯)
        rinv)
Theorem: AIG.denote_idx_gate
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
lhs : Nat
linv : Bool
rhs : Nat
rinv : Bool
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ denote.go { aig := aig, ref := { gate := start, hgate := hstart } }.ref.gate
      { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯ =
    (xor
        (denote.go { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯)
        linv &&
      xor
        (denote.go { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯)
        rinv)
Tactic:
conv =>
  lhs
  unfold denote.go
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
lhs : Nat
linv : Bool
rhs : Nat
rinv : Bool
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ (match elem :
      { aig := aig,
              ref :=
                { gate := start,
                  hgate := hstart } }.aig.decls[{ aig := aig, ref := { gate := start, hgate := hstart } }.ref.gate] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := denote.go lhs { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
      let rval := denote.go rhs { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
      xor lval linv && xor rval rinv) =
    (xor
        (denote.go { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯)
        linv &&
      xor
        (denote.go { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯)
        rinv)
Theorem: AIG.denote_idx_gate
Proof state before:
case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
lhs : Nat
linv : Bool
rhs : Nat
rinv : Bool
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ :
  { aig := aig,
            ref :=
              { gate := start,
                hgate := hstart } }.aig.decls[{ aig := aig, ref := { gate := start, hgate := hstart } }.ref.gate] =
    Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
    xor lval linv✝ && xor rval rinv✝) =
    (xor
        (denote.go { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯)
        linv &&
      xor
        (denote.go { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯)
        rinv)
Tactic:
. next heq =>
  rw [h] at heq
  simp_all
Proof state after:
no goals
Theorem: AIG.denote_idx_gate
Proof state before:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
lhs : Nat
linv : Bool
rhs : Nat
rinv : Bool
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
b✝ : Bool
heq✝ :
  { aig := aig,
            ref :=
              { gate := start,
                hgate := hstart } }.aig.decls[{ aig := aig, ref := { gate := start, hgate := hstart } }.ref.gate] =
    Decl.const b✝
⊢ b✝ =
    (xor
        (denote.go { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯)
        linv &&
      xor
        (denote.go { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯)
        rinv)
Tactic:
simp_all
Proof state after:
no goals
Theorem: AIG.denote_idx_gate
Proof state before:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
lhs : Nat
linv : Bool
rhs : Nat
rinv : Bool
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
idx✝ : α
heq✝ :
  { aig := aig,
            ref :=
              { gate := start,
                hgate := hstart } }.aig.decls[{ aig := aig, ref := { gate := start, hgate := hstart } }.ref.gate] =
    Decl.atom idx✝
⊢ assign idx✝ =
    (xor
        (denote.go { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯)
        linv &&
      xor
        (denote.go { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯)
        rinv)
Tactic:
simp_all
Proof state after:
no goals