Julin S (Jun 10 2022 at 05:23): Julin S (Jun 10 2022 at 05:23):In an effort to understand sumbool, I was trying to define
Definition le_gt_n_m (n m:nat):{n<=m}+{n>m}.
I tried to define it with proof mode (would the other way have been better?)
Wasn't sure how to deal with proofs involving inequalities, but I suppose we would need lia?
This is what I tried:
Require Import Lia.
Definition le_gt_n_m (n m:nat):{n<=m}+{n>m}.
Proof.
induction n.
- left.
lia.
-
At this point, the goal was:
1 subgoal
n, m : nat
IHn : {n <= m} + {n > m}
========================= (1 / 1)
{S n <= m} + {S n > m}
But didn't know how to proceed.
Could someone help me out?
Théo Winterhalter (Jun 10 2022 at 05:25):You need to generalise over m if you want to go anywhere.
induction n in m |- *. would do that.
Théo Winterhalter (Jun 10 2022 at 05:26):But then it's not about understanding sumbool which I guess you understand from your use of left.
{a} + {b} is supposed to represent a meaningful decision between either a or b.
Julin S (Jun 10 2022 at 05:28):I'm still only trying to get the hang of theorem proving. So I guess what I say and what I do must be at odds..:sweat_smile:
Julin S (Jun 10 2022 at 05:29):Please do correct me if you spot discrepancies.
Julin S (Jun 10 2022 at 05:30):Did you mean that using left is not related to using sumbool? I though with n=0, we could definitely go with 0<=m. That's why I went with left there.
Julin S (Jun 10 2022 at 05:35):And any idea where I can read about the |- * syntax?
Théo Winterhalter (Jun 10 2022 at 05:53):I meant the overall induction is unrelated. left is about sumbool.
Théo Winterhalter (Jun 10 2022 at 05:55):I don't find the |- * syntax in the doc, maybe someone else knows?
What I do know is that the variables that you put on the left will be generalised in the induction hypothesis. They are comma separated (x, y, z |- *).
Julin S (Jun 10 2022 at 06:32):I think the * part may be explained by this:
*- introduces one or more quantified variables from the result until there are no more quantified variables.
Michael Soegtrop (Jun 10 2022 at 06:34):The in var |- * syntax is the occurrences part of (https://coq.inria.fr/refman/proofs/writing-proofs/reasoning-inductives.html#grammar-token-induction_clause).
But I don't find this syntax very nice. I would recommend to write a bit longer but easier to understand code using intros and generalize - this makes it more obvious what is going on.
Michael Soegtrop (Jun 10 2022 at 06:36):Also one can't say the description in the reference manual on what the occurrences do here has much to do with what happens - IMHO something one should report as doc bug.
Paolo Giarrusso (Jun 10 2022 at 19:26):re “longer” I’d say YMMV. The verbosity _might_ be helpful when you are a beginner (not sure), but it is pretty wasteful later (I can only type 50 wpm, and Coq is verbose enough that sometimes it is a problem).
Last updated: Oct 05 2023 at 02:01 UTC