## Stream: new members

### Topic: Problems with induction and type inference

#### Patrick Lutz (Jul 30 2020 at 20:35):

I'm trying to prove something by strong induction on the natural numbers and I'm having trouble with type inference. The actual example is pretty complicated, so here's the best mwe I can come up with. Here's what I'd like to prove

import tactic

constant dimension (α : Type) [inhabited α] : ℕ
constant shrink (α : Type) [inhabited α] : Type
constant good : Type → Prop

variables (α : Type) [inhabited α]

constant shrink_inhabited_of_inhabited : shrink α
noncomputable instance shrink_inhabited : inhabited (shrink α) :=
inhabited.mk (shrink_inhabited_of_inhabited α)
axiom good_of_dimension_zero : dimension α = 0 → good α
axiom shrink_decreasing : dimension α > 0 → dimension (shrink α) < dimension α
axiom good_of_shrink_good : good (shrink α) → good α

lemma good_of_inhabited : ∀ n : ℕ, dimension  α = n → good α := sorry


The lemma as stated however, is not quite in the right form to do induction. You want to apply the inductive assumption to shrink α but the inductive assumption doesn't allow this. The obvious solution (and I haven't quite gotten to my actual question yet) is to quantify over α as well. Like so

lemma good_of_inhabited : ∀ n : ℕ, ∀ α [hα : inhabited α], @dimension α hα = n → good α := sorry


Already, I start having some problems with type inference. I'd like to just be able to type dimension α = n but I can't because Lean can't figure out that α is inhabited the same way it could before. When I try to prove the lemma, this keeps coming up. E.g. I can prove it like so

lemma good_of_inhabited : ∀ n : ℕ, ∀ α [hα : inhabited α], @dimension α hα = n → good α
| 0 := λ α hα h, @good_of_dimension_zero α hα h
| (n + 1) :=
begin
intros α hα hn,
let β := @shrink α hα,
let m := dimension β,
let decreasing : m < n + 1 := by rw ← hn; apply shrink_decreasing; linarith,
have : good β := good_of_inhabited m β rfl,
exact @good_of_shrink_good α hα this,
end


But it's annoying to have to tell Lean how to infer types explicitly so much. And in the actual example where I want to do something like this (not this simplified mwe) it's even worse and I'm genuinely having some trouble getting Lean to do all the type inference that I want. Is there a better way to do this?

#### Jalex Stark (Jul 30 2020 at 23:24):

import tactic

constant dimension (α : Type) [inhabited α] : ℕ
constant shrink (α : Type) [inhabited α] : Type
constant good : Type → Prop

variables (α : Type) [inhabited α]

constant shrink_inhabited_of_inhabited : shrink α
noncomputable instance shrink_inhabited : inhabited (shrink α) :=
inhabited.mk (shrink_inhabited_of_inhabited α)
axiom good_of_dimension_zero : dimension α = 0 → good α
axiom shrink_decreasing : dimension α > 0 → dimension (shrink α) < dimension α
axiom good_of_shrink_good : good (shrink α) → good α

lemma good_of_inhabited : ∀ n : ℕ, dimension  α = n → good α :=
begin
intro, tactic.unfreeze_local_instances, revert α,
apply n.strong_induction_on,
intros k hk β _ hβ,
cases k, { apply good_of_dimension_zero, assumption },
apply good_of_shrink_good, apply hk,
{ rw ← hβ, apply shrink_decreasing, omega}, refl,
end


#### Jalex Stark (Jul 30 2020 at 23:27):

I think I just wrote my code "backwards", "like a computer scientist", so that I didn't have to manually specify terms

#### Patrick Lutz (Jul 30 2020 at 23:43):

Hmm, I see you're using nat.strong_induction_on. That is good enough for what I want, but do you know if there's a way to do something like this with pattern matching instead? E.g. in case you want to do induction on a type that doesn't have a lemma like strong_induction_on and you don't want to prove such a lemma? I've been pretty happy with using pattern-matching to do induction in other circumstances.

#### Jalex Stark (Jul 30 2020 at 23:49):

i think you can only pattern match on the actual constructors for the inductive type

#### Jalex Stark (Jul 30 2020 at 23:49):

you can do induction n using nat.strong_induction_on if you want to use that lemma with the induction tactic

#### Patrick Lutz (Jul 31 2020 at 00:15):

Jalex Stark said:

i think you can only pattern match on the actual constructors for the inductive type

That's not really what I'm asking. I believe in the proof I gave above I am using pattern-matching to do induction (with the pipe notation and so on), but maybe that's not actually what it's called. In any case, I am trying to ask if you can basically do something like my original proof but without all the @'s everywhere

#### Jalex Stark (Jul 31 2020 at 01:24):

you can use letI := h\a to promote local hypothesis h\a to a local instance

#### Jalex Stark (Jul 31 2020 at 01:25):

at the beginning of your tactic state, you don't have a local instance of inhabited \a

#### Patrick Lutz (Jul 31 2020 at 19:11):

Okay, I think the phrase I was looking for was "using the equation compiler to do well-founded recursion." Is it possible to give a proof of the example using the equation compiler rather than nat.strong_induction_on without running into problems with type inference?

#### Jalex Stark (Jul 31 2020 at 21:14):

my current guess is no, you'll have to be explicit in the equation compiler before you enter tactic mode

Last updated: May 08 2021 at 10:12 UTC