Trait WellFounded 

pub trait WellFounded: Sized {
    // Required methods
    fn well_founded_relation(self, other: Self) -> bool;
    fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int;
}

Instances of this trait are types which are allowed as variants of recursive definitions.

Required Methods

fn well_founded_relation(self, other: Self) -> bool

Relation used to specify well-foundedness.

fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int

Being well-founded means that there is no infinitely decreasing sequence.

If you can map your type to another that already implements WellFounded (and the mapping preserves well_founded_relation), this lemma is quite easy to prove:

struct MyInt(Int);
impl WellFounded for MyInt {
    #[logic(open, inline)]
    fn well_founded_relation(self, other: Self) -> bool {
        Int::well_founded_relation(self.0, other.0)
    }

    #[logic]
    #[ensures(!Self::well_founded_relation(s[result], s[result + 1]))]
    fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int {
        Int::no_infinite_decreasing_sequence(|i| s[i].0)
    }
}

ensures

result >= 0

ensures

!Self::well_founded_relation(s[result], s[result + 1])

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementations on Foreign Types

impl WellFounded for i8

fn well_founded_relation(self, other: Self) -> bool

(open, inline)

self > other

fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int

ensures

result >= 0

ensures

!Self::well_founded_relation(s[result], s[result + 1])

impl WellFounded for i16

fn well_founded_relation(self, other: Self) -> bool

(open, inline)

self > other

fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int

ensures

result >= 0

ensures

!Self::well_founded_relation(s[result], s[result + 1])

impl WellFounded for i32

fn well_founded_relation(self, other: Self) -> bool

(open, inline)

self > other

fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int

ensures

result >= 0

ensures

!Self::well_founded_relation(s[result], s[result + 1])

impl WellFounded for i64

fn well_founded_relation(self, other: Self) -> bool

(open, inline)

self > other

fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int

ensures

result >= 0

ensures

!Self::well_founded_relation(s[result], s[result + 1])

impl WellFounded for i128

fn well_founded_relation(self, other: Self) -> bool

(open, inline)

self > other

fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int

ensures

result >= 0

ensures

!Self::well_founded_relation(s[result], s[result + 1])

impl WellFounded for isize

fn well_founded_relation(self, other: Self) -> bool

(open, inline)

self > other

fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int

ensures

result >= 0

ensures

!Self::well_founded_relation(s[result], s[result + 1])

impl WellFounded for u8

fn well_founded_relation(self, other: Self) -> bool

(open, inline)

self > other

fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int

ensures

result >= 0

ensures

!Self::well_founded_relation(s[result], s[result + 1])

impl WellFounded for u16

fn well_founded_relation(self, other: Self) -> bool

(open, inline)

self > other

fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int

ensures

result >= 0

ensures

!Self::well_founded_relation(s[result], s[result + 1])

impl WellFounded for u32

fn well_founded_relation(self, other: Self) -> bool

(open, inline)

self > other

fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int

ensures

result >= 0

ensures

!Self::well_founded_relation(s[result], s[result + 1])

impl WellFounded for u64

fn well_founded_relation(self, other: Self) -> bool

(open, inline)

self > other

fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int

ensures

result >= 0

ensures

!Self::well_founded_relation(s[result], s[result + 1])

impl WellFounded for u128

fn well_founded_relation(self, other: Self) -> bool

(open, inline)

self > other

fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int

ensures

result >= 0

ensures

!Self::well_founded_relation(s[result], s[result + 1])

impl WellFounded for ()

fn well_founded_relation(self, _: Self) -> bool

(open, inline)

false

fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int

ensures

result >= 0

ensures

!Self::well_founded_relation(s[result], s[result + 1])

impl WellFounded for usize

fn well_founded_relation(self, other: Self) -> bool

(open, inline)

self > other

fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int

ensures

result >= 0

ensures

!Self::well_founded_relation(s[result], s[result + 1])

impl<T0> WellFounded for (T0,)

where T0: WellFounded,

fn well_founded_relation(self, other: Self) -> bool

(open, inline)

$res

fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int

ensures

result >= 0

ensures

!Self::well_founded_relation(s[result], s[result + 1])

impl<T0, T1> WellFounded for (T0, T1)

where T0: WellFounded, T1: WellFounded,

fn well_founded_relation(self, other: Self) -> bool

(open, inline)

$res

fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int

ensures

result >= 0

ensures

!Self::well_founded_relation(s[result], s[result + 1])

impl<T0, T1, T2> WellFounded for (T0, T1, T2)

where T0: WellFounded, T1: WellFounded, T2: WellFounded,

fn well_founded_relation(self, other: Self) -> bool

(open, inline)

$res

fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int

ensures

result >= 0

ensures

!Self::well_founded_relation(s[result], s[result + 1])

impl<T0, T1, T2, T3> WellFounded for (T0, T1, T2, T3)

where T0: WellFounded, T1: WellFounded, T2: WellFounded, T3: WellFounded,

fn well_founded_relation(self, other: Self) -> bool

(open, inline)

$res

fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int

ensures

result >= 0

ensures

!Self::well_founded_relation(s[result], s[result + 1])

impl<T0, T1, T2, T3, T4> WellFounded for (T0, T1, T2, T3, T4)

where T0: WellFounded, T1: WellFounded, T2: WellFounded, T3: WellFounded, T4: WellFounded,

fn well_founded_relation(self, other: Self) -> bool

(open, inline)

$res

fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int

ensures

result >= 0

ensures

!Self::well_founded_relation(s[result], s[result + 1])

impl<T0, T1, T2, T3, T4, T5> WellFounded for (T0, T1, T2, T3, T4, T5)

where T0: WellFounded, T1: WellFounded, T2: WellFounded, T3: WellFounded, T4: WellFounded, T5: WellFounded,

fn well_founded_relation(self, other: Self) -> bool

(open, inline)

$res

fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int

ensures

result >= 0

ensures

!Self::well_founded_relation(s[result], s[result + 1])

impl<T0, T1, T2, T3, T4, T5, T6> WellFounded for (T0, T1, T2, T3, T4, T5, T6)

where T0: WellFounded, T1: WellFounded, T2: WellFounded, T3: WellFounded, T4: WellFounded, T5: WellFounded, T6: WellFounded,

fn well_founded_relation(self, other: Self) -> bool

(open, inline)

$res

fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int

ensures

result >= 0

ensures

!Self::well_founded_relation(s[result], s[result + 1])

impl<T0, T1, T2, T3, T4, T5, T6, T7> WellFounded for (T0, T1, T2, T3, T4, T5, T6, T7)

where T0: WellFounded, T1: WellFounded, T2: WellFounded, T3: WellFounded, T4: WellFounded, T5: WellFounded, T6: WellFounded, T7: WellFounded,

fn well_founded_relation(self, other: Self) -> bool

(open, inline)

$res

fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int

ensures

result >= 0

ensures

!Self::well_founded_relation(s[result], s[result + 1])

impl<T: WellFounded> WellFounded for &T

fn well_founded_relation(self, other: Self) -> bool

(open, inline)

T::well_founded_relation(*self, *other)

fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int

ensures

result >= 0

ensures

!Self::well_founded_relation(s[result], s[result + 1])

impl<T: WellFounded> WellFounded for Box<T>

fn well_founded_relation(self, other: Self) -> bool

(open, inline)

T::well_founded_relation(*self, *other)

fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int

ensures

result >= 0

ensures

!Self::well_founded_relation(s[result], s[result + 1])

Implementors

impl WellFounded for Int