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.

$\endgroup$

1 Answer 1

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.
$\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$ May 1, 2023 at 15:07

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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