internlm/Lean-Github huggingface dataset:
Theorem: FinInt.eq_of_toUint_eq
Proof state before:
case true.false
sz : ℕ
a' : FinInt sz
ih : ∀ (a b : FinInt (Nat.add sz 0)), toUint a = toUint b → a = b
b' : FinInt sz
h : 2 ^ sz + toUint a' = toUint b'
⊢ False

case true.true
sz : ℕ
a' : FinInt sz
ih : ∀ (a b : FinInt (Nat.add sz 0)), toUint a = toUint b → a = b
b' : FinInt sz
h : toUint a' = toUint b'
⊢ a' = b'
Tactic:
. have h₁ := @toUint_ge _ a'; have h₂ := @toUint_lt _ b'; sorry_arith
Proof state after:
case true.true
sz : ℕ
a' : FinInt sz
ih : ∀ (a b : FinInt (Nat.add sz 0)), toUint a = toUint b → a = b
b' : FinInt sz
h : toUint a' = toUint b'
⊢ a' = b'
Theorem: FinInt.eq_of_toUint_eq
Proof state before:
case true.true
sz : ℕ
a' : FinInt sz
ih : ∀ (a b : FinInt (Nat.add sz 0)), toUint a = toUint b → a = b
b' : FinInt sz
h : toUint a' = toUint b'
⊢ a' = b'
Tactic:
. apply ih; sorry_arith
Proof state after:
no goals
Theorem: FinInt.eq_of_toUint_cong2
Proof state before:
n : ℕ
a b : FinInt n
⊢ toUint a ≡ toUint b [2^n] → a = b
Tactic:
intros h
Proof state after:
n : ℕ
a b : FinInt n
h : toUint a ≡ toUint b [2^n]
⊢ a = b
Theorem: FinInt.eq_of_toUint_cong2
Proof state before:
n : ℕ
a b : FinInt n
h : toUint a ≡ toUint b [2^n]
⊢ a = b
Tactic:
apply eq_of_toUint_eq
Proof state after:
case a
n : ℕ
a b : FinInt n
h : toUint a ≡ toUint b [2^n]
⊢ toUint a = toUint b
Theorem: FinInt.eq_of_toUint_cong2
Proof state before:
case a
n : ℕ
a b : FinInt n
h : toUint a ≡ toUint b [2^n]
⊢ toUint a = toUint b
Tactic:
apply cong2_to_eq n h toUint_bounds toUint_bounds
Proof state after:
no goals
Theorem: FinInt.comp_toUint
Proof state before:
sz : ℕ
n : FinInt sz
⊢ toUint (comp n) = 2 ^ sz - 1 - toUint n
Tactic:
induction sz
Proof state after:
case zero
n : FinInt Nat.zero
⊢ toUint (comp n) = 2 ^ Nat.zero - 1 - toUint n

case succ
n✝ : ℕ
n_ih✝ : ∀ (n : FinInt n✝), toUint (comp n) = 2 ^ n✝ - 1 - toUint n
n : FinInt (Nat.succ n✝)
⊢ toUint (comp n) = 2 ^ Nat.succ n✝ - 1 - toUint n
Theorem: FinInt.comp_toUint
Proof state before:
n : FinInt Nat.zero
⊢ toUint (comp n) = 2 ^ Nat.zero - 1 - toUint n
Tactic:
case zero =>
  cases n; simp
Proof state after:
no goals
Theorem: FinInt.comp_toUint
Proof state before:
sz : ℕ
ih : ∀ (n : FinInt sz), toUint (comp n) = 2 ^ sz - 1 - toUint n
n : FinInt (Nat.succ sz)
⊢ toUint (comp n) = 2 ^ Nat.succ sz - 1 - toUint n
Tactic:
case succ sz ih =>
  simp [comp] at ih
  cases n; case next sz bn n' =>
  cases bn <;> simp [ih]
  . sorry_arith
  . sorry_arith
Proof state after:
no goals
Theorem: FinInt.comp_toUint
Proof state before:
n : FinInt Nat.zero
⊢ toUint (comp n) = 2 ^ Nat.zero - 1 - toUint n
Tactic:
cases n
Proof state after:
case nil

⊢ toUint (comp nil) = 2 ^ Nat.zero - 1 - toUint nil
Theorem: FinInt.comp_toUint
Proof state before:
case nil

⊢ toUint (comp nil) = 2 ^ Nat.zero - 1 - toUint nil
Tactic:
simp
Proof state after:
no goals
Theorem: FinInt.comp_toUint
Proof state before:
sz : ℕ
ih : ∀ (n : FinInt sz), toUint (comp n) = 2 ^ sz - 1 - toUint n
n : FinInt (Nat.succ sz)
⊢ toUint (comp n) = 2 ^ Nat.succ sz - 1 - toUint n
Tactic:
simp [comp] at ih
Proof state after:
sz : ℕ
ih : ∀ (n : FinInt sz), toUint (logic1 (fun x => !x) n) = 2 ^ sz - 1 - toUint n
n : FinInt (Nat.succ sz)
⊢ toUint (comp n) = 2 ^ Nat.succ sz - 1 - toUint n
Theorem: FinInt.comp_toUint
Proof state before:
sz : ℕ
ih : ∀ (n : FinInt sz), toUint (logic1 (fun x => !x) n) = 2 ^ sz - 1 - toUint n
n : FinInt (Nat.succ sz)
⊢ toUint (comp n) = 2 ^ Nat.succ sz - 1 - toUint n
Tactic:
cases n
Proof state after:
case next
n✝ : ℕ
a✝¹ : Bool
a✝ : FinInt n✝
ih : ∀ (n : FinInt (Nat.add n✝ 0)), toUint (logic1 (fun x => !x) n) = 2 ^ Nat.add n✝ 0 - 1 - toUint n
⊢ toUint (comp (next a✝¹ a✝)) = 2 ^ Nat.succ (Nat.add n✝ 0) - 1 - toUint (next a✝¹ a✝)
Theorem: FinInt.comp_toUint
Proof state before:
sz : ℕ
bn : Bool
n' : FinInt sz
ih : ∀ (n : FinInt (Nat.add sz 0)), toUint (logic1 (fun x => !x) n) = 2 ^ Nat.add sz 0 - 1 - toUint n
⊢ toUint (comp (next bn n')) = 2 ^ Nat.succ (Nat.add sz 0) - 1 - toUint (next bn n')
Tactic:
case next sz bn n' =>
cases bn <;> simp [ih]
. sorry_arith
. sorry_arith
Proof state after:
no goals
Theorem: FinInt.comp_toUint
Proof state before:
sz : ℕ
bn : Bool
n' : FinInt sz
ih : ∀ (n : FinInt (Nat.add sz 0)), toUint (logic1 (fun x => !x) n) = 2 ^ Nat.add sz 0 - 1 - toUint n
⊢ toUint (comp (next bn n')) = 2 ^ Nat.succ (Nat.add sz 0) - 1 - toUint (next bn n')
Tactic:
cases bn <;> simp [ih]
Proof state after:
case false
sz : ℕ
n' : FinInt sz
ih : ∀ (n : FinInt (Nat.add sz 0)), toUint (logic1 (fun x => !x) n) = 2 ^ Nat.add sz 0 - 1 - toUint n
⊢ 2 ^ sz + (2 ^ sz - 1 - toUint n') = 2 ^ Nat.succ sz - 1 - toUint n'

case true
sz : ℕ
n' : FinInt sz
ih : ∀ (n : FinInt (Nat.add sz 0)), toUint (logic1 (fun x => !x) n) = 2 ^ Nat.add sz 0 - 1 - toUint n
⊢ 2 ^ sz - 1 - toUint n' = 2 ^ Nat.succ sz - 1 - (2 ^ sz + toUint n')
Theorem: FinInt.comp_toUint
Proof state before:
case false
sz : ℕ
n' : FinInt sz
ih : ∀ (n : FinInt (Nat.add sz 0)), toUint (logic1 (fun x => !x) n) = 2 ^ Nat.add sz 0 - 1 - toUint n
⊢ 2 ^ sz + (2 ^ sz - 1 - toUint n') = 2 ^ Nat.succ sz - 1 - toUint n'

case true
sz : ℕ
n' : FinInt sz
ih : ∀ (n : FinInt (Nat.add sz 0)), toUint (logic1 (fun x => !x) n) = 2 ^ Nat.add sz 0 - 1 - toUint n
⊢ 2 ^ sz - 1 - toUint n' = 2 ^ Nat.succ sz - 1 - (2 ^ sz + toUint n')
Tactic:
. sorry_arith
Proof state after:
case true
sz : ℕ
n' : FinInt sz
ih : ∀ (n : FinInt (Nat.add sz 0)), toUint (logic1 (fun x => !x) n) = 2 ^ Nat.add sz 0 - 1 - toUint n
⊢ 2 ^ sz - 1 - toUint n' = 2 ^ Nat.succ sz - 1 - (2 ^ sz + toUint n')
Theorem: FinInt.comp_toUint
Proof state before:
case true
sz : ℕ
n' : FinInt sz
ih : ∀ (n : FinInt (Nat.add sz 0)), toUint (logic1 (fun x => !x) n) = 2 ^ Nat.add sz 0 - 1 - toUint n
⊢ 2 ^ sz - 1 - toUint n' = 2 ^ Nat.succ sz - 1 - (2 ^ sz + toUint n')
Tactic:
. sorry_arith
Proof state after:
no goals
Theorem: FinInt.addfull_toUint
Proof state before:
sz : ℕ
n m : FinInt sz
⊢ toUint (addfull n m) = toUint n + toUint m
Tactic:
revert n m
Proof state after:
sz : ℕ
⊢ ∀ (n m : FinInt sz), toUint (addfull n m) = toUint n + toUint m
Theorem: FinInt.addfull_toUint
Proof state before:
sz : ℕ
⊢ ∀ (n m : FinInt sz), toUint (addfull n m) = toUint n + toUint m
Tactic:
induction sz <;> intros n m
Proof state after:
case zero
n m : FinInt Nat.zero
⊢ toUint (addfull n m) = toUint n + toUint m

case succ
n✝ : ℕ
n_ih✝ : ∀ (n m : FinInt n✝), toUint (addfull n m) = toUint n + toUint m
n m : FinInt (Nat.succ n✝)
⊢ toUint (addfull n m) = toUint n + toUint m
Theorem: FinInt.addfull_toUint
Proof state before:
n m : FinInt Nat.zero
⊢ toUint (addfull n m) = toUint n + toUint m
Tactic:
case zero =>
  cases n; cases m; simp [addfull]
Proof state after:
no goals
Theorem: FinInt.addfull_toUint
Proof state before:
sz : ℕ
ih : ∀ (n m : FinInt sz), toUint (addfull n m) = toUint n + toUint m
n m : FinInt (Nat.succ sz)
⊢ toUint (addfull n m) = toUint n + toUint m
Tactic:
case succ sz ih =>
  cases n; case next sz dn n' =>
  cases m; case next dm m' =>
  simp [addfull]
  split
  case h_1 r h =>
    have h': r.toUint = n'.toUint + m'.toUint := by
      rw [←ih n' m']; simp [h]
    simp at h'
    cases dn <;> cases dm <;> simp [FinInt.toUint, h']
    <;> sorry_arith
  case h_2 r h =>
    have h': r.toUint = n'.toUint + m'.toUint - 2^sz := by
      rw [←ih n' m']
      simp [h, Int.add_comm, toSint]
    simp at h'
    cases dn <;> cases dm <;> simp [FinInt.toUint, h', toSint]
    <;> sorry_arith
Proof state after:
no goals
Theorem: FinInt.addfull_toUint
Proof state before:
n m : FinInt Nat.zero
⊢ toUint (addfull n m) = toUint n + toUint m
Tactic:
cases n
Proof state after:
case nil
m : FinInt Nat.zero
⊢ toUint (addfull nil m) = toUint nil + toUint m
Theorem: FinInt.addfull_toUint
Proof state before:
case nil
m : FinInt Nat.zero
⊢ toUint (addfull nil m) = toUint nil + toUint m
Tactic:
cases m
Proof state after:
case nil.nil

⊢ toUint (addfull nil nil) = toUint nil + toUint nil
Theorem: FinInt.addfull_toUint
Proof state before:
case nil.nil

⊢ toUint (addfull nil nil) = toUint nil + toUint nil
Tactic:
simp [addfull]
Proof state after:
no goals
Theorem: FinInt.addfull_toUint
Proof state before:
sz : ℕ
ih : ∀ (n m : FinInt sz), toUint (addfull n m) = toUint n + toUint m
n m : FinInt (Nat.succ sz)
⊢ toUint (addfull n m) = toUint n + toUint m
Tactic:
cases n
Proof state after:
case next
n✝ : ℕ
a✝¹ : Bool
a✝ : FinInt n✝
ih : ∀ (n m : FinInt (Nat.add n✝ 0)), toUint (addfull n m) = toUint n + toUint m
m : FinInt (Nat.succ (Nat.add n✝ 0))
⊢ toUint (addfull (next a✝¹ a✝) m) = toUint (next a✝¹ a✝) + toUint m
Theorem: FinInt.addfull_toUint
Proof state before:
sz : ℕ
dn : Bool
n' : FinInt sz
ih : ∀ (n m : FinInt (Nat.add sz 0)), toUint (addfull n m) = toUint n + toUint m
m : FinInt (Nat.succ (Nat.add sz 0))
⊢ toUint (addfull (next dn n') m) = toUint (next dn n') + toUint m
Tactic:
case next sz dn n' =>
cases m; case next dm m' =>
simp [addfull]
split
case h_1 r h =>
have h': r.toUint = n'.toUint + m'.toUint := by
rw [←ih n' m']; simp [h]
simp at h'
cases dn <;> cases dm <;> simp [FinInt.toUint, h']
<;> sorry_arith
case h_2 r h =>
have h': r.toUint = n'.toUint + m'.toUint - 2^sz := by
rw [←ih n' m']
simp [h, Int.add_comm, toSint]
simp at h'
cases dn <;> cases dm <;> simp [FinInt.toUint, h', toSint]
<;> sorry_arith
Proof state after:
no goals
Theorem: FinInt.addfull_toUint
Proof state before:
sz : ℕ
dn : Bool
n' : FinInt sz
ih : ∀ (n m : FinInt (Nat.add sz 0)), toUint (addfull n m) = toUint n + toUint m
m : FinInt (Nat.succ (Nat.add sz 0))
⊢ toUint (addfull (next dn n') m) = toUint (next dn n') + toUint m
Tactic:
cases m
Proof state after:
case next
sz : ℕ
dn : Bool
n' : FinInt sz
ih : ∀ (n m : FinInt (Nat.add sz 0)), toUint (addfull n m) = toUint n + toUint m
a✝¹ : Bool
a✝ : FinInt sz
⊢ toUint (addfull (next dn n') (next a✝¹ a✝)) = toUint (next dn n') + toUint (next a✝¹ a✝)
Theorem: FinInt.addfull_toUint
Proof state before:
sz : ℕ
dn : Bool
n' : FinInt sz
ih : ∀ (n m : FinInt (Nat.add sz 0)), toUint (addfull n m) = toUint n + toUint m
dm : Bool
m' : FinInt sz
⊢ toUint (addfull (next dn n') (next dm m')) = toUint (next dn n') + toUint (next dm m')
Tactic:
case next dm m' =>
simp [addfull]
split
case h_1 r h =>
have h': r.toUint = n'.toUint + m'.toUint := by
rw [←ih n' m']; simp [h]
simp at h'
cases dn <;> cases dm <;> simp [FinInt.toUint, h']
<;> sorry_arith
case h_2 r h =>
have h': r.toUint = n'.toUint + m'.toUint - 2^sz := by
rw [←ih n' m']
simp [h, Int.add_comm, toSint]
simp at h'
cases dn <;> cases dm <;> simp [FinInt.toUint, h', toSint]
<;> sorry_arith
Proof state after:
no goals
Theorem: FinInt.addfull_toUint
Proof state before:
sz : ℕ
dn : Bool
n' : FinInt sz
ih : ∀ (n m : FinInt (Nat.add sz 0)), toUint (addfull n m) = toUint n + toUint m
dm : Bool
m' : FinInt sz
⊢ toUint (addfull (next dn n') (next dm m')) = toUint (next dn n') + toUint (next dm m')
Tactic:
simp [addfull]
Proof state after:
sz : ℕ
dn : Bool
n' : FinInt sz
ih : ∀ (n m : FinInt (Nat.add sz 0)), toUint (addfull n m) = toUint n + toUint m
dm : Bool
m' : FinInt sz
⊢ toUint
      (match addfull n' m' with
      | next false r => next (dn && dm) (next (dn != dm) r)
      | next true r => next (dn || dm) (next (dn == dm) r)) =
    toUint (next dn n') + toUint (next dm m')
Theorem: FinInt.addfull_toUint
Proof state before:
sz : ℕ
dn : Bool
n' : FinInt sz
ih : ∀ (n m : FinInt (Nat.add sz 0)), toUint (addfull n m) = toUint n + toUint m
dm : Bool
m' : FinInt sz
⊢ toUint
      (match addfull n' m' with
      | next false r => next (dn && dm) (next (dn != dm) r)
      | next true r => next (dn || dm) (next (dn == dm) r)) =
    toUint (next dn n') + toUint (next dm m')
Tactic:
split
Proof state after:
case h_1
sz : ℕ
dn : Bool
n' : FinInt sz
ih : ∀ (n m : FinInt (Nat.add sz 0)), toUint (addfull n m) = toUint n + toUint m
dm : Bool
m' : FinInt sz
n✝ : FinInt (sz + 0 + 1)
m✝ : FinInt (sz + 0)
heq✝ : addfull n' m' = next false m✝
⊢ toUint (next (dn && dm) (next (dn != dm) m✝)) = toUint (next dn n') + toUint (next dm m')

case h_2
sz : ℕ
dn : Bool
n' : FinInt sz
ih : ∀ (n m : FinInt (Nat.add sz 0)), toUint (addfull n m) = toUint n + toUint m
dm : Bool
m' : FinInt sz
n✝ : FinInt (sz + 0 + 1)
m✝ : FinInt (sz + 0)
heq✝ : addfull n' m' = next true m✝
⊢ toUint (next (dn || dm) (next (dn == dm) m✝)) = toUint (next dn n') + toUint (next dm m')
Theorem: FinInt.addfull_toUint
Proof state before:
sz : ℕ
dn : Bool
n' : FinInt sz
ih : ∀ (n m : FinInt (Nat.add sz 0)), toUint (addfull n m) = toUint n + toUint m
dm : Bool
m' : FinInt sz
n✝ : FinInt (sz + 0 + 1)
r : FinInt (sz + 0)
h : addfull n' m' = next false r
⊢ toUint (next (dn && dm) (next (dn != dm) r)) = toUint (next dn n') + toUint (next dm m')
Tactic:
case h_1 r h =>
  have h': r.toUint = n'.toUint + m'.toUint := by
    rw [←ih n' m']; simp [h]
  simp at h'
  cases dn <;> cases dm <;> simp [FinInt.toUint, h']
  <;> sorry_arith
Proof state after:
no goals
Theorem: FinInt.addfull_toUint
Proof state before:
sz : ℕ
dn : Bool
n' : FinInt sz
ih : ∀ (n m : FinInt (Nat.add sz 0)), toUint (addfull n m) = toUint n + toUint m
dm : Bool
m' : FinInt sz
n✝ : FinInt (sz + 0 + 1)
r : FinInt (sz + 0)
h : addfull n' m' = next true r
⊢ toUint (next (dn || dm) (next (dn == dm) r)) = toUint (next dn n') + toUint (next dm m')
Tactic:
case h_2 r h =>
  have h': r.toUint = n'.toUint + m'.toUint - 2^sz := by
    rw [←ih n' m']
    simp [h, Int.add_comm, toSint]
  simp at h'
  cases dn <;> cases dm <;> simp [FinInt.toUint, h', toSint]
  <;> sorry_arith
Proof state after:
no goals
Theorem: FinInt.addfull_toUint
Proof state before:
sz : ℕ
dn : Bool
n' : FinInt sz
ih : ∀ (n m : FinInt (Nat.add sz 0)), toUint (addfull n m) = toUint n + toUint m
dm : Bool
m' : FinInt sz
n✝ : FinInt (sz + 0 + 1)
r : FinInt (sz + 0)
h : addfull n' m' = next false r
⊢ toUint (next (dn && dm) (next (dn != dm) r)) = toUint (next dn n') + toUint (next dm m')
Tactic:
have h': r.toUint = n'.toUint + m'.toUint := by
  rw [←ih n' m']; simp [h]
Proof state after:
sz : ℕ
dn : Bool
n' : FinInt sz
ih : ∀ (n m : FinInt (Nat.add sz 0)), toUint (addfull n m) = toUint n + toUint m
dm : Bool
m' : FinInt sz
n✝ : FinInt (sz + 0 + 1)
r : FinInt (sz + 0)
h : addfull n' m' = next false r
h' : toUint r = toUint n' + toUint m'
⊢ toUint (next (dn && dm) (next (dn != dm) r)) = toUint (next dn n') + toUint (next dm m')
Theorem: FinInt.addfull_toUint
Proof state before:
sz : ℕ
dn : Bool
n' : FinInt sz
ih : ∀ (n m : FinInt (Nat.add sz 0)), toUint (addfull n m) = toUint n + toUint m
dm : Bool
m' : FinInt sz
n✝ : FinInt (sz + 0 + 1)
r : FinInt (sz + 0)
h : addfull n' m' = next false r
h' : toUint r = toUint n' + toUint m'
⊢ toUint (next (dn && dm) (next (dn != dm) r)) = toUint (next dn n') + toUint (next dm m')
Tactic:
cases dn <;> cases dm <;> simp [FinInt.toUint, h']
<;> sorry_arith
Proof state after:
no goals
Theorem: FinInt.addfull_toUint
Proof state before:
sz : ℕ
dn : Bool
n' : FinInt sz
ih : ∀ (n m : FinInt (Nat.add sz 0)), toUint (addfull n m) = toUint n + toUint m
dm : Bool
m' : FinInt sz
n✝ : FinInt (sz + 0 + 1)
r : FinInt (sz + 0)
h : addfull n' m' = next false r
⊢ toUint r = toUint n' + toUint m'
Tactic:
rw [←ih n' m']
Proof state after:
sz : ℕ
dn : Bool
n' : FinInt sz
ih : ∀ (n m : FinInt (Nat.add sz 0)), toUint (addfull n m) = toUint n + toUint m
dm : Bool
m' : FinInt sz
n✝ : FinInt (sz + 0 + 1)
r : FinInt (sz + 0)
h : addfull n' m' = next false r
⊢ toUint r = toUint (addfull n' m')
Theorem: FinInt.addfull_toUint
Proof state before:
sz : ℕ
dn : Bool
n' : FinInt sz
ih : ∀ (n m : FinInt (Nat.add sz 0)), toUint (addfull n m) = toUint n + toUint m
dm : Bool
m' : FinInt sz
n✝ : FinInt (sz + 0 + 1)
r : FinInt (sz + 0)
h : addfull n' m' = next false r
⊢ toUint r = toUint (addfull n' m')
Tactic:
simp [h]
Proof state after:
no goals
Theorem: FinInt.addfull_toUint
Proof state before:
sz : ℕ
dn : Bool
n' : FinInt sz
ih : ∀ (n m : FinInt (Nat.add sz 0)), toUint (addfull n m) = toUint n + toUint m
dm : Bool
m' : FinInt sz
n✝ : FinInt (sz + 0 + 1)
r : FinInt (sz + 0)
h : addfull n' m' = next true r
⊢ toUint (next (dn || dm) (next (dn == dm) r)) = toUint (next dn n') + toUint (next dm m')
Tactic:
have h': r.toUint = n'.toUint + m'.toUint - 2^sz := by
  rw [←ih n' m']
  simp [h, Int.add_comm, toSint]
Proof state after:
sz : ℕ
dn : Bool
n' : FinInt sz
ih : ∀ (n m : FinInt (Nat.add sz 0)), toUint (addfull n m) = toUint n + toUint m
dm : Bool
m' : FinInt sz
n✝ : FinInt (sz + 0 + 1)
r : FinInt (sz + 0)
h : addfull n' m' = next true r
h' : toUint r = toUint n' + toUint m' - 2 ^ sz
⊢ toUint (next (dn || dm) (next (dn == dm) r)) = toUint (next dn n') + toUint (next dm m')
Theorem: FinInt.addfull_toUint
Proof state before:
sz : ℕ
dn : Bool
n' : FinInt sz
ih : ∀ (n m : FinInt (Nat.add sz 0)), toUint (addfull n m) = toUint n + toUint m
dm : Bool
m' : FinInt sz
n✝ : FinInt (sz + 0 + 1)
r : FinInt (sz + 0)
h : addfull n' m' = next true r
h' : toUint r = toUint n' + toUint m' - 2 ^ sz
⊢ toUint (next (dn || dm) (next (dn == dm) r)) = toUint (next dn n') + toUint (next dm m')
Tactic:
cases dn <;> cases dm <;> simp [FinInt.toUint, h', toSint]
<;> sorry_arith
Proof state after:
no goals
Theorem: FinInt.addfull_toUint
Proof state before:
sz : ℕ
dn : Bool
n' : FinInt sz
ih : ∀ (n m : FinInt (Nat.add sz 0)), toUint (addfull n m) = toUint n + toUint m
dm : Bool
m' : FinInt sz
n✝ : FinInt (sz + 0 + 1)
r : FinInt (sz + 0)
h : addfull n' m' = next true r
⊢ toUint r = toUint n' + toUint m' - 2 ^ sz
Tactic:
rw [←ih n' m']
Proof state after:
sz : ℕ
dn : Bool
n' : FinInt sz
ih : ∀ (n m : FinInt (Nat.add sz 0)), toUint (addfull n m) = toUint n + toUint m
dm : Bool
m' : FinInt sz
n✝ : FinInt (sz + 0 + 1)
r : FinInt (sz + 0)
h : addfull n' m' = next true r
⊢ toUint r = toUint (addfull n' m') - 2 ^ sz
Theorem: FinInt.addfull_toUint
Proof state before:
sz : ℕ
dn : Bool
n' : FinInt sz
ih : ∀ (n m : FinInt (Nat.add sz 0)), toUint (addfull n m) = toUint n + toUint m
dm : Bool
m' : FinInt sz
n✝ : FinInt (sz + 0 + 1)
r : FinInt (sz + 0)
h : addfull n' m' = next true r
⊢ toUint r = toUint (addfull n' m') - 2 ^ sz
Tactic:
simp [h, Int.add_comm, toSint]
Proof state after:
no goals
Theorem: FinInt.addfull_toSint
Proof state before:
sz : ℕ
n m : FinInt (sz + 1)
⊢ toSint (addfull n m) =
    match n, m with
    | next false n', next false m' => toSint n + toSint m
    | next false n', next true m' =>
      match addfull n m with
      | next false a => toSint n + toSint m + 2 ^ (sz + 1)
      | next true a => toSint n + toSint m - 2 ^ (sz + 1)
    | next true n', next false m' =>
      match addfull n m with
      | next false a => toSint n + toSint m + 2 ^ (sz + 1)
      | next true a => toSint n + toSint m - 2 ^ (sz + 1)
    | next true n', next true m' => toSint n + toSint m
Tactic:
cases n
Proof state after:
case next
sz : ℕ
m : FinInt (sz + 1)
a✝¹ : Bool
a✝ : FinInt sz
⊢ toSint (addfull (next a✝¹ a✝) m) =
    match next a✝¹ a✝, m with
    | next false n', next false m' => toSint (next a✝¹ a✝) + toSint m
    | next false n', next true m' =>
      match addfull (next a✝¹ a✝) m with
      | next false a => toSint (next a✝¹ a✝) + toSint m + 2 ^ (sz + 1)
      | next true a => toSint (next a✝¹ a✝) + toSint m - 2 ^ (sz + 1)
    | next true n', next false m' =>
      match addfull (next a✝¹ a✝) m with
      | next false a => toSint (next a✝¹ a✝) + toSint m + 2 ^ (sz + 1)
      | next true a => toSint (next a✝¹ a✝) + toSint m - 2 ^ (sz + 1)
    | next true n', next true m' => toSint (next a✝¹ a✝) + toSint m
Theorem: FinInt.addfull_toSint
Proof state before:
sz : ℕ
m : FinInt (sz + 1)
bn : Bool
n' : FinInt sz
⊢ toSint (addfull (next bn n') m) =
    match next bn n', m with
    | next false n'_1, next false m' => toSint (next bn n') + toSint m
    | next false n'_1, next true m' =>
      match addfull (next bn n') m with
      | next false a => toSint (next bn n') + toSint m + 2 ^ (sz + 1)
      | next true a => toSint (next bn n') + toSint m - 2 ^ (sz + 1)
    | next true n'_1, next false m' =>
      match addfull (next bn n') m with
      | next false a => toSint (next bn n') + toSint m + 2 ^ (sz + 1)
      | next true a => toSint (next bn n') + toSint m - 2 ^ (sz + 1)
    | next true n'_1, next true m' => toSint (next bn n') + toSint m
Tactic:
case next bn n' =>
cases m; case next bm m' =>
cases bn <;> cases bm <;> simp [addfull]
case false.false =>
match h: addfull n' m' with
| .next br r =>
cases br <;> simp [toSint, ←FinInt.addfull_toUint, h]
case false.true =>
match h: addfull n' m' with
| .next br r =>
have h' := FinInt.addfull_toUint n' m'
rw [h] at h'
cases br <;> simp at h' <;> simp [toSint]
. simp [h']; sorry_arith
. sorry_arith
case true.false =>
match h: addfull n' m' with
| .next br r =>
have h' := FinInt.addfull_toUint n' m'
rw [h] at h'
cases br <;> simp at h' <;> simp [toSint]
. simp [h']; sorry_arith
. sorry_arith
case true.true =>
match h: addfull n' m' with
| .next br r =>
have h' := FinInt.addfull_toUint n' m'
rw [h] at h'
cases br <;> simp at h' <;> simp [toSint, h'] <;> sorry_arith
Proof state after:
no goals
Theorem: FinInt.addfull_toSint
Proof state before:
sz : ℕ
m : FinInt (sz + 1)
bn : Bool
n' : FinInt sz
⊢ toSint (addfull (next bn n') m) =
    match next bn n', m with
    | next false n'_1, next false m' => toSint (next bn n') + toSint m
    | next false n'_1, next true m' =>
      match addfull (next bn n') m with
      | next false a => toSint (next bn n') + toSint m + 2 ^ (sz + 1)
      | next true a => toSint (next bn n') + toSint m - 2 ^ (sz + 1)
    | next true n'_1, next false m' =>
      match addfull (next bn n') m with
      | next false a => toSint (next bn n') + toSint m + 2 ^ (sz + 1)
      | next true a => toSint (next bn n') + toSint m - 2 ^ (sz + 1)
    | next true n'_1, next true m' => toSint (next bn n') + toSint m
Tactic:
cases m
Proof state after:
case next
sz : ℕ
bn : Bool
n' : FinInt sz
a✝¹ : Bool
a✝ : FinInt sz
⊢ toSint (addfull (next bn n') (next a✝¹ a✝)) =
    match next bn n', next a✝¹ a✝ with
    | next false n'_1, next false m' => toSint (next bn n') + toSint (next a✝¹ a✝)
    | next false n'_1, next true m' =>
      match addfull (next bn n') (next a✝¹ a✝) with
      | next false a => toSint (next bn n') + toSint (next a✝¹ a✝) + 2 ^ (sz + 1)
      | next true a => toSint (next bn n') + toSint (next a✝¹ a✝) - 2 ^ (sz + 1)
    | next true n'_1, next false m' =>
      match addfull (next bn n') (next a✝¹ a✝) with
      | next false a => toSint (next bn n') + toSint (next a✝¹ a✝) + 2 ^ (sz + 1)
      | next true a => toSint (next bn n') + toSint (next a✝¹ a✝) - 2 ^ (sz + 1)
    | next true n'_1, next true m' => toSint (next bn n') + toSint (next a✝¹ a✝)
Theorem: FinInt.addfull_toSint
Proof state before:
sz : ℕ
bn : Bool
n' : FinInt sz
bm : Bool
m' : FinInt sz
⊢ toSint (addfull (next bn n') (next bm m')) =
    match next bn n', next bm m' with
    | next false n'_1, next false m'_1 => toSint (next bn n') + toSint (next bm m')
    | next false n'_1, next true m'_1 =>
      match addfull (next bn n') (next bm m') with
      | next false a => toSint (next bn n') + toSint (next bm m') + 2 ^ (sz + 1)
      | next true a => toSint (next bn n') + toSint (next bm m') - 2 ^ (sz + 1)
    | next true n'_1, next false m'_1 =>
      match addfull (next bn n') (next bm m') with
      | next false a => toSint (next bn n') + toSint (next bm m') + 2 ^ (sz + 1)
      | next true a => toSint (next bn n') + toSint (next bm m') - 2 ^ (sz + 1)
    | next true n'_1, next true m'_1 => toSint (next bn n') + toSint (next bm m')
Tactic:
case next bm m' =>
cases bn <;> cases bm <;> simp [addfull]
case false.false =>
match h: addfull n' m' with
| .next br r =>
cases br <;> simp [toSint, ←FinInt.addfull_toUint, h]
case false.true =>
match h: addfull n' m' with
| .next br r =>
have h' := FinInt.addfull_toUint n' m'
rw [h] at h'
cases br <;> simp at h' <;> simp [toSint]
. simp [h']; sorry_arith
. sorry_arith
case true.false =>
match h: addfull n' m' with
| .next br r =>
have h' := FinInt.addfull_toUint n' m'
rw [h] at h'
cases br <;> simp at h' <;> simp [toSint]
. simp [h']; sorry_arith
. sorry_arith
case true.true =>
match h: addfull n' m' with
| .next br r =>
have h' := FinInt.addfull_toUint n' m'
rw [h] at h'
cases br <;> simp at h' <;> simp [toSint, h'] <;> sorry_arith
Proof state after:
no goals