mathport:irreducible

Stream: lean4

[Daniel Selsam]

I see that many but not all of the post-facto [irreducible] attributes have been successfully removed from mathlib. Is there a consensus now that this backport is feasible?

[Gabriel Ebner]

Some easy irreducibles have been ported. But the interesting ones like additive/multiplicative/with_top/with_bot/with_one/with_zero/order_dual are still open as far as I'm concerned.

[Daniel Selsam]

By "open" do you mean "it is an open question if they are feasible" or only that they have not yet been backported?

[Gabriel Ebner]

One of the big issues why we made these type tags irreducible is because of the simplifier. Namely, if you define def WithTop (α) := Option α and def WithBot (α) := Option α, then Lean 3 used to apply simp lemmas for WithTop to WithBot and vice versa.
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.22bug.22.20in.20.60simp.60.3F/near/207319933

[Gabriel Ebner]

I've tried to port additive/multiplicative to structures (which clearly solves the simp issue), but @Mario Carneiro was staunchly against that change.

[Mario Carneiro]

What is the status of type aliases for the purpose of getting different typeclass instances inferred in lean 4?

[Daniel Selsam]

What do you mean by "type alias" here?

[Mario Carneiro]

def foo := bar, instance : my_class foo := something_else

[Mario Carneiro]

It might be possible to label def foo with some irreducibility attribute but it can't be something completely opaque, because the defeq between foo and bar is an essential part of this mechanism

[Mario Carneiro]

but it seems like semireducible should be good enough since type class inference does not see through such definitions

[Mario Carneiro]

The issue Gabriel mentions about simp seeing through semireducible definitions also sounds like a bug in simp, not a reason to mark things irreducible

[Gabriel Ebner]

It's not a bug in simp directly, it's pretty deep in unification.

[Gabriel Ebner]

And yes, instead of marking the type tags irreducible, we might be able to fix these leaks.

[Mario Carneiro]

Alternatively, we could have a reducibility setting which is "irreducible except in opt-out settings"

[Mario Carneiro]

which might also be irreducible, I guess

[Daniel Selsam]

@Mario Carneiro the following technically works in Lean4 because of the discrimination tree indexing:

class Cls (α : Type) := (x : α)
def cls (α : Type) [Cls α] : α := Cls.x

structure Foo : Type := (foo : Bool)

def Bar : Type := Foo

instance : Cls Foo := ⟨⟨false⟩⟩
instance : Cls Bar := ⟨⟨true⟩⟩

theorem fooFalse : cls Foo = ⟨false⟩ := rfl
theorem barTrue  : cls Bar = ⟨true⟩  := rfl

[Mario Carneiro]

That all looks good except for the foreboding "technically"

[Mario Carneiro]

I don't see why this would be any less than a supported feature

[Daniel Selsam]

It works fine, I just hesitate to endorse the style :)

[Mario Carneiro]

In lean 3, this was one of the main reasons to use a type alias

[Daniel Selsam]

To clarify what is happening in the example above: the query Cls Bar asks the discrimination tree for candidate matches to Cls Bar, and since Bar is not reducible, it only returns the desired instance. In Lean3, the query Cls Bar would cause a head-map query for Cls, which would return both.

[Mario Carneiro]

My hope is that this is handled exactly the same as if Bar was a newtype structure around Foo

[Mario Carneiro]

The only difference between them should be during unification, when the reducibility setting is set to semireducible or more

[Mario Carneiro]

and since most tactics like rw and simp use reducible reducibility setting, they should also see Bar as opaque in either case

[Mario Carneiro]

unless of course you use rw [Bar]

[Daniel Selsam]

It seems sketchy to me. Would it really be so bad to use a struct?

[Gabriel Ebner]

AFAICT, the simp issues seem to be solved in Lean 4. Lemmas for the type tags do not leak to the definition.

def Foo := Nat
def Foo.toNat : Foo → Nat := id
instance : HasLessEq Foo := ⟨fun x y => (by exact x : Nat) ≤ y⟩
@[simp] theorem Foo.le_iff (x y : Foo) : x ≤ y ↔ x.toNat ≤ y.toNat := Iff.rfl

def Bar := Nat
def Bar.toNat : Bar → Nat := id
instance : HasLessEq Bar := ⟨fun x y => (by exact x : Nat) ≤ y⟩

set_option trace.Meta.Tactic.simp true
example (x y : Foo) : x ≤ y := by simp -- applies Foo.le_iff once
example (x y : Bar) : x ≤ y := by simp -- doesn't apply Foo.le_iff

In Lean 3, both of the two simp calls actually go into an infinite loop.

[Daniel Selsam]

Yes, for the same reasons as in the Cls example above. The two goals are:

⊢ @HasLessEq.LessEq.{0} Foo instHasLessEqFoo x y
⊢ @HasLessEq.LessEq.{0} Bar instHasLessEqBar x y

and the discrimination tree treats Foo and Bar as separate constants (since they are not reducible).

[Mario Carneiro]

It seems sketchy to me. Would it really be so bad to use a struct?

You lose the defeq, which means that if this thing appears inside types (and since this is a type that's not unusual) there are circumstances where this will unavoidably lead to DTT hell

[Mario Carneiro]

For additive/multiplicative, it is possible to prove theorems in O(1) that otherwise requires the horrible and wasteful hack that is to_additive. It's possible to prove to_additive style theorems in O(statement), but this requires something like equiv_rw and I think it's still open in the general case

[Gabriel Ebner]

Daniel Selsam said:

Yes, for the same reasons as in the Cls example above. The two goals are:

⊢ @HasLessEq.LessEq.{0} Foo instHasLessEqFoo x y
⊢ @HasLessEq.LessEq.{0} Bar instHasLessEqBar x y

and the discrimination tree treats Foo and Bar as separate constants (since they are not reducible).

Ah, so it still leaks when Lean uses unification. :sad:

def Foo := Nat
def Foo.toNat : Foo → Nat := id
instance : HasLessEq Foo := ⟨fun x y => (by exact x : Nat) ≤ y⟩
@[simp] theorem Foo.le_iff (x y : Foo) :
  (∃ _ : Nat, x ≤ y) ↔ (∃ _ : Nat, x.toNat ≤ y.toNat) := Iff.rfl

example (x y : Foo) : ∃ _ : Nat, x ≤ y := by simp -- 100% CPU

[Mario Carneiro]

That sounds like it would be solved by setting the reducibility setting on that unification

[Gabriel Ebner]

@Mario Carneiro The issue has always been that Lean uses more aggressive unification for implicit arguments than for explicit arguments. That is, even if simp uses reducible transparency, Foo and Nat will still unify when they are in implicit arguments. I have no idea whether it would be feasible/desirable/devastating to change that behavior.

[Mario Carneiro]

That kind of sounds like having another reducibility setting would be a good idea then

[Mario Carneiro]

it would be interesting to know exactly what the fallout of not unfolding semireducibles in implicits is though

[Daniel Selsam]

What do you expect to learn? Chances are a ton of things will break and it will be hard to diagnose all the reasons.

[Mario Carneiro]

I don't think we actually depend on it that much. I certainly haven't been writing code with this in mind

[Mario Carneiro]

But it would be good to classify the breakages and see whether they aren't just mistakes

[Daniel Selsam]

You could also instrument the lean3 unifier to print out specifically when an isDefEq call on an implicit argument that succeeds with semireducible would have failed with reducible.

[Mario Carneiro]

Does the unifier ever use reducible in normal usage? i.e. not in a tactic

[Mario Carneiro]

Just because you catch such an instance doesn't mean that the proof would have failed, because it might just be the tactic trying something and if it fails it will do something else

[Mario Carneiro]

those kinds of breakages come up all the time when we have minor tactic semantic changes

[Daniel Selsam]

Mario Carneiro said:

Does the unifier ever use reducible in normal usage? i.e. not in a tactic

In lean3, reducibility status is generally mediated by transparency_scope objects. Here is the grep:

./frontends/lean/elaborator.cpp:2376:            type_context_old::transparency_scope scope(ctx(), transparency_mode::None);
./frontends/lean/inductive_cmds.cpp:422:        type_context_old::transparency_scope scope(m_ctx, transparency_mode::None);
./library/defeq_canonizer.cpp:107:    type_context_old::transparency_scope scope(m_ctx, transparency_mode::Instances);
./library/defeq_canonizer.cpp:115:    type_context_old::transparency_scope scope(m_ctx, transparency_mode::Instances);
./library/compiler/preprocess.cpp:69:        type_context_old::transparency_scope scope(ctx(), transparency_mode::Reducible);
./library/compiler/preprocess.cpp:132:                type_context_old::transparency_scope scope(ctx(), transparency_mode::Reducible);
./library/compiler/preprocess.cpp:145:                type_context_old::transparency_scope scope(ctx(), transparency_mode::Reducible);
./library/compiler/inliner.cpp:138:        type_context_old::transparency_scope _(ctx(), transparency_mode::Instances);
./library/type_context.h:756:    struct transparency_scope : public flet<transparency_mode> {
./library/type_context.h:757:        transparency_scope(type_context_old & ctx, transparency_mode m):
./library/type_context.h:787:        transparency_scope m_transparency_scope;
./library/type_context.h:790:            m_transparency_scope(ctx, m),
./library/equations_compiler/util.cpp:389:    type_context_old::transparency_scope scope(ctx, transparency_mode::Reducible);
./library/inductive_compiler/nested.cpp:238:            type_context_old::transparency_scope scope(tctx, transparency_mode::Instances);
./library/app_builder.cpp:761:        type_context_old::transparency_scope _s1(ctx, *md);
./library/app_builder.cpp:765:        type_context_old::transparency_scope _s1(ctx, transparency_mode::Semireducible);
./library/type_context.cpp:716:        transparency_scope scope(*this, transparency_mode::All);
./library/type_context.cpp:2571:        transparency_scope scope(*this, ensure_semireducible_mode(m_transparency_mode));
./library/tactic/rewrite_tactic.cpp:93:        type_context_old::transparency_scope scope(ctx, ensure_semireducible_mode(ctx.mode()));
./library/tactic/unfold_tactic.cpp:79:        type_context_old::transparency_scope scope(m_ctx, transparency_mode::Instances);
./library/tactic/smt/smt_state.cpp:242:    type_context_old::transparency_scope scope2(ctx, transparency_mode::Reducible);
./library/tactic/simplify.cpp:1109:    type_context_old::transparency_scope scope(ctx, transparency_mode::Semireducible);
./library/tactic/dsimplify.cpp:80:            type_context_old::transparency_scope scope(ctx, transparency_mode::Instances);
./library/tactic/dsimplify.cpp:88:        type_context_old::transparency_scope scope(ctx, transparency_mode::Reducible);
./library/tactic/dsimplify.cpp:322:    type_context_old::transparency_scope s(m_ctx, m_cfg.m_md);
./library/tactic/dsimplify.cpp:337:        type_context_old::transparency_scope s(m_ctx, m_cfg.m_md);
./library/tactic/induction_tactic.cpp:115:    type_context_old::transparency_scope scope(ctx, transparency_mode::All);

[Mario Carneiro]

fyi you need to use ````quote ... ```` to enclose ```lean ... ```

[Daniel Selsam]

That isn't Lean code -- I made it a regular quote so it would line-wrap (though it is still ugly)

[Mario Carneiro]

I guess grep isn't a language id

[Mario Carneiro]

The examples where it is explicitly reducible seem to be in the compiler and the equation compiler. The compiler operation is not very observable so I doubt it matters much, and the equation compiler may or may not cause weird edge case errors but probably doesn't cause too many issues in practice

[Daniel Selsam]

I am happy to push a dont-force-semireducible-for-implicits patch to a lean3 branch if you will run the experiment

[Daniel Selsam]

FYI Lean4 does build with this change

[Daniel Selsam]

There are a ton of breakages even building lean3. Here is the first one:

/home/dselsam/mathport/lean3/library/init/meta/interactive.lean:97:3: error: failed to synthesize type class instance for
tac : itactic,
propagate_tags : tactic unit,
tag : tactic.tag
⊢ decidable (tag = list.nil)

tag has type tactic.tag which is defined to list name. The patch is only one line so I'll just tell you: comment out https://github.com/leanprover-community/lean/blob/master/src/library/type_context.cpp#L2571

[Daniel Selsam]

FYI here is the commit that added this feature in the first place: https://github.com/leanprover-community/lean/commit/e59fd2927a91e4dbe00c825764632786b6388df2

[Daniel Selsam]

I remember this being a big win at the time and I am skeptical about rolling it back. I also doubt Leo would even consider merging it.

[Mario Carneiro]

I expect that there will be a lot of breakages like that example: it was committed because it works, but it's definitely a bug and should be fixed regardless. (In that example, tactic.tag should have decidable_eq)

[Gabriel Ebner]

BTW, there isn't much breakage in core: lean#556

[Mario Carneiro]

Here's an example breakage from mathlib that might be tricky to fix:

/home/mario/Documents/lean/mathlib/src/data/typevec.lean:436:35: error: solve1 tactic failed, focused goal has not been solved
state:
n i_n : ℕ,
i_ᾰ : fin2 i_n,
α β : typevec i_n.succ,
a : α i_ᾰ.fs,
b : β i_ᾰ.fs,
i_ih :
  ∀ {α β : typevec i_n} (a : α i_ᾰ) (b : β i_ᾰ), @prod.fst i_n α β i_ᾰ (@prod.mk i_n α β i_ᾰ a b) = a
⊢ @prod.fst i_n α.drop β.drop i_ᾰ
      (@prod.mk i_n (λ (i : fin2 i_n), α i.fs) (λ (i : fin2 i_n), β i.fs) i_ᾰ a b) = a

This is after a simp [prod.fst, prod.mk, *] at * that was supposed to close the goal. Note that @i_ih (λ (i : fin2 i_n), α i.fs) (λ (i : fin2 i_n), β i.fs) a b unifies with the goal, but only at semireducible because we need to reduce (λ (i : fin2 i_n), α i.fs).drop = α

[Daniel Selsam]

@Gabriel Ebner what do you think about removing irreducible from Lean3 and adding Lean4's constant-with-def, rather than the somewhat hacky plan we sketched in https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/mathport/near/225031878 ?

[Scott Morrison]

(While this will presumably be hard, it hopefully comes out of a fixed budget of hard work for the porting effort. :-)

[Daniel Selsam]

@Scott Morrison this proposal is conditional on the tentative plan to stop using irreducible in Lean3 except in ways that simulate Lean4's constant-with-def. the proposal wouldn't entail much additional work -- it would mainly serve to enforce the irreducible policy

[Mario Carneiro]

I think it would be easier to not remove irreducible but rather restrict its usage to certain patterns that mathport can pick up on and translate to constant-with-def

[Mario Carneiro]

It shouldn't be too hard to lint against unapproved usage patterns

[Gabriel Ebner]

I agree with Mario. The format of irreducible definitions in Lean 3 is easy enough to parse. There's one definition foo with the irreducible attribute, and one lemma foo.equations._eqn_1.

[Gabriel Ebner]

On the other hand, adding Lean 4-style constants to the kernel is a nontrivial effort. And then we'd still need to modify the definition command to actually simulate an irreducible definition using constants.

[Daniel Selsam]

either way, but FYI constant is just a regular definition with reducibility hint opaque.

[Gabriel Ebner]

The meaning of an opaque reducibility hint is probably different in Lean 4, but in Lean 3 it has no real effect:

open tactic
run_cmd add_decl (declaration.defn `a [] `(ℕ) `(42) reducibility_hints.opaque tt)
lemma a_eq_42 : a = 42 := rfl

[Daniel Selsam]

I might be wrong about constant then. Let me confirm.

[Daniel Selsam]

@Gabriel Ebner You are right, constant is stronger than opaque and there is currently no support in Lean3. opaque seems a poor word choice, more like "rigid"

[Daniel Selsam]

FYI these are the differing lines:

https://github.com/leanprover/lean4/blob/master/src/kernel/declaration.h#L444
https://github.com/leanprover/lean4/blob/master/src/kernel/type_checker.cpp#L481

Basically, even though the constants keep their value, they still tell is_delta no, whereas opaque is still a delta and only affects the case when f ... =?= g ...

[Daniel Selsam]

FYI the patch from https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/mathport/near/225031878 complicates mathport a lot (it can no longer process action items in one pass) and also cannot be applied currently due to post-factor semireducible-toggling e.g. https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/mathport/near/225031878