# Zulip Chat Archive

## Stream: new members

### Topic: Trivial tactic not working as I expected it to

#### Kasper (Jan 12 2023 at 13:05):

Hello guys,

first, I am new here so I apologize if this isn't the space to ask these questions.

I'm trying to create a SAT solver where we have variables (of type form.FVar which takes a string as parameter) and each variable is either assigned true or false. This is determined by a object of type valuation which maps a string to a boolean value.

I now want to proof the following:

Given the following SAT problem expression : "x" (just a single var x), give an potential valuation such that the entire expression evaluates to true.

In this example, such a valuation clearly exists. The mapping from "x" to true.

However, when I try to solve this simple tactic, I get a problem:

```
inductive form : Type
| FVar : string → form
def valuation := string -> bool
def valid (V : valuation) : form -> Prop
| (form.FVar s) := V s
def satisfiable (p : form) : Prop := ∃ V : valuation, valid V p
def toyexample := form.FVar "x"
lemma proof_simple : satisfiable toyexample :=
let V : valuation := λ s, if s = "x" then true else false in
begin
rw satisfiable,
apply exists.intro V,
trivial <-- problem here!
end
```

So in my proof I create a valuation V such that the entire sat expression evaluates to true. Then I use exists.intro V to use it as a witness. The goal after this step is ⊢ valid V toyexample, which I thought should be solveable with the 'trivial' tactic. However, applying this I get the following error:

```
trivial tactic failed
state:
V : valuation := λ (s : string), ite (s = "x") (to_bool true) (to_bool false)
⊢ valid V toyexample
```

I have been stuck on this for longer than I'd like to amit, any help is greatly appreciated

#### Henrik Böving (Jan 12 2023 at 13:15):

This is not a lean 4 problem at least judging by your syntax.

#### Notification Bot (Jan 12 2023 at 13:27):

This topic was moved here from #lean4 > Trivial tactic not working as I expected it to by Floris van Doorn.

#### Floris van Doorn (Jan 12 2023 at 13:36):

@Kasper Since your question is not about Lean 4, I moved it here. `trivial`

is not supposed to solve this goal.

You're transitioning between `bool`

and `Prop`

in your code, which adds the coercion `bool -> Prop`

in some places. This coercion defined to be `fun b, b = tt`

. So `exact rfl`

works instead of `trivial`

.

A maybe more systematic approach unfolds the notions in your goal to prove it: `simp_rw [toyexample, valid, V, if_pos, to_bool_true]`

(requires `import tactic.basic`

and a dependency on `mathlib`

)

#### Kasper (Jan 12 2023 at 14:10):

Thank you for the clear explanation! I noticed this when trying to debug too that bool and Prop are not always treated the same (I thought they always converted automatically).

Just a small follow up question, for debugging purposes, I have tried to #eval a Prop but the printed result is always #0 for me regardless if the Prop is true or not. If I try to eval a boolean I correctly get true or false. Is there a way to do this? Might help me in the future with debugging

#### Kevin Buzzard (Jan 12 2023 at 14:57):

Goedel's theorem says that you can't hope to eval the truth-values of Props in general. There is no algorithm for mathematics.

#### Kyle Miller (Jan 12 2023 at 15:02):

Kasper said:

Just a small follow up question, for debugging purposes, I have tried to #eval a Prop but the printed result is always #0 for me regardless if the Prop is true or not

This is sort of a long-standing "bug" in `#eval`

. When you evaluate, what happens is that Lean compiles your code to a bytecode that's then evaluated by a virtual machine. Part of compilation is erasing everything that's computationally irrelevant. This includes types (i.e., type erasure) and proofs. If you evaluate a Prop, then *everything* is erased, and `#0`

is some side-effect of the evaluator trying to get the result of the evaluation of absolutely nothing at all.

#### Kyle Miller (Jan 12 2023 at 15:13):

One way to inspect this is with

```
set_option trace.compiler true
#eval 1 = 1
```

This shows the compiled bytecode

```
[compiler.optimize_bytecode] _main 0
0: scnstr #0
1: ret
```

The `scnstr #0`

pushes a zero-argument constructor number 0 onto the stack, which is then returned with `ret`

, and then printed by the `#eval`

command (note the error "result type does not have an instance of type class 'has_repr', dumping internal representation")

Last updated: Dec 20 2023 at 11:08 UTC