Syntactically-equal forms don't unify - how to disambiguate?

Stream: new members

[Jakob Kreuze]

I'm looking for some tips on figuring out what an identifier actually refers to - or help troubleshooting what I'm perceiving as shadowing, I guess. On line 216 of the attached file, I'm getting the following error:

tactic 'apply' failed, failed to unify
  List.elem x disj = true
with
  List.elem x disj = true

It looks like it should work... My goal state is the following:

disj : List AllOf
context : Request
h_no_match : ∀ (conj : AllOf), conj ∈ disj → AllOf.eval conj context ≠ MatchResult.is_match
h_indet : ∃ conj, conj ∈ disj ∧ AllOf.eval conj context = MatchResult.indeterminate
x : AllOf
hx : x ∈ disj ∧ AllOf.eval x context = MatchResult.indeterminate
a : List.isEmpty disj = false
h : ∀ (x : AllOf), x ∈ disj → ¬AllOf.eval x context = MatchResult.is_match
hx' : AllOf.eval x context = MatchResult.indeterminate
⊢ List.elem x disj = true

It seems like everything should be referring to the same x and the same disj, so I'm not sure what's going on. How would I figure out which x the goal is referring to? And how would I see if that x is the same as the x in hx?

If this looks like a bug, I can try a newer version of Lean and report back. I'm doing this in v4.2.0 right now.

reproducible.lean

[Eric Wieser]

To save people a download:

File contents

import Mathlib.Data.Prod.Basic

inductive MatchResult where
  | is_match      : MatchResult
  | no_match      : MatchResult
  | indeterminate : MatchResult
deriving DecidableEq, BEq, Repr

instance : LawfulBEq MatchResult where
  eq_of_beq := by sorry
  rfl := by sorry

inductive XmlType
  | string            : XmlType
  | boolean           : XmlType
  | integer           : XmlType
  | double            : XmlType
  | time              : XmlType
  | date              : XmlType
  | dateTime          : XmlType
  | anyURI            : XmlType
  | hexBinary         : XmlType
  | base64Binary      : XmlType
  | dayTimeDuration   : XmlType
  | yearMonthDuration : XmlType
  | x500Name          : XmlType
  | rfc822Name        : XmlType
  | ipAddress         : XmlType
  | dnsName           : XmlType
deriving DecidableEq, BEq, Repr

instance : LawfulBEq XmlType where
  eq_of_beq := by
    intros a b h
    induction a
    all_goals induction b
    all_goals
      first
      | rfl
      | contradiction
  rfl := by
    intro a
    induction a
    all_goals rfl

def Primitive : Type := XmlType × String
deriving DecidableEq, BEq, Repr

theorem Prod.beq_iff_fst_eq_snd_eq
  {α β : Type} [BEq α] [BEq β] [LawfulBEq α] [LawfulBEq β]
  (a b : α × β) :
  a == b  ↔ a.fst == b.fst ∧ a.snd == b.snd := by
  apply Iff.intro
  { simp_all only [beq_iff_eq]
    intro _
    trivial }
  { intro h
    simp_all only [beq_iff_eq, Prod.eq_iff_fst_eq_snd_eq] }

instance : LawfulBEq Primitive where
  eq_of_beq := by
    intros a b h
    rw [Prod.eq_iff_fst_eq_snd_eq]
    rw [Prod.beq_iff_fst_eq_snd_eq] at h
    simp [beq_iff_eq] at h
    assumption
  rfl := by
    intro a
    rw [Prod.beq_iff_fst_eq_snd_eq]
    apply And.intro
    all_goals simp

structure Bag where
  contents: List Primitive
deriving DecidableEq, Repr

def Bag.beq (b₁ b₂ : Bag) : Bool :=
  b₁.contents.all (fun x => b₂.contents.count x == b₁.contents.count x)

instance : BEq Bag where
  beq := Bag.beq

inductive Value where
  | primitive (p : Primitive) : Value
  | bag (b : Bag)             : Value
deriving DecidableEq, BEq, Repr

instance : Inhabited Value where
  default := Value.primitive (XmlType.boolean, "Indeterminate")

structure Attribute where
  category   : String
  identifier : String
  issuer     : Option String
  value      : Primitive
deriving DecidableEq, BEq, Repr

instance : LawfulBEq Attribute where
  eq_of_beq := by sorry
  rfl := by sorry

def Request : Type := List Attribute
deriving Repr

def Identifier : Type := String
deriving DecidableEq, BEq, Repr

structure AttributeDesignator where
  category        : String
  identifier      : String
  type            : XmlType
  issuer          : Option String
  must_be_present : Bool
deriving DecidableEq, BEq, Repr

structure Match where
  function   : Identifier
  designator : AttributeDesignator
  value      : Value
deriving DecidableEq, BEq, Repr

namespace Match
  def eval (m : Match) (context : Request) : Option Value :=
    match m with
      | Match.mk fn designator value =>
        match designator.eval context with
          | Sum.inl result =>
            let results := match result with
            | (Value.bag (Bag.mk attrs)) =>
              attrs.map fun attr =>
                let args := [value, Value.primitive attr]
                (Expression.apply fn args).eval context
            | (Value.primitive attr) =>
              let args := [value, Value.primitive attr]
              [(Expression.apply fn args).eval context]

            let results := results.map (fun (x : Option Value) => (x : Value))
            if results.elem (Value.primitive (#<XmlType.boolean, "True">)) then
              (Value.primitive (#<XmlType.boolean, "True">))
            else if results.elem (Value.primitive (#<XmlType.boolean, "Indeterminate">)) then
              (Value.primitive (#<XmlType.boolean, "Indeterminate">))
            else
              Value.primitive (#<XmlType.boolean, "False">)
          | Sum.inr status => Option.none
end Match

instance : LawfulBEq Match where
  eq_of_beq := by sorry
  rfl := by sorry

def AllOf  : Type := List Match
deriving DecidableEq, BEq, Repr

namespace AllOf
  def eval (conj : AllOf) (context : Request) : MatchResult :=
    let result := conj.map (fun x => x.eval context)
    let result := result.map (fun (x : Option Value) => x.get!)
    if result.all (fun x => x == Value.primitive (XmlType.boolean, "True")) then MatchResult.is_match
    else if result.all (fun x => x != Value.primitive (XmlType.boolean, "False")) ∧
            result.elem (Value.primitive (XmlType.boolean, "Indeterminate"))
         then MatchResult.indeterminate
    else MatchResult.no_match
end AllOf

instance : LawfulBEq AllOf where
  eq_of_beq := by sorry
  rfl := by sorry

def AnyOf  : Type := List AllOf
deriving DecidableEq, BEq, Repr

namespace AnyOf
  def eval (disj : AnyOf) (context : Request) : MatchResult :=
    if disj.isEmpty then MatchResult.is_match else
      let result := disj.map (fun x => x.eval context)
      if result.any (fun x => x == MatchResult.is_match) then MatchResult.is_match
      else if result.elem MatchResult.indeterminate then MatchResult.indeterminate
      else MatchResult.no_match
end AnyOf

instance : LawfulBEq AnyOf where
  eq_of_beq := by sorry
  rfl := by sorry

theorem helper { α β : Type } [BEq α] [LawfulBEq α] [BEq β] [LawfulBEq β] (x : α) (xs : List α) (f : α → β) :
  List.elem x xs → List.elem (f x) (List.map f xs) := by
  induction xs with
  | nil => simp
  | cons hd tl ih =>
    intro h
    simp [List.elem_cons] at *
    cases h with
    | inl h =>
      apply Or.intro_left
      exact congrArg f h
    | inr h =>
      apply Or.intro_right
      simp [List.contains] at *
      apply ih h

theorem table_1_target_match_table₂ (disj : List AllOf) (context : Request) :
    (∀ (conj : AllOf), conj ∈ disj → conj.eval context ≠ MatchResult.is_match)
  → (∃ (conj : AllOf), conj ∈ disj ∧ conj.eval context = MatchResult.indeterminate)
  → AnyOf.eval disj context = MatchResult.is_match := by
    intros h_no_match h_indet
    simp [AnyOf.eval]

    let ⟨x, hx⟩ := h_indet

    intros _ h
    have hbranch : List.elem MatchResult.indeterminate (List.map (fun x => AllOf.eval x context) disj) = true := by
      have hx' : AllOf.eval x context = MatchResult.indeterminate := by
        exact hx.right
      rw [←hx']
      apply helper x disj (fun y => y.eval context)
      apply List.elem_eq_true_of_mem hx.left

[Eric Wieser]

Can you tell us which line of the file you're talking about?

[Jakob Kreuze]

Very last one - apply List.elem_eq_true_of_mem hx.left. Line 216

[Eric Wieser]

It works for me without (that) issue in the web editor, which is using a very recently lean/mathlib version. Note that telling us the lean version isn't enough; if you import Mathlib, we need the mathlib commit to fully reproduce.

[Eric Wieser]

You can inspect what went wrong with your version by using set_option pp.explicit true before the lemma in question

[Eric Wieser]

Then the error should be clearer

[Jakob Kreuze]

I had mathlib pinned to v4.2.0.
Not exactly related, but which web editor is this? I didn't know there was one for Lean 4

[Eric Wieser]

image.png

[Jakob Kreuze]

Neat! Thank you

[Jakob Kreuze]

Looks like it works in Lean/mathlib v4.3.0 so maybe this is a bug that's since been fixed. Either way, this lets me get back to work. Appreciate the troubleshooting help

[Eric Rodriguez]

Does set_option pp.explicit true show the real cause? Or worst case, pp.all?

[Kyle Miller]

One good tool for debugging these unification issues is the convert tactic. It looks like that apply could have been an exact, and for a non-unifying exact what you do is use convert instead.

[Kyle Miller]

Either you get new goals showing what wasn't defeq to what, or convert magically solves the goal and, while you don't learn anything, at least the goal is solved.