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?
You need to generalise over m
if you want to go anywhere.
induction n in m  *.
would do that.
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
.
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:
Please do correct me if you spot discrepancies.
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.
And any idea where I can read about the  *
syntax?
I meant the overall induction is unrelated. left
is about sumbool
.
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  *
).
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.
The in var  *
syntax is the occurrences part of (https://coq.inria.fr/refman/proofs/writingproofs/reasoninginductives.html#grammartokeninduction_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.
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.
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: Jun 16 2024 at 02:41 UTC