The Coq mailing list

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

Hi all,

There is some problem when trying to rewrite in complex types. A fragment of code could help:

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).
...
Class Part: Type@{Name} := mkPart { pt01 : particular }.
Variable  c03 : Part -> plural. Coercion c03 : Part >-> plural.
Definition part (A:particular)    := mkPart A.

Axiom TransitivePart :  forall (A B C:particular), A ε part B -> B ε part C -> A ε part C.
Axiom AsymetricPart  : forall (A B :particular),  A ε part B -> ~(B ε part A).

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

Definition element (A:particular) := mkEl A.

Axiom isElement  : forall (A B:particular), A ε element B <-> eqpt A B \/ A ε part B.

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

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

Axiom isKlass : forall (A:particular)(a:name)( p1:exists B:particular, B ε a), A ε (klass a p1) <->
                      (forall B, B ε a -> B ε (element A)) /\  (forall (B:particular), B ε (element A) -> exists (C D:particular), (C ε a /\ D ε (element C) /\ D ε (element B))).

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

Now, when trying to rewrite within the following Lemma:

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).

the context is:

c07 : klass00 → particular
A : particular
a : name
H1 : ∃ B : particular, B ε a
H2 : ∃ B : particular, B ε klass a H1
C, D : particular
H5 : eqpt 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

The problem is that I can rewrite H5 (Leibniz-like equality) in the goal, but not in the hypothesis H0 du to the following message:

Syntax error: illegal begin of vernac. Abstracting over the term "c07 (klass a H1)" leads to a term λ p : particular, A ε klass p H2 which is ill-typed.
Reason is: Illegal application: The term "klass" of type  "∀ a : name, (∃ B : particular, B ε a) → klass00" cannot be applied to the terms  "c02 p" : "name"
 "H2" : "∃ B : particular, B ε klass a H1"
The 2nd term has type "∃ B : particular, B ε klass a H1" which should be coercible to "∃ B : particular, B ε p".

If somebody has an idea?

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/