## Stream: Coq users

### Topic: Function returning sumbool

#### Julin S (Jun 11 2022 at 15:57):

Is it possible to make a function `foobar` returning a `sumbool` like:

``````Definition AProp (n:nat) : Prop := exists x:nat, n + x = 2 -> n <= 2.
Definition BProp (n:nat) : Prop := forall x:nat, x + n = x -> n = 0.

Definition foobar (n:nat) : {AProp n} + {BProp n}.
``````

Couldn't figure out how to be put the proof part into the `left` / `right` constructors?

#### Pierre Castéran (Jun 11 2022 at 17:11):

There is probably an error (lack of parentheses, wrong connectives ?) in your definitions, since `AProp`and `BProp`are always true. Thus, you get two trivial proofs of `foobar`.

``````Require Import Lia.
Lemma A_always_true: forall n, AProp n.
Proof. exists 0. lia. Qed.

Lemma B_always_true: forall n, BProp n.
Proof. intros n x; lia. Qed.

Definition foobar (n:nat) : {AProp n} + {BProp n}.
Proof.  right. apply B_always_true. Defined.

Definition foobar' (n:nat) : {AProp n} + {BProp n}.
Proof. left. apply A_always_true. Defined.
``````

I don't know if it answers your question, but here is a similar example of `sumbool`construction

``````Definition AProp' (n:nat) : Prop :=
exists x:nat, n + x > x.

Definition BProp' (n:nat) : Prop :=
forall x:nat, x + n = x.

Definition foobar' (n: nat) : {AProp' n} + {BProp' n}.
Proof.
destruct n.
- right; intro x; lia.
- left; exists 0; lia.
Defined.
``````

#### Julin S (Jun 12 2022 at 04:44):

Sorry, in the example I put up, I meant

``````Definition AProp (n:nat) : Prop := exists x:nat,
((n + x) = 2) -> (n <= 2).
Definition BProp (n:nat) : Prop := forall x:nat,
((x + n) = x) -> (n = 0).
Definition foobar (n:nat) : {AProp n} + {BProp n}.
Proof.
unfold AProp.
unfold BProp.
destruct n.
- left.
exists 2.
auto.
- right.
intros.
``````

But I still got stuck.

``````1 subgoal

n, x : nat
H : x + S n = x

========================= (1 / 1)

S n = 0
``````

What could be done to make this progress?

#### Julin S (Jun 12 2022 at 04:44):

(And regarding `foobar`, I'll try defining in proof mode. Thanks!)

#### Julin S (Jun 12 2022 at 04:46):

`S n = 0` seems like an impossible goal. Maybe I went in an inappropriate direction to solve the proof?

#### Julin S (Jun 12 2022 at 04:47):

And are `destruct n` and `induction n` equivalent in this particular example?

#### Julin S (Jun 12 2022 at 04:53):

If we use `Nat.neq_succ_0: forall n : nat, S n <> 0`, we can get `S n <> 0`. But how would we get that into the context?

#### Julin S (Jun 12 2022 at 04:55):

Oh, using `pose proof (Nat.neq_succ_0 n).` got that into context.

So I got a goal with

``````n, x : nat
H : x + S n = x
H0 : S n <> 0

========================= (1 / 1)

S n = 0
``````

#### Julin S (Jun 12 2022 at 04:57):

Now need to figure out how to say H0 and goal contradict.

#### Julin S (Jun 12 2022 at 04:58):

`lia` did it.

#### Julin S (Jun 12 2022 at 04:58):

But I wonder if there is a more 'manual' way? Just to understand how the proof works.

#### Julin S (Jun 12 2022 at 05:00):

So now I got:

``````Definition AProp (n:nat) : Prop := exists x:nat,
((n + x) = 2) -> (n <= 2).
Definition BProp (n:nat) : Prop := forall x:nat,
((x + n) = x) -> (n = 0).
Definition foobar (n:nat) : {AProp n} + {BProp n}.
Proof.
unfold AProp.
unfold BProp.
destruct n.
- left.
exists 2.
auto.
- right.
intros.
pose proof (Nat.neq_succ_0 n).
lia.
Defined.
``````

But using this `foobar` always gives `right`.

Can;t be helped I guess. Since a contradiction was abused to define it. And `AProp` and `BProp` aren't mutually exclusive.

Is there a way to give preference to `left` and use `right` only if `left` wont' work out?

#### Julin S (Jun 12 2022 at 05:10):

I then tried a simple odd even function returning a sumbool:

``````Definition oddeven (n:nat):{Nat.Odd n} + {Nat.Even n}.
Proof.
induction n.
- right.
unfold Nat.Even.
exists 0.
auto.
- left.
unfold Nat.Odd.
exists (n/2).   (* Just hopefully put this one *)
``````

but got stuck here when the goal was:

``````n : nat
IHn : {Nat.Odd n} + {Nat.Even n}

========================= (1 / 1)

S n = 2 * (n / 2) + 1
``````

what can be done to go forward from here?

#### Julin S (Jun 12 2022 at 05:14):

Tried using `Nat.Odd_succ: forall n : nat, Nat.Odd (S n) <-> Nat.Even n` to make the goal `Nat.Even n`. But couldn't figure out how to forward there as well.

#### Pierre Castéran (Jun 12 2022 at 05:28):

Here is a proof, by cases over `IHn`.

``````Definition oddeven (n:nat):{Nat.Odd n} + {Nat.Even n}.
Proof.
induction n.
- right; now exists 0.
- destruct IHn as [Ho | He].
+ right; destruct Ho as [p Hp]; exists (S p). lia.
+ left. destruct He as [p Hp]; exists  p; lia.
Qed.
``````

Note that your new definition of `AProp` and `BProp` are equivalent to the previous ones.

#### Julin S (Jun 12 2022 at 05:51):

Thanks. Got the proof to finish now.

And yeah, only now did I read last messages carefully enough. I just sort of cooked some random `Prop` for `AProp` and `BProp`. They are indeed always true.

#### Julin S (Jun 12 2022 at 05:54):

Can a function return a sumbool like `{n > 10} + {n > 20}`? where `n` is any `nat` (`forall n:nat`)? Because in that case values of `n` from `0` to `10` would be left undefined for that function, right?

#### Paolo Giarrusso (Jun 12 2022 at 06:31):

you're right, such a function would not be total

#### Julin S (Jun 12 2022 at 06:53):

And if both `left` and `right` of a `sumbool` can be satisfied for a particular input, is there a way to bias the return value in favour of one of them?

As in

``````Definition foo (n:nat):{n > 5} + {n < 10}.
``````

where both `left` and `right` are `True` with 6,7,8,9 as values of `n`.

Is it possible to favour the `n<10` in those cases?

#### Julin S (Jun 12 2022 at 06:57):

I tried proving this but got stuck again:

``````Definition foo (n:nat):{n > 5} + {n < 10}.
Proof.
induction n.
- right.
lia.
- destruct IHn.
* left.
lia.
*
``````

That goal at this point was:

``````n : nat
l : n < 10

========================= (1 / 1)

{S n > 5} + {S n < 10}
``````

#### Julin S (Jun 12 2022 at 06:57):

How can we proceed from here?

#### Paolo Giarrusso (Jun 12 2022 at 07:40):

In proofs by induction, sometimes you need to generalize your induction hypothesis — maybe you’d prove that `S n < 10` from a proof that `n < 9`, but for that your IH must let you compare `n` with a different `m`

#### Pierre Castéran (Jun 12 2022 at 07:41):

I think it would be better to consider a specification with 3 mutually exclusive cases instead of favoring one case inside an interactive definition.

``````Require Import Compare_dec.

Definition F_5_10 (n:nat) : {n <= 5} + {6 <= n <= 9} + {10 <= n}.
destruct (le_lt_dec 10 n).
- now right.
- left. destruct (le_lt_dec n 5).
+ left; lia.
+ right; lia.
Defined.
``````

#### Paolo Giarrusso (Jun 12 2022 at 07:47):

and by generalizing the induction hypothesis, you get to something similar to `le_lt_dec` (the stdlib one's likely better, this is just a demo):

``````From Coq Require Import Arith Lia.

Definition le_gt_dec (n m : nat) : {n <= m} + {n > m}.
Proof.
revert m; induction n. { left. abstract lia. }
destruct m as [|m]. { right; abstract lia. }
destruct (IHn m); [left|right]; abstract lia.
Defined.
``````

#### Paolo Giarrusso (Jun 12 2022 at 07:48):

instead of favoring one case inside an interactive definition.

I guess the idea is that in an interactive definition we often only care about the return type, so `Definition foo (n:nat):{n > 5} + {n < 10}.` is best defined non-interactively to make the body to clients? (Trying that out)

#### Julin S (Jun 12 2022 at 08:02):

How would we define `Definition foo (n:nat):{n > 5} + {n < 10}.` non-interactively though? I mean, we got to furnish proof anyway right? As argument to `left` or `right`.

#### Pierre Castéran (Jun 12 2022 at 08:06):

Yes, the specification of foo leaves unspecified the cases `n=6,7,8,9`. It may be problematic if you apply `foo`
inside another function.

#### Paolo Giarrusso (Jun 12 2022 at 08:10):

indeed; if I needed the original spec anyway, I'd consider this style acceptable — the spec is insufficient, but the implementation is unambiguous (tho not especially readable):

``````Require Import Arith Lia Program.Tactics.
Definition le_gt_dec (n m : nat) : {n <= m} + {n > m}. (* As above. *)

Program Definition foo (n:nat):{n > 5} + {n < 10} :=
(* Decide if [n >= 10] or [n < 10]; if not,  *)
match le_gt_dec 10 n return _ with
| right X => right X (* n < 10 *)
| left X => left _ (* n >= 10 -> n > 5 *)
end.
Next Obligation. lia. Qed.
``````

#### Gaëtan Gilbert (Jun 12 2022 at 08:20):

you can also define the decision without any high power stuff

``````Fixpoint le_lt_dec (n m : nat) : {n <= m} + {m < n} :=
match n, m with
| 0, _ => left (le_0_n m)
| S n, 0 => right (le_n_S 0 n (le_0_n n))
| S n, S m =>
match le_lt_dec n m with
| left H => left (le_n_S n m H)
| right H => right (le_n_S (S m) n H)
end
end.
``````

Last updated: Jan 29 2023 at 01:02 UTC