CategoryTheory.Functor.FullyFaithful

Stream: mathlib4

[Matej Penciak]

I was hoping to help with the Category theory port effort, and it looks like most of the work is blocked by mathlib4#846 opened by @Richard Osborn .

I'm happy to help with the file if the help is welcome... I've fixed a couple of the errors, and made progress on a couple more.

[Moritz Doll]

I think there is no problem just editting if the file is sitting around for a month and has a 'help wanted' tag

[Scott Morrison]

Sorry, I've been busy with other things and feeling guilty I haven't looked at that.

[Scott Morrison]

From memory Richard indicated that aesop wasn't doing something that tidy used to, so you may need to experiment with powering up aesop (giving it access to more tactics or lemmas or whatever).

[Scott Morrison]

Please ping if you want more eyes!

[Matej Penciak]

I got the file to typecheck! There's still a lot of cleanup left to do, but I'll compile all the weird behaviors I encountered in this thread once I figure out what's going on...

[Scott Morrison]

Describing the weird behaviours as -- Porting note: ... or -- Porting note: TODO ... is good too. :-)

[Adam Topaz]

I took a quick look at this file. It seems that aesop_cat can't see that things like Function.Injective, Function.RightInverse, etc. are functions and that intros should be applied. At least aesop_cat succeeds if the Function.Injective and/or Function.RightInverse are unfolded first. What's the right approach here? How does one train aesop_cat to use intros (or to unfold) in such situations?

[Jannis Limperg]

aesop_cat (add norm unfold Function.Injective) if you want to unfold Injective at one particular Aesop call.

If you want to unfold Injective as a global rule, add @[aesop norm unfold] on Function.Injective. However, this is maybe too aggressive. For example, a rule Involutive -> Injective would not apply any more since Injective is unfolded first. I've had good experiences with this setup:

@[aesop safe forward]
theorem injective_elim (h₁ : Injective f) (h₂ : f a = f b) : a = b :=
  h₁ _ _ h₂

@[aesop 99%]
theorem injective_intro (h : ∀ a b, f a = f b → a = b) : Injective f :=
  h

If you have hypotheses h : Injective f and h' : f a = f b, the first rule will conclude a = b. If you have a target Injective f, the second rule will unfold Injective, but unsafely, thus giving other rules a chance to fire.

[Adam Topaz]

Thanks Jannis! What's the heuristic for that 99%? Does this mean the (unsafe) rule is applied 99% of the time or 1% of the time?

[Matej Penciak]

I haven't marked any of the lemmas in the file for Aesop. Is there a rough guideline for what kinds of lemmas would make for good Aesop lemmas?

[Richard Osborn]

Yea, the files should be complete other than aesop_cat and unfold_proj blocking them. The proofs can fairly easily be rewritten to work around the issues in the short term if you want to start porting subsequent files. I won’t have access to my computer until later tonight, but I can push new proofs while aesop_cat gets fixed and unfold_proj gets implemented. Also, feel free to work on the files. I only have a couple hrs each day to look into them.

[Matej Penciak]

I did some work on it last night, and the file is pretty much done at this point. Just some minor aesthetic issues with one of the proofs...

I think something that would be helpful is if someone more knowledgeable about how casts work in Lean 4 could check out what's going on at this porting note: https://github.com/leanprover-community/mathlib4/blob/60d4254544886e10cfc417aff29a3c6362b1a9c6/Mathlib/CategoryTheory/Functor/FullyFaithful.lean#L324 .

I was able to get around the issue manually, but it seemed like in the Lean 3 proof, Lean was far more willing to rewrite through casts...

[Adam Topaz]

I golfed this proof a little bit...

/-- “Divide” a functor by a faithful functor. -/
protected def Faithful.div (F : C ⥤ E) (G : D ⥤ E) [Faithful G] (obj : C → D)
    (h_obj : ∀ X, G.obj (obj X) = F.obj X) (map : ∀ {X Y}, (X ⟶ Y) → (obj X ⟶ obj Y))
    (h_map : ∀ {X Y} {f : X ⟶ Y}, HEq (G.map (map f)) (F.map f)) : C ⥤ D :=
  { obj, map := @map,
    map_id := by
      intros X
      apply G.map_injective
      apply eq_of_heq
      refine HEq.trans h_map ?_
      simp only [Functor.map_id]
      convert HEq.refl (𝟙 (F.obj X))
      all_goals { apply h_obj }
    map_comp := by
      intros X Y Z f g
      apply G.map_injective
      apply eq_of_heq
      refine HEq.trans h_map ?_
      simp only [Functor.map_comp]
      convert HEq.refl (F.map f ≫ F.map g)
      all_goals { try { apply h_obj } <;> apply h_map } }

[Adam Topaz]

I'm not really sure why casts showed up in the first place?

[Matej Penciak]

Oh that looks way better!

It is quite strange, the original proof could just call
transitive F.map (𝟙 X), but in Lean 4 it was failing to unify F.map (𝟙 X) with something that could be HEq with G.map (map (𝟙 X))

[Matej Penciak]

Could you push to the branch? I'm away from my computer for a few hours...

[Adam Topaz]

pushed!

[Adam Topaz]

Let me add back the porting note about the trans tactic, so we don't forget!

[Jannis Limperg]

Adam Topaz said:

Thanks Jannis! What's the heuristic for that 99%? Does this mean the (unsafe) rule is applied 99% of the time or 1% of the time?

The number is supposed to be a (very rough) estimate of the success probability of a rule. So "when you have an Injective target, how likely is it that this rule will lead to a proof?" Operationally, rules with higher success probability are tried first and the priority of the subgoals of a rule is the priority of the goal to which the rule was applied, multiplied with the success probability.

[Jannis Limperg]

Matej Penciak said:

I haven't marked any of the lemmas in the file for Aesop. Is there a rough guideline for what kinds of lemmas would make for good Aesop lemmas?

I tend to think not so much in terms of individual lemmas but in terms of proofs. So take some class of proofs that seems like they ought to be automatic and add the relevant lemmas as apply rules, if they should be applied to the target, or forward/destruct rules, if they should be used to generate new hypotheses. Equations should be registered as simp lemmas.

To get reasonable performance, you'll have to avoid these sorts of rules:

• Anything that sends Aesop into a loop, e.g. an apply rule that is applicable to one of its own premises. These rules can be useful as low-priority local rules, but generally not as global rules.
• Similarly, anything that introduces metavariables, e.g. exists-intro or transitivity rules, is better used as a local rule (if at all).
• apply rules with many premises on which Aesop can make progress but which don't ultimately lead to a proof.
• Too many forward rules in general, since the implementation of forward rules is currently a bit naive. (destruct is fine.)

Also, the rules should be in simp-normal form (as usual) since Aesop simps the whole goal before it does anything else.

A frequent source of tension is that while you build an API, you want rules that look through abstractions (e.g. unfold Injective) and when the API is built, you want rules that preserve abstractions. One way around this is to define a separate rule set for building the API; the other way is to add abstraction-breaking rules only locally. At some point I'll change the UI such that the rule set approach has less syntactic overhead.

[Adam Topaz]

I had another question while reviewing this PR. Consider the following:

/-- If `F` is full, and naturally isomorphic to some `F'`, then `F'` is also full. -/
def Full.ofIso [Full F] (α : F ≅ F') :
    Full F' where
  preimage {X Y} f := F.preimage ((α.app X).hom ≫ f ≫ (α.app Y).inv)
  witness f := by simp [←NatIso.naturality_1 α]
#align category_theory.full.of_iso CategoryTheory.Full.ofIso

theorem Faithful.of_iso [Faithful F] (α : F ≅ F') : Faithful F' :=
  { map_injective := fun h =>
      F.map_injective (by rw [← NatIso.naturality_1 α.symm, h, NatIso.naturality_1 α.symm]) }
#align category_theory.faithful.of_iso CategoryTheory.Faithful.of_iso

This does technically fit with out naming conventions since Functor.Full has data while Functor.Faithful is a prop-valued class. But the asymmetry in the names here seems quite bad to me!

[Adam Topaz]

My vote would be to use lower-camel-case for both names, and more generally for names of all instances, regardless of whether they are props or not! Thoughts?

[Johan Commelin]

Hmm, I think it's quite a useful feature that we can distinguish prop-vs-data using the naming convention.

[Matej Penciak]

This was a weird thing that came up in porting the file as well:

In writing the proof for Faithful.div , something about the parser for the structure syntax was bugging out and causing some issues. I've minimized it to the following MWE:

structure Foo where
  a : Nat
  b : Nat
  a_eq_b : a = b

def natToFoo (a : Nat) (bar : Foo) (h : a = bar.b) : Foo :=
  { a, b := bar.b,
    a_eq_b := by
      sorry
  }

When trying to fill in the sorry, the only way I can get the infoview to show my goals is to add a done at the end, otherwise it shows nothing.

[Matej Penciak]

This does not happen if instead I write

def natToFoo (a : Nat) (bar : Foo) (h : a = bar.b) : Foo :=
  { a := a, b := bar.b,
    a_eq_b := by
      sorry
  }

so it looks like it's something about the field init shorthand (which I actually didn't even know Lean had until I saw Faithful.div!)

[Kevin Buzzard]

Is that syntax definitely allowed? In my VS Code the a in a, b is blue, indicating that it's not a structure field.

[Kevin Buzzard]

example : Foo :=
  { a, b := 37, -- unknown identifier 'a'
    a_eq_b := by
      sorry
      done
  }

[Matej Penciak]

I'm not sure :grimacing:, but if you fill in the proof Lean doesn't complain, so I assumed it had something to do with this fancy thing I literally just read in the Rust book a couple days ago: https://doc.rust-lang.org/book/ch05-01-defining-structs.html#using-the-field-init-shorthand

[Matej Penciak]

My guess is that if a is in the context, and has the same name and type as a field in the structure you can just put it in.

[Matej Penciak]

def natToFoo (a : Nat) (b : Nat) (a_eq_b : a = b) : Foo :=
  { a, b, a_eq_b}

#eval natToFoo 2 2 rfl -- { a := 2, b := 2, a_eq_b := _ }

works

[Kevin Buzzard]

Oh I see! You weren't attempting to assign bar.b to a too? Sorry, I misunderstood that part.

def natToFoo (a : Nat) (bar : Foo) (h : a = bar.b) : Foo :=
  { a, b := bar.b,
    a_eq_b := by
      -- ⊢ a = bar.b
      sorry
  }

I see the goal if I put the cursor just before the s of sorry (which is something I do a lot).

[Matej Penciak]

Kevin Buzzard said:

Oh I see! You weren't attempting to assign bar.b to a too? Sorry, I misunderstood that part.

def natToFoo (a : Nat) (bar : Foo) (h : a = bar.b) : Foo :=
  { a, b := bar.b,
    a_eq_b := by
      -- ⊢ a = bar.b
      sorry
  }

I see the goal if I put the cursor just before the s of sorry (which is something I do a lot).

But if you delete the sorry and try to fill in the goal, there is nothing in the infoview

[Matej Penciak]

Oh actually this isn't as bad as I remembered, as long as there is even a single line in the proof something appears in the infoview...

[Kevin Buzzard]

Oh this is interesting: I always put a sorry at the end of a proof before I start working on it, so I had never noticed this phenomenon.

[Mario Carneiro]

this is the same issue that people were talking about done/qed in the other thread for: empty blocks are a syntax error and this breaks a lot of things

[Kevin Buzzard]

I see -- the issue is that the } just throws Lean into confusion because it was expecting a tactic.

[Adam Topaz]

Johan Commelin said:

Hmm, I think it's quite a useful feature that we can distinguish prop-vs-data using the naming convention.

This actually brings up another point. IMO Functor.Full could very well be made prop-valued. Anyone, one could certainly make an argument either way. What happens in the future, after the port is done, if we want to make Functor.Full Prop-valued? The current naming convention would probably make such a refactor more annoying.

This is not unprecedented. docs#category_theory.limits.has_limits used to contain data.

[Adam Topaz]

I would guess that such changes occur mostly for typeclasses. So if we choose a uniform naming convention for instances, that would eliminate the potential additional work (or at least most of it)

[Adam Topaz]

I should also mention that I'm not really invested in this suggestion. I'm sure I could get used to whatever convention we settle on. But j do think these things are worth discussing.

[Kevin Buzzard]

I was told by someone that in Isabelle/HOL they stick out the is_ convention for prop-valued typeclasses and if worked great

[Johan Commelin]

I think that with proper language server support, doing a global rename of something should be pretty easy. So I think Lean 4 will actually make this easier then it was in Lean 3.

[Adam Topaz]

Presumably the LSP could also detect which terms are proofs and which are data, and reflect that info in the editor in some way (e.g. text colour).

[Scott Morrison]

Back to the aesop issue, I think the more important question is why aesop is not doing the variable introduction when it sees an injective goal.

[Scott Morrison]

Is it not actually trying intro, but instead looking at the syntactical form of the goal?

[Scott Morrison]

If so, this should be changed (at least under an option).

[Scott Morrison]

We definitely don't want to be adding unsafe rules about unfolding Injective, I think.

[Jannis Limperg]

Aesop uses the MetaM equivalent of intros, which does not unfold Injective to discover the forall binders:

import Mathlib.Init.Function

example (f : α → β) : f.Injective := by
  -- ... ⊢ Function.Injective f
  intros
  -- ... ⊢ Function.Injective f
  intro _ _ _
  -- ... ⊢ a₁ = a₂
  sorry

I can change this of course, but I think the current behaviour is correct. If we eagerly unfold Injective and introduce its premises, rules like Involutive f -> Injective f will not work any more.

(Interestingly, the behaviour of intros does not change if we make Injective an abbrev.)

[Adam Topaz]

As Scott said, maybe we could add an option for aesop to be more aggressive with intros?

[Adam Topaz]

This port PR is holding up a bunch of category theory porting. Do we want to wait until we figure out what to do with aesop_cat before merging?

[Jannis Limperg]

Adam Topaz said:

As Scott said, maybe we could add an option for aesop to be more aggressive with intros?

Can be done, but what's wrong with the scheme I outlined above?

[Adam Topaz]

One issue I see is that it's not just Function.Injective but various other things like Function.RightInverse, etc. I suppose we would have to manually add intro/elim rules for all of these with this approach? Maybe @Scott Morrison had other issues in mind as well?

[Adam Topaz]

In any case, it seems that by adding an "aggressive intros" option to aesop, that could help aesop_cat cover more goals which are handled with tidy in mathlib3, and that would certainly be a great help in porting the category theory library!

[Jannis Limperg]

Yes, my scheme would require two rules per def. I'll implement the option and then you can see whether it works better for you.

[Adam Topaz]

Thanks Jannis! that would be very helpful!

[Jannis Limperg]

Sure, no problem!

[Jannis Limperg]

Implemented in 87a654a5a10f5edf3cfaee9052c08a4342b24179.

[Jannis Limperg]

The new option can be set with aesop (options := { introsTransparency := some .default }), which will cause intros to unfold definitions up to default transparency.

[Scott Morrison]

@Jannis Limperg, adding (options := { introsTransparency := some .default }) to the definition of aesop_cat causes previously working proofs in Mathlib.CategoryTheory.Category.Basic to instead use sorry!

[Scott Morrison]

Strangely this occurs for any value of introsTransparency, including none. Merely having the (options := { }) is fine.

[Scott Morrison]

Ah, all okay. It's introsTransparency?. Not sure why it is generating sorry rather than giving a good error message.

[Jannis Limperg]

Sorry about the error (edited for posterity). I've also changed the elaboration of (options := ) so that it throws an error instead of converting to sorry.