seemingly equal terms are not considered equal

Stream: new members

[One Happy Fellow]

hi all!

I'm proving a lemma about HashSets and I came across an error which roughly says "expected type X but the type is X". I understand this is most likely about different type class instances both sides are using but I cannot figure out what's going on (and set_option pp.all true output it too cryptic to me).

I've tried minimising the example but failed. The problematic error shows up at simpa using hlast line, error being:

Type mismatch: After simplification, term
  hlast
 has type
  @Membership.mem α (HashSet α) HashSet.instMembership s[↑i] x
but is expected to have type
  @Membership.mem α (HashSet α) HashSet.instMembership s[↑i] x

Here's the lemma. Thank you for help!

import Mathlib
open Std

def Array.foldl_0_len
  (l : Array α)
  (init : β)
  (f : β → α → β)
  : Array.foldl f init l 0 0 = init := by
  sorry

variable {α : Type} [BEq α]  [Hashable α]

def HashSet.mem_of_big_union
  (x : α)
  (s : Array (HashSet α))
  (h : x ∈ s.foldl (· ∪ ·) ∅)
  : ∃ (i : ℕ) (_ : i < s.size), x ∈ s[i] := by
  let union : HashSet α := s.foldl (· ∪ ·) ∅
  have : ∃ (i : ℕ) (_ : i < s.size), x ∈ s[i] := by
    suffices ∃ (i : ℕ) (_ : i < s.size), s.size ≤ s.size → x ∈ s[i] by grind
    apply Array.foldl_induction
      (as := s)
      (motive := λ n set =>
        x ∈ s.foldl (· ∪ ·) ∅ 0 n →
          ∃ (i : ℕ) (_ : i < n), (hb : n ≤ s.size) → x ∈ s[i]'?_)
      (init := ∅)
      (f := (· ∪ ·))
      (h0 := ?h0)
      (hf := ?hf)
    · assumption
    · intro inEmpty
      rw [Array.foldl_0_len] at inEmpty
      simp at inEmpty
    · intro i b ih hinfold
      if hlast : x ∈ s[i]
      then
        exists i
        exists ?_; omega
        intro _
        simpa using hlast
      else
        sorry
    omega
  assumption

[Markus Himmel]

Can you make an #mwe? The code is missing import and open statements and it uses the undefined lemma Array.foldl_0_len.

[One Happy Fellow]

apologies, I have edited the code snipped in my original post

[Etienne Marion]

convert hlast works.

[Etienne Marion]

simpa works too.

[One Happy Fellow]

thank you! i'm still struggling to understand what the original error was about and why convert hlast works?

[Etienne Marion]

apply hlast also works.

[Markus Himmel]

The problem is that there is a metavariable in one of the proofs that i is in bounds, because that goal from Array.foldl_induction only comes later. If you solve that goal first, it works:

import Mathlib
open Std

def Array.foldl_0_len
  (l : Array α)
  (init : β)
  (f : β → α → β)
  : Array.foldl f init l 0 0 = init := by
  sorry

variable {α : Type} [BEq α]  [Hashable α]

--set_option pp.all true

def HashSet.mem_of_big_union
  (x : α)
  (s : Array (HashSet α))
  (h : x ∈ s.foldl (· ∪ ·) ∅)
  : ∃ (i : ℕ) (_ : i < s.size), x ∈ s[i] := by
  let union : HashSet α := s.foldl (· ∪ ·) ∅
  have : ∃ (i : ℕ) (_ : i < s.size), x ∈ s[i] := by
    suffices ∃ (i : ℕ) (_ : i < s.size), s.size ≤ s.size → x ∈ s[i] by grind
    apply Array.foldl_induction
      (as := s)
      (motive := λ n set =>
        x ∈ s.foldl (· ∪ ·) ∅ 0 n →
          ∃ (i : ℕ) (_ : i < n), (hb : n ≤ s.size) → x ∈ s[i]'?_)
      (init := ∅)
      (f := (· ∪ ·))
      (h0 := ?h0)
      (hf := ?hf)
    rotate_right
    · omega
    · assumption
    · intro inEmpty
      rw [Array.foldl_0_len] at inEmpty
      simp at inEmpty
    · intro i b ih hinfold
      if hlast : x ∈ s[i]
      then
        exists i
        refine ⟨by omega, ?_⟩
        intro _
        simpa using hlast
      else
        sorry
  assumption

[Etienne Marion]

(deleted)

[Markus Himmel]

It's certainly a very unintuitive behavior. Essentially only tactics that can apply proof irrelevance to unify the two proofs are able to close the goal, and exact (and therefore simpa using) do not do this. I'm pretty sure I was involved in a discussion on the Lean issue tracker about a very similar issue, but I can't find it right now.

[Chris Henson]

Interesting to note, grind gives an error message somewhere on the spectrum from helpful to interesting:

Tactic grind failed: the goal mentions the declaration mem_of_big_union, which is being defined. To avoid circular reasoning, try rewriting the goal to eliminate mem_of_big_union before using grind.

[Chris Henson]

@One Happy Fellow Did you intend for the second quantification in your goal to be existential?

[One Happy Fellow]

@Chris Henson I did not, that's just a late night mistake :oops:

[Eric Wieser]

As an aside, I'd argue this is a bad induction principle, and it should have (motive : (n : ℕ) → n ≤ as.size → β → Prop)