exhausting finite possibilities

Stream: new members

[Petar Maymounkov]

(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!

[Dan Stanescu]

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

[Rob Lewis]

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

[Rob Lewis]

(@Petar Maymounkov )

[Scott Morrison]

We really need to provide @[derive fintype]!