Zulip Chat Archive

Stream: new members

Topic: Match on derived expression with equation compiler


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 08 2020 at 15:54):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 08 2020 at 15:54):

usually we use Prop rather than bool

view this post on Zulip 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)

view this post on Zulip 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