The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Cedric.Auger AT lri.fr
 wrote:
> Hi, i use this context:
>
> 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?
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>   
I believe that for this kind of need, you should rather use dependent 
inversion.

Yves