Swapping iff direction causes type error

Stream: new members

[Snir Broshi]

#mwe:

theorem foo₁ {α : Type} {P : α × α → Prop} {p : α × α} : P p ↔ p.fst = p.snd := sorry
theorem foo₂ {α : Type} {P : α × α → Prop} {a b : α} : P ⟨a, b⟩ ↔ a = b := foo₁
theorem bar₁ {α : Type} {P : α × α → Prop} {p : α × α} : p.fst = p.snd ↔ P p := sorry
theorem bar₂ {α : Type} {P : α × α → Prop} {a b : α} : a = b ↔ P ⟨a, b⟩ := bar₁

The ₁ theorems accept a product type, while the ₂ theorems accept both components separately, and give the same statement as if one passed in a product type to the ₁ theorems: a = b instead of p.fst = p.snd.
The bar theorems are exactly the foo theorems but with the iff direction swapped.

I expected either both ₂ theorems to work or both to fail, but how is only the foo version working?

[Ruben Van de Velde]

All I can say is "Huh"

[Aaron Liu]

Unification goes from left to right

[Aaron Liu]

So with foo we get first ?p =?= (a, b) which unifies ?p := (a, b) and then we get a =?= (a, b).fst and b =?= (a, b).snd which both work

[Aaron Liu]

but with bar we get first a =?= Prod.fst ?p which gets stuck

[Aaron Liu]

that's my guess

[Aaron Liu]

set_option trace.Meta.isDefEq true

theorem foo₁ {α : Type} {P : α × α → Prop} {p : α × α} : P p ↔ p.fst = p.snd := sorry
/-
[Meta.isDefEq] ✅️ P (a, b) ↔ a = b =?= ?m.5 ?m.6 ↔ Prod.fst ?m.6 = Prod.snd ?m.6 ▼
  [] ✅️ P (a, b) =?= ?m.5 ?m.6 ▼
    [] P (a, b) [nonassignable] =?= ?m.5 ?m.6 [assignable]
    [foApprox] ?m.5 [?m.6] := P (a, b)
    [] ✅️ ?m.6 =?= (a, b) ▼
      [] ?m.6 [assignable] =?= (a, b) [nonassignable]
      [] ✅️ ?m.4 × ?m.4 =?= α × α ▶
    [] ✅️ ?m.5 =?= P ▼
      [] ?m.5 [assignable] =?= P [nonassignable]
      [] ✅️ α × α → Prop =?= α × α → Prop ▶
  [] ✅️ a = b =?= (a, b).fst = (a, b).snd ▶
[Meta.isDefEq] ✅️ P (a, b) ↔ (a, b).fst = (a, b).snd =?= P (a, b) ↔ a = b ▶
-/
theorem foo₂ {α : Type} {P : α × α → Prop} {a b : α} : P ⟨a, b⟩ ↔ a = b := foo₁
theorem bar₁ {α : Type} {P : α × α → Prop} {p : α × α} : p.fst = p.snd ↔ P p := sorry
/-
[Meta.isDefEq] ❌️ a = b ↔ P (a, b) =?= Prod.fst ?m.6 = Prod.snd ?m.6 ↔ ?m.5 ?m.6 ▼
  [] ❌️ a = b =?= Prod.fst ?m.6 = Prod.snd ?m.6 ▼
    [] ✅️ α =?= ?m.4 ▶
    [] ❌️ a =?= Prod.fst ?m.6 ▼
      [] ❌️ a =?= ?m.6.1 ▼
        [onFailure] ❌️ a =?= ?m.6.1 ▼
          [stuckMVar] found stuck MVar ?m.6 : α × α
    [onFailure] ❌️ a = b =?= Prod.fst ?m.6 = Prod.snd ?m.6
    [onFailure] ❌️ a = b =?= Prod.fst ?m.6 = Prod.snd ?m.6
  [onFailure] ❌️ a = b ↔ P (a, b) =?= Prod.fst ?m.6 = Prod.snd ?m.6 ↔ ?m.5 ?m.6
  [onFailure] ❌️ a = b ↔ P (a, b) =?= Prod.fst ?m.6 = Prod.snd ?m.6 ↔ ?m.5 ?m.6
[Meta.isDefEq] ❌️ Prod.fst ?m.6 = Prod.snd ?m.6 ↔ ?m.5 ?m.6 =?= a = b ↔ P (a, b) ▼
  [] ❌️ Prod.fst ?m.6 = Prod.snd ?m.6 =?= a = b ▼
    [] ✅️ ?m.4 =?= α ▶
    [] ❌️ Prod.fst ?m.6 =?= a ▼
      [] ❌️ ?m.6.1 =?= a ▼
        [onFailure] ❌️ ?m.6.1 =?= a ▼
          [stuckMVar] found stuck MVar ?m.6 : α × α
    [onFailure] ❌️ Prod.fst ?m.6 = Prod.snd ?m.6 =?= a = b
    [onFailure] ❌️ Prod.fst ?m.6 = Prod.snd ?m.6 =?= a = b
  [onFailure] ❌️ Prod.fst ?m.6 = Prod.snd ?m.6 ↔ ?m.5 ?m.6 =?= a = b ↔ P (a, b)
  [onFailure] ❌️ Prod.fst ?m.6 = Prod.snd ?m.6 ↔ ?m.5 ?m.6 =?= a = b ↔ P (a, b)
etc. etc.
-/
theorem bar₂ {α : Type} {P : α × α → Prop} {a b : α} : a = b ↔ P ⟨a, b⟩ := bar₁

[Snir Broshi]

Very cool, thank you! Followup question: can unification be modified to handle structure projections by calling the constructor? e.g. make a =?= Prod.fst ?m.6 conclude that ?m.6 is Prod.mk a ?m.7

[Snir Broshi]

of course structures that contain proofs will probably have unresolved metavariables for the proofs at the end of unification, but it sounds like it should work fine for structures which are only data

[Snir Broshi]

Both of these work, and I think it makes sense as a default "guess" for unification

theorem bar₂ {α : Type} {P : α × α → Prop} {a b : α} : a = b ↔ P ⟨a, b⟩ := bar₁ (p := ⟨_, _⟩)

theorem bar₂ {α : Type} {P : α × α → Prop} {a b : α} : a = b ↔ P ⟨a, b⟩ := bar₁ (p := Prod.mk ..)

[Robin Arnez]

If you define foo₂ and bar₂ first then unification has no problems:

theorem foo₂ {α : Type} {P : α × α → Prop} {a b : α} : P ⟨a, b⟩ ↔ a = b := sorry
theorem bar₂ {α : Type} {P : α × α → Prop} {a b : α} : a = b ↔ P ⟨a, b⟩ := sorry

theorem foo₁ {α : Type} {P : α × α → Prop} {p : α × α} : P p ↔ p.fst = p.snd := foo₂
theorem bar₁ {α : Type} {P : α × α → Prop} {p : α × α} : p.fst = p.snd ↔ P p := bar₂

So I'd say, if you can decide between one of the variants, then I'd use the foo₂ and bar₂ ones and not the foo₁ and bar₁ ones

[Aaron Liu]

Normally we should have both, right?

[Aaron Liu]

Or rather, we should have a curried P a b version and a product P p version

[Snir Broshi]

Well the mwe is about docs#Prod but my actual statement is about docs#SimpleGraph.Dart. I do plan to include both statements, I think both versions are useful even though they're defeq