Stream: Coq users

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


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Philip B. (Feb 15 2022 at 20:53):

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

view this post on Zulip 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 *)

view this post on Zulip 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)

view this post on Zulip Notification Bot (Feb 15 2022 at 21:29):

Philip B. has marked this topic as resolved.

view this post on Zulip Notification Bot (Feb 15 2022 at 21:29):

Philip B. has marked this topic as unresolved.

view this post on Zulip Notification Bot (Feb 15 2022 at 21:29):

Philip B. has marked this topic as resolved.


Last updated: Jan 27 2023 at 00:03 UTC