internlm/Lean-Github huggingface dataset:
Theorem: getBitRes_castSucc_symm_apply
Proof state before:
m : ℕ
b : Bool
p : BV (m + 1)
i : Fin (m + 1)
⊢ (getBitRes i.castSucc).symm (b, p) =
    (getBitRes (Fin.last (m + 1))).symm
      (((getBitRes (Fin.last m)) p).1, (getBitRes i).symm (b, ((getBitRes (Fin.last m)) p).2))
Tactic:
rw [getBitRes_castSucc, getBitResCastSucc_symm_apply]
Proof state after:
no goals
Theorem: getRes_castSucc
Proof state before:
m : ℕ
q : BV (m + 1 + 1)
i : Fin (m + 1)
⊢ getRes i.castSucc q = mergeBitRes (Fin.last m) (getBit (Fin.last (m + 1)) q) (getRes i (getRes (Fin.last (m + 1)) q))
Tactic:
simp_rw [getRes_apply, mergeBitRes_apply, getBit_apply, getBitRes_castSucc_apply]
Proof state after:
no goals
Theorem: getBit_castSucc
Proof state before:
m : ℕ
q : BV (m + 1 + 1)
i : Fin (m + 1)
⊢ getBit i.castSucc q = getBit i (getRes (Fin.last (m + 1)) q)
Tactic:
simp_rw [getRes_apply, getBit_apply, getBitRes_castSucc_apply]
Proof state after:
no goals
Theorem: mergeBitRes_castSucc
Proof state before:
m : ℕ
b : Bool
q : BV (m + 1)
i : Fin (m + 1)
⊢ mergeBitRes i.castSucc b q =
    mergeBitRes (Fin.last (m + 1)) (getBit (Fin.last m) q) (mergeBitRes i b (getRes (Fin.last m) q))
Tactic:
simp_rw [mergeBitRes_apply, getBit_apply, getRes_apply, getBitRes_castSucc_symm_apply]
Proof state after:
no goals
Theorem: getBitRes_succAbove
Proof state before:
m : ℕ
j : Fin (m + 2)
i : Fin (m + 1)
⊢ getBitRes (j.succAbove i) = getBitResSuccAbove j i
Tactic:
simp_rw [Equiv.ext_iff, getBitResSuccAbove_apply,
  getBitRes_apply, getBitRes_symm_apply, Equiv.symm_apply_apply,
  Prod.mk.injEq, EmbeddingLike.apply_eq_iff_eq,
  Fin.eq_insertNth_iff, Fin.succAbove_succAbove_predAbove,
  Fin.succAbove_succAbove_predAbove_succAbove, true_and, implies_true]
Proof state after:
no goals
Theorem: getBitRes_succAbove_apply
Proof state before:
m : ℕ
q : BV (m + 1 + 1)
j : Fin (m + 2)
i : Fin (m + 1)
⊢ (getBitRes (j.succAbove i)) q =
    (((getBitRes i) ((getBitRes j) q).2).1,
      (getBitRes (i.predAbove j)).symm (((getBitRes j) q).1, ((getBitRes i) ((getBitRes j) q).2).2))
Tactic:
rw [getBitRes_succAbove, getBitResSuccAbove_apply]
Proof state after:
no goals
Theorem: getBitRes_succAbove_symm_apply
Proof state before:
m : ℕ
b : Bool
p : BV (m + 1)
j : Fin (m + 2)
i : Fin (m + 1)
⊢ (getBitRes (j.succAbove i)).symm (b, p) =
    (getBitRes j).symm (((getBitRes (i.predAbove j)) p).1, (getBitRes i).symm (b, ((getBitRes (i.predAbove j)) p).2))
Tactic:
rw [getBitRes_succAbove, getBitResSuccAbove_symm_apply]
Proof state after:
no goals
Theorem: getRes_succAbove
Proof state before:
m : ℕ
q : BV (m + 1 + 1)
j : Fin (m + 2)
i : Fin (m + 1)
⊢ getRes (j.succAbove i) q = mergeBitRes (i.predAbove j) (getBit j q) (getRes i (getRes j q))
Tactic:
simp_rw [getRes_apply, mergeBitRes_apply, getBit_apply, getBitRes_succAbove_apply]
Proof state after:
no goals
Theorem: getBit_succAbove
Proof state before:
m : ℕ
q : BV (m + 1 + 1)
j : Fin (m + 2)
i : Fin (m + 1)
⊢ getBit (j.succAbove i) q = getBit i (getRes j q)
Tactic:
simp_rw [getRes_apply, getBit_apply, getBitRes_succAbove_apply]
Proof state after:
no goals
Theorem: mergeBitRes_succAbove
Proof state before:
m : ℕ
b : Bool
q : BV (m + 1)
j : Fin (m + 2)
i : Fin (m + 1)
⊢ mergeBitRes (j.succAbove i) b q =
    mergeBitRes j (getBit (i.predAbove j) q) (mergeBitRes i b (getRes (i.predAbove j) q))
Tactic:
simp_rw [mergeBitRes_apply, getBit_apply, getRes_apply, getBitRes_succAbove_symm_apply]
Proof state after:
no goals
Theorem: getBit_mergeBitRes
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
b : Bool
p : BV a✝
⊢ getBit i (mergeBitRes i b p) = b
Tactic:
simp_rw [getBit_apply, mergeBitRes_apply, Equiv.apply_symm_apply]
Proof state after:
no goals
Theorem: getRes_mergeBitRes
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
b : Bool
p : BV a✝
⊢ getRes i (mergeBitRes i b p) = p
Tactic:
simp_rw [getRes_apply, mergeBitRes_apply, Equiv.apply_symm_apply]
Proof state after:
no goals
Theorem: mergeBitRes_getBit_getRes
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
q : BV (a✝ + 1)
⊢ mergeBitRes i (getBit i q) (getRes i q) = q
Tactic:
simp_rw [getRes_apply, mergeBitRes_apply, getBit_apply, Prod.mk.eta, Equiv.symm_apply_apply]
Proof state after:
no goals
Theorem: mergeBitRes_Bool_inj
Proof state before:
m : ℕ
b₁ : Bool
p₁ : BV m
b₂ : Bool
p₂ : BV m
i : Fin (m + 1)
h : mergeBitRes i b₁ p₁ = mergeBitRes i b₂ p₂
⊢ b₁ = b₂
Tactic:
have h₂ := (congrArg (getBit i) h)
Proof state after:
m : ℕ
b₁ : Bool
p₁ : BV m
b₂ : Bool
p₂ : BV m
i : Fin (m + 1)
h : mergeBitRes i b₁ p₁ = mergeBitRes i b₂ p₂
h₂ : getBit i (mergeBitRes i b₁ p₁) = getBit i (mergeBitRes i b₂ p₂)
⊢ b₁ = b₂
Theorem: mergeBitRes_Bool_inj
Proof state before:
m : ℕ
b₁ : Bool
p₁ : BV m
b₂ : Bool
p₂ : BV m
i : Fin (m + 1)
h : mergeBitRes i b₁ p₁ = mergeBitRes i b₂ p₂
h₂ : getBit i (mergeBitRes i b₁ p₁) = getBit i (mergeBitRes i b₂ p₂)
⊢ b₁ = b₂
Tactic:
simp only [getBit_mergeBitRes] at h₂
Proof state after:
m : ℕ
b₁ : Bool
p₁ : BV m
b₂ : Bool
p₂ : BV m
i : Fin (m + 1)
h : mergeBitRes i b₁ p₁ = mergeBitRes i b₂ p₂
h₂ : b₁ = b₂
⊢ b₁ = b₂
Theorem: mergeBitRes_Bool_inj
Proof state before:
m : ℕ
b₁ : Bool
p₁ : BV m
b₂ : Bool
p₂ : BV m
i : Fin (m + 1)
h : mergeBitRes i b₁ p₁ = mergeBitRes i b₂ p₂
h₂ : b₁ = b₂
⊢ b₁ = b₂
Tactic:
exact h₂
Proof state after:
no goals
Theorem: mergeBitRes_Fin_inj
Proof state before:
m : ℕ
b₁ : Bool
p₁ : BV m
b₂ : Bool
p₂ : BV m
i : Fin (m + 1)
h : mergeBitRes i b₁ p₁ = mergeBitRes i b₂ p₂
⊢ p₁ = p₂
Tactic:
have h₂ := (congrArg (getRes i) h)
Proof state after:
m : ℕ
b₁ : Bool
p₁ : BV m
b₂ : Bool
p₂ : BV m
i : Fin (m + 1)
h : mergeBitRes i b₁ p₁ = mergeBitRes i b₂ p₂
h₂ : getRes i (mergeBitRes i b₁ p₁) = getRes i (mergeBitRes i b₂ p₂)
⊢ p₁ = p₂
Theorem: mergeBitRes_Fin_inj
Proof state before:
m : ℕ
b₁ : Bool
p₁ : BV m
b₂ : Bool
p₂ : BV m
i : Fin (m + 1)
h : mergeBitRes i b₁ p₁ = mergeBitRes i b₂ p₂
h₂ : getRes i (mergeBitRes i b₁ p₁) = getRes i (mergeBitRes i b₂ p₂)
⊢ p₁ = p₂
Tactic:
simp_rw [getRes_mergeBitRes] at h₂
Proof state after:
m : ℕ
b₁ : Bool
p₁ : BV m
b₂ : Bool
p₂ : BV m
i : Fin (m + 1)
h : mergeBitRes i b₁ p₁ = mergeBitRes i b₂ p₂
h₂ : p₁ = p₂
⊢ p₁ = p₂
Theorem: mergeBitRes_Fin_inj
Proof state before:
m : ℕ
b₁ : Bool
p₁ : BV m
b₂ : Bool
p₂ : BV m
i : Fin (m + 1)
h : mergeBitRes i b₁ p₁ = mergeBitRes i b₂ p₂
h₂ : p₁ = p₂
⊢ p₁ = p₂
Tactic:
exact h₂
Proof state after:
no goals
Theorem: mergeBitRes_inj_iff
Proof state before:
m : ℕ
b₁ : Bool
p₁ : BV m
b₂ : Bool
p₂ : BV m
i : Fin (m + 1)
⊢ b₁ = b₂ ∧ p₁ = p₂ → mergeBitRes i b₁ p₁ = mergeBitRes i b₂ p₂
Tactic:
rintro ⟨rfl, rfl⟩
Proof state after:
case intro
m : ℕ
b₁ : Bool
p₁ : BV m
i : Fin (m + 1)
⊢ mergeBitRes i b₁ p₁ = mergeBitRes i b₁ p₁
Theorem: mergeBitRes_inj_iff
Proof state before:
case intro
m : ℕ
b₁ : Bool
p₁ : BV m
i : Fin (m + 1)
⊢ mergeBitRes i b₁ p₁ = mergeBitRes i b₁ p₁
Tactic:
rfl
Proof state after:
no goals
Theorem: mergeBitRes_ne_inj_iff
Proof state before:
m : ℕ
b₁ : Bool
p₁ : BV m
b₂ : Bool
p₂ : BV m
i : Fin (m + 1)
⊢ mergeBitRes i b₁ p₁ ≠ mergeBitRes i b₂ p₂ ↔ b₁ ≠ b₂ ∨ p₁ ≠ p₂
Tactic:
rw [ne_eq, mergeBitRes_inj_iff, not_and_or]
Proof state after:
no goals
Theorem: getRes_getBit_inj
Proof state before:
m : ℕ
q₁ q₂ : BV (m + 1)
i : Fin (m + 1)
h₁ : getBit i q₁ = getBit i q₂
h₂ : getRes i q₁ = getRes i q₂
⊢ q₁ = q₂
Tactic:
rw [← mergeBitRes_getBit_getRes (i := i) (q := q₁), h₁, h₂, mergeBitRes_getBit_getRes]
Proof state after:
no goals
Theorem: getRes_getBit_inj_iff
Proof state before:
m : ℕ
q₁ q₂ : BV (m + 1)
i : Fin (m + 1)
⊢ q₁ = q₂ → getBit i q₁ = getBit i q₂ ∧ getRes i q₁ = getRes i q₂
Tactic:
rintro rfl
Proof state after:
m : ℕ
q₁ : BV (m + 1)
i : Fin (m + 1)
⊢ getBit i q₁ = getBit i q₁ ∧ getRes i q₁ = getRes i q₁
Theorem: getRes_getBit_inj_iff
Proof state before:
m : ℕ
q₁ : BV (m + 1)
i : Fin (m + 1)
⊢ getBit i q₁ = getBit i q₁ ∧ getRes i q₁ = getRes i q₁
Tactic:
exact ⟨rfl, rfl⟩
Proof state after:
no goals
Theorem: eq_mergeBitRes_iff
Proof state before:
a✝ : ℕ
q : BV (a✝ + 1)
i : Fin (a✝ + 1)
b : Bool
p : BV a✝
⊢ q = mergeBitRes i b p ↔ getBit i q = b ∧ getRes i q = p
Tactic:
rw [← mergeBitRes_eq_iff, eq_comm]
Proof state after:
no goals
Theorem: mergeBitRes_ne_iff
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
b : Bool
p : BV a✝
q : BV (a✝ + 1)
⊢ mergeBitRes i b p ≠ q ↔ getBit i q ≠ b ∨ getRes i q ≠ p
Tactic:
simp_rw [ne_eq, mergeBitRes_eq_iff, Decidable.not_and_iff_or_not]
Proof state after:
no goals
Theorem: ne_mergeBitRes_iff
Proof state before:
a✝ : ℕ
q : BV (a✝ + 1)
i : Fin (a✝ + 1)
b : Bool
p : BV a✝
⊢ q ≠ mergeBitRes i b p ↔ getBit i q ≠ b ∨ getRes i q ≠ p
Tactic:
rw [← mergeBitRes_ne_iff, ne_comm]
Proof state after:
no goals
Theorem: mergeBitRes_getRes_of_getBit_eq
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) = q
Tactic:
simp_rw [← h, mergeBitRes_getBit_getRes]
Proof state after:
no goals
Theorem: mergeBitRes_getRes_cases
Proof state before:
m : ℕ
i : Fin (m + 1)
q : BV (m + 1)
⊢ getBit i q = false ∧ mergeBitRes i false (getRes i q) = q ∨ getBit i q = true ∧ mergeBitRes i true (getRes i q) = q
Tactic:
rcases (getBit i q).dichotomy with (h | h) <;>
simp_rw [h, mergeBitRes_getRes_of_getBit_eq h, false_and, and_self]
Proof state after:
case inl
m : ℕ
i : Fin (m + 1)
q : BV (m + 1)
h : getBit i q = false
⊢ True ∨ False

case inr
m : ℕ
i : Fin (m + 1)
q : BV (m + 1)
h : getBit i q = true
⊢ False ∨ True
Theorem: mergeBitRes_getRes_cases
Proof state before:
case inl
m : ℕ
i : Fin (m + 1)
q : BV (m + 1)
h : getBit i q = false
⊢ True ∨ False
Tactic:
simp_rw [or_false]
Proof state after:
no goals
Theorem: mergeBitRes_getRes_cases
Proof state before:
case inr
m : ℕ
i : Fin (m + 1)
q : BV (m + 1)
h : getBit i q = true
⊢ False ∨ True
Tactic:
simp_rw [or_true]
Proof state after:
no goals
Theorem: mergeBitRes_getBit_of_getRes_eq
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
q : BV (a✝ + 1)
p : BV a✝
h : getRes i q = p
⊢ mergeBitRes i (getBit i q) p = q
Tactic:
simp_rw [← h, mergeBitRes_getBit_getRes]
Proof state after:
no goals
Theorem: mergeBitRes_inv
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
q : BV (a✝ + 1)
b : Bool
p : BV a✝
h₁ : getBit i q = b
h₂ : getRes i q = p
⊢ mergeBitRes i b p = q
Tactic:
simp_rw [← h₁, ← h₂, mergeBitRes_getBit_getRes]
Proof state after:
no goals
Theorem: getRes_inv
Proof state before:
m : ℕ
q : BV (m + 1)
p : BV m
i : Fin (m + 1)
h : mergeBitRes i (getBit i q) p = q
⊢ getRes i q = p
Tactic:
rcases mergeBitRes_surj i q with ⟨b, p', rfl⟩
Proof state after:
case intro.intro
m : ℕ
p : BV m
i : Fin (m + 1)
b : Bool
p' : BV m
h : mergeBitRes i (getBit i (mergeBitRes i b p')) p = mergeBitRes i b p'
⊢ getRes i (mergeBitRes i b p') = p
Theorem: getRes_inv
Proof state before:
case intro.intro
m : ℕ
p : BV m
i : Fin (m + 1)
b : Bool
p' : BV m
h : mergeBitRes i (getBit i (mergeBitRes i b p')) p = mergeBitRes i b p'
⊢ getRes i (mergeBitRes i b p') = p
Tactic:
rw [getRes_mergeBitRes]
Proof state after:
case intro.intro
m : ℕ
p : BV m
i : Fin (m + 1)
b : Bool
p' : BV m
h : mergeBitRes i (getBit i (mergeBitRes i b p')) p = mergeBitRes i b p'
⊢ p' = p
Theorem: getRes_inv
Proof state before:
case intro.intro
m : ℕ
p : BV m
i : Fin (m + 1)
b : Bool
p' : BV m
h : mergeBitRes i (getBit i (mergeBitRes i b p')) p = mergeBitRes i b p'
⊢ p' = p
Tactic:
exact (mergeBitRes_Fin_inj i h).symm
Proof state after:
no goals
Theorem: getBit_inv
Proof state before:
m : ℕ
b : Bool
q : BV (m + 1)
i : Fin (m + 1)
h : mergeBitRes i b (getRes i q) = q
⊢ getBit i q = b
Tactic:
rcases mergeBitRes_surj i q with ⟨b', p', rfl⟩
Proof state after:
case intro.intro
m : ℕ
b : Bool
i : Fin (m + 1)
b' : Bool
p' : BV m
h : mergeBitRes i b (getRes i (mergeBitRes i b' p')) = mergeBitRes i b' p'
⊢ getBit i (mergeBitRes i b' p') = b
Theorem: getBit_inv
Proof state before:
case intro.intro
m : ℕ
b : Bool
i : Fin (m + 1)
b' : Bool
p' : BV m
h : mergeBitRes i b (getRes i (mergeBitRes i b' p')) = mergeBitRes i b' p'
⊢ getBit i (mergeBitRes i b' p') = b
Tactic:
rw [getBit_mergeBitRes]
Proof state after:
case intro.intro
m : ℕ
b : Bool
i : Fin (m + 1)
b' : Bool
p' : BV m
h : mergeBitRes i b (getRes i (mergeBitRes i b' p')) = mergeBitRes i b' p'
⊢ b' = b
Theorem: getBit_inv
Proof state before:
case intro.intro
m : ℕ
b : Bool
i : Fin (m + 1)
b' : Bool
p' : BV m
h : mergeBitRes i b (getRes i (mergeBitRes i b' p')) = mergeBitRes i b' p'
⊢ b' = b
Tactic:
exact (mergeBitRes_Bool_inj i h).symm
Proof state after:
no goals
Theorem: forall_iff_forall_mergeBitRes
Proof state before:
m : ℕ
i : Fin (m + 1)
pr : BV (m + 1) → Prop
h : ∀ (b : Bool) (p : BV m), pr (mergeBitRes i b p)
q : BV (m + 1)
⊢ pr q
Tactic:
rcases mergeBitRes_surj i q with ⟨b, p, rfl⟩
Proof state after:
case intro.intro
m : ℕ
i : Fin (m + 1)
pr : BV (m + 1) → Prop
h : ∀ (b : Bool) (p : BV m), pr (mergeBitRes i b p)
b : Bool
p : BV m
⊢ pr (mergeBitRes i b p)
Theorem: forall_iff_forall_mergeBitRes
Proof state before:
case intro.intro
m : ℕ
i : Fin (m + 1)
pr : BV (m + 1) → Prop
h : ∀ (b : Bool) (p : BV m), pr (mergeBitRes i b p)
b : Bool
p : BV m
⊢ pr (mergeBitRes i b p)
Tactic:
exact h _ _
Proof state after:
no goals
Theorem: forall_iff_forall_mergeBitRes_bool
Proof state before:
m : ℕ
i : Fin (m + 1)
pr : BV (m + 1) → Prop
h : (∀ (p : BV m), pr (mergeBitRes i false p)) ∧ ∀ (p : BV m), pr (mergeBitRes i true p)
q : BV (m + 1)
⊢ pr q
Tactic:
rcases mergeBitRes_surj i q with ⟨(h|h), p, rfl⟩
Proof state after:
case intro.false.intro
m : ℕ
i : Fin (m + 1)
pr : BV (m + 1) → Prop
h : (∀ (p : BV m), pr (mergeBitRes i false p)) ∧ ∀ (p : BV m), pr (mergeBitRes i true p)
p : BV m
⊢ pr (mergeBitRes i false p)

case intro.true.intro
m : ℕ
i : Fin (m + 1)
pr : BV (m + 1) → Prop
h : (∀ (p : BV m), pr (mergeBitRes i false p)) ∧ ∀ (p : BV m), pr (mergeBitRes i true p)
p : BV m
⊢ pr (mergeBitRes i true p)
Theorem: forall_iff_forall_mergeBitRes_bool
Proof state before:
case intro.false.intro
m : ℕ
i : Fin (m + 1)
pr : BV (m + 1) → Prop
h : (∀ (p : BV m), pr (mergeBitRes i false p)) ∧ ∀ (p : BV m), pr (mergeBitRes i true p)
p : BV m
⊢ pr (mergeBitRes i false p)
Tactic:
exact h.1 _
Proof state after:
no goals
Theorem: forall_iff_forall_mergeBitRes_bool
Proof state before:
case intro.true.intro
m : ℕ
i : Fin (m + 1)
pr : BV (m + 1) → Prop
h : (∀ (p : BV m), pr (mergeBitRes i false p)) ∧ ∀ (p : BV m), pr (mergeBitRes i true p)
p : BV m
⊢ pr (mergeBitRes i true p)
Tactic:
exact h.2 _
Proof state after:
no goals
Theorem: ne_iff_getBit_ne_or_getRes_ne
Proof state before:
m : ℕ
q₁ q₂ : BV (m + 1)
i : Fin (m + 1)
⊢ q₁ ≠ q₂ ↔ getBit i q₁ ≠ getBit i q₂ ∨ getRes i q₁ ≠ getRes i q₂
Tactic:
rw [ne_eq q₁, getRes_getBit_inj_iff i, not_and_or]
Proof state after:
no goals
Theorem: getBit_ext_iff
Proof state before:
m : ℕ
q q' : BV (m + 1)
⊢ q = q' ↔ ∀ (i : Fin (m + 1)), getBit i q = getBit i q'
Tactic:
refine' ⟨fun h _ => h ▸ rfl, fun h => _⟩
Proof state after:
m : ℕ
q q' : BV (m + 1)
h : ∀ (i : Fin (m + 1)), getBit i q = getBit i q'
⊢ q = q'
Theorem: getBit_ext_iff
Proof state before:
m : ℕ
q q' : BV (m + 1)
h : ∀ (i : Fin (m + 1)), getBit i q = getBit i q'
⊢ q = q'
Tactic:
induction' m with m IH
Proof state after:
case zero
q q' : BV (0 + 1)
h : ∀ (i : Fin (0 + 1)), getBit i q = getBit i q'
⊢ q = q'

case succ
m : ℕ
IH : ∀ {q q' : BV (m + 1)}, (∀ (i : Fin (m + 1)), getBit i q = getBit i q') → q = q'
q q' : BV (m + 1 + 1)
h : ∀ (i : Fin (m + 1 + 1)), getBit i q = getBit i q'
⊢ q = q'
Theorem: getBit_ext_iff
Proof state before:
case zero
q q' : BV (0 + 1)
h : ∀ (i : Fin (0 + 1)), getBit i q = getBit i q'
⊢ q = q'
Tactic:
simp_rw [getRes_getBit_inj_iff 0, Fin.eq_zero, and_true, h]
Proof state after:
no goals
Theorem: getBit_ext_iff
Proof state before:
case succ
m : ℕ
IH : ∀ {q q' : BV (m + 1)}, (∀ (i : Fin (m + 1)), getBit i q = getBit i q') → q = q'
q q' : BV (m + 1 + 1)
h : ∀ (i : Fin (m + 1 + 1)), getBit i q = getBit i q'
⊢ q = q'
Tactic:
simp_rw [Fin.forall_fin_succ (P := fun i => getBit i q = getBit i q'), getBit_succ] at h
Proof state after:
case succ
m : ℕ
IH : ∀ {q q' : BV (m + 1)}, (∀ (i : Fin (m + 1)), getBit i q = getBit i q') → q = q'
q q' : BV (m + 1 + 1)
h : getBit 0 q = getBit 0 q' ∧ ∀ (i : Fin (m + 1)), getBit i (getRes 0 q) = getBit i (getRes 0 q')
⊢ q = q'
Theorem: getBit_ext_iff
Proof state before:
case succ
m : ℕ
IH : ∀ {q q' : BV (m + 1)}, (∀ (i : Fin (m + 1)), getBit i q = getBit i q') → q = q'
q q' : BV (m + 1 + 1)
h : getBit 0 q = getBit 0 q' ∧ ∀ (i : Fin (m + 1)), getBit i (getRes 0 q) = getBit i (getRes 0 q')
⊢ q = q'
Tactic:
exact (getRes_getBit_inj_iff 0).mpr ⟨h.1, IH h.2⟩
Proof state after:
no goals
Theorem: bitInvar_comp_of_bitInvar
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
f g : Function.End (BV (a✝ + 1))
hf : bitInvar i f
hg : bitInvar i g
q : BV (a✝ + 1)
⊢ getBit i ((f ∘ g) q) = getBit i q
Tactic:
simp_rw [Function.comp_apply, hf (g q), hg q]
Proof state after:
no goals
Theorem: bitInvar_of_comp_bitInvar_bitInvar
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
f g : BV (a✝ + 1) → BV (a✝ + 1)
hfg : bitInvar i (f ∘ g)
h : bitInvar i f
q : BV (a✝ + 1)
⊢ getBit i (g q) = getBit i q
Tactic:
rw [← h (g q), ← hfg q, Function.comp_apply]
Proof state after:
no goals
Theorem: mergeBitRes_getBit_getRes_apply_eq_apply_of_bitinvar
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
f : Function.End (BV (a✝ + 1))
q : BV (a✝ + 1)
h : bitInvar i f
⊢ mergeBitRes i (getBit i q) (getRes i (f q)) = f q
Tactic:
rw [← h q, mergeBitRes_getBit_getRes]
Proof state after:
no goals
Theorem: mergeBitRes_getRes_apply_mergeBitRes_of_bitinvar
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
f : Function.End (BV (a✝ + 1))
b : Bool
p : BV a✝
h : bitInvar i f
⊢ mergeBitRes i b (getRes i (f (mergeBitRes i b p))) = f (mergeBitRes i b p)
Tactic:
convert (getBit_mergeBitRes ▸ mergeBitRes_getBit_getRes_apply_eq_apply_of_bitinvar h)
Proof state after:
no goals
Theorem: endoOfBoolArrowEndo_bitInvar
Proof state before:
m : ℕ
i : Fin (m + 1)
f : Bool → Function.End (BV m)
⊢ bitInvar i (endoOfBoolArrowEndo i f)
Tactic:
simp_rw [bitInvar_iff_getBit_apply_eq_getBit, endoOfBoolArrowEndo_def,
  getBit_mergeBitRes, implies_true]
Proof state after:
no goals
Theorem: endoOfBoolArrowEndo_comp
Proof state before:
m : ℕ
i : Fin (m + 1)
f g : Bool → Function.End (BV m)
⊢ (endoOfBoolArrowEndo i fun b => f b ∘ g b) = endoOfBoolArrowEndo i f ∘ endoOfBoolArrowEndo i g
Tactic:
simp_rw [Function.End.ext_iff, Function.comp_apply, endoOfBoolArrowEndo_def,  getBit_mergeBitRes,
getRes_mergeBitRes, Function.comp_apply, implies_true]
Proof state after:
no goals
Theorem: endoOfBoolArrowEndo_rightInverse
Proof state before:
m : ℕ
i : Fin (m + 1)
f : Bool → Function.End (BV m)
⊢ boolArrowEndoOfEndo i (endoOfBoolArrowEndo i f) = f
Tactic:
ext
Proof state after:
case h.H.h
m : ℕ
i : Fin (m + 1)
f : Bool → Function.End (BV m)
x✝¹ : Bool
x✝ : BV m
⊢ ↑(boolArrowEndoOfEndo i (endoOfBoolArrowEndo i f) x✝¹ x✝) = ↑(f x✝¹ x✝)
Theorem: endoOfBoolArrowEndo_rightInverse
Proof state before:
case h.H.h
m : ℕ
i : Fin (m + 1)
f : Bool → Function.End (BV m)
x✝¹ : Bool
x✝ : BV m
⊢ ↑(boolArrowEndoOfEndo i (endoOfBoolArrowEndo i f) x✝¹ x✝) = ↑(f x✝¹ x✝)
Tactic:
simp_rw [boolArrowEndoOfEndo_def, endoOfBoolArrowEndo_def, getBit_mergeBitRes,
getRes_mergeBitRes]
Proof state after:
no goals
Theorem: endoOfBoolArrowEndo_leftInvOn
Proof state before:
m : ℕ
i : Fin (m + 1)
f : Function.End (BV (m + 1))
hf : f ∈ bitInvar i
⊢ endoOfBoolArrowEndo i (boolArrowEndoOfEndo i f) = f
Tactic:
ext q
Proof state after:
case H.h
m : ℕ
i : Fin (m + 1)
f : Function.End (BV (m + 1))
hf : f ∈ bitInvar i
q : BV (m + 1)
⊢ ↑(endoOfBoolArrowEndo i (boolArrowEndoOfEndo i f) q) = ↑(f q)
Theorem: endoOfBoolArrowEndo_leftInvOn
Proof state before:
case H.h
m : ℕ
i : Fin (m + 1)
f : Function.End (BV (m + 1))
hf : f ∈ bitInvar i
q : BV (m + 1)
⊢ ↑(endoOfBoolArrowEndo i (boolArrowEndoOfEndo i f) q) = ↑(f q)
Tactic:
simp_rw [endoOfBoolArrowEndo_def, boolArrowEndoOfEndo_def, mergeBitRes_getBit_getRes,
mergeBitRes_getRes_of_getBit_eq (hf q)]
Proof state after:
no goals
Theorem: endoOfBoolArrowEndo_leftInverse_apply
Proof state before:
m : ℕ
i : Fin (m + 1)
f g : Bool → Function.End (BV m)
hfg : ∀ (b : Bool), Function.LeftInverse (f b) (g b)
q : BV (m + 1)
⊢ endoOfBoolArrowEndo i f (endoOfBoolArrowEndo i g q) = q
Tactic:
simp_rw [endoOfBoolArrowEndo_def, getBit_mergeBitRes, getRes_mergeBitRes,
  hfg (getBit i q) (getRes i q), mergeBitRes_getBit_getRes]
Proof state after:
no goals
Theorem: boolArrowEndoOfEndo_leftInverse_apply_ofBitInvarLeft
Proof state before:
m : ℕ
i : Fin (m + 1)
f g : Function.End (BV (m + 1))
hfg : Function.LeftInverse f g
hf : bitInvar i f
b : Bool
q : BV m
⊢ boolArrowEndoOfEndo i f b (boolArrowEndoOfEndo i g b q) = q
Tactic:
simp_rw [boolArrowEndoOfEndo_def,
mergeBitRes_getRes_apply_mergeBitRes_of_bitinvar (bitInvar_of_leftInverse_bitInvar hfg hf),
hfg (mergeBitRes i b q), getRes_mergeBitRes]
Proof state after:
no goals
Theorem: boolArrowEndoOfEndo_rightInverse_apply_ofBitInvarLeft
Proof state before:
m : ℕ
i : Fin (m + 1)
f g : Function.End (BV (m + 1))
hfg : Function.RightInverse f g
hf : bitInvar i f
b : Bool
q : BV m
⊢ boolArrowEndoOfEndo i g b (boolArrowEndoOfEndo i f b q) = q
Tactic:
simp_rw [boolArrowEndoOfEndo_def, mergeBitRes_getRes_apply_mergeBitRes_of_bitinvar hf,
hfg (mergeBitRes i b q), getRes_mergeBitRes]
Proof state after:
no goals
Theorem: boolArrowEndoOfEndo_comp_ofBitInvarRight
Proof state before:
m : ℕ
i : Fin (m + 1)
f g : Function.End (BV (m + 1))
hg : bitInvar i g
b : Bool
⊢ boolArrowEndoOfEndo i (f ∘ g) b = boolArrowEndoOfEndo i f b ∘ boolArrowEndoOfEndo i g b
Tactic:
ext
Proof state after:
case H.h
m : ℕ
i : Fin (m + 1)
f g : Function.End (BV (m + 1))
hg : bitInvar i g
b : Bool
x✝ : BV m
⊢ ↑(boolArrowEndoOfEndo i (f ∘ g) b x✝) = ↑((boolArrowEndoOfEndo i f b ∘ boolArrowEndoOfEndo i g b) x✝)
Theorem: boolArrowEndoOfEndo_comp_ofBitInvarRight
Proof state before:
case H.h
m : ℕ
i : Fin (m + 1)
f g : Function.End (BV (m + 1))
hg : bitInvar i g
b : Bool
x✝ : BV m
⊢ ↑(boolArrowEndoOfEndo i (f ∘ g) b x✝) = ↑((boolArrowEndoOfEndo i f b ∘ boolArrowEndoOfEndo i g b) x✝)
Tactic:
simp_rw [boolArrowEndoOfEndo_def, Function.comp_apply, boolArrowEndoOfEndo_def,
mergeBitRes_getRes_apply_mergeBitRes_of_bitinvar hg]
Proof state after:
no goals
Theorem: boolArrowEndoOfEndo_mul_ofBitInvarRight
Proof state before:
m : ℕ
i : Fin (m + 1)
f g : Function.End (BV (m + 1))
hg : bitInvar i g
⊢ boolArrowEndoOfEndo i (f * g) = boolArrowEndoOfEndo i f * boolArrowEndoOfEndo i g
Tactic:
ext : 1
Proof state after:
case h
m : ℕ
i : Fin (m + 1)
f g : Function.End (BV (m + 1))
hg : bitInvar i g
x✝ : Bool
⊢ boolArrowEndoOfEndo i (f * g) x✝ = (boolArrowEndoOfEndo i f * boolArrowEndoOfEndo i g) x✝
Theorem: boolArrowEndoOfEndo_mul_ofBitInvarRight
Proof state before:
case h
m : ℕ
i : Fin (m + 1)
f g : Function.End (BV (m + 1))
hg : bitInvar i g
x✝ : Bool
⊢ boolArrowEndoOfEndo i (f * g) x✝ = (boolArrowEndoOfEndo i f * boolArrowEndoOfEndo i g) x✝
Tactic:
exact boolArrowEndoOfEndo_comp_ofBitInvarRight hg
Proof state after:
no goals
Theorem: flipBit_base
Proof state before:
i : Fin (0 + 1)
⊢ flipBit i = Equiv.swap 0 1
Tactic:
simp_rw [Equiv.ext_iff, flipBit_apply, Fin.eq_zero i]
Proof state after:
i : Fin (0 + 1)
⊢ ∀ (x : BV (0 + 1)), mergeBitRes 0 (!getBit 0 x) (getRes 0 x) = (Equiv.swap 0 1) x
Theorem: flipBit_base
Proof state before:
i : Fin (0 + 1)
⊢ ∀ (x : BV (0 + 1)), mergeBitRes 0 (!getBit 0 x) (getRes 0 x) = (Equiv.swap 0 1) x
Tactic:
exact Fin.forall_fin_two.mpr ⟨rfl, rfl⟩
Proof state after:
no goals
Theorem: flipBit_zero_apply
Proof state before:
a✝ : ℕ
q : BV (a✝ + 1)
⊢ (flipBit 0) q = finProdFinEquiv (q.divNat, q.modNat.rev)
Tactic:
simp_rw [flipBit_apply, getBit_zero, Nat.pow_eq, finTwoEquiv_apply,
  getRes_zero, mergeBitRes_zero, Bool.cond_not, Bool.cond_decide]
Proof state after:
a✝ : ℕ
q : BV (a✝ + 1)
⊢ finProdFinEquiv (q.divNat, if q.modNat = 1 then 0 else 1) = finProdFinEquiv (q.divNat, q.modNat.rev)
Theorem: flipBit_zero_apply
Proof state before:
a✝ : ℕ
q : BV (a✝ + 1)
⊢ finProdFinEquiv (q.divNat, if q.modNat = 1 then 0 else 1) = finProdFinEquiv (q.divNat, q.modNat.rev)
Tactic:
rcases Fin.modNat_two_eq_zero_or_one q with (h | h) <;> simp_rw [h] <;> rfl
Proof state after:
no goals
Theorem: flipBit_mergeBitRes
Proof state before:
a✝ : ℕ
i : Fin (a✝ + 1)
b : Bool
p : BV a✝
⊢ (flipBit i) (mergeBitRes i b p) = mergeBitRes i (!b) p
Tactic:
rw [flipBit_apply, getBit_mergeBitRes, getRes_mergeBitRes]
Proof state after:
no goals