Stream: Coq users

Topic: Definition returning sumbool


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

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

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

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

view this post on Zulip Julin S (Jun 10 2022 at 05:29):

Please do correct me if you spot discrepancies.

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

view this post on Zulip Julin S (Jun 10 2022 at 05:35):

And any idea where I can read about the |- * syntax?

view this post on Zulip Théo Winterhalter (Jun 10 2022 at 05:53):

I meant the overall induction is unrelated. left is about sumbool.

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

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

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

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

view this post on Zulip 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: Feb 09 2023 at 00:03 UTC