import Mathlib.Testing.Plausible.Functions

error:

Found a counter-example! x := 0 y := 0 issue: 0 ≠ 0 does not hold (0 shrinks)

#guard_msgs
Error: ❌️ Docstring on `#guard_msgs` does not match generated message:

-
+ error:
+ ===================
+ Found a counter-example!
+ x := 0
+ y := 0
+ issue: 0 ≠ 0 does not hold
+ (0 shrinks)
+ -------------------
 (whitespace := lax) in
#eval
Error: 
===================
Found a counter-example!
x := 0
y := 0
issue: 0 ≠ 0 does not hold
(0 shrinks)
------------------- 
Plausible.Testable.check: (p : Prop) →
  optParam Plausible.Configuration { } →
    (p' : autoParam (Plausible.Decorations.DecorationsOf p) Plausible.Testable.check._auto_1) →
      [Plausible.Testable p'] → Lean.CoreM PUnit.{1}
Plausible.Testable.check (∀ (
x: ℕ
x 
y: ℕ
y : 
Nat: Type
Nat), 
x: ℕ
x + 
y: ℕ
y ≠ 
y: ℕ
y + 
x: ℕ
x)

instance 
Plausible.Testable.existsTestable: {α : Sort u_1} →
  {var : String} →
    (p : Prop) →
      {β : α → Prop} →
        [Testable (NamedBinder var (∀ (x : α), NamedBinder var (β x → p)))] →
          Testable (NamedBinder var (NamedBinder var (∃ x, β x) → p))
Plausible.Testable.existsTestable (
p: Prop
p : 
Prop: Type
Prop) {
β: α → Prop
β : 
α: Sort u_1
α → 
Prop: Type
Prop}
  [
Testable: Prop → Type
Testable (
NamedBinder: String → Prop → Prop
NamedBinder 
var: String
var (∀ 
x: α
x, 
NamedBinder: String → Prop → Prop
NamedBinder 
var: String
var $ 
β: α → Prop
β 
x: α
x → 
p: Prop
p))] :
  
Testable: Prop → Type
Testable (
NamedBinder: String → Prop → Prop
NamedBinder 
var: String
var (
NamedBinder: String → Prop → Prop
NamedBinder 
var: String
var (∃ 
x: α
x, 
β: α → Prop
β 
x: α
x) → 
p: Prop
p)) where
  run := λ 
cfg: Configuration
cfg 
min: Bool
min => do
    let 
x: TestResult (NamedBinder var (∀ (x : α), NamedBinder var (β x → p)))
x ← 
Testable.runProp: (p : Prop) → [Testable p] → Configuration → Bool → Gen (TestResult p)
Testable.runProp (
NamedBinder: String → Prop → Prop
NamedBinder 
var: String
var (∀ 
x: α
x, 
NamedBinder: String → Prop → Prop
NamedBinder 
var: String
var $ 
β: α → Prop
β 
x: α
x → 
p: Prop
p)) 
cfg: Configuration
cfg 
min: Bool
min
    
pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
pure $ 
Plausible.TestResult.iff: {p q : Prop} → (q ↔ p) → TestResult p → TestResult q
Plausible.TestResult.iff 
exists_imp: ∀ {α : Sort u_1} {p : α → Prop} {b : Prop}, (∃ x, p x) → b ↔ ∀ (x : α), p x → b
exists_imp 
x: TestResult (NamedBinder var (∀ (x : α), NamedBinder var (β x → p)))
x

#eval
Unable to find a counter-example 
Plausible.Testable.check: (p : Prop) →
  optParam Plausible.Configuration { } →
    (p' : autoParam (Plausible.Decorations.DecorationsOf p) Plausible.Testable.check._auto_1) →
      [Plausible.Testable p'] → Lean.CoreM PUnit.{1}
Plausible.Testable.check (∀ (
x: ℕ
x 
y: ℕ
y : 
Nat: Type
Nat), 
x: ℕ
x + 
y: ℕ
y = 
y: ℕ
y + 
x: ℕ
x)

lemma 
ex1: ∀ (v : ℕ × ℕ), v.1 + v.2 = v.2 + v.1
ex1 : ∀ (
v: ℕ × ℕ
v : 
Nat: Type
Nat × 
Nat: Type
Nat), 
v: ℕ × ℕ
v.
1: {α β : Type} → α × β → α
1 + 
v: ℕ × ℕ
v.
2: {α β : Type} → α × β → β
2 = 
v: ℕ × ℕ
v.
2: {α β : Type} → α × β → β
2 + 
v: ℕ × ℕ
v.
1: {α β : Type} → α × β → α
1 := by
Goals accomplished! 🐙
  exact fun 
v: ℕ × ℕ
v => 
Nat.add_comm: ∀ (n m : ℕ), n + m = m + n
Nat.add_comm 
v: ℕ × ℕ
v.
1: {α β : Type} → α × β → α
1 
v: ℕ × ℕ
v.
2: {α β : Type} → α × β → β
2
Goals accomplished! 🐙

lemma 
ex2: ∀ (v : ℕ × ℕ), v.1 + v.2 ≠ v.2 + v.1 → false = true
ex2 : ∀ (
v: ℕ × ℕ
v : 
Nat: Type
Nat × 
Nat: Type
Nat), 
v: ℕ × ℕ
v.
1: {α β : Type} → α × β → α
1 + 
v: ℕ × ℕ
v.
2: {α β : Type} → α × β → β
2 ≠ 
v: ℕ × ℕ
v.
2: {α β : Type} → α × β → β
2 + 
v: ℕ × ℕ
v.
1: {α β : Type} → α × β → α
1 → 
false: Bool
false := by
Goals accomplished! 🐙
  intro 
h: ℕ × ℕ
h
h: ℕ × ℕ
h.1 + h.2 ≠ h.2 + h.1 → false = true
  simp?
Try this:
  [apply] simp only [ne_eq, Bool.false_eq_true, imp_false, Decidable.not_not]
h: ℕ × ℕ
h.1 + h.2 = h.2 + h.1
  exact?
Try this:
  [apply] exact ex1 h
Goals accomplished! 🐙

#eval
Warning: Gave up after failing to generate values that fulfill the preconditions 100 times. 
Plausible.Testable.check: (p : Prop) →
  optParam Plausible.Configuration { } →
    (p' : autoParam (Plausible.Decorations.DecorationsOf p) Plausible.Testable.check._auto_1) →
      [Plausible.Testable p'] → Lean.CoreM PUnit.{1}
Plausible.Testable.check (∀ (
v: ℕ × ℕ
v : 
Nat: Type
Nat × 
Nat: Type
Nat), 
v: ℕ × ℕ
v.
1: {α β : Type} → α × β → α
1 + 
v: ℕ × ℕ
v.
2: {α β : Type} → α × β → β
2 ≠ 
v: ℕ × ℕ
v.
2: {α β : Type} → α × β → β
2 + 
v: ℕ × ℕ
v.
1: {α β : Type} → α × β → α
1 → 
false: Bool
false)

-- set_option trace.Meta.synthInstance true in
-- #eval Plausible.Testable.check (∃ (v : Nat × Nat), v.1 + v.2 ≠ v.2 + v.1 → false)

lemma 
ex'': ∀ (x y : ℕ), x + y = y + x
ex'' : ∀ (
x: ℕ
x 
y: ℕ
y : 
Nat: Type
Nat), 
x: ℕ
x + 
y: ℕ
y = 
y: ℕ
y + 
x: ℕ
x := by
Goals accomplished! 🐙
  exact 
Nat.add_comm: ∀ (n m : ℕ), n + m = m + n
Nat.add_comm
Goals accomplished! 🐙

example: (∃ x y, x + y ≠ y + x) → false = true
example : (∃ (
x: ℕ
x 
y: ℕ
y : 
Nat: Type
Nat), 
x: ℕ
x + 
y: ℕ
y ≠ 
y: ℕ
y + 
x: ℕ
x) → 
false: Bool
false := by
Goals accomplished! 🐙
  intro 
h: ∃ x y, x + y ≠ y + x
h
h: ∃ x y, x + y ≠ y + x
false = true
  obtain 
⟨x, y, h⟩: ∃ y, x + y ≠ y + x
⟨
x: ℕ
x
⟨x, y, h⟩: ∃ y, x + y ≠ y + x
, 
y: ℕ
y
⟨x, y, h⟩: ∃ y, x + y ≠ y + x
, 
h: x + y ≠ y + x
h
⟨x, y, h⟩: ∃ y, x + y ≠ y + x
⟩ := 
h: ∃ x y, x + y ≠ y + x
h
x, y: ℕ
h: x + y ≠ y + x
false = true
  have 
h': x + y = y + x
h' : 
x: ℕ
x + 
y: ℕ
y = 
y: ℕ
y + 
x: ℕ
x := 
ex'': ∀ (x y : ℕ), x + y = y + x
ex'' 
x: ℕ
x 
y: ℕ
y
x, y: ℕ
h: x + y ≠ y + x
h':= ex'' x y: x + y = y + x
false = true
  contradiction
Goals accomplished! 🐙