Zulip Chat Archive

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 : ,  α [ : inhabited α], @dimension α  = 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 : ,  α [ : inhabited α], @dimension α  = n  good α
| 0 := λ α  h, @good_of_dimension_zero α  h
| (n + 1) :=
begin
    intros α  hn,
    let β := @shrink α ,
    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 α  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 β _ ,
  cases k, { apply good_of_dimension_zero, assumption },
  apply good_of_shrink_good, apply hk,
  { rw  , 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: Dec 20 2023 at 11:08 UTC