The Coq mailing list

[Tej Chajed <tchajed AT mit.edu>]

You’re not benefitting from Coq’s implicit arguments feature, which is like automatically passing _ for the argument. If you run [Set Implicit Arguments.] before creating your inductive types and definitions Coq will add some implicit arguments automatically, which often work well - CPDT does this to get usable implicit arguments.

Your original problem seems related to a Coq bug I ran into recently (bug 5142). In order to get a better error message for buggy dependent matches you need to explicitly annotate the match statement:

Fixpoint texpDenote t (e:texp t):typeDenote t:=
  match e in (texp t0) return (typeDenote t0) with
    |TNConst n=>n
    |TBConst b=>b
    |TBinop _ _ _ b e1 e2=>(tbinop b)(texpDenote e1)(texpDenote e2)
  end.

(* Error:
In environment
texpDenote : forall t : type, texp t -> typeDenote t
t : type
e : texp t
t0 : type
t1 : type
t2 : type
b : tbinop t0 t0 t2
e1 : texp t0
e2 : texp t1
The term "b" has type "tbinop t0 t0 t2" while it is expected to have type "type". *)

Unfortunately this return annotation is not inferred if the body has type errors, though it would be nice if it were based on the annotations on texpDenote.

​

On Tue, Oct 18, 2016 at 9:13 AM, Satrajit Roy <satrajit.roy AT gmail.com> wrote:

It seems like a version incompatibility though, doesn't it?

Now I must use ugly syntax like the  following:

 

Eval simpl in texpDenote _ (TNConst 42).
Eval simpl in texpDenote _ (TBConst true).
Eval simpl in texpDenote _ (TBinop _ _ _ TTimes (TBinop _ _ _ TPlus (TNConst 2)(TNConst 2))(TNConst 7)).
Eval simpl in texpDenote _ (TBinop _ _ _ (TEq Nat) (TBinop _ _ _ TPlus (TNConst 2) (TNConst 2))(TNConst 7)).
Eval simpl in texpDenote _ (TBinop _ _ _ TLt (TBinop _ _ _ TPlus (TNConst 2) (TNConst 2))(TNConst 7)).

 

I remember I executed parts of CPDT before and most things worked.

On Mon, Oct 17, 2016 at 4:43 PM, Satrajit Roy <satrajit.roy AT gmail.com> wrote:

Ahhh!!! Thank you so much!!

On Mon, Oct 17, 2016 at 4:18 PM, John Wiegley <johnw AT newartisans.com> wrote:

>>>>> "SR" == Satrajit Roy <satrajit.roy AT gmail.com> writes:

SR> My exposure to COQ is limited; so I'm possibly not seeing something
SR> obvious. Given the following definitions, why isn't the last one working?

After a few changes, this works. What you wrote failed to type check, not
because of the TNConst case, but because the type of the term you were
creating in the TBinop case was not the correct type, and this affected the
type expected for the TNConst case.

--8<---------------cut here---------------start------------->8---
Require Import Bool.Bool Arith List.

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
    |TNConst n=>n
    |TBConst b=>b
    |TBinop _ _ _ b e1 e2=> tbinopDenote _ _ _ b (texpDenote _ e1) (texpDenote _ e2)
  end.
--8<---------------cut here---------------end--------------->8---

--
John Wiegley                  GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com                          60E1 46C4 BD1A 7AC1 4BA2

--

Satrajit

--

Satrajit