rewrite proof terms

Stream: lean4

[Joachim Breitner]

I was looking at the kind of proof terms that rewrite produces, and they look rather complicated, with an Eq.mp, and id, an Eq.ndrec and an Eq.refl, when it seems that Eq.ndrec and (possibly Eq.symm) should suffice; e.g. see this example:

import Std.Tactic.ShowTerm

opaque a : Nat
opaque b : Nat
axiom a_eq_b : a = b
opaque P : Nat → Prop

set_option pp.explicit true

-- Using rw
example (h : P b) : P a := by show_term rw [a_eq_b]; assumption

-- Using the proof term that rw produces
example (h : P b) : P a :=
  @Eq.mpr (P a) (P b)
  (@id (@Eq Prop (P a) (P b))
    (@Eq.ndrec Nat a (fun _a => @Eq Prop (P a) (P _a))
      (@Eq.refl Prop (P a)) b a_eq_b))
  h

-- Using the proof term that I would have expected
example (h : P b) : P a :=
  @Eq.ndrec Nat b (fun _a => P _a) h a a_eq_b.symm


-- A slightly simpler proof term using congrArg
example (h : P b) : P a :=
  @Eq.mpr (P a) (P b)
  (@id (@Eq Prop (P a) (P b))
    (@congrArg Nat Prop a b (fun _a => (P _a)) a_eq_b))
  h

Is there a good reason why rewrite uses a seemingly more convoluted proof term here?

[Joachim Breitner]

I did some code reading, and my current assumption is that we have these proof terms as a consequence of the meta programming structure.

In particular, docs#Lean.MVarId.rewrite runs on on an Expr without knowing whether its the conclusion or a hypothesis of the current goal, and (effectively) returns proof : (oldType = newType). Then docs#Lean.Elab.Tactic.rewriteTarget resp. docs#Lean.Elab.Tactic.rewriteLocalDecl apply that equality to the goal resp. the hypothesis using Eq.mpr resp. Eq.mp.

I don’t know whether and why the @id term, added in

    let newProof ← mkExpectedTypeHint eqProof eq

in docs#Lean.MVarId.replaceTargetEq, is needed. Maybe I should remove it, run CI, see what breaks, and then add a comment.

One could imagine that if docs#Lean.MVarId.rewrite knew whether it should produce oldType → newType or newType → oldType it could produce simpler proof terms, but there may be more reasons behind the current structure that I don't see right now. I wonder if the effect on the mathlib .olean size is noticable, but with the term sharing probably not so much.

[Joachim Breitner]

Although even with that structure I wonder if docs#Lean.MVarId.rewrite could return a (slightly) simpler proof using congrArg (added to the code snippet above). Maybe the problem here is that congrArg only works for non-dependent motives?

[Mario Carneiro]

Joachim Breitner said:

I don’t know whether and why the @id term, added in

    let newProof ← mkExpectedTypeHint eqProof eq

in docs#Lean.MVarId.replaceTargetEq, is needed. Maybe I should remove it, run CI, see what breaks, and then add a comment.

The purpose of the id term is to get the kernel to use the correct type when typechecking the body. This is required in those rare cases where definitional equality as checked by the kernel is not transitive, but much more commonly it will be a situation where A == B and B == C are quick to check but A == C ends up unfolding unnecessary things and being much slower. This is used by dsimp to avoid the kernel having to work too much trying to reconstruct the proof that dsimp found.

[Mario Carneiro]

More generally, lean produces inefficient proofs in many places, and I assure you there is no grander reason for this than it has not been an optimization goal of the lean system to produce short proofs. There are plenty of low hanging fruits you could do in this space like not using Eq.trans rfl all the time. These arise because the simplest way to code the proof generator involves these redundancies.

[Joachim Breitner]

Thanks! Is it worth plucking these fruits when coming across then, or is proof object size just too irrelevant to bother?

[Mario Carneiro]

Speaking for myself I would be very happy to see improvement in this area, I have wanted this for years. Proof object size is very much not irrelevant, it's one contributing factor to mathlib's 4GB

[Joachim Breitner]

Although there the much lower hanging fruit is to simply not ship them by default, because unless you are running a proof checker you don't need them, do you?

[Mario Carneiro]

to_additive reads proof terms

[Joachim Breitner]

Ah, good point.

[Joachim Breitner]

I played with slightly smaller proof terms in https://github.com/leanprover/lean4/pull/3121, and it almost goes through, but something odd is happening with the side-conditions from the lemma (different order, not filled with local assumptions by rw?), and I am bit confused how this rather simple change can affect such things.

[Yaël Dillies]

Mario Carneiro said:

to_additive reads proof terms

... although we've argued in the past that probably it should use transfer theorems and apply the multiplicative version instead