Zulip Chat Archive

Stream: new members

Topic: Can't `rw if_pos` in `let`


view this post on Zulip Marcus Rossel (Jan 19 2021 at 14:59):

Ok, I've got another one I don't know how to fix:

def ports : Type* := list (option empty)
instance : has_append ports := list.has_append.append

def merge (first last : ports) : ports :=
    let p' := last.zip_with (<|>) first in
    if first.length  last.length then p' else p' ++ list.repeat none (first.length - last.length)

example (p : ports) : merge p (list.repeat none p.length) = p :=
begin
  unfold merge,
  have h : list.length p  list.length (list.repeat (none : option empty) (list.length p)), from sorry,
  rw if_pos h,

end

I would like to apply rw if_pos h, but get an error, even though I've literally copy-pasted the hypothesis h out of the goal.
How can I solve this?

view this post on Zulip Patrick Massot (Jan 19 2021 at 15:02):

The main trick is is to read the webpage #mwe.

view this post on Zulip Marcus Rossel (Jan 19 2021 at 15:09):

Patrick Massot said:

The main trick is is to read the webpage #mwe.

Haha sorry, I've updated the example above.

view this post on Zulip Patrick Massot (Jan 19 2021 at 15:11):

Using let like this is asking for trouble.

view this post on Zulip Marcus Rossel (Jan 19 2021 at 15:11):

Patrick Massot said:

Using let like this is asking for trouble.

I've heard this before. What is the right way to use let then, and how can I circumvent it in this example?

view this post on Zulip Patrick Massot (Jan 19 2021 at 15:12):

What about

def merge (first last : ports) : ports :=
    (last.zip_with (<|>) first) ++
    (if first.length  last.length then list.nil else list.repeat none (first.length - last.length))

view this post on Zulip Marcus Rossel (Jan 19 2021 at 15:14):

Patrick Massot said:

What about

def merge (first last : ports) : ports :=
    (last.zip_with (<|>) first) ++
    (if first.length  last.length then list.nil else list.repeat none (first.length - last.length))

Ah yes, :face_palm:🏼‍♀️ Thanks :D


Last updated: May 12 2021 at 23:13 UTC