Zulip Chat Archive
Stream: lean4
Topic: 7 ∧ / ∨
Damiano Testa (Dec 22 2022 at 11:39):
Dear All,
I do not know if what is below is a bug or not and whether it has already been reported. It seems that Lean interprets up to 6 consecutive ands or ors of booleans as booleans, but stops doing so when there are 7. It is not a big deal, since the second example below is an easy workaround, but I was surprised by this!
-- works, 6 `and`s
example (a b c d e f g : Bool) : Bool := a ∧ b ∧ c ∧ d ∧ e ∧ f ∧ g
-- works, 6 `and`s plus an `(_ ∧ _)`
example (a b c d e f g h : Bool) : Bool := a ∧ b ∧ c ∧ d ∧ e ∧ f ∧ (g ∧ h : Bool)
-- fails, 7 `and`s expects a `Bool`, finds a `Prop`
example (a b c d e f g h : Bool) : Bool := a ∧ b ∧ c ∧ d ∧ e ∧ f ∧ g ∧ h
Eric Wieser (Dec 22 2022 at 11:44):
What does this actually generate if you give these examples a name and #print them?
Damiano Testa (Dec 22 2022 at 11:46):
theorem seven (a b c d e f g h : Bool) : Bool := a ∧ b ∧ c ∧ d ∧ e ∧ f ∧ g ∧ h
/-
type mismatch
a = true ∧ b = true ∧ c = true ∧ d = true ∧ e = true ∧ f = true ∧ g = true ∧ h = true
has type
Prop : Type
but is expected to have type
Bool : Type
-/
#print seven
/-
theorem seven : Bool → Bool → Bool → Bool → Bool → Bool → Bool → Bool → Bool :=
sorryAx (Bool → Bool → Bool → Bool → Bool → Bool → Bool → Bool → Bool) true
-/
Damiano Testa (Dec 22 2022 at 11:46):
Is this what you asked?
Eric Wieser (Dec 22 2022 at 11:47):
I mean for the ones that succeeded
Kevin Buzzard (Dec 22 2022 at 11:47):
and expects to eat Props not Bools so the question is why the coercion is not kicking in
Eric Wieser (Dec 22 2022 at 11:47):
... which is why I wanted to see the elaborated output so we can tell where it did kick in in the versions that were ok
Damiano Testa (Dec 22 2022 at 11:48):
theorem six (a b c d e f g : Bool) : Bool := a ∧ b ∧ c ∧ d ∧ e ∧ f ∧ g
theorem six' (a b c d e f g h : Bool) : Bool := a ∧ b ∧ c ∧ d ∧ e ∧ f ∧ (g ∧ h : Bool)
#print six
/-
theorem six : Bool → Bool → Bool → Bool → Bool → Bool → Bool → Bool :=
fun a b c d e f g => decide (a = true ∧ b = true ∧ c = true ∧ d = true ∧ e = true ∧ f = true ∧ g = true)
-/
#print six'
/-
theorem six : Bool → Bool → Bool → Bool → Bool → Bool → Bool → Bool :=
fun a b c d e f g => decide (a = true ∧ b = true ∧ c = true ∧ d = true ∧ e = true ∧ f = true ∧ g = true)
-/
Eric Wieser (Dec 22 2022 at 11:48):
Does adding a direct call to decide on seven solve the issue?
Kevin Buzzard (Dec 22 2022 at 11:49):
Wait, the question is why the decidable Prop isn't being coerced back to a Bool
Damiano Testa (Dec 22 2022 at 11:49):
theorem seven (a b c d e f g h : Bool) : Bool := decide (a ∧ b ∧ c ∧ d ∧ e ∧ f ∧ g ∧ h)
works. Is this what you were suggesting?
Eric Wieser (Dec 22 2022 at 11:49):
Thanks @Damiano Testa, that's exactly the one I was thinking of. Does it fail for 14 or some larger number?
Damiano Testa (Dec 22 2022 at 11:49):
Ok, I am slightly less puzzled now, but I am still surprised by the behaviour!
Kevin Buzzard (Dec 22 2022 at 11:50):
Damiano if you actually want to do this you should be using Boolean and, not proppy and
Eric Wieser (Dec 22 2022 at 11:50):
Which I assume is spelt && (edit: docs4#and)
Kevin Buzzard (Dec 22 2022 at 11:51):
It's Bool.And I think? Possibly with no notation
Damiano Testa (Dec 22 2022 at 11:51):
This is the first that fails:
theorem seven (a b c d e f g h : Bool) : Bool := decide (a ∧ b ∧ c ∧ d ∧ e ∧ f ∧ g ∧ h ∧ b ∧ c ∧ d ∧ e ∧ f ∧ g ∧ h ∧ f ∧ g ∧ h ∧ b ∧ c ∧ d ∧ e ∧ f ∧ g ∧ h ∧ b ∧ c ∧ d ∧ e ∧ f ∧ g ∧ h ∧ b ∧ c ∧ d ∧ e ∧ f ∧ g ∧ h
∧ b ∧ c ∧ d ∧ e ∧ f ∧ g ∧ h ∧ b ∧ c ∧ d ∧ e ∧ f ∧ g ∧ h ∧ b ∧ c ∧ d ∧ e ∧ f ∧ g ∧ h ∧ b ∧ c ∧ d ∧ e ∧ a)
Eric Wieser (Dec 22 2022 at 11:51):
What's the failure message?
Damiano Testa (Dec 22 2022 at 11:51):
Failure:
/-
ands7.lean:19:0
Messages (1)
ands7.lean:19:49
failed to synthesize instance
Decidable
(a = true ∧
b = true ∧
c = true ∧
d = true ∧
e = true ∧
f = true ∧
g = true ∧
h = true ∧
b = true ∧
c = true ∧
d = true ∧
e = true ∧
f = true ∧
g = true ∧
h = true ∧
f = true ∧
g = true ∧
h = true ∧
b = true ∧
c = true ∧
d = true ∧
e = true ∧
f = true ∧
g = true ∧
h = true ∧
b = true ∧
c = true ∧
d = true ∧
e = true ∧
f = true ∧
g = true ∧
h = true ∧
b = true ∧
c = true ∧
d = true ∧
e = true ∧
f = true ∧
g = true ∧
h = true ∧
b = true ∧
c = true ∧
d = true ∧
e = true ∧
f = true ∧
g = true ∧
h = true ∧
b = true ∧
c = true ∧
d = true ∧
e = true ∧
f = true ∧
g = true ∧
h = true ∧
b = true ∧
c =
true ∧
d =
true ∧
e =
true ∧
f =
true ∧
g =
true ∧
h =
true ∧
b =
true ∧
c =
true ∧
d =
true ∧
e =
true ∧
a =
true)
All Messages (4)-/
Eric Wieser (Dec 22 2022 at 11:52):
That doesn't look like an error message?
Damiano Testa (Dec 22 2022 at 11:52):
Yes, sorry, copy-pasted the wrong thing.
Eric Wieser (Dec 22 2022 at 11:52):
So maybe the coercion from Bool to Prop has a super-short timeout / search depth for synthesizing instances?
Eric Wieser (Dec 22 2022 at 11:53):
Or alternatively, maybe it spends most of it's budget in the CoeTC typeclasses
Damiano Testa (Dec 22 2022 at 11:53):
I do not know, but already knowing that ∧ is "just" for Props clarified a lot!
Sebastian Ullrich (Dec 22 2022 at 11:54):
Please update your Lean version, @Gabriel Ebner fixed this yesterday
Eric Wieser (Dec 22 2022 at 11:55):
https://github.com/leanprover/lean4/pull/1981?
Sebastian Ullrich (Dec 22 2022 at 11:56):
Yes! https://github.com/leanprover/lean4/commit/6083b01c86f530e1fb037114d8c0ddd4ac2e909e
Eric Wieser (Dec 22 2022 at 11:56):
Not https://github.com/leanprover/lean4/pull/1981/commits/770ea8e730544d1a81ea19d3560bf10855ed45f9?
Eric Wieser (Dec 22 2022 at 11:56):
Oh I guess it was rebased
Damiano Testa (Dec 22 2022 at 11:57):
I am ashamed for asking, but... how do I update the lean version?
Siddhartha Gadgil (Dec 22 2022 at 12:15):
Edit the lean-toolchain file.
Damiano Testa (Dec 22 2022 at 12:22):
Siddhartha, thank you very much!
Damiano Testa (Dec 22 2022 at 12:22):
I can confirm that the issue that I had raised disappeared!
64 Bools still seem to be too many, though. :lol:
theorem seven (a b c d e f g h : Bool) : Bool := a ∧ b ∧ c ∧ d ∧ e ∧ f ∧ g ∧ h ∧ b ∧ c ∧ d ∧ e ∧ f ∧ g ∧ h ∧ f ∧ h ∧ b ∧ c ∧ d ∧ e ∧ f ∧ g ∧ h ∧ b ∧ c ∧ d ∧ e ∧ f ∧ g ∧ h ∧ b ∧ c ∧ d ∧ e ∧ f ∧ g ∧ h ∧ h ∧ h ∧ h ∧ h ∧ h
∧ h ∧ h ∧ h ∧ h ∧ h ∧ h ∧ h ∧ h ∧ h ∧ h ∧ h ∧ h ∧ h ∧ h ∧ h ∧ h ∧ h ∧ h ∧ h ∧ h ∧ h
/-
type mismatch
a = true ∧
b = true ∧
c = true ∧
d = true ∧
e = true ∧
f = true ∧
g = true ∧
h = true ∧
b = true ∧
c = true ∧
d = true ∧
e = true ∧
f = true ∧
g = true ∧
h = true ∧
f = true ∧
h = true ∧
b = true ∧
c = true ∧
d = true ∧
e = true ∧
f = true ∧
g = true ∧
h = true ∧
b = true ∧
c = true ∧
d = true ∧
e = true ∧
f = true ∧
g = true ∧
h = true ∧
b = true ∧
c = true ∧
d = true ∧
e = true ∧
f = true ∧
g = true ∧
h = true ∧
h = true ∧
h = true ∧
h = true ∧
h = true ∧
h = true ∧
h = true ∧
h = true ∧
h = true ∧
h = true ∧
h = true ∧
h = true ∧
h = true ∧
h = true ∧
h = true ∧
h = true ∧
h = true ∧
h = true ∧
h =
true ∧
h =
true ∧
h =
true ∧
h =
true ∧
h =
true ∧
h =
true ∧
h =
true ∧
h =
true ∧
h =
true
has type
Prop : Type
but is expected to have type
Bool : Type
-/
Now that I know this, this is with leanprover/lean4:nightly-2022-12-22.
Damiano Testa (Dec 22 2022 at 12:23):
Anyway, I am satisfied with the current situation! Thanks a lot to all!
Last updated: Dec 20 2023 at 11:08 UTC