The Coq mailing list

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

Hi,

I have some question about rewriting while some coercions have been set. Some are working, others not.

Here is a minimal fragment to assess the problem.

Universe Name.

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.

...

Class el :Type@{Name} := mkEl { el01  : particular }.
Variable  c04 : el -> plural. Coercion c04 : el >-> plural.

Axiom isElement  : forall (elB:el)(A B:particular), A ε elB <-> Eq_name B (@el01 elB) \/ forall ptB:part, Eq_name (@el01 elB)(@pt01 ptB) /\ A ε ptB.

Class klass : Type@{Name}  := mkKlass {
    k01  : name;
    k02  : exists B:particular, B ε k01 }.

(* Klass sous-type des particulars *)
Variable c07 : klass -> particular. Coercion c07 : klass  >-> particular.

Then in order to prove the following theorem :

Lemma Th10 : forall (A:particular)(a:plural)(klA:klass), A ε a -> Eq_name A (@k01 klA) -> A ε klA.
Proof.
intros A a kA H H'.
rewrite isKlass.
split.
- intros B H1 el1 H2.
  apply (isElement el1 B A).
  left.
  symmetry.
  exact H2.
- intros B elA elB H2.
  destruct H2 as [H2 H3].
  destruct H3 as [H3 H4].
  exists elA, elB.
  split.
    + rewrite <-H'.
     rewrite H2.

===================================================================

the message is: Found no subterm matching "c02 el01" in the current goal.

with hypotheses :

A : particular
a : plural
kA : klass
H : A ε a
H' : Eq_name A k01
B : particular
elA, elB : el
H2 : Eq_name el01 A
H3 : B ε elA
H4 : Eq_name el01 B
______________________________________(1/1)
el01 ε A

Having some idea about this message while c02 el01 has the right type?

Thanks in advance.

--
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/