Computationally irrelevant proofs

Stream: general

[AHan]

Is there any tactics for handling program containing computationally irrelevant proof?
Sometimes it's annoying that the non-trivial proof been replace by _...

[Johan Commelin]

All proofs are irrelevant.

[Johan Commelin]

That's a design choice.

[Johan Commelin]

You shouldn't ever have to care about them again.

[Kenny Lau]

set_option pp.proofs true

[AHan]

@Johan Commelin Why shouldn't I have to care about them again ?
I mean what if I can proof my goal with just unfold definitions of some functions, but they're hided by _?

[AHan]

@Kenny Lau Thanks this is exactly what i'm looking for !

[Mario Carneiro]

The reason they are hidden is because it doesn't matter what is there; all proofs are definitionally equal (so if you unify with a term which has a different proof in that slot it doesn't matter), and proofs are computationally irrelevant (they do not affect control flow in any way) and they are literally thrown away by the VM.

[Mario Carneiro]

if you can prove your goal only by unfolding definitions, then probably rfl or similar will finish the job

[AHan]

Thanks for the explanation!

[petercommand]

is there any rw tactic to deal with programs containing computationally irrelevant proofs? like, sometimes I want to rewrite a subterm in a goal, but the type of the computationally irrelevant proof depends on that subterm

[petercommand]

and that makes it really annoying to manually rewrite that particular subterm

[petercommand]

I would very much want a tactic to deal with this :3

[petercommand]

like, a tactic that can rewrite the type of the proof simutaneously

[petercommand]

(and the type of the terms of the type of the proof etc)

[Chris Hughes]

There is subst, but that isn't too powerful at the moment.

[Mario Carneiro]

simp will do this, but probably not in the full generality you expect

[Mario Carneiro]

the full problem is actually quite hard

[Mario Carneiro]

but it is because of things like this that I try to avoid partial functions

[Mario Carneiro]

there are a variety of tricks for totalizing functions so that there is no proof argument in the way

[Kenny Lau]

@Mario Carneiro does that include using epsilon instead of some?

[Mario Carneiro]

I usually just pair some with an if statement

[Mario Carneiro]

There are other options too, you aren't necessarily removing the proof argument. You could push the proof into the domain, making it a subtype domain like finset, or you could push it into the codomain producing an roption function

[Kevin Buzzard]

This conversation is too abstract for me. Can someone post some examples of what people are saying should be avoided?

[Chris Hughes]

Stuff like log : Π z : ℂ, z ≠ 0 → ℂ because then if I have log x hx in my goal and x = y it's hard to rewrite.

[Patrick Massot]

Teaser: my talk in Amsterdam will feature this discussion on some example

[Kevin Buzzard]

Oh yes, you can't rewrite because hx isn't a proof of the right thing. Thanks.

[Kevin Buzzard]

The CS guys should just fix this

[Kevin Buzzard]

It's a problem with their system. They shouldn't be working around it. We should be making maths the way mathematicians do it, not moaning about things like this. Why can't it be fixed? Can it be fixed in Lean 4?

[Patrick Massot]

It seems the general case is hard for good reasons. But I agree Lean should have tactics that try heuristic or special cases

[Chris Hughes]

I get the sense that it might be much easier to make something that works 95% of the time, and the last 5% is super hard.

[Scott Morrison]

"Perfect is the enemy of good" has never been more appropriate!

[Kenny Lau]

maybe write a tactic to do it

[Kevin Buzzard]

I don't understand what's difficult here, but I'm sure there is something difficult because I'm aware that this issue comes up now and again

[Kevin Buzzard]

It feels the same as the "replace this ring with this isomorphic ring" issue

[petercommand]

It feels the same as the "replace this ring with this isomorphic ring" issue

I would think that "replace this ring with this isomorphic ring" would be even harder than substituting propositionally equal term

[petercommand]

since two isomorphic rings are not necessarily propositionally equal

[Kevin Buzzard]

Right! Mathematicians have a code of honour where we only do things to rings which would work if you replaced the ring with an isomorphic one

[Kenny Lau]

so you mean functors

[Joe Hendrix]

To resurrect this a bit, has there been a tactic that just introduces casts as needed? In the log example, with log : Π z : ℂ, z ≠ 0 → ℂ, if you have the term log x h and equalitye: x = y, the tactic could rewrite log x h to log y (eq.rec h e). I've tried this on an ad-hoc basis and sometimes run into problems later dealing with terms like (eq.rec h e), but perhaps a tactic could systematically rewrite through rec.

[Chris Hughes]

subst already does this but only for local constants. Apparently the problem is very hard in general.

[Mario Carneiro]

You can often get simp to do this, or conv, because they use congruence lemmas for rewriting