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!

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

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: Jun 23 2024 at 23:01 UTC