Zulip Chat Archive

Stream: new members

Topic: How do I map a list along with proof of membership?


view this post on Zulip Marko Grdinić (Oct 23 2019 at 14:11):

def list_dice := [1,2,3,4,5,6]
def list_claim := [(1,2), (1,3), (1,4), (1,5), (1,6), (1,1), (2,2), (2,3), (2,4), (2,5), (2,6), (2,1)]

inductive Action
| Claim (claim : {n // n  list_claim}) : Action
| Dudo : Action

def actions : list Action :=
    let claims : list Action :=
        list_claim.map (fun x,
            Action.Claim  x, sorry 
            ) in
    Action.Dudo :: claims

I've defined an inductive type like this and now I also want to turn it into a list. That having said, I have no idea how to provide the proof of membership. The x is opaque, so I do not have the necessary information to prove this.

How should I approach this?

view this post on Zulip Marc Huisinga (Oct 23 2019 at 14:17):

you can attach the proof of membership before mapping https://github.com/leanprover-community/mathlib/blob/24dd80b0db5f2adbefd3b00709b4a445fc18fb9b/src/data/list/basic.lean#L1720
(edited to provide permalink ;))

view this post on Zulip Marko Grdinić (Oct 23 2019 at 14:19):

Thank you.


Last updated: May 09 2021 at 18:17 UTC