The Coq mailing list

[Georges Gonthier <gonthier AT microsoft.com>]

  Indeed, it would be, because nat enjoys decidable equality and hence UIP in nat is derivable (I believe this is in the FAQ).

In fact you will have to do so – there is no way to generate a correct elimination predicate for your example.

In ssreflect, you’d need to use rewrite eq_axiomK, which despite its name, is a theorem and not a system axiom.

(I’d missed that there were two occurrences of x when I first replied – ssreflect, and the dependent destruct of Coq 8.4 would both give error messages here, less precise but not quite as puzzling as that of destruct).

 

   Georges

 

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Valentin ROBERT
Sent: 17 February 2013 22:24
To: Georges Gonthier
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Abstracting leads to a term ill-typed… yet well-typed

 

Thank you for the answer. It is now clearer what the error is and should have been.

 

What term would ssreflect create to handle this example? Does it rely on eq_rect_eq?

 

It seems that I could just apply UIP_refl and happily rewrite e into Logic.eq_refl... Would that be fair to do?

 

Best regards,

- Valentin

 

On Sun, Feb 17, 2013 at 1:08 PM, Georges Gonthier <gonthier AT microsoft.com> wrote:

  This is just a case of misleading diagnostic. Indeed, the term is well-typed -- but it does have the type expected by the 'eq' eliminator.
That would start with fun (n0 : nat) (e : n = n0) => ... where the n is the variable introduced implicitly by your destruct e.
So what Coq is really saying is that the 'match' proof term it is trying to build to implement the destruct is ill-typed, but the diagnostic assumes the error is yours rather than the system's. The problem is that the Coq code for destruct tries to build dynamically the lambda-abstraction prefix from the current goal, by successively replacing the inductive family instance (e here) and its indices (n here) by variables. When this fails it is usually because some typing constraint of the original goal has been violated, hence the diagnostic. Here the error is somewhat silly because the tactic code just failed to generate the lambda abstraction it knew (from the declaration of eq) it had to come up with. If this annoys you, you can try using the ssreflect case: tactic, which will handle your example successfully.
  Cheers,
Georges

-----Original Message-----
From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of valentin.robert.42 AT gmail.com
Sent: 17 February 2013 18:40
To: coq-club AT inria.fr
Subject: [Coq-Club] Abstracting leads to a term ill-typed… yet well-typed

(Trying again, I might have been posting the previous one wrong, sorry if this ends up being a double-post...)

---

Hello Coq-club,

I posted this on StackOverflow but it seems to reach only a very limited audience, so this might be a better place.
cf.
http://stackoverflow.com/questions/14867685/abstracting-leads-to-a-term-ill-typed-yet-well-typed

---

I was stuck on a problem for a while, for which I derived a smaller standalone
example:

Axiom f : nat -> Set.

Goal forall (n : nat) (e : n = n) (x : f n),
  match e in _ = _n return f _n -> Prop with
  | Logic.eq_refl => fun v : f n => v = x
  end x.
Now, if you try to destruct e, you get the following error message:

Error: Abstracting over the terms "n0" and "e" leads to a term "fun (n0 : nat) (e : n0 = n0) =>  forall x : f n0,  match e in (_ = _n) return (f _n -> Prop) with  | Logic.eq_refl => fun v : f n0 => v = x  end x" which is ill-typed.
After scratching my head for a while, I couldn't figure out what was ill-typed in that term... So I tried this:

Definition illt :=
  fun (n : nat) (e : n = n) =>
  forall x : f n,
  match e in _ = _n return f _n -> Prop with
  | Logic.eq_refl => fun v : f n => v = x
  end x.
And Coq accepts it, at type forall n : nat, n = n -> Prop.

So, what is wrong with this error message, and how could I solve/tweak my initial goal?

Here is the Set Printing All versions of the error message:

Error: Abstracting over the terms "n0" and "e" leads to a term "fun (n0 : nat) (e : @eq nat n0 n0) =>  forall x : f n0,  match e in (@eq _ _ _n) return (f _n -> Prop) with  | eq_refl => fun v : f n0 => @eq (f n0) v x  end x" which is ill-typed.
It seems to be a well-typed term, and nothing is implicit.

Thank you,

- Valentin