Equality of structures with autoparams

Stream: mathlib4

[Yakov Pechersky]

This is part of porting Order.Basic. Consider:

def Function.Injective (f : α → β) : Prop := ∀ ⦃a₁ a₂⦄, f a₁ = f a₂ → a₁ = a₂

class Preorder (α : Type u) extends LE α, LT α :=
(le_refl : ∀ a : α, a ≤ a)
(le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c)
(lt := λ a b => a ≤ b ∧ ¬ b ≤ a)
(lt_iff_le_not_le : ∀ a b : α, a < b ↔ (a ≤ b ∧ ¬ b ≤ a) := by intros; rfl)

theorem Preorder.toLE_injective {α : Type _} : Function.Injective (@Preorder.toLE α) :=
  /-
  fun A B h => by
  cases A
  cases B
  injection h with h_le
  have : A_lt = B_lt := by
    funext a b
    dsimp [(· ≤ ·)] at A_lt_iff_le_not_le B_lt_iff_le_not_le h_le
    simp [A_lt_iff_le_not_le, B_lt_iff_le_not_le, h_le]
  congr
  -/
  fun A B h => match A, B with
  | { lt := A_lt, le := A_le, lt_iff_le_not_le := Ah, .. },
    { lt := B_lt, le := B_le, lt_iff_le_not_le := Bh, .. } => by
    cases h
    have : A_lt = B_lt := by
      funext a b
      show (LT.mk A_lt).lt a b = (LT.mk B_lt).lt a b
      simp [*]
    congr
    -- @HEq (autoParam (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) _auto✝) Ah (autoParam (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) _auto✝) Bh : Prop
    -- how does one solve such a HEq goal? why does it appear here but not in mathlib3

[Yakov Pechersky]

I've commented out the proof that mathport tries to construct. It doesn't work because it relies on unhygienic names, and I think the behavior of the injection tactic has also changed.

[Gabriel Ebner]

Can you try to minimize this a bit? From what I can tell any autoParam should trigger the issue. I wouldn't be surprised if this was an accidental change in congr where in Lean 3 we would unfold auto_param (and then there is no dependent argument anymore that prevents us from applying congr).

[Yakov Pechersky]

Ah...

def Function.Injective (f : α → β) : Prop := ∀ ⦃a₁ a₂⦄, f a₁ = f a₂ → a₁ = a₂

class Preorder (α : Type u) extends LE α, LT α :=
(le_refl : ∀ a : α, a ≤ a)
(le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c)
(lt := λ a b => a ≤ b ∧ ¬ b ≤ a)
(lt_iff_le_not_le : ∀ a b : α, a < b ↔ (a ≤ b ∧ ¬ b ≤ a) := by intros; rfl)

theorem Preorder.toLE_injective {α : Type _} : Function.Injective (@Preorder.toLE α) :=
  fun A B h => match A, B with
  | { lt := A_lt, .. }, { lt := B_lt, ..} => by
    cases h
    have : A_lt = B_lt := by
      funext a b
      show (LT.mk A_lt).lt a b = (LT.mk B_lt).lt a b
      simp [*]
    cases this
    congr

[Yakov Pechersky]

that proves it

[Yakov Pechersky]

Not sure if this example is what you were hoping for:

structure Foo where
  val : Nat := 0
  proof : val = 0 := by rfl

example (A B : Foo) : A = B := by
  congr -- no change, is that expected?
  sorry

example (A B : Foo) : A = B := by
  cases A
  cases B
  congr
  simp [*]

[Yakov Pechersky]

Maybe this is what you meant?

structure Foo where
  val : Nat := 0
  val2 : Nat := val + 1
  proof : val = 0 := by rfl

example (A B : Foo) : A = B := by
  congr -- no change, is that expected?
  sorry

example (A B : Foo) : A = B := by
  cases A
  cases B
  congr
  simp [*]
  sorry -- no idea how to proceed

[Gabriel Ebner]

Your first example works for me (I don't see any autoParam goals). The second example can't work (because A = B is not true in general).

[Yakov Pechersky]

Ah right.

[Yakov Pechersky]

So you want an example that specifically brings up an HEq (autoParam _) (autoParam _)?

[Gabriel Ebner]

That would be great!

[Yakov Pechersky]

I'm having some trouble finding a good example that doesn't fall into just an Eq goal

[Yakov Pechersky]

This is as minimal as I could get it

class Preorder (α : Type u) extends LT α :=
(le : α → α → Prop)
(lt_iff_le_not_le : ∀ a b : α, lt a b ↔ (le a b ∧ ¬ le b a) := by intros; rfl)

theorem Preorder.toLE_injective {α : Type _} (A B : Preorder α) (h : A.le = B.le) : A = B :=
  match A, B with
  | { lt := A_lt, le := A_le, lt_iff_le_not_le := Ah, .. },
    { lt := B_lt, le := B_le, lt_iff_le_not_le := Bh, .. } => by
    cases h
    have : A_lt = B_lt := by
      funext a b
      show (LT.mk A_lt).lt a b = (LT.mk B_lt).lt a b
      simp [*]
    congr

[Gabriel Ebner]

Simplified a bit and filed as #1808.

[Yakov Pechersky]

Thanks, it gets worse for

theorem LinearOrder.toPartialOrder_injective {α : Type _} :
    Function.Injective (@LinearOrder.toPartialOrder α) :=

because of the necessity to match up min and max