Theorem: FinInt.eq_of_toUint_eq (MLIR/Util/FinInt.lean)

State before:
sz : ℕ
a b : FinInt sz
⊢ toUint a = toUint b → a = b
Tactic:
intros h <;> induction sz
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

State before:
a b : FinInt Nat.zero
h : toUint a = toUint b
⊢ a = b
Tactic:
case zero =>
  cases a; cases b; rfl
State after:
no goals

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
State after:
no goals

State before:
a b : FinInt Nat.zero
h : toUint a = toUint b
⊢ a = b
Tactic:
cases a
State after:
case nil
b : FinInt Nat.zero
h : toUint nil = toUint b
⊢ nil = b

State before:
case nil
b : FinInt Nat.zero
h : toUint nil = toUint b
⊢ nil = b
Tactic:
cases b
State after:
case nil.nil
h : toUint nil = toUint nil
⊢ nil = nil

State before:
case nil.nil
h : toUint nil = toUint nil
⊢ nil = nil
Tactic:
rfl
State after:
no goals

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
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

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
State after:
no goals

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
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✝

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
State after:
no goals

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
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'

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
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'

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
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'

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
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'

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
State after:
no goals