Coding style for recursion

Stream: new members

[Patrick Stevens]

Is it considered bad form to use the equation compiler instead of explicit induction? I much, much prefer using the equation compiler like so; it lets me proceed without knowing which induction principle I will require. (Note that the definition of subs_of_size is, as far as I can tell, approximately idiomatic; my question is about the proof of subs_of_size_upper_bound.) I'm aware that my code is complete garbage, with terrible variable names and formatting; I'm only asking whether the overall structure, using the equation compiler to induct for me in a lemma, is considered acceptable for mathlib.

def subs_of_size : Π (m : nat) (i : nat), finset (finset nat)
| 0 0 := finset.singleton finset.empty
| 0 (nat.succ _) := finset.empty
| (nat.succ m) 0 := finset.singleton finset.empty
| (nat.succ m) (nat.succ i) :=
    let from_lower := (subs_of_size m (nat.succ i)) in
    let from_upper := (finset.image (insert m.succ) (subs_of_size m i)) in
    from_lower ∪ from_upper

def subs_of_size_upper_bound : ∀ (m i : nat), ∀ (s : finset nat) (t : s ∈ subs_of_size m i) (x : nat) (u : x ∈ s), x ≤ m
| 0 0 := by {intros s s_in x x_in, unfold subs_of_size at s_in, simp at s_in, rw s_in at x_in, exfalso, exact x_in}
| 0 (nat.succ i) := by {intros s s_in x x_in, unfold subs_of_size at s_in, exfalso, exact s_in}
| (nat.succ m) 0 := by {intros s s_in x x_in, unfold subs_of_size at s_in, simp at s_in, rw s_in at x_in, exfalso, exact x_in}
| (nat.succ m) (nat.succ i) := by
  {
    intros s t x u,
    unfold subs_of_size at t, simp at t,
    cases t,
    {
      exact nat.le_succ_of_le (subs_of_size_upper_bound m i.succ s t x u),
    },
    {
      rcases t with ⟨ a, ⟨ b , c ⟩ ⟩ ,
      rw <- c at u,
      simp at u, cases u,
      { exact le_of_eq u, },
      { exact nat.le_succ_of_le (subs_of_size_upper_bound m i a b x u), }
    }
  }

[Johan Commelin]

No, it's fine. It's done a lot.

[Patrick Stevens]

I ask because I haven't seen any similarly-styled proofs in mathlib yet (which isn't to say that they don't exist)

[Patrick Stevens]

Oh phew, thanks

[Johan Commelin]

But with

begin
  induction foo,
end

you also don't need to know which induction principle you want

[Patrick Stevens]

I got myself into a horrible mess when I wrote the above proof in the lemma blah (m i : nat) (s : finset nat)… form, I just couldn't get the final recursive calls to chain together correctly - is it possible to use induction to match on two naturals simultaneously? The above proof really doesn't want to make two jumps to get from f m.succ n.succ to f m n, I found it very hard to go via f m.succ n or f m n.succ

[Patrick Stevens]

The equation compiler lets me do induction "as God intended", of just assuming that the result is true for any smaller collection of inputs, and I haven't found as intuitive a way of doing that with induction

[Mario Carneiro]

you do induction m generalizing n; cases n

[Reid Barton]

Again, in Lean one would probably use a different strategy from the start, like

import data.finset
import tactic.linarith

def subs_of_size (m i : ℕ) : finset (finset ℕ) :=
(finset.Ico 1 (m+1)).powerset.filter (λ s, s.card = i)

lemma subs_of_size_upper_bound (m i : ℕ) (s : finset ℕ) (t : s ∈ subs_of_size m i)
  (x : ℕ) (hx : x ∈ s) : x ≤ m :=
begin
  have : s ∈ (finset.Ico 1 (m+1)).powerset := (finset.mem_filter.mp t).1,
  rw finset.mem_powerset at this,
  have : x ∈ finset.Ico 1 (m + 1) := this hx,
  rw finset.Ico.mem at this,
  linarith
end