avoid doing the wrong induction

LeventErkok · Sep 23, 2024 · d653d29 · d653d29
1 parent 5150915
commit d653d29
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/Documentation/SBV/Examples/KnuckleDragger/InsertionSort.hs b/Documentation/SBV/Examples/KnuckleDragger/InsertionSort.hs
@@ -62,15 +62,15 @@ correctness = runKDWith cvc5 $ do
 
     insertIntoNonDecreasing2 <- axiom "insertIntoNonDecreasing2"
           (\(Forall @"e" e) (Forall @"x" x) (Forall @"xs" xs) -> e .>  x .=> nonDecreasing (x .: xs) .== nonDecreasing (insert e (x .: xs)))
-          -- []
+          -- [induct (\xs e -> nonDecreasing (insert e xs))]
 
     insertIntoNonDecreasing3 <- lemmaWith z3 "insertIntoNonDecreasing3"
           (\(Forall @"e" e) (Forall @"xs" xs) -> nonDecreasing xs .== nonDecreasing (insert e xs))
-          [induct (\e -> nonDecreasing . insert e), insertIntoNonDecreasing1, insertIntoNonDecreasing2]
+          [induct (\xs e -> nonDecreasing (insert e xs)), insertIntoNonDecreasing1, insertIntoNonDecreasing2]
 
     nonDecreasingInsert <- lemma "nonDecreasingInsert"
                (\(Forall @"e" e) (Forall @"xs" xs) -> nonDecreasing xs .== nonDecreasing (insert e xs))
-               [induct (\e -> nonDecreasing . insert e), insertIntoNonDecreasing3]
+               [induct (\xs e -> nonDecreasing (insert e xs)), insertIntoNonDecreasing3]
 
     lemma "insertionSortCorrect"
           (\(Forall @"l" l) -> nonDecreasing (insertionSort l))