diff --git a/Plausible/Functions.lean b/Plausible/Functions.lean index 882dbc0c..f02ab2e2 100644 --- a/Plausible/Functions.lean +++ b/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,6 +150,7 @@ 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 @@ -156,6 +158,7 @@ instance (priority := 2000) PiUncurry.sampleableExt [SampleableExt (α × β → interp m x y := interp m (x, y) sample := sample shrink := SampleableExt.shrink + proxyExpr? := none end SampleableExt diff --git a/Plausible/MGen.lean b/Plausible/MGen.lean new file mode 100644 index 00000000..d977759a --- /dev/null +++ b/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 diff --git a/Plausible/MetaTestable.lean b/Plausible/MetaTestable.lean new file mode 100644 index 00000000..f9bd996a --- /dev/null +++ b/Plausible/MetaTestable.lean @@ -0,0 +1,781 @@ +/- +Copyright (c) 2022 Henrik Böving. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving, Simon Hudon +-/ +import Lean.Meta +import Lean.Elab.Tactic.Config +import Plausible.Sampleable +import Plausible.Testable +import Plausible.MGen +open Lean + +/-! +# `MetaTestable` Class + +MetaTestable propositions have a procedure that can generate counter-examples together with a proof that they invalidate the proposition. This is a refinement of the `Testable` class. + +Instances of `Testable` are built using `Sampleable` instances. For `MetaTestable` instances, we also need an expression for the proxy in a sampleable type, which is an additional requirement. + +## Main definitions + +* `MetaTestable` class +* `MetaTestable.check`: a way to test a proposition using random examples, givng a proof of the counter-example +-/ + +namespace Plausible + +section Matching +open Lean Meta +/-! +# Matching propositions of specific forms +-/ +def existsProp? (e: Expr) : MetaM (Option Expr × Option Expr) := do + let u ← mkFreshLevelMVar + let α ← mkFreshExprMVar (mkSort u) + let prop := mkSort levelZero + let fmly ← mkArrow α prop + let mvar ← mkFreshExprMVar (some fmly) + let e' ← mkAppM ``Exists #[mvar] + if ← isDefEq e' e then + return (← Lean.getExprMVarAssignment? mvar.mvarId!, ← Lean.getExprMVarAssignment? α.mvarId!) + else + return (none, none) + +def orProp? (e: Expr) : MetaM (Option Expr × Option Expr) := do + let prop := mkSort levelZero + let α ← mkFreshExprMVar prop + let β ← mkFreshExprMVar prop + let e' ← mkAppM ``Or #[α, β] + if ← isDefEq e' e then + return (← Lean.getExprMVarAssignment? α.mvarId!, ← Lean.getExprMVarAssignment? β.mvarId!) + else + return (none, none) + +def andProp? (e: Expr) : MetaM (Option Expr × Option Expr) := do + let prop := mkSort levelZero + let α ← mkFreshExprMVar prop + let β ← mkFreshExprMVar prop + let e' ← mkAppM ``And #[α, β] + if ← isDefEq e' e then + return (← Lean.getExprMVarAssignment? α.mvarId!, ← Lean.getExprMVarAssignment? β.mvarId!) + else + return (none, none) + +def notProp? (e: Expr) : MetaM (Option Expr) := do + let prop := mkSort levelZero + let α ← mkFreshExprMVar prop + let e' ← mkAppM ``Not #[α] + if ← isDefEq e' e then + return (← Lean.getExprMVarAssignment? α.mvarId!) + else + return none + +def forallProp? (e: Expr) : MetaM (Option Expr × Option Expr) := do + let u ← mkFreshLevelMVar + let α ← mkFreshExprMVar (mkSort u) + let prop := mkSort levelZero + let fmlyType ← mkArrow α prop + let fmly ← mkFreshExprMVar (some fmlyType) + let e' ← withLocalDeclD `x α fun x => do + let y ← mkAppM' fmly #[x] + mkForallFVars #[x] y + if ← isDefEq e' e then + return (← Lean.getExprMVarAssignment? fmly.mvarId!, ← Lean.getExprMVarAssignment? α.mvarId!) + else + return (none, none) + +def forallPropProp? (e: Expr) : MetaM (Option Expr × Option Expr × Option Expr) := do + let u ← mkFreshLevelMVar + let α ← mkFreshExprMVar (mkSort u) + let prop := mkSort levelZero + let fmlyType ← mkArrow α prop + let fmly ← mkFreshExprMVar (some fmlyType) + let p ← mkFreshExprMVar (some fmlyType) + let e' ← withLocalDeclD `x α fun x => do + let y ← mkAppM' fmly #[x] + let y' ← mkAppM' p #[x] + let cod ← mkArrow y' y + mkForallFVars #[x] cod + if ← isDefEq e' e then + return (← Lean.getExprMVarAssignment? p.mvarId!, ← Lean.getExprMVarAssignment? fmly.mvarId!, ← Lean.getExprMVarAssignment? α.mvarId!) + else + return (none, none, none) + +def impProp? (e: Expr) : MetaM (Option Expr × Option Expr) := do + let u ← mkFreshLevelMVar + let α ← mkFreshExprMVar (mkSort u) + let prop := mkSort levelZero + let β ← mkFreshExprMVar prop + let e' ← mkArrow α β + if ← isDefEq e' e then + return (← Lean.getExprMVarAssignment? α.mvarId!, ← Lean.getExprMVarAssignment? β.mvarId!) + else + return (none, none) + +def eqlProp? (e: Expr): MetaM (Option (Expr × Expr × Expr)) := do + let level ← mkFreshLevelMVar + let u := mkSort level + let α ← mkFreshExprMVar u + let a ← mkFreshExprMVar α + let b ← mkFreshExprMVar α + let e' ← mkAppM ``Eq #[a, b] + if ← isDefEq e' e then + let α? ← Lean.getExprMVarAssignment? α.mvarId! + let a? ← Lean.getExprMVarAssignment? a.mvarId! + let b? ← Lean.getExprMVarAssignment? b.mvarId! + let triple : Option (Expr × Expr × Expr) := do + let α ← α? + let a ← a? + let b ← b? + return (α, a, b) + return triple + else + return none + +def iffProp? (e: Expr): MetaM (Option (Expr × Expr)) := do + let prop := mkSort levelZero + let α ← mkFreshExprMVar prop + let β ← mkFreshExprMVar prop + let e' ← mkAppM ``Iff #[α , β] + if ← isDefEq e' e then + let α? ← Lean.getExprMVarAssignment? α.mvarId! + let β? ← Lean.getExprMVarAssignment? β.mvarId! + let pair : Option (Expr × Expr) := do + let α ← α? + let β ← β? + return (α, β) + return pair + else + return none + +def equality? (e: Expr): MetaM (Option (Expr × Expr × Expr)) := do + let level ← mkFreshLevelMVar + let u := mkSort level + let α ← mkFreshExprMVar u + let a ← mkFreshExprMVar α + let b ← mkFreshExprMVar α + let e' ← mkAppM ``Eq #[a, b] + let c ← mkFreshExprMVar e' + if ← isDefEq c e then + let α? ← Lean.getExprMVarAssignment? α.mvarId! + let a? ← Lean.getExprMVarAssignment? a.mvarId! + let b? ← Lean.getExprMVarAssignment? b.mvarId! + let triple : Option (Expr × Expr × Expr) := do + let α ← α? + let a ← a? + let b ← b? + return (α, a, b) + return triple + else + return none + + +end Matching + +open Lean Meta + +/-- Result of trying to disprove `p` -/ +inductive MetaTestResult (p : Prop) where + /-- + Succeed when we find another example satisfying `p`. + In `success h`, `h` is an optional proof of the proposition. + Without the proof, all we know is that we found one example + where `p` holds. With a proof, the one test was sufficient to + prove that `p` holds and we do not need to keep finding examples. + -/ + | success : Unit ⊕' p → MetaTestResult p + /-- + Give up when a well-formed example cannot be generated. + `gaveUp n` tells us that `n` invalid examples were tried. + -/ + | gaveUp : Nat → MetaTestResult p + /-- + A counter-example to `p`; the strings specify values for the relevant variables. + `failure h vs n` also carries a proof that `p` does not hold. This way, we can + guarantee that there will be no false positive. The last component, `n`, + is the number of times that the counter-example was shrunk. + -/ + | failure : ¬ p → Option Expr → List String → Nat → MetaTestResult p + deriving Inhabited + + +/-- `MetaTestable p` uses random examples to try to disprove `p`. -/ +class MetaTestable (p : Prop) where + runExpr (cfg : Configuration) (minimize : Bool) (propExpr? : Option Expr) : MGen (MetaTestResult p) + + +namespace MetaTestResult + +def toString : MetaTestResult p → String + | success (PSum.inl _) => "success (no proof)" + | success (PSum.inr _) => "success (proof)" + | gaveUp n => s!"gave {n} times" + | failure _ _ counters _ => s!"failed {counters}" + +instance : ToString (MetaTestResult p) := ⟨toString⟩ + +/-- Applicative combinator proof carrying test results. -/ +def combine {p q : Prop} : Unit ⊕' (p → q) → Unit ⊕' p → Unit ⊕' q + | PSum.inr f, PSum.inr proof => PSum.inr <| f proof + | _, _ => PSum.inl () + +def checkDisproof (pf prop: Expr) : MetaM Unit := do + let negProp ← mkAppM ``Not #[prop] + let pfType ← inferType pf + unless ← isDefEq pfType negProp do + throwError m!"Expected a proof of {negProp}, got proof of {← ppExpr pfType}" + +/-- Combine the test result for properties `p` and `q` to create a test for their conjunction. -/ +def and : MetaTestResult p → MetaTestResult q → Option Expr → MetaM (MetaTestResult (p ∧ q)) + | failure h pf? xs n, _, e? => do + let pf'? ← + match e? with + | none => pure none + | some e => + let (some e₁, some e₂) ← andProp? e | throwError m!"Expected an `And` proposition, got {← ppExpr e}" + pf?.mapM fun pf => withLocalDeclD `h e fun h => do + let x ← mkAppOptM ``And.left #[e₁, e₂, h] + let e' ← mkAppM' pf #[x] + mkLambdaFVars #[h] e' + -- checkDisproof pf' e + return failure (fun h2 => h h2.left) pf'? xs n + | _, failure h pf? xs n, e? => do + let pf' ← + match e? with + | none => pure none + | some e => + let (some e₁, some e₂) ← andProp? e | throwError m!"Expected an `And` proposition, got {← ppExpr e}" + pf?.mapM fun pf => withLocalDeclD `h e fun h => do + let x ← mkAppOptM ``And.right #[e₁, e₂, h] + let e' ← mkAppM' pf #[x] + mkLambdaFVars #[h] e' + -- checkDisproof pf' e + return failure (fun h2 => h h2.right) pf' xs n + | success h1, success h2, _ => + return success <| combine (combine (PSum.inr And.intro) h1) h2 + | gaveUp n, gaveUp m, _ => return gaveUp <| n + m + | gaveUp n, _, _ => return gaveUp n + | _, gaveUp n, _ => return gaveUp n + + +/-- Combine the test result for properties `p` and `q` to create a test for their disjunction. -/ +def or : MetaTestResult p → MetaTestResult q → Option Expr → MetaM (MetaTestResult (p ∨ q)) + | failure h1 pf1 xs n, failure h2 pf2 ys m, e? => do + let pf ← + match e? with + | none => pure none + | some e => + let (some α, some β) ← orProp? e | throwError m!"Expected an `Or` proposition, got {← ppExpr e}" + let motive ← withLocalDeclD `h e fun h => do + mkLambdaFVars #[h] <| mkConst ``False + mkAppOptM ``Or.rec #[α, β, motive, pf1, pf2] + let h3 := fun h => + match h with + | Or.inl h3 => h1 h3 + | Or.inr h3 => h2 h3 + -- checkDisproof pf e + return failure h3 pf (xs ++ ys) (n + m) + | success h, _, _ => return success <| combine (PSum.inr Or.inl) h + | _, success h, _ => return success <| combine (PSum.inr Or.inr) h + | gaveUp n, gaveUp m, _ => return gaveUp <| n + m + | gaveUp n, _, _ => return gaveUp n + | _, gaveUp n, _ => return gaveUp n + +/-- If `q → p`, then `¬ p → ¬ q` which means that testing `p` can allow us +to find counter-examples to `q`. -/ +def imp (h : q → p) (hExp?: Option Expr) (r : MetaTestResult p) + (p : Unit ⊕' (p → q) := PSum.inl ()) : MetaM (MetaTestResult q) := + match r with + | failure h2 pf? xs n => do + let pf' ← + hExp?.bindM fun hExp => pf?.mapM fun pf => mkAppM ``mt #[hExp, pf] + return failure (mt h h2) pf' xs n + | success h2 => return success <| combine p h2 + | gaveUp n => return gaveUp n + +/-- Test `q` by testing `p` and proving the equivalence between the two. -/ +def iff (h : q ↔ p) (hExp? : Option Expr) (r : MetaTestResult p) : MetaM (MetaTestResult q) := do + let hExp' ← hExp?.mapM fun hExp => mkAppM ``Iff.mp #[hExp] + imp h.mp hExp' r (PSum.inr h.mpr) + +/-- When we assign a value to a universally quantified variable, +we record that value using this function so that our counter-examples +can be informative. -/ +def addInfo (x : String) (h : q → p) (hExp?: Option Expr) (r : MetaTestResult p) + (p : Unit ⊕' (p → q) := PSum.inl ()) : (MetaM <| MetaTestResult q) := do + if let failure h2 pf? xs n := r then + let pf' ← hExp?.bindM fun hExp => pf?.mapM fun pf => mkAppM ``mt #[hExp, pf] + return failure (mt h h2) pf' (x :: xs) n + else + imp h hExp? r p + +/-- Add some formatting to the information recorded by `addInfo`. -/ +def addVarInfo {γ : Type _} [Repr γ] (var : String) (x : γ) (h : q → p) (hExp: Option Expr) (r : MetaTestResult p) + (p : Unit ⊕' (p → q) := PSum.inl ()) : MetaM (MetaTestResult q) := do + addInfo s!"{var} := {repr x}" h (hExp: Option Expr) r p + +def isFailure : MetaTestResult p → Bool + | failure .. => true + | _ => false + +end MetaTestResult + + +namespace MetaTestable + +open MetaTestResult + + +def runPropExpr (p : Prop) [MetaTestable p] : Configuration → Bool → Option Expr → MGen (MetaTestResult p) := fun cfg b e => do + runExpr cfg b e + +/-- A `dbgTrace` with special formatting -/ +def slimTrace {m : Type → Type _} [Pure m] (s : String) : m PUnit := + dbgTrace s!"[Plausible: {s}]" (fun _ => pure ()) + + +instance andTestable [MetaTestable p] [MetaTestable q] : MetaTestable (p ∧ q) where + runExpr := fun cfg min e? => do + let (e₁, e₂) ← match e? with + | some e => do + let (some e₁, some e₂) ← andProp? e | throwError m!"Expected an `And` proposition, got {← ppExpr e}" + pure (some e₁, some e₂) + | none => pure (none, none) + let xp ← runPropExpr p cfg min e₁ + let xq ← runPropExpr q cfg min e₂ + and xp xq e? + +instance orTestable [MetaTestable p] [MetaTestable q] : MetaTestable (p ∨ q) where + runExpr := fun cfg min e? => do + let (e₁, e₂) ← match e? with + | some e => do + let (some e₁, some e₂) ← orProp? e | throwError m!"Expected an `Or` proposition, got {← ppExpr e}" + pure (some e₁, some e₂) + | none => pure (none, none) + let xp ← runPropExpr p cfg min e₁ + -- As a little performance optimization we can just not run the second + -- test if the first succeeds + match xp with + | success (PSum.inl h) => return success (PSum.inl h) + | success (PSum.inr h) => return success (PSum.inr <| Or.inl h) + | _ => + let xq ← runPropExpr q cfg min e₂ + or xp xq e? + +theorem iff_resolve (p q : Prop) : (p ↔ q) ↔ p ∧ q ∨ ¬p ∧ ¬q := by + constructor + · intro h + simp [h, Classical.em] + · intro h + rcases h with ⟨hleft, hright⟩ | ⟨hleft, hright⟩ <;> simp [hleft, hright] + +instance iffTestable [MetaTestable ((p ∧ q) ∨ (¬ p ∧ ¬ q))] : MetaTestable (p ↔ q) where + runExpr := fun cfg min e? => do + let hExp ← + match e? with + | none => pure none + | some e => do + let some (α, β) ← iffProp? e | throwError m!"Expected an `Iff` proposition, got {← ppExpr e}" + mkAppM ``iff_resolve #[α, β] + let h ← runPropExpr ((p ∧ q) ∨ (¬ p ∧ ¬ q)) cfg min e? + iff (iff_resolve p q) hExp h + +variable {var : String} + +instance decGuardTestable [PrintableProp p] [Decidable p] {β : p → Prop} [∀ h, MetaTestable (β h)] : + MetaTestable (NamedBinder var <| ∀ h, β h) where + runExpr := fun cfg min e? => do + if h : p then + match e? with + | none => + let res := runPropExpr (β h) cfg min none + let s := printProp p + ← (fun r => addInfo s!"guard: {s}" (· <| h) none r (PSum.inr <| fun q _ => q)) <$> res + | some e => + let (some βExp, some pExp) ← forallProp? e | throwError m!"Expected a `Forall` proposition, got {← ppExpr e}" + let h' := (· <| h) + let yExp ← + mkAppM' βExp #[pExp] + let res := runPropExpr (β h) cfg min yExp + let decInstType ← mkAppM ``Decidable #[pExp] + let inst ← synthInstance decInstType + let falseRefl ← mkAppM ``Eq.refl #[mkConst ``false] + let pf ← mkAppOptM ``of_decide_eq_true #[pExp, inst, falseRefl] + let cod := mkApp βExp pf + let hExp ← + withLocalDeclD `x (← mkArrow pExp cod) fun x => do + let y ← mkAppM' x #[cod] + mkLambdaFVars #[x] y + let s := printProp p + ← (fun r => addInfo s!"guard: {s}" h' hExp r (PSum.inr <| fun q _ => q)) <$> res + else if cfg.traceDiscarded || cfg.traceSuccesses then + let res := fun _ => return gaveUp 1 + let s := printProp p + slimTrace s!"discard: Guard {s} does not hold"; res + else + return gaveUp 1 + +instance forallTypesTestable {f : Type → Prop} [MetaTestable (f Int)] : + MetaTestable (NamedBinder var <| ∀ x, f x) where + runExpr := fun cfg min e => do + let r ← runPropExpr (f Int) cfg min e + addVarInfo var "Int" (· <| Int) e r + +-- TODO: only in mathlib: @[pp_with_univ] +instance (priority := 100) forallTypesULiftTestable.{u} + {f : Type u → Prop} [MetaTestable (f (ULift.{u} Int))] : + MetaTestable (NamedBinder var <| ∀ x, f x) where + runExpr cfg min e := do + let r ← runPropExpr (f (ULift Int)) cfg min e + addVarInfo var "ULift Int" (· <| ULift Int) e r + +/-- +Increase the number of shrinking steps in a test result. +-/ +def addShrinks (n : Nat) : MetaTestResult p → MetaTestResult p + | MetaTestResult.failure p pf xs m => MetaTestResult.failure p pf xs (m + n) + | p => p + +universe u in +instance {α : Type u} {m : Type u → Type _} [Pure m] : Inhabited (OptionT m α) := + ⟨(pure none : m (Option α))⟩ + +variable {α : Sort _} + +/-- Shrink a counter-example `x` by using `Shrinkable.shrink x`, picking the first +candidate that falsifies a property and recursively shrinking that one. +The process is guaranteed to terminate because `shrink x` produces +a proof that all the values it produces are smaller (according to `SizeOf`) +than `x`. -/ +partial def minimizeAux [SampleableExt α] {β : α → Prop} [∀ x, MetaTestable (β x)] (αExp? βExp?: Option Expr) (cfg : Configuration) + (var : String) (x : SampleableExt.proxy α) (n : Nat) : + OptionT MGen (Σ x, MetaTestResult (β (SampleableExt.interp x))) := do + let candidates := SampleableExt.shrink.shrink x + if cfg.traceShrinkCandidates then + slimTrace s!"Candidates for {var} := {repr x}:\n {repr candidates}" + match αExp?, βExp?, getProxyExpr? α with + | some αExp, some βExpr, some _ => + for candidate in candidates do + if cfg.traceShrinkCandidates then + slimTrace s!"Trying {var} := {repr candidate}" + let xExpr := toExpr candidate + let .sort u := ← inferType αExp | throwError m!"Expected a sort, got {αExp}" + let v ← mkFreshLevelMVar + let instType := mkApp (mkConst ``SampleableExt [u, v]) αExp + let samp ← synthInstance instType + let xInterp ← mkAppOptM ``SampleableExt.interp #[αExp, samp, xExpr] + let e' ← mkAppM' βExpr #[xInterp] + let res ← OptionT.lift <| runPropExpr (β (SampleableExt.interp candidate)) cfg true e' + if res.isFailure then + if cfg.traceShrink then + slimTrace s!"{var} shrunk to {repr candidate} from {repr x}" + let currentStep := OptionT.lift <| return Sigma.mk candidate (addShrinks (n + 1) res) + let nextStep := minimizeAux αExp βExpr cfg var candidate (n + 1) + return ← (nextStep <|> currentStep) + | _, _, _ => + for candidate in candidates do + if cfg.traceShrinkCandidates then + slimTrace s!"Trying {var} := {repr candidate}" + let res ← OptionT.lift <| runPropExpr (β (SampleableExt.interp candidate)) cfg true none + if res.isFailure then + if cfg.traceShrink then + slimTrace s!"{var} shrunk to {repr candidate} from {repr x}" + let currentStep := OptionT.lift <| return Sigma.mk candidate (addShrinks (n + 1) res) + let nextStep := minimizeAux none none cfg var candidate (n + 1) + return ← (nextStep <|> currentStep) + if cfg.traceShrink then + slimTrace s!"No shrinking possible for {var} := {repr x}" + failure + +/-- Once a property fails to hold on an example, look for smaller counter-examples +to show the user. -/ +def minimize [SampleableExt α] {β : α → Prop} [∀ x, MetaTestable (β x)] (αExp βExpr: Option Expr)(cfg : Configuration) + (var : String) (x : SampleableExt.proxy α) (r : MetaTestResult (β <| SampleableExt.interp x)) : + MGen (Σ x, MetaTestResult (β <| SampleableExt.interp x)) := do + if cfg.traceShrink then + slimTrace "Shrink" + slimTrace s!"Attempting to shrink {var} := {repr x}" + let res ← OptionT.run <| minimizeAux αExp βExpr cfg var x 0 + return res.getD ⟨x, r⟩ + +open Lean Meta Elab Term Tactic in +/-- Test a universal property by creating a sample of the right type and instantiating the +bound variable with it. -/ +instance varTestable [SampleableExt α] {β : α → Prop} [∀ x, MetaTestable (β x)] : + MetaTestable (NamedBinder var <| ∀ x : α, β x) where + runExpr := fun cfg min e? => do + match e? with + | none => + let x ← SampleableExt.sample + if cfg.traceSuccesses || cfg.traceDiscarded then + slimTrace s!"{var} := {repr x}" + let r ← runPropExpr (β <| SampleableExt.interp x) cfg false none + let ⟨finalX, finalR⟩ ← + if isFailure r then + if cfg.traceSuccesses then + slimTrace s!"{var} := {repr x} is a failure" + if min then + minimize none none cfg var x r + else + pure ⟨x, r⟩ + else + pure ⟨x, r⟩ + let h := (· <| SampleableExt.interp finalX) + addVarInfo var finalX h none finalR + | some e => + let (some βExp, some αExp) ← forallProp? e | throwError m!"Expected a `Forall` proposition, got {← ppExpr e}" + let x ← SampleableExt.sample + let e'? ← match getProxyExpr? α with + | none => pure none + | some inst => + let xExpr := toExpr x + let αExp ← instantiateMVars αExp + let .sort u := ← inferType αExp | throwError m!"Expected a sort, got {αExp}" + let v ← mkFreshLevelMVar + let instType := mkApp (mkConst ``SampleableExt [u, v]) αExp + let samp ← synthInstance instType + let xInterp ← mkAppOptM ``SampleableExt.interp #[αExp, samp, xExpr] + let e' ← mkAppM' βExp #[xInterp] + -- let (e', _) ← dsimp e' {} + pure (some e') + if cfg.traceSuccesses || cfg.traceDiscarded then + slimTrace s!"{var} := {repr x}" + let r ← runPropExpr (β <| SampleableExt.interp x) cfg false e'? + let ⟨finalX, finalR⟩ ← + if isFailure r then + if cfg.traceSuccesses then + slimTrace s!"{var} := {repr x} is a failure" + if min then + minimize αExp βExp cfg var x r + else + pure ⟨x, r⟩ + else + pure ⟨x, r⟩ + let hExpr? ← match getProxyExpr? α with + | none => pure none + | some inst => + let xExpr := toExpr finalX + let .sort u ← inferType αExp | throwError m!"Expected a sort, got {αExp}" + let v ← mkFreshLevelMVar + let instType := mkApp (mkConst ``SampleableExt [u, v]) αExp + let samp ← synthInstance instType + let xInterp ← mkAppOptM ``SampleableExt.interp #[αExp, samp, xExpr] + let hExpr ← withLocalDeclD `x e fun x => do + mkLambdaFVars #[x] (mkApp x xInterp) + pure (some hExpr) + let h := (· <| SampleableExt.interp finalX) + addVarInfo var finalX h hExpr? finalR + + + + +theorem bool_to_prop_fmly (β : Prop → Prop): NamedBinder var (∀ (p : Prop), β p) → ∀ (b : Bool), β (b = true) := fun h b => h (b = true) + +/-- Test a universal property about propositions -/ +instance propVarTestable {β : Prop → Prop} [h: ∀ b : Bool, MetaTestable (β b)] : + MetaTestable (NamedBinder var <| ∀ p : Prop, β p) +where + runExpr := fun cfg min e? => do + let p ← runPropExpr (NamedBinder var <| ∀ b : Bool, β b) cfg min e? + let e' ← + match e? with + | none => pure none + | some e => do + let (some βExpr, _) ← forallProp? e | throwError m!"Expected a `Forall` proposition, got {← ppExpr e}" + let res ← mkAppM ``bool_to_prop_fmly #[βExpr] + pure (some res) + imp (bool_to_prop_fmly β) e' p + +instance (priority := high) unusedVarTestable {β : Prop} [Nonempty α] [MetaTestable β] : + MetaTestable (NamedBinder var (α → β)) +where + runExpr := fun cfg min e? => do + if cfg.traceDiscarded || cfg.traceSuccesses then + slimTrace s!"{var} is unused" + match e? with + | none => + let r ← runPropExpr β cfg min none + let finalR ← addInfo s!"{var} is irrelevant (unused)" id none r + let h := (· <| Classical.ofNonempty) + imp h none finalR (PSum.inr <| fun x _ => x) + | some e => + let (some aExp, some e') ← impProp? e | throwError m!"Expected an `Imp` proposition, got {← ppExpr e}" + let r ← runPropExpr β cfg min e' + let hExp ← mkAppOptM ``id #[e'] + let finalR ← addInfo s!"{var} is irrelevant (unused)" id hExp r + let nInst ← synthInstance <| ← mkAppM ``Nonempty #[aExp] + let hExp ← withLocalDeclD `h e fun h => do + mkLambdaFVars #[h] <| mkApp h nInst + let h := (· <| Classical.ofNonempty) + imp h hExp finalR (PSum.inr <| fun x _ => x) + +theorem prop_iff_subtype (p : α → Prop) (β : α → Prop) : NamedBinder var (∀ (x : α), NamedBinder var' (p x → β x)) ↔ ∀ (x : Subtype p), β x.val := by simp [Subtype.forall, NamedBinder] + +-- This is unlikely to ever be used successfully because of the instance of `SampleableExt (Subtype p)` needed. Should probably have classes for implications instead. +instance (priority := 2000) subtypeVarTestable {p : α → Prop} {β : α → Prop} + [∀ x, PrintableProp (p x)] + [∀ x, MetaTestable (β x)][ToExpr α] + [SampleableExt (Subtype p)] {var'} : + MetaTestable (NamedBinder var <| (x : α) → NamedBinder var' <| p x → β x) where + runExpr cfg min e? := + match e? with + | none => do + letI (x : Subtype p) : MetaTestable (β x) := + { runExpr := fun cfg min e => do + let r ← runPropExpr (β x.val) cfg min none + let idExp ← mkAppOptM ``id #[e] + addInfo s!"guard: {printProp (p x)} (by construction)" id idExp r (PSum.inr id) } + do + let r ← @runExpr (∀ x : Subtype p, β x.val) (@varTestable var _ _ _ _) cfg min none + iff (prop_iff_subtype p β) none r + | some e => do + let (some pExp, some βExp, some _) ← forallPropProp? e | throwError m!"Expected a `Forall` proposition with arrow, got {← ppExpr e}" + let subType ← mkAppM ``Subtype #[pExp] + letI (x : Subtype p) : MetaTestable (β x) := + { runExpr := fun cfg min e => do + let xExp := toExpr x.val + let y ← mkAppM' βExp #[xExp] + let r ← runPropExpr (β x.val) cfg min y + let idExp ← mkAppOptM ``id #[e] + addInfo s!"guard: {printProp (p x)} (by construction)" id idExp r (PSum.inr id) } + do + let e' ← withLocalDeclD `x subType fun x => do + let x' ← mkAppM ``Subtype.val #[x] + let y ← mkAppM' βExp #[x'] + mkForallFVars #[x] y + let r ← @runExpr (∀ x : Subtype p, β x.val) (@varTestable var _ _ _ _) cfg min e' + let hExp ← mkAppM ``prop_iff_subtype #[pExp, βExp] + iff (prop_iff_subtype p β) hExp r + +instance (priority := low) decidableTestable {p : Prop} [PrintableProp p] [Decidable p] : + MetaTestable p where + runExpr := fun _ _ e? _ => do + if h : p then + return success (PSum.inr h) + else + let s := printProp p + let pf' ← do + match e? with + | none => pure none + | some e => + let inst ← synthInstance <| ← mkAppM ``Decidable #[e] + let falseRefl ← mkAppM ``Eq.refl #[mkConst ``false] + mkAppOptM ``of_decide_eq_false #[e, inst, falseRefl] + -- checkDisproof pf' e + -- logInfo "Decidable proof checked" + return failure h pf' [s!"issue: {s} does not hold"] 0 + +end MetaTestable + + +section Meta +open MetaTestResult + +namespace MetaTestable +/-- Execute `cmd` and repeat every time the result is `gaveUp` (at most `n` times). -/ +def retry (cmd : MRand (MetaTestResult p)) : Nat → MRand (MetaTestResult p) + | 0 => return MetaTestResult.gaveUp 1 + | n+1 => do + let r ← cmd + match r with + | .success hp => return success hp + | .failure h pf xs n => return failure h pf xs n + | .gaveUp _ => retry cmd n + +/-- Count the number of times the test procedure gave up. -/ +def giveUp (x : Nat) : MetaTestResult p → MetaTestResult p + | success (PSum.inl ()) => gaveUp x + | success (PSum.inr p) => success <| (PSum.inr p) + | gaveUp n => gaveUp <| n + x + | MetaTestResult.failure h pf xs n => failure h pf xs n + +end MetaTestable + +/-- Try `n` times to find a counter-example for `p`. -/ +def MetaTestable.runSuiteAux (p : Prop) [MetaTestable p] (propExpr: Option Expr) (cfg : Configuration) : + MetaTestResult p → Nat → MRand (MetaTestResult p) + | r, 0 => return r + | r, n+1 => do + let size := (cfg.numInst - n - 1) * cfg.maxSize / cfg.numInst + if cfg.traceSuccesses then + slimTrace s!"New sample" + slimTrace s!"Retrying up to {cfg.numRetries} times until guards hold" + let x ← retry (ReaderT.run (runPropExpr p cfg true propExpr) ⟨size⟩) cfg.numRetries + match x with + | success (PSum.inl ()) => runSuiteAux p propExpr cfg r n + | gaveUp g => runSuiteAux p propExpr cfg (giveUp g r) n + | _ => return x + +/-- Try to find a counter-example of `p`. -/ +def MetaTestable.runSuite (p : Prop) [MetaTestable p] (propExpr: Option Expr) (cfg : Configuration := {}) : MRand (MetaTestResult p) := + MetaTestable.runSuiteAux p propExpr cfg (success <| PSum.inl ()) cfg.numInst + +/-- Run a test suite for `p` in `MetaM` using the global RNG in `stdGenRef`. -/ +def MetaTestable.seekM (p : Prop) [MetaTestable p] (cfg : Configuration := {}) (propExpr: Option Expr) : MetaM (MetaTestResult p) := + match cfg.randomSeed with + | none => runRand (MetaTestable.runSuite p propExpr cfg) + | some seed => runRandWith seed (MetaTestable.runSuite p propExpr cfg) + +end Meta + +open Decorations in +/-- Run a test suite for `p` and throw an exception if `p` does not hold. -/ +def MetaTestable.seek (p : Prop) (cfg : Configuration := {}) + (p' : Decorations.DecorationsOf p := by mk_decorations) [MetaTestable p'](propExpr: Expr) : Lean.MetaM (Option Expr) := do + match ← MetaTestable.seekM p' cfg propExpr with + | MetaTestResult.success _ => + if !cfg.quiet then Lean.logInfo "Unable to find a counter-example" + return none + | MetaTestResult.gaveUp n => + if !cfg.quiet then + let msg := s!"Gave up after failing to generate values that fulfill the preconditions {n} times." + Lean.logWarning msg + return none + | MetaTestResult.failure _ pf xs n => + let msg := "Found a counter-example!" + if cfg.quiet then + Lean.logInfo msg + else + Lean.logInfo <| Testable.formatFailure msg xs n + return pf + +def disproveM? (cfg : Configuration) (tgt: Expr) : MetaM <| Option Expr := do + let tgt' ← Decorations.addDecorations tgt + let inst ← try + synthInstance (← mkAppM ``MetaTestable #[tgt']) + catch _ => + throwError "Failed to create a `testable` instance for `{tgt}`." + let e ← mkAppOptM ``MetaTestable.seek #[tgt, toExpr cfg, tgt', inst] + let expectedType := Lean.Expr.forallE `a + (Lean.Expr.const `Lean.Expr []) + (Lean.Expr.app + (Lean.Expr.const `Lean.Meta.MetaM []) + (Lean.Expr.app + (Lean.Expr.const ``Option [Level.zero]) + (Lean.Expr.const ``Lean.Expr []))) + (Lean.BinderInfo.default) + let code ← unsafe evalExpr (Expr → MetaM (Option Expr)) expectedType e + code tgt + +open Decorations in +/-- Run a test suite for `p` and throw an exception if `p` does not hold. -/ +def MetaTestable.check (p : Prop) (cfg : Configuration := {}) + (p' : Decorations.DecorationsOf p := by mk_decorations) [MetaTestable p'](propExpr: Option Expr := none) : Lean.MetaM Unit := do + match ← MetaTestable.seekM p' cfg propExpr with + | MetaTestResult.success _ => + if !cfg.quiet then Lean.logInfo "Unable to find a counter-example" + | MetaTestResult.gaveUp n => + if !cfg.quiet then + let msg := s!"Gave up after failing to generate values that fulfill the preconditions {n} times." + Lean.logWarning msg + | MetaTestResult.failure _ _ xs n => + let msg := "Found a counter-example!" + if cfg.quiet then + throwError msg + else + throwError Testable.formatFailure msg xs n + + + +end Plausible diff --git a/Plausible/RandomSearch.lean b/Plausible/RandomSearch.lean new file mode 100644 index 00000000..18b7049e --- /dev/null +++ b/Plausible/RandomSearch.lean @@ -0,0 +1,127 @@ +import Plausible.MetaTestable +/-! +## Random Search + +The `random_search` tactic tries to prove a result by searching for a counter-example to its negation using `MetaTestable`. If a counter-example is found, we can prove the result by showing that the negation is false. +-/ + +open Lean Meta Elab Term + +namespace Plausible + +open Classical in +theorem not_not (p: Prop) : ¬ ¬ p → p := + fun h' => if h : p then h else absurd h h' + +open Classical in +theorem not_and {p q : Prop} : ¬ (p ∧ q) → ¬ p ∨ ¬ q := + fun h => if hp : p then Or.inr fun hq => h ⟨hp, hq⟩ else Or.inl hp + +theorem induced_or {p₁ q₁ p₂ q₂ : Prop} (h₁ : p₁ → q₁) (h₂ : p₂ → q₂) : p₁ ∨ p₂ → q₁ ∨ q₂ + | Or.inl h => Or.inl (h₁ h) + | Or.inr h => Or.inr (h₂ h) + +theorem induced_and {p₁ q₁ p₂ q₂ : Prop} (h₁ : p₁ → q₁) (h₂ : p₂ → q₂) : p₁ ∧ p₂ → q₁ ∧ q₂ + | ⟨h1, h2⟩ => ⟨h₁ h1, h₂ h2⟩ + +theorem induced_exists {p q : α → Prop}(f : ∀x : α, p x → q x) : (∃ x, p x) → ∃ x, q x + | ⟨x, h⟩ => ⟨x, f x h⟩ + +theorem not_or_mp {p q : Prop} (h : ¬ (p ∨ q)) : ¬ p ∧ ¬ q := + ⟨fun h' => h (Or.inl h'), fun h' => h (Or.inr h')⟩ + +theorem not_forall {p : α → Prop} : ¬ (∀ x, p x) → ∃ x, ¬ p x := by + intro h + apply not_not + intro contra + have l : ∀ (x : α), p x := by + intro x + by_cases h' : p x + · exact h' + · exfalso + exact contra ⟨x, h'⟩ + contradiction + + +partial def negate (e: Expr) : MetaM <| Expr × Expr := do + match ← notProp? e with + | some e' => + let negProof ← mkAppOptM ``id #[e] + return (e', negProof) + | _ => + match ← andProp? e with + | (some e₁, some e₂) => + let (negProp₁, negProof₁) ← negate e₁ + let (negProp₂, negProof₂) ← negate e₂ + let negProp ← mkAppM ``Or #[negProp₁, negProp₂] + let negPf ← withLocalDeclD `h (← mkAppM ``Not #[negProp]) fun h => do + let h' ← mkAppM ``not_or_mp #[h] + let negProof ← mkAppM ``induced_and #[negProof₁, negProof₂, h'] + mkLambdaFVars #[h] negProof + return (negProp, negPf) + | _ => + match ← orProp? e with + | (some e₁, some e₂) => + let (negProp₁, negProof₁) ← negate e₁ + let (negProp₂, negProof₂) ← negate e₂ + let negProp ← mkAppM ``And #[negProp₁, negProp₂] + let negPf ← withLocalDeclD `h (← mkAppM ``Not #[negProp]) fun h => do + let h' ← mkAppM ``not_and #[h] + let negProof ← mkAppM ``induced_or #[negProof₁, negProof₂, h'] + mkLambdaFVars #[h] negProof + return (negProp, negPf) + | _ => + match ← existsProp? e with + | (some p, some α) => + logInfo m!"Negating existential quantifier {← ppExpr e}, family: {← ppExpr p}, domain: {← ppExpr α}" + let (negProp, negProofFamily) ← withLocalDeclD `x α fun x => do + let y ← mkAppM' p #[x] + let (y, _) ← dsimp y {} + let (negProp, negProof) ← negate y + pure (← mkForallFVars #[x] negProp, ← mkLambdaFVars #[x] negProof) + logInfo m!"Negation of {← ppExpr e} is {← ppExpr negProp}" + let negPf ← withLocalDeclD `h (← mkAppM ``Not #[negProp]) fun h => do + let h' ← mkAppM ``not_forall #[h] + let negProof ← mkAppM ``induced_exists #[negProofFamily, h'] + mkLambdaFVars #[h] negProof + return (negProp, negPf) + | _ => + let negProp ← mkAppM ``Not #[e] + let negProof ← mkAppM ``not_not #[e] + return (negProp, negProof) + +open Elab Term +elab "neg_neg" t:term : term => do + let e ← elabTerm t none + let (negProp, negProof) ← negate e + let pfType ← inferType negProof + -- disproof of negation implies `e` + let goal ← mkArrow (← mkAppM ``Not #[negProp]) e + let check ← isDefEq pfType goal + logInfo m!"Negation of {← ppExpr e} is {← ppExpr negProp}" + logInfo m!"Proof of negation is {← ppExpr negProof} with type {← ppExpr <| ← inferType negProof}, should be {← ppExpr goal}" + logInfo m!"check: {check}" + return negProp + +open Lean.Parser.Tactic Tactic +syntax (name := searchSyntax) "random_search" (config)? : tactic +elab_rules : tactic | `(tactic| random_search $[$cfg]?) => withMainContext do + let cfg ← elabConfig (mkOptionalNode cfg) let (_, g) ← (← getMainGoal).revert ((← getLocalHyps).map (Expr.fvarId!)) + let cfg := { cfg with + traceDiscarded := cfg.traceDiscarded || (← isTracingEnabledFor `plausible.discarded), + traceSuccesses := cfg.traceSuccesses || (← isTracingEnabledFor `plausible.success), + traceShrink := cfg.traceShrink || (← isTracingEnabledFor `plausible.shrink.steps), + traceShrinkCandidates := cfg.traceShrinkCandidates + || (← isTracingEnabledFor `plausible.shrink.candidates) } + g.withContext do + let tgt ← g.getType + let (negProp, negProof) ← negate tgt + match ← disproveM? cfg negProp with + | some pf => + let pf' ← mkAppM' negProof #[pf] + logInfo m!"Found a proof by negated counter-example!" + g.assign pf' + | none => + throwError "could not find a proof by negated counter-example" + +end Plausible diff --git a/Plausible/Sampleable.lean b/Plausible/Sampleable.lean index d538d3f0..7eeac8f8 100644 --- a/Plausible/Sampleable.lean +++ b/Plausible/Sampleable.lean @@ -3,9 +3,12 @@ Copyright (c) 2022 Henrik Böving. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving, Simon Hudon -/ +import Lean.Meta import Lean.Elab.Command import Lean.Meta.Eval import Plausible.Gen +import Qq +open Lean Qq /-! # `SampleableExt` Class @@ -105,28 +108,48 @@ If we test a quantification over functions the counter-examples cannot be shrunken or printed meaningfully. For that purpose, `SampleableExt` provides a proxy representation `proxy` that can be printed and shrunken as well -as interpreted (using `interp`) as an object of the right type. -/ +as interpreted (using `interp`) as an object of the right type. + +SampleableExt can also be used to constuct expressions representing disproofs in some cases. For this, the `proxy` type should be a type that can be represented as an expression and the field `proxyExpr?` should be set to such a function. Expressions for disproofs will not be generated for sampling involving instances where `proxyExpr?` is `none`. +-/ class SampleableExt (α : Sort u) where proxy : Type v [proxyRepr : Repr proxy] [shrink : Shrinkable proxy] + /-- Expressions representing terms of type proxy if available.-/ + proxyExpr? : Option (ToExpr proxy) sample : Gen proxy interp : proxy → α attribute [instance] SampleableExt.proxyRepr attribute [instance] SampleableExt.shrink +def getProxyExpr? (α : Sort u) [inst: SampleableExt α] : + Option (ToExpr (inst.proxy)) := + inst.proxyExpr? namespace SampleableExt /-- Use to generate instance whose purpose is to simply generate values of a type directly using the `Gen` monad -/ -def mkSelfContained [Repr α] [Shrinkable α] (sample : Gen α) : SampleableExt α where +def mkSelfContained [Repr α] [Shrinkable α] [Lean.ToExpr α] (sample : Gen α) : SampleableExt α where + proxy := α + proxyRepr := inferInstance + shrink := inferInstance + proxyExpr? := some inferInstance + sample := sample + interp := id + +/-- Use to generate instance whose purpose is to simply generate values +of a type directly using the `Gen` monad -/ +def mkSelfContainedSimple [Repr α] [Shrinkable α] (sample : Gen α) : SampleableExt α where proxy := α proxyRepr := inferInstance shrink := inferInstance + proxyExpr? := none sample := sample interp := id + /-- First samples a proxy value and interprets it. Especially useful if the proxy and target type are the same. -/ def interpSample (α : Type u) [SampleableExt α] : Gen α := @@ -241,8 +264,23 @@ end Shrinkers section Samplers +variable {α : Type u} {β : Type v} +#check Impl.unquoteExpr + open SampleableExt +instance instToExprSum [ToExpr α] [ToExpr β] : ToExpr (α ⊕ β) := + let αType : Q(Type) := toTypeExpr α + let βType : Q(Type ):= toTypeExpr β + { toExpr : α ⊕ β → Q($αType ⊕ $βType) := fun a => + match a with + | .inl a => + mkApp3 (mkConst ``Sum.inl [levelZero, levelZero]) αType βType (toExpr a) + | .inr a => + mkApp3 (mkConst ``Sum.inr [levelZero, levelZero]) αType βType (toExpr a), + toTypeExpr := mkApp2 (mkConst ``Sum [levelZero, levelZero]) αType βType } + + instance Sum.SampleableExt [SampleableExt α] [SampleableExt β] : SampleableExt (Sum α β) where proxy := Sum (proxy α) (proxy β) sample := do @@ -253,6 +291,10 @@ instance Sum.SampleableExt [SampleableExt α] [SampleableExt β] : SampleableExt match s with | .inl l => .inl (interp l) | .inr r => .inr (interp r) + proxyExpr? := do + let inst₁ ← getProxyExpr? α + let inst₂ ← getProxyExpr? β + pure <| @instToExprSum _ _ inst₁ inst₂ instance Unit.sampleableExt : SampleableExt Unit := mkSelfContained (return ()) @@ -263,6 +305,9 @@ instance [SampleableExt α] [SampleableExt β] : SampleableExt ((_ : α) × β) let p ← prodOf sample sample return ⟨p.fst, p.snd⟩ interp s := ⟨interp s.fst, interp s.snd⟩ + proxyExpr? := none -- did not understand the difference with products + + instance Nat.sampleableExt : SampleableExt Nat := mkSelfContained (do choose Nat 0 (← getSize) (Nat.zero_le _)) @@ -325,6 +370,12 @@ def Char.sampleable (length : Nat) (chars : List Char) (pos : 0 < chars.length) instance Char.sampleableDefault : SampleableExt Char := Char.sampleable 3 " 0123abcABC:,;`\\/".toList (by decide) +def optionExpr {α : Type u} [ToExpr α] : ToExpr (Option α) := + { toExpr := fun + | none => mkConst ``Option.none + | some a => mkApp (mkConst ``Option.some) (toExpr a), + toTypeExpr := mkApp (mkConst ``Option [levelZero]) (toTypeExpr α) } + instance Option.sampleableExt [SampleableExt α] : SampleableExt (Option α) where proxy := Option (proxy α) sample := do @@ -332,45 +383,81 @@ instance Option.sampleableExt [SampleableExt α] : SampleableExt (Option α) whe | true => return none | false => return some (← sample) interp o := o.map interp + proxyExpr? := getProxyExpr? α |>.map fun p => @optionExpr _ p + +def prodExpr {α : Type u} {β : Type v} [ToExpr α] [ToExpr β] : ToExpr (α × β) := + { toExpr := fun ⟨a, b⟩ => + mkApp2 (mkConst ``Prod.mk [levelZero, levelZero]) (toExpr a) (toExpr b), + toTypeExpr := mkApp2 (mkConst ``Prod [levelZero, levelZero]) (toTypeExpr α) (toTypeExpr β) } -instance Prod.sampleableExt {α : Type u} {β : Type v} [SampleableExt α] [SampleableExt β] : +instance Prod.sampleableExt {α : Type u} {β : Type v} [inst₁ : SampleableExt α] [inst₂ : SampleableExt β] : SampleableExt (α × β) where proxy := Prod (proxy α) (proxy β) proxyRepr := inferInstance shrink := inferInstance sample := prodOf sample sample interp := Prod.map interp interp + proxyExpr? := + match inst₁.proxyExpr?, inst₂.proxyExpr? with + | some p₁, some p₂ => some <| @prodExpr _ _ p₁ p₂ + | _ , _ => none + instance Prop.sampleableExt : SampleableExt Prop where proxy := Bool proxyRepr := inferInstance sample := interpSample Bool shrink := inferInstance + proxyExpr? := some inferInstance interp := Coe.coe +def listExpr {α : Type u} [ToExpr α] : ToExpr (List α) := + { toExpr := fun xs => + let xs := xs.toArray + let exprs := xs.map (fun x => toExpr x) + exprs.foldr (fun e es => mkApp2 (mkConst ``List.cons) e es) (mkConst ``List.nil), + toTypeExpr := mkApp (mkConst ``List [levelZero]) (toTypeExpr α) } + instance List.sampleableExt [SampleableExt α] : SampleableExt (List α) where proxy := List (proxy α) sample := Gen.listOf sample interp := List.map interp + proxyExpr? := getProxyExpr? α |>.map fun p => (@listExpr _ p) instance ULift.sampleableExt [SampleableExt α] : SampleableExt (ULift α) where proxy := proxy α sample := sample interp a := ⟨interp a⟩ + proxyExpr? := none + instance String.sampleableExt : SampleableExt String := mkSelfContained do return String.mk (← Gen.listOf (Char.sampleableDefault.sample)) +def arrayExpr {α : Type u} [ToExpr α] : ToExpr (Array α) := + { toExpr := fun xs => + let xs := xs.toList + let lExpr := @toExpr _ (listExpr) xs + mkApp (mkConst ``List.toArray) lExpr, + toTypeExpr := mkApp (mkConst ``Array [levelZero]) (toTypeExpr α) } + instance Array.sampleableExt [SampleableExt α] : SampleableExt (Array α) where proxy := Array (proxy α) sample := Gen.arrayOf sample interp := Array.map interp + proxyExpr? := getProxyExpr? α |>.map fun p => (@arrayExpr _ p) + end Samplers /-- An annotation for values that should never get shrunk. -/ def NoShrink (α : Type u) := α - +open Lean in +instance [inst: ToExpr α] : ToExpr (NoShrink α) := + { + toExpr := fun x => inst.toExpr x + toTypeExpr := inst.toTypeExpr + } namespace NoShrink def mk (x : α) : NoShrink α := x @@ -382,7 +469,7 @@ instance repr [inst : Repr α] : Repr (NoShrink α) := inst instance shrinkable : Shrinkable (NoShrink α) where shrink := fun _ => [] -instance sampleableExt [SampleableExt α] [Repr α] : SampleableExt (NoShrink α) := +instance sampleableExt [SampleableExt α] [Repr α] [Lean.ToExpr α] : SampleableExt (NoShrink α) := SampleableExt.mkSelfContained <| (NoShrink.mk ∘ SampleableExt.interp) <$> SampleableExt.sample end NoShrink diff --git a/Plausible/Vacuous.lean b/Plausible/Vacuous.lean new file mode 100644 index 00000000..ec247034 --- /dev/null +++ b/Plausible/Vacuous.lean @@ -0,0 +1,50 @@ +import Lean +import Plausible +import Plausible.MetaTestable +/-! +## Vacuous Implication + +The `vacuous` tactic is used to prove vacuous implications. We use the plausible search for counterexamples (actually at the `MetaTestable` level) to find a counterexample to the hypothesis. If a counterexample is found, we can prove the vacuous implication by showing that the hypothesis is never satisfied. +-/ + +open Lean Meta Elab Tactic Plausible + +partial def proveVacuous? (p: Expr) (cfg : Configuration := {}) : MetaM <| Option Expr := do + match p with + | .forallE n d b bi => + withLocalDecl n bi d fun x => do + let b := b.instantiate1 x + let contra? ← try + disproveM? cfg d -- proof of ¬d + catch _ => + pure none + match contra? with + | some contra => + logInfo m!"Vacuous Implication. Hypothesis {← ppExpr d} is never satisfied" + let pfFalse ← mkAppM' contra #[x] + let pfBody ← mkAppOptM ``False.elim #[b, pfFalse] + mkLambdaFVars #[x] pfBody + | none => + let inner ← proveVacuous? b cfg + inner.mapM fun pf => mkLambdaFVars #[x] pf + | _ => + return none + +open Lean.Parser.Tactic + +syntax (name := vacuousSyntax) "vacuous" (config)? : tactic +elab_rules : tactic | `(tactic| vacuous $[$cfg]?) => withMainContext do + let cfg ← elabConfig (mkOptionalNode cfg) let (_, g) ← (← getMainGoal).revert ((← getLocalHyps).map (Expr.fvarId!)) + let cfg := { cfg with + traceDiscarded := cfg.traceDiscarded || (← isTracingEnabledFor `plausible.discarded), + traceSuccesses := cfg.traceSuccesses || (← isTracingEnabledFor `plausible.success), + traceShrink := cfg.traceShrink || (← isTracingEnabledFor `plausible.shrink.steps), + traceShrinkCandidates := cfg.traceShrinkCandidates + || (← isTracingEnabledFor `plausible.shrink.candidates) } + g.withContext do + let tgt ← g.getType + match ← proveVacuous? tgt cfg with + | some pf => + g.assign pf + | none => + throwError "no vacuous proof found" diff --git a/Test/MetaTestable.lean b/Test/MetaTestable.lean new file mode 100644 index 00000000..4287ed36 --- /dev/null +++ b/Test/MetaTestable.lean @@ -0,0 +1,191 @@ +import Lean +import Plausible.MetaTestable + +open Plausible Plausible.MetaTestable +open Lean Meta Elab Term Tactic + +-- Testing the pattern matching functions +open Lean Elab Term in +elab "#decompose_prop" t:term : command => + Command.liftTermElabM do + let e ← elabType t + match ← orProp? e with + | (some α, some β) => logInfo s!"Or: {← ppExpr α}; {← ppExpr β}" + | _ => pure () + match ← andProp? e with + | (some α, some β) => logInfo s!"And: {← ppExpr α}; {← ppExpr β}" + | _ => pure () + match ← existsProp? e with + | (some α, some β) => logInfo s!"Exists: {← ppExpr α}; domain {← ppExpr β}" + | _ => pure () + match ← forallProp? e with + | (some α, some β) => logInfo s!"Forall: {← ppExpr α}; domain {← ppExpr β}" + | _ => pure () + match ← impProp? e with + | (some α, some β) => logInfo s!"Implies: {← ppExpr α}; {← ppExpr β}" + | _ => pure () + match ← eqlProp? e with + | some (α, a, b) => logInfo s!"Eq: {← ppExpr α}; {← ppExpr a} and {← ppExpr b}" + | _ => pure () + match ← iffProp? e with + | some (α, β) => logInfo s!"Iff: {← ppExpr α}; {← ppExpr β}" + | _ => pure () + +/-- info: Forall: fun x => x = 0 ∨ x ≠ 0; domain Nat -/ +#guard_msgs in +#decompose_prop ∀ (n: Nat), n = 0 ∨ n ≠ 0 + +/-- info: Forall: fun x => x = 0 ∨ x ≠ 0; domain Nat -/ +#guard_msgs in +#decompose_prop NamedBinder "blah" <| ∀ (n: Nat), n = 0 ∨ n ≠ 0 + +/-- info: Or: 1 = 0; 2 ≠ 0 -/ +#guard_msgs in +#decompose_prop 1 = 0 ∨ 2 ≠ 0 + +/-- info: And: 1 = 0; 2 ≠ 0 -/ +#guard_msgs in +#decompose_prop 1 = 0 ∧ 2 ≠ 0 + +/-- info: Exists: fun n => n = 0 ∨ n ≠ 0; domain Nat -/ +#guard_msgs in +#decompose_prop ∃ (n: Nat), n = 0 ∨ n ≠ 0 + +/-- +info: Forall: fun x => 2 ≠ 0; domain 1 = 0 +--- +info: Implies: 1 = 0; 2 ≠ 0 +-/ +#guard_msgs in +#decompose_prop 1 = 0 → 2 ≠ 0 + + +/-- info: Iff: 1 = 0; 2 ≠ 0 -/ +#guard_msgs in +#decompose_prop 1 = 0 ↔ 2 ≠ 0 + +-- Elaborater to help with testing +elab "disprove%" t:term : term => do + let tgt ← elabType t + let cfg : Configuration := {} + let (some code') ← disproveM? cfg tgt | throwError "disprove% failed" + logInfo s!"disproof: {← ppExpr code'}; \ntype: {← ppExpr <| (← inferType code')}" + return tgt + +-- Testing the disproveM? function +/-- +info: +=================== +Found a counter-example! +a := 0 +b := 0 +issue: 0 < 0 does not hold +(0 shrinks) +------------------- +--- +info: disproof: mt (fun x => x (SampleableExt.interp 0)) (mt (fun x => x (SampleableExt.interp 0)) (of_decide_eq_false (Eq.refl false))); ⏎ +type: ¬∀ (a b : Nat), a < b +--- +info: ∀ (a b : Nat), a < b : Prop +-/ +#guard_msgs in +#check disprove% ∀ (a b : Nat), a < b + +/-- +info: +=================== +Found a counter-example! +a := 0 +b := 0 +issue: 0 < 0 does not hold +issue: 0 < 0 does not hold +(0 shrinks) +------------------- +--- +info: disproof: mt (fun x => x (SampleableExt.interp 0)) + (mt (fun x => x (SampleableExt.interp 0)) + (Or.rec (of_decide_eq_false (Eq.refl false)) (of_decide_eq_false (Eq.refl false)))); ⏎ +type: ¬∀ (a b : Nat), a < b ∨ b < a +--- +info: ∀ (a b : Nat), a < b ∨ b < a : Prop +-/ +#guard_msgs in +#check disprove% ∀ (a b : Nat), a < b ∨ b < a + +/-- +info: +=================== +Found a counter-example! +issue: False does not hold +(0 shrinks) +------------------- +--- +info: disproof: fun h => of_decide_eq_false (Eq.refl false) h.left; ⏎ +type: False ∧ False → False +--- +info: False ∧ False : Prop +-/ +#guard_msgs in +#check disprove% False ∧ False + + +elab "#expr" e:term : command => + Command.liftTermElabM do + let e ← elabTerm e none + logInfo s!"{repr e}" + logInfo s!"{← reduce e}" + +elab "expr%" e:term : term => do + let e ← elabTerm e none + logInfo s!"{repr e}" + logInfo s!"{← reduce e}" + return e + +-- Testing the MetaTestable class can be inferred +example : MetaTestable <| (1: Nat) = 0 := inferInstance + +example : MetaTestable (NamedBinder "a" (∀ (a : Nat), a ≤ 1)) := inferInstance + +example : MetaTestable (NamedBinder "a" (∀ (a : Nat), NamedBinder "b" (∀ (b : Nat), a ≤ b))) := inferInstance + +-- Main tests: finding counterexamples +#eval MetaTestable.seek (∀ (_a : Nat), False) (propExpr := Lean.Expr.forallE `a (Lean.Expr.const `Nat []) (Lean.Expr.const `False []) (Lean.BinderInfo.default)) + + +#eval MetaTestable.seek (∀ (a : Nat), a < 1) (propExpr := Lean.Expr.forallE `a (Lean.Expr.const `Nat []) (Lean.Expr.const `False []) (Lean.BinderInfo.default)) + +#eval MetaTestable.seek (∀ (a b : Nat), a < b) (propExpr := (Lean.Expr.forallE + `a + (Lean.Expr.const `Nat []) + (Lean.Expr.forallE + `b + (Lean.Expr.const `Nat []) + (Lean.Expr.app + (Lean.Expr.app + (Lean.Expr.app + (Lean.Expr.app + (Lean.Expr.const `LT.lt [Level.succ Level.zero]) + (Lean.Expr.const `Nat [])) + (Lean.Expr.const `instLTNat [])) + (Lean.Expr.bvar 1)) + (Lean.Expr.bvar 0)) + (Lean.BinderInfo.default)) + (Lean.BinderInfo.default))) + +#eval MetaTestable.seek (∀ (a _b : Nat), a < 0) (propExpr := (Lean.Expr.forallE + `a + (Lean.Expr.const `Nat []) + (Lean.Expr.forallE + `b + (Lean.Expr.const `Nat []) + (Lean.Expr.app + (Lean.Expr.app + (Lean.Expr.app + (Lean.Expr.app + (Lean.Expr.const `LT.lt [Level.succ Level.zero]) + (Lean.Expr.const `Nat [])) + (Lean.Expr.const `instLTNat [])) + (Lean.Expr.bvar 1)) + (Lean.Expr.lit (Lean.Literal.natVal 0))) + (Lean.BinderInfo.default)) + (Lean.BinderInfo.default))) diff --git a/Test/RandomSeach.lean b/Test/RandomSeach.lean new file mode 100644 index 00000000..a28a36af --- /dev/null +++ b/Test/RandomSeach.lean @@ -0,0 +1,42 @@ +import Plausible.RandomSearch + +open Plausible + +/- +¬1 = 4 : Prop +-/ +#check neg_neg (1 = 4) + +/- +Negation of ¬1 = 4 is 1 = 4 +-/ +#check neg_neg ¬(1 = 4) + +/- +Proof of negation is fun h => + induced_and id (not_not (2 < 4)) + (not_or_mp h) with type ¬(1 = 4 ∨ ¬2 < 4) → ¬1 = 4 ∧ 2 < 4, should be ¬(1 = 4 ∨ ¬2 < 4) → ¬1 = 4 ∧ 2 < 4 +-/ +#check neg_neg ¬(1 = 4) ∧ (2 < 4) + +/- +check: true +-/ +#check neg_neg (1 = 4) ∨ (¬ (2 < 4)) + +/- +check: true +-/ +#check neg_neg ∃ x : Nat, x > 0 + +example : ¬ (1 = 4) := by + /- + Found a proof by negated counter-example! + -/ + random_search + +example : ∃ n : Nat, n > 0 ∧ n < 4 := by + /- + Found a proof by negated counter-example! + -/ + random_search diff --git a/Test/Testable.lean b/Test/Testable.lean index 6df0b4b7..516df023 100644 --- a/Test/Testable.lean +++ b/Test/Testable.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ import Plausible.Testable +import Plausible.MetaTestable open Plausible @@ -19,9 +20,12 @@ instance : Shrinkable MyType where proxy.map (fun (fst, snd) => ⟨fst, fst + snd, by omega⟩) instance : SampleableExt MyType := - SampleableExt.mkSelfContained do + SampleableExt.mkSelfContainedSimple do let x ← SampleableExt.interpSample Nat let xyDiff ← SampleableExt.interpSample Nat return ⟨x, x + xyDiff, by omega⟩ #eval Testable.check <| ∀ a b : MyType, a.y ≤ b.x → a.x ≤ b.y + +set_option trace.profiler true in +#eval MetaTestable.check <| ∀ a b : MyType, a.y ≤ b.x → a.x ≤ b.y diff --git a/Test/Vacuous.lean b/Test/Vacuous.lean new file mode 100644 index 00000000..9e34ff89 --- /dev/null +++ b/Test/Vacuous.lean @@ -0,0 +1,37 @@ +import Plausible.Vacuous +open Lean Meta Elab + +elab "prove_vacuous" type:term : term => do + let p ← Term.elabType type + let vacuous ← proveVacuous? p + match vacuous with + | some pf => + return pf + | none => + logWarning m!"No vacuous proof found" + return mkConst ``False + +/-- +info: +=================== +Found a counter-example! +issue: 2 < 1 does not hold +(0 shrinks) +------------------- +--- +info: Vacuous Implication. Hypothesis 2 < 1 is never satisfied +--- +info: fun a => False.elim (of_decide_eq_false (Eq.refl false) a) : 2 < 1 → 1 ≤ 3 +-/ +#guard_msgs in +#check prove_vacuous ((2 : Nat) < 1) → 1 ≤ 3 + +-- We cannot use `guard_msgs` here because of random search. Need to add seeds as a parameter. + +#check prove_vacuous (∀ n: Nat, n < (4: Nat)) → 1 ≤ 3 + +example : (∀ n: Nat, n < (4: Nat)) → 4 ≤ 3 := by vacuous + +example (h: ∀ n: Nat, n < (4: Nat)) : 4 ≤ 3 := by vacuous + +example (m: Nat) (h: ∀ n: Nat, n < (4: Nat)) : m ≤ 3 := by vacuous diff --git a/lake-manifest.json b/lake-manifest.json index 7cbf64a0..567e5e86 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,5 +1,25 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", - "packages": [], + "packages": + [{"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "aa4c87abed970d9dfad2506000d99d30b02f476b", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.19.0-rc2", + "inherited": false, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "ff4cd734811e5ab091cef2acb4d805737670eced", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.19.0-rc2", + "inherited": false, + "configFile": "lakefile.toml"}], "name": "plausible", "lakeDir": ".lake"} diff --git a/lakefile.toml b/lakefile.toml index e12448bc..37499536 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -8,3 +8,13 @@ name = "Test" [[lean_lib]] name = "Plausible" + +[[require]] +name = "batteries" +scope = "leanprover-community" +rev = "v4.19.0-rc2" + +[[require]] +name = "Qq" +scope = "leanprover-community" +rev = "v4.19.0-rc2"