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 : ℕ, ∀ α [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: Dec 20 2023 at 11:08 UTC