The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

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
>>>
>

Attachment: signature.asc
Description: OpenPGP digital signature