[Agda] Vec _ n cong by n
p.capriotti at gmail.com
Thu Jun 20 12:02:24 CEST 2013
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.
More information about the Agda