## Stream: new members

### Topic: Coding style for recursion

#### Patrick Stevens (May 14 2020 at 07:40):

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 (May 14 2020 at 07:42):

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

#### Patrick Stevens (May 14 2020 at 07:42):

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

Oh phew, thanks

#### Johan Commelin (May 14 2020 at 07:43):

But with

begin
induction foo,
end


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

#### Patrick Stevens (May 14 2020 at 07:47):

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 (May 14 2020 at 07:49):

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 (May 14 2020 at 07:50):

you do induction m generalizing n; cases n

#### Reid Barton (May 14 2020 at 08:37):

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


Last updated: May 09 2021 at 20:11 UTC