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

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?

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

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

Lessness has marked this topic as resolved.

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

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

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

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