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