The Coq mailing list

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

Hi all,

I have some problem for rewriting under compound coercions as follows:

Variable name         : Type@{Name}.
Variable plural       : Type@{Name}.
Variable particular   : Type@{Name}.

Variable c01 : plural -> name. Coercion c01 : plural >-> name.
Variable c02 : particular -> name. Coercion c02 : particular >-> name.

Inductive eps :particular -> name -> Prop :=
 | particularEquality: forall(A:particular)(B:particular), eps A B
 | epsilon : forall(A:particular)(b:plural), eps A b.

Notation "A 'ε' b" := (eps A b)  (at level 40).

Definition Eq_name (a b:name) := @eq name a b.
Definition Eq_plur (a b:plural) := @eq plural a b.
Definition Eq_part (A B :particular) := @eq particular A B.

...

Class Klass: Type@{Name}  := mkKlass {
    k01  : name;
     k02  : exists B:particular, B ε k01 }.
Variable c07 : Klass -> particular. Coercion c07 : Klass  >-> particular.

Definition klass (a:name)(p1:exists B:particular, B ε a) := mkKlass a p1.

The problem appears when I try to rewrite in a compound term as follows:

Lemma Th27 : forall (A:particular)(a:name){p1:exists B:particular, B ε a}{p2:exists B:particular,
                                           B ε (klass a p1)}, A ε (klass (klass a p1) p2) -> A ε (klass a p1).

Hypotheses are:

c07 : Klass → particular
A : particular
a : name
H1 : ∃ B : particular, B ε a
H2 : ∃ B : particular, B ε klass a H1
C, D : particular
H5 : Eq_part C (klass a H1)
H6 : D ε element C ∧ D ε element A
H4 : A ε element A
H0 : A ε klass (klass a H1) H2
______________________________________(1/1)
A ε klass a H1

when i try to rewrite <-H5 in H0, the error is:  The 2nd term has type  "∃ B : particular, B ε klass a H1" which should be coercible to  "∃ B : particular, B ε p".

However (klass a H1) is of type Klass which is coerced to particular?

Thanks in advance,

Richard

--
Richard Dapoigny
Associate Professor - LISTIC Laboratory
University Savoie Mont-Blanc
5, chemin Bellevue
Po. Box 80439
Annecy-le-Vieux 74940
FRANCE
https://www.listic.univ-smb.fr/en/presentation-en/members/lecturers/richard-dapoigny-en/