# 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 μ 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 (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):

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

?

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

Last updated: May 07 2021 at 18:19 UTC