Making a proof term reduce(rewritten)

Stream: mathlib4

[Dan Synek]

This is a rewritten version of a question I asked yesterday. I was asked by @Adam Topaz to provide a #mwe . I have added it to the bottow. I also decided to add some background information to why the question is relevant .
Background
A while ago I had some problems with the lean implementationof the core of a category. I asked here and got a nice answer from @Kim Morrison and @Joel Riou to reimplement it similarly to how the opposite category is implemented by embedding the original category . I started by copying Oppopsite.lean, but didn't like that my code was 90% cut and paste. Also, it is a common pattern in functional languages to make a copy of a type under a new name, so I thought it would be a nice chance to learn some meta programming in Lean.

I now have a first implementation. It does introduce a layer of abstraction to how the original Opposite.lean was implemented. I recompiled Mathlib with my new version of Opposite.lean and it got stuck in a proof in Opposites.lean where simp did not progress in my reimplemented version. I tracked the problem down to a change in the proof of one of the lemmas op_unop. The lemma is identical, of course, only the proof is changed from rfl to something using my new abstractions. I simulate the issue in the question below by adding a structure with the rfl, so that the proof is now just a selector from this structure (see below). It is difficult for me to make a #mwe that showes precisely why simp no longer makes a progress. The proof objects in Opposites.lean printed with pp.all are two pages long and I am not able to precisely pinpoint what the issue is. I understand from surfing around in that it sometimes happens that a proof that involves dependent types sometimes don't go throuh when a proof object it depends on is changed, even though it proves precisely the same theorem. In my illustration below that is the only change, so I assume that it pinpoints the problem. So, if I could just make Lean reduce the proof term of my new proof of op_unop below, to the rfl it reduces to, the problem should be solved.

My original formulation of the problem
I have problems with a proof term that does not simplify if a proof of a lemma is changed.
I have tried to add the hint reducible, but it makes no difference. Is there some other way to guarantee that a proof of a theorem is maxiamally reduced? Or some other solution?
Here is a condensed version of what goes wrong:
In Mathlib.Data.Opposite if I change

@[simp]
theorem op_unop (x : αᵒᵖ) : op (unop x) = x := rfl

to

structure testC (x : αᵒᵖ) where
   out : op (unop x) = x

@[simp, reducible]
def testC1 (x : αᵒᵖ): testC x := {out := rfl}

@[simp]
theorem op_unop (x : αᵒᵖ) : op (unop x) = x :=
(@testC1 α x).out

then a proof in Opposites.lean goes wrong because simp can no longer simplify an expression.
The theorem that goes wrong is

def unop (e : Cᵒᵖ ≌ Dᵒᵖ) : C ≌ D

where the last simp in the proof does not make any progress.
A simplified example of what goes wrong is

def test(e : Cᵒᵖ ≌ Dᵒᵖ) (X : C): e.functor.unop.map ((NatIso.unop e.unitIso).symm.hom.app X) ≫
   (NatIso.unop e.counitIso).symm.hom.app (e.functor.unop.obj X) =
    𝟙 (e.functor.unop.obj X) := by
   apply Quiver.Hom.op_inj
   dsimp
   simp

My attempt at #mwe of the issue to reduce a proof term

variable (α : Type)
variable (x  : α)

theorem iseq (x : α) : x = x := rfl
structure testC (x : α) where
   out : x = x

@[simp, reducible]
def testC1 (x : α): testC α x := {out := rfl}

theorem should_be_rfl (x : α) : x = x :=
  (testC1 α x).out

 theorem is_rfl (x : α) : x = x :=
  rfl

-- I want the proof term of should_be_rfl to be identical to is_rfl
#print should_be_rfl -- fun α x ↦ (testC1 α x).out
#print is_rfl -- fun α x ↦ rfl

[Adam Topaz]

Can you provide a self-contained #mwe please?

[Yury G. Kudryashov]

Note that Lean treats simp lemmas proved by rfl a bit differently. E.g., the dsimp tactic can use them. This tactic just replaces the goal with the simplified version, without using any congruence lemmas.

[Dan Synek]

@Yury G. Kudryashov So, if it turns out that I cannot reduce the proof term to rfl, do you have a pointer to how I can prove the test lemma above? I tried using substitution, but got a error message ['rewrite' failed, motive is not type correct]

[Kevin Buzzard]

I don't understand the question yet. The proof of should_be_rfl is indeed rfl. What am I missing?

example : (testC1 α x).out = rfl := rfl

[Dan Synek]

@Kevin Buzzard Yes, also example(x :αᵒᵖ ) : (@testC1 α x).out = rfl := rfl is provable in my original code above (you can try yourself by adding it to Opposite.lean), but still exchanging one for the other makes the proof of the test theorem go through in the refl case but not the other.

[Yury G. Kudryashov]

Can you make an #mwe with a lemma you can't prove?

[Kevin Buzzard]

I guess the thing I don't understand here is the first premise. You said that if you turn

@[simp]
theorem op_unop (x : αᵒᵖ) : op (unop x) = x := rfl

to

structure testC (x : αᵒᵖ) where
   out : op (unop x) = x

then things go wrong. But testC is a completely unmotivated structure, and removing a simp lemma will of course make things go wrong. I think I'm just not on the right wavelength for this question yet.

[Dan Synek]

@Yury G. Kudryashov I did make the test lemma in the code above which is relatively short. To try it, checkout a fresh copy of Mathlib, exchange the theorem op_unop (x : αᵒᵖ) : op (unop x) = x := rfl line in Mathlib/Data/Opposite.lean to

structure testC (x : αᵒᵖ) where
   out : op (unop x) = x

@[simp, reducible]
def testC1 (x : αᵒᵖ): testC x := {out := rfl}

@[simp]
theorem op_unop (x : αᵒᵖ) : op (unop x) = x :=
(@testC1 α x).out

recompile Mathlab and you will get an error on the proof of `def unop (e : Cᵒᵖ ≌ Dᵒᵖ) : C ≌ D in Mathlib/CategoryTheory/Opposites.lean I simplified that to the test definition above which you can insert at the same section as the theorem.

I will try to make an isolated example that doesn't depend on Mathlib, but even getting this far has been difficult for a relative beginner as I am, so it might take time (and there is no guarantee I will succeed)

[Yury G. Kudryashov]

Dan Synek said:

Yury G. Kudryashov So, if it turns out that I cannot reduce the proof term to rfl

For dsimp, it isn't important if the proof term reduces to rfl. It's important if it's literally rfl.

[Yury G. Kudryashov]

That's because Mathlib relies on op_unop being a dsimp lemma.

[Yury G. Kudryashov]

Why do you want to modify Opposites in this way?

[Kevin Buzzard]

Oh -- something which might be confusing you -- in this definition which is bothering you

protected def op (F : C ⥤ D) : Cᵒᵖ ⥤ Dᵒᵖ where
  obj X := op (F.obj (unop X))
  map f := (F.map f.unop).op

there are two proofs which are hidden from you: the two axioms map_id and map_comp of a functor. They are being proved by aesop_cat (they are omitted completely in the code, and are hence being proved by a given default tactic, which for Functor is aesop_cat), and your change is changing the behaviour of dsimp and hence, presumably, of this more high-powered tactic.

[Dan Synek]

@Kevin Buzzard the testC structure is a simplification of the class I introduced to abstract from the Opposite definition. I made it as simple as I could, so of course it looks unmotivated. The isue is quiet natural and I think it must occur often. You abstract from a specific implementation, but retain the theorems. Naively, you would expect that as long as you prove the same theorems, the proofs that depend on them would remain provable, but in this case that is not the case. .

[Kevin Buzzard]

But you're not leaving the system in the same state that it was, you're just leaving it in a similar state :-)

[Yury G. Kudryashov]

Currently, category theory relies on unop_op being a rfl lemma all over the place. With dependent type theory, changing rfl/non-rfl can be important, if the term appears in the type of something else.

[Yury G. Kudryashov]

E.g., if you have (f : α → Type*) (x : α) (y : f x) (z : f (unop (op x))), then without unop_op being a rfl lemma, you can't even write y = z, you have to use docs#HEq instead.

[Dan Synek]

@Yury G. Kudryashov Why do you want to modify Opposites in this way?
So what I actually did was to make a macro (I called newtype) that makes a structure like the one used in Opposite.lean but with new names for constructos and the type.

structure Opposite :=
  /-- The canonical map `α → αᵒᵖ`. -/
  op ::
  /-- The canonical map `αᵒᵖ → α`. -/
  unop : α

I then make an abstract versions of the lemmas proved in Opposite.lean. I reimplementf the original Opposite by applying my macro and instantiating the abstracted theorems. In this way the proof that used to be ref in Opposite.lean are now the proofs of my abstract theorems instantiated to the Opposite I generated with my macro(and naively should be reducible to rfl).

Of course I am not sure that this is a good project that should be pushed into the main branch, even though it was an interesting project for me. But it is worrying that there is a lack of referential transparency in substituting a proof to another proof of a lemma. Most of the time in mathematics, you wouldn't want a theorem to depend on a particular proof of the lemmas it uses. Also, my project is still doable, I just have to move all the theorems into the macro, so that they are reproved every time a new instantiation is done. I wantedt avoid this, since it is not much better than the cut and paste I started with...

When you write:
E.g., if you have (f : α → Type*) (x : α) (y : f x) (z : f (unop (op x))), then without unop_op being a rfl lemma, you can't even write y = z, you have to use docs#HEq instead.
Is this true, even if the proof object reduces to rfl. But equality in type theory is a difficult subject, so I guess I am missing something.

[Yury G. Kudryashov]

If you want to autogenerate types like Opposite, then you should make sure that the lemmas like unop_op are proved by rfl, not something else. Otherwise dsimp won't use them.

[Dan Synek]

Thanks @Yury G. Kudryashov I can't say I understand exactly what is going on, but I will continue my project by generatig the proof in my macro to avoid the extra level of abstraction, which should solve the acute issues. You have been very helpful, so yet again the Lean community has been great! I will mark it as resolved, though I think it does point at a problem with the category theory implementation of Lean.

[Notification Bot]

Dan Synek has marked this topic as resolved.

[Kyle Miller]

Here's another explanation, since this is something that people working on the category theory library have found they need to understand:

If a @[simp] theorem is literally proved with rfl or Iff.rfl, it is marked as being a "dsimp theorem". These mark that the LHS and RHS are defeq, meaning that the LHS can always be replaced with the RHS no matter the context. Using rfl/Iff.rfl is also a marker by the user that they want this behavior.

Normally, simp can only rewrite in some contexts. Those contexts are constrained by the structure of congruence lemmas it generates. Dependent types prevent certain arguments from being rewritten by simp (for example, if there is an argument A : Type and an argument x : A, then usually only x will be rewritable by the general simp set). The non-rewritable arguments will be rewritten using the dsimp algorithm. All this complexity is due to the difference between definitional equality and propositional equality.

This doesn't have anything to do with proof reduction. Usually Lean doesn't reduce proofs, and it even avoids reducing them if it can help it. Note that the proof of a dsimp theorem doesn't matter: you can always replace the proof with rfl/Iff.rfl and see if it succeeds, and if it does then proof irrelevance says that this new proof is defeq to the old one. In principle, @[simp] could try re-proving a theorem with rfl/Iff.rfl when it decides what counts as a dsimp theorem, but it's at least more predictable that it looks for literally one of these proofs.

[Yury G. Kudryashov]

BTW, sometimes I wish we had an attribute for "this is a generic lemma, but in practice it's usually a rfl, so let dsimp try to use it".

[Yury G. Kudryashov]

This would make it possible to add a generic DFunLike.add_apply lemma that uses a (not yet existing) DFunLike.PointwiseAdd typeclass but is usable for dsimp for specific types.

[Dan Synek]

Yury G. Kudryashov said:

BTW, sometimes I wish we had an attribute for "this is a generic lemma, but in practice it's usually a rfl, so let dsimp try to use it".

Do I understand correctly that if I had a way of saying that "try to use this lemma as if it was proved by rfl" it would solve my problem since when applying the lemma it would actually be reduced to rfl.

[Dan Synek]

@Kyle Miller
I find this topic interestingand would like to understand it better.
Cold you expand on this:
you can always replace the proof with rfl/Iff.rfl and see if it succeeds, and if it does then proof irrelevance says that this new proof is defeq to the old one.
What does "it" refer to in your explanation. The theorem we are proving or the lemma we are using?

[Notification Bot]

Dan Synek has marked this topic as unresolved.

[Kyle Miller]

"it succeeds" -> "whether rfl/Iff.rfl can typecheck as a proof for the theorem"

In other words, when @[simp] processes a lemma, it could check for itself whether the LHS and RHS are defeq, and if so add it to the list of dsimp lemmas. Note that dsimp lemmas don't need proofs, since they're all lemmas whose LHS and RHS are defeq, so rfl/Iff.rfl may always be used to synthesize a proof as needed.

[Kyle Miller]

That's supposing that at declaration time the LHS and RHS are defeq and you just didn't realize it yet.

[Kyle Miller]

Yury's idea is interesting, where at dsimp application time, you can have it attempt to apply certain simp lemmas in addition to the dsimp lemmas, where the simp lemma only succeeds if the new term is defeq to the old one.