Problems with induction and type inference

Stream: new members

[Patrick Lutz]

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]

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]

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

[Patrick Lutz]

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]

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

[Jalex Stark]

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

[Patrick Lutz]

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]

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

[Jalex Stark]

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

[Patrick Lutz]

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]

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