Zulip Chat Archive

Stream: new members

Topic: exhausting finite possibilities

view this post on Zulip Petar Maymounkov (Apr 21 2020 at 15:36):

(Carrying this over from a google group post)
I am trying to understand how to write a simple exhaustive search (in proof space) in Lean.

-- Suppose I have a finite inductive type, e.g.

inductive bit : Type
| zero : bit
| one : bit

-- I'd like to prove that among all functions over bits, there exists a constant, i.e.

lemma exist_constant : \exist f : bit -> bit, \all x : bit, f x = x

-- I'd like to prove this with a tactic that exhaustively check the finitely many possibilities for a function in bit -> bit.

Is that possible?

Mario had answered that this is possible, using dec_trivial. Being fairly new to Lean, I need a bit more help: Is there a link to an example usage of dec_trivial? Or part of the documentation/books I should focus on reading?

Thank you!

view this post on Zulip Dan Stanescu (Apr 21 2020 at 16:32):

This looks like the identity function to me, not a constant.
Wouldn't a constant rather be something like this below?
lemma exist_constant : \exist f : bit -> bit, \all x : bit, f x = zero

view this post on Zulip Rob Lewis (Apr 21 2020 at 16:45):

Yes, the name exist_constant isn't exactly right. Also, FYI, you can write Lean code in this chat by enclosing it in triple backticks ```

The following works for your example:

import tactic

@[derive decidable_eq]
inductive bit : Type
| zero : bit
| one : bit

instance : fintype bit :=
[bit.zero, bit.one].to_finset, by {rintro ⟨⟩; exact dec_trivial}

example :  f : bit  bit,  b : bit, f b = b := dec_trivial

You can read a bit about dec_trivial in Theorem Proving in Lean . The idea is that for a closed proposition (no free variables), if Lean can infer an instance that the proposition is decidable, it can evaluate that instance. In this case, there's a library instance that says quantifiers over a finite type are decidable. So we just need to add an instance that shows bit is finite.

Notice we also use dec_trivial in defining the instance. That's because it's decidable that bit.zero ∈ [bit.zero, bit.one] and bit.one ∈ [bit.zero, bit.one].

view this post on Zulip Rob Lewis (Apr 21 2020 at 16:45):

(@Petar Maymounkov )

view this post on Zulip Scott Morrison (Apr 22 2020 at 09:12):

We really need to provide @[derive fintype]!

Last updated: May 14 2021 at 07:19 UTC