chore: add porting headers to slim_check files (#5505)

Just so these get marked off the dashboard. These files have already been ported by hand.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib/Control/Random.lean

@@ -2,7 +2,13 @@
 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
+
+! This file was ported from Lean 3 source module control.random
+! leanprover-community/mathlib commit fdc286cc6967a012f41b87f76dcd2797b53152af
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
+
 import Mathlib.Init.Algebra.Order
 import Mathlib.Init.Data.Nat.Lemmas
 import Mathlib.Init.Data.Int.Order
@@ -11,17 +17,23 @@ import Mathlib.Data.Nat.Basic
 
 /-!
 # Rand Monad and Random Class
+
 This module provides tools for formulating computations guided by randomness and for
 defining objects that can be created randomly.
+
 ## Main definitions
-  * `Rand` and `RandG` monad for computations guided by randomness;
-  * `Random` class for objects that can be generated randomly;
-    * `random` to generate one object;
-  * `BoundedRandom` class for objects that can be generated randomly inside a range;
-    * `randomR` to generate one object inside a range;
-  * `IO.runRand` to run a randomized computation inside the `IO` monad;
+
+* `Rand` and `RandG` monad for computations guided by randomness;
+* `Random` class for objects that can be generated randomly;
+  * `random` to generate one object;
+* `BoundedRandom` class for objects that can be generated randomly inside a range;
+  * `randomR` to generate one object inside a range;
+* `IO.runRand` to run a randomized computation inside the `IO` monad;
+
 ## References
-  * Similar library in Haskell: https://hackage.haskell.org/package/MonadRandom
+
+* Similar library in Haskell: https://hackage.haskell.org/package/MonadRandom
+
 -/
 
 /-- A monad to generate random objects using the generic generator type `g` -/

Mathlib/Testing/SlimCheck/Gen.lean

@@ -2,6 +2,11 @@
 Copyright (c) 2021 Henrik Böving. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving, Simon Hudon
+
+! This file was ported from Lean 3 source module testing.slim_check.testable
+! leanprover-community/mathlib commit fdc286cc6967a012f41b87f76dcd2797b53152af
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 import Mathlib.Control.Random
 import Mathlib.Data.List.Perm
@@ -10,19 +15,22 @@ import Mathlib.Data.Nat.Basic
 
 /-!
 # `Gen` Monad
+
 This monad is used to formulate randomized computations with a parameter
 to specify the desired size of the result.
 This is a port of the Haskell QuickCheck library.
 
 ## Main definitions
-  * `Gen` monad
+
+* `Gen` monad
 
 ## Tags
 
 random testing
 
 ## References
-  * https://hackage.haskell.org/package/QuickCheck
+
+* https://hackage.haskell.org/package/QuickCheck
 -/
 
 namespace SlimCheck

Mathlib/Testing/SlimCheck/Sampleable.lean

@@ -2,16 +2,23 @@
 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
+
+! This file was ported from Lean 3 source module testing.slim_check.testable
+! leanprover-community/mathlib commit fdc286cc6967a012f41b87f76dcd2797b53152af
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 import Mathlib.Testing.SlimCheck.Gen
 import Qq
 
 /-!
 # `SampleableExt` Class
+
 This class permits the creation samples of a given type
 controlling the size of those values using the `Gen` monad.
 
 # `Shrinkable` Class
+
 This class helps minimize examples by creating smaller versions of
 given values.
 
@@ -29,10 +36,12 @@ the test passes and `SlimCheck` moves on to trying more examples.
 This is a port of the Haskell QuickCheck library.
 
 ## Main definitions
-  * `SampleableExt` class
-  * `Shrinkable` class
+
+* `SampleableExt` class
+* `Shrinkable` class
 
 ### `SampleableExt`
+
 `SampleableExt` can be used in two ways. The first (and most common)
 is to simply generate values of a type directly using the `Gen` monad,
 if this is what you want to do then `SampleableExt.mkSelfContained` is
@@ -49,10 +58,12 @@ are using it in the first way, this proxy type will simply be the type
 itself and the `interp` function `id`.
 
 ### `Shrinkable`
+
 Given an example `x : α`, `Shrinkable α` gives us a way to shrink it
 and suggest simpler examples.
 
 ## Shrinking
+
 Shrinking happens when `SlimCheck` find a counter-example to a
 property.  It is likely that the example will be more complicated than
 necessary so `SlimCheck` proceeds to shrink it as much as
@@ -72,7 +83,9 @@ argument, we know that `SlimCheck` is guaranteed to terminate.
 random testing
 
 ## References
-  * https://hackage.haskell.org/package/QuickCheck
+
+* https://hackage.haskell.org/package/QuickCheck
+
 -/
 
 namespace SlimCheck

Mathlib/Testing/SlimCheck/Testable.lean

@@ -2,18 +2,25 @@
 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
+
+! This file was ported from Lean 3 source module testing.slim_check.testable
+! leanprover-community/mathlib commit fdc286cc6967a012f41b87f76dcd2797b53152af
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
 -/
 import Mathlib.Testing.SlimCheck.Sampleable
 import Lean
 
 /-!
 # `Testable` Class
+
 Testable propositions have a procedure that can generate counter-examples
 together with a proof that they invalidate the proposition.
 
 This is a port of the Haskell QuickCheck library.
 
 ## Creating Customized Instances
+
 The type classes `Testable`, `SampleableExt` and `Shrinkable` are the
 means by which `SlimCheck` creates samples and tests them. For instance,
 the proposition `∀ i j : ℕ, i ≤ j` has a `Testable` instance because `ℕ`
@@ -25,18 +32,22 @@ example. This allows the user to create new instances and apply
 `SlimCheck` to new situations.
 
 ### What do I do if I'm testing a property about my newly defined type?
+
 Let us consider a type made for a new formalization:
+
 ```lean
 structure MyType where
   x : ℕ
   y : ℕ
   h : x ≤ y
   deriving Repr
 ```
+
 How do we test a property about `MyType`? For instance, let us consider
 `Testable.check $ ∀ a b : MyType, a.y ≤ b.x → a.x ≤ b.y`. Writing this
 property as is will give us an error because we do not have an instance
 of `Shrinkable MyType` and `SampleableExt MyType`. We can define one as follows:
+
 ```lean
 instance : Shrinkable MyType where
   shrink := λ ⟨x,y,h⟩ =>
@@ -49,44 +60,48 @@ instance : SampleableExt MyType :=
     let xyDiff ← SampleableExt.interpSample Nat
     pure $ ⟨x, x + xyDiff, sorry⟩
 ```
+
 Again, we take advantage of the fact that other types have useful
 `Shrinkable` implementations, in this case `Prod`. Note that the second
 proof is heavily based on `WellFoundedRelation` since its used for termination so
 the first step you want to take is almost always to `simp_wf` in order to
 get through the `WellFoundedRelation`.
 
 ## Main definitions
-  * `Testable` class
-  * `Testable.check`: a way to test a proposition using random examples
+
+* `Testable` class
+* `Testable.check`: a way to test a proposition using random examples
 
 ## Tags
 
 random testing
 
 ## References
-  * https://hackage.haskell.org/package/QuickCheck
+
+* https://hackage.haskell.org/package/QuickCheck
+
 -/
 
 namespace SlimCheck
 
 /-- Result of trying to disprove `p`
 The constructors are:
-  *  `success : (PSum Unit p) → TestResult p`
-     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.
-   * `gaveUp : ℕ → TestResult p`
-     give up when a well-formed example cannot be generated.
-     `gaveUp n` tells us that `n` invalid examples were tried.
-     Above 100, we give up on the proposition and report that we
-     did not find a way to properly test it.
-   * `failure : ¬ p → (List String) → ℕ → TestResult 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.
+*  `success : (PSum Unit p) → TestResult p`
+  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.
+* `gaveUp : ℕ → TestResult p`
+  give up when a well-formed example cannot be generated.
+  `gaveUp n` tells us that `n` invalid examples were tried.
+  Above 100, we give up on the proposition and report that we
+  did not find a way to properly test it.
+* `failure : ¬ p → (List String) → ℕ → TestResult 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.
 -/
 inductive TestResult (p : Prop) where
   | success : PSum Unit p → TestResult p