# 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
@[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 (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):

Thanks!

Last updated: Dec 20 2023 at 11:08 UTC