The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

You may be able to play some tricks with maximally inserted implicit arguments.  For example, I can define

Inductive list' {A : Type} : Type :=
  | nil' : list'
  | cons' : A -> list' -> list'.

However, Coq won't infer the hole if you instead type @list' _, so I'm not sure how useful this will be.  

-Jason

On Oct 9, 2012 12:28 PM, "AUGER Cédric" <sedrikov AT gmail.com> wrote:

Hi all, I think there is no real work around for my problem here, but I
still ask to the list.

Imagine, I have an AST, like this one:

Inductive exp : Type → Type :=
| Nat : nat → exp nat
| Bool : bool → exp bool
| Plus : exp nat → exp nat → exp nat
| If : exp bool → exp nat → exp nat → exp nat.

I find it cumbersome to have to deal with dependant types directly, so
I use parameters in stead of indice:

Inductive exp_ (T : Type) : Type :=
| Nat_ : T=nat → nat → exp_ T
| Bool_ : T=bool → bool → exp_ T
| Plus_ : T=nat → exp_ nat → exp_ nat → exp_ T
| If_ : T=nat → exp_ bool → exp_ nat → exp_ nat → exp_ T.

With that, I do not require inversion tactic any more (at least for
'exp_'), since there is no dependance. But inserting all these
equalities in the definition is ugly, the version with dependant types
is a lot nicer. So I wanted to trick Coq using notations.

Definition app (U : Type) : (Type → Type) → (Type → Type) :=
  λ p t, (U=t → p t).

Reserved Notation "[ e ∷ t ]". (* := (app t e _).*)

Inductive exp__ (T : Type) : Type :=
| Nat__ : nat → [exp__ ∷ nat] T
| Bool__ : bool → [exp__ ∷ bool] T
| Plus__ : exp__ nat → exp__ nat → [exp__ ∷ nat] T
| If__ : exp__ bool → exp__ nat → exp__ nat → [exp__ ∷ nat] T
where "[ e ∷ t ]" := (app t e).

This works, and I find it a lot better than exp_. But there are
trailing 'T's which seem rather strange. So I would rather write

Inductive exp__ (T : Type) : Type :=
| Nat__ : nat → [exp__ ∷ nat]
| Bool__ : bool → [exp__ ∷ bool]
| Plus__ : exp__ nat → exp__ nat → [exp__ ∷ nat]
| If__ : exp__ bool → exp__ nat → exp__ nat → [exp__ ∷ nat]
where "[ e ∷ t ]" := (app t e T).

but it does not work, since T is not known to the system at this place
(sad thing), and putting '_' instead of 'T' does not work either as
the type system is not able to infer it.

There are mainly two reasons, the first one is that it would require to
reduce "app" before finding that 'T' is the only possibility, and the
second one is that even in some basic case, such as "Inductive list
(A:Type) : Type := nil : list _ | cons : A → list A → list _." it does
not work even if the '_' cannot be filled with anything else than A.

Do you think some feature request should be sent, or do you have some
workaround ?