The Coq mailing list

[Richard Dapoigny <richard.dapoigny AT univ-savoie.fr>]

Hi all,
I encounter some problem for unification in the theorem T6.
The environment is as follows :
****************************************************************
Class N   : Type.
Parameter pt : N -> N.
Parameter el : N -> N.

Definition epsilon := fun (A a:N) => { o:Kind | DenoteS A o /\ Denote a o}.
Definition singular_equality := fun A B => epsilon A B /\ epsilon B A.
Definition P001_isElementOf := fun A B:N => epsilon A (el B)
                                             <-> (singular_equality A B \/ isPartOf A B).
Class isPartOf (A B:N)        := ispart001      :> epsilon A (pt B).
Class isElementOf (A B:N) := isElem001     :> epsilon A (el B). 

Lemma L001 : forall A:N, epsilon A A -> singular_equality A A.
Proof.
intros A H1.
red; split; [ exact H1 | exact H1 ].
Qed.

Lemma L002 : forall P Q:Prop, P -> P \/ Q.
Proof.
intros H1 H2 H3.
left.
assumption.
Qed.

Lemma T5 : forall A b, epsilon A b -> epsilon A A.
Proof.
intros A a H0.
apply isEpsilon in H0.
decompose [and] H0.
clear H0.
destruct H.
replace x with A in H.
assumption.
admit.
Qed.

*****************************************
When I try solving the following theorem :

Lemma T6 : forall A a:N, epsilon A a -> isElementOf A A.
Proof.
intros A a H0.
apply T5 in H0.
apply L001 in H0.
apply L002 with (P:=singular_equality A A)(Q:=isPartOf A A) in H0.
unfold isElementOf.

I cannot unify the conclusion using P001_isElementOf while the type of H0 and the conclusion are equivalent.
Is somebody has an idea?

Thanks in advance.
Richard

--

begin:vcard
fn:Richard Dapoigny
n:Dapoigny;Richard
email;internet:richard.dapoigny AT univ-savoie.fr
tel;work:+33 450 09 65 29
tel;cell:+33 621 35 31 43
version:2.1
end:vcard