## Stream: Coq users

### Topic: case on an if statement inside a let

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

#### Li-yao (Nov 14 2020 at 00:29):

``````destruct (proper r) eqn:Epr.
``````

or introduce the relevant assumptions before destructing

``````pose proof (proper_splits_correct r) as Hpr; destruct (proper r).
``````

#### Sam Nolan (Nov 14 2020 at 00:45):

Ok, you are legendary, exactly what I needed. You're amazing.

Last updated: Jun 23 2024 at 23:01 UTC