Zulip Chat Archive

Stream: new members

Topic: Coding style for recursion


view this post on Zulip 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), }
    }
  }

view this post on Zulip Johan Commelin (May 14 2020 at 07:42):

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

view this post on Zulip 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)

view this post on Zulip Patrick Stevens (May 14 2020 at 07:42):

Oh phew, thanks

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 14 2020 at 07:50):

you do induction m generalizing n; cases n

view this post on Zulip 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