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?

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.)

I would like to add something,

working example of your code:

```
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.

@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?

@Natasha Klaus

coq not able to build term in

`Definition tbinopDenote`

, because term is not finished

Oh.. since stuff like `TEq`

and `TLt`

were mentioned, those too need to be handled at `tbinopDenote`

. That's it, right?

The error that I started out with was this:

```
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}".
*)
```

Couldn't figure why the error was showing up there.

@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").
*)
```

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

Ju-sh said:

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?

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).

Thanks @Kenji Maillard, I got a better idea now.

But I ran into new problems with the same example.

```
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?

But

`typeDenote Nat`

would give nat itself

the expected type is not `typeDenote Nat`

so that doesn't matter

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

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.

Last updated: Oct 13 2024 at 01:02 UTC