[Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq

[Matthieu Sozeau]

Hi all,

On 8 janv. 2014, at 10:52, Altenkirch Thorsten =
<psztxa at exmail.nottingham.ac.uk> wrote:

> On 07/01/2014 23:03, "Conor McBride" <conor at strictlypositive.org> =
wrote:
>=20
>>=20
>> On 7 Jan 2014, at 22:47, Altenkirch Thorsten
>> <psztxa at exmail.nottingham.ac.uk> wrote:
>>=20
>>> Hi Conor,
>>>=20
>>> I am sure this must be a stupid question but why is this not covered
>>> by your result that pattern matching can be reduced to eliminators + =
K?
>>=20
>> The recursive call isn't covered by the inductive hypothesis. The =
direct
>> version
>> gives no account of the inductive hypothesis *at all*, hence the =
whole
>> mess.
>>=20
>>>>>> moo (wrap f) =3D noo (Zero -> WOne) myIso f
>>>>>> noo .WOne Refl x =3D moo x
>>=20
>> The recursive call
>>=20
>> moo x
>>=20
>> is really a recursive call
>>=20
>> moo (subst myIso ... f)
>>=20
>> but the inductive hypothesis tells us just that we can call moo on
>> outputs of f.
>>=20
>> Bottom line: it's not structurally recursive.
>=20
> I know this - this was precisely the comment I made in my reply to =
Maxime.
>=20
> However, it seems I am a victim of my own propaganda: I was always
> thinking that Conor's result tells us that we can replace pattern =
matching
> (with guarded recursion) by elimination constants.


>=20
> However, this example shows that this is not true. Once we perform the
> unification required by pattern matching we obtain a a term which =
"looks"
> as if it is structurally smaller even though it isn=A1=AFt


Pattern-matching and termination checking are still two different =
things,=20
especially in Coq where match and fix are separate constructs. However,
one could allow recursive calls on subst=A1=AFed arguments by providing =
a different
recursion eliminator (measures, general well-foundedness etc=A1=AD). You =
would just
have to find a well-founded order for which [subst (foo : Empty -> Box =
=A1=D4 Box) f <=3D f].

> One obvious question is how we can recognize good instances of pattern
> matching from bad ones.

Termination checking being undecidable I think that obligation to show =
it=A1=AFs
a =A1=B0good=A1=B1 pattern-matching has to be left to the user =
(providing as much
automation as we can without getting in her way of course). That=A1=AFs =
what
my Equations package does (it also implements Conor=A1=AFs et al =
elimination of=20
pattern-matching down to eliminators).=20

> This also increases the argument in favour of a safe version of =
pattern
> matching which is evidence producing. One of my new students, Gabe
> Dijkstra, is working on this - mainly triggered by the without-K =
issue.
> However, as we see now there are other issues which went unnoticed.

Indeed, "better be safe than sorry".

Cheers,
=A1=AA Matthieu