Zulip Chat Archive

Stream: lean4

Topic: mathport:irreducible


view this post on Zulip Daniel Selsam (Mar 17 2021 at 15:25):

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?

view this post on Zulip Gabriel Ebner (Mar 17 2021 at 15:30):

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.

view this post on Zulip Daniel Selsam (Mar 17 2021 at 15:33):

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

view this post on Zulip Gabriel Ebner (Mar 17 2021 at 15:33):

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

view this post on Zulip Gabriel Ebner (Mar 17 2021 at 15:34):

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

view this post on Zulip Mario Carneiro (Mar 17 2021 at 15:37):

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

view this post on Zulip Daniel Selsam (Mar 17 2021 at 15:39):

What do you mean by "type alias" here?

view this post on Zulip Mario Carneiro (Mar 17 2021 at 15:39):

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

view this post on Zulip Mario Carneiro (Mar 17 2021 at 15:40):

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

view this post on Zulip Mario Carneiro (Mar 17 2021 at 15:41):

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

view this post on Zulip Mario Carneiro (Mar 17 2021 at 15:43):

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

view this post on Zulip Gabriel Ebner (Mar 17 2021 at 15:44):

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

view this post on Zulip Gabriel Ebner (Mar 17 2021 at 15:44):

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

view this post on Zulip Mario Carneiro (Mar 17 2021 at 15:45):

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

view this post on Zulip Mario Carneiro (Mar 17 2021 at 15:45):

which might also be irreducible, I guess

view this post on Zulip Daniel Selsam (Mar 17 2021 at 15:46):

@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

view this post on Zulip Mario Carneiro (Mar 17 2021 at 15:47):

That all looks good except for the foreboding "technically"

view this post on Zulip Mario Carneiro (Mar 17 2021 at 15:47):

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

view this post on Zulip Daniel Selsam (Mar 17 2021 at 15:47):

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

view this post on Zulip Mario Carneiro (Mar 17 2021 at 15:48):

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

view this post on Zulip Daniel Selsam (Mar 17 2021 at 15:51):

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.

view this post on Zulip Mario Carneiro (Mar 17 2021 at 15:52):

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

view this post on Zulip Mario Carneiro (Mar 17 2021 at 15:53):

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

view this post on Zulip Mario Carneiro (Mar 17 2021 at 15:54):

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

view this post on Zulip Mario Carneiro (Mar 17 2021 at 15:54):

unless of course you use rw [Bar]

view this post on Zulip Daniel Selsam (Mar 17 2021 at 16:00):

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

view this post on Zulip Gabriel Ebner (Mar 17 2021 at 16:03):

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.

view this post on Zulip Daniel Selsam (Mar 17 2021 at 16:06):

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).

view this post on Zulip Mario Carneiro (Mar 17 2021 at 16:07):

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

view this post on Zulip Mario Carneiro (Mar 17 2021 at 16:09):

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

view this post on Zulip Gabriel Ebner (Mar 17 2021 at 16:11):

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

view this post on Zulip Mario Carneiro (Mar 17 2021 at 16:14):

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

view this post on Zulip Gabriel Ebner (Mar 17 2021 at 16:18):

@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.

view this post on Zulip Mario Carneiro (Mar 17 2021 at 16:19):

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

view this post on Zulip Mario Carneiro (Mar 17 2021 at 16:20):

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

view this post on Zulip Daniel Selsam (Mar 17 2021 at 16:24):

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

view this post on Zulip Mario Carneiro (Mar 17 2021 at 16:26):

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

view this post on Zulip Mario Carneiro (Mar 17 2021 at 16:27):

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

view this post on Zulip Daniel Selsam (Mar 17 2021 at 16:27):

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.

view this post on Zulip Mario Carneiro (Mar 17 2021 at 16:28):

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

view this post on Zulip Mario Carneiro (Mar 17 2021 at 16:29):

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

view this post on Zulip Mario Carneiro (Mar 17 2021 at 16:30):

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

view this post on Zulip Daniel Selsam (Mar 17 2021 at 16:31):

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);

view this post on Zulip Mario Carneiro (Mar 17 2021 at 16:34):

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

view this post on Zulip Daniel Selsam (Mar 17 2021 at 16:34):

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

view this post on Zulip Mario Carneiro (Mar 17 2021 at 16:35):

I guess grep isn't a language id

view this post on Zulip Mario Carneiro (Mar 17 2021 at 16:38):

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

view this post on Zulip Daniel Selsam (Mar 17 2021 at 16:42):

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

view this post on Zulip Daniel Selsam (Mar 17 2021 at 16:44):

FYI Lean4 does build with this change

view this post on Zulip Daniel Selsam (Mar 17 2021 at 16:54):

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

view this post on Zulip Daniel Selsam (Mar 17 2021 at 17:01):

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

view this post on Zulip Daniel Selsam (Mar 17 2021 at 17:03):

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.

view this post on Zulip Mario Carneiro (Mar 17 2021 at 18:02):

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)

view this post on Zulip Gabriel Ebner (Mar 17 2021 at 18:06):

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

view this post on Zulip Mario Carneiro (Mar 17 2021 at 19:35):

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 = α

view this post on Zulip Daniel Selsam (Mar 18 2021 at 02:37):

@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 ?

view this post on Zulip Scott Morrison (Mar 18 2021 at 02:40):

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

view this post on Zulip Daniel Selsam (Mar 18 2021 at 02:44):

@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

view this post on Zulip Mario Carneiro (Mar 18 2021 at 04:44):

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

view this post on Zulip Mario Carneiro (Mar 18 2021 at 04:44):

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

view this post on Zulip Gabriel Ebner (Mar 18 2021 at 09:21):

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.

view this post on Zulip Gabriel Ebner (Mar 18 2021 at 09:23):

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.

view this post on Zulip Daniel Selsam (Mar 18 2021 at 13:22):

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

view this post on Zulip Gabriel Ebner (Mar 18 2021 at 13:38):

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

view this post on Zulip Daniel Selsam (Mar 18 2021 at 13:47):

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

view this post on Zulip Daniel Selsam (Mar 18 2021 at 13:59):

@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"

view this post on Zulip Daniel Selsam (Mar 18 2021 at 14:03):

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 ...

view this post on Zulip Daniel Selsam (Mar 19 2021 at 15:04):

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


Last updated: May 18 2021 at 23:14 UTC