coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: e+coq-club AT x80.org (Emilio Jesús Gallego Arias)
- To: Kiarash Rahmani <rahmank AT purdue.edu>
- Cc: "coq-club\@inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Equality in the assumptions
- Date: Tue, 01 Mar 2016 02:23:12 +0100
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=e+coq-club AT x80.org; spf=Neutral smtp.mailfrom=e+coq-club AT x80.org; spf=None smtp.helo=postmaster AT jiboia.ensmp.fr
- Ironport-phdr: 9a23:Cc2ZJB8qalHyBP9uRHKM819IXTAuvvDOBiVQ1KB92+McTK2v8tzYMVDF4r011RmSDdqdtaMP0LqempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXsq3G/pQQfBg/4fVIsYL+lRciM3o/sh6ibwN76XUZhvHKFe7R8LRG7/036l/I9ps9cEJs30QbDuXBSeu5blitCLFOXmAvgtI/rpMYwuwwZgf8q9tZBXKPmZOx4COUAVHV1e1wyse7qvAPKVgvH3HIcV2wQk1IcGQHF6Rj8Xb/przH2q+c71SWHa57YV7cxDDnh5KByDRTslS0vJ25htmbNhYQwoadapBOm7z5y2BzPKK6cMP5zcaSVVMkbTHEADZUZbDBIHo7pN9hHNOEGJ+sN6tCl/1Y=
- Organization: X80 Heavy Industries
Hey Kiarash,
Kiarash Rahmani
<rahmank AT purdue.edu>
writes:
> I am stuck in the middle of a proof. Here is a toy example to explain
> it:
As other have pointed out, your example may not be the best; given that
is easy to prove.
A comment on your code thou:
> Inductive my_ind (a b:my_type) : my_type -> Prop :=
> | cons_introl :forall x: my_type, b = one -> my_ind a b x
> | cons_intror :forall x: my_type, a = one -> my_ind a b x.
>
> Theorem my_theorem (a b c: my_type) (H : my_ind a b = my_ind b c) -> 2 = 2.
> (*How sould I make use of H? inversion, injection, unfold, does not
> seem to work*)
H looks a bit suspicious, it is a very strong equality and may be hard
to prove in the first place.
Note that in particular "forall x, my_ind a b x = my_ind b c x" doesn't
imply H unless you assume an axiom.
The converse is trivial, is that what you'd want?
Also, note that ("my_ind a b x") is an inhabitant of Prop, equality
between such objects may not be the most convenient to use.
Given what the nature of the "my_ind" relation, a boolean
characterization could result more convenient.
Best regards,
E.
- Re: [Coq-Club] Equality in the assumptions, Benoît Viguier, 03/01/2016
- <Possible follow-up(s)>
- Re: [Coq-Club] Equality in the assumptions, Vadim Zaliva, 03/01/2016
- Re: [Coq-Club] Equality in the assumptions, Emilio Jesús Gallego Arias, 03/01/2016
Archive powered by MHonArc 2.6.18.