minimize find_unique_maximal_ensures

verus-lang · Jul 27, 2023 · 7643b3d · 7643b3d
1 parent 1367f30
commit 7643b3d
Showing 1 changed file with 2 additions and 44 deletions.
diff --git a/source/pervasive/set_lib.rs b/source/pervasive/set_lib.rs
@@ -498,33 +498,20 @@ pub proof fn find_unique_minimal_ensures<A>(s: Set<A>, r: FnSpec(A,A) -> bool)
     lemma_set_properties::<A>();
     if s.len() == 1 {
         let x = choose |x: A| s.contains(x);
-        //assert(s.finite());
-        //assert(s.remove(x) =~= Set::<A>::empty());
         assert(s.remove(x).insert(x) =~= s);
-        // assert(s.contains(s.find_unique_minimal(r)));
-        // assert(r(x,x));
         assert(is_minimal(r, s.find_unique_minimal(r),s));
-
-       // assert((forall |min_poss: A| is_minimal(r, min_poss, s) ==> s.find_unique_minimal(r) == min_poss));
     }
     else {
         let x = choose |x: A| s.contains(x);
         find_unique_minimal_ensures(s.remove(x),r);
         assert(is_minimal(r, s.remove(x).find_unique_minimal(r),s.remove(x)));
-        //assert(s.remove(x).insert(x) =~= s);
         let y = s.remove(x).find_unique_minimal(r);
         let min_updated = s.find_unique_minimal(r); 
-        //assert(min_updated == x || min_updated == y);
-        //assert(r(y,x) ==> min_updated == y);
         assert(!r(y,x) ==> min_updated == x);
-        //assert(!r(y,x) ==> r(x,y));
         assert(forall |elt: A| s.remove(x).contains(elt) && #[trigger] r(elt,y) ==> #[trigger] r(y,elt));
-        //assert(s.contains(min_updated));
         assert forall |elt: A| s.contains(elt) && #[trigger] r(elt,min_updated) implies #[trigger] r(min_updated,elt) by {
             assert(r(min_updated,x) || r(min_updated,y));
             if min_updated == y { // Case where the new min is the old min
-                //assert(r(min_updated,elt));
-               // assert(r(min_updated,x));
                 assert(is_minimal(r, s.find_unique_minimal(r),s));
             } else { //Case where the new min is the newest element
                 assert(s.remove(x).contains(elt) || elt ==x);
@@ -534,21 +521,10 @@ pub proof fn find_unique_minimal_ensures<A>(s: Set<A>, r: FnSpec(A,A) -> bool)
                 assert(!(min_updated == y) ==> !r(y,x));
                 assert(r(x,y));
                 if (s.remove(x).contains(elt)) {
-                    //assert(r(elt,y) ==> r(y,elt));
                     assert(r(elt,y) && r(y,elt) ==> elt == y); 
-                    //assert(r(x,elt));
-                   // assert(r(min_updated,elt))
-                } else {
-                    // assert(elt == x);
-                    // assert(r(x,y));
-                    // assert(r(elt,y));
-                    // assert(r(min_updated,y));
-                    // assert(r(min_updated,elt));
-                }
+                } else {}
             }
         }
-        //assert(is_minimal(r, s.find_unique_minimal(r),s));
-        //assert(antisymmetric(r));
         assert forall |min_poss: A| is_minimal(r, min_poss, s) implies s.find_unique_minimal(r) == min_poss by {
             assert(is_minimal(r, min_poss, s.remove(x)) || x == min_poss);                
             assert(r(min_poss, s.find_unique_minimal(r)));
@@ -571,12 +547,7 @@ pub proof fn find_unique_maximal_ensures<A>(s: Set<A>, r: FnSpec(A,A) -> bool)
     if s.len() == 1 {
         let x = choose |x: A| s.contains(x);
         assert(s.remove(x) =~= Set::<A>::empty());
-        assert(s.remove(x).insert(x) =~= s);
         assert(s.contains(s.find_unique_maximal(r)));
-        assert(r(x,x));
-        assert(is_maximal(r, s.find_unique_maximal(r),s));
-
-        assert((forall |max_poss: A| is_maximal(r, max_poss, s) ==> s.find_unique_maximal(r) == max_poss));
     }
     else {
         let x = choose |x: A| s.contains(x);
@@ -586,11 +557,7 @@ pub proof fn find_unique_maximal_ensures<A>(s: Set<A>, r: FnSpec(A,A) -> bool)
         let y = s.remove(x).find_unique_maximal(r);
         let max_updated = s.find_unique_maximal(r); 
         assert(max_updated == x || max_updated == y);
-        assert(r(x,y) ==> max_updated == y);
         assert(!r(x,y) ==> max_updated == x);
-        assert(!r(x,y) ==> r(y,x));
-        assert(forall |elt: A| s.remove(x).contains(elt) && #[trigger] r(y,elt) ==> #[trigger] r(elt,y));
-        assert(s.contains(max_updated));
         assert forall |elt: A| s.contains(elt) && #[trigger] r(max_updated,elt) implies #[trigger] r(elt,max_updated) by {
             assert(r(x,max_updated) || r(y,max_updated));
             if max_updated == y { // Case where the new max is the old max
@@ -605,21 +572,12 @@ pub proof fn find_unique_maximal_ensures<A>(s: Set<A>, r: FnSpec(A,A) -> bool)
                 assert(!(max_updated == y) ==> !r(x,y));
                 assert(r(y,x));
                 if (s.remove(x).contains(elt)) {
-                    assert(r(y,elt) ==> r(elt,y));
                     assert(r(y,elt) && r(elt,y) ==> elt == y); 
                     assert(r(elt,x));
                     assert(r(elt,max_updated))
-                } else {
-                    assert(elt == x);
-                    assert(r(y,x));
-                    assert(r(y,elt));
-                    assert(r(y,max_updated));
-                    assert(r(elt, max_updated));
-                }
+                } else {}
             }
         }
-        assert(is_maximal(r, s.find_unique_maximal(r),s));
-        assert(antisymmetric(r));
         assert forall |max_poss: A| is_maximal(r, max_poss, s) implies s.find_unique_maximal(r) == max_poss by {
             assert(is_maximal(r, max_poss, s.remove(x)) || x == max_poss);     
             assert(r(max_poss, s.find_unique_maximal(r)));