From f9c2fad6a82a654c7c07c36b48d794e47f276ac2 Mon Sep 17 00:00:00 2001
From: Edwin Fernando <ef322@ic.ac.uk>
Date: Mon, 23 Dec 2024 09:45:22 +0000
Subject: [PATCH] remove commented proof code from 007

---
 tasks/human_eval_007.rs | 44 +----------------------------------------
 1 file changed, 1 insertion(+), 43 deletions(-)

diff --git a/tasks/human_eval_007.rs b/tasks/human_eval_007.rs
index 845210b..3922afa 100644
--- a/tasks/human_eval_007.rs
+++ b/tasks/human_eval_007.rs
@@ -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 <= s@.len() - sub@.len() && s@.subrange(i, #[trigger] (i + sub@.len())) == sub@,
-
 {
     let s_len = s.unicode_len();
     let sub_len = sub.unicode_len();
@@ -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 < strings@.len() &&
-//     // strings@.filter (|s: &str| is_subseq_of(s@, sub@)) == res@
-//     is_subseq_of(strings[i]@, sub@) ==> res@.contains(
-//         #[trigger] (strings[i]),
-//     ) && res@.contains(#[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 (strings@.subrange(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@) ==> res@.contains(
-    //         #[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 = strings@.subrange(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 == strings@.subrange(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(res@.last() == strings[n as int]);
-            // assert (strings[n as int] == strings@.subrange(0, n as int + 1).last());
-            // assert (res_old == filtered_sub);
-            // assert (strings[n as int] == strings@.subrange(0, n as int + 1).filter (|s: &str| is_subseq_of(s@, sub@)).last());
-            // assert (strings@.subrange(0, (n as int) + 1).filter (|s: &str| is_subseq_of(s@, sub@)) == strings@.subrange(0, n as int).filter (|s: &str| is_subseq_of(s@, sub@)).push(strings[n as int]));
-            // assert(strings[n as int]@ == strings@.subrange(0, n + 1).filter(|s: &str| is_subseq_of(s@, sub@)).last()@);
-            // assert(res@.drop_last() == res_old);
         }
     }
     assert(strings@.subrange(0, strings@.len() as int) == strings@);
-    // assert (strings@.subrange(0, n as int).filter (|s: &str| is_subseq_of(s@, sub@)) == res@);
     res
 }