internlm/Lean-Github huggingface dataset:
Theorem: flipBit_mergeBitRes_zero
Proof state before:
b : Bool
a✝ : ℕ
p : BV a✝
⊢ (flipBit 0) (mergeBitRes 0 b p) = finProdFinEquiv (p, bif b then 0 else 1)
Tactic:
simp_rw [flipBit_zero_apply, mergeBitRes_zero_divNat,
  mergeBitRes_zero_modNat, Bool.apply_cond (Fin.rev)]
Proof state after:
b : Bool
a✝ : ℕ
p : BV a✝
⊢ finProdFinEquiv (p, bif b then Fin.rev 1 else Fin.rev 0) = finProdFinEquiv (p, bif b then 0 else 1)
Theorem: flipBit_mergeBitRes_zero
Proof state before:
b : Bool
a✝ : ℕ
p : BV a✝
⊢ finProdFinEquiv (p, bif b then Fin.rev 1 else Fin.rev 0) = finProdFinEquiv (p, bif b then 0 else 1)
Tactic:
rfl
Proof state after:
no goals
Theorem: mergeBitRes_getRes_of_getBit_not
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
q : BV (a✝ + 1)
b : Bool
h : getBit i q = !b
⊢ mergeBitRes i b (getRes i q) = (flipBit i) q
Tactic:
simp_rw [flipBit_apply, h, Bool.not_not]
Proof state after:
no goals
Theorem: flipBit_succ
Proof state before:
a✝ : ℕ
q : BV (a✝ + 1 + 1)
i : Fin (a✝ + 1)
⊢ (flipBit i.succ) q = mergeBitRes 0 (getBit 0 q) ((flipBit i) (getRes 0 q))
Tactic:
simp_rw [flipBit_apply, getBit_succ, getRes_succ, mergeBitRes_succ,
getBit_mergeBitRes, getRes_mergeBitRes]
Proof state after:
no goals
Theorem: flipBit_castSucc
Proof state before:
a✝ : ℕ
q : BV (a✝ + 1 + 1)
i : Fin (a✝ + 1)
⊢ (flipBit i.castSucc) q =
    mergeBitRes (Fin.last (a✝ + 1)) (getBit (Fin.last (a✝ + 1)) q) ((flipBit i) (getRes (Fin.last (a✝ + 1)) q))
Tactic:
simp_rw [flipBit_apply, getBit_castSucc, getRes_castSucc, mergeBitRes_castSucc,
getBit_mergeBitRes, getRes_mergeBitRes]
Proof state after:
no goals
Theorem: flipBit_succAbove
Proof state before:
m : ℕ
i : Fin (m + 1)
q : BV (m + 1 + 1)
j : Fin (m + 2)
⊢ (flipBit (j.succAbove i)) q = mergeBitRes j (getBit j q) ((flipBit i) (getRes j q))
Tactic:
simp_rw [flipBit_apply, getBit_succAbove, getRes_succAbove, mergeBitRes_succAbove,
getBit_mergeBitRes, getRes_mergeBitRes]
Proof state after:
no goals
Theorem: eq_flipBit_iff
Proof state before:
a✝ : ℕ
q : BV (a✝ + 1)
i : Fin (a✝ + 1)
r : BV (a✝ + 1)
⊢ q = (flipBit i) r ↔ getBit i q = !getBit i r ∧ getRes i q = getRes i r
Tactic:
rcases mergeBitRes_surj i q with ⟨bq, pq, rfl⟩
Proof state after:
case intro.intro
a✝ : ℕ
i : Fin (a✝ + 1)
r : BV (a✝ + 1)
bq : Bool
pq : BV a✝
⊢ mergeBitRes i bq pq = (flipBit i) r ↔
    getBit i (mergeBitRes i bq pq) = !getBit i r ∧ getRes i (mergeBitRes i bq pq) = getRes i r
Theorem: eq_flipBit_iff
Proof state before:
case intro.intro
a✝ : ℕ
i : Fin (a✝ + 1)
r : BV (a✝ + 1)
bq : Bool
pq : BV a✝
⊢ mergeBitRes i bq pq = (flipBit i) r ↔
    getBit i (mergeBitRes i bq pq) = !getBit i r ∧ getRes i (mergeBitRes i bq pq) = getRes i r
Tactic:
rcases mergeBitRes_surj i r with ⟨br, pr, rfl⟩
Proof state after:
case intro.intro.intro.intro
a✝ : ℕ
i : Fin (a✝ + 1)
bq : Bool
pq : BV a✝
br : Bool
pr : BV a✝
⊢ mergeBitRes i bq pq = (flipBit i) (mergeBitRes i br pr) ↔
    getBit i (mergeBitRes i bq pq) = !getBit i (mergeBitRes i br pr) ∧
      getRes i (mergeBitRes i bq pq) = getRes i (mergeBitRes i br pr)
Theorem: eq_flipBit_iff
Proof state before:
case intro.intro.intro.intro
a✝ : ℕ
i : Fin (a✝ + 1)
bq : Bool
pq : BV a✝
br : Bool
pr : BV a✝
⊢ mergeBitRes i bq pq = (flipBit i) (mergeBitRes i br pr) ↔
    getBit i (mergeBitRes i bq pq) = !getBit i (mergeBitRes i br pr) ∧
      getRes i (mergeBitRes i bq pq) = getRes i (mergeBitRes i br pr)
Tactic:
simp_rw [flipBit_mergeBitRes, getBit_mergeBitRes, getRes_mergeBitRes,
  mergeBitRes_inj_iff]
Proof state after:
no goals
Theorem: flipBit_flipBit
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
q : BV (a✝ + 1)
⊢ (flipBit i) ((flipBit i) q) = q
Tactic:
simp_rw [flipBit_apply (q := q), flipBit_mergeBitRes,
  Bool.not_not, mergeBitRes_getBit_getRes]
Proof state after:
no goals
Theorem: flipBit_mul_self
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
⊢ flipBit i * flipBit i = 1
Tactic:
rw [mul_eq_one_iff_inv_eq]
Proof state after:
a✝ : ℕ
i : Fin (a✝ + 1)
⊢ (flipBit i)⁻¹ = flipBit i
Theorem: flipBit_mul_self
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
⊢ (flipBit i)⁻¹ = flipBit i
Tactic:
exact flipBit_inv
Proof state after:
no goals
Theorem: flipBit_mul_cancel_right
Proof state before:
a✝ : ℕ
ρ : Equiv.Perm (BV (a✝ + 1))
i : Fin (a✝ + 1)
⊢ ρ * flipBit i * flipBit i = ρ
Tactic:
rw [mul_assoc, flipBit_mul_self, mul_one]
Proof state after:
no goals
Theorem: flipBit_mul_cancel_left
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
ρ : Equiv.Perm (BV (a✝ + 1))
⊢ flipBit i * (flipBit i * ρ) = ρ
Tactic:
rw [← mul_assoc, flipBit_mul_self, one_mul]
Proof state after:
no goals
Theorem: getBit_flipBit
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
q : BV (a✝ + 1)
⊢ getBit i ((flipBit i) q) = !getBit i q
Tactic:
simp_rw [flipBit_apply, getBit_mergeBitRes]
Proof state after:
no goals
Theorem: getRes_flipBit
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
q : BV (a✝ + 1)
⊢ getRes i ((flipBit i) q) = getRes i q
Tactic:
rw [flipBit_apply, getRes_mergeBitRes]
Proof state after:
no goals
Theorem: getBit_flipBit_of_ne
Proof state before:
m : ℕ
q : BV (m + 1)
i j : Fin (m + 1)
h : i ≠ j
⊢ getBit i ((flipBit j) q) = getBit i q
Tactic:
cases m
Proof state after:
case zero
q : BV (0 + 1)
i j : Fin (0 + 1)
h : i ≠ j
⊢ getBit i ((flipBit j) q) = getBit i q

case succ
n✝ : ℕ
q : BV (n✝ + 1 + 1)
i j : Fin (n✝ + 1 + 1)
h : i ≠ j
⊢ getBit i ((flipBit j) q) = getBit i q
Theorem: getBit_flipBit_of_ne
Proof state before:
case zero
q : BV (0 + 1)
i j : Fin (0 + 1)
h : i ≠ j
⊢ getBit i ((flipBit j) q) = getBit i q
Tactic:
exact (h ((Fin.subsingleton_one).elim i j)).elim
Proof state after:
no goals
Theorem: getBit_flipBit_of_ne
Proof state before:
case succ
n✝ : ℕ
q : BV (n✝ + 1 + 1)
i j : Fin (n✝ + 1 + 1)
h : i ≠ j
⊢ getBit i ((flipBit j) q) = getBit i q
Tactic:
rcases Fin.exists_succAbove_eq h with ⟨k, rfl⟩
Proof state after:
case succ.intro
n✝ : ℕ
q : BV (n✝ + 1 + 1)
j : Fin (n✝ + 1 + 1)
k : Fin (n✝ + 1)
h : j.succAbove k ≠ j
⊢ getBit (j.succAbove k) ((flipBit j) q) = getBit (j.succAbove k) q
Theorem: getBit_flipBit_of_ne
Proof state before:
case succ.intro
n✝ : ℕ
q : BV (n✝ + 1 + 1)
j : Fin (n✝ + 1 + 1)
k : Fin (n✝ + 1)
h : j.succAbove k ≠ j
⊢ getBit (j.succAbove k) ((flipBit j) q) = getBit (j.succAbove k) q
Tactic:
simp_rw [getBit_succAbove, getRes_flipBit]
Proof state after:
no goals
Theorem: getBit_zero_flipBit_succ
Proof state before:
m : ℕ
q : BV (m + 1)
i : Fin m
⊢ getBit 0 ((flipBit i.succ) q) = getBit 0 q
Tactic:
cases m
Proof state after:
case zero
q : BV (0 + 1)
i : Fin 0
⊢ getBit 0 ((flipBit i.succ) q) = getBit 0 q

case succ
n✝ : ℕ
q : BV (n✝ + 1 + 1)
i : Fin (n✝ + 1)
⊢ getBit 0 ((flipBit i.succ) q) = getBit 0 q
Theorem: getBit_zero_flipBit_succ
Proof state before:
case zero
q : BV (0 + 1)
i : Fin 0
⊢ getBit 0 ((flipBit i.succ) q) = getBit 0 q
Tactic:
exact i.elim0
Proof state after:
no goals
Theorem: getBit_zero_flipBit_succ
Proof state before:
case succ
n✝ : ℕ
q : BV (n✝ + 1 + 1)
i : Fin (n✝ + 1)
⊢ getBit 0 ((flipBit i.succ) q) = getBit 0 q
Tactic:
rw [flipBit_succ, getBit_mergeBitRes]
Proof state after:
no goals
Theorem: getBit_succ_flipBit_zero
Proof state before:
m : ℕ
q : BV (m + 1)
i : Fin m
⊢ getBit i.succ ((flipBit 0) q) = getBit i.succ q
Tactic:
cases m
Proof state after:
case zero
q : BV (0 + 1)
i : Fin 0
⊢ getBit i.succ ((flipBit 0) q) = getBit i.succ q

case succ
n✝ : ℕ
q : BV (n✝ + 1 + 1)
i : Fin (n✝ + 1)
⊢ getBit i.succ ((flipBit 0) q) = getBit i.succ q
Theorem: getBit_succ_flipBit_zero
Proof state before:
case zero
q : BV (0 + 1)
i : Fin 0
⊢ getBit i.succ ((flipBit 0) q) = getBit i.succ q
Tactic:
exact i.elim0
Proof state after:
no goals
Theorem: getBit_succ_flipBit_zero
Proof state before:
case succ
n✝ : ℕ
q : BV (n✝ + 1 + 1)
i : Fin (n✝ + 1)
⊢ getBit i.succ ((flipBit 0) q) = getBit i.succ q
Tactic:
simp_rw [getBit_succ, getRes_flipBit]
Proof state after:
no goals
Theorem: flipBit_ne_self
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
q : BV (a✝ + 1)
⊢ (flipBit i) q ≠ q
Tactic:
apply ne_of_getBit_ne i
Proof state after:
a✝ : ℕ
i : Fin (a✝ + 1)
q : BV (a✝ + 1)
⊢ getBit i ((flipBit i) q) ≠ getBit i q
Theorem: flipBit_ne_self
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
q : BV (a✝ + 1)
⊢ getBit i ((flipBit i) q) ≠ getBit i q
Tactic:
rw [getBit_flipBit, ne_eq, Bool.not_not_eq]
Proof state after:
no goals
Theorem: getRes_zero_eq_and_getBit_zero_opp_of_lt_of_flipBit_gt
Proof state before:
a✝ : ℕ
r q : BV (a✝ + 1)
h : r < q
hf : (flipBit 0) q < (flipBit 0) r
⊢ getBit 0 r = false ∧ getBit 0 q = true ∧ getRes 0 r = getRes 0 q
Tactic:
rcases mergeBitRes_surj 0 q with ⟨bq, pq, rfl⟩
Proof state after:
case intro.intro
a✝ : ℕ
r : BV (a✝ + 1)
bq : Bool
pq : BV a✝
h : r < mergeBitRes 0 bq pq
hf : (flipBit 0) (mergeBitRes 0 bq pq) < (flipBit 0) r
⊢ getBit 0 r = false ∧ getBit 0 (mergeBitRes 0 bq pq) = true ∧ getRes 0 r = getRes 0 (mergeBitRes 0 bq pq)
Theorem: getRes_zero_eq_and_getBit_zero_opp_of_lt_of_flipBit_gt
Proof state before:
case intro.intro
a✝ : ℕ
r : BV (a✝ + 1)
bq : Bool
pq : BV a✝
h : r < mergeBitRes 0 bq pq
hf : (flipBit 0) (mergeBitRes 0 bq pq) < (flipBit 0) r
⊢ getBit 0 r = false ∧ getBit 0 (mergeBitRes 0 bq pq) = true ∧ getRes 0 r = getRes 0 (mergeBitRes 0 bq pq)
Tactic:
rcases mergeBitRes_surj 0 r with ⟨br, pr, rfl⟩
Proof state after:
case intro.intro.intro.intro
a✝ : ℕ
bq : Bool
pq : BV a✝
br : Bool
pr : BV a✝
h : mergeBitRes 0 br pr < mergeBitRes 0 bq pq
hf : (flipBit 0) (mergeBitRes 0 bq pq) < (flipBit 0) (mergeBitRes 0 br pr)
⊢ getBit 0 (mergeBitRes 0 br pr) = false ∧
    getBit 0 (mergeBitRes 0 bq pq) = true ∧ getRes 0 (mergeBitRes 0 br pr) = getRes 0 (mergeBitRes 0 bq pq)
Theorem: getRes_zero_eq_and_getBit_zero_opp_of_lt_of_flipBit_gt
Proof state before:
case intro.intro.intro.intro
a✝ : ℕ
bq : Bool
pq : BV a✝
br : Bool
pr : BV a✝
h : mergeBitRes 0 br pr < mergeBitRes 0 bq pq
hf : (flipBit 0) (mergeBitRes 0 bq pq) < (flipBit 0) (mergeBitRes 0 br pr)
⊢ getBit 0 (mergeBitRes 0 br pr) = false ∧
    getBit 0 (mergeBitRes 0 bq pq) = true ∧ getRes 0 (mergeBitRes 0 br pr) = getRes 0 (mergeBitRes 0 bq pq)
Tactic:
simp_rw [flipBit_mergeBitRes, getBit_mergeBitRes, getRes_mergeBitRes,
  Fin.lt_iff_val_lt_val, mergeBitRes_zero, finProdFinEquiv_apply_val, Bool.cond_not, add_comm,
  Bool.apply_cond (Fin.val), Fin.val_one, Fin.val_zero] at hf h ⊢
Proof state after:
case intro.intro.intro.intro
a✝ : ℕ
bq : Bool
pq : BV a✝
br : Bool
pr : BV a✝
hf : (2 * ↑pq + bif bq then 0 else 1) < 2 * ↑pr + bif br then 0 else 1
h : (2 * ↑pr + bif br then 1 else 0) < 2 * ↑pq + bif bq then 1 else 0
⊢ br = false ∧ bq = true ∧ pr = pq
Theorem: getRes_zero_eq_and_getBit_zero_opp_of_lt_of_flipBit_gt
Proof state before:
case intro.intro.intro.intro
a✝ : ℕ
bq : Bool
pq : BV a✝
br : Bool
pr : BV a✝
hf : (2 * ↑pq + bif bq then 0 else 1) < 2 * ↑pr + bif br then 0 else 1
h : (2 * ↑pr + bif br then 1 else 0) < 2 * ↑pq + bif bq then 1 else 0
⊢ br = false ∧ bq = true ∧ pr = pq
Tactic:
rcases Nat.eq_false_true_of_cond_succ_lt_of_cond_succ_lt h hf with ⟨hr, hq, he⟩
Proof state after:
case intro.intro.intro.intro.intro.intro
a✝ : ℕ
bq : Bool
pq : BV a✝
br : Bool
pr : BV a✝
hf : (2 * ↑pq + bif bq then 0 else 1) < 2 * ↑pr + bif br then 0 else 1
h : (2 * ↑pr + bif br then 1 else 0) < 2 * ↑pq + bif bq then 1 else 0
hr : br = false
hq : bq = true
he : 2 * ↑pr = 2 * ↑pq
⊢ br = false ∧ bq = true ∧ pr = pq
Theorem: getRes_zero_eq_and_getBit_zero_opp_of_lt_of_flipBit_gt
Proof state before:
case intro.intro.intro.intro.intro.intro
a✝ : ℕ
bq : Bool
pq : BV a✝
br : Bool
pr : BV a✝
hf : (2 * ↑pq + bif bq then 0 else 1) < 2 * ↑pr + bif br then 0 else 1
h : (2 * ↑pr + bif br then 1 else 0) < 2 * ↑pq + bif bq then 1 else 0
hr : br = false
hq : bq = true
he : 2 * ↑pr = 2 * ↑pq
⊢ br = false ∧ bq = true ∧ pr = pq
Tactic:
exact ⟨hr, hq, Fin.ext (Nat.eq_of_mul_eq_mul_left zero_lt_two he)⟩
Proof state after:
no goals
Theorem: eq_flipBit_zero_of_lt_of_flipBit_zero_gt
Proof state before:
a✝ : ℕ
r q : BV (a✝ + 1)
h : r < q
hf : (flipBit 0) q < (flipBit 0) r
⊢ r = (flipBit 0) q
Tactic:
rcases getRes_zero_eq_and_getBit_zero_opp_of_lt_of_flipBit_gt h hf with ⟨hr, hq, hrq⟩
Proof state after:
case intro.intro
a✝ : ℕ
r q : BV (a✝ + 1)
h : r < q
hf : (flipBit 0) q < (flipBit 0) r
hr : getBit 0 r = false
hq : getBit 0 q = true
hrq : getRes 0 r = getRes 0 q
⊢ r = (flipBit 0) q
Theorem: eq_flipBit_zero_of_lt_of_flipBit_zero_gt
Proof state before:
case intro.intro
a✝ : ℕ
r q : BV (a✝ + 1)
h : r < q
hf : (flipBit 0) q < (flipBit 0) r
hr : getBit 0 r = false
hq : getBit 0 q = true
hrq : getRes 0 r = getRes 0 q
⊢ r = (flipBit 0) q
Tactic:
simp only [eq_flipBit_iff, hr, hq, hrq, Bool.not_true, and_self]
Proof state after:
no goals
Theorem: eq_flipBit_zero_of_lt_of_flipBit_zero_gt'
Proof state before:
a✝ : ℕ
r q : BV (a✝ + 1)
i : Fin (a✝ + 1)
h : r < q
hf : (flipBit i) q < (flipBit i) r
⊢ ∀ k ≥ i, getBit k r = getBit k ((flipBit i) q)
Tactic:
rcases mergeBitRes_surj i q with ⟨bq, pq, rfl⟩
Proof state after:
case intro.intro
a✝ : ℕ
r : BV (a✝ + 1)
i : Fin (a✝ + 1)
bq : Bool
pq : BV a✝
h : r < mergeBitRes i bq pq
hf : (flipBit i) (mergeBitRes i bq pq) < (flipBit i) r
⊢ ∀ k ≥ i, getBit k r = getBit k ((flipBit i) (mergeBitRes i bq pq))
Theorem: eq_flipBit_zero_of_lt_of_flipBit_zero_gt'
Proof state before:
case intro.intro
a✝ : ℕ
r : BV (a✝ + 1)
i : Fin (a✝ + 1)
bq : Bool
pq : BV a✝
h : r < mergeBitRes i bq pq
hf : (flipBit i) (mergeBitRes i bq pq) < (flipBit i) r
⊢ ∀ k ≥ i, getBit k r = getBit k ((flipBit i) (mergeBitRes i bq pq))
Tactic:
rcases mergeBitRes_surj i r with ⟨br, pr, rfl⟩
Proof state after:
case intro.intro.intro.intro
a✝ : ℕ
i : Fin (a✝ + 1)
bq : Bool
pq : BV a✝
br : Bool
pr : BV a✝
h : mergeBitRes i br pr < mergeBitRes i bq pq
hf : (flipBit i) (mergeBitRes i bq pq) < (flipBit i) (mergeBitRes i br pr)
⊢ ∀ k ≥ i, getBit k (mergeBitRes i br pr) = getBit k ((flipBit i) (mergeBitRes i bq pq))
Theorem: eq_flipBit_zero_of_lt_of_flipBit_zero_gt'
Proof state before:
case intro.intro.intro.intro
a✝ : ℕ
i : Fin (a✝ + 1)
bq : Bool
pq : BV a✝
br : Bool
pr : BV a✝
h : mergeBitRes i br pr < mergeBitRes i bq pq
hf : (flipBit i) (mergeBitRes i bq pq) < (flipBit i) (mergeBitRes i br pr)
⊢ ∀ k ≥ i, getBit k (mergeBitRes i br pr) = getBit k ((flipBit i) (mergeBitRes i bq pq))
Tactic:
simp_rw [flipBit_mergeBitRes] at hf
Proof state after:
case intro.intro.intro.intro
a✝ : ℕ
i : Fin (a✝ + 1)
bq : Bool
pq : BV a✝
br : Bool
pr : BV a✝
h : mergeBitRes i br pr < mergeBitRes i bq pq
hf : mergeBitRes i (!bq) pq < mergeBitRes i (!br) pr
⊢ ∀ k ≥ i, getBit k (mergeBitRes i br pr) = getBit k ((flipBit i) (mergeBitRes i bq pq))
Theorem: eq_flipBit_zero_of_lt_of_flipBit_zero_gt'
Proof state before:
case intro.intro.intro.intro
a✝ : ℕ
i : Fin (a✝ + 1)
bq : Bool
pq : BV a✝
br : Bool
pr : BV a✝
h : mergeBitRes i br pr < mergeBitRes i bq pq
hf : mergeBitRes i (!bq) pq < mergeBitRes i (!br) pr
⊢ ∀ k ≥ i, getBit k (mergeBitRes i br pr) = getBit k ((flipBit i) (mergeBitRes i bq pq))
Tactic:
cases br <;> cases bq
Proof state after:
case intro.intro.intro.intro.false.false
a✝ : ℕ
i : Fin (a✝ + 1)
pq pr : BV a✝
h : mergeBitRes i false pr < mergeBitRes i false pq
hf : mergeBitRes i (!false) pq < mergeBitRes i (!false) pr
⊢ ∀ k ≥ i, getBit k (mergeBitRes i false pr) = getBit k ((flipBit i) (mergeBitRes i false pq))

case intro.intro.intro.intro.false.true
a✝ : ℕ
i : Fin (a✝ + 1)
pq pr : BV a✝
h : mergeBitRes i false pr < mergeBitRes i true pq
hf : mergeBitRes i (!true) pq < mergeBitRes i (!false) pr
⊢ ∀ k ≥ i, getBit k (mergeBitRes i false pr) = getBit k ((flipBit i) (mergeBitRes i true pq))

case intro.intro.intro.intro.true.false
a✝ : ℕ
i : Fin (a✝ + 1)
pq pr : BV a✝
h : mergeBitRes i true pr < mergeBitRes i false pq
hf : mergeBitRes i (!false) pq < mergeBitRes i (!true) pr
⊢ ∀ k ≥ i, getBit k (mergeBitRes i true pr) = getBit k ((flipBit i) (mergeBitRes i false pq))

case intro.intro.intro.intro.true.true
a✝ : ℕ
i : Fin (a✝ + 1)
pq pr : BV a✝
h : mergeBitRes i true pr < mergeBitRes i true pq
hf : mergeBitRes i (!true) pq < mergeBitRes i (!true) pr
⊢ ∀ k ≥ i, getBit k (mergeBitRes i true pr) = getBit k ((flipBit i) (mergeBitRes i true pq))
Theorem: eq_flipBit_zero_of_lt_of_flipBit_zero_gt'
Proof state before:
case intro.intro.intro.intro.false.false
a✝ : ℕ
i : Fin (a✝ + 1)
pq pr : BV a✝
h : mergeBitRes i false pr < mergeBitRes i false pq
hf : mergeBitRes i (!false) pq < mergeBitRes i (!false) pr
⊢ ∀ k ≥ i, getBit k (mergeBitRes i false pr) = getBit k ((flipBit i) (mergeBitRes i false pq))
Tactic:
sorry
Proof state after:
no goals
Theorem: eq_flipBit_zero_of_lt_of_flipBit_zero_gt'
Proof state before:
case intro.intro.intro.intro.false.true
a✝ : ℕ
i : Fin (a✝ + 1)
pq pr : BV a✝
h : mergeBitRes i false pr < mergeBitRes i true pq
hf : mergeBitRes i (!true) pq < mergeBitRes i (!false) pr
⊢ ∀ k ≥ i, getBit k (mergeBitRes i false pr) = getBit k ((flipBit i) (mergeBitRes i true pq))
Tactic:
sorry
Proof state after:
no goals
Theorem: eq_flipBit_zero_of_lt_of_flipBit_zero_gt'
Proof state before:
case intro.intro.intro.intro.true.false
a✝ : ℕ
i : Fin (a✝ + 1)
pq pr : BV a✝
h : mergeBitRes i true pr < mergeBitRes i false pq
hf : mergeBitRes i (!false) pq < mergeBitRes i (!true) pr
⊢ ∀ k ≥ i, getBit k (mergeBitRes i true pr) = getBit k ((flipBit i) (mergeBitRes i false pq))
Tactic:
sorry
Proof state after:
no goals
Theorem: eq_flipBit_zero_of_lt_of_flipBit_zero_gt'
Proof state before:
case intro.intro.intro.intro.true.true
a✝ : ℕ
i : Fin (a✝ + 1)
pq pr : BV a✝
h : mergeBitRes i true pr < mergeBitRes i true pq
hf : mergeBitRes i (!true) pq < mergeBitRes i (!true) pr
⊢ ∀ k ≥ i, getBit k (mergeBitRes i true pr) = getBit k ((flipBit i) (mergeBitRes i true pq))
Tactic:
sorry
Proof state after:
no goals
Theorem: condFlipBitCore_condFlipBitCore
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
⊢ condFlipBitCore i c (condFlipBitCore i c q) = q
Tactic:
rcases (c (getRes i q)).dichotomy with h | h <;>
simp only [condFlipBitCore, h, cond_true, cond_false, getRes_flipBit, flipBit_flipBit]
Proof state after:
no goals
Theorem: condFlipBit_apply_eq_mergeBitRes
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
⊢ (condFlipBit i c) q = mergeBitRes i (xor (c (getRes i q)) (getBit i q)) (getRes i q)
Tactic:
rw [condFlipBit_apply]
Proof state after:
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
⊢ (bif c (getRes i q) then (flipBit i) q else q) = mergeBitRes i (xor (c (getRes i q)) (getBit i q)) (getRes i q)
Theorem: condFlipBit_apply_eq_mergeBitRes
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
⊢ (bif c (getRes i q) then (flipBit i) q else q) = mergeBitRes i (xor (c (getRes i q)) (getBit i q)) (getRes i q)
Tactic:
cases (c (getRes i q))
Proof state after:
case false
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
⊢ (bif false then (flipBit i) q else q) = mergeBitRes i (xor false (getBit i q)) (getRes i q)

case true
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
⊢ (bif true then (flipBit i) q else q) = mergeBitRes i (xor true (getBit i q)) (getRes i q)
Theorem: condFlipBit_apply_eq_mergeBitRes
Proof state before:
case false
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
⊢ (bif false then (flipBit i) q else q) = mergeBitRes i (xor false (getBit i q)) (getRes i q)
Tactic:
rw [cond_false, Bool.false_xor, mergeBitRes_getBit_getRes]
Proof state after:
no goals
Theorem: condFlipBit_apply_eq_mergeBitRes
Proof state before:
case true
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
⊢ (bif true then (flipBit i) q else q) = mergeBitRes i (xor true (getBit i q)) (getRes i q)
Tactic:
rw [cond_true, Bool.true_xor, flipBit_apply]
Proof state after:
no goals
Theorem: condFlipBit_apply_eq_swap_apply
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
⊢ (condFlipBit i c) q = (Equiv.swap q (mergeBitRes i (xor (c (getRes i q)) (getBit i q)) (getRes i q))) q
Tactic:
exact condFlipBit_apply_eq_mergeBitRes.trans (Equiv.swap_apply_left _ _).symm
Proof state after:
no goals
Theorem: condFlipBit_base
Proof state before:
i : Fin (0 + 1)
c : BV 0 → Bool
⊢ condFlipBit i c = bif c 0 then Equiv.swap 0 1 else 1
Tactic:
ext q : 1
Proof state after:
case H
i : Fin (0 + 1)
c : BV 0 → Bool
q : BV (0 + 1)
⊢ (condFlipBit i c) q = (bif c 0 then Equiv.swap 0 1 else 1) q
Theorem: condFlipBit_base
Proof state before:
case H
i : Fin (0 + 1)
c : BV 0 → Bool
q : BV (0 + 1)
⊢ (condFlipBit i c) q = (bif c 0 then Equiv.swap 0 1 else 1) q
Tactic:
rw [condFlipBit_apply, Fin.eq_zero (getRes i q), flipBit_base]
Proof state after:
case H
i : Fin (0 + 1)
c : BV 0 → Bool
q : BV (0 + 1)
⊢ (bif c 0 then (Equiv.swap 0 1) q else q) = (bif c 0 then Equiv.swap 0 1 else 1) q
Theorem: condFlipBit_base
Proof state before:
case H
i : Fin (0 + 1)
c : BV 0 → Bool
q : BV (0 + 1)
⊢ (bif c 0 then (Equiv.swap 0 1) q else q) = (bif c 0 then Equiv.swap 0 1 else 1) q
Tactic:
cases (c 0) <;> rfl
Proof state after:
no goals
Theorem: condFlipBit_mergeBitRes
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
b : Bool
p : BV a✝
⊢ (condFlipBit i c) (mergeBitRes i b p) = mergeBitRes i (xor (c p) b) p
Tactic:
rw [condFlipBit_apply_eq_mergeBitRes, getRes_mergeBitRes, getBit_mergeBitRes]
Proof state after:
no goals
Theorem: condFlipBit_mul_self
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
⊢ condFlipBit i c * condFlipBit i c = 1
Tactic:
ext
Proof state after:
case H.h
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
x✝ : BV (a✝ + 1)
⊢ ↑((condFlipBit i c * condFlipBit i c) x✝) = ↑(1 x✝)
Theorem: condFlipBit_mul_self
Proof state before:
case H.h
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
x✝ : BV (a✝ + 1)
⊢ ↑((condFlipBit i c * condFlipBit i c) x✝) = ↑(1 x✝)
Tactic:
simp_rw [Equiv.Perm.coe_mul, Function.comp_apply,
condFlipBit_condFlipBit, Equiv.Perm.coe_one, id_eq]
Proof state after:
no goals
Theorem: condFlipBit_mul_cancel_right
Proof state before:
a✝ : ℕ
ρ : Equiv.Perm (BV (a✝ + 1))
i : Fin (a✝ + 1)
c : BV a✝ → Bool
⊢ ρ * condFlipBit i c * condFlipBit i c = ρ
Tactic:
rw [mul_assoc, condFlipBit_mul_self, mul_one]
Proof state after:
no goals
Theorem: condFlipBit_mul_cancel_left
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
ρ : Equiv.Perm (BV (a✝ + 1))
⊢ condFlipBit i c * (condFlipBit i c * ρ) = ρ
Tactic:
rw [← mul_assoc, condFlipBit_mul_self, one_mul]
Proof state after:
no goals
Theorem: condFlipBit_flipBit_of_all_true
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
⊢ flipBit i = condFlipBit i (Function.const (BV a✝) true)
Tactic:
ext
Proof state after:
case H.h
a✝ : ℕ
i : Fin (a✝ + 1)
x✝ : BV (a✝ + 1)
⊢ ↑((flipBit i) x✝) = ↑((condFlipBit i (Function.const (BV a✝) true)) x✝)
Theorem: condFlipBit_flipBit_of_all_true
Proof state before:
case H.h
a✝ : ℕ
i : Fin (a✝ + 1)
x✝ : BV (a✝ + 1)
⊢ ↑((flipBit i) x✝) = ↑((condFlipBit i (Function.const (BV a✝) true)) x✝)
Tactic:
rw [condFlipBit_apply]
Proof state after:
case H.h
a✝ : ℕ
i : Fin (a✝ + 1)
x✝ : BV (a✝ + 1)
⊢ ↑((flipBit i) x✝) = ↑(bif Function.const (BV a✝) true (getRes i x✝) then (flipBit i) x✝ else x✝)
Theorem: condFlipBit_flipBit_of_all_true
Proof state before:
case H.h
a✝ : ℕ
i : Fin (a✝ + 1)
x✝ : BV (a✝ + 1)
⊢ ↑((flipBit i) x✝) = ↑(bif Function.const (BV a✝) true (getRes i x✝) then (flipBit i) x✝ else x✝)
Tactic:
rfl
Proof state after:
no goals
Theorem: condFlipBit_apply_comm
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
c d : BV a✝ → Bool
q : BV (a✝ + 1)
⊢ (condFlipBit i c) ((condFlipBit i d) q) = (condFlipBit i d) ((condFlipBit i c) q)
Tactic:
simp_rw [condFlipBit_apply_eq_mergeBitRes, getRes_mergeBitRes,
  getBit_mergeBitRes, Bool.xor_left_comm]
Proof state after:
no goals
Theorem: condFlipBit_comm
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
c d : BV a✝ → Bool
⊢ condFlipBit i c * condFlipBit i d = condFlipBit i d * condFlipBit i c
Tactic:
ext
Proof state after:
case H.h
a✝ : ℕ
i : Fin (a✝ + 1)
c d : BV a✝ → Bool
x✝ : BV (a✝ + 1)
⊢ ↑((condFlipBit i c * condFlipBit i d) x✝) = ↑((condFlipBit i d * condFlipBit i c) x✝)
Theorem: condFlipBit_comm
Proof state before:
case H.h
a✝ : ℕ
i : Fin (a✝ + 1)
c d : BV a✝ → Bool
x✝ : BV (a✝ + 1)
⊢ ↑((condFlipBit i c * condFlipBit i d) x✝) = ↑((condFlipBit i d * condFlipBit i c) x✝)
Tactic:
simp_rw [Equiv.Perm.coe_mul, Function.comp_apply, condFlipBit_apply_comm]
Proof state after:
no goals
Theorem: condFlipBit_apply_comm_flipBit
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
⊢ (condFlipBit i c) ((flipBit i) q) = (flipBit i) ((condFlipBit i c) q)
Tactic:
rw [condFlipBit_flipBit_of_all_true, condFlipBit_apply_comm]
Proof state after:
no goals