Zulip Chat Archive

Stream: new members

Topic: Unfold partially applied inductive func


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Mar 03 2021 at 21:17):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Mar 03 2021 at 22:32):

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

view this post on Zulip Eric Wieser (Mar 03 2021 at 22:33):

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

view this post on Zulip Yakov Pechersky (Mar 03 2021 at 22:47):

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

view this post on Zulip Eric Wieser (Mar 03 2021 at 22:48):

I want to unfold nth into a lambda

view this post on Zulip Eric Wieser (Mar 03 2021 at 22:48):

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

view this post on Zulip Eric Wieser (Mar 03 2021 at 22:48):

Because unfold works in that second case

view this post on Zulip Yakov Pechersky (Mar 03 2021 at 22:51):

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

view this post on Zulip Eric Wieser (Mar 03 2021 at 22:58):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Mar 04 2021 at 16:37):

Do you know that mjoin here is injective?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Mar 04 2021 at 16:40):

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

view this post on Zulip Yakov Pechersky (Mar 04 2021 at 16:41):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Marcus Rossel (Mar 04 2021 at 16:54):

But thanks for your help!

view this post on Zulip Yakov Pechersky (Mar 04 2021 at 17:05):

In general, the simplifier is your friend!

view this post on Zulip 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