# Zulip Chat Archive

## Stream: new members

### Topic: Match on derived expression with equation compiler

#### Donald Sebastian Leung (Apr 08 2020 at 15:42):

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 (Apr 08 2020 at 15:50):

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 (Apr 08 2020 at 15:54):

Maybe `2 := (27 <= n)`

? But this is a Prop not a bool.

#### Kenny Lau (Apr 08 2020 at 15:54):

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

#### Kenny Lau (Apr 08 2020 at 15:54):

usually we use Prop rather than bool

#### Mario Carneiro (Apr 08 2020 at 21:58):

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 (Apr 09 2020 at 01:48):

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

construct.

Last updated: May 18 2021 at 16:25 UTC