vstd/arithmetic/internals/
div_internals_nonlinear.rs

Help
1//! This file contains proofs related to division that require
2//! nonlinear-arithmetic reasoning to prove. These are internal
3//! functions used within the math standard library.
4//!
5//! It's based on the following file from the Dafny math standard library:
6//! `Source/DafnyStandardLibraries/src/Std/Arithmetic/Internal/DivInternalsNonlinear.dfy`.
7//! That file has the following copyright notice:
8//! /*******************************************************************************
9//! *  Original: Copyright (c) Microsoft Corporation
10//! *  SPDX-License-Identifier: MIT
11//! *
12//! *  Modifications and Extensions: Copyright by the contributors to the Dafny Project
13//! *  SPDX-License-Identifier: MIT
14//! *******************************************************************************/
15#[allow(unused_imports)]
16use super::super::super::prelude::*;
17
18verus! {
19
20/// Proof that 0 divided by any given integer `d` is 0
21#[verifier::nonlinear]
22pub proof fn lemma_div_of0(d: int)
23    requires
24        d != 0 as int,
25    ensures
26        0 as int / d == 0 as int,
27{
28}
29
30/// Proof that any given integer `d` divided by itself is 1
31pub proof fn lemma_div_by_self(d: int)
32    requires
33        d != 0,
34    ensures
35        d / d == 1,
36{
37}
38
39/// Proof that dividing a non-negative integer by a larger integer results in a quotient of 0
40#[verifier::nonlinear]
41pub proof fn lemma_small_div()
42    ensures
43        forall|x: int, d: int| 0 <= x < d && d > 0 ==> #[trigger] (x / d) == 0,
44{
45}
46
47} // verus!
vstd/arithmetic/internals/div_internals_nonlinear.rs

vstd/arithmetic/internals/
div_internals_nonlinear.rs
