## Stream: maths

### Topic: induction generalizing

#### Kevin Buzzard (Jan 28 2020 at 17:35):

induction isn't documented in the tactics doc as far as I can see, and I think I need to use it in a slightly fancy way (is it generalizing I want here?). I have some slightly messy goal involving quantifying over all finite subsets of a type K. I want to prove the goal by induction on the size of the subset. In particular the inductive hypotheses in data.set.finite are not right for me -- they involve hypotheses of the form "if it's true for S then it's true for S union {x}" but what I can prove is that it's true for the empty subset, and if n>=1 is the size of non-empty S, and if it's true for all subsets of S of size n-1, then it's true for S.

I can probably do this by explicitly copying my messy goal (which will mention typeclasses) and putting a "forall n" in front of it and an assumption which says n is the size of S, proving that this suffices, and then doing induction on n -- but is there some cheap way to do this just using the induction tactic?

#### Kevin Buzzard (Jan 28 2020 at 18:27):

dammit

theorem Zariskis_lemma
-- let k be a field
(k : Type u) [discrete_field k]
-- and let k ⊆ K be another field
(K : Type v) [discrete_field K] [algebra k K]
-- Assume that there's a finite subset S of K
(S : set K) (hfs : S.finite)
-- which generates K as a k-algebra
-- (note: ⊤ is "the largest k-subalgebra of K", i.e., K)
(hsgen : algebra.adjoin k S = ⊤)
-- Then
:
-- K is finitely-generated as a k-vector space
(⊤ : submodule k K).fg
:=
begin
unfreezeI, -- to get next line to work; I need to quantify over k
revert k,
set n := @fintype.card S (set.finite.fintype hfs) with hn,
induction n with d hd,
/-
induction tactic failed, failed to create new goal
-/


this is more annoying than I realised. This works:

begin
unfreezeI, -- to get next line to work; I need to quantify over k
revert k,
suffices : ∀ (n : ℕ) (k : Type u) [discrete_field k]
(K : Type v) [discrete_field K] [algebra k K]
(S : set K) (hfs : S.finite) (hn : n = @fintype.card S (set.finite.fintype hfs))
(hsgen : algebra.adjoin k S = ⊤),  (⊤ : submodule k K).fg,
intros,
exact this _ _ _ S hfs rfl hsgen,
sorry,
end


but I feel like I'm missing a trick (the rfl is hn).




#### Floris van Doorn (Jan 28 2020 at 18:39):

The problem is that n is a let-expression.

#### Floris van Doorn (Jan 28 2020 at 18:40):

This works, but is still ugly:

import ring_theory.all

universe variables u v

theorem Zariskis_lemma
-- let k be a field
(k : Type u) [discrete_field k]
-- and let k ⊆ K be another field
(K : Type v) [discrete_field K] [algebra k K]
-- Assume that there's a finite subset S of K
(S : set K) (hfs : S.finite)
-- which generates K as a k-algebra
-- (note: ⊤ is "the largest k-subalgebra of K", i.e., K)
(hsgen : algebra.adjoin k S = ⊤)
-- Then
:
-- K is finitely-generated as a k-vector space
(⊤ : submodule k K).fg
:=
begin
unfreezeI, -- to get next line to work; I need to quantify over k
revert k,
obtain ⟨n, hn⟩ : {n : ℕ // @fintype.card S (set.finite.fintype hfs) = n} := ⟨_, rfl⟩,
induction n with d hd,
end


#### Floris van Doorn (Jan 28 2020 at 18:41):

• Is there a tactic that forgets the body of a local hypothesis (in Coq this is clearbody n)?
• Is there a tactic that does the same as set x := t with hx, but makes x a normal variable, instead of a let-expression?

#### Kevin Buzzard (Jan 28 2020 at 18:42):

Yes, I used set instead of let to try and somehow get around this but clearly it didn't work (because set uses let). Your method is better than mine because you didn't have to rewrite the goal. Thanks!

#### Kevin Buzzard (Jan 28 2020 at 18:42):

nice use of obtain there ;-)

#### Floris van Doorn (Jan 28 2020 at 18:42):

I updated it to use obtain instead of have.

#### Floris van Doorn (Jan 28 2020 at 18:43):

Oh, you saw it :)

#### Kevin Buzzard (Jan 28 2020 at 18:43):

I was trying to understand it when it changed in front of me :-)

#### Floris van Doorn (Jan 28 2020 at 18:44):

Another shortening, now there is just O(1) extra stuff you have to type compared to a dedicated tactic for this purpose.

#### Kevin Buzzard (Jan 28 2020 at 18:44):

So am I wrong in thinking that there is some option to induction which does this for me automatically?

#### Floris van Doorn (Jan 28 2020 at 18:45):

I don't think such option currently exist. But we could let induction call clearbody on its argument if the clearbody tactic exists.

#### Floris van Doorn (Jan 28 2020 at 18:45):

which turns a let-expression into a normal variable.

#### Kevin Buzzard (Jan 28 2020 at 18:45):

This is actually a tricky commutative algebra lemma, but I had no idea that this part was the tricky part :-/

:)

#### Mario Carneiro (Jan 28 2020 at 20:50):

@Floris van Doorn what do you mean by "forgets the body of a local hypothesis"? Do you want to replace a let bound x : A := t in the context with x : A?

#### Kevin Buzzard (Jan 28 2020 at 21:16):

I think that this was precisely what stopped my induction tactic from working

#### Floris van Doorn (Jan 28 2020 at 21:37):

@Mario Carneiro Exactly.

#### Kevin Buzzard (Jan 28 2020 at 22:00):

No doubt this is called upsilon reduction or something

Last updated: May 10 2021 at 08:14 UTC