Cases on a Bool

Stream: lean4

[Brandon Brown]

I've defined the integers as a subtype that defines integers to be either zero or of the form pred^n zero or succ^n zero. I want to write a function that takes an arbitrary term of the base type and coerce it to the subtype by doing cases on whether the base int is already in normal form or not. So if it's in normal form, just package that as the int, and if not, just return zero packaged as an int.

inductive b_int : Type
| zero : b_int
| succ : b_int → b_int
| pred : b_int → b_int

open b_int

def is_norm (a : b_int) : Bool :=
match a with
| zero => true
| succ (pred a) => false
| pred (succ a) => false
| succ zero => true
| pred zero => true
| succ a => is_norm a
| pred a => is_norm a

def int := {x : b_int // is_norm x}

-- doesn't let me have access to proof that `is_norm x` when `c` is true
def b_int_to_int (x : b_int) : int := do
  let c := is_norm x
  if c then
    return ((Subtype.mk x rfl) : int) -- error
  else
    return ((Subtype.mk zero rfl) : int)

[Kyle Miller]

There's a special syntax to get the proof in an if statement:

def b_int_to_int (x : b_int) : int := do
  if c : is_norm x then
    return ((Subtype.mk x c) : int)
  else
    return ((Subtype.mk zero rfl) : int)

[Kyle Miller]

You can also use the angle bracket constructor notation:

def b_int_to_int (x : b_int) : int :=
  if c : is_norm x then
    return ⟨x, c⟩
  else
    return ⟨zero, rfl⟩

[Brandon Brown]

Awesome, thanks!