doing induction

Stream: mathlib4

[Antoine Chambert-Loir]

Imagine I want to prove a property of x : A, and I have a function f : A -> B, where B is well ordered. Can I do it by induction, thanks to some ‘termination-by‘ stuff? But I can't understand what I need to fill in. (This is to prove 'euclDivd‘ in branch#ACL/CombNS)

[Antoine Chambert-Loir]

A mwe could be

 import Init.WF

theorem hasP (A B : Type) (r : B → B → Prop) (hr : WellFounded r)
    (f : A → B) (P : A → Prop)  (a : A) : P a := by
  sorry

where, in the proof, I only apply hasP to elements b : A such that r b a.

[Bjørn Kjos-Hanssen]

The mwe theorem is false (P could be fun a => False)...?

[Giacomo Stevanato]

Have you seen WellFounded.induction?

I guess in your mwe you meant P and f to not be part of the theorem and instead something you defined yourself?

[Edward van de Meent]

i'd guess you need a statement saying that r is wellfounded on the range of f, along with a statement like wf_hyp : ∀ a, (∀ a', r (f a') (f a) → P a') → P a

[Edward van de Meent]

i think the first part is easily satisfied if r is a transitive relation?

[Edward van de Meent]

i'm not very sure though

[Johan Commelin]

You can indeed use termination by.
So just write the proof as usual, and put a sorry to get rid of the termination goal. Then focus on it separately when you are done

[Johan Commelin]

You can also use decreasing_by to apply your f

[Antoine Chambert-Loir]

Giacomo Stevanato said:

Have you seen WellFounded.induction?

I guess in your mwe you meant P and f to not be part of the theorem and instead something you defined yourself?

In my not minimal example (see branch#ACL/CombNS), fis a multivariate polynomial and P is a complicated property, so docs#WellFounded.induction does not immediately apply. Of course, I could set up some induction procedure, but my point was to have it on the spot, just having a function applying itself recursively, while checking that the things I apply it to are always strictly smaller than my initial stuff.

[Giacomo Stevanato]

Antoine Chambert-Loir said:

fis a multivariate polynomial and P is a complicated property, so docs#WellFounded.induction does not immediately apply.

I'm not sure why you think that is the case. From a quick glance it seems you should be able to apply it right after creating the instance of the well-founded relation.

[Violeta Hernández]

Sometimes induction lemmas don't like playing nice with apply, so you might want to use the induction or refine tactics with them instead.

[Giacomo Stevanato]

This seems to work for me:

diff --git a/Mathlib/Combinatorics/Nullstellensatz.lean b/Mathlib/Combinatorics/Nullstellensatz.lean
index 5b39e4d..18410f3 100644
--- a/Mathlib/Combinatorics/Nullstellensatz.lean
+++ b/Mathlib/Combinatorics/Nullstellensatz.lean
@@ -624,9 +624,11 @@ theorem euclDivd (S : σ → Finset R) (Sne : ∀ i, (S i).Nonempty) (f : MvPoly
       (∀ i, (h i * (S i).prod (fun (s : R) ↦ (X i - C s))).totalDegree ≤ f.totalDegree) ∧
       (∀ i, r.weightedTotalDegree (Finsupp.single i 1) < (S i).card) := by
   letI : LinearOrder σ := WellOrderingRel.isWellOrder.linearOrder
-  haveI wfr : WellFoundedRelation (MvPolynomial σ R) := {
+  let wfr : WellFoundedRelation (MvPolynomial σ R) := {
     rel := Function.onFun (· < ·) fun f ↦ f.lexHomDegree
     wf := WellFounded.onFun wellFounded_lt }
+  apply wfr.wf.induction f
+  intro f h_ind
   by_cases hD0 : f.lexHomDegree = ⊥
   · use fun _ ↦ 0, f
     rw [lexHomDegree_eq_bot_iff] at hD0
@@ -663,7 +665,7 @@ theorem euclDivd (S : σ → Finset R) (Sne : ∀ i, (S i).Nonempty) (f : MvPoly
       rw [lt_iff_le_and_ne, ← hd]
       exact ⟨le_lexHomDegree hc.2, fun h ↦ hc.1 (toLexHom.injective h)⟩
     · exact Ne.bot_lt' fun a ↦ hD0 a.symm
-  obtain ⟨h', r', Hf', Hh', Hr'⟩ := euclDivd S Sne f' -- hf'D
+  obtain ⟨h', r', Hf', Hh', Hr'⟩ := h_ind f' hf'D
   by_cases H : ∀ i, d i < (S i).card
   · -- First case, the monomial `d` is small, we just add it to the remainder
     use h', r' + monomial d (f.coeff d)
@@ -782,7 +784,7 @@ theorem euclDivd (S : σ → Finset R) (Sne : ∀ i, (S i).Nonempty) (f : MvPoly
       left
       simp only [lexHomDegree_degree]
       exact hf''_degree
-    obtain ⟨h'', r'', Hf'', Hh'', Hr''⟩ := euclDivd S Sne f'' -- hf''2
+    obtain ⟨h'', r'', Hf'', Hh'', Hr''⟩ := h_ind f'' hf''2
     use h' + h'' + single i (monomial d' (f.coeff d)), r' + r''
     constructor
     · nth_rewrite 1 [hf, Hf', hf'', Hf'']

[Antoine Chambert-Loir]

A similar thing worked for me as well (see commented out code just below), but I expected to be able to do it differently, by using directly the function on smaller arguments.

[Violeta Hernández]

FYI WellFoundedRelation is probably not what you want to be using. The purpose of that typeclass is to establish a default well-founded relation for the termination checker whenever you're working with a certain type. If you just want a well-founded predicate you can use WellFounded, and if you want a bundled version that works with typeclass inference you can use IsWellFounded or something stronger like WellFoundedLT or IsWellOrder.

[Antoine Chambert-Loir]

I had used IsWellFounded but devised an additional induction theorem for docs#MvPolynomial for lexicographic order (see the commented out proof of euclDivd in the branch). My question (sorry if I didn't make myself clearer) came out of wondering whether this additional theorem was indeed necessary or if it is possible to prove a theorem directly along the lines of the current attempt.
Maybe the difficulty is that I use the function twice, for two different arguments f' and f'', each of them smaller than the initial one. Possibly, terminating_by doesn't understand what I need.

By the way, the error message is

Not considering parameter R of MvPolynomial.euclDivd:
  it is unchanged in the recursive calls
Not considering parameter #2 of MvPolynomial.euclDivd:
  it is unchanged in the recursive calls
Not considering parameter σ of MvPolynomial.euclDivd:
  it is unchanged in the recursive calls
Not considering parameter #4 of MvPolynomial.euclDivd:
  it is unchanged in the recursive calls
Not considering parameter S of MvPolynomial.euclDivd:
  it is unchanged in the recursive calls
Not considering parameter Sne of MvPolynomial.euclDivd:
  it is unchanged in the recursive calls
Cannot use parameter f:
  the type (σ →₀ ℕ) →₀ R does not have a `.brecOn` recursor


Could not find a decreasing measure.
The arguments relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)

1) 666:36-53
2) 785:43-61
Please use `termination_by` to specify a decreasing measure.

and the decreasing measures are proved in hf'D : f'.lexHomDegree < f.lexHomDegree (just before line 666) and hf''2 : f''.lexHomDegree < f.lexHomDegree (just before line 785). In both cases, MvPolynomial.lexHomDegree is a function from MvPolynomial α R to a type synonym LexHom (α →₀ N) of monomials α →₀ N but endowed with a well ordering (see instance on line 199, WellFoundedLT (LexHom (α →₀ N)).

[Giacomo Stevanato]

I believe you need to use WellFounded.wrap to use an arbitrary WellFounded relation with termination_by (or add an instance for that WellFoundedRelation outside the theorem, but this should be cleaner):

diff --git a/Mathlib/Combinatorics/Nullstellensatz.lean b/Mathlib/Combinatorics/Nullstellensatz.lean
index 5b39e4d..eb0ef5b 100644
--- a/Mathlib/Combinatorics/Nullstellensatz.lean
+++ b/Mathlib/Combinatorics/Nullstellensatz.lean
@@ -618,15 +618,13 @@ lemma prod_totalDegree [Nontrivial R] {ι : Type*} (i : ι) (s : Finset R) :
   rw [mem_support_iff, prod_leadCoeff]
   exact one_ne_zero

+noncomputable instance : LinearOrder σ := WellOrderingRel.isWellOrder.linearOrder
+
 theorem euclDivd (S : σ → Finset R) (Sne : ∀ i, (S i).Nonempty) (f : MvPolynomial σ R) :
     ∃ (h : σ → MvPolynomial σ R) (r : MvPolynomial σ R),
       f = Finset.univ.sum (fun i => (h i) * (S i).prod (fun (s : R) ↦ (X i - C s))) + r ∧
       (∀ i, (h i * (S i).prod (fun (s : R) ↦ (X i - C s))).totalDegree ≤ f.totalDegree) ∧
       (∀ i, r.weightedTotalDegree (Finsupp.single i 1) < (S i).card) := by
-  letI : LinearOrder σ := WellOrderingRel.isWellOrder.linearOrder
-  haveI wfr : WellFoundedRelation (MvPolynomial σ R) := {
-    rel := Function.onFun (· < ·) fun f ↦ f.lexHomDegree
-    wf := WellFounded.onFun wellFounded_lt }
   by_cases hD0 : f.lexHomDegree = ⊥
   · use fun _ ↦ 0, f
     rw [lexHomDegree_eq_bot_iff] at hD0
@@ -654,7 +652,7 @@ theorem euclDivd (S : σ → Finset R) (Sne : ∀ i, (S i).Nonempty) (f : MvPoly
     split_ifs with h
     · simp [h]
     · simp [sub_zero, Ne.symm h]
-  haveI hf'D : f'.lexHomDegree < f.lexHomDegree := by
+  have : f'.lexHomDegree < f.lexHomDegree := by
     rw [hd]
     unfold lexHomDegree
     rw [Finset.sup_lt_iff]
@@ -777,7 +775,7 @@ theorem euclDivd (S : σ → Finset R) (Sne : ∀ i, (S i).Nonempty) (f : MvPoly
         apply lt_of_lt_of_le (b := (S i).card)
         simp only [bot_eq_zero', Finset.card_pos, Sne i]
         exact Nat.le_add_left (S i).card d'.degree
-    haveI hf''2 : f''.lexHomDegree < f.lexHomDegree := by
+    have : f''.lexHomDegree < f.lexHomDegree := by
       rw [LexHom.lt_iff]
       left
       simp only [lexHomDegree_degree]
@@ -834,6 +832,8 @@ theorem euclDivd (S : σ → Finset R) (Sne : ∀ i, (S i).Nonempty) (f : MvPoly
       apply lt_of_le_of_lt (weightedTotalDegree_add _)
       simp only [sup_lt_iff]
       exact ⟨Hr' i, Hr'' i⟩
+termination_by LexHom.wellFoundedLT.wf.wrap f.lexHomDegree
+decreasing_by repeat assumption

 /- -- OLD VERSION
 theorem euclDivd (S : σ → Finset R) (Sne : ∀ i, (S i).Nonempty)

[Antoine Chambert-Loir]

Thanks a lot, that's exactly the kind of things I expected was possible.
(repeat assumption did not work, though, but I could insert the proofs at this place.)