feat: lift to expressions, vacuous and random_search tactics

Plausible/Functions.lean

@@ -131,11 +131,12 @@ instance Pi.sampleableExt : SampleableExt (α → β) where
   interp f := SampleableExt.interp ∘ f.apply
   sample := do
     let xs : List (_ × _) ← (SampleableExt.sample (α := List (α × β)))
-    let ⟨x⟩ ← Gen.up <| (SampleableExt.sample : Gen (SampleableExt.proxy β))
+    let ⟨x⟩ ← Gen.up (SampleableExt.sample : Gen (SampleableExt.proxy β))
     pure <| TotalFunction.withDefault (List.toFinmap' <| xs.map <|
       Prod.map SampleableExt.interp id) x
   -- note: no way of shrinking the domain without an inverse to `interp`
   shrink := { shrink := letI : Shrinkable α := {}; TotalFunction.shrink }
+  proxyExpr? := none
 
 end
 
@@ -149,13 +150,15 @@ instance (priority := 2000) PiPred.sampleableExt [SampleableExt (α → Bool)] :
   interp m x := interp m x
   sample := sample
   shrink := SampleableExt.shrink
+  proxyExpr? := none
 
 instance (priority := 2000) PiUncurry.sampleableExt [SampleableExt (α × β → γ)] :
     SampleableExt.{imax (u + 1) (v + 1) w} (α → β → γ) where
   proxy := proxy (α × β → γ)
   interp m x y := interp m (x, y)
   sample := sample
   shrink := SampleableExt.shrink
+  proxyExpr? := none
 
 end SampleableExt
 

Plausible/MGen.lean

@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2025 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Siddhartha Gadgil
+-/
+import Plausible.Random
+import Batteries.Data.List.Perm
+import Plausible.Gen
+import Lean
+open Lean Meta
+
+namespace Plausible
+
+open Random
+
+abbrev MRand := RandT MetaM
+
+instance : MonadLift Rand MRand where
+  monadLift := fun x s => return x.run s
+
+abbrev MGen (α : Type) := ReaderT (ULift Nat) MRand α
+
+instance : MonadLift Gen MGen where
+  monadLift := fun x n => x.run n.down