[Agda] Vec _ n cong by n

[Paolo Capriotti]

On Thu, Jun 20, 2013 at 9:43 AM, Sergei Meshveliani <mechvel at botik.ru> wrote:
> On Wed, 2013-06-19 at 20:16 +0200, Jesper Cockx wrote:
>> I'm sorry, I didn't realize you were not familiar with inaccessible
>> (dotted) patterns. There are other ways to define this function (for
>> example by using the rewrite keyword), but dotted patterns are the
>> most basic. Dotted patterns are a really useful technique when writing
>> any program in agda with dependent types, and you shouldn't be afraid
>> of them ;) You can use them whenever the types force a variable into a
>> unique value (not very precise, but a good way to think about it). In
>> this case, pattern matching on |xs|=n forces n to be equal to (length
>> xs), hence the inaccessible pattern.
>> [..]
>
> I thank you and Francesco for helpful remarks.
>
> I knew the meaning of dotted patterns, but decided to avoid them --
> while possible, and see further. I have forgotten of them, and now was
> not able to use them in this concrete example.
>
> Further, I have a feeling that something is strange in the Language.
> Suppose that a type
>                      Foo a
>
>   depends on  a : C,  A : Setoid,  C = Carrier A,
>   the equivalence  p : a \~~ b   is proved,
>   f : Foo a  is built,
>   and we need to return  f : Foo b,
>   and also somehow to express that  f : Foo a  can be replaced with
>   f : Foo b    if  a \~~ b.
>
> Can this be expressed in Agda ?

No, you can't prove this for any dependent type `Foo`. If it is true in your
particular case, you will need to prove it specifically for that.

To see why it's not true in general, pick any `a : C`, and define

    Foo : C → Set
    Foo x = a ≡ x

Now, if you had:

    cong≈ : (a ≈ b) → Foo a → Foo b

you could prove:

    discr : (b : C) → a ≈ b → a ≡ b
    discr b p = cong≈ p refl

which, abstracted on `a`, would imply that `A` is discrete.

Paolo