Dependent substitution

Stream: general

[Patrick Johnson]

How to deal with this?

import tactic

constant n : ℕ
constant init : ℕ → ℕ
constant V : ℕ → Type
constant f : Π (n : ℕ), V n
constant ma : V (init n)

example
  (h : ∀ (m : V n), f n = m)
  (H : init n = n) :
  f (init n) = ma :=
begin
  simp_rw H, -- fails
  subst H,   -- fails
  cases H,   -- fails
end

[Mario Carneiro]

the theorem isn't provable?

[Floris van Doorn]

What do you want your goal to be after any of these tactics?

[Floris van Doorn]

Here is to prove it. You want to generalize one of the sides of the equality H to be a fresh variable, so you can substitute/case it away.

example
  (h : ∀ (m : V n), f n = m)
  (H : (init n) = n) :
  f (init n) = ma :=
begin
  have : ∀ {n' : ℕ} (h : ∀ (m : V n'), f n' = m) (H : (init n) = n'), f (init n) = ma,
  { intros n' h' H', subst H', apply h' },
  exact this h H
end

[Patrick Johnson]

Thanks, it works. But I'm wondering can simp_rw be improved to handle such situations?
I was expecting to have goal f n = H.rec ma after simp_rw.

[Eric Wieser]

I ran into something similar with cons_induction_cons #13027. It would be nice if generalize could help

[Mario Carneiro]

here's a proof that doesn't require stating the induction hypothesis:

example
  (h : ∀ (m : V n), f n = m)
  (H : init n = n) :
  f (init n) = ma :=
begin
  generalize : ma = m,
  revert m,
  rw H,
  apply h
end

[Eric Wieser]

Does something similar work for my cons proof?

[Patrick Johnson]

@Mario Carneiro That works only in this contrived example, because h is universally quantified over V n and doesn't need any properties of ma. In my actual context, it cannot be applied. Floris van Doorn's solution cannot be applied either. Here is a very simplified and minimized example obtained from my actual lemma:

import tactic
import tactic.induction

noncomputable theory
open_locale classical

constant A : Type
constant B : Type
structure C : Type := (a : B) (b : list B) (c : Prop)
def D : Type := A
def E : Type := option A
def f₁ (y : ℕ) (b : B) := true
structure F (y : ℕ) (b : B) := (m : D) (h : true)
structure G (b : B) := (m : E) (h : true)
def f₂ (s : C) (b : B) : C := {s with a := b, b := s.b ++ [s.a] }
constant H (s : C) : E → B
def f₃ (s : C) (m : E) : C := f₂ s (H s m)
structure I (y : ℕ) : Type := (f : Π (s : C), s.c → true → F y s.a)
structure J : Type := (f : Π (s : C), s.c → G s.a)
constant I.x (y : ℕ) : I y
constant I.f₄ {y : ℕ} (a : I y) (s : C) (ma : F y s.a) : I y
@[ext] structure K (y : ℕ) : Type := (a : I y) (d : J) (s : C)
def m := @K.mk
def K.f₅ {y : ℕ} (g : K y) (s₁ : C) : K y := {g with s := s₁}
def f₆ {y : ℕ} (g : K y) (hs) := g.f₅ (f₃ g.s (g.d.f g.s hs).m)

example {y : ℕ} {s s' : C} {md : G s.a} {ma : F y s'.a}
  (hs : s.c) (hs₁ : s'.c) (d : J) (hx : f₁ y s'.a) :
  let a : I y := (I.x y).f₄ s' ma
  in ∀ (h₂ : f₁ y (f₆ (m a d s) hs).s.a), (f₆ (m a d s) hs).s = s' →
  (a.f (f₆ (m a d s) hs).s hs h₂).m = (a.f s' hs₁ hx).m :=
begin
  rintro a h₂ h₁,
  simp_rw h₁, -- fails
end

We don't need to look at all those definitions. All we can observe is that we have hypothesis h₁ and the goal would be refl after rewriting h₁. I don't really see what to generalize in order to close this goal...?

[Mario Carneiro]

kind of messy, but congr, exact h₁, exact h₁, apply proof_irrel_heq, works

[Mario Carneiro]

or just congr'

[Patrick Johnson]

This is the shortest proof I can get (for the first example). We don't need to generalize anything.

example
  (h : ∀ (m : V n), f n = m)
  (H : init n = n) :
  f (init n) = ma :=
begin
  convert h _,
  exact heq_of_eq_rec_left H rfl,
end

[Kyle Miller]

@Patrick Johnson Here's another proof:

example
  (h : ∀ (m : V n), f n = m)
  (H : init n = n) :
  f (init n) = ma :=
begin
  rw ← H at h,
  exact h ma,
end

[Eric Wieser]

Eric Wieser said:

I ran into something similar with cons_induction_cons #13027. It would be nice if generalize could help

Here's a mwe of this proof, in case anyone feels like being sniped by it:

import data.fin.tuple
variables {n : ℕ} {α : fin n.succ → Type*}
universes u v
open fin

/-- Recurse on an `n+1`-tuple by splitting it into a single element and an `n`-tuple. -/
@[elab_as_eliminator]
def cons_induction {P : (Π i : fin n.succ, α i) → Sort v}
  (h : ∀ x₀ x, P (fin.cons x₀ x)) (x : (Π i : fin n.succ, α i)) : P x :=
_root_.cast (by rw cons_self_tail) $ h (x 0) (tail x)

@[simp] lemma cons_induction_cons {P : (Π i : fin n.succ, α i) → Sort v}
  (h : Π x₀ x, P (fin.cons x₀ x)) (x₀ : α 0) (x : Π i : fin n, α i.succ) :
  @cons_induction _ _ _ h (cons x₀ x) = h x₀ x :=
begin
  suffices : ∀ y (hy : y = cons x₀ x), _root_.cast (by rw hy) (@cons_induction _ _ _ h y) = h x₀ x,
  { convert this _ rfl },
  rintro y rfl,
  dunfold cons_induction,
  simp_rw [cast_cast, cast_eq],
  congr,
  rw tail_cons,
end

[Eric Rodriguez]

@[simp] lemma cons_induction_cons {P : (Π i : fin n.succ, α i) → Sort v}
  (h : Π x₀ x, P (fin.cons x₀ x)) (x₀ : α 0) (x : Π i : fin n, α i.succ) :
  @cons_induction _ _ _ h (cons x₀ x) = h x₀ x :=
begin
  simp only [cons_induction, cast_eq],
  congr',
  exact tail_cons _ _
end

[Eric Rodriguez]

do we have a dependent congr_arg(₂)? I think this is the correct glue, this congr does some crazy eq.recs that I don't understand

[Eric Rodriguez]

which makes sense, I guess, as that is what congr_arg basically is

[Eric Rodriguez]

I feel like I'm understanding this a bit better; in some ways you want to rw (h)eq.rec (h x_0 x) (tail_cons _ _) but the elaborator is not going to be happy matching that

[Yaël Dillies]

I've been wanting congr_arg₂, congr_fun₂ and funext₂ recently. I was about to add them. What do people think?

[Eric Rodriguez]

seems like a good idea to me!

[Eric Wieser]

Thanks @Eric Rodriguez, I have no idea how I didn't find that; edited the PR to use your proof