Zulip Chat Archive

Stream: new members

Topic: list.map with pi


Gavid Liebnich (Nov 09 2018 at 07:27):

Hello. I have an issue using dependent function space in conjunction with list.map. Could anyone take a peek?
In the following state:

α : Type,
g g' : list α,
f : Π (a : α), a  g  α,
h : g = g'
 map (λ (c : {x // x  g}), f (c.val) _) (attach g) = nil

I would like to rewrite g with g'. However, I get "motive is not type correct" error.
I think I understand why this is. Given c.2 is supposed to be x ∈ g, I would end up with mismatching types as attach g' would lead to c.2 being x ∈ g'.
However, I am not sure how to proceed - I think I need some kind of a congruence that says I can switch map f l for map f' l' if I can show f = f' and l = l', but "modulo types".
You can reconstruct the goal (and the error) with:

import data.list
open list
variables {α : Type} {g g' : list α} {f : Π(a : α) (h : a  g), α}
def foo := map (λ(c : {x // x  g}), f c.1 c.2) (attach g)
example (h : g = g') : @foo α g f = [] :=
begin
  unfold foo,
  rw h -- motive not type correct
end

Mario Carneiro (Nov 09 2018 at 07:39):

Is g a variable? If so, subst g is probably the easiest thing

Gavid Liebnich (Nov 09 2018 at 07:47):

I am not sure I know what variable means in this context, but g is a list computed by a function, so I think it is not. The equivalence h : g = g' basically expands bar x y to x :: bar x' y. I've tried subst expand_bar, but the "given expression is not a local constant".

Gavid Liebnich (Nov 09 2018 at 07:52):

Definitely not a variable, come to think of it, h : g = g' is just h : expand_bar a b = a :: expand_bar a' b. And I don't think I can subst expand_bar.

Mario Carneiro (Nov 09 2018 at 08:05):

I think you need to unsimplify your example then. This is generally speaking a complicated problem with nonuniform solutions, I would have to know more about the problem to say how to proceed

Gavid Liebnich (Nov 09 2018 at 08:07):

I will give it a try, thanks. I did a lot of simplifying, may have lost something along the way :).

Patrick Massot (Nov 09 2018 at 08:11):

The subst tactic (instead of rw) may help you

Floris van Doorn (Nov 10 2018 at 15:08):

I don't know if this works in your actual example, but you could try reverting everything which depends on g:

example (h : g = g') : @foo α g f = [] :=
begin
  unfold foo,
  revert f,
  rw h,
  intro f
end

Floris van Doorn (Nov 10 2018 at 15:10):

Note that this rw now also rewrites the type of f.


Last updated: Dec 20 2023 at 11:08 UTC