Stream: Coq users

Topic: Function returning sumbool


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

view this post on Zulip Pierre Castéran (Jun 11 2022 at 17:11):

There is probably an error (lack of parentheses, wrong connectives ?) in your definitions, since APropand BPropare 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 sumboolconstruction

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.

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

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?

view this post on Zulip Julin S (Jun 12 2022 at 04:44):

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

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

view this post on Zulip Julin S (Jun 12 2022 at 04:47):

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

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

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

view this post on Zulip Julin S (Jun 12 2022 at 04:57):

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

view this post on Zulip Julin S (Jun 12 2022 at 04:58):

lia did it.

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

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

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

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

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

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

view this post on Zulip Julin S (Jun 12 2022 at 05:54):

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?

view this post on Zulip Paolo Giarrusso (Jun 12 2022 at 06:31):

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

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

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

view this post on Zulip Julin S (Jun 12 2022 at 06:57):

How can we proceed from here?

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

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

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

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

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

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

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

view this post on Zulip 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: Mar 28 2024 at 18:02 UTC