Search code examples
coq

"if" is not just sugar for "match"

What is the difference between these two definitions:

Definition f : forall x:bool, if x then bool else nat :=
  fun x => match x with
           | true => true
           | false => 42
           end.
(* ^ Accepted by Coq *)

Definition g : forall x:bool, if x then bool else nat :=
  fun x => if x then true else 42.
(* ^ REJECTED *)

Before, I assumed that if is literally sugar for match but it seems that it is more restrictive when it comes to dependent pattern-matching, even though it also supports the return syntax anyway.

Is this intentional, and if so, what is the rule?

Solution

  • This looks like a bug to me: if you ask Coq to print f, it shows the match as an if.

    f = 
fun x : bool =>
if x as x0 return (if x0 then bool else nat) then true else 42
     : forall x : bool, if x then bool else nat

f is not universe polymorphic
Argument scope is [bool_scope]