1
$\begingroup$

I have a recursive function combine defined as following:

Fixpoint combine {X Y : Type} (lx : list X) (ly : list Y)
           : list (X*Y) :=
  match lx, ly with
  | [], _ => []
  | _, [] => []
  | x :: tx, y :: ty => (x, y) :: (combine tx ty)
  end.

Where list is defined as:

Inductive list (X:Type) : Type :=
  | nil
  | cons (x : X) (l : list X).

then I tried to define a lemma that looks like this:

Lemma list_nil_imply_combine_nil: forall {X: Type} (l: list X), 
  l = [] -> combine l [] = [].

but when executing the Lemma definition, Output says:

Cannot infer the implicit parameter Y of combine whose type is 
"Type" in environment:
X : Type
l : list X

I'm not sure how to correctly feed type arguments to [] i.e. nil constructor.. Any hint or direction for help material is appreciated!

$\endgroup$

2 Answers 2

2
$\begingroup$

Should your lemma rather read:

Lemma list_nil_imply_combine_nil: forall {X Y: Type} (l: list X), 
  combine l ([] : list Y) = [].

?

Anyway, a solution is to explicitly give the type of [], which is enough to help Coq find the type argument by itself:

Lemma list_nil_imply_combine_nil: forall {X Y: Type} (l: list X), 
  combine l ([] : list Y) = [].

Another is to feed the argument yourself, like so:

Lemma list_nil_imply_combine_nil: forall {X Y: Type} (l: list X), 
  combine l (@nil Y) = [].

The use of @ locally deactivates the implicit arguments, letting you give all arguments.

$\endgroup$
2
$\begingroup$

you need to type the nil :

Lemma list_nil_imply_combine_nil: forall {X Y : Type} (l: list X), 
  l = [] -> combine l ([] : list Y) = [].
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.