The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi,
Several remarks:
1) Please give the complete file. Here you seem to be inside a section
(which is the problem, see below) but you did not give the context of
this section.

2) Sections do not work the way you think. Section variables are
considered as constants inside the section. This explains the strange
message you get.

Check eq_succ.
eq_succ
     : n = m -> S n = S m

See? n and m are not quantified in this statement (they will be only
after closing the section). To apply eq_succ you need EXACTLY the
hypothesis n=m, not just something of the form (foo=bar). Sine H0 has
not exactly this type you get the message:

Check (eq_succ H0).
The term "H0" has type "m = S m" while it is expected to have type "n = m".

My advice: don't use sections if you are a beginner: putting "forall n
m" in all your statements is much clearer.

3) I don't know what you are trying with the proof of le_to_eq_or_lt
but it probably needs rethinking. For the least: consider using
"destruct" instead of "induction" when you just need case splitting.
Using "rewrite" instead of "induction" is also probably a good idea.

Hope this helps.
Pierre

Le mar. 22 sept. 2020 à 08:47, Patricia Peratto
<psperatto AT vera.com.uy> a écrit :
>
> 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
>
>
>