Stream: Coq users

Topic: ✔ Error in typeDenote function

Julin S (Dec 23 2021 at 09:22):

I was trying a simple example from the beginning of Chlipala's CPDT book like

Inductive type : Set := Nat | Bool.

Inductive tbinop : type -> type -> type -> Set :=
| TPlus : tbinop Nat Nat Nat
| TMult : tbinop Nat Nat Nat
| TEq : forall (t : type), tbinop t t Bool
| TLe : tbinop Nat Nat Bool.

Definition eqb (a b : bool) : bool := negb (xorb a b).

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

Definition tbinopDenote {t1 t2 t : type} (op : tbinop t1 t2 t) : (typeDenote t1) -> (typeDenote t2)->  (typeDenote t) -> Set :=
  match op with
  | TPlus => Nat.add
  | TMult => mult
  | TEq Nat => Nat.eqb
  | TEq Bool => eqb
  | TLe => Nat.ltb
  end.

But I got an error at the first pattern (any pattern actually. Had tried chaning the order patterns) of tbinopDenote.

In environment
t1 : type
t2 : type
t : type
op : tbinop t1 t2 t
The term "Nat.add" has type "nat -> nat -> nat"
while it is expected to have type
 "typeDenote ?t@{t5:=Nat} ->
  typeDenote ?t0@{t6:=Nat} -> typeDenote ?t1@{t7:=Nat} -> Set".

I thought stuff like ?t@{t5:=Nat} meant that there is a value t whose possible value is Nat. But if that was so, it's the only possibility and coq would've inferred it so I guess I'm wrong about that.

How can this error be fixed?

Gaëtan Gilbert (Dec 23 2021 at 09:29):

I thought stuff like ?t@{t5:=Nat} meant that there is a value t whose possible value is Nat

no, it means there is a value t which can use the variable t5 and is used with t5 set to Nat
so both ?t := t5 and ?t := Nat would work
in this case coq is smart enough to pick the first one, but your type is wrong because you put -> Set

Julin S (Dec 23 2021 at 09:35):

Ah.. I hadn't noticed the type was different.. :sweat_smile: :grimacing:

it means there is a value `t` which can use the variable `t5` and is used with `t5` set to `Nat`

So t5 is just a placeholder? ?t@{t5:=Nat} could also be just ?t@{Nat}?

Gaëtan Gilbert (Dec 23 2021 at 09:38):

we don't print the accessible variables when they're the same as the ones in the context so it's really ?t@{t1:=t1;t5:=Nat}

Gaëtan Gilbert (Dec 23 2021 at 09:39):

you can see it with Set Printing Existential Instances.

Julin S (Dec 23 2021 at 10:03):

Thanks.

Notification Bot (Dec 23 2021 at 10:03):

Ju-sh has marked this topic as resolved.

Last updated: Oct 13 2024 at 01:02 UTC