The Coq mailing list

[vincent rahli <vincent.rahli AT gmail.com>]

Thanks a lot for your quick replies.

I forgot to mention that the version we're using is that one:
   https://github.com/HoTT/coq.

I should also have mentioned that that [try] in the proof script is really something
that one of our tactic tries.

One issue we're having now is that with these definitions tagged with [Polymorphic]
what was taking a few minutes to compile now takes several hours.

Is there a workaround that problem?

Thanks.
Vincent.

On Fri, Sep 6, 2013 at 5:01 AM, Matthieu Sozeau <matthieu.sozeau AT gmail.com> wrote:

On 6 sept. 2013, at 01:07, vincent rahli <vincent.rahli AT gmail.com> wrote:

> Hi,
>
> We're trying to use the HoTT branch of Coq (downloaded today) in order to get
> universe polymorphism.
>
> Unfortunately we keep on running into this error [Error: Universe inconsistency],
> which is the very error we were trying to avoid by using the HoTT branch of Coq.
>
> One of our problems is that [try] does not catch this error (see the code below).
>
>   - Why doesn't [try] catch that error?
>   - Why do we get a universe inconsistency error here and not
>     [Error: Unable to unify.] (without the [try])?

Hi,

  Indeed that version of unification didn't turn inconsistencies into unification
failures. The current development version [1] fixes this, I hope to push it to the
HoTT/coq repository soon. The proof goes through though if you avoid this step:

Proof.
induction sub; simpl; intros.
destruct H.

simpl in IHsub.
split; try right; (apply (IHsub vars);
destruct a, sub; [apply X| destruct p; apply X]).
Qed.

  Also, as a workaround, putting NTerm in [Set] where it naturally falls gets rid
of the inconsistency.

[1] git AT github.com:mattam82/coq.git branch univpolyproj

Best,
-- Matthieu

> Thanks.
> Vincent & Abhishek.
>
> -----------------------------------------------------------------------------------------
>
> Require Export Coq.Lists.List.
>
> Polymorphic Fixpoint LIn (A : Type) (a:A) (l:list A) : Type :=
>   match l with
>     | nil => False
>     | b :: m => (b = a) + LIn A a m
>   end.
>
> Polymorphic Inductive NTerm : Type :=
> | cterm : NTerm
> | oterm : list NTerm -> NTerm.
>
> Polymorphic Fixpoint dummy {A B} (x : list (A * B)) : list (A * B) :=
>   match x with
>     | nil => nil
>     | (_, _) :: _ => nil
>   end.
>
> Lemma foo :
>   forall v t sub vars,
>     LIn (nat * NTerm) (v, t) (dummy sub)
>     ->
>     (
>       LIn (nat * NTerm) (v, t) sub
>       *
>       notT (LIn nat v vars)
>     ).
> Proof.
>   induction sub; simpl; intros.
>   destruct H.
>   try (apply IHsub in X).
>