internlm/Lean-Github huggingface dataset:
Theorem: List.nodupkeys_eq_of_fst_eq
Proof state before:
case right.cons.inr.intro.intro.intro.intro.intro.inl.inr
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_eq_hd : s = hd
s'_in_tl : s' ∈ tl
nd1 : ¬s.fst = s'.fst
⊢ s.snd = s'.snd
Tactic:
exfalso
Proof state after:
case right.cons.inr.intro.intro.intro.intro.intro.inl.inr
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_eq_hd : s = hd
s'_in_tl : s' ∈ tl
nd1 : ¬s.fst = s'.fst
⊢ False
Theorem: List.nodupkeys_eq_of_fst_eq
Proof state before:
case right.cons.inr.intro.intro.intro.intro.intro.inl.inr
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_eq_hd : s = hd
s'_in_tl : s' ∈ tl
nd1 : ¬s.fst = s'.fst
⊢ False
Tactic:
exact nd1 keys_eq
Proof state after:
no goals
Theorem: List.nodupkeys_eq_of_fst_eq
Proof state before:
case right.cons.inr.intro.intro.intro.intro.intro.inr
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
h' : s' = hd ∨ s' ∈ tl
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
⊢ s.snd = s'.snd
Tactic:
rcases h' with s'_eq_hd | s'_in_tl
Proof state after:
case right.cons.inr.intro.intro.intro.intro.intro.inr.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_eq_hd : s' = hd
⊢ s.snd = s'.snd

case right.cons.inr.intro.intro.intro.intro.intro.inr.inr
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_in_tl : s' ∈ tl
⊢ s.snd = s'.snd
Theorem: List.nodupkeys_eq_of_fst_eq
Proof state before:
case right.cons.inr.intro.intro.intro.intro.intro.inr.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_eq_hd : s' = hd
⊢ s.snd = s'.snd

case right.cons.inr.intro.intro.intro.intro.intro.inr.inr
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_in_tl : s' ∈ tl
⊢ s.snd = s'.snd
Tactic:
. rw [← nd3, ← hd_fst_eq_a, ← s'_eq_hd] at nd1
  specialize nd1 s.1
  simp only [List.mem_map, Prod.exists, exists_and_right, exists_eq_right,
    forall_exists_index] at nd1
  specialize nd1 s.2 s_in_tl
  exfalso
  exact nd1 keys_eq.symm
Proof state after:
case right.cons.inr.intro.intro.intro.intro.intro.inr.inr
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_in_tl : s' ∈ tl
⊢ s.snd = s'.snd
Theorem: List.nodupkeys_eq_of_fst_eq
Proof state before:
case right.cons.inr.intro.intro.intro.intro.intro.inr.inr
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_in_tl : s' ∈ tl
⊢ s.snd = s'.snd
Tactic:
. exact ih s_in_tl s'_in_tl
Proof state after:
no goals
Theorem: List.nodupkeys_eq_of_fst_eq
Proof state before:
case right.cons.inr.intro.intro.intro.intro.intro.inr.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_eq_hd : s' = hd
⊢ s.snd = s'.snd
Tactic:
rw [← nd3, ← hd_fst_eq_a, ← s'_eq_hd] at nd1
Proof state after:
case right.cons.inr.intro.intro.intro.intro.intro.inr.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ map (fun x => x.fst) tl → ¬s'.fst = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_eq_hd : s' = hd
⊢ s.snd = s'.snd
Theorem: List.nodupkeys_eq_of_fst_eq
Proof state before:
case right.cons.inr.intro.intro.intro.intro.intro.inr.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ map (fun x => x.fst) tl → ¬s'.fst = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_eq_hd : s' = hd
⊢ s.snd = s'.snd
Tactic:
specialize nd1 s.1
Proof state after:
case right.cons.inr.intro.intro.intro.intro.intro.inr.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_eq_hd : s' = hd
nd1 : s.fst ∈ map (fun x => x.fst) tl → ¬s'.fst = s.fst
⊢ s.snd = s'.snd
Theorem: List.nodupkeys_eq_of_fst_eq
Proof state before:
case right.cons.inr.intro.intro.intro.intro.intro.inr.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_eq_hd : s' = hd
nd1 : s.fst ∈ map (fun x => x.fst) tl → ¬s'.fst = s.fst
⊢ s.snd = s'.snd
Tactic:
simp only [List.mem_map, Prod.exists, exists_and_right, exists_eq_right,
  forall_exists_index] at nd1
Proof state after:
case right.cons.inr.intro.intro.intro.intro.intro.inr.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_eq_hd : s' = hd
nd1 : ∀ (x : β), (s.fst, x) ∈ tl → ¬s'.fst = s.fst
⊢ s.snd = s'.snd
Theorem: List.nodupkeys_eq_of_fst_eq
Proof state before:
case right.cons.inr.intro.intro.intro.intro.intro.inr.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_eq_hd : s' = hd
nd1 : ∀ (x : β), (s.fst, x) ∈ tl → ¬s'.fst = s.fst
⊢ s.snd = s'.snd
Tactic:
specialize nd1 s.2 s_in_tl
Proof state after:
case right.cons.inr.intro.intro.intro.intro.intro.inr.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_eq_hd : s' = hd
nd1 : ¬s'.fst = s.fst
⊢ s.snd = s'.snd
Theorem: List.nodupkeys_eq_of_fst_eq
Proof state before:
case right.cons.inr.intro.intro.intro.intro.intro.inr.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_eq_hd : s' = hd
nd1 : ¬s'.fst = s.fst
⊢ s.snd = s'.snd
Tactic:
exfalso
Proof state after:
case right.cons.inr.intro.intro.intro.intro.intro.inr.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_eq_hd : s' = hd
nd1 : ¬s'.fst = s.fst
⊢ False
Theorem: List.nodupkeys_eq_of_fst_eq
Proof state before:
case right.cons.inr.intro.intro.intro.intro.intro.inr.inl
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_eq_hd : s' = hd
nd1 : ¬s'.fst = s.fst
⊢ False
Tactic:
exact nd1 keys_eq.symm
Proof state after:
no goals
Theorem: List.nodupkeys_eq_of_fst_eq
Proof state before:
case right.cons.inr.intro.intro.intro.intro.intro.inr.inr
α : Type u_1
β : Type u_2
s s' : α × β
keys_eq : s.fst = s'.fst
goal_rw : (s = s') = (s.fst = s'.fst ∧ s.snd = s'.snd)
hd : α × β
tl : List (α × β)
a : α
l' : List α
nd1 : ∀ (a' : α), a' ∈ l' → ¬a = a'
nd2 : Pairwise (fun x x_1 => ¬x = x_1) (map (fun x => x.fst) tl)
hd_fst_eq_a : hd.fst = a
nd3 : map (fun x => x.fst) tl = l'
ih : s ∈ tl → s' ∈ tl → s.snd = s'.snd
s_in_tl : s ∈ tl
s'_in_tl : s' ∈ tl
⊢ s.snd = s'.snd
Tactic:
exact ih s_in_tl s'_in_tl
Proof state after:
no goals
Theorem: List.nodupkeys_eq_of_mk_mem
Proof state before:
α : Type u_1
β : Type u_2
a : α
b b' : β
l : List (α × β)
nd : l.Nodupkeys
h : (a, b) ∈ l
h' : (a, b') ∈ l
⊢ b = b'
Tactic:
have goal := nodupkeys_eq_of_fst_eq nd h h' rfl
Proof state after:
α : Type u_1
β : Type u_2
a : α
b b' : β
l : List (α × β)
nd : l.Nodupkeys
h : (a, b) ∈ l
h' : (a, b') ∈ l
goal : (a, b) = (a, b')
⊢ b = b'
Theorem: List.nodupkeys_eq_of_mk_mem
Proof state before:
α : Type u_1
β : Type u_2
a : α
b b' : β
l : List (α × β)
nd : l.Nodupkeys
h : (a, b) ∈ l
h' : (a, b') ∈ l
goal : (a, b) = (a, b')
⊢ b = b'
Tactic:
simp only [Prod.mk.injEq, true_and] at goal
Proof state after:
α : Type u_1
β : Type u_2
a : α
b b' : β
l : List (α × β)
nd : l.Nodupkeys
h : (a, b) ∈ l
h' : (a, b') ∈ l
goal : b = b'
⊢ b = b'
Theorem: List.nodupkeys_eq_of_mk_mem
Proof state before:
α : Type u_1
β : Type u_2
a : α
b b' : β
l : List (α × β)
nd : l.Nodupkeys
h : (a, b) ∈ l
h' : (a, b') ∈ l
goal : b = b'
⊢ b = b'
Tactic:
exact goal
Proof state after:
no goals
Theorem: bitwise_unit_1
Proof state before:
x y : BitVec 64
⊢ ~~~(x &&& y) = ~~~x ||| ~~~y
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitwise_unit_1'
Proof state before:
x y : BitVec 64
⊢ ~~~x.and y = x.not ||| ~~~y
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitwise_unit_2
Proof state before:
x : BitVec 64
⊢ x ^^^ x = 0
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitwise_unit_2'
Proof state before:
x : BitVec 64
⊢ x.xor x = 0
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitwise_unit_3
Proof state before:
x : BitVec 64
⊢ (x ^^^ x).getLsb 32 = false
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitwise_unit_4
Proof state before:
x : BitVec 64
⊢ (x ^^^ ~~~x).getLsb 32 = true
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitwise_unit_5
Proof state before:
x : BitVec 64
⊢ (x ^^^ ~~~x).getLsb 128 = false
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitwise_unit_6
Proof state before:
x : BitVec 64
⊢ (x ^^^ ~~~x).getLsb 63 = (x ^^^ ~~~x).msb
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitwise_unit_7
Proof state before:
x : BitVec 32
⊢ 123 < 2 ^ 32
Tactic:
decide
Proof state after:
no goals
Theorem: bitwise_unit_7
Proof state before:
x : BitVec 32
⊢ x ^^^ 123#32 = 123#'⋯ ^^^ x
Tactic:
bv_decide
Proof state after:
no goals
Theorem: AIG.Ref_cast'
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig1 aig2 : AIG α
ref : aig1.Ref
h : aig1.decls.size ≤ aig2.decls.size
⊢ ref.gate < aig2.decls.size
Tactic:
have := ref.hgate
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig1 aig2 : AIG α
ref : aig1.Ref
h : aig1.decls.size ≤ aig2.decls.size
this : ref.gate < aig1.decls.size
⊢ ref.gate < aig2.decls.size
Theorem: AIG.Ref_cast'
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig1 aig2 : AIG α
ref : aig1.Ref
h : aig1.decls.size ≤ aig2.decls.size
this : ref.gate < aig1.decls.size
⊢ ref.gate < aig2.decls.size
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.BinaryInput.cast_each
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig1 aig2 : AIG α
lhs rhs : aig1.Ref
h1 h2 : aig1.decls.size ≤ aig2.decls.size
⊢ { lhs := lhs.cast h1, rhs := rhs.cast h2 } = { lhs := lhs, rhs := rhs }.cast h2
Tactic:
simp [BinaryInput.cast]
Proof state after:
no goals
Theorem: AIG.denote_projected_entry
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
entry : Entrypoint α
⊢ ⟦{ aig := entry.aig, ref := entry.ref }, assign⟧ = ⟦entry, assign⟧
Tactic:
cases entry
Proof state after:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig✝ : AIG α
ref✝ : aig✝.Ref
⊢ ⟦{ aig := { aig := aig✝, ref := ref✝ }.aig, ref := { aig := aig✝, ref := ref✝ }.ref }, assign⟧ =
    ⟦{ aig := aig✝, ref := ref✝ }, assign⟧
Theorem: AIG.denote_projected_entry
Proof state before:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig✝ : AIG α
ref✝ : aig✝.Ref
⊢ ⟦{ aig := { aig := aig✝, ref := ref✝ }.aig, ref := { aig := aig✝, ref := ref✝ }.ref }, assign⟧ =
    ⟦{ aig := aig✝, ref := ref✝ }, assign⟧
Tactic:
simp
Proof state after:
no goals
Theorem: AIG.denote_projected_entry'
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
entry : Entrypoint α
⊢ ⟦{ aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }, assign⟧ = ⟦entry, assign⟧
Tactic:
cases entry
Proof state after:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig✝ : AIG α
ref✝ : aig✝.Ref
⊢ ⟦{ aig := { aig := aig✝, ref := ref✝ }.aig, ref := { gate := { aig := aig✝, ref := ref✝ }.ref.gate, hgate := ⋯ } },
      assign⟧ =
    ⟦{ aig := aig✝, ref := ref✝ }, assign⟧
Theorem: AIG.denote_projected_entry'
Proof state before:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig✝ : AIG α
ref✝ : aig✝.Ref
⊢ ⟦{ aig := { aig := aig✝, ref := ref✝ }.aig, ref := { gate := { aig := aig✝, ref := ref✝ }.ref.gate, hgate := ⋯ } },
      assign⟧ =
    ⟦{ aig := aig✝, ref := ref✝ }, assign⟧
Tactic:
simp
Proof state after:
no goals
Theorem: AIG.mkGate_le_size
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
⊢ aig.decls.size ≤ (aig.mkGate input).aig.decls.size
Tactic:
simp_arith [mkGate]
Proof state after:
no goals
Theorem: AIG.mkGate_decl_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.GateInput
h : idx < aig.decls.size
this : aig.decls.size ≤ (aig.mkGate input).aig.decls.size
⊢ idx < (aig.mkGate input).aig.decls.size
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.mkGate_decl_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.GateInput
h : idx < aig.decls.size
⊢ let_fun this := ⋯;
  (aig.mkGate input).aig.decls[idx] = aig.decls[idx]
Tactic:
simp only [mkGate, Array.get_push]
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.GateInput
h : idx < aig.decls.size
⊢ (if h : idx < aig.decls.size then aig.decls[idx]
    else Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) =
    aig.decls[idx]
Theorem: AIG.mkGate_decl_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.GateInput
h : idx < aig.decls.size
⊢ (if h : idx < aig.decls.size then aig.decls[idx]
    else Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) =
    aig.decls[idx]
Tactic:
split
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.GateInput
h h✝ : idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.GateInput
h : idx < aig.decls.size
h✝ : ¬idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]
Theorem: AIG.mkGate_decl_eq
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.GateInput
h h✝ : idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.GateInput
h : idx < aig.decls.size
h✝ : ¬idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]
Tactic:
. rfl
Proof state after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.GateInput
h : idx < aig.decls.size
h✝ : ¬idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]
Theorem: AIG.mkGate_decl_eq
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.GateInput
h : idx < aig.decls.size
h✝ : ¬idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]
Tactic:
. contradiction
Proof state after:
no goals
Theorem: AIG.mkGate_decl_eq
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.GateInput
h h✝ : idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]
Tactic:
rfl
Proof state after:
no goals
Theorem: AIG.mkGate_decl_eq
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
idx : Nat
aig : AIG α
input : aig.GateInput
h : idx < aig.decls.size
h✝ : ¬idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]
Tactic:
contradiction
Proof state after:
no goals
Theorem: AIG.denote_mkGate
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
⊢ ⟦aig.mkGate input, assign⟧ =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)
Tactic:
conv =>
  lhs
  unfold denote denote.go
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
⊢ (match elem : (aig.mkGate input).aig.decls[(aig.mkGate input).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.mkGate input).aig.decls assign ⋯ ⋯;
      let rval := denote.go rhs (aig.mkGate input).aig.decls assign ⋯ ⋯;
      xor lval linv && xor rval rinv) =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)
Theorem: AIG.denote_mkGate
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
⊢ (match elem : (aig.mkGate input).aig.decls[(aig.mkGate input).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.mkGate input).aig.decls assign ⋯ ⋯;
      let rval := denote.go rhs (aig.mkGate input).aig.decls assign ⋯ ⋯;
      xor lval linv && xor rval rinv) =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)
Tactic:
split
Proof state after:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
b✝ : Bool
heq✝ : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.const b✝
⊢ b✝ =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)

case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
idx✝ : α
heq✝ : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.atom idx✝
⊢ assign idx✝ =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)

case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯;
    xor lval linv✝ && xor rval rinv✝) =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)