Match on derived expression with equation compiler

Stream: new members

[Donald Sebastian Leung]

So I was just looking into translating this nice little exercise in Coq into Lean and realized that I don't understand Lean's equation compiler at all.

In Coq, we can match on a derived expression of an argument as follows (example taken from that exercise):

Definition decide n : bool :=
  match n mod 5 with
  | 0 => false
  | 2 => 27 <=? n
  | 4 => 9 <=? n
  | _ => true
  end.

Basically, this means that, given a natural number n, we compute n mod 5 and then perform case analysis on this intermediate result (with the match expression). How do we do that using Lean's equation compiler? I quickly skimmed through the Induction and Recursion chapter of TPIL again but could not seem to find a similar example.

[Alex J. Best]

I don't know what <=? does but this compiles

def decide (n: ℕ) : bool :=
  match n % 5 with
  | 0 := false
  | 2 :=  true
  | 4 := true
  | _ := true
  end

  #eval decide 3

[Kevin Buzzard]

Maybe 2 := (27 <= n)? But this is a Prop not a bool.

[Kenny Lau]

def decide (n: ℕ) : Prop :=
match n % 5 with
| 0 := false
| 2 := 27 ≤ n
| 4 := 9 ≤ n
| _ := true
end

[Kenny Lau]

usually we use Prop rather than bool

[Mario Carneiro]

To write the equivalent of a <=? b you can use the coercion from Prop to bool:

def decide (n: ℕ) : bool :=
match n % 5 with
| 0 := ff
| 2 := 27 ≤ n
| 4 := 9 ≤ n
| _ := tt
end

#eval decide 12

Kenny's version using Prop is usually preferred, but in that case decidability is not for free anymore, you have to prove it by cases:

def decide (n : ℕ) : Prop :=
match n % 5 with
| 0 := false
| 2 := 27 ≤ n
| 4 := 9 ≤ n
| _ := true
end

instance (n : ℕ) : decidable (decide n) :=
by unfold decide; exact
match n % 5 with
| 0 := decidable.false
| 2 := nat.decidable_le _ _
| 4 := nat.decidable_le _ _
| 1 := decidable.true
| 3 := decidable.true
| (n+5) := decidable.true
end

#eval (decide 12 : bool)

[Donald Sebastian Leung]

Thanks, I didn't realize that Lean's equation compiler also provided a similar match construct.