Ssreflect Users Discussion List

[Georges Gonthier <>]

  Indeed, the error message is probably due to the special case. In ssreflect, doing case on an equality tries to project equality along constructor arguments, using the same primitive as Ltac’s injection tactic. This can’t work in your case, since the goal depends on the equality proof.

To do dependent elimination on an equality you need to invoke the dependent form of case:

  case: false / e1 (or case: _  / e1 if you are a lazy typist)

Even this won’t work (but with a decent error message), as in eliminating e1 one generalizes only the second occurrence of false in

  @eq (@eq bool false false) e1 e2

and also the type of e2 depends on that occurrence. You actually need to use the rather contrived

   case: {2 4}false / e1 in e2 *

to generalize over e2 as well (and the second occurrence of false in its type as well.

  As Benjamin points out, this ugly step doesn’t really help you, because you won’t be able to eliminate e2 in

  erefl false = e2

without generalizing erefl false back into e1. There is a workaround for this, which is encapsulated in the proof of eqtype/eq_irrelevance (it’s just 5 lines!).

   As for the obscure error message, I suspect it comes directly from the injection primitive, because we probably fail to check for dependencies before invoking it. I guess we should do that (and perhaps switch to the dependent elimination code in that case, though in your example that would also have given you an longer obscure error message).

   Georges

 

From: Benjamin Werner [mailto:]
Sent: 23 October 2013 08:55
To: Frédéric Chyzak
Cc:
Subject: Re: case: returns blank error message

 

Not about the error message but :

 

Proving that equality proofs are equal cannot be done in general in Coq's type theory.

(whether this is good, is bad, is a minor defect of the type theory, etc is another story).

Here your lemma is true because equality is decidable over the considered type (boolean).

 

In SSR, this is proved generally for eqtypes by the lemma eq_irrelevance.

 

Benjamin

 

 

Le 23 oct. 2013 à 09:11, Frédéric Chyzak <> a écrit :

Hi,

 

Maybe I am in a special case of case: (applied to equalities), but I would expect a more informative error message.

 

Frédéric

 

 

 

 

$ coq/bin/coqtop -I coqfinitgroup

Welcome to Coq 8.4pl2 (June 2013)

 

Coq < Require Import ssreflect.

 

Small Scale Reflection version 1.4 loaded.

Copyright 2005-2012 Microsoft Corporation and INRIA.

Distributed under the terms of the CeCILL-B license.

 

[Loading ML file ssreflect.cmxs ... done]

 

Coq < Lemma foo (e1 e2 : false = false) : e1 = e2.

1 subgoal

e1 : false = false

e2 : false = false

============================

e1 = e2

 

foo < case: e1.

Toplevel input, characters 0-8:

> case: e1.

> ^^^^^^^^

Error:

 

foo <