# Zulip Chat Archive

## Stream: general

### Topic: Dependently typed proof

#### Frantisek Silvasi (Feb 27 2018 at 10:47):

I don't suppose this sorry is provable - how does one convince Lean that whatever it is that I am mapping over comes from the list being mapped over? I can show that: `x ∈ filter P xs -> P x`

, but I can't tell map `x ∈ filter P xs`

, even though it's "obvious". This is a toy version of what I am trying to do:

def positive := {x : ℤ // x > 0} def x_of_positive : positive → ℤ | ⟨a, _⟩ := a def is_positive (x : ℤ) := x > 0 instance {x : ℤ} : decidable (is_positive x) := by simp [is_positive]; apply_instance def make_positive (x : ℤ) (h : x > 0) : positive := ⟨x, h⟩ def test_two (x : positive) := let pos := x_of_positive x in [pos+1, pos-1] def foo (x : positive) := let to_check := test_two x in let checked := list.filter is_positive to_check in let positives := list.map (λx, make_positive x sorry) checked in positives

#### Andrew Ashworth (Feb 27 2018 at 11:33):

you want the `of_mem_filter`

lemma in mathlib

#### Andrew Ashworth (Feb 27 2018 at 11:35):

wait, sorry, I didn't look closely enough at your code snippet

#### Frantisek Silvasi (Feb 27 2018 at 11:37):

The idea is to escape positive to Z and check x+/-1. Then I filter the ones that are not positive and now I need a way to inject them back to the dependent type.

#### Chris Hughes (Feb 27 2018 at 11:39):

list.pmap in mathlib is probably what you want

#### Andrew Ashworth (Feb 27 2018 at 11:40):

one way to do it would be to prove that all the operations you use preserve the `is_positive`

invariant

#### Andrew Ashworth (Feb 27 2018 at 11:42):

this is kind of tedious, i'd be hunting for a appropriate function in the data.list namespace, maybe `pmap`

would be appropriate as Chris mentioned

#### Patrick Massot (Feb 27 2018 at 11:42):

Don't forget to use````lean`

instead of ````` at the beginning of your code blocks to have (partial) syntax highlighting

#### Frantisek Silvasi (Feb 27 2018 at 11:43):

I'll take a look at the pmap, thank you.

#### Frantisek Silvasi (Feb 27 2018 at 11:46):

Interesting. This `pmap`

contraption is basically `map . filter`

, which is exactly what I do, except I manage to lose some information in between.

#### Chris Hughes (Feb 27 2018 at 11:46):

import data.list.basic def positive := {x : ℤ // x > 0} def x_of_positive : positive → ℤ | ⟨a, _⟩ := a def is_positive (x : ℤ) := x > 0 instance {x : ℤ} : decidable (is_positive x) := by simp [is_positive]; apply_instance def make_positive (x : ℤ) (h : x > 0) : positive := ⟨x, h⟩ def test_two (x : positive) := let pos := x_of_positive x in [pos+1, pos-1] def foo (x : positive) := let to_check := test_two x in let checked := list.filter is_positive to_check in let positives := list.pmap (λ x (hx : x > 0), make_positive x hx) checked (λ a ha, (list.mem_filter.1 ha).right) in positives

#### Frantisek Silvasi (Feb 27 2018 at 11:47):

Is the `a ha`

accidental ;)?

#### Frantisek Silvasi (Feb 27 2018 at 11:47):

Thank you kindly for your help, I'm going to take `pmap`

for a spin.

#### Mario Carneiro (Feb 27 2018 at 17:50):

@Frantisek Silvasi The combination of filter and map in the positive case is `filter_map`

. You should `filter_map`

with the function `if h : x > 0 then some (is_positive x h) else none`

Last updated: Aug 03 2023 at 10:10 UTC