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?

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 foobar2 (n: nat) : {AProp' n} + {BProp' n}.
Proof.
destruct n.
- right; intro x; lia.
- left; exists 0; lia.
Defined.
```

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.

The goal had become:

```
1 subgoal
n, x : nat
H : x + S n = x
========================= (1 / 1)
S n = 0
```

What could be done to make this progress?

(And regarding `foobar`

, I'll try defining in proof mode. Thanks!)

`S n = 0`

seems like an impossible goal. Maybe I went in an inappropriate direction to solve the proof?

And are `destruct n`

and `induction n`

equivalent in this particular example?

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?

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

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

`lia`

did it.

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

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?

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?

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.

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.

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.

I had another doubt.

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?

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

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?

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}
```

How can we proceed from here?

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`

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.
```

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.
```

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)

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`

.

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.

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.
```

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: Sep 23 2023 at 08:01 UTC