3185 leanchecker failure

Stream: PR reviews

[Yury G. Kudryashov]

Leanchecker times out in #3185, and I have no idea how to fix this.

[Yury G. Kudryashov]

I tried to run export&leanchecker for master + changes to complete_lattice, and it worked. So, the problem is in complete_lattice_of_Sup/Inf-based instances. Any ideas how to fix this?

[Yury G. Kudryashov]

Bisection says that the offender is this instance:

instance : has_Inf (measure α) :=
⟨λm, (Inf (to_outer_measure '' m)).to_measure $ Inf_caratheodory⟩

lemma Inf_apply {m : set (measure α)} {s : set α} (hs : is_measurable s) :
  Inf m s = Inf (to_outer_measure '' m) s :=
to_measure_apply _ _ hs

private lemma Inf_le (h : μ ∈ m) : Inf m ≤ μ :=
have Inf (to_outer_measure '' m) ≤ μ.to_outer_measure := Inf_le (mem_image_of_mem _ h),
assume s hs, by rw [Inf_apply hs, ← to_outer_measure_apply]; exact this s

private lemma le_Inf (h : ∀μ' ∈ m, μ ≤ μ') : μ ≤ Inf m :=
have μ.to_outer_measure ≤ Inf (to_outer_measure '' m) :=
  le_Inf $ ball_image_of_ball $ assume μ hμ, to_outer_measure_le.2 $ h _ hμ,
assume s hs, by rw [Inf_apply hs, ← to_outer_measure_apply]; exact this s

instance : order_bot (measure α) :=
{ bot := 0, bot_le := assume a s hs, by exact bot_le, .. measure.partial_order }

instance : order_top (measure α) :=
{ top := (⊤ : outer_measure α).to_measure (by rw [outer_measure.top_caratheodory]; exact le_top),
  le_top := assume a s hs,
    by cases s.eq_empty_or_nonempty with h  h;
      simp [h, to_measure_apply ⊤ _ hs, outer_measure.top_apply],
  .. measure.partial_order }

instance : complete_lattice (measure α) :=
{ .. measure.partial_order, .. measure.order_top, .. measure.order_bot,
  .. complete_lattice_of_Inf (measure α) (λ ms, ⟨λ _, Inf_le, λ _, le_Inf⟩) }

[Yury G. Kudryashov]

ping here. Need an expert on the internals of lean/leanchecker. @Gabriel Ebner ?

[Bryan Gin-ge Chen]

@Mario Carneiro Have you seen this thread?

[Mario Carneiro]

One thing that strikes me about that instance is that complete_lattice_of_Inf is going to prescribe one kind of inf and measure.order_top is going to give a different one

[Mario Carneiro]

the clash will appear several times in showing that all the mixed-in fields are coherent

[Mario Carneiro]

and that involves proving stuff like Inf empty = 0 by refl

[Mario Carneiro]

I'm kind of surprised this is even true, but it must be a lot of unfolding to prove

[Floris van Doorn]

I was also thinking that, but I don't think that is true. In a complete_lattice, all operations are only proven correct relative to the ordering, and that there are no axioms relating two different operations. So as long as the order is (easily seen to be) definitionally equal, then you can mix and match the other operations however you want.

[Bryan Gin-ge Chen]

I'm puzzled as to how there can be an issue like this that only shows up using leanchecker.

[Mario Carneiro]

the external checkers generally have lower quality heuristics for defeq than lean

[Mario Carneiro]

leanchecker actually uses the same kernel as lean, but it is still possible that some information in the environment is not being stored in the export format that is helpful as a defeq hint

[Yury G. Kudryashov]

I tried with .. partial_order and explicit bot/bot_le, and got the same result.

[Mario Carneiro]

which theorem exactly does it get stuck on? Is it the instance itself or one of the _proof_n auxiliaries?

[Bryan Gin-ge Chen]

For what it's worth, nanoda was happy with the mathlib.txt export.

### Finished checking 86172 items in 185.075931s; to the best of our knowledge, all terms were well-typed! ###

[Mario Carneiro]

Whoa, this isn't a good sign:

instance : complete_lattice (measure α) :=
{ .. measure.partial_order, .. measure.order_top, .. measure.order_bot,
  .. complete_lattice_of_Inf (measure α) _ }

times out in lean

[Mario Carneiro]

PS: I like the hedging in nanoda's output :grinning:

[Bryan Gin-ge Chen]

Mario Carneiro said:

which theorem exactly does it get stuck on? Is it the instance itself or one of the _proof_n auxiliaries?

How would one find out what leanchecker gets stuck on?

[Mario Carneiro]

You could try trimming the export until it doesn't hang

[Mario Carneiro]

IIUC every prefix of a valid export is also valid

[Mario Carneiro]

I have managed to confirm, using

lean -E mathlib.txt --only-export=measure_theory.measure.complete_lattice src/measure_theory/measure_space.lean

that the line that causes it to hang is the very last one, the #DEF that defines measure_theory.measure.complete_lattice

[Bryan Gin-ge Chen]

I did something similar by searching for mentions of 7890 (which corresponds to measure_theory.measure.complete_lattice) and then manually deleting parts of the txt file. This attachment blows up leanchecker. mathlib_def_7890.txt.zip

edit: since I'm already attaching a bunch of files to this thread, here's the result of Mario's command above: mathlib_only_export.txt.zip

[Bryan Gin-ge Chen]

leanchecker is happy with everything up to and including measure_theory.measure.complete_lattice._proof_17: mathlib_proof_17b.txt.zip

[Mario Carneiro]

I'm not sure if lean does typechecking on expr construction lines; maybe it can't because of de bruijn variables

[Bryan Gin-ge Chen]

In case the diff is meaningful:

764535,764629d764534
< 744689 #EA 524211 699822
< 744690 #EP #BC 186 697985 744689
< 744691 #EP #BI 3 24295 744690
< 744692 #EA 524214 699822
< 744693 #EA 733404 699822
< 744694 #EC 10886 20
< 744695 #EA 744694 2
< 744696 #EA 744695 1
< 744697 #EA 738880 744696
< 744698 #EA 744693 744697
< 744699 #EA 744692 744698
< 744700 #EA 744699 744144
< 744701 #EA 744700 744147
< 744702 #EC 10896 20
< 744703 #EA 744702 2
< 744704 #EA 744703 1
< 744705 #EA 744701 744704
< 744706 #EC 10897 20
< 744707 #EA 744706 2
< 744708 #EA 744707 1
< 744709 #EA 744705 744708
< 744710 #EC 10898 20
< 744711 #EA 744710 2
< 744712 #EA 744711 1
< 744713 #EA 744709 744712
< 744714 #EC 10899 20
< 744715 #EA 744714 2
< 744716 #EA 744715 1
< 744717 #EA 744713 744716
< 744718 #EC 10900 20
< 744719 #EA 744718 2
< 744720 #EA 744719 1
< 744721 #EA 744717 744720
< 744722 #EC 10901 20
< 744723 #EA 744722 2
< 744724 #EA 744723 1
< 744725 #EA 744721 744724
< 744726 #EC 10902 20
< 744727 #EA 744726 2
< 744728 #EA 744727 1
< 744729 #EA 744725 744728
< 744730 #EA 733722 699822
< 744731 #EA 744730 744697
< 744732 #EA 744729 744731
< 744733 #EC 10903 20
< 744734 #EA 744733 2
< 744735 #EA 744734 1
< 744736 #EA 744732 744735
< 744737 #EC 10904 20
< 744738 #EA 744737 2
< 744739 #EA 744738 1
< 744740 #EA 744736 744739
< 744741 #EC 10905 20
< 744742 #EA 744741 2
< 744743 #EA 744742 1
< 744744 #EA 744740 744743
< 744745 #EA 744206 699822
< 744746 #EA 744745 744218
< 744747 #EA 744744 744746
< 744748 #EC 10970 20
< 744749 #EA 744748 2
< 744750 #EA 744749 1
< 744751 #EA 744747 744750
< 744752 #EA 733875 699822
< 744753 #EA 744752 744528
< 744754 #EA 744751 744753
< 744755 #EC 10982 20
< 744756 #EA 744755 2
< 744757 #EA 744756 1
< 744758 #EA 744754 744757
< 744759 #EA 733940 699822
< 744760 #EA 744759 744697
< 744761 #EA 744758 744760
< 744762 #EA 734016 699822
< 744763 #EA 744762 744697
< 744764 #EA 744761 744763
< 744765 #EC 10983 20
< 744766 #EA 744765 2
< 744767 #EA 744766 1
< 744768 #EA 744764 744767
< 744769 #EC 10984 20
< 744770 #EA 744769 2
< 744771 #EA 744770 1
< 744772 #EA 744768 744771
< 744773 #EC 10985 20
< 744774 #EA 744773 2
< 744775 #EA 744774 1
< 744776 #EA 744772 744775
< 744777 #EC 10986 20
< 744778 #EA 744777 2
< 744779 #EA 744778 1
< 744780 #EA 744776 744779
< 744781 #EL #BC 186 697985 744780
< 744782 #EL #BI 3 24295 744781
< #DEF 7890 744691 744782 663

[Mario Carneiro]

My next tactic has been to rewrite the definition like so:

axiom not_sorry {α} : α

theorem complete_lattice' {α : Type u_1} [_inst_1 : measurable_space.{u_1} α] :
  complete_lattice.{u_1} (@measure_theory.measure.{u_1} α _inst_1) :=
@complete_lattice.mk.{u_1} (@measure_theory.measure.{u_1} α _inst_1)
  (@complete_lattice.sup.{u_1} (@measure_theory.measure.{u_1} α _inst_1)
      (@complete_lattice_of_Inf.{u_1} (@measure_theory.measure.{u_1} α _inst_1)
        (@measure_theory.measure.partial_order.{u_1} α _inst_1)
        (@measure_theory.measure.has_Inf.{u_1} α _inst_1)
        (@measure_theory.measure.complete_lattice._aux_1.{u_1} α _inst_1)))
  (@partial_order.le.{u_1} (@measure_theory.measure.{u_1} α _inst_1)
      (@measure_theory.measure.partial_order.{u_1} α _inst_1))
  (@partial_order.lt.{u_1} (@measure_theory.measure.{u_1} α _inst_1)
      (@measure_theory.measure.partial_order.{u_1} α _inst_1))
  (@measure_theory.measure.complete_lattice._proof_1.{u_1} α _inst_1)
  (@measure_theory.measure.complete_lattice._proof_2.{u_1} α _inst_1)
  (@measure_theory.measure.complete_lattice._proof_3.{u_1} α _inst_1)
  (@measure_theory.measure.complete_lattice._proof_4.{u_1} α _inst_1)
  (@measure_theory.measure.complete_lattice._proof_5.{u_1} α _inst_1)
  (@measure_theory.measure.complete_lattice._proof_6.{u_1} α _inst_1)
  (@measure_theory.measure.complete_lattice._proof_7.{u_1} α _inst_1)
  not_sorry -- (@complete_lattice.inf.{u_1} (@measure_theory.measure.{u_1} α _inst_1)
        --   (@complete_lattice_of_Inf.{u_1} (@measure_theory.measure.{u_1} α _inst_1)
        --     (@measure_theory.measure.partial_order.{u_1} α _inst_1)
        --     (@measure_theory.measure.has_Inf.{u_1} α _inst_1)
        --     (@measure_theory.measure.complete_lattice._aux_1.{u_1} α _inst_1)))
  not_sorry -- (@measure_theory.measure.complete_lattice._proof_8.{u_1} α _inst_1)
  not_sorry -- (@measure_theory.measure.complete_lattice._proof_9.{u_1} α _inst_1)
  not_sorry -- (@measure_theory.measure.complete_lattice._proof_10.{u_1} α _inst_1)
  not_sorry -- (@order_top.top.{u_1} (@measure_theory.measure.{u_1} α _inst_1)
        --   (@measure_theory.measure.order_top.{u_1} α _inst_1))
  not_sorry -- (@measure_theory.measure.complete_lattice._proof_11.{u_1} α _inst_1)
  not_sorry -- (@order_bot.bot.{u_1} (@measure_theory.measure.{u_1} α _inst_1)
        --   (@measure_theory.measure.order_bot.{u_1} α _inst_1))
  not_sorry -- (@measure_theory.measure.complete_lattice._proof_12.{u_1} α _inst_1)
  not_sorry -- (@complete_lattice.Sup.{u_1} (@measure_theory.measure.{u_1} α _inst_1)
        --   (@complete_lattice_of_Inf.{u_1} (@measure_theory.measure.{u_1} α _inst_1)
        --     (@measure_theory.measure.partial_order.{u_1} α _inst_1)
        --     (@measure_theory.measure.has_Inf.{u_1} α _inst_1)
        --     (@measure_theory.measure.complete_lattice._aux_1.{u_1} α _inst_1)))
  not_sorry -- (@complete_lattice.Inf.{u_1} (@measure_theory.measure.{u_1} α _inst_1)
        --   (@complete_lattice_of_Inf.{u_1} (@measure_theory.measure.{u_1} α _inst_1)
        --     (@measure_theory.measure.partial_order.{u_1} α _inst_1)
        --     (@measure_theory.measure.has_Inf.{u_1} α _inst_1)
        --     (@measure_theory.measure.complete_lattice._aux_1.{u_1} α _inst_1)))
  not_sorry -- (@measure_theory.measure.complete_lattice._proof_13.{u_1} α _inst_1)
  not_sorry -- (@measure_theory.measure.complete_lattice._proof_14.{u_1} α _inst_1)
  not_sorry -- (@measure_theory.measure.complete_lattice._proof_15.{u_1} α _inst_1)
  not_sorry -- (@measure_theory.measure.complete_lattice._proof_16.{u_1} α _inst_1)

and see how much of the definition I can unsorry before leanchecker chokes

[Mario Carneiro]

proof_13 causes the hang

[Bryan Gin-ge Chen]

theorem measure_theory.measure.complete_lattice._proof_13 :
  Π {α : Type u_1}, Π [_inst_1 : measurable_space α], Π a : measure_theory.measure α, has_le.le (has_bot.bot) a

[Mario Carneiro]

all the action is in the implicit args, of course

[Mario Carneiro]

the theorem is massive

[Mario Carneiro]

actually that doesn't match my proof_13, although I modified the original instance to make pp.all output a bit more bearable

instance : complete_lattice (measure α) :=
begin
  have : ∀ (s : set (measure α)), is_glb s (Inf s),
  abstract {exact λ ms, ⟨λ _, Inf_le, λ _, le_Inf⟩},
  exact
  { .. measure.partial_order, .. measure.order_top, .. measure.order_bot,
    .. complete_lattice_of_Inf (measure α) this }
end

[Mario Carneiro]

For me proof_13 is the one that says ∀ (s : set (measure α)) (a : measure α), a ∈ s → a ≤ complete_lattice.Sup s

[Bryan Gin-ge Chen]

Ah, OK, so it's:

theorem measure_theory.measure.complete_lattice._proof_14 :
  Π {α : Type u_1}, Π [_inst_1 : measurable_space α], Π s : set (measure_theory.measure α), Π a : measure_theory.measure α,
  has_mem.mem a s -> has_le.le a (complete_lattice.Sup s)

[Mario Carneiro]

Yes, that one

[Mario Carneiro]

Here's a self contained hang script:

instance : complete_lattice (measure α) :=
begin
  have : ∀ (s : set (measure α)), is_glb s (Inf s),
  abstract {exact λ ms, ⟨λ _, Inf_le, λ _, le_Inf⟩},
  exact
  { .. measure.partial_order, .. measure.order_top, .. measure.order_bot,
    .. complete_lattice_of_Inf (measure α) this }
end

theorem foo {α : Type u_1} [_inst_1 : measurable_space.{u_1} α] :
  ∀ (s : set.{u_1} (@measure_theory.measure.{u_1} α _inst_1)) (a : @measure_theory.measure.{u_1} α _inst_1),
    @has_mem.mem.{u_1 u_1} (@measure_theory.measure.{u_1} α _inst_1)
      (set.{u_1} (@measure_theory.measure.{u_1} α _inst_1))
      (@set.has_mem.{u_1} (@measure_theory.measure.{u_1} α _inst_1))
      a
      s →
    @has_le.le.{u_1} (@measure_theory.measure.{u_1} α _inst_1)
      (@preorder.to_has_le.{u_1} (@measure_theory.measure.{u_1} α _inst_1)
         (@partial_order.to_preorder.{u_1} (@measure_theory.measure.{u_1} α _inst_1)
            (@order_bot.to_partial_order.{u_1} (@measure_theory.measure.{u_1} α _inst_1)
               (@bounded_lattice.to_order_bot.{u_1} (@measure_theory.measure.{u_1} α _inst_1)
                  (@bounded_lattice.mk.{u_1} (@measure_theory.measure.{u_1} α _inst_1)
                     (@complete_lattice.sup.{u_1} (@measure_theory.measure.{u_1} α _inst_1)
                        (@complete_lattice_of_Inf.{u_1} (@measure_theory.measure.{u_1} α _inst_1)
                           (@measure_theory.measure.partial_order.{u_1} α _inst_1)
                           (@measure_theory.measure.has_Inf.{u_1} α _inst_1)
                           (@measure_theory.measure.complete_lattice._aux_1.{u_1} α _inst_1)))
                     (@partial_order.le.{u_1} (@measure_theory.measure.{u_1} α _inst_1)
                        (@measure_theory.measure.partial_order.{u_1} α _inst_1))
                     (@partial_order.lt.{u_1} (@measure_theory.measure.{u_1} α _inst_1)
                        (@measure_theory.measure.partial_order.{u_1} α _inst_1))
                     (@measure_theory.measure.complete_lattice._proof_1.{u_1} α _inst_1)
                     (@measure_theory.measure.complete_lattice._proof_2.{u_1} α _inst_1)
                     (@measure_theory.measure.complete_lattice._proof_3.{u_1} α _inst_1)
                     (@measure_theory.measure.complete_lattice._proof_4.{u_1} α _inst_1)
                     (@measure_theory.measure.complete_lattice._proof_5.{u_1} α _inst_1)
                     (@measure_theory.measure.complete_lattice._proof_6.{u_1} α _inst_1)
                     (@measure_theory.measure.complete_lattice._proof_7.{u_1} α _inst_1)
                     (@complete_lattice.inf.{u_1} (@measure_theory.measure.{u_1} α _inst_1)
                        (@complete_lattice_of_Inf.{u_1} (@measure_theory.measure.{u_1} α _inst_1)
                           (@measure_theory.measure.partial_order.{u_1} α _inst_1)
                           (@measure_theory.measure.has_Inf.{u_1} α _inst_1)
                           (@measure_theory.measure.complete_lattice._aux_1.{u_1} α _inst_1)))
                     (@measure_theory.measure.complete_lattice._proof_8.{u_1} α _inst_1)
                     (@measure_theory.measure.complete_lattice._proof_9.{u_1} α _inst_1)
                     (@measure_theory.measure.complete_lattice._proof_10.{u_1} α _inst_1)
                     (@order_top.top.{u_1} (@measure_theory.measure.{u_1} α _inst_1)
                        (@measure_theory.measure.order_top.{u_1} α _inst_1))
                     (@measure_theory.measure.complete_lattice._proof_11.{u_1} α _inst_1)
                     (@order_bot.bot.{u_1} (@measure_theory.measure.{u_1} α _inst_1)
                        (@measure_theory.measure.order_bot.{u_1} α _inst_1))
                     (@measure_theory.measure.complete_lattice._proof_12.{u_1} α _inst_1))))))
      a
      (@complete_lattice.Sup.{u_1} (@measure_theory.measure.{u_1} α _inst_1)
         (@complete_lattice_of_Inf.{u_1} (@measure_theory.measure.{u_1} α _inst_1)
            (@measure_theory.measure.partial_order.{u_1} α _inst_1)
            (@measure_theory.measure.has_Inf.{u_1} α _inst_1)
            (@measure_theory.measure.complete_lattice._aux_1.{u_1} α _inst_1))
         s) :=
@measure_theory.measure.complete_lattice._proof_13.{u_1} α _inst_1

lean -E mathlib.txt --only-export=measure_theory.measure.foo src/measure_theory/measure_space.lean
leanchecker mathlib.txt

[Bryan Gin-ge Chen]

Given that nanoda was happy with this, is the bug in Lean or in nanoda?

[Mario Carneiro]

given the lean was also happy, it is probably a bug in leanchecker

[Mario Carneiro]

Okay, I think I'm homing in on the issue:

theorem foo {α : Type u_1} [_inst_1 : measurable_space.{u_1} α] :
  @has_le.le (@measure α _inst_1)
    (@preorder.to_has_le (@measure α _inst_1)
      (@partial_order.to_preorder (@measure α _inst_1)
        (@order_bot.to_partial_order (@measure α _inst_1)
          (@bounded_lattice.to_order_bot (@measure α _inst_1)
            (@bounded_lattice.mk (@measure α _inst_1)
              (@complete_lattice.sup (@measure α _inst_1)
                (@complete_lattice_of_Inf (@measure α _inst_1)
                  (@measure.partial_order α _inst_1)
                  (@measure.has_Inf α _inst_1)
                  (@measure.complete_lattice._aux_1 α _inst_1)))
              (@partial_order.le (@measure α _inst_1)
                (@measure.partial_order α _inst_1))
              (@partial_order.lt (@measure α _inst_1)
                (@measure.partial_order α _inst_1))
              (@measure.complete_lattice._proof_1 α _inst_1)
              (@measure.complete_lattice._proof_2 α _inst_1)
              (@measure.complete_lattice._proof_3 α _inst_1)
              (@measure.complete_lattice._proof_4 α _inst_1)
              (@measure.complete_lattice._proof_5 α _inst_1)
              (@measure.complete_lattice._proof_6 α _inst_1)
              (@measure.complete_lattice._proof_7 α _inst_1)
              (@complete_lattice.inf (@measure α _inst_1)
                (@complete_lattice_of_Inf (@measure α _inst_1)
                  (@measure.partial_order α _inst_1)
                  (@measure.has_Inf α _inst_1)
                  (@measure.complete_lattice._aux_1 α _inst_1)))
              (@measure.complete_lattice._proof_8 α _inst_1)
              (@measure.complete_lattice._proof_9 α _inst_1)
              (@measure.complete_lattice._proof_10 α _inst_1)
              (@order_top.top (@measure α _inst_1)
                (@measure.order_top α _inst_1))
              (@measure.complete_lattice._proof_11 α _inst_1)
              (@order_bot.bot (@measure α _inst_1)
                (@measure.order_bot α _inst_1))
              (@measure.complete_lattice._proof_12 α _inst_1))))))
    =
  @has_le.le (@measure α _inst_1)
    (@preorder.to_has_le (@measure α _inst_1)
      (@partial_order.to_preorder (@measure α _inst_1)
        (@order_bot.to_partial_order (@measure α _inst_1)
          (@bounded_lattice.to_order_bot (@measure α _inst_1)
            (@bounded_lattice.mk (@measure α _inst_1)
              (@complete_lattice.sup (@measure α _inst_1)
                (@complete_lattice_of_Inf (@measure α _inst_1)
                  (@measure.partial_order α _inst_1)
                  (@measure.has_Inf α _inst_1)
                  (@measure.complete_lattice._aux_1 α _inst_1)))
              (@complete_lattice.le (@measure α _inst_1)
                (@complete_lattice_of_Inf (@measure α _inst_1)
                  (@measure.partial_order α _inst_1)
                  (@measure.has_Inf α _inst_1)
                  (@measure.complete_lattice._aux_1 α _inst_1)))
              (@complete_lattice.lt (@measure α _inst_1)
                (@complete_lattice_of_Inf (@measure α _inst_1)
                  (@measure.partial_order α _inst_1)
                  (@measure.has_Inf α _inst_1)
                  (@measure.complete_lattice._aux_1 α _inst_1)))
              (@complete_lattice.le_refl (@measure α _inst_1)
                (@complete_lattice_of_Inf (@measure α _inst_1)
                  (@measure.partial_order α _inst_1)
                  (@measure.has_Inf α _inst_1)
                  (@measure.complete_lattice._aux_1 α _inst_1)))
              (@complete_lattice.le_trans (@measure α _inst_1)
                (@complete_lattice_of_Inf (@measure α _inst_1)
                  (@measure.partial_order α _inst_1)
                  (@measure.has_Inf α _inst_1)
                  (@measure.complete_lattice._aux_1 α _inst_1)))
              (@complete_lattice.lt_iff_le_not_le (@measure α _inst_1)
                (@complete_lattice_of_Inf (@measure α _inst_1)
                  (@measure.partial_order α _inst_1)
                  (@measure.has_Inf α _inst_1)
                  (@measure.complete_lattice._aux_1 α _inst_1)))
              (@complete_lattice.le_antisymm (@measure α _inst_1)
                (@complete_lattice_of_Inf (@measure α _inst_1)
                  (@measure.partial_order α _inst_1)
                  (@measure.has_Inf α _inst_1)
                  (@measure.complete_lattice._aux_1 α _inst_1)))
              (@complete_lattice.le_sup_left (@measure α _inst_1)
                (@complete_lattice_of_Inf (@measure α _inst_1)
                  (@measure.partial_order α _inst_1)
                  (@measure.has_Inf α _inst_1)
                  (@measure.complete_lattice._aux_1 α _inst_1)))
              (@complete_lattice.le_sup_right (@measure α _inst_1)
                (@complete_lattice_of_Inf (@measure α _inst_1)
                  (@measure.partial_order α _inst_1)
                  (@measure.has_Inf α _inst_1)
                  (@measure.complete_lattice._aux_1 α _inst_1)))
              (@complete_lattice.sup_le (@measure α _inst_1)
                (@complete_lattice_of_Inf (@measure α _inst_1)
                  (@measure.partial_order α _inst_1)
                  (@measure.has_Inf α _inst_1)
                  (@measure.complete_lattice._aux_1 α _inst_1)))
              (@complete_lattice.inf (@measure α _inst_1)
                (@complete_lattice_of_Inf (@measure α _inst_1)
                  (@measure.partial_order α _inst_1)
                  (@measure.has_Inf α _inst_1)
                  (@measure.complete_lattice._aux_1 α _inst_1)))
              (@complete_lattice.inf_le_left (@measure α _inst_1)
                (@complete_lattice_of_Inf (@measure α _inst_1)
                  (@measure.partial_order α _inst_1)
                  (@measure.has_Inf α _inst_1)
                  (@measure.complete_lattice._aux_1 α _inst_1)))
              (@complete_lattice.inf_le_right (@measure α _inst_1)
                (@complete_lattice_of_Inf (@measure α _inst_1)
                  (@measure.partial_order α _inst_1)
                  (@measure.has_Inf α _inst_1)
                  (@measure.complete_lattice._aux_1 α _inst_1)))
              (@complete_lattice.le_inf (@measure α _inst_1)
                (@complete_lattice_of_Inf (@measure α _inst_1)
                  (@measure.partial_order α _inst_1)
                  (@measure.has_Inf α _inst_1)
                  (@measure.complete_lattice._aux_1 α _inst_1)))
              (@complete_lattice.top (@measure α _inst_1)
                (@complete_lattice_of_Inf (@measure α _inst_1)
                  (@measure.partial_order α _inst_1)
                  (@measure.has_Inf α _inst_1)
                  (@measure.complete_lattice._aux_1 α _inst_1)))
              (@complete_lattice.le_top (@measure α _inst_1)
                (@complete_lattice_of_Inf (@measure α _inst_1)
                  (@measure.partial_order α _inst_1)
                  (@measure.has_Inf α _inst_1)
                  (@measure.complete_lattice._aux_1 α _inst_1)))
              (@complete_lattice.bot (@measure α _inst_1)
                (@complete_lattice_of_Inf (@measure α _inst_1)
                  (@measure.partial_order α _inst_1)
                  (@measure.has_Inf α _inst_1)
                  (@measure.complete_lattice._aux_1 α _inst_1)))
              (@complete_lattice.bot_le (@measure α _inst_1)
                (@complete_lattice_of_Inf (@measure α _inst_1)
                  (@measure.partial_order α _inst_1)
                  (@measure.has_Inf α _inst_1)
                  (@measure.complete_lattice._aux_1 α _inst_1))))))))
  :=
@eq.trans _ _
  (@complete_lattice.le (@measure α _inst_1)
    (@complete_lattice_of_Inf (@measure α _inst_1)
      (@measure.partial_order α _inst_1)
      (@measure.has_Inf α _inst_1)
      (@measure.complete_lattice._aux_1 α _inst_1)))
  _ rfl rfl

[Mario Carneiro]

This proof, by eq.trans rfl rfl, goes through in leanchecker, but the proof using rfl does not

[Mario Carneiro]

Furthermore, if you attempt to prove the has_le instances equal (by commenting out the @has_le.le (@measure α _inst_1) line on each side) then lean times out

[Mario Carneiro]

In other words, leanchecker used the heuristic that says f x = f y <- x = y and timed out while proving x = y

[Mario Carneiro]

Yep, after applying this heuristic 4 times you get to prove bounded_lattice.mk ... = bounded_lattice.mk ... here, which produces exactly the bad subgoal that I was afraid of:

theorem foo {α : Type u_1} [_inst_1 : measurable_space.{u_1} α] :
    (@order_top.top (@measure α _inst_1)
                (@measure.order_top α _inst_1))
    =
    (@complete_lattice.top (@measure α _inst_1)
      (@complete_lattice_of_Inf (@measure α _inst_1)
        (@measure.partial_order α _inst_1)
        (@measure.has_Inf α _inst_1)
        (@measure.complete_lattice._aux_1 α _inst_1)))
  := rfl

[Bryan Gin-ge Chen]

lean#364, though I suspect @Gabriel Ebner may already be on it.

[Yury G. Kudryashov]

I wonder why we hit this with #3185 but not with other complete_lattice_of_Inf instances.

[Mario Carneiro]

as long as the defeq problem is obviously true or obviously false there is no problem

[Mario Carneiro]

it's only when it triggers a lot of unfolding without a conclusive result that it has the bad behavior

[Mario Carneiro]

I'm not entirely sure what specifically there is about the definition that causes the problem, probably it ended up unfolding real

[Gabriel Ebner]

attribute [irreducible] real? Oh wait, the external typechecker doesn't get this info.

[Reid Barton]

A potential solution is to change real to a 1-field structure.

[Reid Barton]

Does the Lean kernel use irreducible as a hint?

[Mario Carneiro]

@Gabriel Ebner Could it be that this is the key difference, why lean works but leanchecker doesn't?

[Mario Carneiro]

Should we add irreducible markings to the export format?

[Gabriel Ebner]

The Lean type checker doesn't care about irreducible.

[Gabriel Ebner]

I don't think it makes sense to add irreducible to the export format. We often need to local attribute [semireducible], and we do not store which declarations require this local reducibility change.

[Mario Carneiro]

Doesn't the kernel have its own version of reducibility hints?

[Mario Carneiro]

abbreviation hooks into this IIRC

[Mario Carneiro]

What I want to understand is what makes lean act differently from leanchecker in this instance, even though they use the same kernel code

[Mario Carneiro]

Could it be that the decision to unfold the projection in lean#364 is due to some magic in the projection macro?

[Gabriel Ebner]

Yes, I think the only difference here is the reducibility hints. For example most (all?) of the constructions (brec_on, rec_on, cases_on, etc.) are marked as abbreviation.

[Gabriel Ebner]

I'm not sure if the projection macros make it into the type checker. If they do, then that's another difference.

[Yury G. Kudryashov]

The problem is in the top field.

[Violeta Hernández]

Sorry for reviving an ancient thread, but is this fixed? I removed the comment and got the top field working with no issue