Zulip Chat Archive

Stream: PR reviews

Topic: 3185 leanchecker failure


view this post on Zulip Yury G. Kudryashov (Jun 26 2020 at 23:31):

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

view this post on Zulip 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?

view this post on Zulip 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) }

view this post on Zulip Yury G. Kudryashov (Jun 28 2020 at 03:51):

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

view this post on Zulip Bryan Gin-ge Chen (Jun 28 2020 at 05:28):

@Mario Carneiro Have you seen this thread?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 28 2020 at 05:32):

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

view this post on Zulip Mario Carneiro (Jun 28 2020 at 05:33):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jun 28 2020 at 05:46):

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

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (Jun 28 2020 at 06:11):

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

view this post on Zulip 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?

view this post on Zulip 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! ###

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 28 2020 at 06:17):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jun 28 2020 at 06:21):

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

view this post on Zulip Mario Carneiro (Jun 28 2020 at 06:22):

IIUC every prefix of a valid export is also valid

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 28 2020 at 07:10):

proof_13 causes the hang

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 28 2020 at 07:12):

all the action is in the implicit args, of course

view this post on Zulip Mario Carneiro (Jun 28 2020 at 07:12):

the theorem is massive

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Jun 28 2020 at 07:17):

Yes, that one

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jun 28 2020 at 07:25):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Bryan Gin-ge Chen (Jun 28 2020 at 09:54):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jun 28 2020 at 13:22):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Gabriel Ebner (Jun 28 2020 at 13:40):

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

view this post on Zulip Reid Barton (Jun 28 2020 at 13:47):

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

view this post on Zulip Reid Barton (Jun 28 2020 at 13:47):

Does the Lean kernel use irreducible as a hint?

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jun 28 2020 at 13:50):

Should we add irreducible markings to the export format?

view this post on Zulip Gabriel Ebner (Jun 28 2020 at 13:54):

The Lean type checker doesn't care about irreducible.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jun 28 2020 at 14:00):

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

view this post on Zulip Mario Carneiro (Jun 28 2020 at 14:00):

abbreviation hooks into this IIRC

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Jun 28 2020 at 17:11):

The problem is in the top field.


Last updated: May 07 2021 at 18:19 UTC