matching `instBEqOfDecidableEq` and `List.instBEq`

Stream: lean4

[Paige Thomas]

I'm wondering if someone might know what I need to make these match, where the first has instBEqOfDecidableEq and the other has List.instBEq?

1 goal
PSS QSS : List (List Formula_)
s1 : Function.Injective (List.map not_)
s2 : List.map (List.map not_) (PSS ∪ QSS) = List.map (List.map not_) PSS ∪ List.map (List.map not_) QSS
⊢ List.map (List.map not_) (PSS ∪ QSS) = List.map (List.map not_) PSS ∪ List.map (List.map not_) QSS
Expected type
PSS QSS : List (List Formula_)
s1 : Function.Injective (List.map not_)
s2 : List.map (List.map not_) (PSS ∪ QSS) = List.map (List.map not_) PSS ∪ List.map (List.map not_) QSS
⊢ List.map (List.map not_) (PSS ∪ QSS) = List.map (List.map not_) PSS ∪ List.map (List.map not_) QSS
Messages (1)
ToCNF.lean:40:2
type mismatch
  s2
has type
  List.map (List.map not_)
      (@Union.union (List (List Formula_)) (@List.instUnionOfBEq_batteries (List Formula_) instBEqOfDecidableEq) PSS
        QSS) =
    List.map (List.map not_) PSS ∪ List.map (List.map not_) QSS : Prop
but is expected to have type
  List.map (List.map not_)
      (@Union.union (List (List Formula_)) (@List.instUnionOfBEq_batteries (List Formula_) List.instBEq) PSS QSS) =
    List.map (List.map not_) PSS ∪ List.map (List.map not_) QSS : Prop

[Paige Thomas]

This comes from:

lemma map_map_not_union
  (PSS QSS : List (List Formula_)) :
  map_map_not (PSS ∪ QSS) = (map_map_not PSS) ∪ (map_map_not QSS) :=
  by
  unfold map_map_not
  have s1 : Function.Injective (List.map not_) :=
  by
    simp only [List.map_injective_iff]
    unfold Function.Injective
    intro P Q a1
    simp only [not_.injEq] at a1
    exact a1

  obtain s2 := List.map_union (List.map not_) PSS QSS s1
  exact s2

where List.map_union is:

lemma List.map_union
  {α β : Type}
  [DecidableEq α]
  [DecidableEq β]
  (f : α → β)
  (l1 l2 : List α)
  (h1 : Function.Injective f) :
  List.map f (l1 ∪ l2) = (List.map f l1) ∪ (List.map f l2) :=

[Paige Thomas]

and

def map_map_not
  (FSS : List (List Formula_)) :
  List (List Formula_) :=
  List.map (List.map not_) FSS

[Kyle Miller]

Could you give a #mwe?

Something I'd suggest trying is using mathlib's convert s2, which tries to deal with these sorts of differences. Mathlib also has subsingleton, which might be useful for discharging some of the remaining goals.

[Paige Thomas]

I guess I'm not sure what is going on enough to give a mwe?

[Paige Thomas]

For some reason this gives

typeclass instance problem is stuck, it is often due to metavariables
Union (List (List ?m.11303))Lean 4

on the web, but not in my VS code.

import Mathlib

inductive Formula_ : Type
  | false_ : Formula_
  | true_ : Formula_
  | atom_ : String → Formula_
  | not_ : Formula_ → Formula_
  | and_ : Formula_ → Formula_ → Formula_
  | or_ : Formula_ → Formula_ → Formula_
  | imp_ : Formula_ → Formula_ → Formula_
  | iff_ : Formula_ → Formula_ → Formula_
  deriving Inhabited, DecidableEq, Hashable, Repr

compile_inductive% Formula_

theorem extracted_1
  (PSS QSS : List (List Formula_))
  (s1 : List.map (List.map not_) (PSS ∪ QSS) = List.map (List.map not_) PSS ∪ List.map (List.map not_) QSS) :
  List.map (List.map not_) (PSS ∪ QSS) = List.map (List.map not_) PSS ∪ List.map (List.map not_) QSS := sorry

[Kyle Miller]

It might be called "MWE" but it doesn't need to be minimal or working. The point is to have something we can paste into an editor to help you diagnose the issue and find something that works.

[Kyle Miller]

It saves collective time too, since then people don't have to individually try to reproduce the issue locally.

[Paige Thomas]

This reproduces it:

import Mathlib


lemma List.map_union
  {α β : Type}
  [DecidableEq α]
  [DecidableEq β]
  (f : α → β)
  (l1 l2 : List α)
  (h1 : Function.Injective f) :
  List.map f (l1 ∪ l2) = (List.map f l1) ∪ (List.map f l2) :=
  by
  induction l1
  case nil =>
    simp only [List.map_nil]
    simp only [List.nil_union]
  case cons hd tl ih =>
    simp only [List.cons_union, List.map_cons]
    rewrite [← ih]
    unfold List.insert

    have s1 : List.elem (f hd) (List.map f (tl ∪ l2)) = true ↔ List.elem hd (tl ∪ l2) = true :=
    by
      simp only [List.elem_eq_mem, decide_eq_true_eq]
      apply List.mem_map_of_injective
      exact h1

    simp only [s1]
    split_ifs
    case pos c1 =>
      rfl
    case neg c1 =>
      simp only [List.map_cons]


inductive Formula_ : Type
  | false_ : Formula_
  | true_ : Formula_
  | atom_ : String → Formula_
  | not_ : Formula_ → Formula_
  | and_ : Formula_ → Formula_ → Formula_
  | or_ : Formula_ → Formula_ → Formula_
  | imp_ : Formula_ → Formula_ → Formula_
  | iff_ : Formula_ → Formula_ → Formula_
  deriving Inhabited, DecidableEq, Hashable, Repr

compile_inductive% Formula_

open Formula_


def map_map_not
  (FSS : List (List Formula_)) :
  List (List Formula_) :=
  List.map (List.map not_) FSS


lemma map_map_not_union
  (PSS QSS : List (List Formula_)) :
  map_map_not (PSS ∪ QSS) = (map_map_not PSS) ∪ (map_map_not QSS) :=
  by
  unfold map_map_not
  have s1 : Function.Injective (List.map not_) :=
  by
    simp only [List.map_injective_iff]
    unfold Function.Injective
    intro P Q a1
    simp only [not_.injEq] at a1
    exact a1

  obtain s2 := List.map_union (List.map not_) PSS QSS s1
  exact s2

[Kyle Miller]

Kyle Miller said:

Something I'd suggest trying is using mathlib's convert s2

This works

[Paige Thomas]

Oh, oops, I didn't realize it was a finishing tactic. I had an exact after it. Thank you!

[Ruben Van de Velde]

It can be, but isn't always

[Robin Arnez]

Union on lists is defined using BEq, so use [BEq α] [LawfulBEq α] [BEq β] [LawfulBEq β] instead of the DecidableEq assumptions. Eventually, this might become unnecessary though if Decidable was redefined such as in lean4#8309

[Paige Thomas]

Oh, ok. Thank you.