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

[=?GB2312?B?TWF4aW1lIESopm6oqHM=?=]

Hello Conor,

In fact, I was wondering why the call to subst (which is defined by
pattern matching) destroys the proper subterm status, while it is not
the case for pattern matching. It does not seem very uniform, does it?

In Coq, a reduction step would replace subst by its body before
computing the size information.

I agree that elaboration is nice. However, sometimes you don't want to
pay the price for encoding things. In an ideal world, you could prove
the elaboration process correct, and extract a checker that is correct
by construction with respect to the target type theory you mention. Is
there any existing work in that direction?

Maxime.


On 01/07/2014 12:25 PM, Conor McBride wrote:
> Hi Maxime
>
> On 7 Jan 2014, at 16:56, Maxime D¨¦n¨¨s <mail at maximedenes.fr> wrote:
>
>> Still, I don't understand why replacing the pattern matching in my
>> example by a call to subst makes the termination check fail.
> A call to subst destroys the "proper subterm" status, whereas
> pattern matching naively preserves it.
>
>> Maxime.
>>> {-# OPTIONS --without-K #-}
>>>
>>> module BadWithoutK where
>>>
>>> data Zero : Set where
>>>
>>> data WOne : Set where
>>>  wrap : (Zero -> WOne) -> WOne
>>>
>>> data _<->_ (X : Set) : Set -> Set where
>>>  Refl : X <-> X
>>>
>>> postulate
>>>  myIso : WOne <-> (Zero -> WOne)
>>>
>>> moo : WOne -> Zero
>>> noo : (X : Set) -> (WOne <-> X) -> X -> Zero
>>>
>>> moo (wrap f) = noo (Zero -> WOne) myIso f
>>> noo .WOne Refl x = moo x
> moo's input is bigger than the third argument in its noo call
> noo's third input is the same as the argument in its moo call
>
> Size-change termination, how are ye?
>
> When you do the translation to eliminators, you're obliged to
> show how recursive calls correspond to invocations of the
> inductive hypothesis: here that's just not going to happen.
> Transporting f across myIso does indeed give an element of
> WOne (your Box), but that does not make a nullary inductive
> hypothesis any easier to invoke.
>
> I'd quite like to see us defining a type theory in which the
> only checking is type checking, then using it as a target for
> elaboration. Eliminators are one candidate, but there are
> others. Sized types are certainly another strong candidate.
> I'm also interested to see whether there are "locally clocked"
> explanations for termination, as there seem to be for
> productivity.
>
> Interesting times
>
> Conor