A fix to the consistency problem raised by Anthony Bordg

[bertot]

Dear all,

I would like to thank Anthony for exposing the weakness of the
implementation of higher inductive types that was proposed with the help
of private types. I discussed this problem with a few other researchers
and during a discussion with Benedikt Ahrens, it appeared that there
must be a fix, because there is not fundamental reason why the Agda
implementation of functions defined by cases should be that different
from the Coq implementation of pattern-matching.

The fix is to make sure that the use of non-zero arguments (or more
precisely, the lack of these use) is protected inside the
pattern-matching construct. Thus, the conversion mechanism of the type
theory does not see immediately that the variable is not used and is not
able to convert.

As an illustration, I will show what happens for the circle. Let's
start again with the definition of the circle as written in the HoTT
library. I only comment out the part that is faulty and write my
proposed fix on the next line.

(* start of a Coq excerpt *)
Module Export Circle.

Local Inductive S1 : Type :=
| base : S1.

Axiom loop : base = base.

Definition S1_rect (P : S1 -> Type) (b : P base) (l : loop # b = b)
: forall (x:S1), P x
:= fun x => (* match x with base => b end. -- this part is being fixed *)
match x return _ -> B x with fun _ => base => b end l.

Axiom S1_rect_beta_loop
: forall (P : S1 -> Type) (b : P base) (l : loop # b = b),
apD (S1_rect P b l) loop = l.

End Circle.

(* end of the Coq excerpt *)

Thus the pattern matching construct is not programmed to return a value
in P x, but to return
a function that will be applied to the constraint l. Thus, the
conversion algorithm can not
determine that l is not being used directly. Now, Anthony's proof is
not accepted anymore, as illustrated by the following attempt.


Definition S1_rect_eq : forall (B : S1 -> Type) (b : B base) (l k : loop
# b = b),
S1_rect B b l = S1_rect B b k.
intros B b l k.
Fail reflexivity.

To show that the function S1_rect behaves the same on l and k, one would
need to get rid of the pattern-matching construct. The way to get rid
of pattern matching construct is usually to reason by cases, but this is
forbidden by the private inductive type.

So in a sense, the solution is to chain beta expansions for all the
non-zero values provided to the recursor and inverse-lambda-lifting.

In the case of S1:

match x with base => b end

--- beta expansion on l --->

(fun l' => match x with base => b end) l

--- inverse lambda-lifting --->

match x with base => fun l' => b end l

And, since l' is not used, we can replace it with an underscore.

Again, thanks to Anthony and Benedikt for their questions and suggestions,

Yves

[Guillaume Brunerie]

Great, is it still as easy to use as before (for instance for stating
the computation rule for loop?)
And did you check that the proof of pi_1(S^1) still works?

By the way, I disagree with the following sentence:

> [There] is not fundamental reason why the Agda implementation of

> functions defined by cases should be that different from the Coq
> implementation of pattern-matching.

As far as I know, the implementation of pattern-matching in Agda is
very different from Coq, because functions defined by pattern matching
is a primitive notion in Agda.
Pattern matching is not syntactic sugar for the use of an eliminator
or for a match construct. In Agda a function defined by pattern
matching is never desugared to a single term, it is just stored as a
sequence of clauses according to the form of the patterns and it will
only reduce to an actual term when the function is applied to an
argument matching one of the patterns. So Agda can’t notice that the
two terms are equal given that there are no terms to compare.
Just to be clear I’m not saying that it’s better (the fact that
pattern matching can be reduced to eliminators is still an open
question), it’s just different and happens to change something in this
case.

Guillaume

> --
> You received this message because you are subscribed to the Google Groups
> "IAS Univalent Foundations" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to univalent-founda...@googlegroups.com.
> To post to this group, send email to univalent-...@googlegroups.com.
> Visit this group at
> http://groups.google.com/group/univalent-foundations?hl=en.
> For more options, visit https://groups.google.com/groups/opt_out.
>
>

[bertot]

On 11/4/13 3:07 PM, Guillaume Brunerie wrote:
> Great, is it still as easy to use as before (for instance for stating
> the computation rule for loop?)
> And did you check that the proof of pi_1(S^1) still works?

I just did. The answer is yes.

> By the way, I disagree with the following sentence:
>

I think I see what you mean. I am lucky that my misconception gave me
an idea for the fix, then.

Yves

[bertot]

On 11/4/13 2:47 PM, bertot wrote:
> Definition S1_rect (P : S1 -> Type) (b : P base) (l : loop # b = b)
> : forall (x:S1), P x
> := fun x => (* match x with base => b end. -- this part is being
> fixed *)
> match x return _ -> B x with fun _ => base => b end l.

As Anthony Bordg just pointed to me, this is wrong, it should be:

match x return _ -> B x with base => fun _ => b end l.

Sorry for this mistake.

Yves