internlm/Lean-Github huggingface dataset:
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
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
Tactic:
cases n
Proof state after:
case next
sz : ℕ
m : FinInt (sz + 1)
a✝¹ : Bool
a✝ : FinInt sz
h_nov :
  (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)).snd =
    false
h :
  toSint (next a✝¹ a✝ + m) =
    match next a✝¹ a✝, m with
    | next false n', next false m' =>
      match next a✝¹ a✝ + m with
      | next false a => toSint (next a✝¹ a✝) + toSint m
      | next true a => toSint (next a✝¹ a✝) + toSint m - 2 ^ (sz + 1)
    | next false n', next true m' => toSint (next a✝¹ a✝) + toSint m
    | next true n', next false m' => toSint (next a✝¹ a✝) + toSint m
    | next true n', next true m' =>
      match 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
⊢ toSint
      (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)).fst =
    toSint (next a✝¹ a✝) + toSint m
Theorem: FinInt.addv_toSint
Proof state before:
sz : ℕ
m : FinInt (sz + 1)
dn : Bool
n' : FinInt sz
h_nov :
  (match next dn n', m with
      | next false n'_1, next false m' =>
        match next dn n' + m with
        | next msb r' => (next msb r', msb)
      | next true n'_1, next true m' =>
        match next dn n' + m with
        | next msb r' => (next msb r', !msb)
      | x, x_1 => (next dn n' + m, false)).snd =
    false
h :
  toSint (next dn n' + m) =
    match next dn n', m with
    | next false n'_1, next false m' =>
      match next dn n' + m with
      | next false a => toSint (next dn n') + toSint m
      | next true a => toSint (next dn n') + toSint m - 2 ^ (sz + 1)
    | next false n'_1, next true m' => toSint (next dn n') + toSint m
    | next true n'_1, next false m' => toSint (next dn n') + toSint m
    | next true n'_1, next true m' =>
      match next dn n' + m with
      | next false a => toSint (next dn n') + toSint m + 2 ^ (sz + 1)
      | next true a => toSint (next dn n') + toSint m
⊢ toSint
      (match next dn n', m with
        | next false n'_1, next false m' =>
          match next dn n' + m with
          | next msb r' => (next msb r', msb)
        | next true n'_1, next true m' =>
          match next dn n' + m with
          | next msb r' => (next msb r', !msb)
        | x, x_1 => (next dn n' + m, false)).fst =
    toSint (next dn n') + toSint m
Tactic:
case next dn n' =>
cases m; case next dm m' =>
cases dn <;> cases dm <;> simp [h] at *
case false.false =>
match h: next false n' + next false m' with
| .next br r =>
rw [h] at h_nov
cases br <;> simp at *
rw [←h]; simp [add_toSint_msb]; simp [h]
case true.true =>
match h: next true n' + next true m' with
| .next br r =>
rw [h] at h_nov
cases br <;> simp at *
rw [←h]; simp [add_toSint_msb]; simp [h]
Proof state after:
no goals
Theorem: FinInt.addv_toSint
Proof state before:
sz : ℕ
m : FinInt (sz + 1)
dn : Bool
n' : FinInt sz
h_nov :
  (match next dn n', m with
      | next false n'_1, next false m' =>
        match next dn n' + m with
        | next msb r' => (next msb r', msb)
      | next true n'_1, next true m' =>
        match next dn n' + m with
        | next msb r' => (next msb r', !msb)
      | x, x_1 => (next dn n' + m, false)).snd =
    false
h :
  toSint (next dn n' + m) =
    match next dn n', m with
    | next false n'_1, next false m' =>
      match next dn n' + m with
      | next false a => toSint (next dn n') + toSint m
      | next true a => toSint (next dn n') + toSint m - 2 ^ (sz + 1)
    | next false n'_1, next true m' => toSint (next dn n') + toSint m
    | next true n'_1, next false m' => toSint (next dn n') + toSint m
    | next true n'_1, next true m' =>
      match next dn n' + m with
      | next false a => toSint (next dn n') + toSint m + 2 ^ (sz + 1)
      | next true a => toSint (next dn n') + toSint m
⊢ toSint
      (match next dn n', m with
        | next false n'_1, next false m' =>
          match next dn n' + m with
          | next msb r' => (next msb r', msb)
        | next true n'_1, next true m' =>
          match next dn n' + m with
          | next msb r' => (next msb r', !msb)
        | x, x_1 => (next dn n' + m, false)).fst =
    toSint (next dn n') + toSint m
Tactic:
cases m
Proof state after:
case next
sz : ℕ
dn : Bool
n' : FinInt sz
a✝¹ : Bool
a✝ : FinInt sz
h_nov :
  (match next dn n', next a✝¹ a✝ with
      | next false n'_1, next false m' =>
        match next dn n' + next a✝¹ a✝ with
        | next msb r' => (next msb r', msb)
      | next true n'_1, next true m' =>
        match next dn n' + next a✝¹ a✝ with
        | next msb r' => (next msb r', !msb)
      | x, x_1 => (next dn n' + next a✝¹ a✝, false)).snd =
    false
h :
  toSint (next dn n' + next a✝¹ a✝) =
    match next dn n', next a✝¹ a✝ with
    | next false n'_1, next false m' =>
      match next dn n' + next a✝¹ a✝ with
      | next false a => toSint (next dn n') + toSint (next a✝¹ a✝)
      | next true a => toSint (next dn n') + toSint (next a✝¹ a✝) - 2 ^ (sz + 1)
    | next false n'_1, next true m' => toSint (next dn n') + toSint (next a✝¹ a✝)
    | next true n'_1, next false m' => toSint (next dn n') + toSint (next a✝¹ a✝)
    | next true n'_1, next true m' =>
      match next dn n' + next a✝¹ a✝ with
      | next false a => toSint (next dn n') + toSint (next a✝¹ a✝) + 2 ^ (sz + 1)
      | next true a => toSint (next dn n') + toSint (next a✝¹ a✝)
⊢ toSint
      (match next dn n', next a✝¹ a✝ with
        | next false n'_1, next false m' =>
          match next dn n' + next a✝¹ a✝ with
          | next msb r' => (next msb r', msb)
        | next true n'_1, next true m' =>
          match next dn n' + next a✝¹ a✝ with
          | next msb r' => (next msb r', !msb)
        | x, x_1 => (next dn n' + next a✝¹ a✝, false)).fst =
    toSint (next dn n') + toSint (next a✝¹ a✝)
Theorem: FinInt.addv_toSint
Proof state before:
sz : ℕ
dn : Bool
n' : FinInt sz
dm : Bool
m' : FinInt sz
h_nov :
  (match next dn n', next dm m' with
      | next false n'_1, next false m'_1 =>
        match next dn n' + next dm m' with
        | next msb r' => (next msb r', msb)
      | next true n'_1, next true m'_1 =>
        match next dn n' + next dm m' with
        | next msb r' => (next msb r', !msb)
      | x, x_1 => (next dn n' + next dm m', false)).snd =
    false
h :
  toSint (next dn n' + next dm m') =
    match next dn n', next dm m' with
    | next false n'_1, next false m'_1 =>
      match next dn n' + next dm m' with
      | next false a => toSint (next dn n') + toSint (next dm m')
      | next true a => toSint (next dn n') + toSint (next dm m') - 2 ^ (sz + 1)
    | next false n'_1, next true m'_1 => toSint (next dn n') + toSint (next dm m')
    | next true n'_1, next false m'_1 => toSint (next dn n') + toSint (next dm m')
    | next true n'_1, next true m'_1 =>
      match next dn n' + next dm m' with
      | next false a => toSint (next dn n') + toSint (next dm m') + 2 ^ (sz + 1)
      | next true a => toSint (next dn n') + toSint (next dm m')
⊢ toSint
      (match next dn n', next dm m' with
        | next false n'_1, next false m'_1 =>
          match next dn n' + next dm m' with
          | next msb r' => (next msb r', msb)
        | next true n'_1, next true m'_1 =>
          match next dn n' + next dm m' with
          | next msb r' => (next msb r', !msb)
        | x, x_1 => (next dn n' + next dm m', false)).fst =
    toSint (next dn n') + toSint (next dm m')
Tactic:
case next dm m' =>
cases dn <;> cases dm <;> simp [h] at *
case false.false =>
match h: next false n' + next false m' with
| .next br r =>
rw [h] at h_nov
cases br <;> simp at *
rw [←h]; simp [add_toSint_msb]; simp [h]
case true.true =>
match h: next true n' + next true m' with
| .next br r =>
rw [h] at h_nov
cases br <;> simp at *
rw [←h]; simp [add_toSint_msb]; simp [h]
Proof state after:
no goals
Theorem: FinInt.addv_toSint
Proof state before:
sz : ℕ
dn : Bool
n' : FinInt sz
dm : Bool
m' : FinInt sz
h_nov :
  (match next dn n', next dm m' with
      | next false n'_1, next false m'_1 =>
        match next dn n' + next dm m' with
        | next msb r' => (next msb r', msb)
      | next true n'_1, next true m'_1 =>
        match next dn n' + next dm m' with
        | next msb r' => (next msb r', !msb)
      | x, x_1 => (next dn n' + next dm m', false)).snd =
    false
h :
  toSint (next dn n' + next dm m') =
    match next dn n', next dm m' with
    | next false n'_1, next false m'_1 =>
      match next dn n' + next dm m' with
      | next false a => toSint (next dn n') + toSint (next dm m')
      | next true a => toSint (next dn n') + toSint (next dm m') - 2 ^ (sz + 1)
    | next false n'_1, next true m'_1 => toSint (next dn n') + toSint (next dm m')
    | next true n'_1, next false m'_1 => toSint (next dn n') + toSint (next dm m')
    | next true n'_1, next true m'_1 =>
      match next dn n' + next dm m' with
      | next false a => toSint (next dn n') + toSint (next dm m') + 2 ^ (sz + 1)
      | next true a => toSint (next dn n') + toSint (next dm m')
⊢ toSint
      (match next dn n', next dm m' with
        | next false n'_1, next false m'_1 =>
          match next dn n' + next dm m' with
          | next msb r' => (next msb r', msb)
        | next true n'_1, next true m'_1 =>
          match next dn n' + next dm m' with
          | next msb r' => (next msb r', !msb)
        | x, x_1 => (next dn n' + next dm m', false)).fst =
    toSint (next dn n') + toSint (next dm m')
Tactic:
cases dn <;> cases dm <;> simp [h] at *
Proof state after:
case false.false
sz : ℕ
n' m' : FinInt sz
h_nov :
  (match next false n' + next false m' with
      | next msb r' => (next msb r', msb)).snd =
    false
h : True
⊢ toSint
      (match next false n' + next false m' with
        | next msb r' => (next msb r', msb)).fst =
    toSint (next false n') + toSint (next false m')

case true.true
sz : ℕ
n' m' : FinInt sz
h_nov :
  (match next true n' + next true m' with
      | next msb r' => (next msb r', !msb)).snd =
    false
h : True
⊢ toSint
      (match next true n' + next true m' with
        | next msb r' => (next msb r', !msb)).fst =
    toSint (next true n') + toSint (next true m')
Theorem: FinInt.addv_toSint
Proof state before:
sz : ℕ
n' m' : FinInt sz
h_nov :
  (match next false n' + next false m' with
      | next msb r' => (next msb r', msb)).snd =
    false
h : True
⊢ toSint
      (match next false n' + next false m' with
        | next msb r' => (next msb r', msb)).fst =
    toSint (next false n') + toSint (next false m')
Tactic:
case false.false =>
  match h: next false n' + next false m' with
  | .next br r =>
    rw [h] at h_nov
    cases br <;> simp at *
    rw [←h]; simp [add_toSint_msb]; simp [h]
Proof state after:
no goals
Theorem: FinInt.addv_toSint
Proof state before:
sz : ℕ
n' m' : FinInt sz
h_nov :
  (match next true n' + next true m' with
      | next msb r' => (next msb r', !msb)).snd =
    false
h : True
⊢ toSint
      (match next true n' + next true m' with
        | next msb r' => (next msb r', !msb)).fst =
    toSint (next true n') + toSint (next true m')
Tactic:
case true.true =>
  match h: next true n' + next true m' with
  | .next br r =>
    rw [h] at h_nov
    cases br <;> simp at *
    rw [←h]; simp [add_toSint_msb]; simp [h]
Proof state after:
no goals
Theorem: FinInt.addv_toSint
Proof state before:
sz : ℕ
n' m' : FinInt sz
h_nov :
  (match next false n' + next false m' with
      | next msb r' => (next msb r', msb)).snd =
    false
h : True
⊢ toSint
      (match next false n' + next false m' with
        | next msb r' => (next msb r', msb)).fst =
    toSint (next false n') + toSint (next false m')
Tactic:
match h: next false n' + next false m' with
| .next br r =>
  rw [h] at h_nov
  cases br <;> simp at *
  rw [←h]; simp [add_toSint_msb]; simp [h]
Proof state after:
no goals
Theorem: FinInt.addv_toSint
Proof state before:
sz : ℕ
n' m' : FinInt sz
h_nov :
  (match next false n' + next false m' with
      | next msb r' => (next msb r', msb)).snd =
    false
h✝ : True
br : Bool
r : FinInt sz
h : next false n' + next false m' = next br r
⊢ toSint
      (match next br r with
        | next msb r' => (next msb r', msb)).fst =
    toSint (next false n') + toSint (next false m')
Tactic:
rw [h] at h_nov
Proof state after:
sz : ℕ
n' m' : FinInt sz
h✝ : True
br : Bool
r : FinInt sz
h_nov :
  (match next br r with
      | next msb r' => (next msb r', msb)).snd =
    false
h : next false n' + next false m' = next br r
⊢ toSint
      (match next br r with
        | next msb r' => (next msb r', msb)).fst =
    toSint (next false n') + toSint (next false m')
Theorem: FinInt.addv_toSint
Proof state before:
sz : ℕ
n' m' : FinInt sz
h✝ : True
br : Bool
r : FinInt sz
h_nov :
  (match next br r with
      | next msb r' => (next msb r', msb)).snd =
    false
h : next false n' + next false m' = next br r
⊢ toSint
      (match next br r with
        | next msb r' => (next msb r', msb)).fst =
    toSint (next false n') + toSint (next false m')
Tactic:
cases br <;> simp at *
Proof state after:
case false
sz : ℕ
n' m' : FinInt sz
h✝ : True
r : FinInt sz
h : next false n' + next false m' = next false r
h_nov : True
⊢ toSint (next false r) = toSint (next false n') + toSint (next false m')
Theorem: FinInt.addv_toSint
Proof state before:
case false
sz : ℕ
n' m' : FinInt sz
h✝ : True
r : FinInt sz
h : next false n' + next false m' = next false r
h_nov : True
⊢ toSint (next false r) = toSint (next false n') + toSint (next false m')
Tactic:
rw [←h]
Proof state after:
case false
sz : ℕ
n' m' : FinInt sz
h✝ : True
r : FinInt sz
h : next false n' + next false m' = next false r
h_nov : True
⊢ toSint (next false n' + next false m') = toSint (next false n') + toSint (next false m')
Theorem: FinInt.addv_toSint
Proof state before:
case false
sz : ℕ
n' m' : FinInt sz
h✝ : True
r : FinInt sz
h : next false n' + next false m' = next false r
h_nov : True
⊢ toSint (next false n' + next false m') = toSint (next false n') + toSint (next false m')
Tactic:
simp [add_toSint_msb]
Proof state after:
case false
sz : ℕ
n' m' : FinInt sz
h✝ : True
r : FinInt sz
h : next false n' + next false m' = next false r
h_nov : True
⊢ (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)) =
    toSint (next false n') + toSint (next false m')
Theorem: FinInt.addv_toSint
Proof state before:
case false
sz : ℕ
n' m' : FinInt sz
h✝ : True
r : FinInt sz
h : next false n' + next false m' = next false r
h_nov : True
⊢ (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)) =
    toSint (next false n') + toSint (next false m')
Tactic:
simp [h]
Proof state after:
no goals
Theorem: FinInt.addv_toSint
Proof state before:
sz : ℕ
n' m' : FinInt sz
h_nov :
  (match next true n' + next true m' with
      | next msb r' => (next msb r', !msb)).snd =
    false
h : True
⊢ toSint
      (match next true n' + next true m' with
        | next msb r' => (next msb r', !msb)).fst =
    toSint (next true n') + toSint (next true m')
Tactic:
match h: next true n' + next true m' with
| .next br r =>
  rw [h] at h_nov
  cases br <;> simp at *
  rw [←h]; simp [add_toSint_msb]; simp [h]
Proof state after:
no goals
Theorem: FinInt.addv_toSint
Proof state before:
sz : ℕ
n' m' : FinInt sz
h_nov :
  (match next true n' + next true m' with
      | next msb r' => (next msb r', !msb)).snd =
    false
h✝ : True
br : Bool
r : FinInt sz
h : next true n' + next true m' = next br r
⊢ toSint
      (match next br r with
        | next msb r' => (next msb r', !msb)).fst =
    toSint (next true n') + toSint (next true m')
Tactic:
rw [h] at h_nov
Proof state after:
sz : ℕ
n' m' : FinInt sz
h✝ : True
br : Bool
r : FinInt sz
h_nov :
  (match next br r with
      | next msb r' => (next msb r', !msb)).snd =
    false
h : next true n' + next true m' = next br r
⊢ toSint
      (match next br r with
        | next msb r' => (next msb r', !msb)).fst =
    toSint (next true n') + toSint (next true m')
Theorem: FinInt.addv_toSint
Proof state before:
sz : ℕ
n' m' : FinInt sz
h✝ : True
br : Bool
r : FinInt sz
h_nov :
  (match next br r with
      | next msb r' => (next msb r', !msb)).snd =
    false
h : next true n' + next true m' = next br r
⊢ toSint
      (match next br r with
        | next msb r' => (next msb r', !msb)).fst =
    toSint (next true n') + toSint (next true m')
Tactic:
cases br <;> simp at *
Proof state after:
case true
sz : ℕ
n' m' : FinInt sz
h✝ : True
r : FinInt sz
h : next true n' + next true m' = next true r
h_nov : True
⊢ toSint (next true r) = toSint (next true n') + toSint (next true m')
Theorem: FinInt.addv_toSint
Proof state before:
case true
sz : ℕ
n' m' : FinInt sz
h✝ : True
r : FinInt sz
h : next true n' + next true m' = next true r
h_nov : True
⊢ toSint (next true r) = toSint (next true n') + toSint (next true m')
Tactic:
rw [←h]
Proof state after:
case true
sz : ℕ
n' m' : FinInt sz
h✝ : True
r : FinInt sz
h : next true n' + next true m' = next true r
h_nov : True
⊢ toSint (next true n' + next true m') = toSint (next true n') + toSint (next true m')
Theorem: FinInt.addv_toSint
Proof state before:
case true
sz : ℕ
n' m' : FinInt sz
h✝ : True
r : FinInt sz
h : next true n' + next true m' = next true r
h_nov : True
⊢ toSint (next true n' + next true m') = toSint (next true n') + toSint (next true m')
Tactic:
simp [add_toSint_msb]
Proof state after:
case true
sz : ℕ
n' m' : FinInt sz
h✝ : True
r : FinInt sz
h : next true n' + next true m' = next true r
h_nov : True
⊢ (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')) =
    toSint (next true n') + toSint (next true m')
Theorem: FinInt.addv_toSint
Proof state before:
case true
sz : ℕ
n' m' : FinInt sz
h✝ : True
r : FinInt sz
h : next true n' + next true m' = next true r
h_nov : True
⊢ (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')) =
    toSint (next true n') + toSint (next true m')
Tactic:
simp [h]
Proof state after:
no goals
Theorem: FinInt.neg_toUint
Proof state before:
sz : ℕ
n : FinInt sz
⊢ toUint (-n) = mod2 (-toUint n) sz
Tactic:
sorry
Proof state after:
no goals
Theorem: FinInt.neg_toUint_cong2
Proof state before:
sz : ℕ
n : FinInt sz
⊢ toUint (-n) ≡ -toUint n [2^sz]
Tactic:
simp [cong2, toUint_mod2]
Proof state after:
sz : ℕ
n : FinInt sz
⊢ toUint (-n) = mod2 (-toUint n) sz
Theorem: FinInt.neg_toUint_cong2
Proof state before:
sz : ℕ
n : FinInt sz
⊢ toUint (-n) = mod2 (-toUint n) sz
Tactic:
apply neg_toUint
Proof state after:
no goals
Theorem: FinInt.neg_minusOne
Proof state before:
sz : ℕ
⊢ -1 = minusOne
Tactic:
match H: sz with
| 0 => decide
| sz'+1 =>
    have h: sz' + 1 > 0 := by sorry_arith
    apply eq_of_toUint_cong2
    simp [toUint_minusOne]
    simp [neg_toUint]
    apply cong2_mod2_left
    simp [ofInt_1, toUint_one h]
    sorry_arith
Proof state after:
no goals
Theorem: FinInt.neg_minusOne
Proof state before:
sz : ℕ
H : sz = 0
⊢ -1 = minusOne
Tactic:
decide
Proof state after:
no goals
Theorem: FinInt.neg_minusOne
Proof state before:
sz sz' : ℕ
H : sz = Nat.succ sz'
⊢ -1 = minusOne
Tactic:
have h: sz' + 1 > 0 := by sorry_arith
Proof state after:
sz sz' : ℕ
H : sz = Nat.succ sz'
h : sz' + 1 > 0
⊢ -1 = minusOne
Theorem: FinInt.neg_minusOne
Proof state before:
sz sz' : ℕ
H : sz = Nat.succ sz'
h : sz' + 1 > 0
⊢ -1 = minusOne
Tactic:
apply eq_of_toUint_cong2
Proof state after:
case a
sz sz' : ℕ
H : sz = Nat.succ sz'
h : sz' + 1 > 0
⊢ toUint (-1) ≡ toUint minusOne [2^sz' + 1]
Theorem: FinInt.neg_minusOne
Proof state before:
case a
sz sz' : ℕ
H : sz = Nat.succ sz'
h : sz' + 1 > 0
⊢ toUint (-1) ≡ toUint minusOne [2^sz' + 1]
Tactic:
simp [toUint_minusOne]
Proof state after:
case a
sz sz' : ℕ
H : sz = Nat.succ sz'
h : sz' + 1 > 0
⊢ toUint (-1) ≡ 2 ^ sz' + (2 ^ sz' - 1) [2^sz' + 1]
Theorem: FinInt.neg_minusOne
Proof state before:
case a
sz sz' : ℕ
H : sz = Nat.succ sz'
h : sz' + 1 > 0
⊢ toUint (-1) ≡ 2 ^ sz' + (2 ^ sz' - 1) [2^sz' + 1]
Tactic:
simp [neg_toUint]
Proof state after:
case a
sz sz' : ℕ
H : sz = Nat.succ sz'
h : sz' + 1 > 0
⊢ mod2 (-toUint 1) (sz' + 1) ≡ 2 ^ sz' + (2 ^ sz' - 1) [2^sz' + 1]
Theorem: FinInt.neg_minusOne
Proof state before:
case a
sz sz' : ℕ
H : sz = Nat.succ sz'
h : sz' + 1 > 0
⊢ mod2 (-toUint 1) (sz' + 1) ≡ 2 ^ sz' + (2 ^ sz' - 1) [2^sz' + 1]
Tactic:
apply cong2_mod2_left
Proof state after:
case a.a
sz sz' : ℕ
H : sz = Nat.succ sz'
h : sz' + 1 > 0
⊢ (-toUint 1) ≡ 2 ^ sz' + (2 ^ sz' - 1) [2^sz' + 1]
Theorem: FinInt.neg_minusOne
Proof state before:
case a.a
sz sz' : ℕ
H : sz = Nat.succ sz'
h : sz' + 1 > 0
⊢ (-toUint 1) ≡ 2 ^ sz' + (2 ^ sz' - 1) [2^sz' + 1]
Tactic:
sorry_arith
Proof state after:
no goals
Theorem: FinInt.neg_minusOne
Proof state before:
sz sz' : ℕ
H : sz = Nat.succ sz'
⊢ sz' + 1 > 0
Tactic:
sorry_arith
Proof state after:
no goals
Theorem: FinInt.comp_eq_xor_minusOne
Proof state before:
sz : ℕ
n : FinInt sz
⊢ comp n = n ^^^ -1
Tactic:
simp [neg_minusOne, HXor.hXor]
Proof state after:
sz : ℕ
n : FinInt sz
⊢ comp n = xor n minusOne
Theorem: FinInt.comp_eq_xor_minusOne
Proof state before:
sz : ℕ
n : FinInt sz
⊢ comp n = xor n minusOne
Tactic:
induction sz <;> simp [comp, xor, logic1, logic2, minusOne] at *
Proof state after:
case zero
n : FinInt Nat.zero
⊢ logic1 (fun x => !x) n = logic2 (fun x x_1 => x != x_1) n nil

case succ
n✝ : ℕ
n_ih✝ : ∀ (n : FinInt n✝), logic1 (fun x => !x) n = logic2 (fun x x_1 => x != x_1) n minusOne
n : FinInt (Nat.succ n✝)
⊢ logic1 (fun x => !x) n = logic2 (fun x x_1 => x != x_1) n (I minusOne)
Theorem: FinInt.comp_eq_xor_minusOne
Proof state before:
n : FinInt Nat.zero
⊢ logic1 (fun x => !x) n = logic2 (fun x x_1 => x != x_1) n nil
Tactic:
case zero =>
  cases n; simp
Proof state after:
no goals
Theorem: FinInt.comp_eq_xor_minusOne
Proof state before:
sz : ℕ
ih : ∀ (n : FinInt sz), logic1 (fun x => !x) n = logic2 (fun x x_1 => x != x_1) n minusOne
n : FinInt (Nat.succ sz)
⊢ logic1 (fun x => !x) n = logic2 (fun x x_1 => x != x_1) n (I minusOne)
Tactic:
case succ sz ih =>
  match n with
  | .I m => simp [logic1, logic2, ih]
  | .O m => simp [logic1, logic2, ih]
Proof state after:
no goals
Theorem: FinInt.comp_eq_xor_minusOne
Proof state before:
n : FinInt Nat.zero
⊢ logic1 (fun x => !x) n = logic2 (fun x x_1 => x != x_1) n nil
Tactic:
cases n
Proof state after:
case nil

⊢ logic1 (fun x => !x) nil = logic2 (fun x x_1 => x != x_1) nil nil