[Newbie] Error involving curly braces · Coq users

Hi. I had been trying out an example for the CPDT book by Adam Chlipala but ran into an error that I couldn't understand. Could someone help me figure it out?

Inductive type : Set := Nat | Bool.

Inductive tbinop : type -> type -> type -> Set :=
| TPlus : tbinop Nat Nat Nat
| TTimes : tbinop Nat Nat Nat
| TEq: forall t, tbinop t t Bool
| TLt: tbinop Nat Nat Bool.

Inductive texp : type -> Set :=
| TNConst : nat -> texp Nat
| TBConst : bool -> texp Bool
| TBinop t1 t2 t : tbinop t1 t2 t -> texp t1 -> texp t2 -> texp t.

Definition typeDenote (t :type) : Set :=
  match t with
  | Nat => nat
  | Bool => bool
  end.

Definition tbinopDenote arg1 arg2 res (b : tbinop arg1 arg2 res)
  : typeDenote arg1 -> typeDenote arg2 -> typeDenote res :=
  match b with
  | TPlus => plus
  end.

(* ERROR:

In environment
arg1 : type
arg2 : type
res : type
b : tbinop arg1 arg2 res
The term "Nat.add" has type "nat -> nat -> nat"
while it is expected to have type
 "typeDenote ?t@{a1:=Nat} ->
  typeDenote ?t0@{a2:=Nat} -> typeDenote ?t1@{r0:=Nat}".
*)

The ? means an implicit argument, right? What does the curly brackets mean? And why were more variable names like t0 and t1 created?

Guillaume Melquiond (Sep 03 2021 at 06:44):

No, the question mark does not necessarily mean implicit. It just denotes an unknown term. And what is between brackets is what this unknown term is allowed to use. For example, ?t@{a1:=Nat} could be as simple as just a1 (or Nat), but it could not be a2, since a2 does not occur between brackets. As for t0 and t1, those are presumably the names used by Coq to denote the arguments of the type of b. Indeed, arg1, arg2, and res are not constant over all the branches of match b, they depend on the actual constructor. For instance, with TPlus, res is Nat, but with TLt, res is Bool. So, Coq provides a new variables to encompass all these constants. (In that simple case, it could just have been reusing res rather than creating a new variable.)

Natasha Klaus (Sep 03 2021 at 07:10):

Require Import Bool Arith.

Inductive type : Set := Nat | Bool.

Inductive tbinop : type -> type -> type -> Set :=
| TPlus : tbinop Nat Nat Nat
| TTimes : tbinop Nat Nat Nat
| TEq: forall t, tbinop t t Bool
| TLt: tbinop Nat Nat Bool.

Inductive texp : type -> Set :=
| TNConst : nat -> texp Nat
| TBConst : bool -> texp Bool
| TBinop t1 t2 t : tbinop t1 t2 t -> texp t1 -> texp t2 -> texp t.

Definition typeDenote (t :type) : Set :=
  match t with
  | Nat => nat
  | Bool => bool
  end.

Definition tbinopDenote arg1 arg2 res (b : tbinop arg1 arg2 res)
  : typeDenote arg1 -> typeDenote arg2 -> typeDenote res :=
  match b with
  | TPlus => plus
  | TTimes => mult
  | TEq Nat => beq_nat
  | TEq Bool => eqb
  | TLt => leb
  end.

Looks like coq is not able to build term in Definition tbinopDenote, because term is not finished.

Julin S (Sep 03 2021 at 09:37):

@Guillaume Melquiond So does ?t@{a1:=Nat} mean that t is allowed to be either a1 or Nat? Or is it that only a1 but where a1 is of type Nat?

What if other values are also possible? How would coq show that as? Something like ?t@{a1,a2:=Nat} if a1 and a2 are possible values?

Julin S (Sep 03 2021 at 09:41):

Oh.. since stuff like TEq and TLt were mentioned, those too need to be handled at tbinopDenote. That's it, right?

Require Import Arith.  (* beq_nat *)
Require Import Bool.  (* eqb *)

Inductive type : Set := Nat | Bool.

Inductive tbinop : type -> type -> type -> Set :=
| TPlus : tbinop Nat Nat Nat
| TTimes : tbinop Nat Nat Nat
| TEq: forall t, tbinop t t Bool
| TLt: tbinop Nat Nat Bool.

Inductive texp : type -> Set :=
| TNConst : nat -> texp Nat
| TBConst : bool -> texp Bool
| TBinop t1 t2 t : tbinop t1 t2 t -> texp t1 -> texp t2 -> texp t.

Definition typeDenote (t :type) : Set :=
  match t with
  | Nat => nat
  | Bool => bool
  end.

Definition tbinopDenote arg1 arg2 res (b : tbinop arg1 arg2 res)
  : typeDenote arg1 -> typeDenote arg2 -> typeDenote res :=
  match b with
  | TPlus => plus
  | TTimes => mult
  | TEq Nat => beq_nat
  | TEq Bool => eqb
  | TLt => le
  end.

(*
In environment
arg1 : type
arg2 : type
res : type
b : tbinop arg1 arg2 res
The term "Init.Nat.add" has type "nat -> nat -> nat"
while it is expected to have type
 "typeDenote ?t@{a1:=Nat} ->
  typeDenote ?t0@{a2:=Nat} -> typeDenote ?t1@{r0:=Nat}".
*)

Kenji Maillard (Sep 03 2021 at 09:49):

@Ju-sh your original error is due to a type mismatch on the last line TLt => le, you can see it if you are explicit about the dependent pattern match:

Definition tbinopDenote arg1 arg2 res (b : tbinop arg1 arg2 res)
  : typeDenote arg1 -> typeDenote arg2 -> typeDenote res :=
  match b in tbinop arg1 arg2 res
        return typeDenote arg1 -> typeDenote arg2 -> typeDenote res with
  | TPlus => plus
  | TTimes => mult
  | TEq Nat => beq_nat
  | TEq Bool => eqb
  | TLt => le
  end.
(*
Error:
In environment
arg1 : type
arg2 : type
res : type
b : tbinop arg1 arg2 res
The term "le" has type "nat -> nat -> Prop" while it is expected to have type
 "typeDenote Nat -> typeDenote Nat -> typeDenote Bool" (cannot unify
"Prop" and "typeDenote Bool").
*)

Kenji Maillard (Sep 03 2021 at 09:50):

And coq does not give you the right error because it rightfully fails to infer a type for the pattern match with this type error

Kenji Maillard (Sep 03 2021 at 09:55):

No, it means that t should be an arbitrary term in a context a1 : type (so it can only use that variable), and moreover in that branch a1 is defined to be Nat. If Coq was able to assign t := a1, t0 := a2 and t1 := r0 then everything would be fine for that branch because nat -> nat -> nat and

typeDenote Nat ->
  typeDenote Nat -> typeDenote Nat

would end up convertible. But it cannot do this assignment because of a type error in the following branches of the match (and Coq does not "know" where this failure comes from so it just bails out with the first branch mismatching).

Julin S (Sep 04 2021 at 14:22):

Require Import Bool Arith List.

(*Set Implicit Arguments.*)
(*Set Asymmetric Patterns.*)

Inductive type : Set := Nat | Bool.

Inductive tbinop : type -> type -> type -> Set :=
| TPlus : tbinop Nat Nat Nat
| TTimes : tbinop Nat Nat Nat
| TEq : forall t, tbinop t t Bool
| TLt : tbinop Nat Nat Bool.

Inductive texp : type -> Set :=
| TNConst : nat -> texp Nat
| TBConst : bool -> texp Bool
| TBinop : forall t1 t2 t, tbinop t1 t2 t -> texp t1 -> texp t2 -> texp t.

Definition typeDenote (t : type) : Set :=
  match t with
    | Nat => nat
    | Bool => bool
  end.

Definition tbinopDenote arg1 arg2 res (b : tbinop arg1 arg2 res)
  : typeDenote arg1 -> typeDenote arg2 -> typeDenote res :=
  match b with
    | TPlus => plus
    | TTimes => mult
    | TEq Nat => beq_nat
    | TEq Bool => eqb
    | TLt => leb
  end.

Fixpoint texpDenote t (e : texp t) : typeDenote t :=
  match e with
    (* Doubt1: How does [Set Implicit Arguments] affect the following line? *)
    | TNConst n => n
    | TBConst b => b

   (* Doubt2: How does [Set Asymmetric Patterns] affect the following line? *)
    | TBinop _ _ _ b e1 e2 => (tbinopDenote b) (texpDenote e1) (texpDenote e2)
  end.

If I remove the Set Implicit Arguments, the definition of texpDenote would complain:

In environment
texpDenote : forall t : type, texp t -> typeDenote t
t : type
e : texp t
n : nat
The term "n" has type "nat" while it is expected to have type
 "typeDenote ?t@{t1:=Nat}".

But typeDenote Nat would give nat itself, right? And n is nat. So why is this causing an error?

Gaëtan Gilbert (Sep 04 2021 at 14:38):

you need to do something like match e in texp t' return typeDenote t' with ...

Asymmetric Patterns only matters when there are parameters to an inductive type which is not the case here
Implicit Arguments should not affect TNCons/TBConst, but does affect TBinop

Meven Lennon-Bertrand (Sep 06 2021 at 08:46):

Again, Coq is misleading you here. It tries to infer the return clause of your pattern-matching, but fails to do so because of an unrelated error. If you do the modification @Gaëtan Gilbert suggested, the error message is much better: The term "b" has type "tbinop t0 t1 t2" while it is expected to have type "type".. This tells you that when deactivating implicit arguments, you need to pass more arguments to tbinopDenote, namely those that are not implicit. A working last line would be

| TBinop _ _ _ b e1 e2 => (tbinopDenote _ _ _ b) (texpDenote _ e1) (texpDenote _ e2)

and once you’ve got it right, Coq can infer the correct return type and you can drop the return clause of your match.

Stream: Coq users

Topic: [Newbie] Error involving curly braces

Julin S (Sep 03 2021 at 05:53):