# Zulip Chat Archive

## Stream: new members

### Topic: exhausting finite possibilities

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

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

#### 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]`

.

#### Rob Lewis (Apr 21 2020 at 16:45):

(@Petar Maymounkov )

#### Scott Morrison (Apr 22 2020 at 09:12):

We really need to provide `@[derive fintype]`

!

Last updated: Dec 20 2023 at 11:08 UTC