coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] problem with goal and environment

From: Patricia Peratto <psperatto AT vera.com.uy>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] problem with goal and environment
Date: Sat, 19 Sep 2020 18:55:07 -0300 (UYT)
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=psperatto AT vera.com.uy; spf=Pass smtp.mailfrom=psperatto AT vera.com.uy; spf=None smtp.helo=postmaster AT mail.vera.com.uy
Dkim-filter: OpenDKIM Filter v2.9.0 mta02.in.vera.com.uy 5B11022213F
Ironport-phdr: 9a23:/ogw8h/lDVOPif9uRHKM819IXTAuvvDOBiVQ1KB20u4cTK2v8tzYMVDF4r011RmVBNqds6MP07Oe8/i5HzBZv9DZ6DFKWacPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3wOgVvO+v6BJPZgdip2OCu4Z3TZBhDiCagbb9oIxi6sAfcutMKjYZmJao91gbFqWZMd+hK2G9kP12ekwv968uq4JJv7yFcsO89+sBdVqn3Y742RqFCAjQ8NGA16szrtR3dQgaK+3ARTGYYnAdWDgbc9B31UYv/vSX8tupmxSmVJtb2QqwuWTSj9KhkVhnlgzoaOjEj8WHXjstwjL9HoB+kuhdyzZLYbJ2TOfFjeazTfdQaRXBaUcZQSiNOH52zb40NAeUcJ+ZTso3xqlsSoReiAAWhAv7kxD1ViX/sxaA03eQvHx/F0gMiAtwBv2jbrNTpNKoJS++50LXHwi7fY/9K3zr29YjGcgomofGJRb9+a9DeyVU1FwPEklqQqJbqNC6P2OsTqWiU9fZgVf6oi2U6rAxxuiOvxt8yhYnTnI0V1kzE9SJizYYrO9K4UlR0bcS4H5tXsiGWLZZ2Q8M7TmxupS00yaUGtIalcCQW1Jgr3RHSZ+Cdf4WG/x7vTumcLDZgiH54er+zmQy+/Vavx+HmWMS4zUxGoyRZntTKq3sD1xvT6tKcRft840iuxCiA1wbR5O5ZO0A5jaTVJZ4/zLAzlJUdrEvMETP3mEXql6KZbFko9fSz5Oj7frnqvpGSOY9qhA/9MKsgh8OwDvg5MggSRGWU4/iw26H48kHlXLlHiOA9nLPDv5DAP8sbo7a0Aw9L3YYn7BayFzKm384ZnXkDNl5FZgyIj5LzNF3UPP/4CvK/j06xkDZr3/zGP7vhDYvRLnXbjrvtYapx51RTxQYv19xS6Y9YBqsOLf/yQkPxscbXDh49Mwy62ebnD9B925sGWWKUGq+WLrnSvkWU5uIzJOmBf5EVtyjnK/c//fLhkXg5mVoHcam03ZobcGq4Eeh+I0WFfXrshc8MHnsNvgonVeDllFmCUSNIaHupRKI95jQ7CJq8AovZR4CthqaB3CahEZFMaGBGEAPELXC9fIKdHvwIdSjadsRmi3kPUaWrY44nzxCn8gHgnelJNO3RrxURqYji39l8r9Xejxgu6Ts8W9yGy2yXRn1omUsWSiU/mqt4pApg2wHQguBDn/VEGIkKtLtyWQAgOMuBl7QjV4LCHznZd9LMc26IB828CGhqHMw82dZIaEF4Xciz3EiajniaRoQNnrnOP6Qat6fV3nz/PcF4ki2UyqQ7hh8tRc4JKHz03/cipTiWPJbAlgCir4jvdakY23edpmKKzG7IokxCWUh7VqCDQGFNPkY=

I have the following definitions:

Theorem lt_n_S : (lt n (S n)).
unfold lt.
exact (le_n (S n)).
Qed.

Theorem eq_succ : (n=m) -> (S n = S m).
intro.
rewrite -> H.
reflexivity.
Qed.

I'm proving the following theorem:

Theorem le_to_eq_or_lt :
(le n m) -> (or(n=m) (lt n m)).
intro.
induction H.
apply or_introl.
reflexivity.
induction IHle.
induction H0.
induction H.
exact (or_intror lt_n_S).
induction IHle.

The following environment:

A, B : Prop
x, y, z : A
P : A -> Prop
f : A -> B
n, p, m : nat
H : le n m
H0 : m = S m
______________________________________(1/3)
S m = S (S m) \/ lt (S m) (S (S m))
______________________________________(2/3)
S m = S (S m) \/ lt (S m) (S (S m))
______________________________________(3/3)
n = S m \/ lt n (S m)

when I want to solve it with:

exact (or_introl (eq_succ H0)).

I get the following message:

In environment
A, B : Prop
x, y, z : A
P : A -> Prop
f : A -> B
n, p, m : nat
H : le n m
H0 : m = S m
The term "H0" has type "m = S m"
while it is expected to have type
"n = m".

There is something wrong.
The goal is (S m) = (S (S m)).

Regards,
Patricia

[Coq-Club] problem with goal and environment, Patricia Peratto, 09/19/2020
- Re: [Coq-Club] problem with goal and environment, Pierre Courtieu, 09/22/2020