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
  rw satisfiable,
  apply exists.intro V,
  trivial <-- problem here!

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