internlm/Lean-Github huggingface dataset:
Theorem: FinInt.toUint_ge
Proof state before:
sz : ℕ
⊢ ∀ {n : FinInt sz}, toUint n ≥ 0
Tactic:
induction sz <;> intros n <;> cases n <;> simp
Proof state after:
case succ.next
n✝ : ℕ
a✝¹ : Bool
a✝ : FinInt n✝
n_ih✝ : ∀ {n : FinInt (Nat.add n✝ 0)}, toUint n ≥ 0
⊢ 0 ≤ toUint (next a✝¹ a✝)
Theorem: FinInt.toUint_ge
Proof state before:
sz : ℕ
bn : Bool
n' : FinInt sz
ih : ∀ {n : FinInt (Nat.add sz 0)}, toUint n ≥ 0
⊢ 0 ≤ toUint (next bn n')
Tactic:
case next sz bn n' ih =>
  cases bn <;> simp [@ih n']
  apply Int.add_ge_zero; apply Int.pow_ge_zero; decide; apply ih
Proof state after:
no goals
Theorem: FinInt.toUint_ge
Proof state before:
sz : ℕ
bn : Bool
n' : FinInt sz
ih : ∀ {n : FinInt (Nat.add sz 0)}, toUint n ≥ 0
⊢ 0 ≤ toUint (next bn n')
Tactic:
cases bn <;> simp [@ih n']
Proof state after:
case true
sz : ℕ
n' : FinInt sz
ih : ∀ {n : FinInt (Nat.add sz 0)}, toUint n ≥ 0
⊢ 0 ≤ 2 ^ sz + toUint n'
Theorem: FinInt.toUint_ge
Proof state before:
case true
sz : ℕ
n' : FinInt sz
ih : ∀ {n : FinInt (Nat.add sz 0)}, toUint n ≥ 0
⊢ 0 ≤ 2 ^ sz + toUint n'
Tactic:
apply Int.add_ge_zero
Proof state after:
case true.a
sz : ℕ
n' : FinInt sz
ih : ∀ {n : FinInt (Nat.add sz 0)}, toUint n ≥ 0
⊢ 2 ^ sz ≥ 0

case true.a
sz : ℕ
n' : FinInt sz
ih : ∀ {n : FinInt (Nat.add sz 0)}, toUint n ≥ 0
⊢ toUint n' ≥ 0
Theorem: FinInt.toUint_ge
Proof state before:
case true.a
sz : ℕ
n' : FinInt sz
ih : ∀ {n : FinInt (Nat.add sz 0)}, toUint n ≥ 0
⊢ 2 ^ sz ≥ 0

case true.a
sz : ℕ
n' : FinInt sz
ih : ∀ {n : FinInt (Nat.add sz 0)}, toUint n ≥ 0
⊢ toUint n' ≥ 0
Tactic:
apply Int.pow_ge_zero
Proof state after:
case true.a.a
sz : ℕ
n' : FinInt sz
ih : ∀ {n : FinInt (Nat.add sz 0)}, toUint n ≥ 0
⊢ 2 ≥ 0

case true.a
sz : ℕ
n' : FinInt sz
ih : ∀ {n : FinInt (Nat.add sz 0)}, toUint n ≥ 0
⊢ toUint n' ≥ 0
Theorem: FinInt.toUint_ge
Proof state before:
case true.a.a
sz : ℕ
n' : FinInt sz
ih : ∀ {n : FinInt (Nat.add sz 0)}, toUint n ≥ 0
⊢ 2 ≥ 0

case true.a
sz : ℕ
n' : FinInt sz
ih : ∀ {n : FinInt (Nat.add sz 0)}, toUint n ≥ 0
⊢ toUint n' ≥ 0
Tactic:
decide
Proof state after:
case true.a
sz : ℕ
n' : FinInt sz
ih : ∀ {n : FinInt (Nat.add sz 0)}, toUint n ≥ 0
⊢ toUint n' ≥ 0
Theorem: FinInt.toUint_ge
Proof state before:
case true.a
sz : ℕ
n' : FinInt sz
ih : ∀ {n : FinInt (Nat.add sz 0)}, toUint n ≥ 0
⊢ toUint n' ≥ 0
Tactic:
apply ih
Proof state after:
no goals
Theorem: FinInt.toUint_lt
Proof state before:
sz : ℕ
n : FinInt sz
⊢ toUint n < 2 ^ sz
Tactic:
revert n
Proof state after:
sz : ℕ
⊢ ∀ {n : FinInt sz}, toUint n < 2 ^ sz
Theorem: FinInt.toUint_lt
Proof state before:
sz : ℕ
⊢ ∀ {n : FinInt sz}, toUint n < 2 ^ sz
Tactic:
induction sz <;> intros n <;> cases n <;> simp
Proof state after:
case succ.next
n✝ : ℕ
a✝¹ : Bool
a✝ : FinInt n✝
n_ih✝ : ∀ {n : FinInt (Nat.add n✝ 0)}, toUint n < 2 ^ Nat.add n✝ 0
⊢ toUint (next a✝¹ a✝) < 2 ^ Nat.succ n✝
Theorem: FinInt.toUint_lt
Proof state before:
case succ.next
n✝ : ℕ
a✝¹ : Bool
a✝ : FinInt n✝
n_ih✝ : ∀ {n : FinInt (Nat.add n✝ 0)}, toUint n < 2 ^ Nat.add n✝ 0
⊢ toUint (next a✝¹ a✝) < 2 ^ Nat.succ n✝
Tactic:
sorry
Proof state after:
no goals
Theorem: FinInt.toSint_ge
Proof state before:
sz : ℕ
n : FinInt (sz + 1)
⊢ toSint n ≥ -2 ^ sz
Tactic:
sorry
Proof state after:
no goals
Theorem: FinInt.toSint_lt
Proof state before:
sz : ℕ
n : FinInt (sz + 1)
⊢ toSint n < 2 ^ sz
Tactic:
cases n
Proof state after:
case next
sz : ℕ
a✝¹ : Bool
a✝ : FinInt sz
⊢ toSint (next a✝¹ a✝) < 2 ^ sz
Theorem: FinInt.toSint_lt
Proof state before:
sz : ℕ
bn : Bool
n' : FinInt sz
⊢ toSint (next bn n') < 2 ^ sz
Tactic:
case next bn n' =>
cases bn <;> simp [toSint]
. apply toUint_lt
. sorry_arith
Proof state after:
no goals
Theorem: FinInt.toSint_lt
Proof state before:
sz : ℕ
bn : Bool
n' : FinInt sz
⊢ toSint (next bn n') < 2 ^ sz
Tactic:
cases bn <;> simp [toSint]
Proof state after:
case false
sz : ℕ
n' : FinInt sz
⊢ toUint n' < 2 ^ sz

case true
sz : ℕ
n' : FinInt sz
⊢ toUint n' - 2 ^ sz < 2 ^ sz
Theorem: FinInt.toSint_lt
Proof state before:
case false
sz : ℕ
n' : FinInt sz
⊢ toUint n' < 2 ^ sz

case true
sz : ℕ
n' : FinInt sz
⊢ toUint n' - 2 ^ sz < 2 ^ sz
Tactic:
. apply toUint_lt
Proof state after:
case true
sz : ℕ
n' : FinInt sz
⊢ toUint n' - 2 ^ sz < 2 ^ sz
Theorem: FinInt.toSint_lt
Proof state before:
case true
sz : ℕ
n' : FinInt sz
⊢ toUint n' - 2 ^ sz < 2 ^ sz
Tactic:
. sorry_arith
Proof state after:
no goals
Theorem: FinInt.toUint_zero
Proof state before:
sz : ℕ
⊢ toUint zero = 0
Tactic:
induction sz with
| zero => decide
| succ n ih => simp [toUint, ih]
Proof state after:
no goals
Theorem: FinInt.toUint_zero
Proof state before:
case zero

⊢ toUint zero = 0
Tactic:
decide
Proof state after:
no goals
Theorem: FinInt.toUint_zero
Proof state before:
case succ
n : ℕ
ih : toUint zero = 0
⊢ toUint zero = 0
Tactic:
simp [toUint, ih]
Proof state after:
no goals
Theorem: FinInt.toUint_one
Proof state before:
sz : ℕ
⊢ sz > 0 → toUint one = 1
Tactic:
intros h
Proof state after:
sz : ℕ
h : sz > 0
⊢ toUint one = 1
Theorem: FinInt.toUint_one
Proof state before:
sz : ℕ
h : sz > 0
⊢ toUint one = 1
Tactic:
induction sz with
| zero => cases (by decide: ¬ 0 > 0) h
| succ n ih => cases n; decide; simp [toUint]; apply ih; simp_arith
Proof state after:
no goals
Theorem: FinInt.toUint_one
Proof state before:
case zero
h : Nat.zero > 0
⊢ toUint one = 1
Tactic:
cases (by decide: ¬ 0 > 0) h
Proof state after:
no goals
Theorem: FinInt.toUint_one
Proof state before:
h : Nat.zero > 0
⊢ ¬0 > 0
Tactic:
decide
Proof state after:
no goals
Theorem: FinInt.toUint_one
Proof state before:
case succ
n : ℕ
ih : n > 0 → toUint one = 1
h : Nat.succ n > 0
⊢ toUint one = 1
Tactic:
cases n
Proof state after:
case succ.zero
ih : Nat.zero > 0 → toUint one = 1
h : Nat.succ Nat.zero > 0
⊢ toUint one = 1

case succ.succ
n✝ : ℕ
ih : Nat.succ n✝ > 0 → toUint one = 1
h : Nat.succ (Nat.succ n✝) > 0
⊢ toUint one = 1
Theorem: FinInt.toUint_one
Proof state before:
case succ.zero
ih : Nat.zero > 0 → toUint one = 1
h : Nat.succ Nat.zero > 0
⊢ toUint one = 1

case succ.succ
n✝ : ℕ
ih : Nat.succ n✝ > 0 → toUint one = 1
h : Nat.succ (Nat.succ n✝) > 0
⊢ toUint one = 1
Tactic:
decide
Proof state after:
case succ.succ
n✝ : ℕ
ih : Nat.succ n✝ > 0 → toUint one = 1
h : Nat.succ (Nat.succ n✝) > 0
⊢ toUint one = 1
Theorem: FinInt.toUint_one
Proof state before:
case succ.succ
n✝ : ℕ
ih : Nat.succ n✝ > 0 → toUint one = 1
h : Nat.succ (Nat.succ n✝) > 0
⊢ toUint one = 1
Tactic:
apply ih
Proof state after:
case succ.succ
n✝ : ℕ
ih : Nat.succ n✝ > 0 → toUint one = 1
h : Nat.succ (Nat.succ n✝) > 0
⊢ Nat.succ n✝ > 0
Theorem: FinInt.toUint_one
Proof state before:
case succ.succ
n✝ : ℕ
ih : Nat.succ n✝ > 0 → toUint one = 1
h : Nat.succ (Nat.succ n✝) > 0
⊢ Nat.succ n✝ > 0
Tactic:
simp_arith
Proof state after:
no goals
Theorem: FinInt.toUint_minusOne
Proof state before:
sz : ℕ
⊢ toUint minusOne = 2 ^ sz - 1
Tactic:
induction sz with
| zero => decide
| succ n ih => simp [toUint, ih]; sorry_arith
Proof state after:
no goals
Theorem: FinInt.toUint_minusOne
Proof state before:
case zero

⊢ toUint minusOne = 2 ^ Nat.zero - 1
Tactic:
decide
Proof state after:
no goals
Theorem: FinInt.toUint_minusOne
Proof state before:
case succ
n : ℕ
ih : toUint minusOne = 2 ^ n - 1
⊢ toUint minusOne = 2 ^ Nat.succ n - 1
Tactic:
simp [toUint, ih]
Proof state after:
case succ
n : ℕ
ih : toUint minusOne = 2 ^ n - 1
⊢ 2 ^ n + (2 ^ n - 1) = 2 ^ Nat.succ n - 1
Theorem: FinInt.toUint_minusOne
Proof state before:
case succ
n : ℕ
ih : toUint minusOne = 2 ^ n - 1
⊢ 2 ^ n + (2 ^ n - 1) = 2 ^ Nat.succ n - 1
Tactic:
sorry_arith
Proof state after:
no goals
Theorem: FinInt.msb_bound
Proof state before:
sz : ℕ
b : Bool
n : FinInt sz
⊢ toUint (next b n) < 2 ^ sz ↔ b = false
Tactic:
sorry
Proof state after:
no goals
Theorem: FinInt.toSint_of_toUint
Proof state before:
sz : ℕ
n : FinInt (sz + 1)
⊢ toSint n =
    match n with
    | next false a => toUint n
    | next true a => toUint n - 2 ^ (sz + 1)
Tactic:
match n with
| .O m => simp [toSint, toUint]
| .I m => simp [toSint, toUint]; sorry_arith
Proof state after:
no goals
Theorem: FinInt.toSint_of_toUint
Proof state before:
sz : ℕ
n : FinInt (sz + 1)
m : FinInt sz
⊢ toSint (O m) =
    match O m with
    | next false a => toUint (O m)
    | next true a => toUint (O m) - 2 ^ (sz + 1)
Tactic:
simp [toSint, toUint]
Proof state after:
no goals
Theorem: FinInt.toSint_of_toUint
Proof state before:
sz : ℕ
n : FinInt (sz + 1)
m : FinInt sz
⊢ toSint (I m) =
    match I m with
    | next false a => toUint (I m)
    | next true a => toUint (I m) - 2 ^ (sz + 1)
Tactic:
simp [toSint, toUint]
Proof state after:
sz : ℕ
n : FinInt (sz + 1)
m : FinInt sz
⊢ toUint m - 2 ^ sz = 2 ^ sz + toUint m - 2 ^ (sz + 1)
Theorem: FinInt.toSint_of_toUint
Proof state before:
sz : ℕ
n : FinInt (sz + 1)
m : FinInt sz
⊢ toUint m - 2 ^ sz = 2 ^ sz + toUint m - 2 ^ (sz + 1)
Tactic:
sorry_arith
Proof state after:
no goals
Theorem: FinInt.toUint_of_toSint
Proof state before:
sz : ℕ
n : FinInt (sz + 1)
⊢ toUint n =
    match n with
    | next false a => toSint n
    | next true a => toSint n + 2 ^ (sz + 1)
Tactic:
match n with
| .O m => simp [toSint, toUint]
| .I m => simp [toSint, toUint]; sorry_arith
Proof state after:
no goals
Theorem: FinInt.toUint_of_toSint
Proof state before:
sz : ℕ
n : FinInt (sz + 1)
m : FinInt sz
⊢ toUint (O m) =
    match O m with
    | next false a => toSint (O m)
    | next true a => toSint (O m) + 2 ^ (sz + 1)
Tactic:
simp [toSint, toUint]
Proof state after:
no goals
Theorem: FinInt.toUint_of_toSint
Proof state before:
sz : ℕ
n : FinInt (sz + 1)
m : FinInt sz
⊢ toUint (I m) =
    match I m with
    | next false a => toSint (I m)
    | next true a => toSint (I m) + 2 ^ (sz + 1)
Tactic:
simp [toSint, toUint]
Proof state after:
sz : ℕ
n : FinInt (sz + 1)
m : FinInt sz
⊢ 2 ^ sz + toUint m = toUint m - 2 ^ sz + 2 ^ (sz + 1)
Theorem: FinInt.toUint_of_toSint
Proof state before:
sz : ℕ
n : FinInt (sz + 1)
m : FinInt sz
⊢ 2 ^ sz + toUint m = toUint m - 2 ^ sz + 2 ^ (sz + 1)
Tactic:
sorry_arith
Proof state after:
no goals
Theorem: FinInt.toUint_ofInt
Proof state before:
sz : ℕ
n : ℤ
⊢ toUint (ofInt sz n) = mod2 n sz
Tactic:
induction sz
Proof state after:
case zero
n : ℤ
⊢ toUint (ofInt Nat.zero n) = mod2 n Nat.zero

case succ
n : ℤ
n✝ : ℕ
n_ih✝ : toUint (ofInt n✝ n) = mod2 n n✝
⊢ toUint (ofInt (Nat.succ n✝) n) = mod2 n (Nat.succ n✝)
Theorem: FinInt.toUint_ofInt
Proof state before:
n : ℤ
⊢ toUint (ofInt Nat.zero n) = mod2 n Nat.zero
Tactic:
case zero =>
  simp [mod2]; sorry_arith
Proof state after:
no goals
Theorem: FinInt.toUint_ofInt
Proof state before:
n : ℤ
sz : ℕ
ih : toUint (ofInt sz n) = mod2 n sz
⊢ toUint (ofInt (Nat.succ sz) n) = mod2 n (Nat.succ sz)
Tactic:
case succ sz ih =>
  sorry
Proof state after:
no goals
Theorem: FinInt.toUint_ofInt
Proof state before:
n : ℤ
⊢ toUint (ofInt Nat.zero n) = mod2 n Nat.zero
Tactic:
simp [mod2]
Proof state after:
n : ℤ
⊢ 0 = n % 1
Theorem: FinInt.toUint_ofInt
Proof state before:
n : ℤ
⊢ 0 = n % 1
Tactic:
sorry_arith
Proof state after:
no goals
Theorem: FinInt.toUint_ofInt
Proof state before:
n : ℤ
sz : ℕ
ih : toUint (ofInt sz n) = mod2 n sz
⊢ toUint (ofInt (Nat.succ sz) n) = mod2 n (Nat.succ sz)
Tactic:
sorry
Proof state after:
no goals
Theorem: FinInt.toUint_ofNat
Proof state before:
sz n : ℕ
⊢ toUint (OfNat.ofNat n) = mod2 (↑n) sz
Tactic:
simp [OfNat.ofNat, toUint_ofInt]
Proof state after:
no goals
Theorem: FinInt.toSint_ofSint
Proof state before:
sz : ℕ
n : ℤ
⊢ toSint (ofInt (sz + 1) n) = smod2 n sz
Tactic:
sorry
Proof state after:
no goals
Theorem: FinInt.ofIntAux_spec
Proof state before:
sz : ℕ
n : ℤ
⊢ toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
Tactic:
induction sz
Proof state after:
case zero
n : ℤ
⊢ toUint (FinInt.ofIntAux Nat.zero n).fst = mod2 n Nat.zero ∧ (FinInt.ofIntAux Nat.zero n).snd = n / 2 ^ Nat.zero

case succ
n : ℤ
n✝ : ℕ
n_ih✝ : toUint (FinInt.ofIntAux n✝ n).fst = mod2 n n✝ ∧ (FinInt.ofIntAux n✝ n).snd = n / 2 ^ n✝
⊢ toUint (FinInt.ofIntAux (Nat.succ n✝) n).fst = mod2 n (Nat.succ n✝) ∧
    (FinInt.ofIntAux (Nat.succ n✝) n).snd = n / 2 ^ Nat.succ n✝
Theorem: FinInt.ofIntAux_spec
Proof state before:
n : ℤ
⊢ toUint (FinInt.ofIntAux Nat.zero n).fst = mod2 n Nat.zero ∧ (FinInt.ofIntAux Nat.zero n).snd = n / 2 ^ Nat.zero
Tactic:
case zero =>
  simp [FinInt.ofIntAux]; sorry_arith
Proof state after:
no goals
Theorem: FinInt.ofIntAux_spec
Proof state before:
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
⊢ toUint (FinInt.ofIntAux (Nat.succ sz) n).fst = mod2 n (Nat.succ sz) ∧
    (FinInt.ofIntAux (Nat.succ sz) n).snd = n / 2 ^ Nat.succ sz
Tactic:
case succ sz ih =>
  simp [FinInt.ofIntAux, ih]; constructor
  . have h: (n / 2^sz % 2 = 0) ∨ (n / 2^sz %2 = 1) := by sorry
    match h with
    | .inl h => simp [h, ih]; sorry_arith
    | .inr h => simp [h, ih]; sorry_arith
  . sorry_arith
Proof state after:
no goals
Theorem: FinInt.ofIntAux_spec
Proof state before:
n : ℤ
⊢ toUint (FinInt.ofIntAux Nat.zero n).fst = mod2 n Nat.zero ∧ (FinInt.ofIntAux Nat.zero n).snd = n / 2 ^ Nat.zero
Tactic:
simp [FinInt.ofIntAux]
Proof state after:
n : ℤ
⊢ 0 = mod2 n 0
Theorem: FinInt.ofIntAux_spec
Proof state before:
n : ℤ
⊢ 0 = mod2 n 0
Tactic:
sorry_arith
Proof state after:
no goals
Theorem: FinInt.ofIntAux_spec
Proof state before:
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
⊢ toUint (FinInt.ofIntAux (Nat.succ sz) n).fst = mod2 n (Nat.succ sz) ∧
    (FinInt.ofIntAux (Nat.succ sz) n).snd = n / 2 ^ Nat.succ sz
Tactic:
simp [FinInt.ofIntAux, ih]
Proof state after:
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
⊢ toUint (next (n / 2 ^ sz % 2 == 1) (FinInt.ofIntAux sz n).fst) = mod2 n (Nat.succ sz) ∧
    n / 2 ^ sz / 2 = n / 2 ^ Nat.succ sz
Theorem: FinInt.ofIntAux_spec
Proof state before:
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
⊢ toUint (next (n / 2 ^ sz % 2 == 1) (FinInt.ofIntAux sz n).fst) = mod2 n (Nat.succ sz) ∧
    n / 2 ^ sz / 2 = n / 2 ^ Nat.succ sz
Tactic:
constructor
Proof state after:
case left
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
⊢ toUint (next (n / 2 ^ sz % 2 == 1) (FinInt.ofIntAux sz n).fst) = mod2 n (Nat.succ sz)

case right
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
⊢ n / 2 ^ sz / 2 = n / 2 ^ Nat.succ sz
Theorem: FinInt.ofIntAux_spec
Proof state before:
case left
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
⊢ toUint (next (n / 2 ^ sz % 2 == 1) (FinInt.ofIntAux sz n).fst) = mod2 n (Nat.succ sz)

case right
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
⊢ n / 2 ^ sz / 2 = n / 2 ^ Nat.succ sz
Tactic:
. have h: (n / 2^sz % 2 = 0) ∨ (n / 2^sz %2 = 1) := by sorry
  match h with
  | .inl h => simp [h, ih]; sorry_arith
  | .inr h => simp [h, ih]; sorry_arith
Proof state after:
case right
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
⊢ n / 2 ^ sz / 2 = n / 2 ^ Nat.succ sz
Theorem: FinInt.ofIntAux_spec
Proof state before:
case right
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
⊢ n / 2 ^ sz / 2 = n / 2 ^ Nat.succ sz
Tactic:
. sorry_arith
Proof state after:
no goals
Theorem: FinInt.ofIntAux_spec
Proof state before:
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
⊢ n / 2 ^ sz % 2 = 0 ∨ n / 2 ^ sz % 2 = 1
Tactic:
sorry
Proof state after:
no goals
Theorem: FinInt.ofIntAux_spec
Proof state before:
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
h✝ : n / 2 ^ sz % 2 = 0 ∨ n / 2 ^ sz % 2 = 1
h : n / 2 ^ sz % 2 = 0
⊢ toUint (next (n / 2 ^ sz % 2 == 1) (FinInt.ofIntAux sz n).fst) = mod2 n (Nat.succ sz)
Tactic:
simp [h, ih]
Proof state after:
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
h✝ : n / 2 ^ sz % 2 = 0 ∨ n / 2 ^ sz % 2 = 1
h : n / 2 ^ sz % 2 = 0
⊢ mod2 n sz = mod2 n (Nat.succ sz)
Theorem: FinInt.ofIntAux_spec
Proof state before:
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
h✝ : n / 2 ^ sz % 2 = 0 ∨ n / 2 ^ sz % 2 = 1
h : n / 2 ^ sz % 2 = 0
⊢ mod2 n sz = mod2 n (Nat.succ sz)
Tactic:
sorry_arith
Proof state after:
no goals
Theorem: FinInt.ofIntAux_spec
Proof state before:
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
h✝ : n / 2 ^ sz % 2 = 0 ∨ n / 2 ^ sz % 2 = 1
h : n / 2 ^ sz % 2 = 1
⊢ toUint (next (n / 2 ^ sz % 2 == 1) (FinInt.ofIntAux sz n).fst) = mod2 n (Nat.succ sz)
Tactic:
simp [h, ih]
Proof state after:
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
h✝ : n / 2 ^ sz % 2 = 0 ∨ n / 2 ^ sz % 2 = 1
h : n / 2 ^ sz % 2 = 1
⊢ 2 ^ sz + mod2 n sz = mod2 n (Nat.succ sz)
Theorem: FinInt.ofIntAux_spec
Proof state before:
n : ℤ
sz : ℕ
ih : toUint (FinInt.ofIntAux sz n).fst = mod2 n sz ∧ (FinInt.ofIntAux sz n).snd = n / 2 ^ sz
h✝ : n / 2 ^ sz % 2 = 0 ∨ n / 2 ^ sz % 2 = 1
h : n / 2 ^ sz % 2 = 1
⊢ 2 ^ sz + mod2 n sz = mod2 n (Nat.succ sz)
Tactic:
sorry_arith
Proof state after:
no goals
Theorem: FinInt.eq_of_toUint_eq
Proof state before:
sz : ℕ
a b : FinInt sz
⊢ toUint a = toUint b → a = b
Tactic:
intros h <;> induction sz
Proof state after:
case zero
a b : FinInt Nat.zero
h : toUint a = toUint b
⊢ a = b

case succ
n✝ : ℕ
n_ih✝ : ∀ (a b : FinInt n✝), toUint a = toUint b → a = b
a b : FinInt (Nat.succ n✝)
h : toUint a = toUint b
⊢ a = b
Theorem: FinInt.eq_of_toUint_eq
Proof state before:
a b : FinInt Nat.zero
h : toUint a = toUint b
⊢ a = b
Tactic:
case zero =>
  cases a; cases b; rfl
Proof state after:
no goals
Theorem: FinInt.eq_of_toUint_eq
Proof state before:
sz : ℕ
ih : ∀ (a b : FinInt sz), toUint a = toUint b → a = b
a b : FinInt (Nat.succ sz)
h : toUint a = toUint b
⊢ a = b
Tactic:
case succ sz ih =>
  cases a; case next sz da a' =>
  cases b; case next db b' =>
  cases da <;> cases db <;> simp [toUint] at h <;> simp
  . apply ih _ _ h
  . have h₁ := @toUint_lt _ a'; have h₂ := @toUint_ge _ b'; sorry_arith
  . have h₁ := @toUint_ge _ a'; have h₂ := @toUint_lt _ b'; sorry_arith
  . apply ih; sorry_arith
Proof state after:
no goals
Theorem: FinInt.eq_of_toUint_eq
Proof state before:
a b : FinInt Nat.zero
h : toUint a = toUint b
⊢ a = b
Tactic:
cases a
Proof state after:
case nil
b : FinInt Nat.zero
h : toUint nil = toUint b
⊢ nil = b
Theorem: FinInt.eq_of_toUint_eq
Proof state before:
case nil
b : FinInt Nat.zero
h : toUint nil = toUint b
⊢ nil = b
Tactic:
cases b
Proof state after:
case nil.nil
h : toUint nil = toUint nil
⊢ nil = nil
Theorem: FinInt.eq_of_toUint_eq
Proof state before:
case nil.nil
h : toUint nil = toUint nil
⊢ nil = nil
Tactic:
rfl
Proof state after:
no goals
Theorem: FinInt.eq_of_toUint_eq
Proof state before:
sz : ℕ
ih : ∀ (a b : FinInt sz), toUint a = toUint b → a = b
a b : FinInt (Nat.succ sz)
h : toUint a = toUint b
⊢ a = b
Tactic:
cases a
Proof state after:
case next
n✝ : ℕ
a✝¹ : Bool
a✝ : FinInt n✝
ih : ∀ (a b : FinInt (Nat.add n✝ 0)), toUint a = toUint b → a = b
b : FinInt (Nat.succ (Nat.add n✝ 0))
h : toUint (next a✝¹ a✝) = toUint b
⊢ next a✝¹ a✝ = b
Theorem: FinInt.eq_of_toUint_eq
Proof state before:
sz : ℕ
da : Bool
a' : FinInt sz
ih : ∀ (a b : FinInt (Nat.add sz 0)), toUint a = toUint b → a = b
b : FinInt (Nat.succ (Nat.add sz 0))
h : toUint (next da a') = toUint b
⊢ next da a' = b
Tactic:
case next sz da a' =>
cases b; case next db b' =>
cases da <;> cases db <;> simp [toUint] at h <;> simp
. apply ih _ _ h
. have h₁ := @toUint_lt _ a'; have h₂ := @toUint_ge _ b'; sorry_arith
. have h₁ := @toUint_ge _ a'; have h₂ := @toUint_lt _ b'; sorry_arith
. apply ih; sorry_arith
Proof state after:
no goals
Theorem: FinInt.eq_of_toUint_eq
Proof state before:
sz : ℕ
da : Bool
a' : FinInt sz
ih : ∀ (a b : FinInt (Nat.add sz 0)), toUint a = toUint b → a = b
b : FinInt (Nat.succ (Nat.add sz 0))
h : toUint (next da a') = toUint b
⊢ next da a' = b
Tactic:
cases b
Proof state after:
case next
sz : ℕ
da : Bool
a' : FinInt sz
ih : ∀ (a b : FinInt (Nat.add sz 0)), toUint a = toUint b → a = b
a✝¹ : Bool
a✝ : FinInt sz
h : toUint (next da a') = toUint (next a✝¹ a✝)
⊢ next da a' = next a✝¹ a✝
Theorem: FinInt.eq_of_toUint_eq
Proof state before:
sz : ℕ
da : Bool
a' : FinInt sz
ih : ∀ (a b : FinInt (Nat.add sz 0)), toUint a = toUint b → a = b
db : Bool
b' : FinInt sz
h : toUint (next da a') = toUint (next db b')
⊢ next da a' = next db b'
Tactic:
case next db b' =>
cases da <;> cases db <;> simp [toUint] at h <;> simp
. apply ih _ _ h
. have h₁ := @toUint_lt _ a'; have h₂ := @toUint_ge _ b'; sorry_arith
. have h₁ := @toUint_ge _ a'; have h₂ := @toUint_lt _ b'; sorry_arith
. apply ih; sorry_arith
Proof state after:
no goals
Theorem: FinInt.eq_of_toUint_eq
Proof state before:
sz : ℕ
da : Bool
a' : FinInt sz
ih : ∀ (a b : FinInt (Nat.add sz 0)), toUint a = toUint b → a = b
db : Bool
b' : FinInt sz
h : toUint (next da a') = toUint (next db b')
⊢ next da a' = next db b'
Tactic:
cases da <;> cases db <;> simp [toUint] at h <;> simp
Proof state after:
case false.false
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'

case false.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' = 2 ^ sz + toUint b'
⊢ False

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'
Theorem: FinInt.eq_of_toUint_eq
Proof state before:
case false.false
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'

case false.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' = 2 ^ sz + toUint b'
⊢ False

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:
. apply ih _ _ h
Proof state after:
case false.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' = 2 ^ sz + toUint b'
⊢ False

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'
Theorem: FinInt.eq_of_toUint_eq
Proof state before:
case false.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' = 2 ^ sz + toUint b'
⊢ False

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_lt _ a'; have h₂ := @toUint_ge _ b'; sorry_arith
Proof state after:
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'