logic.equiv.basic mathlib4#631

Stream: mathlib4

[Scott Morrison]

We're very close on logic.equiv.basic.

[Scott Morrison]

The remaining problem is the simpNF linter is unhappy with lemmas like:

theorem sumCompl_apply_symm_of_pos (p : α → Prop) [DecidablePred p] (a : α) (h : p a) :
    (sumCompl p).symm a = Sum.inl ⟨a, h⟩ :=
  dif_pos h

[Scott Morrison]

It doesn't explain why, and just says you'll have to debug it yourself.

[Scott Morrison]

The current PR has just removed the @[simp] on this lemma (and three others like it), but I'm as yet unconvinced.

[Scott Morrison]

As long as simp can prove p a itself, it seems this is a perfectly reasonable simp lemma.

[Scott Morrison]

Or am I forgetting that something about simp has changed in Lean 4, and it is less aggressive about solving side-conditions?

[Mario Carneiro]

can you make a MWE version (no mathlib)?

[Scott Morrison]

import Std.Tactic.Lint

protected def Sum.elim {α β γ : Sort _} (f : α → γ) (g : β → γ) : Sum α β → γ :=
  fun x => Sum.casesOn x f g

structure Equiv (α : Sort _) (β : Sort _) where
  toFun : α → β
  invFun : β → α

infixl:25 " ≃ " => Equiv

namespace Equiv

instance : CoeFun (α ≃ β) fun _ => α → β := ⟨toFun⟩

protected def symm (e : α ≃ β) : β ≃ α := ⟨e.invFun, e.toFun⟩

def sumCompl {α : Type _} (p : α → Prop) [DecidablePred p] :
    Sum { a // p a } { a // ¬p a } ≃ α where
  toFun := Sum.elim Subtype.val Subtype.val
  invFun a := if h : p a then Sum.inl ⟨a, h⟩ else Sum.inr ⟨a, h⟩

@[simp]
theorem sumCompl_apply_symm_of_pos (p : α → Prop) [DecidablePred p] (a : α) (h : p a) :
    (sumCompl p).symm a = Sum.inl ⟨a, h⟩ :=
  dif_pos h

#lint
/- The `simpNF` linter reports:
SOME SIMP LEMMAS ARE NOT IN SIMP-NORMAL FORM.
see note [simp-normal form] for tips how to debug this.
https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20form -/
#check @sumCompl_apply_symm_of_pos /- Left-hand side does not simplify.
You need to debug this yourself using `set_option trace.Meta.Tactic.simp.rewrite true` -/

[Kevin Buzzard]

example (p : α → Prop) [DecidablePred p] (a : α) (h : p a) :
    (sumCompl p).symm a = Sum.inl ⟨a, h⟩ := by simp -- fails :-(

I can't even make set_option trace.Meta.Tactic.simp.rewrite true do anything. Where am I supposed to be writing this and/or looking at the output?

[Mario Carneiro]

The error message is saying that simp does not rewrite with the simp lemma

[Mario Carneiro]

so set_option trace.Meta.Tactic.simp.rewrite true will predictably be empty

[Mario Carneiro]

fixed in 68581a4

[Scott Morrison]

Oh, it is saying that it can't simplify the LHS, even using the simp lemma itself? I assumed it was about not simplifying with other simp lemmas.

[Mario Carneiro]

not simplifying with other simp lemmas is the good case

[Mario Carneiro]

simp lemma LHSs should not simplify when using everything else in the simp set, and they should simplify when using the simp lemma itself

[Scott Morrison]

Could we change the error message for when they do not simplify when using the simp lemma itself?

[Scott Morrison]

To be explicit that this is the test that is failing? I missed that in this case.

[Scott Morrison]

Weird,

@[simp] theorem coe_fn_mk (f : α → β) (g l r) : (Equiv.mk f g l r : α → β) = f :=
rfl

was omitted in Logic.Equiv.Defs...

[Kevin Buzzard]

Where is this simp lemma supposed to find h by the way?

[Mario Carneiro]

it's a conditional rewrite rule, it would normally be proved by recursive application of simp, possibly including hypotheses passed to the original invocation

[Mario Carneiro]

the bug here was that it failed to detect that this was a conditional rewrite rule

[Scott Morrison]

Okay, Logic.Equiv.Basic now compiles and lints locally.

[Scott Morrison]

Review would be great.

[Scott Morrison]

Hmm, we're not there yet. My fixes for duplicate Coe instances in Logic.Equiv.Defs has broken things in other places.

[Scott Morrison]

in Order.Monotone,

@[simp]
theorem monotone_toDual_comp_iff : Monotone (toDual ∘ f) ↔ Antitone f :=
  Iff.rfl

is now failing with

type mismatch
  Iff.rfl
has type
  Monotone (FunLike.coe toDual ∘ f) ↔ Monotone (FunLike.coe toDual ∘ f) : Prop
but is expected to have type
  Monotone (FunLike.coe toDual ∘ f) ↔ Antitone f : Prop

I neither understand why the FunLike.coe is printing here, nor why Iff.rfl doesn't work... :-(

[Mario Carneiro]

I think the FunLike.coe printing might be because it is an under-application? Can you make a MWE? (I think functions with the right arity and implicitness for FunLike.coe and toDual should suffice)

[Mario Carneiro]

for the iff.rfl proof it might help to look at set_option trace.Meta.isDefEq true

[Mario Carneiro]

@Scott Morrison I took a look at this issue, and the reason the iff.rfl proof fails is because Monotone has inferred the original order on beta, not the dual one

[Scott Morrison]

:racecar:, yes

[Scott Morrison]

Curiously before I took away the duplicate Coe instance for Equiv, this proof was working.

[Scott Morrison]

Perhaps because the duplicate one was not a coercion to a dependently typed function.

[Scott Morrison]

And this made it easier for Lean to get the type right?

[Scott Morrison]

I can add type ascriptions, but it feels like a work-around rather than a solution.

[Scott Morrison]

Could we have a higher priority CoeFun for FunLikes indexed by a constant type family?

[Mario Carneiro]

MWE:

class MyFunLike (F : Sort _) (β : outParam <| Nat → Sort _) where
  coe : F → ∀ a, β a

inductive Secret
def Wrapper := Secret
inductive Bla | z
instance : MyFunLike Bla (fun _ => Wrapper) := sorry

instance (priority := 100) {F β} [MyFunLike F β] :
  CoeFun F fun _ => ∀ a : Nat, β a where coe := MyFunLike.coe

#check Bla.z 0 -- MyFunLike.coe Bla.z 0 : (fun x => Wrapper) 0
set_option trace.Meta.isDefEq true in
#check Bla.z ∘ id -- MyFunLike.coe Bla.z ∘ id : ℤ → Secret

[Scott Morrison]

So you think this is something that should be fixed in core?

[Mario Carneiro]

yes, there is at least one core bug here

[Scott Morrison]

In mathlib4#631, I have just worked around this issue for now (and left a note pointing to this thread).

[Scott Morrison]

Shall I post your MWE as a Lean 4 issue, or is it still in your court?

[Scott Morrison]

Separately, mathlib4#631 now has a green tick, so if someone would like to have a look and/or merge that would be great.

[Kevin Buzzard]

(looking now)

[Scott Morrison]

@Kevin Buzzard, @Eric Rodriguez, @Ruben Van de Velde, thanks for all the review comments. Would you mind, where possible, just making the changes? It's twice as much work to have conversations about things.

[Kevin Buzzard]

I'll make my changes, all of which are trivial.

[Scott Morrison]

Thanks.

[Ruben Van de Velde]

I'll deal with min now, unless you already started, @Scott Morrison

[Scott Morrison]

I think I got them.

[Scott Morrison]

Here's the #mwe extracted from this branch:

notation:arg "⟦" a "⟧" => Quotient.mk _ a

namespace Function

def LeftInverse (g : β → α) (f : α → β) : Prop := ∀ x, g (f x) = x

def RightInverse (g : β → α) (f : α → β) : Prop := LeftInverse f g

theorem hfunext {α α': Sort u} {β : α → Sort v} {β' : α' → Sort v} {f : ∀a, β a} {f' : ∀a, β' a}
  (hα : α = α') (h : ∀a a', HEq a a' → HEq (f a) (f' a')) : HEq f f' := by
  subst hα
  have : ∀a, HEq (f a) (f' a) := λ a => h a a (HEq.refl a)
  have : β = β' := by funext a
                      exact type_eq_of_heq (this a)
  subst this
  apply heq_of_eq
  funext a
  exact eq_of_heq (this a)

end Function

namespace Subtype
variable {α β γ : Sort _} {p q : α → Prop}

protected theorem ext : ∀ {a1 a2 : { x // p x }}, (a1 : α) = (a2 : α) → a1 = a2
  | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl

theorem ext_val {a1 a2 : { x // p x }} : a1.1 = a2.1 → a1 = a2 :=
  Subtype.ext

end Subtype

open Function

structure Equiv (α : Sort _) (β : Sort _) where
  toFun : α → β
  invFun : β → α
  left_inv : LeftInverse invFun toFun
  right_inv : RightInverse invFun toFun

infixl:25 " ≃ " => Equiv

def subtypeQuotientEquivQuotientSubtype (p₁ : α → Prop) [s₁ : Setoid α] [s₂ : Setoid (Subtype p₁)]
    (p₂ : Quotient s₁ → Prop) (hp₂ : ∀ a, p₁ a ↔ p₂ ⟦a⟧)
    (h : ∀ x y : Subtype p₁, @Setoid.r _ s₂ x y ↔ (x : α) ≈ y) :
    { x // p₂ x } ≃ Quotient s₂ where
  toFun a :=
    Quotient.hrecOn a.1 (fun a h => ⟦⟨a, (hp₂ _).2 h⟩⟧)
      (fun a b hab => hfunext (by rw [Quotient.sound hab]) fun h₁ h₂ _ =>
        heq_of_eq (Quotient.sound ((h _ _).2 hab)))
      a.2
  invFun a :=
    Quotient.liftOn a (fun a => (⟨⟦a.1⟧, (hp₂ _).1 a.2⟩ : { x // p₂ x })) fun a b hab =>
      Subtype.ext_val (Quotient.sound ((h _ _).1 hab))
  -- This fails (but worked in Lean 3), but the next line using `rcases` succeeds:
  left_inv := fun ⟨a, ha⟩ => Quotient.inductionOn a (fun b hb => rfl) ha
  -- Needs `import Std.Tactic.RCases`:
  -- left_inv t := by rcases t with ⟨a, ha⟩; exact Quotient.inductionOn a (fun b hb => rfl) ha
  right_inv a := Quotient.inductionOn a fun ⟨a, ha⟩ => rfl

[Scott Morrison]

(Sorry, it's not super minimal...)

[Scott Morrison]

Unless someone has an idea I will post an issue on the Lean 4 repository. If anyone wants to further minimise first, that would be great.

[Scott Morrison]

For now I'll just put a link to this message at the regression in mathlib4#631, but let's not otherwise wait.

[Kyle Miller]

I think in that MWE that left_inv t is meant to be left_inv

[Kyle Miller]

I tried using intro with a pattern match, and it creates two goals. I used Quotient.sound to handle one of them, but then it lead to there being an error on a random other line...

def subtypeQuotientEquivQuotientSubtype (p₁ : α → Prop) [s₁ : Setoid α] [s₂ : Setoid (Subtype p₁)]
    (p₂ : Quotient s₁ → Prop) (hp₂ : ∀ a, p₁ a ↔ p₂ ⟦a⟧)
    (h : ∀ x y : Subtype p₁, @Setoid.r _ s₂ x y ↔ (x : α) ≈ y) :
    { x // p₂ x } ≃ Quotient s₂ where
  toFun a :=
    Quotient.hrecOn a.1 (fun a h => ⟦⟨a, (hp₂ _).2 h⟩⟧)
      (fun a b hab => hfunext (by rw [Quotient.sound hab]) fun h₁ h₂ _ => -- why is there now an error on `rw`??
        heq_of_eq (Quotient.sound ((h _ _).2 hab)))
      a.2
  invFun a :=
    Quotient.liftOn a (fun a => (⟨⟦a.1⟧, (hp₂ _).1 a.2⟩ : { x // p₂ x })) fun a b hab =>
      Subtype.ext_val (Quotient.sound ((h _ _).1 hab))
  left_inv := --fun ⟨a, ha⟩ => Quotient.inductionOn a (fun b hb => rfl) ha
    -- Workaround:
    by
      intro ⟨a, ha⟩
      · simp [Quotient.sound hab]
      exact Quotient.inductionOn a (fun b hb => rfl) ha
  right_inv a := Quotient.inductionOn a fun ⟨a, ha⟩ => rfl

[Gabriel Ebner]

I think this is a just a typical elaboration order / metavariables not instantiated yet kind of issue. If you insert a by exact after left_inv it works.