feat(tactic/linarith): modularize coefficient oracle (#3502)

This makes it easy to plug an alternate certificate search method (e.g. simplex-based) into `linarith`, should one desire.



Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>

src/tactic/linarith/datatypes.lean

@@ -256,6 +256,18 @@ do l ← pp.transform l,
 meta instance : has_coe preprocessor global_preprocessor :=
 ⟨preprocessor.globalize⟩
 
+/--
+A `certificate_oracle` is a function `produce_certificate : list comp → ℕ → option (rb_map ℕ ℕ)`.
+`produce_certificate hyps max_var` tries to derive a contradiction from the comparisons in `hyps`
+by eliminating all variables ≤ `max_var`.
+If successful, it returns a map `coeff : ℕ → ℕ` as a certificate.
+This map represents that we can find a contradiction by taking the sum  `∑ (coeff i) * hyps[i]`.
+
+The default `certificate_oracle` used by `linarith` is `linarith.fourier_motzkin.produce_certificate`
+-/
+meta def certificate_oracle : Type :=
+list comp → ℕ → option (rb_map ℕ ℕ)
+
 /-- A configuration object for `linarith`. -/
 meta structure linarith_config : Type :=
 (discharger : tactic unit := `[ring])
@@ -265,6 +277,7 @@ meta structure linarith_config : Type :=
 (transparency : tactic.transparency := reducible)
 (split_hypotheses : bool := tt)
 (preprocessors : option (list global_preprocessor) := none)
+(oracle : option certificate_oracle := none)
 
 /--
 `cfg.update_reducibility reduce_semi` will change the transparency setting of `cfg` to

src/tactic/linarith/elimination.lean

@@ -319,8 +319,8 @@ by eliminating all variables ≤ `max_var`.
 If successful, it returns a map `coeff : ℕ → ℕ` as a certificate.
 This map represents that we can find a contradiction by taking the sum  `∑ (coeff i) * hyps[i]`.
 -/
-meta def fourier_motzkin.produce_certificate (hyps : list comp) (max_var : ℕ) :
-  option (rb_map ℕ ℕ) :=
+meta def fourier_motzkin.produce_certificate : certificate_oracle :=
+λ hyps max_var,
 let state := mk_linarith_structure hyps max_var in
 match except_t.run (state_t.run (validate >> elim_all_vars) state) with
 | (except.ok (a, _)) := none

src/tactic/linarith/frontend.lean

@@ -75,10 +75,10 @@ disequality hypotheses, since this would lead to a number of runs exponential in
 disequalities in the context.
 
 The Fourier-Motzkin oracle is very modular. It can easily be replaced with another function of type
-`list comp → ℕ → option (rb_map ℕ ℕ)`, which takes a list of comparisons and the largest variable
+`certificate_oracle := list comp → ℕ → option (rb_map ℕ ℕ)`,
+which takes a list of comparisons and the largest variable
 index appearing in those comparisons, and returns a map from comparison indices to coefficients.
-Because we do not expect another oracle to be available any time soon, there is no convenient hook
-to replace it, but doing so requires only a few lines of code to change.
+An alternate oracle can be specified in the `linarith_config` object.
 
 A variant, `nlinarith`, adds an extra preprocessing step to handle some basic nonlinear goals.
 There is a hook in the `linarith_config` configuration object to add custom preprocessing routines.

src/tactic/linarith/verification.lean

@@ -162,7 +162,7 @@ meta def prove_false_by_linarith (cfg : linarith_config) : list expr → tactic
     let inputs := hz::l',
     -- perform the elimination and fail if no contradiction is found.
     (comps, max_var) ← linear_forms_and_max_var cfg.transparency inputs,
-    certificate ← fourier_motzkin.produce_certificate comps max_var
+    certificate ← cfg.oracle.get_or_else fourier_motzkin.produce_certificate comps max_var
       | fail "linarith failed to find a contradiction",
     linarith_trace "linarith has found a contradiction",
     let enum_inputs := inputs.enum,