Built with Alectryon. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+πŸ–±οΈ to focus. On Mac, use ⌘ instead of Ctrl.
Hover-Settings: Show types: Show goals:
import Mathlib.Testing.SlimCheck.Functions

info:

error:

Found problems! x := 0 y := 0 issue: 0 β‰  0 does not hold (0 shrinks)

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

info: 
---
error:
===================
Found problems!
x := 0
y := 0
issue: 0 β‰  0 does not hold
(0 shrinks)
-------------------
 (whitespace := lax) in

Error: 
===================
Found problems!
x := 0
y := 0
issue: 0 β‰  0 does not hold
(0 shrinks)
-------------------
 
Error: 
===================
Found problems!
x := 0
y := 0
issue: 0 β‰  0 does not hold
(0 shrinks)
-------------------
Goals accomplished! πŸ™
 
Error: 
===================
Found problems!
x := 0
y := 0
issue: 0 β‰  0 does not hold
(0 shrinks)
-------------------


instance 
SlimCheck.Testable.existsTestable: {Ξ± : Sort u_1} β†’
  {var : String} β†’
    (p : Prop) β†’
      {Ξ² : Ξ± β†’ Prop} β†’
        [inst : Testable (NamedBinder var (βˆ€ (x : Ξ±), NamedBinder var (Ξ² x β†’ p)))] β†’
          Testable (NamedBinder var (NamedBinder var (βˆƒ x, Ξ² x) β†’ p))
SlimCheck.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) β†’ [inst : 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 $ 
SlimCheck.TestResult.iff: {p q : Prop} β†’ (q ↔ p) β†’ TestResult p β†’ TestResult q
SlimCheck.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


 
Goals accomplished! πŸ™
 (βˆ€ (
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 := 
Goals accomplished! πŸ™

  
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 := 
Goals accomplished! πŸ™

  
h: β„• Γ— β„•
h.1 + h.2 β‰  h.2 + h.1 β†’ false = true

  
Try this: simp only [ne_eq, Bool.false_eq_true, imp_false, Decidable.not_not]
h: β„• Γ— β„•
h.1 + h.2 = h.2 + h.1

  
Try this: exact ex1 h
Goals accomplished! πŸ™



 
Goals accomplished! πŸ™
 (βˆ€ (
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 SlimCheck.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 := 
Goals accomplished! πŸ™

  
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 := 
Goals accomplished! πŸ™

  
h: βˆƒ x y, x + y β‰  y + x
false = true

  
x, y: β„•
h: x + y β‰  y + x
intro.intro
false = true

  
x, y: β„•
h: x + y β‰  y + x
h': x + y = y + x
intro.intro
false = true

  
Goals accomplished! πŸ™