The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Sat, 14 Dec 2013 19:36:58 +0100 (CET),
Jacques-Henri Jourdan 
<jacques-henri.jourdan AT inria.fr>
 a écrit :

> Note that we can build a similar contradiction without using a
> pattern matching with no branches :
> 
> Require Import ClassicalFacts.
> 
> Inductive True1 : Prop := I1 : True1
> with True2 : Prop := I2 : True1 -> True2.
> 
> Section func_unit_discr.
>  
>  Hypothesis Heq : True1 = True2.
>  
>  Fixpoint contradiction (u : True2) : False :=
>  contradiction (
>      match u with
>        | I2 Tr =>
>           match Heq in (_ = T) return T with
>           | eq_refl => Tr
>           end
>      end).
>  
> End func_unit_discr.
> 
> Lemma foo : provable_prop_extensionality -> False.
> Proof.
>  intro; apply contradiction.
>  etransitivity. apply H. constructor.
>  symmetry. apply H. constructor. constructor.
>  constructor. constructor.
> Qed.
> 
> 
> I am not sure I have understood the tentative fix of Christine
> Paulin, but it seems like this would not solve this case either
> (True1 and True2 are in the same inductive definition. 
> 

I think there should clearly be a bug here.
When I first saw:

> Inductive True1 : Prop := I1 : True1
> with True2 : Prop := I2 : True1 -> True2.

I immediately thought "hey, this should not be marked as mutually
inductive, True simply depends on True1, but True1 does not depend on
True2".

So I removed the "with" and replaced it with a ". Inductive", but there
"contradiction" became rejected while original form is accepted. From my
point of view, such a diverging behavior should never occur.