CODEWITHSUNDEEP
coq
pedroabreu
pedroabreu

Reputation: 61

Using List remove function

I'm trying to use the list remove function in Coq standard library but it asks for a bizarre typing and I don't know how to solve.

The function I'm implementing is to make a list of free variables in a lambda term as follows:

Fixpoint fv (t : trm) : vars :=
  match t with
    | Var v => [v]
    | App t1 t2 => (fv t1) ++ (fv t2)
    | Abs x t' => remove x (fv t')
  end.

And it gives me the following error:

Error: In environment
fv : trm -> vars
t : trm
x : nat
t' : trm
The term "x" has type "nat" while it is expected to have type
 "forall x0 y : ?171, {x0 = y} + {x0 <> y}".

I'm pretty sure there is something to do with that hyphotesis thing in the definition of the remove function. I have no idea how to deal with it though, any helps?

Upvotes: 4

Views: 918

Answers (1)

Ptival
Ptival

Reputation: 9437

remove is defined in a context containing:

Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}.

The function removes takes this as a first argument (which you can see by doing Print remove.)

This hypothesis is a function deciding equality of elements of the type in your list. In your case, you will have to provide a function to decide equality of var (which seems to be nat, so there is probably such a function in the standard library too).

If you do not know the "{p} + {q}" notation, you can look it up here: http://coq.inria.fr/library/Coq.Init.Specif.html#sumbool

Upvotes: 4

Related Questions