Trivial tactic not working as I expected it to

Stream: new members

[Kasper]

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]

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

[Notification Bot]

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

[Floris van Doorn]

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

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]

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]

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]

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")