## Stream: new members

### Topic: Unfold partially applied inductive func

#### Marcus Rossel (Mar 03 2021 at 21:13):

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 (Mar 03 2021 at 21:15):

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 (Mar 03 2021 at 21:16):

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 (Mar 03 2021 at 21:17):

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

#### Eric Wieser (Mar 03 2021 at 22:29):

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

#### Eric Wieser (Mar 03 2021 at 22:32):

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

#### Eric Wieser (Mar 03 2021 at 22:33):

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

#### Yakov Pechersky (Mar 03 2021 at 22:47):

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

#### Eric Wieser (Mar 03 2021 at 22:48):

I want to unfold nth into a lambda

#### Eric Wieser (Mar 03 2021 at 22:48):

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

#### Eric Wieser (Mar 03 2021 at 22:48):

Because unfold works in that second case

#### Yakov Pechersky (Mar 03 2021 at 22:51):

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

#### Eric Wieser (Mar 03 2021 at 22:58):

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

#### Yakov Pechersky (Mar 04 2021 at 01:16):

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

#### Yakov Pechersky (Mar 04 2021 at 01:20):

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 (Mar 04 2021 at 16:24):

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 (Mar 04 2021 at 16:26):

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 (Mar 04 2021 at 16:32):

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 (Mar 04 2021 at 16:37):

Do you know that mjoin here is injective?

#### Marcus Rossel (Mar 04 2021 at 16:38):

Yakov Pechersky said:

Do you know that mjoin here is injective?

What does that mean in this context?

#### Yakov Pechersky (Mar 04 2021 at 16:38):

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 (Mar 04 2021 at 16:40):

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

#### Yakov Pechersky (Mar 04 2021 at 16:41):

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

#### Yakov Pechersky (Mar 04 2021 at 16:51):

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 (Mar 04 2021 at 16:53):

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 (Mar 04 2021 at 16:54):

But thanks for your help!

#### Yakov Pechersky (Mar 04 2021 at 17:05):

In general, the simp`lifier is your friend!

#### Marcus Rossel (Mar 04 2021 at 18:31):

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

Last updated: May 14 2021 at 07:19 UTC