Divmod equation

Using Coq
1

I’m stuck with a proof because I don’t know how to deal with divmod equations. Here’s what I need to prove.

fst (Nat.divmod (n * (n - 1)) 1 0 1) + n =
fst(Nat.divmod (n - 0 + n * (n - 0)) 1 0 1)

2

You could rely on Nat.divmod_spec (which looks like the only available statement):

Require Import Arith Psatz.

Search Nat.divmod.
(*
Nat.divmod_spec:
  forall x y q u : nat,
  u <= y -> let (q', u') :=
    Nat.divmod x y q u in x + S y * q + (y - u) = S y * q' + (y - u') /\ u' <= y
*)

Lemma divmod_equation n :
   fst (Nat.divmod (n * (n - 1)) 1 0 1) + n
 = fst (Nat.divmod (n - 0 + n * (n - 0)) 1 0 1).
Proof.
assert (1 <= 1) as Hle11 by reflexivity. (* useful since dealing with Nat.divmod _ 1 _ 1 *)

(* expand specification for first component *)
assert (H1 := Nat.divmod_spec (n * (n - 1)) 1 0 1 Hle11).
destruct (Nat.divmod (n * (n - 1)) 1 0 1).

(* expand specification for second component *)
assert (H2 := Nat.divmod_spec (n - 0 + n * (n - 0)) 1 0 1 Hle11).
destruct (Nat.divmod (n - 0 + n * (n - 0)) 1 0 1).

(* now it is just a matter of dealing with more standard arithmetic operations *)
cbn; nia.
Qed.
1 Like
3

According to the shape of your statement, it might come from a reduction (simpl, cbn, etc.) of things of the shape Nat.div _ 2. Going back gives you access to lots of lemmas about Nat.div (or even Nat.div2 through Nat.div2_div : forall a : nat, Nat.div2 a = Nat.div a 2).

Require Import Arith Psatz.

Lemma divmod_equation_div n :
   fst (Nat.divmod (n * (n - 1)) 1 0 1) + n
 = fst (Nat.divmod (n - 0 + n * (n - 0)) 1 0 1).
Proof.
(* fold into Nat.div _ 2 *)
fold (Nat.div (n * (n - 1)) 2) (Nat.div (n - 0 + n * (n - 0)) 2).

(* put everything with same denominator *)
rewrite <- Nat.div_add by intros [=].

(* compare separately numerators and denominators (trivial for denominators) *)
f_equal.

(* arithmetic computation to conclude *)
nia.
Qed.
1 Like
4

Thank you so much! You saved my life lol.