Julin S (Dec 31 2021 at 17:24): Julin S (Dec 31 2021 at 17:24):I was trying an example from the CPDT book in here (under the 'Typed expressions' section) and made.
Require Import List.
Import ListNotations.
Inductive type : Set := Nat | Bool.
Definition typeDenote (t : type) : Set :=
match t with
| Nat => nat
| Bool => bool
end.
Definition tstack : Set := list type.
Fixpoint vstack (ts : tstack) : Set :=
match ts with
| []%list => unit
| (x::xs)%list => (typeDenote x * vstack xs)%type
end.
Inductive tbinop : type -> type -> type -> Set :=
| TPlus : tbinop Nat Nat Nat
| TMult : tbinop Nat Nat Nat
| TEq : forall (t : type), tbinop t t Bool
| TLt : tbinop Nat Nat Bool.
Inductive tinstr : tstack -> tstack -> Set :=
| TiNConst : forall (s : tstack), nat -> tinstr s (Nat::s)%list
| TiBConst : forall (s : tstack), bool -> tinstr s (Bool::s)%list
| TiBinop : forall (t1 t2 t : type) (s : tstack),
tbinop t1 t2 t -> tinstr (t2 :: t1 :: s)%list (t :: s)%list.
Inductive tprog : tstack -> tstack -> Set :=
| TNil : forall (s : tstack), tprog s s
| TCons : forall (s1 s2 s3 : tstack),
tinstr s1 s2 -> tprog s2 s3 -> tprog s1 s3.
Definition eqb (a b : bool) : bool := negb (xorb a b).
Definition tbinopDenote {t1 t2 t : type} (op : tbinop t1 t2 t)
: (typeDenote t1) -> (typeDenote t2) -> (typeDenote t) :=
match op with
| TPlus => plus
| TMult => mult
| TEq Nat => Nat.eqb
| TEq Bool => eqb
| TLt => Nat.ltb
end.
Fixpoint tinstrDenote {ts1 ts2 : tstack} (i : tinstr ts1 ts2) :
vstack ts1 -> vstack ts2 :=
match i with
| TiNConst _ n => fun s => (n, s)
| TiBConst _ b => fun s => (b, s)
| TiBinop _ _ _ _ op => fun s =>
let '(arg1, (arg2, s')) := s in
((tbinopDenote op) arg1 arg2, s')
end.
But at tinstrDenote, I got an error that I couldn't figure out:
In environment
tinstrDenote : forall ts1 ts2 : tstack,
tinstr ts1 ts2 -> vstack ts1 -> vstack ts2
ts1 : tstack
ts2 : tstack
i : tinstr ts1 ts2
t : tstack
n : nat
s : vstack ?t@{t1:=t}
The term "(n, s)" has type "(nat * vstack ?t@{t1:=t})%type"
while it is expected to have type "vstack ?t0@{t2:=Nat :: t}".
The books mentions that an error like this can appear if tinstrDenote was defined like
Fixpoint tinstrDenote {ts1 ts2 : tstack} (i : tinstr ts1 ts2) (vs : vstack ts1) : vstack ts2 :=
But such an error is still showing up.
How can this be fixed?
Gaëtan Gilbert (Dec 31 2021 at 17:53):you need to switch the arg1/arg2 order in (tbinopDenote op) arg1 arg2
not sure if coq could produce a better error here
Tomás Díaz (Dec 31 2021 at 20:08):just in case, in your definition of tinstr the TiBinop constructor has its args swapped:
[...] tinstr (t2 :: t1 :: s) (t :: s) instead of tinstr (t1 :: t2 :: s) (t :: s). If you use the latter, then everything should be ok after (I also swapped the args and was having the same issues as you lol)
Gaëtan Gilbert (Dec 31 2021 at 21:26):also if you make the return clause explicit you get a sane error
Definition tinstrDenote ts1 ts2 (i : tinstr ts1 ts2) : vstack ts1 -> vstack ts2 :=
match i in tinstr ts1 ts2 return vstack ts1 -> vstack ts2 with
| TiNConst _ n => fun s => (n, s)
| TiBConst _ b => fun s => (b, s)
| TiBinop _ op => fun s =>
let '(arg1, (arg2, s')) := s in
((tbinopDenote op) arg1 arg2, s')
end.
(* The term "arg1" has type "typeDenote t0" while it is expected to have type "typeDenote t". *)
Thanks. :smile:
Last updated: Sep 30 2023 at 07:01 UTC