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.

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.

Follow the definition of `==`

. Is it a `Fixpoint`

? then use `induction`

. Does it use `match`

? Then use `destruct`

.

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.

@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.

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.

I think `case: n => [| [| m]].`

? This (`[...|...]`

is the one syntax that coincides between normal intro patterns and ssreflect introduction patterns.

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

I am unfamiliar with `[...|...]`

and also I don't know `=>`

after `case`

does.

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 *)
```

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)

Philip B. has marked this topic as resolved.

Philip B. has marked this topic as unresolved.

Philip B. has marked this topic as resolved.

Last updated: May 19 2024 at 16:02 UTC