From afdec6bf6b95234c786cf5ecf559270e479b781a Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Tue, 24 Dec 2024 18:59:03 -0800 Subject: [PATCH] chore: Restore a proof --- .../DafnyStandardLibraries/src/Std/Arithmetic/DivMod.dfy | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/Source/DafnyStandardLibraries/src/Std/Arithmetic/DivMod.dfy b/Source/DafnyStandardLibraries/src/Std/Arithmetic/DivMod.dfy index b40ee42269..0fa5e77d23 100644 --- a/Source/DafnyStandardLibraries/src/Std/Arithmetic/DivMod.dfy +++ b/Source/DafnyStandardLibraries/src/Std/Arithmetic/DivMod.dfy @@ -629,12 +629,15 @@ module Std.Arithmetic.DivMod { } } - lemma LemmaIndistinguishableQuotients(a: int, b: int, d: int) + lemma {:induction false} LemmaIndistinguishableQuotients(a: int, b: int, d: int) requires 0 < d requires 0 <= a - a % d <= b < a + d - a % d ensures a / d == b / d { - LemmaDivInductionAuto(d, a - b, ab => var u := ab + b; 0 <= u - u % d <= b < u + d - u % d ==> u / d == b / d); + var f := ab => var u := ab + b; 0 <= u - u % d <= b < u + d - u % d ==> u / d == b / d; + assert f(a - b) by { + LemmaDivInductionAuto(d, a - b, f); + } } lemma LemmaIndistinguishableQuotientsAuto()