Zulip Chat Archive

Stream: maths

Topic: induction generalizing


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

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


view this post on Zulip Floris van Doorn (Jan 28 2020 at 18:39):

The problem is that n is a let-expression.

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

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

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

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

view this post on Zulip Kevin Buzzard (Jan 28 2020 at 18:42):

nice use of obtain there ;-)

view this post on Zulip Floris van Doorn (Jan 28 2020 at 18:42):

I updated it to use obtain instead of have.

view this post on Zulip Floris van Doorn (Jan 28 2020 at 18:43):

Oh, you saw it :)

view this post on Zulip Kevin Buzzard (Jan 28 2020 at 18:43):

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

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

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

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

view this post on Zulip Floris van Doorn (Jan 28 2020 at 18:45):

which turns a let-expression into a normal variable.

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

view this post on Zulip Floris van Doorn (Jan 28 2020 at 18:46):

:)

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

view this post on Zulip Kevin Buzzard (Jan 28 2020 at 21:16):

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

view this post on Zulip Floris van Doorn (Jan 28 2020 at 21:37):

@Mario Carneiro Exactly.

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