Zulip Chat Archive

Stream: general

Topic: induction' question

Patrick Massot (May 16 2021 at 20:31):

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

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) :=
  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

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

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 :=
  rw h, letI := generate_from X s,
  { 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 } },

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 :=
  simp_rw [seq_lim, nhds_gen_iff h],
  { 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 }, },

Eric Wieser (May 16 2021 at 21:14):

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 (May 16 2021 at 21:16):

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

Eric Wieser (May 16 2021 at 21:23):

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 (May 16 2021 at 21:37):

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

Jannis Limperg (May 17 2021 at 14:50):

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 (May 27 2021 at 12:07):

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 (May 27 2021 at 12:32):


Last updated: Aug 03 2023 at 10:10 UTC