Create choose.lean #48

ChrisHughes24 · 2018-02-11T16:53:08Z

Definition of choose function for naturals and basic lemmas

johoelzl · 2018-02-14T10:22:30Z

data/nat/choose.lean

+
+@[simp]
+lemma choose_zero_right (n : ℕ) : choose n 0 = 1 := begin
+  cases n with n,unfold choose,unfold choose,


here and anywhere else: move the begin to the next line.

I also think the proof would be clearer as by cases n; refl

johoelzl · 2018-02-14T10:24:19Z

data/nat/choose.lean

+lemma choose_succ_succ (n k : ℕ) : choose (succ n) (succ k) = choose n k + choose n (succ k) := rfl
+
+lemma choose_eq_zero_of_lt {n k : ℕ} : n < k → choose n k = 0 := begin
+  revert k,


instead of reverting at the beginning state your theorem different, i.e. {n : ℕ} : \Pi k, n < k → choose n k = 0

johoelzl · 2018-02-14T10:25:11Z

data/nat/choose.lean

+lemma choose_eq_zero_of_lt {n k : ℕ} : n < k → choose n k = 0 := begin
+  revert k,
+  induction n with n' hi,
+  assume k nk,cases k,exact absurd nk dec_trivial,


avoid writing multiple tactics in one line.
Here you use multiple tactics to proof the first induction step. Please mark it with { ... } and indent it properly.

Also, space after ,

This also goes for further proofs.

johoelzl · 2018-02-14T10:31:00Z

Dear Chris,

this is of course a theory we want to see in mathlib. But for maintenance it is important to see where a proof breaks. The more explicit structure you add to tactic scripts the better. So for induction, cases, etc. we want to see explicitly which tactics are responsible for which subgoal: use { ... } to mark them.

spl · 2018-02-14T10:45:44Z

@johoelzl:

The more explicit structure you add to tactic scripts the better. So for induction, cases, etc. we want to see explicitly which tactics are responsible for which subgoal: use { ... } to mark them.

I'm just curious about your style guidelines. Would case <constructor> { ... } be better than { ... }? The explicit tags help document the tactics.

johoelzl · 2018-02-14T10:48:40Z

Hard to say. For longer proofs were it is hard to see what you are refering to case <constructor> { ... } is preferred. For short proofs { ... } is just less cluttered and hence more readable. But then if your { ... } starts with a intro you might as well use case <constructor> : h ... { .. }

digama0 · 2018-02-14T10:48:46Z

My view is that case is most useful when you have >2 constructors and the inductive type is "unfamiliar". If you are doing cases on an expression in the C grammar, absolutely. If it's just or.inl and or.inr, I wouldn't bother.

Especially since or.inl doesn't actually tell the reader much about what the goal is, while case expr.lam does.

spl · 2018-02-14T10:57:06Z

Thanks for the responses! It seems that there is a spectrum of opinions. I must say that I lean strongly toward the “use case <constructor> often” end of the spectrum. It helps me when revisiting proofs after a long time. I do see @digama0's point about or.inl/or.inr, but I've found that even using case list.nil/case list.cons makes it more clear which part is being proved.

Hopefully stylistically better now

johoelzl · 2018-02-14T14:16:40Z

data/nat/choose.lean

+lemma succ_mul_choose_eq (n : ℕ) : ∀ k, succ n * choose n k = choose (succ n) (succ k) * succ k := 
+begin
+  induction n with n' hi,
+  { assume k, simp,


Using simp in the middle should be avoided. When the set of simp-rules changes (and it changes fast) then the goals afterwards change also. This results in unpredictable goals. Try to do a more structured approach:

introduce a have with some subgoal?

add maybe simp rules to solve the goal in one step

move the simp further down, in this case distribute it into both cases

johoelzl · 2018-02-14T14:18:45Z

data/nat/choose.lean

+  induction n with n' hi,
+  { assume k, simp,
+    cases k with k', 
+      simp,


Put simp into { simp }. This is especially important for simp. Otherwise it might happen that the simp set changes and the next tactics still work. Then it is hard to figure out which simp call failed.

johoelzl · 2018-02-14T14:24:12Z

data/nat/choose.lean

+begin
+  induction n with n' hi,
+  { assume k hk,
+    rw [eq_zero_of_le_zero hk,choose_zero_right],


can you replace this branch by a simp call a la: simp [nat.le_zero_iff] {contextual := tt} (maybe with dec_trivial afterwards)

I don't actually know what {contextual := tt} means, so possibly, but I don't really know how.

Play around! With this the simplifier gets very powerful :-)
What does it do: when the simplifier rewrites a term of the form a -> b, it first rewrites a = a', and then when it rewrites b it adds a' to its new context. So if a' is a rewrite rule it can use it for rewriting, if a' is a proposition it will at least use this proposition to fullfill any conditions on rewrite rules.

Your goal has the form ∀n, 0 ≥ n → choose n k = ..., now with nat.le_zero_iff the simplifier will rewrite (0 ≥ n) = (n = 0). This is again a nice rewrite rule, so choose n k = ... is rewritten to choose 0 k = ... and choose_zero_right matches!

johoelzl · 2018-02-14T14:31:07Z

Hey Chris,

some further notes. The changed indentation helped me to see further problems in the tactic scripts.

Also I have more stylisic change requests:

If you write a list of rules (for example: rw [a, b, c]) there is always a space after the comma
similar with ;: e.g. by cases n; simp
no comma before end: begin t1, t2, t3 end
put a space before the closing bracket when you have a space after the opening one:
{ a, b, c }
or
```
{ t1,
  t2,
  t3 }
```

I know all these stylistic changes seam to be annoying and bike shedding, but they drastically increase readability.

slightly simplify proof

Shorten proofs

johoelzl

Further proof cleanup suggestions: choose is a nice recursively defined function. So lets use the equation compiler to simplify our proofs.

Warning: the induction hypothesis has the name of the lemma you proof. It looks very general, but the equation compiler foes not support more than primitive induction. So avoid giving it directly to the simplifier (no simp [*]), but only instantiated

johoelzl · 2018-02-15T10:38:36Z

data/nat/choose.lean

+def choose : ℕ → ℕ → ℕ
+| _              0  := 1
+| 0        (succ k) := 0
+| (succ n) (succ k) := choose n k + choose n (succ k)


The equation compiler and the elaborator understand that succ n = n + 1, so it's nicer to use n + 1 instead of succ.

johoelzl · 2018-02-15T10:40:15Z

data/nat/choose.lean

+| 0        (succ k) := 0
+| (succ n) (succ k) := choose n k + choose n (succ k)
+
+@[simp]


@[simp] is on the same line as the lemma. Change this here and in the following lemmas.
Move the proof to the next line, especially when the line gets longer than 100 characters.

johoelzl · 2018-02-15T10:43:12Z

data/nat/choose.lean

+lemma choose_succ_succ (n k : ℕ) : choose (succ n) (succ k) = choose n k + choose n (succ k) := rfl
+
+lemma choose_eq_zero_of_lt {n : ℕ} : ∀ {k}, n < k → choose n k = 0 :=
+begin


This can be written very nice using the equation compiler:

lemma choose_eq_zero_of_lt : ∀ {n k}, n < k → choose n k = 0 | 0 (k+1) hk := by simp | (n+1) (k+1) hk := have hnk : n < k, from lt_of_succ_lt_succ hk, have hnk1 : n < k + 1, from lt_of_succ_lt hk, by rw [choose_succ_succ, choose_eq_zero_of_lt hnk, choose_eq_zero_of_lt hnk1]

The equation compiler takes care of the absurd cases (n < m is n + 1 ≤ m which is inductively defined). My personal preference is to state proofs explicitly using have .. instead of adding the proof to to the rw list.

johoelzl · 2018-02-15T10:44:36Z

data/nat/choose.lean

+by induction n; simp [*, choose]
+
+lemma choose_pos {n : ℕ} : ∀ {k}, k ≤ n → 0 < choose n k :=
+begin


this may also be a good application for the equation compiler. I guess 3 cases (0 n, (n+1) 0, (n+1) (k+1)) are needed, but they could go through using simp.

johoelzl · 2018-02-15T10:45:00Z

data/nat/choose.lean

+end
+
+lemma succ_mul_choose_eq (n : ℕ) : ∀ k, succ n * choose n k = choose (succ n) (succ k) * succ k := 
+begin


try again the equation compiler

johoelzl · 2018-02-15T10:45:06Z

data/nat/choose.lean

+end
+
+lemma choose_mul_fact_mul_fact {n : ℕ} : ∀ {k}, k ≤ n → choose n k * fact k * fact (n - k) = fact n :=
+begin


Used the equation compiler for inductive proofs

johoelzl · 2018-02-19T10:02:47Z

data/nat/choose.lean

+    { rw [hk₁, choose_succ_self, zero_mul, zero_mul, add_zero, fact_succ, mul_comm] } 
+end
+
+theorem choose_def_alt {n k : ℕ} (hk : k ≤ n) : choose n k = fact n / (fact k * fact (n - k)) :=


what about calling it: choose_eq_fact_div_fact

State in the have what you get after the rw [..] at this. And then prove it using the rw and the choose_mul_fact_mul. Then you can even replace the begin .. end part by have _, begin ... end, _

johoelzl · 2018-02-19T10:03:06Z

data/nat/choose.lean

+  rw [choose_succ_succ, succ_sub_succ, add_mul, add_mul],
+  have : choose n k * fact (succ k) * fact (n - k) = choose n k * fact k * fact (n - k) * succ k :=
+    by unfold fact; simp[mul_comm, mul_assoc, mul_left_comm],
+    rw [this, choose_mul_fact_mul_fact (le_of_succ_le_succ hk)],


indentation is wrong after this line; remove two spaces from the following tactics

johoelzl · 2018-02-19T10:06:26Z

data/nat/choose.lean

+    rw [this, choose_mul_fact_mul_fact (le_of_succ_le_succ hk)],
+    cases lt_or_eq_of_le hk with hk₁ hk₁,
+    { have : n - k = succ (n - succ k) := by rw [←succ_sub (le_of_succ_le_succ hk₁), succ_sub_succ],
+      rw [this, fact_succ (n - succ k), mul_comm (succ (n - succ k)), ←mul_assoc], 


could you sqash the follow rw into one?

johoelzl · 2018-02-19T10:08:50Z

data/nat/choose.lean

+| (n + 1)        0 hk := by simp
+| (n + 1) (succ k) hk := 
+begin 
+  rw [choose_succ_succ, succ_sub_succ, add_mul, add_mul],


Why do you first rw, then show something, then continue rw, then a case and then more rw?
Move the have to the front. Then make the case distinction. And then do the rw at once. But take a look at the goal of you rw, maybe you can do it in one simp call?

Slightly neater proof of `choose_mul_fact_mul_fact`. The proof involves subtraction of naturals, so cannot easily be done using simp.

deat(data/nat): add choose function to compute the binomial coefficients

Create choose.lean

b672169

Definition of choose function for naturals and basic lemmas

johoelzl reviewed Feb 14, 2018

View reviewed changes

Update choose.lean

ba9ad8c

Hopefully stylistically better now

johoelzl reviewed Feb 14, 2018

View reviewed changes

ChrisHughes24 added 3 commits February 14, 2018 14:42

Update choose.lean

b75cd8a

Update choose.lean

79ca3d3

slightly simplify proof

Update choose.lean

8f6099c

Shorten proofs

johoelzl requested changes Feb 15, 2018

View reviewed changes

ChrisHughes24 added 2 commits February 15, 2018 12:00

Update choose.lean

56fceee

Used the equation compiler for inductive proofs

Update choose.lean

6f7f1e7

johoelzl requested changes Feb 19, 2018

View reviewed changes

Update choose.lean

7300b45

Slightly neater proof of `choose_mul_fact_mul_fact`. The proof involves subtraction of naturals, so cannot easily be done using simp.

johoelzl merged commit 504a2dc into leanprover-community:master Feb 20, 2018

johoelzl pushed a commit to johoelzl/mathlib that referenced this pull request Mar 5, 2018

Create choose.lean (leanprover-community#48)

24c0825

deat(data/nat): add choose function to compute the binomial coefficients

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Create choose.lean #48

Create choose.lean #48

ChrisHughes24 commented Feb 11, 2018

johoelzl Feb 14, 2018

johoelzl Feb 14, 2018

johoelzl Feb 14, 2018

johoelzl Feb 14, 2018

johoelzl Feb 14, 2018

johoelzl Feb 14, 2018

johoelzl commented Feb 14, 2018

spl commented Feb 14, 2018

johoelzl commented Feb 14, 2018

digama0 commented Feb 14, 2018 •

edited

spl commented Feb 14, 2018

johoelzl Feb 14, 2018

johoelzl Feb 14, 2018

johoelzl Feb 14, 2018

ChrisHughes24 Feb 14, 2018

johoelzl Feb 14, 2018

johoelzl commented Feb 14, 2018

johoelzl left a comment

johoelzl Feb 15, 2018

johoelzl Feb 15, 2018

johoelzl Feb 15, 2018

johoelzl Feb 15, 2018

johoelzl Feb 15, 2018

johoelzl Feb 15, 2018

johoelzl Feb 19, 2018

johoelzl Feb 19, 2018

johoelzl Feb 19, 2018

johoelzl Feb 19, 2018

johoelzl Feb 19, 2018

Create choose.lean #48

Create choose.lean #48

Conversation

ChrisHughes24 commented Feb 11, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

johoelzl commented Feb 14, 2018

spl commented Feb 14, 2018

johoelzl commented Feb 14, 2018

digama0 commented Feb 14, 2018 • edited

spl commented Feb 14, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

johoelzl commented Feb 14, 2018

johoelzl left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

digama0 commented Feb 14, 2018 •

edited