[Agda] exercice of Peter Dybjer

[James Wood]

Hi Michel,

To add to what Jesper said, you can also note that subst is the
non-dependent eliminator of equality. Similarly to how any simple
function over lists defined by pattern matching can be rewritten using
foldr, any simple function matching on equality proofs can be rewritten
mechanically in terms of subst.

By “simple”, I mean that the result type does not depend on the value
being eliminated, and nothing too tricky is going on with respect to
totality checking (this doesn't matter anyway for things just involving
equality, because you're never doing anything recursive or corecursive).
In the case where you do have dependency on the equality proof being
eliminated (which is also a bit unusual, but comes up), you'd need the J
eliminator.

Regards,
James

On 22/03/2020 12:13, Jesper Cockx wrote:
> Hi Michel,
> 
> Here's a hint for sym: starting from `x ≡ y`, if you can prove that `P z
> = z ≡ x` holds for `z = x`, then you can use `subst` to prove that it
> also holds for `z = y`. For `trans`, there is a similar trick but now
> you need to choose `P` to be an implication between two identity types.
> 
> -- Jesper
> 
> 
> 
> On Sun, Mar 22, 2020 at 12:38 PM Michel Levy <michel.levy.imag at free.fr
> <mailto:michel.levy.imag at free.fr>> wrote:
> 
>     In the paper AgdaLectureNotes2018
>     <https://eur02.safelinks.protection.outlook.com/?url=http:%2F%2Fwww.cse.chalmers.se%2F~peterd%2Fpapers%2FAgdaLectureNotes2018.pdf&data=02%7C01%7Cjames.wood.100%40strath.ac.uk%7Cec5e2aa521e9417d91be08d7ce5a840a%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637204760886940338&sdata=Iue9XI2BrTiYoOPPNiLA9kk82CkKuG4fewKmkXNa2jg%3D&reserved=0>
>     of Peter Dybjer, there is this exercise page 19
> 
>     Exercise: prove symmetry and transitivity using subst but without
>     using pattern matching!
> 
>     I don't find the solution, can you help me to solve it ?
> 
>     -- 
>     courriel : michel.levy.imag at free.fr <mailto:michel.levy.imag at free.fr>
>     mobile : 06 59 13 42 53
>     web : michel.levy.imag.free.fr
>     <https://eur02.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmichel.levy.imag.free.fr%2F&data=02%7C01%7Cjames.wood.100%40strath.ac.uk%7Cec5e2aa521e9417d91be08d7ce5a840a%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637204760886950334&sdata=KM2TaT%2B%2BhB%2FExuJ19FF%2FbD94rmokOOOUgHBUFeVaJ2M%3D&reserved=0>
> 
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>     <https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&data=02%7C01%7Cjames.wood.100%40strath.ac.uk%7Cec5e2aa521e9417d91be08d7ce5a840a%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637204760886950334&sdata=kkdK5BLOn0duBGf35spZQFMGh7kwhLPv9YGeu61FCwM%3D&reserved=0>
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&data=02%7C01%7Cjames.wood.100%40strath.ac.uk%7Cec5e2aa521e9417d91be08d7ce5a840a%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637204760886970322&sdata=o%2BHXNEJ9eIC33S08AiR6%2B7wYM1eMcydBQJGY8XvDMSs%3D&reserved=0
>