The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Le 3 sept. 08 à 12:20, Yves Bertot a écrit :

> Cedric.Auger AT lri.fr
>  wrote:
> > Hi, i use this context:

Hi,

> > Parameter A : Set.
> > Axiom A_dec : forall (a b : A), { a = b } + { a <> b }.
> > Parameter B : A -> Set.
> > Axiom B_dec : forall c (a b : B c), { a = b } + { a <> b }.
> > Inductive C : Set :=
> > C_of_B : forall a, B a -> C.
> >
> > and want to prove:
> >
> > Axiom C_struct : forall c (a b : B c), C_of_B c a = C_of_B c b -> a  
> > = b.
> >
> > to be able to decide equality over C:
> >
> > Lemma C_dec : forall (a b : C), { a = b } + { a <> b }.
> > Proof.
> > intros; destruct a; destruct b.
> > revert b; revert b0; destruct (A_dec a a0).
> > rewrite e; clear e; intros; destruct (B_dec a0 b0 b).
> >   rewrite e; left; reflexivity.
> >   right; intro; destruct n; apply C_struct; assumption.
> > intros; right; intro; inversion H; exact (n H1).
> > Qed.
> >
> > But inversion is not enough powerfull in the way i use it, is it  
> > known to
> > be impossible to prove it?

Rather, it is know to be provable in such a context because you have  
decidable equality on
the index type A.
<<
Require Import Eqdep_dec.

Lemma C_struct : forall c (a b : B c), C_of_B c a = C_of_B c b -> a = b.
Proof. intros. inversion H. apply inj_pair2_eq_dec with (P:=fun a => B  
a). apply A_dec. apply H1. Qed.
>>

-- Matthieu