Proving two filterMaps are equal

Stream: new members

[Dhruv Chaurasiya]

import Std
import Lean
open Std
open Lean

abbrev SortName := String

structure TypedValue where
  sort : SortName
  val  : String
  deriving Repr, BEq, Hashable, Inhabited, DecidableEq

def tv (s : SortName) (v : String) : TypedValue := { sort := s, val := v }

inductive Param where
  | bot
  | top
  | val (tv : TypedValue)
  deriving Repr, BEq, Hashable,Inhabited, DecidableEq

def get_top_indices (ps : List Param) : List Nat :=
  (List.range ps.length |>.zip ps).filterMap fun
    | (i, Param.top) => some i
    | _              => none

theorem tops_equal
(i : Nat)
(params1 params2 : List Param)
(h_len : params1.length = params2.length)
(h_at_i_bot : params1[i]? = some Param.bot)
(h_at_i_val : ∃ tv : TypedValue, params2[i]? = some (Param.val tv))
(h_others_match : ∀ (j : Nat), ¬j = i → params1[j]? = params2[j]?) :
get_top_indices params1 = get_top_indices params2 := by
simp [get_top_indices]

How can i go on proving two List.filterMap are equal, from the given hypothesis, that the length of both the List are same, and other hypothesis regarding their values at each index, I can see this must be true, but I cannot find any way too simplify this.
Is there any dedicated channel for such issues?

[Johannes Tantow]

#mwe

[Ruben Van de Velde]

Here is fine, but yes, please follow the #mwe link and give us a code snippet we can easily work with

[Dhruv Chaurasiya]

Ruben Van de Velde said:

Here is fine, but yes, please follow the #mwe link and give us a code snippet we can easily work with

I have provided the information needed, please let me know if anything else is required

[Ruben Van de Velde]

Can you read it again? I don't see a single code snippet that I can run to see the exact issue you're asking for help with

[Dhruv Chaurasiya]

Ruben Van de Velde said:

Here is fine, but yes, please follow the #mwe link and give us a code snippet we can easily work with

Ruben Van de Velde said:

Can you read it again? I don't see a single code snippet that I can run to see the exact issue you're asking for help with

you can copy paste the first code snippet in your lean file to check that

[Robin Arnez]

Here's a proof:

abbrev SortName := String

structure TypedValue where
  sort : SortName
  val  : String
  deriving Repr, BEq, Hashable, Inhabited, DecidableEq


def tv (s : SortName) (v : String) : TypedValue := { sort := s, val := v }

inductive Param where
  | bot
  | top
  | val (tv : TypedValue)
  deriving Repr, BEq, Hashable, Inhabited, DecidableEq

def get_top_indices (ps : List Param) : List Nat :=
  (List.range ps.length |>.zip ps).filterMap fun
    | (i, Param.top) => some i
    | _              => none

theorem filterMap_id_map (l : List α) (f : α → Option β) :
    List.filterMap id (List.map f l) = List.filterMap f l := by simp

theorem tops_equal {tv : TypedValue}
    (i : Nat)
    (params1 params2 : List Param)
    (h_len : params1.length = params2.length)
    (h_at_i_bot : params1[i]? = some Param.bot)
    (h_at_i_val : params2[i]? = some (Param.val tv))
    (h_others_match : ∀ (j : Nat), ¬j = i → params1[j]? = params2[j]?) :
    get_top_indices params1 = get_top_indices params2 := by
  simp only [get_top_indices]
  conv => lhs; rw [← filterMap_id_map]
  conv => rhs; rw [← filterMap_id_map]
  congr 1
  ext1 k
  specialize h_others_match k
  grind

The argument is basically that you can rewrite a filterMap to flattening a map and the maps are equal at every position.

[Dhruv Chaurasiya]

Robin Arnez said:

Here's a proof:

abbrev SortName := String

structure TypedValue where
  sort : SortName
  val  : String
  deriving Repr, BEq, Hashable, Inhabited, DecidableEq


def tv (s : SortName) (v : String) : TypedValue := { sort := s, val := v }

inductive Param where
  | bot
  | top
  | val (tv : TypedValue)
  deriving Repr, BEq, Hashable, Inhabited, DecidableEq

def get_top_indices (ps : List Param) : List Nat :=
  (List.range ps.length |>.zip ps).filterMap fun
    | (i, Param.top) => some i
    | _              => none

theorem filterMap_id_map (l : List α) (f : α → Option β) :
    List.filterMap id (List.map f l) = List.filterMap f l := by simp

theorem tops_equal {tv : TypedValue}
    (i : Nat)
    (params1 params2 : List Param)
    (h_len : params1.length = params2.length)
    (h_at_i_bot : params1[i]? = some Param.bot)
    (h_at_i_val : params2[i]? = some (Param.val tv))
    (h_others_match : ∀ (j : Nat), ¬j = i → params1[j]? = params2[j]?) :
    get_top_indices params1 = get_top_indices params2 := by
  simp only [get_top_indices]
  conv => lhs; rw [← filterMap_id_map]
  conv => rhs; rw [← filterMap_id_map]
  congr 1
  ext1 k
  specialize h_others_match k
  grind

The argument is basically that you can rewrite a filterMap to flattening a map and the maps are equal at every position.

thanks a lot for the proof.

[Johannes Tantow]

You can also express your zip construction with List.zipIdx

[Dhruv Chaurasiya]

Johannes Tantow said:

You can also express your zip construction with List.zipIdx

I did not know that. Thanks, I would try it out.