The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

I managed to get this working with type classes, see below. Only now, 
instead of having an eq_refl for the proof, you have something that type 
class search generates and which can thus become rather big.

Require Import Decidable List String.
Open Scope string_scope.

Implicit Type (x : string).
Implicit Type (X : list string).

Class IsIn (x : string) (X : list string) := is_in : In x X.
Instance is_in_here x X : IsIn x (x :: X). now left. Qed.
Instance is_in_further x y X : IsIn x X -> IsIn x (y :: X). now right. Qed.

Inductive expr X : Type :=
  | Var x `{IsIn x X} : expr X
  | App : expr X -> expr X -> expr X
  | Lam x : expr (x::X) -> expr X.

Arguments Var {_} _ {_}.
Arguments App {_} _ _.
Arguments Lam {_} _ _.

Definition test2 : expr nil :=
  Lam "x" (Lam "y" (App (Var "x") (Var "y"))).

On 03/03/2016 09:26 PM, Ralf Jung wrote:
> Hi everybody,
>
> I am trying to use dependent types to represent the free variables of a
> deeply embedded language that uses names for binders -- and I am running
> into some trouble.
> Yeah, I know that "dependent types" and "names for binders" are asking
> for trouble. The point is, we actually want to be able to read the
> programs we are writing in that deeply embedded language, an deBruijn
> indices are rather cryptic. And we need to keep track of whether the
> terms are closed, hence the dependent types. This actually worked out
> much better than I anticipated, but there still is a serious problem.
>
> The concrete problem we are having is that, if we omit all the type
> annotations you want to omit, then Coq fails to type-check the term even
> though there is a pretty straight-forward well to add the missing types.
> For example:
>
> ------ BEGIN ------
> Require Import Decidable List String.
> Import ListNotations Sumbool.
> Open Scope string_scope.
> Obligation Tactic := fail.
>
> Implicit Type (x : string).
> Implicit Type (X : list string).
>
> Definition in_dec := List.in_dec string_dec.
> Definition in_dec_bool x X := proj1_sig (bool_of_sumbool (in_dec x X)).
>
> Inductive expr X : Type :=
>    (* We don't use lists in our actual code, but that doesn't matter.
>       What matters is that the proof obligation on variables is something
>       that can be discharged by "eq_refl". *)
> | Var x : in_dec_bool x X = true -> expr X
> | App : expr X -> expr X -> expr X
> | Lam x : expr (x::X) -> expr X.
>
> (* This works, but having to state the context in which the
>     variable is checked is silly. *)
> Definition test1 : expr nil :=
>    Lam _ "x" (Var ["x"] "x" eq_refl).
> (* Omitting the context fails. *)
> Fail Definition test2 : expr nil :=
>    Lam _ "x" (Var _ "x" eq_refl).
> (* With Program, it works. *)
> Program Definition test3 : expr nil :=
>    Lam _ "x" (Var _ "x" eq_refl).
> --------- END --------------
>
> The comments explain the problem. The "test2" fails with:
>
> > The term "eq_refl" has type "in_dec_bool "x" ?l0 = in_dec_bool "x" ?l0" while 
> > it is expected to have type
> >   "in_dec_bool "x" ?l0 = true".
>
> It seems that Coq starts unifying too early or in the wrong order. If it
> would just propagate the X downwards, it would notice that the first "_"
> can only be "nil", and the second "_" can only be "[x]", and "eq_refl"
> actually works.
>
> Using "Program Definition", we can write this down; but this is rather
> annoying because Program cannot be used everywhere. Also, in the full
> language, we have some trouble with "Program" generating obligations to
> prove some equalities, even though the "eq_refl" should be enough --
> which means the terms end up containing more and different proofs than
> they should. I have not yet tried to reproduce this in the simple
> example, since we'd rather avoid "Program" altogether.
>
> Is there some way to make Coq typecheck "test2"; preferably something
> that's consistent enough so we could hide it behind the notation that we
> use anyway to write these programs?
>
> Kind regards,
> Ralf