induction' question

Stream: general

[Patrick Massot]

Some of my students tried to use inductive types (Props actually) in topology (I many real inductive types: several constructor, no natural number). I tried to fix their code a bit. Then I found induction was disappointing. I was very happy because I thought it was a perfect opportunity to try @Jannis Limperg induction'. It indeed allowed me to make progress. However I also encountered issues with induction'. This is most probably because I know nothing about real inductive types. I'd be very happy to read comments about the following code to learn more or contribute to bug hunting. Uses of induction or induction' are flagged.

import tactic
import tactic.induction

open set

open_locale classical

@[ext]
class topological_space (X : Type) :=
  (is_open  : set X → Prop)
  (univ_mem : is_open univ)
  (union    : ∀ (B : set (set X)) (h : ∀ b ∈ B, is_open b), is_open (⋃₀ B))
  (inter    : ∀ (A B : set X) (hA : is_open A) (hB : is_open B), is_open (A ∩ B))

namespace topological_space

inductive generated_open (X : Type) (g : set (set X)) : set X → Prop
| generator : ∀ A ∈ g, generated_open A
| inter     : ∀ A B, generated_open A → generated_open B → generated_open (A ∩ B)
| union     : ∀ (B : set (set X)), (∀ b ∈ B, generated_open b) → generated_open (⋃₀ B)
| univ      : generated_open univ

def generate_from (X : Type) (g : set (set X)) : topological_space X :=
{ is_open   := generated_open X g,
  univ_mem  := generated_open.univ,
  inter     := generated_open.inter,
  union     := generated_open.union }

end topological_space

open topological_space

def neighbourhood {X : Type} [topological_space X] (x : X) (V : set X) : Prop :=
∃ (U : set X), is_open U ∧ x ∈ U ∧ U ⊆ V

def seq_lim {X : Type} [topological_space X] (u : ℕ → X) (l : X) : Prop :=
∀ (V : set X), neighbourhood l V → ∃ (N : ℕ), ∀ n ≥ N, u n ∈ V

lemma nhd_inter {X : Type*} [topological_space X] {x : X} {U V : set X}
  (hU : neighbourhood x U) (hV : neighbourhood x V) : neighbourhood x (U ∩ V) :=
begin
  rcases hU with ⟨S, hS, hxS, hUS⟩,
  rcases hV with ⟨T, hT, hxT, hVT⟩,
  exact ⟨S ∩ T, inter S T hS hT, ⟨hxS, hxT⟩, inter_subset_inter hUS hVT⟩
end

lemma nhd_superset {X : Type*} [topological_space X] {x : X} {U V : set X}
  (hU : neighbourhood x U) (hUV : U ⊆ V) : neighbourhood x V :=
begin
  rcases hU with ⟨S, hS, hxS, hUS⟩,
  exact ⟨S, hS, hxS, subset.trans hUS hUV⟩
end

lemma nhd_univ {X : Type*} [topological_space X] {x : X} : neighbourhood x univ :=
⟨univ, univ_mem, trivial, subset.refl _⟩

def pointwise_lim {X Y : Type} [topological_space Y] (f : ℕ → (X → Y)) (F : X → Y) : Prop :=
∀ (x : X), seq_lim (λ n, f n x) (F x)

inductive generated_filter {X : Type*} (g : set (set X)) : set X → Prop
| generator {A} : A ∈ g → generated_filter A
| inter   {A B} : generated_filter A → generated_filter B → generated_filter (A ∩ B)
| subset  {A B} : generated_filter A → A ⊆ B → generated_filter B
| univ          : generated_filter univ

lemma nhds_gen_iff {X : Type*} [T : topological_space X] {s : set (set X)} (h : T = generate_from X s) {U : set X} {x : X} :
  neighbourhood x U ↔ generated_filter {V | V ∈ s ∧ x ∈ V} U :=
begin
  rw h, letI := generate_from X s,
  split,
  { rintros ⟨V, V_op, x_in, hUV⟩,
    apply generated_filter.subset _ hUV,
    clear hUV,
    induction V_op, -- **FAIL** induction' simply refuses to work here
    { apply generated_filter.generator,
      split ; assumption },
    { cases x_in,
      apply generated_filter.inter ; tauto },
    { dsimp at V_op_ih,
      rw mem_sUnion at x_in,
      rcases x_in with ⟨W, hW, hxW⟩,
      exact generated_filter.subset (V_op_ih W hW hxW) (subset_sUnion_of_mem hW)},
    { apply generated_filter.univ },},
  { intro U_in,
    -- **FAIL** induction' generates crazy goals
    induction U_in with U hU U V U_gen V_gen hU hV U V U_gen hUV hU,
    { exact ⟨U, generated_open.generator U hU.1, hU.2, subset.refl U⟩ },
    { exact nhd_inter hU hV },
    { exact nhd_superset hU hUV },
    { apply nhd_univ } },
end

lemma lim_gen {X : Type*} [T : topological_space X] {s : set (set X)} (h : T = generate_from X s) {u : ℕ → X} {x : X} :
seq_lim u x ↔ ∀ U ∈ s, x ∈ U → ∃ N, ∀ n ≥ N, u n ∈ U :=
begin
  simp_rw [seq_lim, nhds_gen_iff h],
  split,
  { intros H U U_in x_in,
    apply H,
    apply generated_filter.generator,
    split ; assumption, },
  { intros H V hV,
    -- **WARN** works but generates useless assumptions U_gen, V_gen, U_gen
    induction' hV fixing h u with V hV U V U_gen V_gen ihU ihV U V U_gen hUV hU,
    { cases hV,
      apply H ; assumption },
    { rcases ihU H with ⟨N₁, hN₁⟩,
      rcases ihV H with ⟨N₂, hN₂⟩,
      use max N₁ N₂,
      rintros n (hn : max N₁ N₂ ≤ n),
      rw max_le_iff at hn,
      exact ⟨hN₁ n hn.1, hN₂ n hn.2⟩ },
    { rcases hU H with ⟨N, hN⟩,
      use N,
      intros n hn,
      exact hUV (hN n hn) },
    { exact ⟨0, λ n hn, trivial⟩ }, },
end

[Eric Wieser]

What do you mean by "generates useless assumptions U_gen, V_gen, U_gen"? Are they useless in that they are constructible from the other hypotheses? Or just in that you didn't end up needing them to prove the goal?

[Patrick Massot]

I think they would be useless whatever the goal, but I haven't thought too hard about this.

[Eric Wieser]

I think you're using domain-specific knowledge to conclude that. I guess it would be nice if - were allowed like it is in rcases, as in induction' hV fixing h u with V hV U V - - ihU ihV U V - hUV hU

[Patrick Massot]

Yes, this would be a nice feature that is hopefully easy to implement.

[Jannis Limperg]

Thanks for the bug report! The useless U_gen and V_gen are supposed to be there. They correspond to arguments of the generated_filter.inter constructor. However, I can implement the - feature for the with clause so that they can be cleared. The two FAILs indeed look like bugs; I'm investigating.

[Jannis Limperg]

PRs for the bugs (#7717) and the with - (#7726) are now in-flight. The bugs came down to interactions with Lean features (frozen instances, local defs and infinitely-branching types) which were never used in Jasmin's course and which severely messed up some of my internal assumptions. So thanks again for the bug report!

While investigating these use cases, I had some second thoughts about the auto-generalisation feature. By default, induction' reverts any hypothesis that can be reverted to get the most general induction hypothesis. But in the use cases here, that's not super helpful since there are a lot of random things in the context (instances, equations, hypotheses that don't need generalising), so the induction hypothesis ends up having a lot of mostly useless quantifiers. I might have to turns this feature off for general mathlib use. (It was intended for Jasmin's teaching setting, where it works very well.)

[Patrick Massot]

Thanks!