Zulip Chat Archive

Stream: PR reviews

Topic: 3185 leanchecker failure


Yury G. Kudryashov (Jun 26 2020 at 23:31):

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

Yury G. Kudryashov (Jun 26 2020 at 23:33):

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 (Jun 27 2020 at 01:04):

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 μ , to_outer_measure_le.2 $ 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 (Jun 28 2020 at 03:51):

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

Bryan Gin-ge Chen (Jun 28 2020 at 05:28):

@Mario Carneiro Have you seen this thread?

Mario Carneiro (Jun 28 2020 at 05:31):

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 (Jun 28 2020 at 05:32):

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

Mario Carneiro (Jun 28 2020 at 05:33):

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

Mario Carneiro (Jun 28 2020 at 05:34):

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

Floris van Doorn (Jun 28 2020 at 05:39):

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 (Jun 28 2020 at 05:41):

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

Mario Carneiro (Jun 28 2020 at 05:46):

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

Mario Carneiro (Jun 28 2020 at 05:47):

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 (Jun 28 2020 at 06:11):

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

Mario Carneiro (Jun 28 2020 at 06:12):

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

Bryan Gin-ge Chen (Jun 28 2020 at 06:16):

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 (Jun 28 2020 at 06:16):

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 (Jun 28 2020 at 06:17):

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

Bryan Gin-ge Chen (Jun 28 2020 at 06:20):

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 (Jun 28 2020 at 06:21):

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

Mario Carneiro (Jun 28 2020 at 06:22):

IIUC every prefix of a valid export is also valid

Mario Carneiro (Jun 28 2020 at 06:36):

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 (Jun 28 2020 at 06:41):

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 (Jun 28 2020 at 06:44):

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

Mario Carneiro (Jun 28 2020 at 06:45):

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 (Jun 28 2020 at 06:47):

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 (Jun 28 2020 at 06:59):

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 (Jun 28 2020 at 07:10):

proof_13 causes the hang

Bryan Gin-ge Chen (Jun 28 2020 at 07:11):

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 (Jun 28 2020 at 07:12):

all the action is in the implicit args, of course

Mario Carneiro (Jun 28 2020 at 07:12):

the theorem is massive

Mario Carneiro (Jun 28 2020 at 07:14):

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 (Jun 28 2020 at 07:14):

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 (Jun 28 2020 at 07:16):

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 (Jun 28 2020 at 07:17):

Yes, that one

Mario Carneiro (Jun 28 2020 at 07:18):

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 (Jun 28 2020 at 07:24):

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

Mario Carneiro (Jun 28 2020 at 07:25):

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

Mario Carneiro (Jun 28 2020 at 07:39):

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 (Jun 28 2020 at 07:41):

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

Mario Carneiro (Jun 28 2020 at 07:42):

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 (Jun 28 2020 at 07:43):

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

Mario Carneiro (Jun 28 2020 at 07:50):

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 (Jun 28 2020 at 09:54):

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

Yury G. Kudryashov (Jun 28 2020 at 13:20):

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

Mario Carneiro (Jun 28 2020 at 13:22):

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

Mario Carneiro (Jun 28 2020 at 13:22):

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

Mario Carneiro (Jun 28 2020 at 13:23):

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

Gabriel Ebner (Jun 28 2020 at 13:40):

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

Reid Barton (Jun 28 2020 at 13:47):

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

Reid Barton (Jun 28 2020 at 13:47):

Does the Lean kernel use irreducible as a hint?

Mario Carneiro (Jun 28 2020 at 13:50):

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

Mario Carneiro (Jun 28 2020 at 13:50):

Should we add irreducible markings to the export format?

Gabriel Ebner (Jun 28 2020 at 13:54):

The Lean type checker doesn't care about irreducible.

Gabriel Ebner (Jun 28 2020 at 13:54):

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 (Jun 28 2020 at 14:00):

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

Mario Carneiro (Jun 28 2020 at 14:00):

abbreviation hooks into this IIRC

Mario Carneiro (Jun 28 2020 at 14:01):

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 (Jun 28 2020 at 14:03):

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

Gabriel Ebner (Jun 28 2020 at 14:39):

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 (Jun 28 2020 at 14:39):

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 (Jun 28 2020 at 17:11):

The problem is in the top field.

Violeta Hernández (Jun 21 2022 at 23:00):

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


Last updated: Dec 20 2023 at 11:08 UTC