The Coq mailing list

[Christine Paulin <Christine.Paulin AT lri.fr>]

On 12/14/2013 07:36 PM, Jacques-Henri Jourdan wrote:
> 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.

My proposition is to reject

 match Heq in (_ = T) return T with
          | eq_refl => Tr
          end

because of the elimination predicate (fun T => T) which is not related 
to the original inductive definition
but these examples show that we should be very careful in the 
justification when a match term is a proper subterm.

Christine

>