From 68d2d213b04bd7083020dfea6614292840c0bb9d Mon Sep 17 00:00:00 2001
From: Alex J Best <alex.j.best@gmail.com>
Date: Tue, 4 Jan 2022 16:45:18 +0000
Subject: [PATCH] feat(testing/slim_check): teach slim_check about `finsupp`s
 (#10916)

We add some instances so that `slim_check` can generate `finsupp`s and hence try to provide counterexamples for them.
As the way the original slim_check for functions works is to generate a finite list of random values and pick a default for the rest of the values these `total_functions` are quite close to finsupps already, we just have to map the default value to zero, and prove various things about the support.
There might be conceptually nicer ways of building this instance but this seems functional enough.

Seeing as many finsupp defs are classical (and noncomputable) this isn't quite as useful for generating counterexamples as I originally hoped.

See the test at `test/slim_check.lean` for a basic example of usage

I wrote this while working on flt-regular but it is hopefully useful outside of that




Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
---
 src/testing/slim_check/functions.lean | 65 +++++++++++++++++++++++++++
 test/slim_check.lean                  | 34 ++++++++++++++
 2 files changed, 99 insertions(+)

diff --git a/src/testing/slim_check/functions.lean b/src/testing/slim_check/functions.lean
index a05183a357cf5..f57461eff2c5a 100644
--- a/src/testing/slim_check/functions.lean
+++ b/src/testing/slim_check/functions.lean
@@ -5,6 +5,8 @@ Authors: Simon Hudon
 -/
 import data.list.sigma
 import data.int.range
+import data.finsupp.basic
+import data.finsupp.to_dfinsupp
 import tactic.pretty_cases
 import testing.slim_check.sampleable
 import testing.slim_check.testable
@@ -129,6 +131,69 @@ instance pi.sampleable_ext : sampleable_ext (α → β) :=
 
 end
 
+section finsupp
+
+variables [has_zero β]
+/-- Map a total_function to one whose default value is zero so that it represents a finsupp. -/
+@[simp]
+def zero_default : total_function α β → total_function α β
+| (with_default A y) := with_default A 0
+
+variables [decidable_eq α] [decidable_eq β]
+/-- The support of a zero default `total_function`. -/
+@[simp]
+def zero_default_supp : total_function α β → finset α
+| (with_default A y) :=
+  list.to_finset $ (A.erase_dupkeys.filter (λ ab, sigma.snd ab ≠ 0)).map sigma.fst
+
+/-- Create a finitely supported function from a total function by taking the default value to
+zero. -/
+def apply_finsupp (tf : total_function α β) : α →₀ β :=
+{ support := zero_default_supp tf,
+  to_fun := tf.zero_default.apply,
+  mem_support_to_fun := begin
+    intro a,
+    rcases tf with ⟨A, y⟩,
+    simp only [apply, zero_default_supp, list.mem_map, list.mem_filter, exists_and_distrib_right,
+      list.mem_to_finset, exists_eq_right, sigma.exists, ne.def, zero_default],
+    split,
+    { rintro ⟨od, hval, hod⟩,
+      have := list.mem_lookup (list.nodupkeys_erase_dupkeys A) hval,
+      rw (_ : list.lookup a A = od),
+      { simpa, },
+      { simpa [list.lookup_erase_dupkeys, with_top.some_eq_coe], }, },
+    { intro h,
+      use (A.lookup a).get_or_else (0 : β),
+      rw ← list.lookup_erase_dupkeys at h ⊢,
+      simp only [h, ←list.mem_lookup_iff A.nodupkeys_erase_dupkeys,
+        and_true, not_false_iff, option.mem_def],
+      cases list.lookup a A.erase_dupkeys,
+      { simpa using h, },
+      { simp, }, }
+  end }
+
+variables [sampleable α] [sampleable β]
+instance finsupp.sampleable_ext [has_repr α] [has_repr β] : sampleable_ext (α →₀ β) :=
+{ proxy_repr := total_function α β,
+  interp := total_function.apply_finsupp,
+  sample := (do
+    xs ← (sampleable.sample (list (α × β)) : gen (list (α × β))),
+    ⟨x⟩ ← (uliftable.up $ sample β : gen (ulift.{max u v} β)),
+    pure $ total_function.with_default (list.to_finmap' xs) x),
+  shrink := total_function.shrink }
+
+-- TODO: support a non-constant codomain type
+instance dfinsupp.sampleable_ext [has_repr α] [has_repr β] : sampleable_ext (Π₀ a : α, β) :=
+{ proxy_repr := total_function α β,
+  interp := finsupp.to_dfinsupp ∘ total_function.apply_finsupp,
+  sample := (do
+    xs ← (sampleable.sample (list (α × β)) : gen (list (α × β))),
+    ⟨x⟩ ← (uliftable.up $ sample β : gen (ulift.{max u v} β)),
+    pure $ total_function.with_default (list.to_finmap' xs) x),
+  shrink := total_function.shrink }
+
+end finsupp
+
 section sampleable_ext
 open sampleable_ext
 
diff --git a/test/slim_check.lean b/test/slim_check.lean
index 212959f0474ec..7e50cd1a8a419 100644
--- a/test/slim_check.lean
+++ b/test/slim_check.lean
@@ -392,3 +392,37 @@ issue: ¬ true does not hold
   admit,
   trivial,
 end
+
+example (f : ℕ →₀ ℕ) : true :=
+begin
+  have : f = 0,
+  success_if_fail_with_msg
+  { slim_check { random_seed := some 257 } }
+"
+===================
+Found problems!
+
+f := [0 ↦ 1, _ ↦ 0]
+(2 shrinks)
+-------------------
+",
+  admit,
+  trivial,
+end
+
+example (f : Π₀ n : ℕ, ℕ) : true :=
+begin
+  have : f.update 0 0 = 0,
+  success_if_fail_with_msg
+  { slim_check { random_seed := some 257 } }
+"
+===================
+Found problems!
+
+f := [1 ↦ 1, _ ↦ 0]
+(1 shrinks)
+-------------------
+",
+  admit,
+  trivial,
+end