implementation of evaluation of a real-valued logic

Stream: general

[Alexandre Rademaker]

I am trying to implement a real-valued logic starting from the definition of the language and a simple eval function. Formulas are propositional logic formulas. Propositions are interpreted into interval of real values.

import data.real.basic

structure interval :=
 mk :: (l : ℝ) (h : ℝ)

inductive Expr : Type
  | atom : interval → Expr
  | neg  : Expr → Expr
  | and  : Expr → Expr → Expr
  |  or  : Expr → Expr → Expr

open Expr
variables a b : interval

#check and (or (atom a) (atom b)) (or (atom a) (atom b))

def eval : Expr → interval
 | (atom i) := i
 | (and e1 e2) := interval.mk ((eval e1).h + (eval e2).h) ((eval e1).l + (eval e2).l)
 | _ := interval.mk 0 0

def e1 : Expr := atom (interval.mk 0 1)
#reduce eval (and e1 e1)

But I got a timeout in the reduce! Why?

[Alexandre Rademaker]

The eval of and is not final, just testing the ideas.

[Kevin Buzzard]

If you try #eval instead of #reduce you'll see why you're getting a timeout!

[Kevin Buzzard]

Even #reduce (0 : ℝ) times out.

[Alexandre Rademaker]

Hum, so cant I play with reals in Lean?

[Kevin Buzzard]

We play with them all the time! We just don't try to evaluate them :-)

[Rob Lewis]

Here's how I would do this, using rat and #eval instead of real and #reduce:

import data.rat

structure interval :=
 mk :: (l : ℚ) (h : ℚ)

instance : has_repr interval :=
⟨λ i, match i with
| ⟨l, h⟩ := sformat!"⟨{l}, {h}⟩"
end⟩

inductive Expr : Type
  | atom : interval → Expr
  | neg  : Expr → Expr
  | and  : Expr → Expr → Expr
  |  or  : Expr → Expr → Expr

open Expr
variables a b : interval

#check and (or (atom a) (atom b)) (or (atom a) (atom b))

def eval : Expr → interval
 | (atom i) := i
 | (and e1 e2) := interval.mk ((eval e1).h + (eval e2).h) ((eval e1).l + (eval e2).l)
 | _ := interval.mk 0 0

def e1 : Expr := atom (interval.mk 0 1)

#eval eval (and e1 e1)

[Adam Topaz]

Unfortunately, for continuous logic the quantifiers are inf and sup, so one must really use real numbers :)
I should add that I think it would be VERY interesting to formalize stuff around continuous logic!

[Alexandre Rademaker]

A stupid question: what is the problema with reals? Why can't we evaluate them? does Lean 4 will solve this limitation?

[Reid Barton]

Well they do go on forever