Coercion nightmares

Stream: new members

[Antoine Chambert-Loir]

A subgroup of a subgroup is a subgroup, but this proof looks ridiculous. Am I that much ignorant ?

import tactic

import group_theory.subgroup.basic

variable (α : Type*)

example : ∀ (s : set α) (t : set ↥s), ∃ (u : set α),
  ∀ (a : α), a ∈ u ↔ ∃ (hs : a ∈ s), (⟨a, hs⟩ : ↥s) ∈ t :=
begin
  intros s t,
  let j : ↥s → α := λ x, ↑x,
  use j '' t,
  intro a,
  split,
  { intro ha,
    simp only [set.mem_image, set_coe.exists] at ha,
    obtain ⟨b, hb, hb', hb''⟩ := ha,
    suffices : a = b,
    { rw this, use hb, exact hb' },
    rw ← hb'',
    refl },
  { rintro ⟨hs', hs''⟩,
    simp only [set.mem_image, set_coe.exists],
    use a, use hs', apply and.intro hs'',
    refl }
end

variable [hα : group α]

example : ∀ (G : @subgroup α hα) (H : subgroup G),
  ∃ (H' : subgroup α), ∀ (a : α), a ∈ H' ↔
  ∃ (ha : a ∈ G), (⟨a, ha⟩ : ↥G) ∈ H :=
begin
  intros G H,
  have j : G →* α := subgroup.subtype G,
  use H.map (G.subtype),
  intro a,
  split,
  { intro ha,
    simp only [subgroup.mem_map, exists_prop] at ha,
    obtain ⟨b, hb, hb'⟩ := ha,
    suffices : a = b,
    { have this': a ∈ G,
      { rw this, exact set_like.coe_mem b, },
      use this',
      have this' : b = ⟨a, this'⟩,
      { exact subtype.eq (eq.symm this), },
      rw this' at hb, exact hb },
    rw ← hb',
    refine congr _ rfl,
    refine subgroup.coe_subtype G },
  { rintro ⟨ha, ha'⟩,
    simp only [subgroup.mem_map, subgroup.coe_subtype, exists_prop],
    use (⟨a, ha⟩),
    apply and.intro ha',
    exact subtype.coe_mk a ha },
end

[Kevin Buzzard]

The trick is to use map and comap to push sets forwards and backwards along the map from \u s to alpha

[Johan Commelin]

And sometimes it turns out to be better to work with injective group homs.

[Riccardo Brasca]

The map is docs#subgroup.subtype

[Antoine Chambert-Loir]

The whole role of this is to be able teach Lean that fixing_subgroup (fixing_subgroup M s) t = fixing_subgroup M (s \cup t), but Lean resists…

[Kevin Buzzard]

example (s : set α) (t : set ↥s) : ∃ (u : set α),
  ∀ (a : α), a ∈ u ↔ ∃ (hs : a ∈ s), (⟨a, hs⟩ : ↥s) ∈ t :=
begin
  -- move s, t before the colon to save `intro`
  use (coe : s → α) '' t, -- the map is already there and this is the simp normal form
  finish, -- this is now just logic nonsense, unpacking and repacking
end

some tips @Antoine Chambert-Loir

[Antoine Chambert-Loir]

I learn about finish!

[Antoine Chambert-Loir]

By the way, do you understand why I needed to specify @subgroup hM M (where hM : group M) in the second proof above ? — subgroup M didn't suffice to find an instance of group M.

[Riccardo Brasca]

This is weird

[Riccardo Brasca]

ah, wait, this is because you named the instance

[Riccardo Brasca]

variable [group α]

example : ∀ (G : subgroup α) (H : subgroup G),
  ∃ (H' : subgroup α), ∀ (a : α), a ∈ H' ↔
  ∃ (ha : a ∈ G), (⟨a, ha⟩ : ↥G) ∈ H :=

should be OK

[Riccardo Brasca]

If you give a name to a variable between square brackets, then Lean will not include it unless you mention it. So with variable [hα : group α] it doesn't know that α is a group

[Antoine Chambert-Loir]

In any case, now I can at least state what I wish to prove :

lemma certainly_easy_to_prove_nightmare_to_state {s t : set α} : fixing_subgroup M (s ∪ t) =
  (fixing_subgroup (fixing_subgroup M s) t).map (fixing_subgroup M s).subtype :=
sorry

[Riccardo Brasca]

If you need to give it a name and use it several time you can write include hα.

[Riccardo Brasca]

It seems we are missing a reasonable API for fixing_subgroup. For example the first sorry here

variables {M : Type*} [group M] [mul_action M α]

lemma certainly_easy_to_prove_nightmare_to_state {s t : set α} : fixing_subgroup M (s ∪ t) =
  (fixing_subgroup (fixing_subgroup M s) t).map (fixing_subgroup M s).subtype :=
begin
  ext x,
  split,
  { intros hx,
    refine ⟨⟨x, _⟩, ⟨_, _⟩⟩,
    { sorry },
    { sorry },
    { sorry } },
  { rintros hx ⟨y, hy₁ | hy₂⟩,
    { sorry },
    { sorry } }
end

should follow from some monotonicity of fixing_subgroup, that I don't find.

[Kevin Buzzard]

@Antoine Chambert-Loir

import tactic

import group_theory.subgroup.basic

variable (α : Type*)

example (s : set α) (t : set ↥s) : ∃ (u : set α),
  ∀ (a : α), a ∈ u ↔ ∃ (hs : a ∈ s), (⟨a, hs⟩ : ↥s) ∈ t :=
begin
  use (coe : s → α) '' t,
  intro a,
  split,
  { -- We begin by abusing definitional equality and use the `rfl` trick.
    rintro ⟨⟨b, hbs⟩, hbt, rfl⟩, -- The `rfl` trick *defines* `a` to be `b`, substitutes in and then just rerases `a`.
    exact ⟨hbs, hbt⟩ }, -- Can now just make the term
  { rintro ⟨has, hat⟩,
    -- the proof should now be one line, of the form `exact ⟨⟨t₁, t₂⟩, ⟨t₃, t₄, t₅⟩⟩`.
    -- Let's *experiment* now in tactic mode, and then use the `refine` tactic to make the
    -- term we need.
    -- `use a`, Oh this made progress. I now randomly have two goals but they
    -- both look pretty simple. I'll take that.
    -- But actually `use` just ran the `refine` tactic on something else.
    -- Let's see what `use a` actually did:
    refine ⟨⟨a, _⟩, _⟩,  -- The two underscores are the new goals.
    { -- two goals so make a new bracket
      -- `use has` closes this goal! Now let's think about how to write it using `refine`
      exact has, }, -- the first `_` was just the term `has`.
    { -- second goal
      -- `apply and.intro hat,` looks like a good first move. But `apply` just used `refine`:
      refine and.intro hat _,
      refl -- now solves the goal!
       -- but if the proof was refl we can just use `rfl` on the previous line
    }
  }
  -- Therefore, the one line proof is `exact ⟨⟨a, has⟩, and.intro hat rfl⟩`,
end

[Antoine Chambert-Loir]

@Riccardo Brasca , Yes, docs#fixing_subgroup `is defined « par la bande » in the files devoted to Galois theory. I believe one needs to transfer them somewhere in the files related to docs#mul_action, as well as adding much stuff. For example, I found useful to have

lemma mem_fixing_subgroup_iff (s : set α) (g : M) :
  g ∈ fixing_subgroup M s ↔ ∀ (y : α) (hy : y ∈ s), g • y = y := ⟨λ hg y hy, hg ⟨y, hy⟩, λ h ⟨y, hy⟩, h y hy⟩

[Riccardo Brasca]

I totally agree that lemma should be immediately after the definition, that should be elsewhere

[Riccardo Brasca]

There is docs#mul_action.stabilizer

[Riccardo Brasca]

With an API, but it is for a singleton (I didn't check the whole file).

[Kevin Buzzard]

example (s : set α) (t : set ↥s) : ∃ (u : set α),
  ∀ (a : α), a ∈ u ↔ ∃ (hs : a ∈ s), (⟨a, hs⟩ : ↥s) ∈ t :=
⟨(coe : s → α) '' t,λ a, ⟨by {rintro ⟨⟨b, hbs⟩, hbt, rfl⟩,exact ⟨hbs, hbt⟩},
  -- no rfl trick here so can do it all in term mode
  λ ha, ⟨⟨a, ha.some⟩, ⟨ha.some_spec, rfl⟩⟩⟩⟩

[Kevin Buzzard]

The rfl trick in rintro involves a "deep eq.rec" so you don't want to translate it into term mode, my guess is that the term generated by the rintro rfl tactic is really nasty.

[Kevin Buzzard]

Oh by the way I used the axiom of choice with exists.some and exists.some_spec

[Reid Barton]

quite unnecessarily though: λ ⟨ha₁, ha₂⟩, ⟨⟨a, ha₁⟩, ⟨ha₂, rfl⟩⟩

[Kevin Buzzard]

I thought that term mode lambda pointies were discouraged!

[Reid Barton]

Only for defining data

[Reid Barton]

It will produce a term with a whatever.rec in a place that usually isn't the best place for it

[Reid Barton]

but for a proof we don't care