Philip B. (Feb 15 2022 at 15:49): 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
boolandPropare related. To do that, I tried to proveforall m n : nat, m == n -> m = n, and while that seemed too difficult, I decided to prove a particular caseforall 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 *)
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 13 2024 at 01:02 UTC