The Coq mailing list

[Gregory Malecha <gmalecha AT gmail.com>]

Hi, Ralf --

I ran into something similar to this yesterday and came up with the following solution:

(** This is my 'Var' constructor **)

Var_ctx

     : forall (a : otype) (n : nat) (ls : list otype),

       List.nth_error ls n = Some a -> InCtx ls a

(** This tactic exposes the spine of a list **)

Ltac make_cons T n :=

  let rec go n :=

      lazymatch n with

      | 0 => uconstr:(@cons T _ _)

      | S ?Z =>

        let p := go Z in

        uconstr:(@cons T _ p)

      end

  in

  let z := go n in

  refine z.

(** Here is the notation that uses tactics-in-terms to call [make_cons] **)

Notation "# n" := (@Var_ctx _ n%nat ltac:(make_cons otype n) eq_refl) (at level 0) : ctx_scope.

Here, the [make_cons] tactic makes a list that exposes the spine, e.g. [make_cons nat 2] will produce (_ :: _ :: _ :: _). When Coq sees this, it can reduce the fixpoint to [Some _ = Some _] which [eq_refl] solves. Then, later is unifies (_ :: _ :: _ :: _) with this list.

On Fri, Mar 4, 2016 at 12:24 AM, Ralf Jung <jung AT mpi-sws.org> wrote:

Indeed, dependent name-based _expression_ may actually work out nicely :)

Kind regards,
Ralf

On 03.03.2016 23:16, Clément Pit--Claudel wrote:
> Very nice!
>
> On 03/03/2016 02:59 PM, Robbert Krebbers wrote:
>> Using some more type class magic I managed to let a "Hint Extern" generate "eq_refl" proofs. It even generates sensible error messages in case you are using variables that are not bound.
>>
>> ===========
>>
>> Require Import Decidable List String.
>> Open Scope string_scope.
>> Import ListNotations Sumbool.
>>
>> Definition in_dec := List.in_dec string_dec.
>> Definition in_dec_bool x X := proj1_sig (bool_of_sumbool (in_dec x X)).
>>
>> Class IsIn (x : string) (X : list string) :=
>>   is_in : in_dec_bool x X = true.
>> Hint Extern 0 (IsIn _ _) =>
>>   vm_compute; apply eq_refl : typeclass_instances.
>>
>> Inductive expr (X : list string) :=
>>   | Var (x : string) `{IsIn x X} : expr X
>>   | App : expr X -> expr X -> expr X
>>   | Lam (x : string) : expr (x :: X) -> expr X.
>>
>> Arguments Var {_} _ {_}.
>> Arguments App {_} _ _.
>> Arguments Lam {_} _ _.
>>
>> Coercion App : expr >-> Funclass.
>> Notation "# x" := (Var x) (at level 8, format "# x").
>> Notation "λ: x .. y , e" := (Lam x .. (Lam y e) ..)
>>   (at level 102, x, y at level 1, e at level 200).
>>
>> Definition test1 : expr nil :=
>>   λ: "x" "y" "z", #"z" #"x" (λ: "foo", #"foo" #"x").
>> Fail Definition test2 : expr nil :=
>>   λ: "x" "y" "z", #"z" #"x" (λ: "q" "foo", #"foo" #"bar").
>> (*
>> Unable to satisfy the following constraints:
>>
>> ?H2 : "IsIn "bar" ["foo"; "q"; "z"; "y"; "x"]"
>> *)
>> Definition test3 : expr ["bar"] :=
>>   λ: "x" "y" "z", #"z" #"x" (λ: "q" "foo", #"foo" #"bar").
>>
>> On 03/03/2016 10:30 PM, Robbert Krebbers wrote:
>>> 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
>>>>
>>
>

--

gregory malecha