coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Fabian Kunze <kunze AT ps.uni-saarland.de>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Rewriting through coercions
- Date: Wed, 5 Dec 2018 14:41:49 +1300
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=kunze AT ps.uni-saarland.de; spf=Pass smtp.mailfrom=kunze AT ps.uni-saarland.de; spf=None smtp.helo=postmaster AT triton.rz.uni-saarland.de
- Ironport-phdr: 9a23:hAcSoRSLDuZmpNcbtpzS4o6Gqdpsv+yvbD5Q0YIujvd0So/mwa6yZBWN2/xhgRfzUJnB7Loc0qyK6/CmATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfbB/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/27ZisNyjKxVrhGvqQFhzYHIe4yaLuZyc7nHcN8GWWZMXMBcXDFBDIOmaIsPCvIMM+ZCoIbmplsBtx2+DhSpCuPyzD9Jh2H51rA93uQiDAHG2g0hEMwVvXTMt9X5LroSUea0zKXR1jXMdelZ2S356IfSdBAuvOuAUq9ufsfIz0QkCg3LjlKVqYP/PjOV0PwAs3Wd7+phS+KjknUnqwRqrTS1yMcskJHFho0SylDD+iV5xJg6KcekR058ZN6pFoZbuSKCN4ZuX88vTW5ltDw+x7AHo5K2fjIGxIonyhLHdfCLb4yF7gjgWeuROzt0mXNodbOlixqv80Wty+vxXdSu3llQtCpKiNzMu2gN1xPN7siHTeNw/lu72TaOywDT7edELVoulavaMZIh37gwlpsKvUTYBCD5gl/2jKuMeUUi5+ek8fnobav+qp+dMY97lB3+P7wzlsGxDuk0KAwDUmmB9em+zrHv4030TK1PjvIsk6nZtJ7aJd4cpq68GwJV0Zsj6xC+Dji4y9kYhWIHIEhYeBKBjojlIkrOL+riAvelh1SjijFryO3cMrL8HJrBNmLDn6v5fbZh905czxI+wsxY55JNE70OPPbzWlLqu9HDFR84Mwm0w/79B9ln14MeX3iPAq6DP6/Iv1+I/LFnH+7Zb4gM/T35NvIN5vj0jHZ/l0VOU7Ou2M45YXq5F/IuAFifc3ek1tQcF3UHlhIlCvHsiRiZWDdJY3+0U+Qw62doW8qdEY7fS9X10/S61yChE8gOPzEUOhW3CX7tMr68dbIJYSOWLNVml2ZcB6C6DZIn1FS1vQbgz7NhIqzY939B7M6x5J1O/+TW0CoK23lsFc3HizOVVCdpmGJNXDY/xqR2p0A7xlrRifEl0cwdLsRa4rZyail/NZPYyLYlWczoWx7GeJGTWhC7RNTjGjg4VNY4xdNIb0svQ9g=
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 ε AHaving 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/
- [Coq-Club] Rewriting through coercions, richard Dapoigny, 12/03/2018
- Re: [Coq-Club] Rewriting through coercions, Fabian Kunze, 12/05/2018
Archive powered by MHonArc 2.6.18.