Stream: Coq users

Topic: ✔ Asking for hints to prove a theorem

view this post on Zulip Lessness (Jul 30 2021 at 15:43):

I tried to prove such theorem Theorem thm_3 a n (Ha: 0 < a) (Hn: 0 <= n): (n + 1) / a = if Zdivide_dec a (n + 1) then n / a + 1 else n / a.
Here's what I have got for now. I have no idea how to prove last case. If anyone has some hints, I would be grateful. :)

Require Import VST.floyd.proofauto.

Theorem thm_3 a n (Ha: 0 < a) (Hn: 0 <= n):
  (n + 1) / a = if Zdivide_dec a (n + 1) then n / a + 1 else n / a.
Proof.
  revert n Hn. apply natlike_ind.
  + simpl. destruct (Zdivide_dec a 1).
    - apply Z.divide_1_r_nonneg in d. subst. auto. lia.
    - assert (1 < a).
      { assert (a = 1 \/ 1 < a) by lia. destruct H.
        + subst. exfalso. apply n. exists 1. auto.
        + auto. }
      rewrite Zdiv_0_l. rewrite Z.div_1_l; auto.
  + intros. destruct (Zdivide_dec a (x + 1)).
    - destruct d. assert (x = x0 * a - 1) by lia. rewrite H2 in *.
      clear H1. replace (Z.succ (x0 * a - 1) + 1) with (x0 * a + 1) by lia.
      destruct Zdivide_dec.
      * destruct d. assert (a = 1).
        { assert ((x1 - x0) * a = 1) by lia. rewrite Z.mul_comm in H3.
          apply Z.mul_eq_1 in H3. lia. }
        subst. repeat rewrite Z.div_1_r. lia.
      * assert (1 < a).
        { assert (a = 1 \/ 1 < a) by lia. destruct H1; auto. exfalso.
          subst a. apply n. exists (x0 + 1). lia. }
        replace (Z.succ (x0 * a - 1)) with (x0 * a) by lia.
        rewrite Z_div_mult; try lia. rewrite Z_div_plus_full_l; try lia.
        assert (1 / a = 0).
        { apply Z.div_small. lia. }
        lia.
    - destruct Zdivide_dec.
      * destruct d. rewrite H1. rewrite Z_div_mult; try lia.
        assert (Z.succ x = x0 * a - 1) by lia. rewrite H2.
        assert (a <> 1).
        { intro. apply n. subst. exists (x + 1). ring. }
        replace (x0 * a - 1) with (x0 * a + (-1)) by ring.
        rewrite Z_div_plus_full_l; try lia.
        assert (-1 / a = -1).
        { replace (-1) with (Z.opp 1). rewrite Z.div_opp_l_nz; try lia.
          rewrite Z.div_1_l. ring. lia. rewrite Z.mod_1_l. lia. lia. ring. }
        rewrite H4. ring.
      * assert (a <> 1).
        { intro. subst. apply n. exists (x + 1). ring. }
Admitted.

view this post on Zulip Andrés Goens (Jul 30 2021 at 15:46):

have you tried with pen and paper, understanding why it is true? In other words, are you asking for hints on how to prove it conceptually or how to formalize it?

view this post on Zulip Lessness (Jul 30 2021 at 15:56):

It seems, both. It seems too obvious, but simultaneously I have no idea (for now) how to prove it with Coq.
Probably I don't understand it good enough to prove it with pen and paper, too.

1 subgoal
a : Z
Ha : 0 < a
x : Z
H : 0 <= x
n : ~ (a | x + 1)
H0 : (x + 1) / a = x / a
n0 : ~ (a | Z.succ x + 1)
H1 : a <> 1
______________________________________(1/1)
(Z.succ x + 1) / a = Z.succ x / a

view this post on Zulip Lessness (Jul 31 2021 at 16:00):

Here we go, it's success. I had to use 'size induction' (is it the correct name for it?) for nonnegative Z numbers or Z_lt_induction.
Although, maybe I did something wrong as I found necessary to duplicate Hn hypothesis.

Require Import VST.floyd.proofauto.

Theorem thm_3 a n (Ha: 0 < a) (Hn: 0 <= n):
  (n + 1) / a = if Zdivide_dec a (n + 1) then n / a + 1 else n / a.
Proof.
  pose proof Hn as Hn'. revert Hn. pattern n. apply Z_lt_induction.
  + intros. assert (0 <= x <= a - 2 \/ a - 1 = x \/ a <= x) by lia.
    destruct H0; [|destruct H0].
    - assert (1 <= x + 1 < a) by lia. rewrite Z.div_small; try lia.
      destruct Zdivide_dec.
      * destruct d. assert (x0 = 0 \/ 1 <= x0) by lia. destruct H3.
        ++ lia.
        ++ nia.
      * rewrite Z.div_small; lia.
    - subst. replace (a - 1 + 1) with a by ring.
      rewrite Z.div_same; try lia. destruct Zdivide_dec.
      * rewrite Z.div_small; lia.
      * exfalso. apply n0. exists 1. lia.
    - assert (0 <= x - a < x) by lia. pose proof (H _ H1 (proj1 H1)).
      destruct (Zdivide_dec a (x - a + 1)).
      * destruct d. destruct Zdivide_dec.
        ++ assert (x + 1 = (x0 + 1) * a) by lia. rewrite H4.
           assert (x = x0 * a + (a - 1)) by lia. rewrite H5.
           rewrite Z_div_mult; try lia.
           rewrite Z.div_add_l; try lia.
           rewrite Z.div_small; lia.
        ++ exfalso. apply n0. exists (x0 + 1). lia.
      * destruct Zdivide_dec.
        ++ destruct d. exfalso. apply n0. exists (x0 - 1). lia.
        ++ replace (x + 1) with (1 * a + (x - a + 1)) by ring.
           rewrite Z.div_add_l; try lia.
           replace x with (1 * a + (x - a)) at 2 by ring.
           rewrite Z.div_add_l; lia.
  + auto.
Qed.

view this post on Zulip Notification Bot (Jul 31 2021 at 16:01):

Lessness has marked this topic as resolved.

view this post on Zulip Ben Siraphob (Jul 31 2021 at 16:05):

@Lessness have you also been formally verifying C programs with VST?

view this post on Zulip Ben Siraphob (Jul 31 2021 at 16:05):

I've been working through https://softwarefoundations.cis.upenn.edu/vc-current/index.html and found it a great resource

view this post on Zulip Lessness (Jul 31 2021 at 17:12):

Yes, I'm at the start of it. :)

Got my focus diverted by the first exercise of Project Euler, for which I hope to write formally verified C program. Of course, later, when I understand more of the VST and maybe have worked through all the book. (Right now I'm only formalizing math part of the first exercise.)

view this post on Zulip Ben Siraphob (Jul 31 2021 at 19:14):

Nice! I had to do some extra exercises on the side as well to get familiar with the library, mostly math algorithms like fibonacci, gcd, factorial. I'm struggling with the hash tables part myself.

Last updated: Sep 28 2023 at 11:01 UTC