internlm/Lean-Github huggingface dataset:
Theorem: FinInt.add_toSint_msb
Proof state before:
sz : ℕ
n' m' : FinInt sz
h :
  toSint
      (match addfull n' m' with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r)) =
    match
      match addfull n' m' with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r) with
    | next false a => toSint (next false n') + toSint (next true m') + 2 ^ (sz + 1)
    | next true a => toSint (next false n') + toSint (next true m') - 2 ^ (sz + 1)
⊢ toSint (next false n' + next true m') = toSint (next false n') + toSint (next true m')
Tactic:
case false.true =>
  match h': addfull n' m' with
  | .next br r =>
    rw [h'] at h
    cases br <;> simp [bne, BEq.beq, toSint] at * <;> sorry_arith
Proof state after:
no goals
Theorem: FinInt.add_toSint_msb
Proof state before:
sz : ℕ
n' m' : FinInt sz
h :
  toSint
      (match addfull n' m' with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r)) =
    match
      match addfull n' m' with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r) with
    | next false a => toSint (next true n') + toSint (next false m') + 2 ^ (sz + 1)
    | next true a => toSint (next true n') + toSint (next false m') - 2 ^ (sz + 1)
⊢ toSint (next true n' + next false m') = toSint (next true n') + toSint (next false m')
Tactic:
case true.false =>
  match h': addfull n' m' with
  | .next br r =>
    rw [h'] at h
    cases br <;> simp [bne, BEq.beq, toSint] at * <;> sorry_arith
Proof state after:
no goals
Theorem: FinInt.add_toSint_msb
Proof state before:
sz : ℕ
n' m' : FinInt sz
h :
  toSint
      (match addfull n' m' with
      | next false r => next true (next false r)
      | next true r => next true (next true r)) =
    toSint (next true n') + toSint (next true m')
⊢ toSint (next true n' + next true m') =
    match next true n' + next true m' with
    | next false a => toSint (next true n') + toSint (next true m') + 2 ^ (sz + 1)
    | next true a => toSint (next true n') + toSint (next true m')
Tactic:
case true.true =>
  match h': addfull n' m' with
  | .next br r =>
    rw [h'] at h
    cases br <;> simp [bne, toSint] at * <;> sorry_arith
Proof state after:
no goals
Theorem: FinInt.add_toSint_msb
Proof state before:
sz : ℕ
n' m' : FinInt sz
h :
  toSint
      (match addfull n' m' with
      | next false r => next false (next false r)
      | next true r => next false (next true r)) =
    toSint (next false n') + toSint (next false m')
⊢ toSint (next false n' + next false m') =
    match next false n' + next false m' with
    | next false a => toSint (next false n') + toSint (next false m')
    | next true a => toSint (next false n') + toSint (next false m') - 2 ^ (sz + 1)
Tactic:
match h': addfull n' m' with
| .next br r =>
  rw [h'] at h
  cases br <;> simp [bne, toSint] at * <;> sorry_arith
Proof state after:
no goals
Theorem: FinInt.add_toSint_msb
Proof state before:
sz : ℕ
n' m' : FinInt sz
h :
  toSint
      (match addfull n' m' with
      | next false r => next false (next false r)
      | next true r => next false (next true r)) =
    toSint (next false n') + toSint (next false m')
br : Bool
r : FinInt sz
h' : addfull n' m' = next br r
⊢ toSint (next false n' + next false m') =
    match next false n' + next false m' with
    | next false a => toSint (next false n') + toSint (next false m')
    | next true a => toSint (next false n') + toSint (next false m') - 2 ^ (sz + 1)
Tactic:
rw [h'] at h
Proof state after:
sz : ℕ
n' m' : FinInt sz
br : Bool
r : FinInt sz
h :
  toSint
      (match next br r with
      | next false r => next false (next false r)
      | next true r => next false (next true r)) =
    toSint (next false n') + toSint (next false m')
h' : addfull n' m' = next br r
⊢ toSint (next false n' + next false m') =
    match next false n' + next false m' with
    | next false a => toSint (next false n') + toSint (next false m')
    | next true a => toSint (next false n') + toSint (next false m') - 2 ^ (sz + 1)
Theorem: FinInt.add_toSint_msb
Proof state before:
sz : ℕ
n' m' : FinInt sz
br : Bool
r : FinInt sz
h :
  toSint
      (match next br r with
      | next false r => next false (next false r)
      | next true r => next false (next true r)) =
    toSint (next false n') + toSint (next false m')
h' : addfull n' m' = next br r
⊢ toSint (next false n' + next false m') =
    match next false n' + next false m' with
    | next false a => toSint (next false n') + toSint (next false m')
    | next true a => toSint (next false n') + toSint (next false m') - 2 ^ (sz + 1)
Tactic:
cases br <;> simp [bne, toSint] at * <;> sorry_arith
Proof state after:
no goals
Theorem: FinInt.add_toSint_msb
Proof state before:
sz : ℕ
n' m' : FinInt sz
h :
  toSint
      (match addfull n' m' with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r)) =
    match
      match addfull n' m' with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r) with
    | next false a => toSint (next false n') + toSint (next true m') + 2 ^ (sz + 1)
    | next true a => toSint (next false n') + toSint (next true m') - 2 ^ (sz + 1)
⊢ toSint (next false n' + next true m') = toSint (next false n') + toSint (next true m')
Tactic:
match h': addfull n' m' with
| .next br r =>
  rw [h'] at h
  cases br <;> simp [bne, BEq.beq, toSint] at * <;> sorry_arith
Proof state after:
no goals
Theorem: FinInt.add_toSint_msb
Proof state before:
sz : ℕ
n' m' : FinInt sz
h :
  toSint
      (match addfull n' m' with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r)) =
    match
      match addfull n' m' with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r) with
    | next false a => toSint (next false n') + toSint (next true m') + 2 ^ (sz + 1)
    | next true a => toSint (next false n') + toSint (next true m') - 2 ^ (sz + 1)
br : Bool
r : FinInt sz
h' : addfull n' m' = next br r
⊢ toSint (next false n' + next true m') = toSint (next false n') + toSint (next true m')
Tactic:
rw [h'] at h
Proof state after:
sz : ℕ
n' m' : FinInt sz
br : Bool
r : FinInt sz
h :
  toSint
      (match next br r with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r)) =
    match
      match next br r with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r) with
    | next false a => toSint (next false n') + toSint (next true m') + 2 ^ (sz + 1)
    | next true a => toSint (next false n') + toSint (next true m') - 2 ^ (sz + 1)
h' : addfull n' m' = next br r
⊢ toSint (next false n' + next true m') = toSint (next false n') + toSint (next true m')
Theorem: FinInt.add_toSint_msb
Proof state before:
sz : ℕ
n' m' : FinInt sz
br : Bool
r : FinInt sz
h :
  toSint
      (match next br r with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r)) =
    match
      match next br r with
      | next false r => next false (next (false != true) r)
      | next true r => next true (next (false == true) r) with
    | next false a => toSint (next false n') + toSint (next true m') + 2 ^ (sz + 1)
    | next true a => toSint (next false n') + toSint (next true m') - 2 ^ (sz + 1)
h' : addfull n' m' = next br r
⊢ toSint (next false n' + next true m') = toSint (next false n') + toSint (next true m')
Tactic:
cases br <;> simp [bne, BEq.beq, toSint] at * <;> sorry_arith
Proof state after:
no goals
Theorem: FinInt.add_toSint_msb
Proof state before:
sz : ℕ
n' m' : FinInt sz
h :
  toSint
      (match addfull n' m' with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r)) =
    match
      match addfull n' m' with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r) with
    | next false a => toSint (next true n') + toSint (next false m') + 2 ^ (sz + 1)
    | next true a => toSint (next true n') + toSint (next false m') - 2 ^ (sz + 1)
⊢ toSint (next true n' + next false m') = toSint (next true n') + toSint (next false m')
Tactic:
match h': addfull n' m' with
| .next br r =>
  rw [h'] at h
  cases br <;> simp [bne, BEq.beq, toSint] at * <;> sorry_arith
Proof state after:
no goals
Theorem: FinInt.add_toSint_msb
Proof state before:
sz : ℕ
n' m' : FinInt sz
h :
  toSint
      (match addfull n' m' with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r)) =
    match
      match addfull n' m' with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r) with
    | next false a => toSint (next true n') + toSint (next false m') + 2 ^ (sz + 1)
    | next true a => toSint (next true n') + toSint (next false m') - 2 ^ (sz + 1)
br : Bool
r : FinInt sz
h' : addfull n' m' = next br r
⊢ toSint (next true n' + next false m') = toSint (next true n') + toSint (next false m')
Tactic:
rw [h'] at h
Proof state after:
sz : ℕ
n' m' : FinInt sz
br : Bool
r : FinInt sz
h :
  toSint
      (match next br r with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r)) =
    match
      match next br r with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r) with
    | next false a => toSint (next true n') + toSint (next false m') + 2 ^ (sz + 1)
    | next true a => toSint (next true n') + toSint (next false m') - 2 ^ (sz + 1)
h' : addfull n' m' = next br r
⊢ toSint (next true n' + next false m') = toSint (next true n') + toSint (next false m')
Theorem: FinInt.add_toSint_msb
Proof state before:
sz : ℕ
n' m' : FinInt sz
br : Bool
r : FinInt sz
h :
  toSint
      (match next br r with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r)) =
    match
      match next br r with
      | next false r => next false (next (true != false) r)
      | next true r => next true (next (true == false) r) with
    | next false a => toSint (next true n') + toSint (next false m') + 2 ^ (sz + 1)
    | next true a => toSint (next true n') + toSint (next false m') - 2 ^ (sz + 1)
h' : addfull n' m' = next br r
⊢ toSint (next true n' + next false m') = toSint (next true n') + toSint (next false m')
Tactic:
cases br <;> simp [bne, BEq.beq, toSint] at * <;> sorry_arith
Proof state after:
no goals
Theorem: FinInt.add_toSint_msb
Proof state before:
sz : ℕ
n' m' : FinInt sz
h :
  toSint
      (match addfull n' m' with
      | next false r => next true (next false r)
      | next true r => next true (next true r)) =
    toSint (next true n') + toSint (next true m')
⊢ toSint (next true n' + next true m') =
    match next true n' + next true m' with
    | next false a => toSint (next true n') + toSint (next true m') + 2 ^ (sz + 1)
    | next true a => toSint (next true n') + toSint (next true m')
Tactic:
match h': addfull n' m' with
| .next br r =>
  rw [h'] at h
  cases br <;> simp [bne, toSint] at * <;> sorry_arith
Proof state after:
no goals
Theorem: FinInt.add_toSint_msb
Proof state before:
sz : ℕ
n' m' : FinInt sz
h :
  toSint
      (match addfull n' m' with
      | next false r => next true (next false r)
      | next true r => next true (next true r)) =
    toSint (next true n') + toSint (next true m')
br : Bool
r : FinInt sz
h' : addfull n' m' = next br r
⊢ toSint (next true n' + next true m') =
    match next true n' + next true m' with
    | next false a => toSint (next true n') + toSint (next true m') + 2 ^ (sz + 1)
    | next true a => toSint (next true n') + toSint (next true m')
Tactic:
rw [h'] at h
Proof state after:
sz : ℕ
n' m' : FinInt sz
br : Bool
r : FinInt sz
h :
  toSint
      (match next br r with
      | next false r => next true (next false r)
      | next true r => next true (next true r)) =
    toSint (next true n') + toSint (next true m')
h' : addfull n' m' = next br r
⊢ toSint (next true n' + next true m') =
    match next true n' + next true m' with
    | next false a => toSint (next true n') + toSint (next true m') + 2 ^ (sz + 1)
    | next true a => toSint (next true n') + toSint (next true m')
Theorem: FinInt.add_toSint_msb
Proof state before:
sz : ℕ
n' m' : FinInt sz
br : Bool
r : FinInt sz
h :
  toSint
      (match next br r with
      | next false r => next true (next false r)
      | next true r => next true (next true r)) =
    toSint (next true n') + toSint (next true m')
h' : addfull n' m' = next br r
⊢ toSint (next true n' + next true m') =
    match next true n' + next true m' with
    | next false a => toSint (next true n') + toSint (next true m') + 2 ^ (sz + 1)
    | next true a => toSint (next true n') + toSint (next true m')
Tactic:
cases br <;> simp [bne, toSint] at * <;> sorry_arith
Proof state after:
no goals
Theorem: FinInt.addv_comm
Proof state before:
sz : ℕ
n m : FinInt (sz + 1)
⊢ addv n m = addv m n
Tactic:
simp [addv]
Proof state after:
sz : ℕ
n m : FinInt (sz + 1)
⊢ (match n, m with
    | next false n', next false m' =>
      match n + m with
      | next msb r' => (next msb r', msb)
    | next true n', next true m' =>
      match n + m with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (n + m, false)) =
    match m, n with
    | next false n', next false m' =>
      match m + n with
      | next msb r' => (next msb r', msb)
    | next true n', next true m' =>
      match m + n with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (m + n, false)
Theorem: FinInt.addv_comm
Proof state before:
sz : ℕ
n m : FinInt (sz + 1)
⊢ (match n, m with
    | next false n', next false m' =>
      match n + m with
      | next msb r' => (next msb r', msb)
    | next true n', next true m' =>
      match n + m with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (n + m, false)) =
    match m, n with
    | next false n', next false m' =>
      match m + n with
      | next msb r' => (next msb r', msb)
    | next true n', next true m' =>
      match m + n with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (m + n, false)
Tactic:
cases n
Proof state after:
case next
sz : ℕ
m : FinInt (sz + 1)
a✝¹ : Bool
a✝ : FinInt sz
⊢ (match next a✝¹ a✝, m with
    | next false n', next false m' =>
      match next a✝¹ a✝ + m with
      | next msb r' => (next msb r', msb)
    | next true n', next true m' =>
      match next a✝¹ a✝ + m with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (next a✝¹ a✝ + m, false)) =
    match m, next a✝¹ a✝ with
    | next false n', next false m' =>
      match m + next a✝¹ a✝ with
      | next msb r' => (next msb r', msb)
    | next true n', next true m' =>
      match m + next a✝¹ a✝ with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (m + next a✝¹ a✝, false)
Theorem: FinInt.addv_comm
Proof state before:
case next
sz : ℕ
m : FinInt (sz + 1)
a✝¹ : Bool
a✝ : FinInt sz
⊢ (match next a✝¹ a✝, m with
    | next false n', next false m' =>
      match next a✝¹ a✝ + m with
      | next msb r' => (next msb r', msb)
    | next true n', next true m' =>
      match next a✝¹ a✝ + m with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (next a✝¹ a✝ + m, false)) =
    match m, next a✝¹ a✝ with
    | next false n', next false m' =>
      match m + next a✝¹ a✝ with
      | next msb r' => (next msb r', msb)
    | next true n', next true m' =>
      match m + next a✝¹ a✝ with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (m + next a✝¹ a✝, false)
Tactic:
cases m
Proof state after:
case next.next
sz : ℕ
a✝³ : Bool
a✝² : FinInt sz
a✝¹ : Bool
a✝ : FinInt sz
⊢ (match next a✝³ a✝², next a✝¹ a✝ with
    | next false n', next false m' =>
      match next a✝³ a✝² + next a✝¹ a✝ with
      | next msb r' => (next msb r', msb)
    | next true n', next true m' =>
      match next a✝³ a✝² + next a✝¹ a✝ with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (next a✝³ a✝² + next a✝¹ a✝, false)) =
    match next a✝¹ a✝, next a✝³ a✝² with
    | next false n', next false m' =>
      match next a✝¹ a✝ + next a✝³ a✝² with
      | next msb r' => (next msb r', msb)
    | next true n', next true m' =>
      match next a✝¹ a✝ + next a✝³ a✝² with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (next a✝¹ a✝ + next a✝³ a✝², false)
Theorem: FinInt.addv_comm
Proof state before:
sz : ℕ
bn : Bool
n' : FinInt sz
bm : Bool
m' : FinInt sz
⊢ (match next bn n', next bm m' with
    | next false n'_1, next false m'_1 =>
      match next bn n' + next bm m' with
      | next msb r' => (next msb r', msb)
    | next true n'_1, next true m'_1 =>
      match next bn n' + next bm m' with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (next bn n' + next bm m', false)) =
    match next bm m', next bn n' with
    | next false n'_1, next false m'_1 =>
      match next bm m' + next bn n' with
      | next msb r' => (next msb r', msb)
    | next true n'_1, next true m'_1 =>
      match next bm m' + next bn n' with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (next bm m' + next bn n', false)
Tactic:
case next.next bn n' bm m' =>
simp [add_comm]; cases bn <;> cases bm <;> rfl
Proof state after:
no goals
Theorem: FinInt.addv_comm
Proof state before:
sz : ℕ
bn : Bool
n' : FinInt sz
bm : Bool
m' : FinInt sz
⊢ (match next bn n', next bm m' with
    | next false n'_1, next false m'_1 =>
      match next bn n' + next bm m' with
      | next msb r' => (next msb r', msb)
    | next true n'_1, next true m'_1 =>
      match next bn n' + next bm m' with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (next bn n' + next bm m', false)) =
    match next bm m', next bn n' with
    | next false n'_1, next false m'_1 =>
      match next bm m' + next bn n' with
      | next msb r' => (next msb r', msb)
    | next true n'_1, next true m'_1 =>
      match next bm m' + next bn n' with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (next bm m' + next bn n', false)
Tactic:
simp [add_comm]
Proof state after:
sz : ℕ
bn : Bool
n' : FinInt sz
bm : Bool
m' : FinInt sz
⊢ (match next bn n', next bm m' with
    | next false n'_1, next false m'_1 =>
      match next bn n' + next bm m' with
      | next msb r' => (next msb r', msb)
    | next true n'_1, next true m'_1 =>
      match next bn n' + next bm m' with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (next bn n' + next bm m', false)) =
    match next bm m', next bn n' with
    | next false n'_1, next false m'_1 =>
      match next bn n' + next bm m' with
      | next msb r' => (next msb r', msb)
    | next true n'_1, next true m'_1 =>
      match next bn n' + next bm m' with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (next bn n' + next bm m', false)
Theorem: FinInt.addv_comm
Proof state before:
sz : ℕ
bn : Bool
n' : FinInt sz
bm : Bool
m' : FinInt sz
⊢ (match next bn n', next bm m' with
    | next false n'_1, next false m'_1 =>
      match next bn n' + next bm m' with
      | next msb r' => (next msb r', msb)
    | next true n'_1, next true m'_1 =>
      match next bn n' + next bm m' with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (next bn n' + next bm m', false)) =
    match next bm m', next bn n' with
    | next false n'_1, next false m'_1 =>
      match next bn n' + next bm m' with
      | next msb r' => (next msb r', msb)
    | next true n'_1, next true m'_1 =>
      match next bn n' + next bm m' with
      | next msb r' => (next msb r', !msb)
    | x, x_1 => (next bn n' + next bm m', false)
Tactic:
cases bn <;> cases bm <;> rfl
Proof state after:
no goals
Theorem: FinInt.addv_toSint
Proof state before:
sz : ℕ
n m : FinInt (sz + 1)
⊢ (addv n m).snd = false → toSint (addv n m).fst = toSint n + toSint m
Tactic:
intros h_nov
Proof state after:
sz : ℕ
n m : FinInt (sz + 1)
h_nov : (addv n m).snd = false
⊢ toSint (addv n m).fst = toSint n + toSint m
Theorem: FinInt.addv_toSint
Proof state before:
sz : ℕ
n m : FinInt (sz + 1)
h_nov : (addv n m).snd = false
⊢ toSint (addv n m).fst = toSint n + toSint m
Tactic:
simp [addv] at *
Proof state after:
sz : ℕ
n m : FinInt (sz + 1)
h_nov :
  (match n, m with
      | next false n', next false m' =>
        match n + m with
        | next msb r' => (next msb r', msb)
      | next true n', next true m' =>
        match n + m with
        | next msb r' => (next msb r', !msb)
      | x, x_1 => (n + m, false)).snd =
    false
⊢ toSint
      (match n, m with
        | next false n', next false m' =>
          match n + m with
          | next msb r' => (next msb r', msb)
        | next true n', next true m' =>
          match n + m with
          | next msb r' => (next msb r', !msb)
        | x, x_1 => (n + m, false)).fst =
    toSint n + toSint m
Theorem: FinInt.addv_toSint
Proof state before:
sz : ℕ
n m : FinInt (sz + 1)
h_nov :
  (match n, m with
      | next false n', next false m' =>
        match n + m with
        | next msb r' => (next msb r', msb)
      | next true n', next true m' =>
        match n + m with
        | next msb r' => (next msb r', !msb)
      | x, x_1 => (n + m, false)).snd =
    false
⊢ toSint
      (match n, m with
        | next false n', next false m' =>
          match n + m with
          | next msb r' => (next msb r', msb)
        | next true n', next true m' =>
          match n + m with
          | next msb r' => (next msb r', !msb)
        | x, x_1 => (n + m, false)).fst =
    toSint n + toSint m
Tactic:
have h := add_toSint_msb n m
Proof state after:
sz : ℕ
n m : FinInt (sz + 1)
h_nov :
  (match n, m with
      | next false n', next false m' =>
        match n + m with
        | next msb r' => (next msb r', msb)
      | next true n', next true m' =>
        match n + m with
        | next msb r' => (next msb r', !msb)
      | x, x_1 => (n + m, false)).snd =
    false
h :
  toSint (n + m) =
    match n, m with
    | next false n', next false m' =>
      match n + m with
      | next false a => toSint n + toSint m
      | next true a => toSint n + toSint m - 2 ^ (sz + 1)
    | next false n', next true m' => toSint n + toSint m
    | next true n', next false m' => toSint n + toSint m
    | next true n', next true m' =>
      match n + m with
      | next false a => toSint n + toSint m + 2 ^ (sz + 1)
      | next true a => toSint n + toSint m
⊢ toSint
      (match n, m with
        | next false n', next false m' =>
          match n + m with
          | next msb r' => (next msb r', msb)
        | next true n', next true m' =>
          match n + m with
          | next msb r' => (next msb r', !msb)
        | x, x_1 => (n + m, false)).fst =
    toSint n + toSint m