Unfold partially applied inductive func

Stream: new members

[Marcus Rossel]

In the following example. ..

structure thing :=
(input : list ℕ)
(output : list ℕ)

inductive side
| front : side
| back : side

def thing.nth (t : thing) : side → ℕ → option ℕ
| side.front n := t.input.nth n
| side.back n := t.output.nth n

lemma front_eq_input (t : thing) : t.input.nth = t.nth side.front :=
begin
  unfold thing.nth,
  -- simplify tactic failed to simplify
end

... why can't I unfold thing.nth?
I feel like it has to do something with the fact that the ℕ is on the right side of the colon in thing.nth, but I don't actually know.

[Yakov Pechersky]

Yes, you have to invent a nat there:

lemma front_eq_input (t : thing) : t.input.nth = t.nth side.front :=
begin
  ext,
  rw thing.nth
end

[Yakov Pechersky]

Compare to:

def thing.nth (t : thing) : side → ℕ → option ℕ
| side.front := t.input.nth
| side.back := t.output.nth

lemma front_eq_input (t : thing) : t.input.nth = t.nth side.front := rfl

[Yakov Pechersky]

I've removed the repetitive ... n := ... n into a ... := ...

[Eric Wieser]

This is particularly pernicious when the inductive function is in the middle of a larger expression so ext doesn't work

[Eric Wieser]

Eg list.map (t.nth side.back) l

[Eric Wieser]

Is the some way to un-delta/beta/whatever-it-is reduce the function?

[Yakov Pechersky]

You mean to rewrite within the map if the lemma exists only in fully applied form?

[Eric Wieser]

I want to unfold nth into a lambda

[Eric Wieser]

As if I'd written list.map (fun n, t.nth side.back n) l

[Eric Wieser]

Because unfold works in that second case

[Yakov Pechersky]

have : t.nth side.back = fun n, t.nth side.back n := rfl, rw this?

[Eric Wieser]

More awkward if the arguments are some ugly expression, but I guess that works

[Yakov Pechersky]

Nope, doesn't work. But it wouldn't have worked even for the either type of defining it.

[Yakov Pechersky]

I did experiment with a tactic that would do exactly what I suggested, but it got me nowhere. For posterity:

open tactic expr

meta def expr.pi_to_lam : expr → expr
| (pi n bi d b) := lam n bi d b.pi_to_lam
| e := e

meta def expr.count_pis : expr → ℕ
| (pi n bi d b) := 1 + b.count_pis
| e := 0

meta def func_to_lam (e : expr) : tactic unit := do
  eo ← to_expr ``(%%e),
  t ← infer_type e,
  let k : ℕ := t.count_pis,
  e' ← list.mfoldl (λ e' _, to_expr ``(λ x, %%e' x))
    e (list.range k),
  pe ← to_expr ``(%%eo = %%e'),
  h ← get_unused_name,
  rflp ← to_expr ``(rfl),
  note h (some pe) rflp,
  he ← get_local h,
  -- how do I run `rw %%he` now?
  pure ()

meta def interactive.func_to_lam : tactic unit := do
  e ← to_expr ```(t.nth side.front),
  func_to_lam e

lemma front_eq_input (t : thing) : list.map (t.input.nth) = list.map (t.nth side.front) :=
begin
  interactive.func_to_lam,
  rw _x,
  sorry
end

[Marcus Rossel]

I feel like I've run into the same situation again.
Is this one solvable, or does there exists some workaround? :pray:
And why doesn't this just work?

variable (υ : Type*)

def ports := list (option υ)

variable {υ}

def ports.nth (p : ports υ) (n : ℕ) : option υ := mjoin (list.nth p n)

example {p p' : ports υ} (h : p.nth = p'.nth) : true :=
begin
  unfold ports.nth at h, -- doesn't unfold
end

[Yakov Pechersky]

What do you want to do here?

example {p p' : ports υ} (h : p.nth = p'.nth) : true :=
begin
  have h' : ∀ n, p.nth n = p'.nth n := congr_fun h,
  unfold ports.nth at h'
end

[Marcus Rossel]

Ok now I'm confused, this doesn't work for me outside of the MWE.
I'm trying to prove this:

lemma ext {p p' : ports υ} (hₚ : p.nth = p'.nth) (hₗ : p.length = p'.length) : p = p' :=
begin
  ext1 x,
  by_cases hc : x < p.length,
    {
      have h' : ∀ n, p.nth n = p'.nth n, from congr_fun hₚ,
      unfold ports.nth at h',
      -- ...
    },
    {
      have h, from not_lt.mp hc,
      rw hₗ at hc,
      have h', from not_lt.mp hc,
      rw [list.nth_len_le h, list.nth_len_le h'],
    }
end

[Yakov Pechersky]

Do you know that mjoin here is injective?

[Marcus Rossel]

Yakov Pechersky said:

Do you know that mjoin here is injective?

What does that mean in this context?

[Yakov Pechersky]

lemma ext {p p' : ports υ} (hₚ : p.nth = p'.nth) (hₗ : p.length = p'.length) : p = p' :=
begin
  ext1 x,
  by_cases hc : x < p.length,
    { have h' : ∀ n, p.nth n = p'.nth n, from congr_fun hₚ,
      unfold ports.nth at h',
      have hm : function.injective (mjoin : option (option υ) → option υ) := sorry,
      apply hm,
      rw h' },
    { have h, from not_lt.mp hc,
      rw hₗ at hc,
      have h', from not_lt.mp hc,
      rw [list.nth_len_le h, list.nth_len_le h'] }
end

[Yakov Pechersky]

In general, option.join is not injective because option.join none = option.join (some none)

[Yakov Pechersky]

You'll have to show that list.nth must be some when in bounds

[Yakov Pechersky]

lemma ext {p p' : ports υ} (hₚ : p.nth = p'.nth) (hₗ : p.length = p'.length) : p = p' :=
begin
  ext1 x,
  by_cases hc : x < p.length,
    { have h' : ∀ n, p.nth n = p'.nth n, from congr_fun hₚ,
      unfold ports.nth at h',
      have : ∀ (p : ports υ) n < p.length, ∃ v, list.nth p n = some v,
        { intros p n hn,
          use list.nth_le p n hn,
          rw list.nth_eq_some,
          simp [hn] },
      specialize h' x,
      obtain ⟨v, hv⟩ := this p x hc,
      obtain ⟨v', hv'⟩ := this p' x (hₗ ▸ hc),
      simpa [hv, hv', option.join_eq_join] using h' },
    { have h, from not_lt.mp hc,
      rw hₗ at hc,
      have h', from not_lt.mp hc,
      rw [list.nth_len_le h, list.nth_len_le h'] }
end

[Marcus Rossel]

I ended up doing it this way :D

  lemma ext {p p' : ports υ} (hₚ : p.nth = p'.nth) (hₗ : p.length = p'.length) : p = p' :=
    begin
      ext1 x,
      by_cases hc : x < p.length,
        {
          have h' : ∀ n, p.nth n = p'.nth n, from congr_fun hₚ,
          unfold nth at h',
          replace h' := h' x,
          rw list.nth_le_nth hc at h' ⊢,
          have hj : ∀ n : option υ, (option.some n).join = n, by finish,
          rw hj at h',
          rw hₗ at hc,
          rw list.nth_le_nth hc at h' ⊢,
          rw hj at h',
          rw h',
        },
        {
          have h, from not_lt.mp hc,
          rw hₗ at hc,
          have h', from not_lt.mp hc,
          rw [list.nth_len_le h, list.nth_len_le h']
        }
    end

[Marcus Rossel]

But thanks for your help!

[Yakov Pechersky]

In general, the simplifier is your friend!

[Marcus Rossel]

@Yakov Pechersky are you talking about that sequence of rewrites I have? :D