feat: make Fact testable for slim_check (leanprover-community#12566)

Closes leanprover-community#12565

Also adds a sort-of-missing `g.withContext`. I don't think its absence causes any errors.

Mathlib/Logic/Basic.lean

@@ -128,6 +128,9 @@ theorem fact_iff {p : Prop} : Fact p ↔ p := ⟨fun h ↦ h.1, fun h ↦ ⟨h
 #align fact_iff fact_iff
 #align fact.elim Fact.elim
 
+instance {p : Prop} [Decidable p] : Decidable (Fact p) :=
+  decidable_of_iff _ fact_iff.symm
+
 /-- Swaps two pairs of arguments to a function. -/
 @[reducible] def Function.swap₂ {ι₁ ι₂ : Sort*} {κ₁ : ι₁ → Sort*} {κ₂ : ι₂ → Sort*}
     {φ : ∀ i₁, κ₁ i₁ → ∀ i₂, κ₂ i₂ → Sort*} (f : ∀ i₁ j₁ i₂ j₂, φ i₁ j₁ i₂ j₂)

Mathlib/Tactic/SlimCheck.lean

@@ -166,6 +166,7 @@ syntax (name := slimCheckSyntax) "slim_check" (config)? : tactic
 elab_rules : tactic | `(tactic| slim_check $[$cfg]?) => withMainContext do
   let cfg ← elabConfig (mkOptionalNode cfg)
   let (_, g) ← (← getMainGoal).revert ((← getLocalHyps).map (Expr.fvarId!))
+  g.withContext do
   let tgt ← g.getType
   let tgt' ← addDecorations tgt
   let cfg := { cfg with

Mathlib/Testing/SlimCheck/Testable.lean

@@ -291,6 +291,11 @@ instance forallTypesTestable {f : Type → Prop} [Testable (f Int)] :
     let r ← runProp (f Int) cfg min
     pure <| addVarInfo var "ℤ" (· <| Int) r
 
+instance factTestable [Testable p] : Testable (Fact p) where
+  run cfg min := do
+    let h ← runProp p cfg min
+    pure <| iff fact_iff h
+
 /--
 Format the counter-examples found in a test failure.
 -/
@@ -451,6 +456,9 @@ instance False.printableProp : PrintableProp False where
 instance Bool.printableProp {b : Bool} : PrintableProp b where
   printProp := if b then "true" else "false"
 
+instance Fact.printableProp [PrintableProp p] : PrintableProp (Fact p) where
+  printProp := printProp p
+
 end PrintableProp
 
 section IO

test/slim_check.lean

@@ -3,6 +3,7 @@ import Mathlib.Tactic.SuccessIfFailWithMsg
 import Mathlib.Data.Finsupp.Notation
 import Mathlib.Testing.SlimCheck.Functions
 import Mathlib.Tactic.Have
+import Mathlib.Data.Nat.Prime
 
 private axiom test_sorry : ∀ {α}, α
 
@@ -452,3 +453,20 @@ theorem testBit_pred :
     testBit (pred x) i = (decide (0 < x) &&
       (Bool.xor ((List.range i).all fun j => ! testBit x j) (testBit x i))) := by
   slim_check
+
+-- https://github.com/leanprover-community/mathlib4/issues/12565
+-- Make `slim_check` handle `Fact` instances.
+/--
+error:
+===================
+Found problems!
+a := 7
+guard: ⋯
+issue: ⋯ does not hold
+issue: ⋯ does not hold
+(0 shrinks)
+-------------------
+-/
+#guard_msgs in
+example {a : ℕ} [Fact a.Prime] : (a + 1).Prime ∨ (a + 2).Prime := by
+  slim_check (config := { randomSeed := some 257 })