Defining a Semantic evaluator for Props

Stream: lean4

[Bernardo Borges]

While learning logic, I find the two definitions of consequence quite interesting:

Syntactic consequence Γ ⊢ φ says: sentence φ is provable from the set of assumptions Γ.

Semantic consequence Γ ⊨ φ says: sentence φ is true in all models of Γ.

The Syntactic consequence is the natural way of proving theorems in lean, by manipulating assumptions. In this sense, I am interested in creating a Semantic consequence evaluation for some Prop in Lean. This function should try to valorate the atomic props in the context (Values that make all hypothesis true) and then derive true for the consequence in all these.

def semantic [Decidable α] (α : Prop) : Bool :=
  if h : α then true else false

In this first implementation I am stuck with the error

failed to synthesize instance
  Decidable α

Any suggestions?

[Ruben Van de Velde]

Reorder your arguments, you're asking for a property of \a before you define \a

[Ruben Van de Velde]

If you look in the infoview, you'll probably see there's two \a's

[Bernardo Borges]

Given the fix, I wish it would prove statements like this:

def semantic (α : Prop) [Decidable α] : Bool :=
  if h : α then true else false

variable {P Q : Prop}
#eval semantic (P ∨ Q)

In the sense that, choose either P is true or P is false, also for Q, the OR can be satisfied. But I am getting the same typeclass problem:

failed to synthesize instance
  Decidable (P ∨ Q)

[Henrik Böving]

That's because you are not providing Decidable instances for the propositions P an Q in your example.

[Bernardo Borges]

I might me wanting too much. How can I express the search for all possible values for P and Q and then find if some is proved?

[Henrik Böving]

I don't really understand what you want to do here? your semantic function says "I want a decidable property" Deciding an or is only possible if the properties it is made of are decidable.

Your example is basically telling Lean "I have two properties P and Q that I know absolutely nothing about, figure out whether P or Q is decidable" and of course it cannot do that, after all for all Lean knows both might be undecidable. If you provided it with this information like so:

variable {P Q : Prop} [Decidable P] [Decidable Q]
#check semantic (P ∨ Q)

It will happily do that. You can however still not evaluate this code because again P and Q are completely opaque propositions that we know nothing about.

[Henrik Böving]

A search for "all possible values of P and Q" is not possible since there are infinitely many possible propositions out there. What you can do is use Bool instead of Prop and start working with either manual case bashing or LeanSAT: https://github.com/leanprover/leansat to figure out whether your formula is satisfiable or not

[Bernardo Borges]

Interesting. Can I define P and Q to be either False or True but not a composite expression? This way I could try to evaluate them using excluded middle (maybe). This semantic argument is basically "build the truth table for the hypothesis, filter the ones that make all hypothesis true. Then check if all them make the consequence true" Hypothesis in this case is P, Q

[Yaël Dillies]

Are you looking for docs#Bool ?

[Bernardo Borges]

Some cases of what I was hoping to achieve:

semantic (P \or Q) ==> true
semantic (\notP \and P) ==> false
semantic ( (P \r Q) \and P \and Q) ==> true
semantic ( (P \r Q) \and \notQ \and P) ==> true

[Enrico Borba]

It sounds like you want a function that returns whether a boolean formula is satisfiable

[Enrico Borba]

Not sure why

semantic (P \or Q) ==> true

would be obviously true. Is there a typo here?

[Bernardo Borges]

Yes, satisfiable. It means the expression is not a contradiction

[Bernardo Borges]

Thinking about it, I might need some metaprogramming, to handle the Prop type, parse it, then identify all free variables, then pick values for them, then map the operations to boolean ones (\and to &&) and return true iff some satisfiable was found. Does this sound promising?

[Yaël Dillies]

Do you know about the two projects called Leansat?

[Bernardo Borges]

I didn't know about it! I'll take a look now, thanks :+1: