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
    May 1 at 15:07

Your Answer

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

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