Give TestResult.success (.inl ()) higher priority than .gaveUp

If some runs succeeded and some runs didn't produce a well-formed
example, then the overall result should be that some runs succeeded,
not that we couldn't generate a well-formed example.

(The handling of `TestResult.success (.inr h)` is unchanged -- it
already had higher priority than `.gaveUp`, and further it triggers
immediate termination because it has a positive proof.)

Fixes #15.

Author: tom93

Plausible/Testable.lean

@@ -518,10 +518,8 @@ def retry (cmd : Gen (TestResult p)) : Nat → Gen (TestResult p)
 
 /-- Count the number of times the test procedure gave up. -/
 def giveUp (x : Nat) : TestResult p → TestResult p
-  | success (PSum.inl ()) => gaveUp x
-  | success (PSum.inr p) => success <| (PSum.inr p)
   | gaveUp n => gaveUp <| n + x
-  | TestResult.failure h xs n => failure h xs n
+  | r => r
 
 /-- Try `n` times to find a counter-example for `p`. -/
 def Testable.runSuiteAux (p : Prop) [Testable p] (cfg : Configuration) :
@@ -534,13 +532,13 @@ def Testable.runSuiteAux (p : Prop) [Testable p] (cfg : Configuration) :
       slimTrace s!"Retrying up to {cfg.numRetries} times until guards hold"
     let x ← retry ((Testable.runProp p cfg true).resize size) cfg.numRetries
     match x with
-    | success (PSum.inl ()) => runSuiteAux p cfg r n
+    | success (PSum.inl ()) => runSuiteAux p cfg x n
     | gaveUp g => runSuiteAux p cfg (giveUp g r) n
     | _ => return x
 
 /-- Try to find a counter-example of `p`. -/
 def Testable.runSuite (p : Prop) [Testable p] (cfg : Configuration := {}) : Gen (TestResult p) :=
-  Testable.runSuiteAux p cfg (success <| PSum.inl ()) cfg.numInst
+  Testable.runSuiteAux p cfg (gaveUp 0) cfg.numInst
 
 /-- Run a test suite for `p` in `IO` using the global RNG in `stdGenRef`. -/
 def Testable.checkIO (p : Prop) [Testable p] (cfg : Configuration := {}) : IO (TestResult p) :=

Test/Tactic.lean

@@ -159,3 +159,13 @@ theorem ulift_nat (f : ULift.{1} Nat) : f = ⟨0⟩ := by
 #guard_msgs in
 theorem type_u (α : Type u) (l : List α) : l = l ++ l := by
   plausible (config := {quiet := true})
+
+-- https://github.com/leanprover-community/plausible/issues/15
+/--
+info: Unable to find a counter-example
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+theorem true_example_with_guard (a : Nat) (ha : 4 ≤ a) : a = a := by
+  plausible