## Stream: Coq users

### Topic: ✔ Non-ugly proof of forall n : nat, 1 == n -> 1 = n

#### Philip B. (Feb 15 2022 at 15:49):

I am a Coq-newbie. I'm trying to prove some trivial things just for practice and to see what's possible to prove. In particular, I decided to learn how `bool` and `Prop` are related. To do that, I tried to prove `forall m n : nat, m == n -> m = n`, and while that seemed too difficult, I decided to prove a particular case `forall n : nat, 1 == n -> 1 = n`. I proved it but the proof is quite ugly:

``````Lemma one_eqn_impl_one_eq (n : nat) (one_eqn_n : is_true (1 == n)) : 1 = n.
Proof.
move: one_eqn_n.
elim: n.
- done.
- elim; done.
Qed.
``````

I don't like that I have to use `elim` inside `elim` in order to get to the assumption that `n` is at least 2. Is there a nicer way to prove this? I think it should be possible to do nicely without using tactics, by using `match n with | n'.+2 ...` but I couldn't figure it out. If someone shows me how to do that, I'll be glad. Also, if you show me how to match the case of n having the form `n'.+2` using tactics, that would be great as well.

#### Philip B. (Feb 15 2022 at 16:00):

After some more thinking I've realized that I have no idea how to prove `forall m n : nat, m == n -> m = n`. Give me a hint please.

#### Li-yao (Feb 15 2022 at 16:04):

Follow the definition of `==`. Is it a `Fixpoint`? then use `induction`. Does it use `match`? Then use `destruct`.

#### Pierre Jouvelot (Feb 15 2022 at 19:39):

Philip B. said:

I am a Coq-newbie. I'm trying to prove some trivial things just for practice and to see what's possible to prove. In particular, I decided to learn how `bool` and `Prop` are related. To do that, I tried to prove `forall m n : nat, m == n -> m = n`, and while that seemed too difficult, I decided to prove a particular case `forall n : nat, 1 == n -> 1 = n`. I proved it but the proof is quite ugly ...

If you're interested in this `bool/Prop` relation, you might want to look at the SSReflect proof language (https://hal.inria.fr/inria-00407778/document), where the intimate relationship between `bool` and `Prop` is a foundation of the proof technique called "reflection". In your case, the proof is one line:

``````Lemma one_eqn_impl_one_eq (n : nat) (one_eqn_n : is_true (1 == n)) : 1 = n.
Proof. exact/eqP. Qed.
``````

where the `/eqP` indicates that, by using this relation on the goal term `1 = n`, then the proof is done.

#### Philip B. (Feb 15 2022 at 19:50):

@Pierre Jouvelot I've started reading "Mathematical Components" by Mahboubi just today, it uses ssreflect too so it'll probably teach me ssreflect. I'll use your linked tutorial if I need another source. And thanks for pointing out `eqP` to me but I'm interested in figuring out how to do things like `match n with | n'.+1.+1.+1.+1` but in proof mode.

#### Théo Winterhalter (Feb 15 2022 at 19:59):

The `destruct` tactic uses intropatterns so you could do `destruct n as [| m]` so do a case analysis on `n`. You separate the cases by `|` and for each case, you list the variables. In the case of `0` there are none, and for the successor case there is one which I call `m`.
The thing is you can nest those and do

``````destruct n as [| [| m]].
``````

I'm not sure it really helps you though. And I don't know how people would do it using ssreflect.

#### Paolo Giarrusso (Feb 15 2022 at 20:21):

I think `case: n => [| [| m]].`? This (`[...|...]` is the one syntax that coincides between normal intro patterns and ssreflect introduction patterns.

#### Philip B. (Feb 15 2022 at 20:48):

That works. Nice. Where can I quickly read what all the tactics and tacticals used there do?

#### Philip B. (Feb 15 2022 at 20:53):

I am unfamiliar with `[...|...]` and also I don't know `=>` after `case` does.

#### Pierre Jouvelot (Feb 15 2022 at 20:59):

Paolo Giarrusso said:

I think `case: n => [| [| m]].`? This (`[...|...]` is the one syntax that coincides between normal intro patterns and ssreflect introduction patterns.

Another way would be a usual case analysis along the following line:

``````case le4n: (4 <= n).
- (* case when n = (n - 4) + 4 *)
- (* other case, i.e.,  n < 4 *)
``````

#### Enrico Tassi (Feb 15 2022 at 21:26):

Philip B. said:

That works. Nice. Where can I quickly read what all the tactics and tacticals used there do?

You can find it in the MathComp book you are reading, at chapter 4 (`eqP` is chapter 5)

#### Notification Bot (Feb 15 2022 at 21:29):

Philip B. has marked this topic as resolved.

#### Notification Bot (Feb 15 2022 at 21:29):

Philip B. has marked this topic as unresolved.

#### Notification Bot (Feb 15 2022 at 21:29):

Philip B. has marked this topic as resolved.

Last updated: Oct 01 2023 at 17:01 UTC