## Stream: Coq users

### Topic: Definition returning sumbool

#### 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