expects 'List.union = Union.union'

Stream: lean4

[Jared green]

why does it expect List.union = Union.union? what can be done about it?

import Init.Data.List
import Init.PropLemmas
import Mathlib.Algebra.BigOperators.Group.List
import Mathlib.Data.List.Dedup
import Mathlib.Data.List.Pairwise
import Mathlib.Data.List.Join
import Mathlib.Data.List.Basic
import Mathlib.Data.List.Defs
import Mathlib.Data.List.Infix
import Mathlib.Data.List.Lattice
import Mathlib.Data.List.Lemmas
import Mathlib.Data.Bool.AllAny
import Mathlib.Data.Bool.Basic
import Mathlib.Logic.Basic
import Batteries.Data.List.Lemmas
import Batteries.Data.List.Basic
import Aesop
open Classical

variable {α : Type}[h : DecidableEq α]
inductive normalizable α (pred : α -> Prop)
  where
  | atom : α -> (normalizable α pred)
  | And : (normalizable α pred) -> (normalizable α pred) -> normalizable α pred
  | Or : (normalizable α pred) -> (normalizable α pred) -> normalizable α pred
  | Not : normalizable α pred -> normalizable α pred
deriving DecidableEq

namespace normalizable


@[reducible]
def toProp (n : normalizable α pred) : Prop :=
  match n with
  | atom a => pred a
  | And a b =>  toProp a ∧ toProp b
  | Or a b => (toProp a) ∨ toProp b
  | Not i => ¬(toProp i)

@[simp]
theorem toProp_not : toProp (Not n₁) ↔ ¬ toProp n₁ := Iff.rfl

@[simp]
theorem toProp_and : toProp (And n₁ n₂) ↔ toProp n₁ ∧ toProp n₂ := Iff.rfl

@[simp]
theorem toProp_or : toProp (Or n₁ n₂) ↔ toProp n₁ ∨ toProp n₂ := Iff.rfl

@[simp]
theorem toProp_atom {a : α} : toProp (atom a : normalizable α pred) ↔ pred a := Iff.rfl

def wToProp (w : Bool × normalizable α pred) : Prop :=
  if w.fst then toProp w.snd else ¬(toProp w.snd)

def sToProp (s : List (Bool × normalizable α pred)) : Prop :=
  s.all (fun x => wToProp x)

def gToProp (g : List (List (Bool × normalizable α pred))) : Prop :=
  g.any (fun x => sToProp x)

def nToProp (n : List (List (List (Bool × normalizable α pred)))) : Prop :=
  n.all (fun x => gToProp x)

def fToProp (n : List (List (List (normalizable α pred)))) : Prop :=
  n.all (fun x => x.any (fun y => y.all (fun z => toProp z)))

def bcompatible (s : List (Bool × normalizable α pred)) (t : List (Bool × normalizable α pred)) : Bool :=
  s.all (fun x => t.all (fun y =>  x.snd == y.snd -> x.fst == y.fst))

theorem s_nodup : ∀ s : List (Bool × normalizable α pred), ((∀ w : Bool × normalizable α pred,∀ x : Bool × normalizable α pred, w ∈ s ∧ x ∈ s ->
  w.snd == x.snd -> w.fst == x.fst) ∧ s.Nodup) -> (s.map Prod.snd).Nodup :=
  by
  intro s hs
  obtain ⟨ hcond,hnodup⟩ := hs
  induction' s with hd tl ht
  simp [List.Nodup]
  unfold List.Nodup
  simp? --not this one
  sorry

def coherent (n : List (List (List (Bool × normalizable α pred)))) : Prop :=
  ∀ g : List (List (Bool × normalizable α pred)), g ∈ n ->
  ∀ s : List (Bool × normalizable α pred), s ∈ g ->
  (s.map Prod.snd).Nodup

theorem all_length_list (c : List a -> Prop): (∀ l : List a, c l) <-> (∀ n : Nat,∀ l:List a , l.length = n -> c l) :=
  by
  sorry

theorem c3 : ∀ n : List (List (List (Bool × normalizable α pred))),
             (coherent n ->
            ¬ (∃ g: List (List (Bool × normalizable α pred)), g ∈ n ∧
            ∃ s : List (Bool × normalizable α pred), s ∈ g ∧
            ∃ h : List (List (Bool × normalizable α pred)),h ∈ n ∧
            ((∃ w : Bool × normalizable α pred , w ∉ s ∧
            ∀ t ∈ h, bcompatible s t -> w ∈ t) ∨ ¬(∃ t ∈ h, bcompatible s t ))) ->
            (∀ g ∈ n, ∀ s ∈ g, ∃ t, List.Subset s t ∧ (t.map Prod.snd).Nodup ∧ (sToProp t -> nToProp n))) :=
  by
  --do induction over the length of n three times
  rw [ all_length_list (fun n => (coherent n ->
            ¬ (∃ g: List (List (Bool × normalizable α pred)), g ∈ n ∧
            ∃ s : List (Bool × normalizable α pred), s ∈ g ∧
            ∃ h : List (List (Bool × normalizable α pred)),h ∈ n ∧
            ((∃ w : Bool × normalizable α pred , w ∉ s ∧
            ∀ t ∈ h, bcompatible s t -> w ∈ t) ∨ ¬(∃ t ∈ h, bcompatible s t ))) ->
            (∀ g ∈ n, ∀ s ∈ g, ∃ t, List.Subset s t ∧ (t.map Prod.snd).Nodup ∧ (sToProp t -> nToProp n))) ) ]
  intro m
  induction' m with m ih
  sorry
  clear ih
  induction' m with m' ih
  sorry
  clear ih
  induction' m' with m'' ih
  intro n hn
  simp at hn
  intro hcoh hneg
  push_neg at hneg
  cases' n with g1 n1
  contradiction
  cases' n1 with g2 n2
  simp at hn
  simp at hn
  rw [hn]
  rw [hn] at hneg
  intro g hg
  have hhg : g = g1 ∨ g = g2 := by {
   sorry
  }
  cases' hhg with hg1 hg2
  intro s hs
  have hhs : s ∈ g1 := by {
    sorry
  }
  have hcompat := hneg g hg s hs g2 (by simp)
  obtain ⟨ _,t,ht,hcompat⟩ := hcompat
  use (s.union t)
  constructor
  intro x hx
  convert List.mem_union_left hx t

[Ruben Van de Velde]

I would suggest you try to minimise the code you're asking us to look at. Possibly the last four lines of the proof are relevant

[Jared green]

yes.

[Jared green]

it is now minimized.

[Damiano Testa]

Opening the above in the online server, the first error that I see is on line 32. Since there are quite a few other lines below that, I do not imagine that you are asking about that, right?

[Jared green]

try it again

[Damiano Testa]

I suspect that Lean's autoImplicit are producing confusing errors: bcompatible is not something that has been defined, so Lean treats it as a new variable, but it cannot take inputs. If you use

set_option autoImplicit false

you will likely get better error messages.

[Jared green]

try it again

[Damiano Testa]

If you use

  convert List.mem_union_left hx t using 1
  congr

you will see that there is an issue with instBEqProd = instBEqOfDecidableEq. This could be a problem arising from the presence of explicit Decidable assumptions and open Classical.

[Ruben Van de Velde]

Isn't that the long standing core issues about DecidableEq and BEq?