Julin S (Jun 11 2022 at 15:57): 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 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.
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?
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
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):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?
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}
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.
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)
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.
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