Ssreflect Users Discussion List

[Benjamin Werner <>]

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 <