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
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
Any help would be greatly appreciated!
What should work is "unfold ceil in *" then "destruct (proper r)", "simpl in *" and finally "destruct (Qeb_bool remainder 0)"
The second step is the least obvious
If that doesn't work, maybe add the statement and incomplete proof.
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.
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: Jan 29 2023 at 01:02 UTC