From c8da0a280591ee1d0a89e279f018746bf15b6bec Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Sat, 2 Oct 2021 16:18:51 -0700 Subject: [PATCH 1/3] Progress (not verifying yet) --- src/Collections/Multisets/Multiset.dfy | 56 ++ src/Collections/Sequences/Seq.dfy | 1026 ++++++++++++------------ 2 files changed, 578 insertions(+), 504 deletions(-) create mode 100644 src/Collections/Multisets/Multiset.dfy diff --git a/src/Collections/Multisets/Multiset.dfy b/src/Collections/Multisets/Multiset.dfy new file mode 100644 index 00000000..347af652 --- /dev/null +++ b/src/Collections/Multisets/Multiset.dfy @@ -0,0 +1,56 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +/******************************************************************************* +* Copyright by the contributors to the Dafny Project +* SPDX-License-Identifier: MIT +*******************************************************************************/ + +module Multiset { + + /* converts a multiset to a set */ + function method {:opaque} ToSet(s: multiset): set + { + set x: T | x in s + } + + lemma LemmaSingletonSize(s: multiset, e: T) + requires e in s + requires forall e' | e' in s && e' != e :: s[e'] == 0 + decreases s[e] + ensures |s| == s[e] + { + reveal ToSet(); + if s[e] == 1 { + assert s == multiset{e}; + } else { + var s' := s[e := s[e] - 1]; + LemmaSingletonSize(s', e); + } + } + + lemma LemmaToSetOfDisjointUnion(a: multiset, b: multiset) + requires a !! b + ensures ToSet(a + b) == ToSet(a) + ToSet(b) + { + } + + /* proves that the cardinality of a multiset is always more than or equal to that + of the conversion to a set */ + lemma LemmaCardinalityOfSet(s: multiset) + ensures |ToSet(s)| <= |s| + { + reveal ToSet(); + if |s| == 0 { + } else { + var x :| x in s; + var xs := multiset{}[x := s[x]]; + assert ToSet(xs) == {x}; + var rest := s - xs; + LemmaCardinalityOfSet(rest); + LemmaToSetOfDisjointUnion(xs, rest); + assert |s| == |xs| + |rest|; + assert ToSet(s) == ToSet(xs) + ToSet(rest); + } + } +} \ No newline at end of file diff --git a/src/Collections/Sequences/Seq.dfy b/src/Collections/Sequences/Seq.dfy index 2eb850c9..61de3539 100644 --- a/src/Collections/Sequences/Seq.dfy +++ b/src/Collections/Sequences/Seq.dfy @@ -14,6 +14,7 @@ * SPDX-License-Identifier: MIT *******************************************************************************/ +include "../Multisets/Multiset.dfy" include "../../Wrappers.dfy" include "../../Math.dfy" @@ -21,6 +22,7 @@ module Seq { import opened Wrappers import Math + import Multiset /********************************************************** * @@ -200,6 +202,22 @@ module Seq { } } + /* A sequence that converts to a set of the same cardinality has no duplicates */ + lemma LemmaNoDuplicatesCardinalityOfSet(s: seq) + requires |ToSet(s)| == |s| + ensures HasNoDuplicates(s) + { + reveal HasNoDuplicates(); + reveal ToSet(); + if i,j :| 0 <= i < j < |s| && s[i] == s[j] { + var x := s[i]; + assert s == s[..j] + s[j..]; + assert multiset(s)[x] >= 2; + Multiset.LemmaCardinalityOfSet(multiset(s)); + assert |multiset(s)| < |s|; + } + } + /* proves that there are no duplicate values in the multiset version of the sequence */ lemma LemmaMultisetHasNoDuplicates(s: seq) requires HasNoDuplicates(s) @@ -218,512 +236,512 @@ module Seq { } } - /* finds the index of the first occurrence of an element in the sequence */ - function method {:opaque} IndexOf(s: seq, v: T): (i: nat) - requires v in s - ensures i < |s| && s[i] == v - ensures forall j {:trigger s[j]} :: 0 <= j < i ==> s[j] != v - { - if s[0] == v then 0 else 1 + IndexOf(s[1..], v) - } - - /* finds the index of the first occurrence of an element in the sequence if - found */ - function method {:opaque} IndexOfOption(s: seq, v: T): (o: Option) - ensures if o.Some? then o.value < |s| && s[o.value] == v && - forall j {:trigger s[j]} :: 0 <= j < o.value ==> s[j] != v - else v !in s - { - if |s| == 0 then None() - else - if s[0] == v then Some(0) - else - var o' := IndexOfOption(s[1..], v); - if o'.Some? then Some(o'.value + 1) else None() - } - - /* finds the index of the last occurrence of an element in the sequence */ - function method {:opaque} LastIndexOf(s: seq, v: T): (i: nat) - requires v in s - ensures i < |s| && s[i] == v - ensures forall j {:trigger s[j]} :: i < j < |s| ==> s[j] != v - { - if s[|s|-1] == v then |s| - 1 else LastIndexOf(s[..|s|-1], v) - } - - /* finds the index of the last occurrence of an element in the sequence if - found */ - function method {:opaque} LastIndexOfOption(s: seq, v: T): (o: Option) - ensures if o.Some? then o.value < |s| && s[o.value] == v && - forall j {:trigger s[j]} :: o.value < j < |s| ==> s[j] != v - else v !in s - { - if |s| == 0 then None() - else if s[|s|-1] == v then Some(|s| - 1) else LastIndexOfOption(s[..|s|-1], v) - } - - /* slices out a specific position's value from the sequence */ - function method {:opaque} Remove(s: seq, pos: nat): (s': seq) - requires pos < |s| - ensures |s'| == |s| - 1 - ensures forall i {:trigger s'[i], s[i]} | 0 <= i < pos :: s'[i] == s[i] - ensures forall i {:trigger s'[i]} | pos <= i < |s| - 1 :: s'[i] == s[i+1] - { - s[..pos] + s[pos+1..] - } - - /* slices out a specific value from the sequence */ - function method {:opaque} RemoveValue(s: seq, v: T): (s': seq) - ensures v !in s ==> s == s' - ensures v in s ==> |multiset(s')| == |multiset(s)| - 1 - ensures v in s ==> multiset(s')[v] == multiset(s)[v] - 1 - ensures HasNoDuplicates(s) ==> HasNoDuplicates(s') && ToSet(s') == ToSet(s) - {v} - { - reveal HasNoDuplicates(); - reveal ToSet(); - if v !in s then s - else - var i := IndexOf(s, v); - assert s == s[..i] + [v] + s[i+1..]; - s[..i] + s[i+1..] - } - - /* inserts a certain value into a specified index of the sequence */ - function method {:opaque} Insert(s: seq, a: T, pos: nat): seq - requires pos <= |s| - ensures |Insert(s, a, pos)| == |s| + 1 - ensures forall i {:trigger Insert(s, a, pos)[i], s[i]} :: 0 <= i < pos ==> Insert(s, a, pos)[i] == s[i] - ensures forall i {:trigger s[i]} :: pos <= i < |s| ==> Insert(s, a, pos)[i+1] == s[i] - ensures Insert(s, a, pos)[pos] == a - ensures multiset(Insert(s, a, pos)) == multiset(s) + multiset{a} - { - assert s == s[..pos] + s[pos..]; - s[..pos] + [a] + s[pos..] - } - - function method {:opaque} Reverse(s: seq): (s': seq) - ensures |s'| == |s| - ensures forall i {:trigger s'[i]}{:trigger s[|s| - i - 1]} :: 0 <= i < |s| ==> s'[i] == s[|s| - i - 1] - { - if s == [] then [] else [s[|s|-1]] + Reverse(s[0 .. |s|-1]) - } + // /* finds the index of the first occurrence of an element in the sequence */ + // function method {:opaque} IndexOf(s: seq, v: T): (i: nat) + // requires v in s + // ensures i < |s| && s[i] == v + // ensures forall j {:trigger s[j]} :: 0 <= j < i ==> s[j] != v + // { + // if s[0] == v then 0 else 1 + IndexOf(s[1..], v) + // } + + // /* finds the index of the first occurrence of an element in the sequence if + // found */ + // function method {:opaque} IndexOfOption(s: seq, v: T): (o: Option) + // ensures if o.Some? then o.value < |s| && s[o.value] == v && + // forall j {:trigger s[j]} :: 0 <= j < o.value ==> s[j] != v + // else v !in s + // { + // if |s| == 0 then None() + // else + // if s[0] == v then Some(0) + // else + // var o' := IndexOfOption(s[1..], v); + // if o'.Some? then Some(o'.value + 1) else None() + // } + + // /* finds the index of the last occurrence of an element in the sequence */ + // function method {:opaque} LastIndexOf(s: seq, v: T): (i: nat) + // requires v in s + // ensures i < |s| && s[i] == v + // ensures forall j {:trigger s[j]} :: i < j < |s| ==> s[j] != v + // { + // if s[|s|-1] == v then |s| - 1 else LastIndexOf(s[..|s|-1], v) + // } + + // /* finds the index of the last occurrence of an element in the sequence if + // found */ + // function method {:opaque} LastIndexOfOption(s: seq, v: T): (o: Option) + // ensures if o.Some? then o.value < |s| && s[o.value] == v && + // forall j {:trigger s[j]} :: o.value < j < |s| ==> s[j] != v + // else v !in s + // { + // if |s| == 0 then None() + // else if s[|s|-1] == v then Some(|s| - 1) else LastIndexOfOption(s[..|s|-1], v) + // } + + // /* slices out a specific position's value from the sequence */ + // function method {:opaque} Remove(s: seq, pos: nat): (s': seq) + // requires pos < |s| + // ensures |s'| == |s| - 1 + // ensures forall i {:trigger s'[i], s[i]} | 0 <= i < pos :: s'[i] == s[i] + // ensures forall i {:trigger s'[i]} | pos <= i < |s| - 1 :: s'[i] == s[i+1] + // { + // s[..pos] + s[pos+1..] + // } + + // /* slices out a specific value from the sequence */ + // function method {:opaque} RemoveValue(s: seq, v: T): (s': seq) + // ensures v !in s ==> s == s' + // ensures v in s ==> |multiset(s')| == |multiset(s)| - 1 + // ensures v in s ==> multiset(s')[v] == multiset(s)[v] - 1 + // ensures HasNoDuplicates(s) ==> HasNoDuplicates(s') && ToSet(s') == ToSet(s) - {v} + // { + // reveal HasNoDuplicates(); + // reveal ToSet(); + // if v !in s then s + // else + // var i := IndexOf(s, v); + // assert s == s[..i] + [v] + s[i+1..]; + // s[..i] + s[i+1..] + // } + + // /* inserts a certain value into a specified index of the sequence */ + // function method {:opaque} Insert(s: seq, a: T, pos: nat): seq + // requires pos <= |s| + // ensures |Insert(s, a, pos)| == |s| + 1 + // ensures forall i {:trigger Insert(s, a, pos)[i], s[i]} :: 0 <= i < pos ==> Insert(s, a, pos)[i] == s[i] + // ensures forall i {:trigger s[i]} :: pos <= i < |s| ==> Insert(s, a, pos)[i+1] == s[i] + // ensures Insert(s, a, pos)[pos] == a + // ensures multiset(Insert(s, a, pos)) == multiset(s) + multiset{a} + // { + // assert s == s[..pos] + s[pos..]; + // s[..pos] + [a] + s[pos..] + // } + + // function method {:opaque} Reverse(s: seq): (s': seq) + // ensures |s'| == |s| + // ensures forall i {:trigger s'[i]}{:trigger s[|s| - i - 1]} :: 0 <= i < |s| ==> s'[i] == s[|s| - i - 1] + // { + // if s == [] then [] else [s[|s|-1]] + Reverse(s[0 .. |s|-1]) + // } - function method {:opaque} Repeat(v: T, length: nat): (s: seq) - ensures |s| == length - ensures forall i: nat {:trigger s[i]} | i < |s| :: s[i] == v - { - if length == 0 then - [] - else - [v] + Repeat(v, length - 1) - } + // function method {:opaque} Repeat(v: T, length: nat): (s: seq) + // ensures |s| == length + // ensures forall i: nat {:trigger s[i]} | i < |s| :: s[i] == v + // { + // if length == 0 then + // [] + // else + // [v] + Repeat(v, length - 1) + // } - /* unzips a sequence that contains ordered pairs into 2 seperate sequences */ - function method {:opaque} Unzip(s: seq<(A, B)>): (seq, seq) - ensures |Unzip(s).0| == |Unzip(s).1| == |s| - ensures forall i {:trigger Unzip(s).0[i]} {:trigger Unzip(s).1[i]} - :: 0 <= i < |s| ==> (Unzip(s).0[i], Unzip(s).1[i]) == s[i] - { - if |s| == 0 then ([], []) - else - var (a, b):= Unzip(DropLast(s)); - (a + [Last(s).0], b + [Last(s).1]) - } - - /* takes two sequences, a and b, and combines then to form one sequence in which - each position contains an ordered pair from a and b */ - function method {:opaque} Zip(a: seq, b: seq): seq<(A, B)> - requires |a| == |b| - ensures |Zip(a, b)| == |a| - ensures forall i {:trigger Zip(a, b)[i]}:: 0 <= i < |Zip(a, b)| ==> Zip(a, b)[i] == (a[i], b[i]) - ensures Unzip(Zip(a, b)).0 == a - ensures Unzip(Zip(a, b)).1 == b - { - if |a| == 0 then [] - else Zip(DropLast(a), DropLast(b)) + [(Last(a), Last(b))] - } - - /* if a sequence is unzipped and then zipped, it forms the original sequence */ - lemma LemmaZipOfUnzip(s: seq<(A,B)>) - ensures Zip(Unzip(s).0, Unzip(s).1) == s - { - } - - /********************************************************** - * - * Extrema in Sequences - * - ***********************************************************/ - - /* finds the maximum integer value in the sequence */ - function method {:opaque} Max(s: seq): int - requires 0 < |s| - ensures forall k {:trigger k in s} :: k in s ==> Max(s) >= k - ensures Max(s) in s - { - assert s == [s[0]] + s[1..]; - if |s| == 1 then s[0] else Math.Max(s[0], Max(s[1..])) - } - - /* the greater maximum value of two sequences, a and b, becomes the maximum of the total sequence when - a and b are concatenated */ - lemma LemmaMaxOfConcat(a: seq, b: seq) - requires 0 < |a| && 0 < |b| - ensures Max(a+b) >= Max(a) - ensures Max(a+b) >= Max(b) - ensures forall i {:trigger i in [Max(a + b)]} :: i in a + b ==> Max(a + b) >= i - { - reveal Max(); - if |a| == 1 { - } else { - assert a[1..] + b == (a + b)[1..]; - LemmaMaxOfConcat(a[1..], b); - } - } - - /* finds the minimum integer value in the sequence */ - function method {:opaque} Min(s: seq): int - requires 0 < |s| - ensures forall k {:trigger k in s} :: k in s ==> Min(s) <= k - ensures Min(s) in s - { - assert s == [s[0]] + s[1..]; - if |s| == 1 then s[0] else Math.Min(s[0], Min(s[1..])) - } - - /* the smaller minimum value of two sequences, a and b, becomes the minimum of the total sequence when - a and b are concatenated */ - lemma LemmaMinOfConcat(a: seq, b: seq) - requires 0 < |a| && 0 < |b| - ensures Min(a+b) <= Min(a) - ensures Min(a+b) <= Min(b) - ensures forall i {:trigger i in a + b} :: i in a + b ==> Min(a + b) <= i - { - reveal Min(); - if |a| == 1 { - } else { - assert a[1..] + b == (a + b)[1..]; - LemmaMinOfConcat(a[1..], b); - } - } - - /* the maximum element in any subsequence will not be greater than the maximum element in - the full sequence */ - lemma LemmaSubseqMax(s: seq, from: nat, to: nat) - requires from < to <= |s| - ensures Max(s[from..to]) <= Max(s) - { - var subseq := s[from..to]; - if Max(subseq) > Max(s) { - var k :| 0 <= k < |subseq| && subseq[k] == Max(subseq); - assert s[seq(|subseq|, i requires 0 <= i < |subseq| => i + from)[k]] in s; - assert false; - } - } - - /* the minimum element in any subsequence will not be less than the minimum element in - the full sequence */ - lemma LemmaSubseqMin(s: seq, from: nat, to: nat) - requires from < to <= |s| - ensures Min(s[from..to]) >= Min(s) - { - var subseq := s[from..to]; - if Min(subseq) < Min(s) { - var k :| 0 <= k < |subseq| && subseq[k] == Min(subseq); - assert s[seq(|subseq|, i requires 0 <= i < |subseq| => i + from)[k]] in s; - } - } - - /********************************************************** - * - * Sequences of Sequences - * - ***********************************************************/ - - /*concatenates a sequence of sequences into a single sequence. Works by adding - elements in order from first to last */ - function method Flatten(s: seq>): seq - decreases |s| - { - if |s| == 0 then [] - else s[0] + Flatten(s[1..]) - } - - /* concatenating two sequences of sequences is equivalent to concatenating - each sequence of sequences seperately, and then concatenating the two resulting - sequences together */ - lemma LemmaFlattenConcat(a: seq>, b: seq>) - ensures Flatten(a + b) == Flatten(a) + Flatten(b) - { - if |a| == 0 { - assert a + b == b; - } else { - calc == { - Flatten(a + b); - { assert (a + b)[0] == a[0]; assert (a + b)[1..] == a[1..] + b; } - a[0] + Flatten(a[1..] + b); - a[0] + Flatten(a[1..]) + Flatten(b); - Flatten(a) + Flatten(b); - } - } - } - - /* concatenates the sequence of sequences into a single sequence. Works by concatenating - elements from last to first */ - function method FlattenReverse(s: seq>): seq - decreases |s| - { - if |s| == 0 then [] - else FlattenReverse(DropLast(s)) + Last(s) - } - - /* concatenating two reversed sequences of sequences is the same as reversing two - sequences of sequences and then concattenating the two resulting sequences together */ - lemma LemmaFlattenReverseConcat(a: seq>, b: seq>) - ensures FlattenReverse(a + b) == FlattenReverse(a) + FlattenReverse(b) - { - if |b| == 0 { - assert FlattenReverse(b) == []; - assert a + b == a; - } else { - calc == { - FlattenReverse(a + b); - { assert Last(a + b) == Last(b); assert DropLast(a + b) == a + DropLast(b); } - FlattenReverse(a + DropLast(b)) + Last(b); - FlattenReverse(a) + FlattenReverse(DropLast(b)) + Last(b); - FlattenReverse(a) + FlattenReverse(b); - } - } - } - - /* both methods of concatenating sequence (starting from front v. starting from back) - result in the same sequence */ - lemma LemmaFlattenAndFlattenReverseAreEquivalent(s: seq>) - ensures Flatten(s) == FlattenReverse(s) - { - if |s| == 0 { - } else { - calc == { - FlattenReverse(s); - FlattenReverse(DropLast(s)) + Last(s); - { LemmaFlattenAndFlattenReverseAreEquivalent(DropLast(s)); } - Flatten(DropLast(s)) + Last(s); - Flatten(DropLast(s)) + Flatten([Last(s)]); - { LemmaFlattenConcat(DropLast(s), [Last(s)]); - assert s == DropLast(s) + [Last(s)]; } - Flatten(s); - } - } - } - - /* the concatenated sequence's length is greater than or equal to each individual - inner sequence's length */ - lemma LemmaFlattenLengthGeSingleElementLength(s: seq>, i: int) - requires 0 <= i < |s| - ensures |FlattenReverse(s)| >= |s[i]| - { - if i < |s| - 1 { - LemmaFlattenLengthGeSingleElementLength(s[..|s|-1], i); - } - } - - /* the length of concatenating sequence in a sequence together will be no longer - than the length of the original sequence of sequences multiplied by the length of - the longest sequence */ - lemma LemmaFlattenLengthLeMul(s: seq>, j: int) - requires forall i {:trigger s[i]} | 0 <= i < |s| :: |s[i]| <= j - ensures |FlattenReverse(s)| <= |s| * j - { - if |s| == 0 { - } else { - LemmaFlattenLengthLeMul(s[..|s|-1], j); - } - } - - - /********************************************************** - * - * Higher-Order Sequence Functions - * - ***********************************************************/ - - /* applies a transformation function on the sequence */ - function method {:opaque} Map(f: (T ~> R), s: seq): (result: seq) - requires forall i {:trigger s[i]} :: 0 <= i < |s| ==> f.requires(s[i]) - ensures |result| == |s| - ensures forall i {:trigger result[i]}:: 0 <= i < |s| ==> result[i] == f(s[i]); - reads set i, o {:trigger o in f.reads(s[i])} | 0 <= i < |s| && o in f.reads(s[i]):: o - { - if |s| == 0 then [] - else [f(s[0])] + Map(f, s[1..]) - } - - /* concatenating two sequences and then applying Map is the same as applying - Map on each sequence seperately and then concatenating the two resulting - sequences */ - lemma {:opaque} LemmaMapDistributesOverConcat(f: (T ~> R), a: seq, b: seq) - requires forall i {:trigger a[i]}:: 0 <= i < |a| ==> f.requires(a[i]) - requires forall j {:trigger b[j]}:: 0 <= j < |b| ==> f.requires(b[j]) - ensures Map(f, a + b) == Map(f, a) + Map(f, b) - { - reveal Map(); - if |a| == 0 { - assert a + b == b; - } else { - calc { - Map(f, a + b); - { assert (a + b)[0] == a[0]; assert (a + b)[1..] == a[1..] + b; } - Map(f, [a[0]]) + Map(f, a[1..] + b); - Map(f, [a[0]]) + Map(f, a[1..]) + Map(f, b); - {assert [(a + b)[0]] + a[1..] + b == a + b;} - Map(f, a) + Map(f, b); - } - } - } - - /* uses a selection function to select elements from the sequence */ - function method {:opaque} Filter(f: (T ~> bool), s: seq): (result: seq) - requires forall i :: 0 <= i < |s| ==> f.requires(s[i]) - ensures |result| <= |s| - ensures forall i: nat {:trigger result[i]} :: i < |result| && f.requires(result[i]) ==> f(result[i]) - reads f.reads - { - if |s| == 0 then [] - else (if f(s[0]) then [s[0]] else []) + Filter(f, s[1..]) - } - - /* concatenating two sequences and then using "filter" is the same as using "filter" on each sequences - seperately and then concatenating their resulting sequences */ - lemma {:opaque} LemmaFilterDistributesOverConcat(f: (T ~> bool), a: seq, b: seq) - requires forall i {:trigger a[i]}:: 0 <= i < |a| ==> f.requires(a[i]) - requires forall j {:trigger b[j]}:: 0 <= j < |b| ==> f.requires(b[j]) - ensures Filter(f, a + b) == Filter(f, a) + Filter(f, b) - { - reveal Filter(); - if |a| == 0 { - assert a + b == b; - } else { - calc { - Filter(f, a + b); - { assert (a + b)[0] == a[0]; assert (a + b)[1..] == a[1..] + b; } - Filter(f, [a[0]]) + Filter(f, a[1..] + b); - Filter(f, [a[0]]) + Filter(f, a[1..]) + Filter(f, b); - { assert [(a + b)[0]] + a[1..] + b == a + b; } - Filter(f, a) + Filter(f, b); - } - } - } + // /* unzips a sequence that contains ordered pairs into 2 seperate sequences */ + // function method {:opaque} Unzip(s: seq<(A, B)>): (seq, seq) + // ensures |Unzip(s).0| == |Unzip(s).1| == |s| + // ensures forall i {:trigger Unzip(s).0[i]} {:trigger Unzip(s).1[i]} + // :: 0 <= i < |s| ==> (Unzip(s).0[i], Unzip(s).1[i]) == s[i] + // { + // if |s| == 0 then ([], []) + // else + // var (a, b):= Unzip(DropLast(s)); + // (a + [Last(s).0], b + [Last(s).1]) + // } + + // /* takes two sequences, a and b, and combines then to form one sequence in which + // each position contains an ordered pair from a and b */ + // function method {:opaque} Zip(a: seq, b: seq): seq<(A, B)> + // requires |a| == |b| + // ensures |Zip(a, b)| == |a| + // ensures forall i {:trigger Zip(a, b)[i]}:: 0 <= i < |Zip(a, b)| ==> Zip(a, b)[i] == (a[i], b[i]) + // ensures Unzip(Zip(a, b)).0 == a + // ensures Unzip(Zip(a, b)).1 == b + // { + // if |a| == 0 then [] + // else Zip(DropLast(a), DropLast(b)) + [(Last(a), Last(b))] + // } + + // /* if a sequence is unzipped and then zipped, it forms the original sequence */ + // lemma LemmaZipOfUnzip(s: seq<(A,B)>) + // ensures Zip(Unzip(s).0, Unzip(s).1) == s + // { + // } + + // /********************************************************** + // * + // * Extrema in Sequences + // * + // ***********************************************************/ + + // /* finds the maximum integer value in the sequence */ + // function method {:opaque} Max(s: seq): int + // requires 0 < |s| + // ensures forall k {:trigger k in s} :: k in s ==> Max(s) >= k + // ensures Max(s) in s + // { + // assert s == [s[0]] + s[1..]; + // if |s| == 1 then s[0] else Math.Max(s[0], Max(s[1..])) + // } + + // /* the greater maximum value of two sequences, a and b, becomes the maximum of the total sequence when + // a and b are concatenated */ + // lemma LemmaMaxOfConcat(a: seq, b: seq) + // requires 0 < |a| && 0 < |b| + // ensures Max(a+b) >= Max(a) + // ensures Max(a+b) >= Max(b) + // ensures forall i {:trigger i in [Max(a + b)]} :: i in a + b ==> Max(a + b) >= i + // { + // reveal Max(); + // if |a| == 1 { + // } else { + // assert a[1..] + b == (a + b)[1..]; + // LemmaMaxOfConcat(a[1..], b); + // } + // } + + // /* finds the minimum integer value in the sequence */ + // function method {:opaque} Min(s: seq): int + // requires 0 < |s| + // ensures forall k {:trigger k in s} :: k in s ==> Min(s) <= k + // ensures Min(s) in s + // { + // assert s == [s[0]] + s[1..]; + // if |s| == 1 then s[0] else Math.Min(s[0], Min(s[1..])) + // } + + // /* the smaller minimum value of two sequences, a and b, becomes the minimum of the total sequence when + // a and b are concatenated */ + // lemma LemmaMinOfConcat(a: seq, b: seq) + // requires 0 < |a| && 0 < |b| + // ensures Min(a+b) <= Min(a) + // ensures Min(a+b) <= Min(b) + // ensures forall i {:trigger i in a + b} :: i in a + b ==> Min(a + b) <= i + // { + // reveal Min(); + // if |a| == 1 { + // } else { + // assert a[1..] + b == (a + b)[1..]; + // LemmaMinOfConcat(a[1..], b); + // } + // } + + // /* the maximum element in any subsequence will not be greater than the maximum element in + // the full sequence */ + // lemma LemmaSubseqMax(s: seq, from: nat, to: nat) + // requires from < to <= |s| + // ensures Max(s[from..to]) <= Max(s) + // { + // var subseq := s[from..to]; + // if Max(subseq) > Max(s) { + // var k :| 0 <= k < |subseq| && subseq[k] == Max(subseq); + // assert s[seq(|subseq|, i requires 0 <= i < |subseq| => i + from)[k]] in s; + // assert false; + // } + // } + + // /* the minimum element in any subsequence will not be less than the minimum element in + // the full sequence */ + // lemma LemmaSubseqMin(s: seq, from: nat, to: nat) + // requires from < to <= |s| + // ensures Min(s[from..to]) >= Min(s) + // { + // var subseq := s[from..to]; + // if Min(subseq) < Min(s) { + // var k :| 0 <= k < |subseq| && subseq[k] == Min(subseq); + // assert s[seq(|subseq|, i requires 0 <= i < |subseq| => i + from)[k]] in s; + // } + // } + + // /********************************************************** + // * + // * Sequences of Sequences + // * + // ***********************************************************/ + + // /*concatenates a sequence of sequences into a single sequence. Works by adding + // elements in order from first to last */ + // function method Flatten(s: seq>): seq + // decreases |s| + // { + // if |s| == 0 then [] + // else s[0] + Flatten(s[1..]) + // } + + // /* concatenating two sequences of sequences is equivalent to concatenating + // each sequence of sequences seperately, and then concatenating the two resulting + // sequences together */ + // lemma LemmaFlattenConcat(a: seq>, b: seq>) + // ensures Flatten(a + b) == Flatten(a) + Flatten(b) + // { + // if |a| == 0 { + // assert a + b == b; + // } else { + // calc == { + // Flatten(a + b); + // { assert (a + b)[0] == a[0]; assert (a + b)[1..] == a[1..] + b; } + // a[0] + Flatten(a[1..] + b); + // a[0] + Flatten(a[1..]) + Flatten(b); + // Flatten(a) + Flatten(b); + // } + // } + // } + + // /* concatenates the sequence of sequences into a single sequence. Works by concatenating + // elements from last to first */ + // function method FlattenReverse(s: seq>): seq + // decreases |s| + // { + // if |s| == 0 then [] + // else FlattenReverse(DropLast(s)) + Last(s) + // } + + // /* concatenating two reversed sequences of sequences is the same as reversing two + // sequences of sequences and then concattenating the two resulting sequences together */ + // lemma LemmaFlattenReverseConcat(a: seq>, b: seq>) + // ensures FlattenReverse(a + b) == FlattenReverse(a) + FlattenReverse(b) + // { + // if |b| == 0 { + // assert FlattenReverse(b) == []; + // assert a + b == a; + // } else { + // calc == { + // FlattenReverse(a + b); + // { assert Last(a + b) == Last(b); assert DropLast(a + b) == a + DropLast(b); } + // FlattenReverse(a + DropLast(b)) + Last(b); + // FlattenReverse(a) + FlattenReverse(DropLast(b)) + Last(b); + // FlattenReverse(a) + FlattenReverse(b); + // } + // } + // } + + // /* both methods of concatenating sequence (starting from front v. starting from back) + // result in the same sequence */ + // lemma LemmaFlattenAndFlattenReverseAreEquivalent(s: seq>) + // ensures Flatten(s) == FlattenReverse(s) + // { + // if |s| == 0 { + // } else { + // calc == { + // FlattenReverse(s); + // FlattenReverse(DropLast(s)) + Last(s); + // { LemmaFlattenAndFlattenReverseAreEquivalent(DropLast(s)); } + // Flatten(DropLast(s)) + Last(s); + // Flatten(DropLast(s)) + Flatten([Last(s)]); + // { LemmaFlattenConcat(DropLast(s), [Last(s)]); + // assert s == DropLast(s) + [Last(s)]; } + // Flatten(s); + // } + // } + // } + + // /* the concatenated sequence's length is greater than or equal to each individual + // inner sequence's length */ + // lemma LemmaFlattenLengthGeSingleElementLength(s: seq>, i: int) + // requires 0 <= i < |s| + // ensures |FlattenReverse(s)| >= |s[i]| + // { + // if i < |s| - 1 { + // LemmaFlattenLengthGeSingleElementLength(s[..|s|-1], i); + // } + // } + + // /* the length of concatenating sequence in a sequence together will be no longer + // than the length of the original sequence of sequences multiplied by the length of + // the longest sequence */ + // lemma LemmaFlattenLengthLeMul(s: seq>, j: int) + // requires forall i {:trigger s[i]} | 0 <= i < |s| :: |s[i]| <= j + // ensures |FlattenReverse(s)| <= |s| * j + // { + // if |s| == 0 { + // } else { + // LemmaFlattenLengthLeMul(s[..|s|-1], j); + // } + // } + + + // /********************************************************** + // * + // * Higher-Order Sequence Functions + // * + // ***********************************************************/ + + // /* applies a transformation function on the sequence */ + // function method {:opaque} Map(f: (T ~> R), s: seq): (result: seq) + // requires forall i {:trigger s[i]} :: 0 <= i < |s| ==> f.requires(s[i]) + // ensures |result| == |s| + // ensures forall i {:trigger result[i]}:: 0 <= i < |s| ==> result[i] == f(s[i]); + // reads set i, o {:trigger o in f.reads(s[i])} | 0 <= i < |s| && o in f.reads(s[i]):: o + // { + // if |s| == 0 then [] + // else [f(s[0])] + Map(f, s[1..]) + // } + + // /* concatenating two sequences and then applying Map is the same as applying + // Map on each sequence seperately and then concatenating the two resulting + // sequences */ + // lemma {:opaque} LemmaMapDistributesOverConcat(f: (T ~> R), a: seq, b: seq) + // requires forall i {:trigger a[i]}:: 0 <= i < |a| ==> f.requires(a[i]) + // requires forall j {:trigger b[j]}:: 0 <= j < |b| ==> f.requires(b[j]) + // ensures Map(f, a + b) == Map(f, a) + Map(f, b) + // { + // reveal Map(); + // if |a| == 0 { + // assert a + b == b; + // } else { + // calc { + // Map(f, a + b); + // { assert (a + b)[0] == a[0]; assert (a + b)[1..] == a[1..] + b; } + // Map(f, [a[0]]) + Map(f, a[1..] + b); + // Map(f, [a[0]]) + Map(f, a[1..]) + Map(f, b); + // {assert [(a + b)[0]] + a[1..] + b == a + b;} + // Map(f, a) + Map(f, b); + // } + // } + // } + + // /* uses a selection function to select elements from the sequence */ + // function method {:opaque} Filter(f: (T ~> bool), s: seq): (result: seq) + // requires forall i :: 0 <= i < |s| ==> f.requires(s[i]) + // ensures |result| <= |s| + // ensures forall i: nat {:trigger result[i]} :: i < |result| && f.requires(result[i]) ==> f(result[i]) + // reads f.reads + // { + // if |s| == 0 then [] + // else (if f(s[0]) then [s[0]] else []) + Filter(f, s[1..]) + // } + + // /* concatenating two sequences and then using "filter" is the same as using "filter" on each sequences + // seperately and then concatenating their resulting sequences */ + // lemma {:opaque} LemmaFilterDistributesOverConcat(f: (T ~> bool), a: seq, b: seq) + // requires forall i {:trigger a[i]}:: 0 <= i < |a| ==> f.requires(a[i]) + // requires forall j {:trigger b[j]}:: 0 <= j < |b| ==> f.requires(b[j]) + // ensures Filter(f, a + b) == Filter(f, a) + Filter(f, b) + // { + // reveal Filter(); + // if |a| == 0 { + // assert a + b == b; + // } else { + // calc { + // Filter(f, a + b); + // { assert (a + b)[0] == a[0]; assert (a + b)[1..] == a[1..] + b; } + // Filter(f, [a[0]]) + Filter(f, a[1..] + b); + // Filter(f, [a[0]]) + Filter(f, a[1..]) + Filter(f, b); + // { assert [(a + b)[0]] + a[1..] + b == a + b; } + // Filter(f, a) + Filter(f, b); + // } + // } + // } - function method {:opaque} FoldLeft(f: (A, T) -> A, init: A, s: seq): A - { - if |s| == 0 then init - else FoldLeft(f, f(init, s[0]), s[1..]) - } - - /* Concatenating two sequences, then folding left is the same as folding the first sequence and using the result as the initial value to fold the second - sequence. */ - lemma {:opaque} LemmaFoldLeftDistributesOverConcat(f: (A, T) -> A, init: A, a: seq, b: seq) - requires 0 <= |a + b| - ensures FoldLeft(f, init, a + b) == FoldLeft(f, FoldLeft(f, init, a), b) - { - reveal FoldLeft(); - if |a| == 0 { - assert a + b == b; - } else { - assert |a| >= 1; - assert ([a[0]] + a[1..] + b)[0] == a[0]; - calc { - FoldLeft(f, FoldLeft(f, init, a), b); - FoldLeft(f, FoldLeft(f, f(init, a[0]), a[1..]), b); - { LemmaFoldLeftDistributesOverConcat(f, f(init, a[0]), a[1..], b); } - FoldLeft(f, f(init, a[0]), a[1..] + b); - { assert (a + b)[0] == a[0]; - assert (a + b)[1..] == a[1..] + b; } - FoldLeft(f, init, a + b); - } - } - } - - /* inv is an invariant under stp, which is a relational version of the - function f passed to fold. */ - predicate InvFoldLeft(inv: (B, seq) -> bool, - stp: (B, A, B) -> bool) - { - forall x: A, xs: seq, b: B, b': B :: - inv(b, [x] + xs) && stp(b, x, b') ==> inv(b', xs) - } - - /* inv(b, xs) ==> inv(FoldLeft(f, b, xs), []). */ - lemma LemmaInvFoldLeft(inv: (B, seq) -> bool, - stp: (B, A, B) -> bool, - f: (B, A) -> B, - b: B, - xs: seq) - requires InvFoldLeft(inv, stp) - requires forall b, a :: stp(b, a, f(b, a)) - requires inv(b, xs) - ensures inv(FoldLeft(f, b, xs), []) - { - reveal FoldLeft(); - if xs == [] { - } else { - assert [xs[0]] + xs[1..] == xs; - LemmaInvFoldLeft(inv, stp, f, f(b, xs[0]), xs[1..]); - } - } - - function method {:opaque} FoldRight(f: (T, A) -> A, s: seq, init: A): A - { - if |s| == 0 then init - else f(s[0], FoldRight(f, s[1..], init)) - } - - /* Concatenating two sequences, then folding right is the same as folding the second sequence and using the result as the initial value to fold the first - sequence. */ - lemma {:opaque} LemmaFoldRightDistributesOverConcat(f: (T, A) -> A, init: A, a: seq, b: seq) - requires 0 <= |a + b| - ensures FoldRight(f, a + b, init) == FoldRight(f, a, FoldRight(f, b, init)) - { - reveal FoldRight(); - if |a| == 0 { - assert a + b == b; - } else { - calc { - FoldRight(f, a, FoldRight(f, b, init)); - f(a[0], FoldRight(f, a[1..], FoldRight(f, b, init))); - f(a[0], FoldRight(f, a[1..] + b, init)); - { assert (a + b)[0] == a[0]; - assert (a + b)[1..] == a[1..] + b; } - FoldRight(f, a + b, init); - } - } - } - - /* inv is an invariant under stp, which is a relational version of the - function f passed to fold. */ - predicate InvFoldRight(inv: (seq, B) -> bool, - stp: (A, B, B) -> bool) - { - forall x: A, xs: seq, b: B, b': B :: - inv(xs, b) && stp(x, b, b') ==> inv(([x] + xs), b') - } - - /* inv([], b) ==> inv(xs, FoldRight(f, xs, b)) */ - lemma LemmaInvFoldRight(inv: (seq, B) -> bool, - stp: (A, B, B) -> bool, - f: (A, B) -> B, - b: B, - xs: seq) - requires InvFoldRight(inv, stp) - requires forall a, b :: stp(a, b, f(a, b)) - requires inv([], b) - ensures inv(xs, FoldRight(f, xs, b)) - { - reveal FoldRight(); - if xs == [] { - } else { - assert [xs[0]] + xs[1..] == xs; - } - } + // function method {:opaque} FoldLeft(f: (A, T) -> A, init: A, s: seq): A + // { + // if |s| == 0 then init + // else FoldLeft(f, f(init, s[0]), s[1..]) + // } + + // /* Concatenating two sequences, then folding left is the same as folding the first sequence and using the result as the initial value to fold the second + // sequence. */ + // lemma {:opaque} LemmaFoldLeftDistributesOverConcat(f: (A, T) -> A, init: A, a: seq, b: seq) + // requires 0 <= |a + b| + // ensures FoldLeft(f, init, a + b) == FoldLeft(f, FoldLeft(f, init, a), b) + // { + // reveal FoldLeft(); + // if |a| == 0 { + // assert a + b == b; + // } else { + // assert |a| >= 1; + // assert ([a[0]] + a[1..] + b)[0] == a[0]; + // calc { + // FoldLeft(f, FoldLeft(f, init, a), b); + // FoldLeft(f, FoldLeft(f, f(init, a[0]), a[1..]), b); + // { LemmaFoldLeftDistributesOverConcat(f, f(init, a[0]), a[1..], b); } + // FoldLeft(f, f(init, a[0]), a[1..] + b); + // { assert (a + b)[0] == a[0]; + // assert (a + b)[1..] == a[1..] + b; } + // FoldLeft(f, init, a + b); + // } + // } + // } + + // /* inv is an invariant under stp, which is a relational version of the + // function f passed to fold. */ + // predicate InvFoldLeft(inv: (B, seq) -> bool, + // stp: (B, A, B) -> bool) + // { + // forall x: A, xs: seq, b: B, b': B :: + // inv(b, [x] + xs) && stp(b, x, b') ==> inv(b', xs) + // } + + // /* inv(b, xs) ==> inv(FoldLeft(f, b, xs), []). */ + // lemma LemmaInvFoldLeft(inv: (B, seq) -> bool, + // stp: (B, A, B) -> bool, + // f: (B, A) -> B, + // b: B, + // xs: seq) + // requires InvFoldLeft(inv, stp) + // requires forall b, a :: stp(b, a, f(b, a)) + // requires inv(b, xs) + // ensures inv(FoldLeft(f, b, xs), []) + // { + // reveal FoldLeft(); + // if xs == [] { + // } else { + // assert [xs[0]] + xs[1..] == xs; + // LemmaInvFoldLeft(inv, stp, f, f(b, xs[0]), xs[1..]); + // } + // } + + // function method {:opaque} FoldRight(f: (T, A) -> A, s: seq, init: A): A + // { + // if |s| == 0 then init + // else f(s[0], FoldRight(f, s[1..], init)) + // } + + // /* Concatenating two sequences, then folding right is the same as folding the second sequence and using the result as the initial value to fold the first + // sequence. */ + // lemma {:opaque} LemmaFoldRightDistributesOverConcat(f: (T, A) -> A, init: A, a: seq, b: seq) + // requires 0 <= |a + b| + // ensures FoldRight(f, a + b, init) == FoldRight(f, a, FoldRight(f, b, init)) + // { + // reveal FoldRight(); + // if |a| == 0 { + // assert a + b == b; + // } else { + // calc { + // FoldRight(f, a, FoldRight(f, b, init)); + // f(a[0], FoldRight(f, a[1..], FoldRight(f, b, init))); + // f(a[0], FoldRight(f, a[1..] + b, init)); + // { assert (a + b)[0] == a[0]; + // assert (a + b)[1..] == a[1..] + b; } + // FoldRight(f, a + b, init); + // } + // } + // } + + // /* inv is an invariant under stp, which is a relational version of the + // function f passed to fold. */ + // predicate InvFoldRight(inv: (seq, B) -> bool, + // stp: (A, B, B) -> bool) + // { + // forall x: A, xs: seq, b: B, b': B :: + // inv(xs, b) && stp(x, b, b') ==> inv(([x] + xs), b') + // } + + // /* inv([], b) ==> inv(xs, FoldRight(f, xs, b)) */ + // lemma LemmaInvFoldRight(inv: (seq, B) -> bool, + // stp: (A, B, B) -> bool, + // f: (A, B) -> B, + // b: B, + // xs: seq) + // requires InvFoldRight(inv, stp) + // requires forall a, b :: stp(a, b, f(a, b)) + // requires inv([], b) + // ensures inv(xs, FoldRight(f, xs, b)) + // { + // reveal FoldRight(); + // if xs == [] { + // } else { + // assert [xs[0]] + xs[1..] == xs; + // } + // } } From 13214c9dbd046181b0d1517198d1457449705af8 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Sat, 2 Oct 2021 17:09:18 -0700 Subject: [PATCH 2/3] Verifies, now let's clean it up --- src/Collections/Multisets/Multiset.dfy | 32 ++++++++++++++++++-------- src/Collections/Sequences/Seq.dfy | 6 +++-- 2 files changed, 26 insertions(+), 12 deletions(-) diff --git a/src/Collections/Multisets/Multiset.dfy b/src/Collections/Multisets/Multiset.dfy index 347af652..cb575269 100644 --- a/src/Collections/Multisets/Multiset.dfy +++ b/src/Collections/Multisets/Multiset.dfy @@ -29,15 +29,9 @@ module Multiset { } } - lemma LemmaToSetOfDisjointUnion(a: multiset, b: multiset) - requires a !! b - ensures ToSet(a + b) == ToSet(a) + ToSet(b) - { - } - /* proves that the cardinality of a multiset is always more than or equal to that of the conversion to a set */ - lemma LemmaCardinalityOfSet(s: multiset) + lemma LemmaCardinalityOfSetBound(s: multiset) ensures |ToSet(s)| <= |s| { reveal ToSet(); @@ -47,10 +41,28 @@ module Multiset { var xs := multiset{}[x := s[x]]; assert ToSet(xs) == {x}; var rest := s - xs; - LemmaCardinalityOfSet(rest); - LemmaToSetOfDisjointUnion(xs, rest); - assert |s| == |xs| + |rest|; + LemmaCardinalityOfSetBound(rest); + assert ToSet(s) == ToSet(xs) + ToSet(rest); + } + } + + lemma LemmaCardinalityOfSet(s: multiset, e: T) + requires s[e] > 1 + ensures |ToSet(s)| < |s| + { + reveal ToSet(); + if |s| == 0 { + } else { + var x :| x in s && s[x] > 1; + var xs := multiset{}[x := s[x]]; + assert ToSet(xs) == {x}; + var rest := s - xs; + LemmaCardinalityOfSetBound(rest); assert ToSet(s) == ToSet(xs) + ToSet(rest); + assert ToSet(xs) !! ToSet(rest); + assert |ToSet(s)| == |ToSet(xs)| + |ToSet(rest)|; + assert |ToSet(s)| <= |ToSet(xs)| + |rest|; + assert |xs| > 1; } } } \ No newline at end of file diff --git a/src/Collections/Sequences/Seq.dfy b/src/Collections/Sequences/Seq.dfy index 61de3539..1f91aa32 100644 --- a/src/Collections/Sequences/Seq.dfy +++ b/src/Collections/Sequences/Seq.dfy @@ -209,12 +209,14 @@ module Seq { { reveal HasNoDuplicates(); reveal ToSet(); + reveal Multiset.ToSet(); if i,j :| 0 <= i < j < |s| && s[i] == s[j] { var x := s[i]; assert s == s[..j] + s[j..]; assert multiset(s)[x] >= 2; - Multiset.LemmaCardinalityOfSet(multiset(s)); - assert |multiset(s)| < |s|; + Multiset.LemmaCardinalityOfSet(multiset(s), x); + assert ToSet(s) == Multiset.ToSet(multiset(s)); + assert |ToSet(s)| < |s|; } } From c502c4aaeac359cd357f85066ead38aa6ef40bda Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Sat, 2 Oct 2021 18:16:51 -0700 Subject: [PATCH 3/3] Cleanup --- src/Collections/Multisets/Multiset.dfy | 54 +- src/Collections/Multisets/Multiset.dfy.expect | 2 + src/Collections/Sequences/Seq.dfy | 1012 +++++++++-------- src/Collections/Sequences/Seq.dfy.expect | 2 +- 4 files changed, 526 insertions(+), 544 deletions(-) create mode 100644 src/Collections/Multisets/Multiset.dfy.expect diff --git a/src/Collections/Multisets/Multiset.dfy b/src/Collections/Multisets/Multiset.dfy index cb575269..0fb997d1 100644 --- a/src/Collections/Multisets/Multiset.dfy +++ b/src/Collections/Multisets/Multiset.dfy @@ -14,55 +14,33 @@ module Multiset { set x: T | x in s } - lemma LemmaSingletonSize(s: multiset, e: T) - requires e in s - requires forall e' | e' in s && e' != e :: s[e'] == 0 - decreases s[e] - ensures |s| == s[e] - { - reveal ToSet(); - if s[e] == 1 { - assert s == multiset{e}; - } else { - var s' := s[e := s[e] - 1]; - LemmaSingletonSize(s', e); - } - } - /* proves that the cardinality of a multiset is always more than or equal to that of the conversion to a set */ - lemma LemmaCardinalityOfSetBound(s: multiset) - ensures |ToSet(s)| <= |s| + lemma LemmaCardinalityOfSetBound(m: multiset) + ensures |ToSet(m)| <= |m| { reveal ToSet(); - if |s| == 0 { + if |m| == 0 { } else { - var x :| x in s; - var xs := multiset{}[x := s[x]]; + var x :| x in m; + var xs := multiset{}[x := m[x]]; assert ToSet(xs) == {x}; - var rest := s - xs; + var rest := m - xs; LemmaCardinalityOfSetBound(rest); - assert ToSet(s) == ToSet(xs) + ToSet(rest); + assert ToSet(m) == ToSet(xs) + ToSet(rest); } } - lemma LemmaCardinalityOfSet(s: multiset, e: T) - requires s[e] > 1 - ensures |ToSet(s)| < |s| + lemma LemmaCardinalityOfSetWithDuplicates(m: multiset, x: T) + requires m[x] > 1 + ensures |ToSet(m)| < |m| { reveal ToSet(); - if |s| == 0 { - } else { - var x :| x in s && s[x] > 1; - var xs := multiset{}[x := s[x]]; - assert ToSet(xs) == {x}; - var rest := s - xs; - LemmaCardinalityOfSetBound(rest); - assert ToSet(s) == ToSet(xs) + ToSet(rest); - assert ToSet(xs) !! ToSet(rest); - assert |ToSet(s)| == |ToSet(xs)| + |ToSet(rest)|; - assert |ToSet(s)| <= |ToSet(xs)| + |rest|; - assert |xs| > 1; - } + var xs := multiset{}[x := m[x]]; + assert ToSet(xs) == {x}; + var rest := m - xs; + LemmaCardinalityOfSetBound(rest); + assert ToSet(m) == ToSet(xs) + ToSet(rest); + assert |xs| > 1; } } \ No newline at end of file diff --git a/src/Collections/Multisets/Multiset.dfy.expect b/src/Collections/Multisets/Multiset.dfy.expect new file mode 100644 index 00000000..ebe2328e --- /dev/null +++ b/src/Collections/Multisets/Multiset.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 2 verified, 0 errors diff --git a/src/Collections/Sequences/Seq.dfy b/src/Collections/Sequences/Seq.dfy index 1f91aa32..791f6ef9 100644 --- a/src/Collections/Sequences/Seq.dfy +++ b/src/Collections/Sequences/Seq.dfy @@ -210,11 +210,13 @@ module Seq { reveal HasNoDuplicates(); reveal ToSet(); reveal Multiset.ToSet(); + // Proof by contrapositive: if there is a duplicate, then the cardinality of the + // set would be strictly less than that of the sequence, which contradicts the precondition. if i,j :| 0 <= i < j < |s| && s[i] == s[j] { var x := s[i]; assert s == s[..j] + s[j..]; assert multiset(s)[x] >= 2; - Multiset.LemmaCardinalityOfSet(multiset(s), x); + Multiset.LemmaCardinalityOfSetWithDuplicates(multiset(s), x); assert ToSet(s) == Multiset.ToSet(multiset(s)); assert |ToSet(s)| < |s|; } @@ -238,512 +240,512 @@ module Seq { } } - // /* finds the index of the first occurrence of an element in the sequence */ - // function method {:opaque} IndexOf(s: seq, v: T): (i: nat) - // requires v in s - // ensures i < |s| && s[i] == v - // ensures forall j {:trigger s[j]} :: 0 <= j < i ==> s[j] != v - // { - // if s[0] == v then 0 else 1 + IndexOf(s[1..], v) - // } - - // /* finds the index of the first occurrence of an element in the sequence if - // found */ - // function method {:opaque} IndexOfOption(s: seq, v: T): (o: Option) - // ensures if o.Some? then o.value < |s| && s[o.value] == v && - // forall j {:trigger s[j]} :: 0 <= j < o.value ==> s[j] != v - // else v !in s - // { - // if |s| == 0 then None() - // else - // if s[0] == v then Some(0) - // else - // var o' := IndexOfOption(s[1..], v); - // if o'.Some? then Some(o'.value + 1) else None() - // } - - // /* finds the index of the last occurrence of an element in the sequence */ - // function method {:opaque} LastIndexOf(s: seq, v: T): (i: nat) - // requires v in s - // ensures i < |s| && s[i] == v - // ensures forall j {:trigger s[j]} :: i < j < |s| ==> s[j] != v - // { - // if s[|s|-1] == v then |s| - 1 else LastIndexOf(s[..|s|-1], v) - // } - - // /* finds the index of the last occurrence of an element in the sequence if - // found */ - // function method {:opaque} LastIndexOfOption(s: seq, v: T): (o: Option) - // ensures if o.Some? then o.value < |s| && s[o.value] == v && - // forall j {:trigger s[j]} :: o.value < j < |s| ==> s[j] != v - // else v !in s - // { - // if |s| == 0 then None() - // else if s[|s|-1] == v then Some(|s| - 1) else LastIndexOfOption(s[..|s|-1], v) - // } - - // /* slices out a specific position's value from the sequence */ - // function method {:opaque} Remove(s: seq, pos: nat): (s': seq) - // requires pos < |s| - // ensures |s'| == |s| - 1 - // ensures forall i {:trigger s'[i], s[i]} | 0 <= i < pos :: s'[i] == s[i] - // ensures forall i {:trigger s'[i]} | pos <= i < |s| - 1 :: s'[i] == s[i+1] - // { - // s[..pos] + s[pos+1..] - // } - - // /* slices out a specific value from the sequence */ - // function method {:opaque} RemoveValue(s: seq, v: T): (s': seq) - // ensures v !in s ==> s == s' - // ensures v in s ==> |multiset(s')| == |multiset(s)| - 1 - // ensures v in s ==> multiset(s')[v] == multiset(s)[v] - 1 - // ensures HasNoDuplicates(s) ==> HasNoDuplicates(s') && ToSet(s') == ToSet(s) - {v} - // { - // reveal HasNoDuplicates(); - // reveal ToSet(); - // if v !in s then s - // else - // var i := IndexOf(s, v); - // assert s == s[..i] + [v] + s[i+1..]; - // s[..i] + s[i+1..] - // } - - // /* inserts a certain value into a specified index of the sequence */ - // function method {:opaque} Insert(s: seq, a: T, pos: nat): seq - // requires pos <= |s| - // ensures |Insert(s, a, pos)| == |s| + 1 - // ensures forall i {:trigger Insert(s, a, pos)[i], s[i]} :: 0 <= i < pos ==> Insert(s, a, pos)[i] == s[i] - // ensures forall i {:trigger s[i]} :: pos <= i < |s| ==> Insert(s, a, pos)[i+1] == s[i] - // ensures Insert(s, a, pos)[pos] == a - // ensures multiset(Insert(s, a, pos)) == multiset(s) + multiset{a} - // { - // assert s == s[..pos] + s[pos..]; - // s[..pos] + [a] + s[pos..] - // } - - // function method {:opaque} Reverse(s: seq): (s': seq) - // ensures |s'| == |s| - // ensures forall i {:trigger s'[i]}{:trigger s[|s| - i - 1]} :: 0 <= i < |s| ==> s'[i] == s[|s| - i - 1] - // { - // if s == [] then [] else [s[|s|-1]] + Reverse(s[0 .. |s|-1]) - // } + /* finds the index of the first occurrence of an element in the sequence */ + function method {:opaque} IndexOf(s: seq, v: T): (i: nat) + requires v in s + ensures i < |s| && s[i] == v + ensures forall j {:trigger s[j]} :: 0 <= j < i ==> s[j] != v + { + if s[0] == v then 0 else 1 + IndexOf(s[1..], v) + } + + /* finds the index of the first occurrence of an element in the sequence if + found */ + function method {:opaque} IndexOfOption(s: seq, v: T): (o: Option) + ensures if o.Some? then o.value < |s| && s[o.value] == v && + forall j {:trigger s[j]} :: 0 <= j < o.value ==> s[j] != v + else v !in s + { + if |s| == 0 then None() + else + if s[0] == v then Some(0) + else + var o' := IndexOfOption(s[1..], v); + if o'.Some? then Some(o'.value + 1) else None() + } + + /* finds the index of the last occurrence of an element in the sequence */ + function method {:opaque} LastIndexOf(s: seq, v: T): (i: nat) + requires v in s + ensures i < |s| && s[i] == v + ensures forall j {:trigger s[j]} :: i < j < |s| ==> s[j] != v + { + if s[|s|-1] == v then |s| - 1 else LastIndexOf(s[..|s|-1], v) + } + + /* finds the index of the last occurrence of an element in the sequence if + found */ + function method {:opaque} LastIndexOfOption(s: seq, v: T): (o: Option) + ensures if o.Some? then o.value < |s| && s[o.value] == v && + forall j {:trigger s[j]} :: o.value < j < |s| ==> s[j] != v + else v !in s + { + if |s| == 0 then None() + else if s[|s|-1] == v then Some(|s| - 1) else LastIndexOfOption(s[..|s|-1], v) + } + + /* slices out a specific position's value from the sequence */ + function method {:opaque} Remove(s: seq, pos: nat): (s': seq) + requires pos < |s| + ensures |s'| == |s| - 1 + ensures forall i {:trigger s'[i], s[i]} | 0 <= i < pos :: s'[i] == s[i] + ensures forall i {:trigger s'[i]} | pos <= i < |s| - 1 :: s'[i] == s[i+1] + { + s[..pos] + s[pos+1..] + } + + /* slices out a specific value from the sequence */ + function method {:opaque} RemoveValue(s: seq, v: T): (s': seq) + ensures v !in s ==> s == s' + ensures v in s ==> |multiset(s')| == |multiset(s)| - 1 + ensures v in s ==> multiset(s')[v] == multiset(s)[v] - 1 + ensures HasNoDuplicates(s) ==> HasNoDuplicates(s') && ToSet(s') == ToSet(s) - {v} + { + reveal HasNoDuplicates(); + reveal ToSet(); + if v !in s then s + else + var i := IndexOf(s, v); + assert s == s[..i] + [v] + s[i+1..]; + s[..i] + s[i+1..] + } + + /* inserts a certain value into a specified index of the sequence */ + function method {:opaque} Insert(s: seq, a: T, pos: nat): seq + requires pos <= |s| + ensures |Insert(s, a, pos)| == |s| + 1 + ensures forall i {:trigger Insert(s, a, pos)[i], s[i]} :: 0 <= i < pos ==> Insert(s, a, pos)[i] == s[i] + ensures forall i {:trigger s[i]} :: pos <= i < |s| ==> Insert(s, a, pos)[i+1] == s[i] + ensures Insert(s, a, pos)[pos] == a + ensures multiset(Insert(s, a, pos)) == multiset(s) + multiset{a} + { + assert s == s[..pos] + s[pos..]; + s[..pos] + [a] + s[pos..] + } + + function method {:opaque} Reverse(s: seq): (s': seq) + ensures |s'| == |s| + ensures forall i {:trigger s'[i]}{:trigger s[|s| - i - 1]} :: 0 <= i < |s| ==> s'[i] == s[|s| - i - 1] + { + if s == [] then [] else [s[|s|-1]] + Reverse(s[0 .. |s|-1]) + } - // function method {:opaque} Repeat(v: T, length: nat): (s: seq) - // ensures |s| == length - // ensures forall i: nat {:trigger s[i]} | i < |s| :: s[i] == v - // { - // if length == 0 then - // [] - // else - // [v] + Repeat(v, length - 1) - // } + function method {:opaque} Repeat(v: T, length: nat): (s: seq) + ensures |s| == length + ensures forall i: nat {:trigger s[i]} | i < |s| :: s[i] == v + { + if length == 0 then + [] + else + [v] + Repeat(v, length - 1) + } - // /* unzips a sequence that contains ordered pairs into 2 seperate sequences */ - // function method {:opaque} Unzip(s: seq<(A, B)>): (seq, seq) - // ensures |Unzip(s).0| == |Unzip(s).1| == |s| - // ensures forall i {:trigger Unzip(s).0[i]} {:trigger Unzip(s).1[i]} - // :: 0 <= i < |s| ==> (Unzip(s).0[i], Unzip(s).1[i]) == s[i] - // { - // if |s| == 0 then ([], []) - // else - // var (a, b):= Unzip(DropLast(s)); - // (a + [Last(s).0], b + [Last(s).1]) - // } - - // /* takes two sequences, a and b, and combines then to form one sequence in which - // each position contains an ordered pair from a and b */ - // function method {:opaque} Zip(a: seq, b: seq): seq<(A, B)> - // requires |a| == |b| - // ensures |Zip(a, b)| == |a| - // ensures forall i {:trigger Zip(a, b)[i]}:: 0 <= i < |Zip(a, b)| ==> Zip(a, b)[i] == (a[i], b[i]) - // ensures Unzip(Zip(a, b)).0 == a - // ensures Unzip(Zip(a, b)).1 == b - // { - // if |a| == 0 then [] - // else Zip(DropLast(a), DropLast(b)) + [(Last(a), Last(b))] - // } - - // /* if a sequence is unzipped and then zipped, it forms the original sequence */ - // lemma LemmaZipOfUnzip(s: seq<(A,B)>) - // ensures Zip(Unzip(s).0, Unzip(s).1) == s - // { - // } - - // /********************************************************** - // * - // * Extrema in Sequences - // * - // ***********************************************************/ - - // /* finds the maximum integer value in the sequence */ - // function method {:opaque} Max(s: seq): int - // requires 0 < |s| - // ensures forall k {:trigger k in s} :: k in s ==> Max(s) >= k - // ensures Max(s) in s - // { - // assert s == [s[0]] + s[1..]; - // if |s| == 1 then s[0] else Math.Max(s[0], Max(s[1..])) - // } - - // /* the greater maximum value of two sequences, a and b, becomes the maximum of the total sequence when - // a and b are concatenated */ - // lemma LemmaMaxOfConcat(a: seq, b: seq) - // requires 0 < |a| && 0 < |b| - // ensures Max(a+b) >= Max(a) - // ensures Max(a+b) >= Max(b) - // ensures forall i {:trigger i in [Max(a + b)]} :: i in a + b ==> Max(a + b) >= i - // { - // reveal Max(); - // if |a| == 1 { - // } else { - // assert a[1..] + b == (a + b)[1..]; - // LemmaMaxOfConcat(a[1..], b); - // } - // } - - // /* finds the minimum integer value in the sequence */ - // function method {:opaque} Min(s: seq): int - // requires 0 < |s| - // ensures forall k {:trigger k in s} :: k in s ==> Min(s) <= k - // ensures Min(s) in s - // { - // assert s == [s[0]] + s[1..]; - // if |s| == 1 then s[0] else Math.Min(s[0], Min(s[1..])) - // } - - // /* the smaller minimum value of two sequences, a and b, becomes the minimum of the total sequence when - // a and b are concatenated */ - // lemma LemmaMinOfConcat(a: seq, b: seq) - // requires 0 < |a| && 0 < |b| - // ensures Min(a+b) <= Min(a) - // ensures Min(a+b) <= Min(b) - // ensures forall i {:trigger i in a + b} :: i in a + b ==> Min(a + b) <= i - // { - // reveal Min(); - // if |a| == 1 { - // } else { - // assert a[1..] + b == (a + b)[1..]; - // LemmaMinOfConcat(a[1..], b); - // } - // } - - // /* the maximum element in any subsequence will not be greater than the maximum element in - // the full sequence */ - // lemma LemmaSubseqMax(s: seq, from: nat, to: nat) - // requires from < to <= |s| - // ensures Max(s[from..to]) <= Max(s) - // { - // var subseq := s[from..to]; - // if Max(subseq) > Max(s) { - // var k :| 0 <= k < |subseq| && subseq[k] == Max(subseq); - // assert s[seq(|subseq|, i requires 0 <= i < |subseq| => i + from)[k]] in s; - // assert false; - // } - // } - - // /* the minimum element in any subsequence will not be less than the minimum element in - // the full sequence */ - // lemma LemmaSubseqMin(s: seq, from: nat, to: nat) - // requires from < to <= |s| - // ensures Min(s[from..to]) >= Min(s) - // { - // var subseq := s[from..to]; - // if Min(subseq) < Min(s) { - // var k :| 0 <= k < |subseq| && subseq[k] == Min(subseq); - // assert s[seq(|subseq|, i requires 0 <= i < |subseq| => i + from)[k]] in s; - // } - // } - - // /********************************************************** - // * - // * Sequences of Sequences - // * - // ***********************************************************/ - - // /*concatenates a sequence of sequences into a single sequence. Works by adding - // elements in order from first to last */ - // function method Flatten(s: seq>): seq - // decreases |s| - // { - // if |s| == 0 then [] - // else s[0] + Flatten(s[1..]) - // } - - // /* concatenating two sequences of sequences is equivalent to concatenating - // each sequence of sequences seperately, and then concatenating the two resulting - // sequences together */ - // lemma LemmaFlattenConcat(a: seq>, b: seq>) - // ensures Flatten(a + b) == Flatten(a) + Flatten(b) - // { - // if |a| == 0 { - // assert a + b == b; - // } else { - // calc == { - // Flatten(a + b); - // { assert (a + b)[0] == a[0]; assert (a + b)[1..] == a[1..] + b; } - // a[0] + Flatten(a[1..] + b); - // a[0] + Flatten(a[1..]) + Flatten(b); - // Flatten(a) + Flatten(b); - // } - // } - // } - - // /* concatenates the sequence of sequences into a single sequence. Works by concatenating - // elements from last to first */ - // function method FlattenReverse(s: seq>): seq - // decreases |s| - // { - // if |s| == 0 then [] - // else FlattenReverse(DropLast(s)) + Last(s) - // } - - // /* concatenating two reversed sequences of sequences is the same as reversing two - // sequences of sequences and then concattenating the two resulting sequences together */ - // lemma LemmaFlattenReverseConcat(a: seq>, b: seq>) - // ensures FlattenReverse(a + b) == FlattenReverse(a) + FlattenReverse(b) - // { - // if |b| == 0 { - // assert FlattenReverse(b) == []; - // assert a + b == a; - // } else { - // calc == { - // FlattenReverse(a + b); - // { assert Last(a + b) == Last(b); assert DropLast(a + b) == a + DropLast(b); } - // FlattenReverse(a + DropLast(b)) + Last(b); - // FlattenReverse(a) + FlattenReverse(DropLast(b)) + Last(b); - // FlattenReverse(a) + FlattenReverse(b); - // } - // } - // } - - // /* both methods of concatenating sequence (starting from front v. starting from back) - // result in the same sequence */ - // lemma LemmaFlattenAndFlattenReverseAreEquivalent(s: seq>) - // ensures Flatten(s) == FlattenReverse(s) - // { - // if |s| == 0 { - // } else { - // calc == { - // FlattenReverse(s); - // FlattenReverse(DropLast(s)) + Last(s); - // { LemmaFlattenAndFlattenReverseAreEquivalent(DropLast(s)); } - // Flatten(DropLast(s)) + Last(s); - // Flatten(DropLast(s)) + Flatten([Last(s)]); - // { LemmaFlattenConcat(DropLast(s), [Last(s)]); - // assert s == DropLast(s) + [Last(s)]; } - // Flatten(s); - // } - // } - // } - - // /* the concatenated sequence's length is greater than or equal to each individual - // inner sequence's length */ - // lemma LemmaFlattenLengthGeSingleElementLength(s: seq>, i: int) - // requires 0 <= i < |s| - // ensures |FlattenReverse(s)| >= |s[i]| - // { - // if i < |s| - 1 { - // LemmaFlattenLengthGeSingleElementLength(s[..|s|-1], i); - // } - // } - - // /* the length of concatenating sequence in a sequence together will be no longer - // than the length of the original sequence of sequences multiplied by the length of - // the longest sequence */ - // lemma LemmaFlattenLengthLeMul(s: seq>, j: int) - // requires forall i {:trigger s[i]} | 0 <= i < |s| :: |s[i]| <= j - // ensures |FlattenReverse(s)| <= |s| * j - // { - // if |s| == 0 { - // } else { - // LemmaFlattenLengthLeMul(s[..|s|-1], j); - // } - // } - - - // /********************************************************** - // * - // * Higher-Order Sequence Functions - // * - // ***********************************************************/ - - // /* applies a transformation function on the sequence */ - // function method {:opaque} Map(f: (T ~> R), s: seq): (result: seq) - // requires forall i {:trigger s[i]} :: 0 <= i < |s| ==> f.requires(s[i]) - // ensures |result| == |s| - // ensures forall i {:trigger result[i]}:: 0 <= i < |s| ==> result[i] == f(s[i]); - // reads set i, o {:trigger o in f.reads(s[i])} | 0 <= i < |s| && o in f.reads(s[i]):: o - // { - // if |s| == 0 then [] - // else [f(s[0])] + Map(f, s[1..]) - // } - - // /* concatenating two sequences and then applying Map is the same as applying - // Map on each sequence seperately and then concatenating the two resulting - // sequences */ - // lemma {:opaque} LemmaMapDistributesOverConcat(f: (T ~> R), a: seq, b: seq) - // requires forall i {:trigger a[i]}:: 0 <= i < |a| ==> f.requires(a[i]) - // requires forall j {:trigger b[j]}:: 0 <= j < |b| ==> f.requires(b[j]) - // ensures Map(f, a + b) == Map(f, a) + Map(f, b) - // { - // reveal Map(); - // if |a| == 0 { - // assert a + b == b; - // } else { - // calc { - // Map(f, a + b); - // { assert (a + b)[0] == a[0]; assert (a + b)[1..] == a[1..] + b; } - // Map(f, [a[0]]) + Map(f, a[1..] + b); - // Map(f, [a[0]]) + Map(f, a[1..]) + Map(f, b); - // {assert [(a + b)[0]] + a[1..] + b == a + b;} - // Map(f, a) + Map(f, b); - // } - // } - // } - - // /* uses a selection function to select elements from the sequence */ - // function method {:opaque} Filter(f: (T ~> bool), s: seq): (result: seq) - // requires forall i :: 0 <= i < |s| ==> f.requires(s[i]) - // ensures |result| <= |s| - // ensures forall i: nat {:trigger result[i]} :: i < |result| && f.requires(result[i]) ==> f(result[i]) - // reads f.reads - // { - // if |s| == 0 then [] - // else (if f(s[0]) then [s[0]] else []) + Filter(f, s[1..]) - // } - - // /* concatenating two sequences and then using "filter" is the same as using "filter" on each sequences - // seperately and then concatenating their resulting sequences */ - // lemma {:opaque} LemmaFilterDistributesOverConcat(f: (T ~> bool), a: seq, b: seq) - // requires forall i {:trigger a[i]}:: 0 <= i < |a| ==> f.requires(a[i]) - // requires forall j {:trigger b[j]}:: 0 <= j < |b| ==> f.requires(b[j]) - // ensures Filter(f, a + b) == Filter(f, a) + Filter(f, b) - // { - // reveal Filter(); - // if |a| == 0 { - // assert a + b == b; - // } else { - // calc { - // Filter(f, a + b); - // { assert (a + b)[0] == a[0]; assert (a + b)[1..] == a[1..] + b; } - // Filter(f, [a[0]]) + Filter(f, a[1..] + b); - // Filter(f, [a[0]]) + Filter(f, a[1..]) + Filter(f, b); - // { assert [(a + b)[0]] + a[1..] + b == a + b; } - // Filter(f, a) + Filter(f, b); - // } - // } - // } + /* unzips a sequence that contains ordered pairs into 2 seperate sequences */ + function method {:opaque} Unzip(s: seq<(A, B)>): (seq, seq) + ensures |Unzip(s).0| == |Unzip(s).1| == |s| + ensures forall i {:trigger Unzip(s).0[i]} {:trigger Unzip(s).1[i]} + :: 0 <= i < |s| ==> (Unzip(s).0[i], Unzip(s).1[i]) == s[i] + { + if |s| == 0 then ([], []) + else + var (a, b):= Unzip(DropLast(s)); + (a + [Last(s).0], b + [Last(s).1]) + } + + /* takes two sequences, a and b, and combines then to form one sequence in which + each position contains an ordered pair from a and b */ + function method {:opaque} Zip(a: seq, b: seq): seq<(A, B)> + requires |a| == |b| + ensures |Zip(a, b)| == |a| + ensures forall i {:trigger Zip(a, b)[i]}:: 0 <= i < |Zip(a, b)| ==> Zip(a, b)[i] == (a[i], b[i]) + ensures Unzip(Zip(a, b)).0 == a + ensures Unzip(Zip(a, b)).1 == b + { + if |a| == 0 then [] + else Zip(DropLast(a), DropLast(b)) + [(Last(a), Last(b))] + } + + /* if a sequence is unzipped and then zipped, it forms the original sequence */ + lemma LemmaZipOfUnzip(s: seq<(A,B)>) + ensures Zip(Unzip(s).0, Unzip(s).1) == s + { + } + + /********************************************************** + * + * Extrema in Sequences + * + ***********************************************************/ + + /* finds the maximum integer value in the sequence */ + function method {:opaque} Max(s: seq): int + requires 0 < |s| + ensures forall k {:trigger k in s} :: k in s ==> Max(s) >= k + ensures Max(s) in s + { + assert s == [s[0]] + s[1..]; + if |s| == 1 then s[0] else Math.Max(s[0], Max(s[1..])) + } + + /* the greater maximum value of two sequences, a and b, becomes the maximum of the total sequence when + a and b are concatenated */ + lemma LemmaMaxOfConcat(a: seq, b: seq) + requires 0 < |a| && 0 < |b| + ensures Max(a+b) >= Max(a) + ensures Max(a+b) >= Max(b) + ensures forall i {:trigger i in [Max(a + b)]} :: i in a + b ==> Max(a + b) >= i + { + reveal Max(); + if |a| == 1 { + } else { + assert a[1..] + b == (a + b)[1..]; + LemmaMaxOfConcat(a[1..], b); + } + } + + /* finds the minimum integer value in the sequence */ + function method {:opaque} Min(s: seq): int + requires 0 < |s| + ensures forall k {:trigger k in s} :: k in s ==> Min(s) <= k + ensures Min(s) in s + { + assert s == [s[0]] + s[1..]; + if |s| == 1 then s[0] else Math.Min(s[0], Min(s[1..])) + } + + /* the smaller minimum value of two sequences, a and b, becomes the minimum of the total sequence when + a and b are concatenated */ + lemma LemmaMinOfConcat(a: seq, b: seq) + requires 0 < |a| && 0 < |b| + ensures Min(a+b) <= Min(a) + ensures Min(a+b) <= Min(b) + ensures forall i {:trigger i in a + b} :: i in a + b ==> Min(a + b) <= i + { + reveal Min(); + if |a| == 1 { + } else { + assert a[1..] + b == (a + b)[1..]; + LemmaMinOfConcat(a[1..], b); + } + } + + /* the maximum element in any subsequence will not be greater than the maximum element in + the full sequence */ + lemma LemmaSubseqMax(s: seq, from: nat, to: nat) + requires from < to <= |s| + ensures Max(s[from..to]) <= Max(s) + { + var subseq := s[from..to]; + if Max(subseq) > Max(s) { + var k :| 0 <= k < |subseq| && subseq[k] == Max(subseq); + assert s[seq(|subseq|, i requires 0 <= i < |subseq| => i + from)[k]] in s; + assert false; + } + } + + /* the minimum element in any subsequence will not be less than the minimum element in + the full sequence */ + lemma LemmaSubseqMin(s: seq, from: nat, to: nat) + requires from < to <= |s| + ensures Min(s[from..to]) >= Min(s) + { + var subseq := s[from..to]; + if Min(subseq) < Min(s) { + var k :| 0 <= k < |subseq| && subseq[k] == Min(subseq); + assert s[seq(|subseq|, i requires 0 <= i < |subseq| => i + from)[k]] in s; + } + } + + /********************************************************** + * + * Sequences of Sequences + * + ***********************************************************/ + + /*concatenates a sequence of sequences into a single sequence. Works by adding + elements in order from first to last */ + function method Flatten(s: seq>): seq + decreases |s| + { + if |s| == 0 then [] + else s[0] + Flatten(s[1..]) + } + + /* concatenating two sequences of sequences is equivalent to concatenating + each sequence of sequences seperately, and then concatenating the two resulting + sequences together */ + lemma LemmaFlattenConcat(a: seq>, b: seq>) + ensures Flatten(a + b) == Flatten(a) + Flatten(b) + { + if |a| == 0 { + assert a + b == b; + } else { + calc == { + Flatten(a + b); + { assert (a + b)[0] == a[0]; assert (a + b)[1..] == a[1..] + b; } + a[0] + Flatten(a[1..] + b); + a[0] + Flatten(a[1..]) + Flatten(b); + Flatten(a) + Flatten(b); + } + } + } + + /* concatenates the sequence of sequences into a single sequence. Works by concatenating + elements from last to first */ + function method FlattenReverse(s: seq>): seq + decreases |s| + { + if |s| == 0 then [] + else FlattenReverse(DropLast(s)) + Last(s) + } + + /* concatenating two reversed sequences of sequences is the same as reversing two + sequences of sequences and then concattenating the two resulting sequences together */ + lemma LemmaFlattenReverseConcat(a: seq>, b: seq>) + ensures FlattenReverse(a + b) == FlattenReverse(a) + FlattenReverse(b) + { + if |b| == 0 { + assert FlattenReverse(b) == []; + assert a + b == a; + } else { + calc == { + FlattenReverse(a + b); + { assert Last(a + b) == Last(b); assert DropLast(a + b) == a + DropLast(b); } + FlattenReverse(a + DropLast(b)) + Last(b); + FlattenReverse(a) + FlattenReverse(DropLast(b)) + Last(b); + FlattenReverse(a) + FlattenReverse(b); + } + } + } + + /* both methods of concatenating sequence (starting from front v. starting from back) + result in the same sequence */ + lemma LemmaFlattenAndFlattenReverseAreEquivalent(s: seq>) + ensures Flatten(s) == FlattenReverse(s) + { + if |s| == 0 { + } else { + calc == { + FlattenReverse(s); + FlattenReverse(DropLast(s)) + Last(s); + { LemmaFlattenAndFlattenReverseAreEquivalent(DropLast(s)); } + Flatten(DropLast(s)) + Last(s); + Flatten(DropLast(s)) + Flatten([Last(s)]); + { LemmaFlattenConcat(DropLast(s), [Last(s)]); + assert s == DropLast(s) + [Last(s)]; } + Flatten(s); + } + } + } + + /* the concatenated sequence's length is greater than or equal to each individual + inner sequence's length */ + lemma LemmaFlattenLengthGeSingleElementLength(s: seq>, i: int) + requires 0 <= i < |s| + ensures |FlattenReverse(s)| >= |s[i]| + { + if i < |s| - 1 { + LemmaFlattenLengthGeSingleElementLength(s[..|s|-1], i); + } + } + + /* the length of concatenating sequence in a sequence together will be no longer + than the length of the original sequence of sequences multiplied by the length of + the longest sequence */ + lemma LemmaFlattenLengthLeMul(s: seq>, j: int) + requires forall i {:trigger s[i]} | 0 <= i < |s| :: |s[i]| <= j + ensures |FlattenReverse(s)| <= |s| * j + { + if |s| == 0 { + } else { + LemmaFlattenLengthLeMul(s[..|s|-1], j); + } + } + + + /********************************************************** + * + * Higher-Order Sequence Functions + * + ***********************************************************/ + + /* applies a transformation function on the sequence */ + function method {:opaque} Map(f: (T ~> R), s: seq): (result: seq) + requires forall i {:trigger s[i]} :: 0 <= i < |s| ==> f.requires(s[i]) + ensures |result| == |s| + ensures forall i {:trigger result[i]}:: 0 <= i < |s| ==> result[i] == f(s[i]); + reads set i, o {:trigger o in f.reads(s[i])} | 0 <= i < |s| && o in f.reads(s[i]):: o + { + if |s| == 0 then [] + else [f(s[0])] + Map(f, s[1..]) + } + + /* concatenating two sequences and then applying Map is the same as applying + Map on each sequence seperately and then concatenating the two resulting + sequences */ + lemma {:opaque} LemmaMapDistributesOverConcat(f: (T ~> R), a: seq, b: seq) + requires forall i {:trigger a[i]}:: 0 <= i < |a| ==> f.requires(a[i]) + requires forall j {:trigger b[j]}:: 0 <= j < |b| ==> f.requires(b[j]) + ensures Map(f, a + b) == Map(f, a) + Map(f, b) + { + reveal Map(); + if |a| == 0 { + assert a + b == b; + } else { + calc { + Map(f, a + b); + { assert (a + b)[0] == a[0]; assert (a + b)[1..] == a[1..] + b; } + Map(f, [a[0]]) + Map(f, a[1..] + b); + Map(f, [a[0]]) + Map(f, a[1..]) + Map(f, b); + {assert [(a + b)[0]] + a[1..] + b == a + b;} + Map(f, a) + Map(f, b); + } + } + } + + /* uses a selection function to select elements from the sequence */ + function method {:opaque} Filter(f: (T ~> bool), s: seq): (result: seq) + requires forall i :: 0 <= i < |s| ==> f.requires(s[i]) + ensures |result| <= |s| + ensures forall i: nat {:trigger result[i]} :: i < |result| && f.requires(result[i]) ==> f(result[i]) + reads f.reads + { + if |s| == 0 then [] + else (if f(s[0]) then [s[0]] else []) + Filter(f, s[1..]) + } + + /* concatenating two sequences and then using "filter" is the same as using "filter" on each sequences + seperately and then concatenating their resulting sequences */ + lemma {:opaque} LemmaFilterDistributesOverConcat(f: (T ~> bool), a: seq, b: seq) + requires forall i {:trigger a[i]}:: 0 <= i < |a| ==> f.requires(a[i]) + requires forall j {:trigger b[j]}:: 0 <= j < |b| ==> f.requires(b[j]) + ensures Filter(f, a + b) == Filter(f, a) + Filter(f, b) + { + reveal Filter(); + if |a| == 0 { + assert a + b == b; + } else { + calc { + Filter(f, a + b); + { assert (a + b)[0] == a[0]; assert (a + b)[1..] == a[1..] + b; } + Filter(f, [a[0]]) + Filter(f, a[1..] + b); + Filter(f, [a[0]]) + Filter(f, a[1..]) + Filter(f, b); + { assert [(a + b)[0]] + a[1..] + b == a + b; } + Filter(f, a) + Filter(f, b); + } + } + } - // function method {:opaque} FoldLeft(f: (A, T) -> A, init: A, s: seq): A - // { - // if |s| == 0 then init - // else FoldLeft(f, f(init, s[0]), s[1..]) - // } - - // /* Concatenating two sequences, then folding left is the same as folding the first sequence and using the result as the initial value to fold the second - // sequence. */ - // lemma {:opaque} LemmaFoldLeftDistributesOverConcat(f: (A, T) -> A, init: A, a: seq, b: seq) - // requires 0 <= |a + b| - // ensures FoldLeft(f, init, a + b) == FoldLeft(f, FoldLeft(f, init, a), b) - // { - // reveal FoldLeft(); - // if |a| == 0 { - // assert a + b == b; - // } else { - // assert |a| >= 1; - // assert ([a[0]] + a[1..] + b)[0] == a[0]; - // calc { - // FoldLeft(f, FoldLeft(f, init, a), b); - // FoldLeft(f, FoldLeft(f, f(init, a[0]), a[1..]), b); - // { LemmaFoldLeftDistributesOverConcat(f, f(init, a[0]), a[1..], b); } - // FoldLeft(f, f(init, a[0]), a[1..] + b); - // { assert (a + b)[0] == a[0]; - // assert (a + b)[1..] == a[1..] + b; } - // FoldLeft(f, init, a + b); - // } - // } - // } - - // /* inv is an invariant under stp, which is a relational version of the - // function f passed to fold. */ - // predicate InvFoldLeft(inv: (B, seq) -> bool, - // stp: (B, A, B) -> bool) - // { - // forall x: A, xs: seq, b: B, b': B :: - // inv(b, [x] + xs) && stp(b, x, b') ==> inv(b', xs) - // } - - // /* inv(b, xs) ==> inv(FoldLeft(f, b, xs), []). */ - // lemma LemmaInvFoldLeft(inv: (B, seq) -> bool, - // stp: (B, A, B) -> bool, - // f: (B, A) -> B, - // b: B, - // xs: seq) - // requires InvFoldLeft(inv, stp) - // requires forall b, a :: stp(b, a, f(b, a)) - // requires inv(b, xs) - // ensures inv(FoldLeft(f, b, xs), []) - // { - // reveal FoldLeft(); - // if xs == [] { - // } else { - // assert [xs[0]] + xs[1..] == xs; - // LemmaInvFoldLeft(inv, stp, f, f(b, xs[0]), xs[1..]); - // } - // } - - // function method {:opaque} FoldRight(f: (T, A) -> A, s: seq, init: A): A - // { - // if |s| == 0 then init - // else f(s[0], FoldRight(f, s[1..], init)) - // } - - // /* Concatenating two sequences, then folding right is the same as folding the second sequence and using the result as the initial value to fold the first - // sequence. */ - // lemma {:opaque} LemmaFoldRightDistributesOverConcat(f: (T, A) -> A, init: A, a: seq, b: seq) - // requires 0 <= |a + b| - // ensures FoldRight(f, a + b, init) == FoldRight(f, a, FoldRight(f, b, init)) - // { - // reveal FoldRight(); - // if |a| == 0 { - // assert a + b == b; - // } else { - // calc { - // FoldRight(f, a, FoldRight(f, b, init)); - // f(a[0], FoldRight(f, a[1..], FoldRight(f, b, init))); - // f(a[0], FoldRight(f, a[1..] + b, init)); - // { assert (a + b)[0] == a[0]; - // assert (a + b)[1..] == a[1..] + b; } - // FoldRight(f, a + b, init); - // } - // } - // } - - // /* inv is an invariant under stp, which is a relational version of the - // function f passed to fold. */ - // predicate InvFoldRight(inv: (seq, B) -> bool, - // stp: (A, B, B) -> bool) - // { - // forall x: A, xs: seq, b: B, b': B :: - // inv(xs, b) && stp(x, b, b') ==> inv(([x] + xs), b') - // } - - // /* inv([], b) ==> inv(xs, FoldRight(f, xs, b)) */ - // lemma LemmaInvFoldRight(inv: (seq, B) -> bool, - // stp: (A, B, B) -> bool, - // f: (A, B) -> B, - // b: B, - // xs: seq) - // requires InvFoldRight(inv, stp) - // requires forall a, b :: stp(a, b, f(a, b)) - // requires inv([], b) - // ensures inv(xs, FoldRight(f, xs, b)) - // { - // reveal FoldRight(); - // if xs == [] { - // } else { - // assert [xs[0]] + xs[1..] == xs; - // } - // } + function method {:opaque} FoldLeft(f: (A, T) -> A, init: A, s: seq): A + { + if |s| == 0 then init + else FoldLeft(f, f(init, s[0]), s[1..]) + } + + /* Concatenating two sequences, then folding left is the same as folding the first sequence and using the result as the initial value to fold the second + sequence. */ + lemma {:opaque} LemmaFoldLeftDistributesOverConcat(f: (A, T) -> A, init: A, a: seq, b: seq) + requires 0 <= |a + b| + ensures FoldLeft(f, init, a + b) == FoldLeft(f, FoldLeft(f, init, a), b) + { + reveal FoldLeft(); + if |a| == 0 { + assert a + b == b; + } else { + assert |a| >= 1; + assert ([a[0]] + a[1..] + b)[0] == a[0]; + calc { + FoldLeft(f, FoldLeft(f, init, a), b); + FoldLeft(f, FoldLeft(f, f(init, a[0]), a[1..]), b); + { LemmaFoldLeftDistributesOverConcat(f, f(init, a[0]), a[1..], b); } + FoldLeft(f, f(init, a[0]), a[1..] + b); + { assert (a + b)[0] == a[0]; + assert (a + b)[1..] == a[1..] + b; } + FoldLeft(f, init, a + b); + } + } + } + + /* inv is an invariant under stp, which is a relational version of the + function f passed to fold. */ + predicate InvFoldLeft(inv: (B, seq) -> bool, + stp: (B, A, B) -> bool) + { + forall x: A, xs: seq, b: B, b': B :: + inv(b, [x] + xs) && stp(b, x, b') ==> inv(b', xs) + } + + /* inv(b, xs) ==> inv(FoldLeft(f, b, xs), []). */ + lemma LemmaInvFoldLeft(inv: (B, seq) -> bool, + stp: (B, A, B) -> bool, + f: (B, A) -> B, + b: B, + xs: seq) + requires InvFoldLeft(inv, stp) + requires forall b, a :: stp(b, a, f(b, a)) + requires inv(b, xs) + ensures inv(FoldLeft(f, b, xs), []) + { + reveal FoldLeft(); + if xs == [] { + } else { + assert [xs[0]] + xs[1..] == xs; + LemmaInvFoldLeft(inv, stp, f, f(b, xs[0]), xs[1..]); + } + } + + function method {:opaque} FoldRight(f: (T, A) -> A, s: seq, init: A): A + { + if |s| == 0 then init + else f(s[0], FoldRight(f, s[1..], init)) + } + + /* Concatenating two sequences, then folding right is the same as folding the second sequence and using the result as the initial value to fold the first + sequence. */ + lemma {:opaque} LemmaFoldRightDistributesOverConcat(f: (T, A) -> A, init: A, a: seq, b: seq) + requires 0 <= |a + b| + ensures FoldRight(f, a + b, init) == FoldRight(f, a, FoldRight(f, b, init)) + { + reveal FoldRight(); + if |a| == 0 { + assert a + b == b; + } else { + calc { + FoldRight(f, a, FoldRight(f, b, init)); + f(a[0], FoldRight(f, a[1..], FoldRight(f, b, init))); + f(a[0], FoldRight(f, a[1..] + b, init)); + { assert (a + b)[0] == a[0]; + assert (a + b)[1..] == a[1..] + b; } + FoldRight(f, a + b, init); + } + } + } + + /* inv is an invariant under stp, which is a relational version of the + function f passed to fold. */ + predicate InvFoldRight(inv: (seq, B) -> bool, + stp: (A, B, B) -> bool) + { + forall x: A, xs: seq, b: B, b': B :: + inv(xs, b) && stp(x, b, b') ==> inv(([x] + xs), b') + } + + /* inv([], b) ==> inv(xs, FoldRight(f, xs, b)) */ + lemma LemmaInvFoldRight(inv: (seq, B) -> bool, + stp: (A, B, B) -> bool, + f: (A, B) -> B, + b: B, + xs: seq) + requires InvFoldRight(inv, stp) + requires forall a, b :: stp(a, b, f(a, b)) + requires inv([], b) + ensures inv(xs, FoldRight(f, xs, b)) + { + reveal FoldRight(); + if xs == [] { + } else { + assert [xs[0]] + xs[1..] == xs; + } + } } diff --git a/src/Collections/Sequences/Seq.dfy.expect b/src/Collections/Sequences/Seq.dfy.expect index b0a9b1ad..dacccf30 100644 --- a/src/Collections/Sequences/Seq.dfy.expect +++ b/src/Collections/Sequences/Seq.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 69 verified, 0 errors +Dafny program verifier finished with 70 verified, 0 errors