0
$\begingroup$

I have another proof I'm trying to complete in Coq involving the Divmod function, but the inductive case has a different value of q for the divmod function.

The q parameter is only involved in the divisor, so it shouldn't affect the remainder part of the function.

I can't find a way to prove that snd (divmod x y q u) = snd (divmod x y (S q) u) however.

The q parameter is only involved in the divisor, but because q only goes up, not down in the inductive definition, I haven't been able to prove this statement about divmod.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
0
$\begingroup$

Something like this?

Require Import PeanoNat.
Import Nat.

Lemma snd_divmod_S x y q u :
  snd (divmod x y q u) = snd (divmod x y (S q) u).
Proof.
revert y q u; induction x as [|x IH]; intros y q [|u]; simpl; auto.
Qed.
Improve this answer
$\endgroup$
1
  • $\begingroup$ Ok, not sure why I struggled so much with this one. I think I didn't have q in the quantifiers in the Inductive hypothesis. $\endgroup$
    – Tony Peterson
    Commented May 1, 2023 at 15:07

Not the answer you're looking for? Browse other questions tagged or ask your own question.