Stream: Coq users

Topic: case on an if statement inside a let


view this post on Zulip 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!

view this post on Zulip 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)"

view this post on Zulip Paolo Giarrusso (Nov 12 2020 at 10:27):

The second step is the least obvious

view this post on Zulip Paolo Giarrusso (Nov 12 2020 at 10:28):

If that doesn't work, maybe add the statement and incomplete proof.

view this post on Zulip 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)
  ).

view this post on Zulip 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).

view this post on Zulip Sam Nolan (Nov 14 2020 at 00:45):

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


Last updated: Jan 29 2023 at 01:02 UTC