Skip to content

Commit

Permalink
remove commented proof code from 007
Browse files Browse the repository at this point in the history
  • Loading branch information
edwin1729 committed Dec 23, 2024
1 parent f7a7d83 commit f9c2fad
Showing 1 changed file with 1 addition and 43 deletions.
44 changes: 1 addition & 43 deletions tasks/human_eval_007.rs
Original file line number Diff line number Diff line change
Expand Up @@ -43,9 +43,6 @@ spec fn is_subseq_of<A>(s: Seq<A>, sub: Seq<A>) -> bool {
fn check_substring(s: &str, sub: &str) -> (result: bool)
ensures
result <==> is_subseq_of(s@, sub@),
// exists|i: int|
// 0 <= i <= [email protected]() - [email protected]() && [email protected](i, #[trigger] (i + [email protected]())) == sub@,

{
let s_len = s.unicode_len();
let sub_len = sub.unicode_len();
Expand Down Expand Up @@ -74,62 +71,23 @@ fn check_substring(s: &str, sub: &str) -> (result: bool)

fn filter_by_sub<'a>(strings: &Vec<&'a str>, sub: &str) -> (res: Vec<&'a str>)
ensures
strings@.filter(|s: &str| is_subseq_of(s@, sub@))
== res@,
// forall|i: int|
// 0 <= i < [email protected]() &&
// // [email protected] (|s: &str| is_subseq_of(s@, sub@)) == res@
// is_subseq_of(strings[i]@, sub@) ==> [email protected](
// #[trigger] (strings[i]),
// ) && [email protected](#[trigger] (strings[i])) ==> is_subseq_of(strings[i]@, sub@),

strings@.filter(|s: &str| is_subseq_of(s@, sub@)) == res@,
{
let mut res = Vec::new();
// assert ([email protected](0, 0).filter (|s: &str| is_subseq_of(s@, sub@)) == res@);
assert(res@ == Seq::<&str>::empty());
let mut n = 0;
// while n < strings.len()
for n in 0..strings.len()
invariant
// n < strings.len(),
// forall|i: int|
// 0 <= i < n && is_subseq_of(strings[i]@, sub@) ==> [email protected](
// #[trigger] (strings[i]),
// ),

strings@.subrange(0, n as int).filter(|s: &str| is_subseq_of(s@, sub@)) == res@,
n <= strings.len(),
{
reveal(Seq::filter);
assert(strings@.subrange(0, n as int + 1).drop_last() == strings@.subrange(0, n as int));
if check_substring(strings[n], sub) {
// let ghost res_old = res@;
// let ghost filtered_sub = [email protected](0, n as int).filter (|s: &str| is_subseq_of(s@, sub@));
// let ghost pred = |s: &str| is_subseq_of(s@, sub@);
// let ghost last = ran.last();
// assert (last@ == strings[n as int]@);
// let ghost ra = ran.drop_last();
// assert(ra.push(last) == ran);
// assert (ra == [email protected](0, n as int));
// assert (pred(last));
// let ghost ran_f = ran.filter(pred);
// let ghost ra_f = ra.filter(pred);
// assert(ra_f == res@);
// assert(ra_f.push(last) == ran_f);
// assert (ran.filter (|s: &str| is_subseq_of(s@, sub@)).last()@ == ran.last()@);
res.push(strings[n]);
// assert (ran_f == res@);
// assert([email protected]() == strings[n as int]);
// assert (strings[n as int] == [email protected](0, n as int + 1).last());
// assert (res_old == filtered_sub);
// assert (strings[n as int] == [email protected](0, n as int + 1).filter (|s: &str| is_subseq_of(s@, sub@)).last());
// assert ([email protected](0, (n as int) + 1).filter (|s: &str| is_subseq_of(s@, sub@)) == [email protected](0, n as int).filter (|s: &str| is_subseq_of(s@, sub@)).push(strings[n as int]));
// assert(strings[n as int]@ == [email protected](0, n + 1).filter(|s: &str| is_subseq_of(s@, sub@)).last()@);
// assert([email protected]_last() == res_old);
}
}
assert(strings@.subrange(0, strings@.len() as int) == strings@);
// assert ([email protected](0, n as int).filter (|s: &str| is_subseq_of(s@, sub@)) == res@);
res
}

Expand Down

0 comments on commit f9c2fad

Please sign in to comment.