Sam Nolan (Nov 12 2020 at 06:47): Sam Nolan (Nov 12 2020 at 06:47):Hello! Beginner question incoming.
I'm trying to prove that a property holds whether or not if statement evaluates as true or false. Now... this is usually a simple matter of the case tactic, however, I have my if inside a let.
Here's my definition, it very simply defines a ceiling function based off a proper (floor) function.
Definition ciel (r : Q) : Z * Q :=
let (quotient, remainder) := proper r in
if Qeq_bool remainder 0
then (quotient, remainder)
else ((quotient + 1)%Z, remainder - 1).
I know that quotient + remainder = r for proper and have proved it, and this is obviously also true for this definition of cieling for both cases. I just don't know how to case this if statement inside the let expression.
Any help would be greatly appreciated!
Paolo Giarrusso (Nov 12 2020 at 10:27):What should work is "unfold ceil in *" then "destruct (proper r)", "simpl in *" and finally "destruct (Qeb_bool remainder 0)"
Paolo Giarrusso (Nov 12 2020 at 10:27):The second step is the least obvious
Paolo Giarrusso (Nov 12 2020 at 10:28):If that doesn't work, maybe add the statement and incomplete proof.
Sam Nolan (Nov 14 2020 at 00:13):Hmmmm, That doesn't work because destruct loses the fact that the quotient and remainder came from proper r. This means I can't use the fact that I've proved it for proper.
This is the incomplete proof:
Lemma ciel_splits_correct : forall r, (let (whole, fraction) := (ciel r) in (whole # 1) + fraction) == r.
Proof.
intros.
unfold ciel.
destruct (proper r).
That ends up with the proof state:
1 subgoal
r : Q
z : Z
q : Q
______________________________________(1/1)
(let (whole, fraction) :=
if Qeq_bool q 0 then (z, q) else ((z + 1)%Z, q - 1) in
(whole # 1) + fraction) == r
Which means I cannot use my other lemma proper_splits_correct because it is no longer in the goal. proper_splits_correct is defined as:
Lemma proper_splits_correct : forall r, (let (whole, fraction) := (proper r) in (whole # 1) + fraction) == r.
Other definitions:
Definition proper (number : Q) : Z * Q :=
match Z.div_eucl (Qnum number) (Zpos (Qden number)) with
| (quotient, remainder) => (quotient , remainder # Qden number)
end.
Definition ciel (number : Q) : Z * Q :=
(let (quotient, remainder) := proper number
in if Qeq_bool (remainder) 0
then (quotient, remainder)
else ((quotient + 1)%Z, remainder - 1)
).
destruct (proper r) eqn:Epr.
or introduce the relevant assumptions before destructing
pose proof (proper_splits_correct r) as Hpr; destruct (proper r).
Ok, you are legendary, exactly what I needed. You're amazing.
Last updated: Sep 23 2023 at 06:01 UTC