induction generalizing

Stream: maths

[Kevin Buzzard]

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]

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]

The problem is that n is a let-expression.

[Floris van Doorn]

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]

• 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?

We should add both these tactics if they don't already exist.

[Kevin Buzzard]

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]

nice use of obtain there ;-)

[Floris van Doorn]

I updated it to use obtain instead of have.

[Floris van Doorn]

Oh, you saw it :)

[Kevin Buzzard]

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

[Floris van Doorn]

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

[Kevin Buzzard]

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

[Floris van Doorn]

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]

which turns a let-expression into a normal variable.

[Kevin Buzzard]

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

[Floris van Doorn]

:)

[Mario Carneiro]

@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]

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

[Floris van Doorn]

@Mario Carneiro Exactly.

[Kevin Buzzard]

No doubt this is called upsilon reduction or something