The Coq mailing list

[t x <txrev319 AT gmail.com>]

Thanks for the detailed explaination on (1) it was failing and (2) how the hints is resolving it.

On Wed, Aug 14, 2013 at 9:49 AM, Valentin Robert <valentin.robert.42 AT gmail.com> wrote:

In this context:

T : Type
ls1 ls2 : list T
tup1 : tuple ls1
tup2 : tuple ls2
v : f t
concat {ls1 ls2 : list T} : tuple ls1 -> tuple ls2 -> tuple (ls1 ++ ls2)

When you write:
concat tup1 (v, tup2)

It is not obvious to Coq that "(v, tup2)" is a "tuple ls2" for some "ls2":

The term "(v, tup2)" has type "(f t * tuple ls2)%type" while it is
expected to have type "tuple ?1997".

Now, you can tell Coq for which ls2 this is supposed to work, by
explicitly supplying the implicit argument ls2, using the syntax:

concat (ls2 := t :: ls2) tup1 (v, tup2)

Note that the two occurences of ls2 mean two different things: the
first one refers to an implicit argument of concat that we try to
instantiate explicitly, while the second one is the ls2 in your
context. So this says: for the implicit argument named ls2 in concat,
use the value "t :: ls2".

Now Coq is able to check that "(v, tup2)" indeed has type "tuple (t ::
ls2)", since the latter reduces to (f t * tuple ls2), which is the
type of (v, tup2).

- Valentin

On Wed, Aug 14, 2013 at 9:28 AM, Beta Ziliani <beta AT mpi-sws.org> wrote:
> Hi, without looking into the details, yes, the (x := y) notation is to set
> (implicit) argument x to y.
>
>
> On Wed, Aug 14, 2013 at 3:26 AM, t x <txrev319 AT gmail.com> wrote:
>>
>> With apologies for spamming, the following (
>> https://gist.github.com/anonymous/4d7e55a5aabbf8e2f001 ) seems to imply it's
>> a way to set the implicit "ls2" argument of the concat function.
>>
>> If someone could confirm this understanding is correct, I'd appreciate it.
>>
>> Thanks!
>>
>>
>> On Wed, Aug 14, 2013 at 1:14 AM, t x <txrev319 AT gmail.com> wrote:
>>>
>>> Hi,
>>>
>>>   What is happening at
>>> https://gist.github.com/anonymous/6227214#file-util-v-L342 ?
>>>
>>>   In particular, I'm confused about:
>>>
>>>   "(ls2 := t :: ls2)"
>>>
>>>   The proof goes through on Coq -- so clearly it works and I'm in the
>>> wrong, but I don't understand what I'm misunderstanding. Here's what I know:
>>>
>>>   (x: T)
>>>   (ls2: list T)
>>>   (ls1: list T)
>>>
>>>   and I understand the Fixpoints/Theorems defined earlier in the file.
>>> However, I don't understand what is going on with:
>>>
>>>   "(concat (ls2 := t :: ls2) tup1 (v, tup2))"
>>>
>>>   In particular, the "ls2 := t :: ls2" part makes no sense to me:
>>>
>>>   (1) how can this ever be satisfied?
>>>   (2) why do make this assignment since ls2 isn't used anywhere else?
>>>
>>> Thanks!
>>
>>
>