2. Slang: Arithmetic and Boolean Expressions
We need to figure out our approach to text width, especially for proofs. Quite a few proofs here don't render into the chosen page width, and for terse mode it will be worse.
2.1. Arithmetic and Boolean Expressions
2.1.1. Syntax
namespace Slang
Abstract syntax trees for arithmetic and boolean expressions:
inductive Aexp where
| num (n : Nat)
| plus (a₁ a₂ : Aexp)
| minus (a₁ a₂ : Aexp)
| mult (a₁ a₂ : Aexp)
inductive Bexp where
| bool (b : Bool)
| eq (a₁ a₂ : Aexp)
| neq (a₁ a₂ : Aexp)
| le (a₁ a₂ : Aexp)
| gt (a₁ a₂ : Aexp)
| not (b : Bexp)
| and (b₁ b₂ : Bexp)
2.1.2. Evaluation
Evaluating an arithmetic expression produces a number.
namespace Aexp
def eval (a : Aexp) : Nat :=
match a with
| num n => n
| plus a₁ a₂ => a₁.eval + a₂.eval
| minus a₁ a₂ => a₁.eval - a₂.eval
| mult a₁ a₂ => a₁.eval * a₂.eval
@[simp] theorem eval_num (n : Nat) : (num n).eval = n := rfl
@[simp] theorem eval_plus (a₁ a₂ : Aexp) : (plus a₁ a₂).eval = a₁.eval + a₂.eval := rfl
@[simp] theorem eval_minus (a₁ a₂ : Aexp) : (minus a₁ a₂).eval = a₁.eval - a₂.eval := rfl
@[simp] theorem eval_mult (a₁ a₂ : Aexp) : (mult a₁ a₂).eval = a₁.eval * a₂.eval := rfl
example : eval (.plus (.num 2) (.num 2)) = 4 := ⊢ ((num 2).plus (num 2)).eval = 4 All goals completed! 🐙
end Aexp
Similarly, evaluating a boolean expression yields a boolean.
namespace Bexp
def eval (b : Bexp) : Bool :=
match b with
| bool b => b
| eq a₁ a₂ => a₁.eval == a₂.eval
| neq a₁ a₂ => a₁.eval != a₂.eval
| le a₁ a₂ => a₁.eval ≤ a₂.eval
| gt a₁ a₂ => a₁.eval > a₂.eval
| not b₁ => !eval b₁
| and b₁ b₂ => eval b₁ && eval b₂
@[simp] theorem eval_bool (b : Bool) : (bool b).eval = b := rfl
@[simp] theorem eval_eq (a₁ a₂ : Aexp) : (eq a₁ a₂).eval = (a₁.eval == a₂.eval) := rfl
@[simp] theorem eval_neq (a₁ a₂ : Aexp) : (neq a₁ a₂).eval = (a₁.eval != a₂.eval) := rfl
@[simp] theorem eval_le (a₁ a₂ : Aexp) : (le a₁ a₂).eval = (a₁.eval ≤ a₂.eval : Bool) := rfl
@[simp] theorem eval_gt (a₁ a₂ : Aexp) : (gt a₁ a₂).eval = (a₁.eval > a₂.eval : Bool) := rfl
@[simp] theorem eval_not (b : Bexp) : (not b).eval = !b.eval := rfl
@[simp] theorem eval_and (b₁ b₂ : Bexp) : (and b₁ b₂).eval = (b₁.eval && b₂.eval) := rfl
end Bexp
It's worth noting that ≤ and > are Prop-valued, i.e. a₁.eval st ≤ a₂.eval st is a proposition,
but Bexp.eval returns a Bool, so Lean implicitly inserts a decide coercion.
You can observe the call to decide by hovering over Bexp.eval_le and Bexp.eval_gt.
What does the following expression evaluate to?
Aexp.eval (.plus (.num 3) (.minus (.num 4) (.num 1)))
(A) true (B) false (C) 0 (D) 3 (E) 6
Show solution
(E) 6
2.1.3. Optimization
namespace Aexp
def optimize0plus (a : Aexp) : Aexp :=
match a with
| num n => num n
| plus (num 0) e₂ => optimize0plus e₂
| plus e₁ e₂ => plus (optimize0plus e₁) (optimize0plus e₂)
| minus e₁ e₂ => minus (optimize0plus e₁) (optimize0plus e₂)
| mult e₁ e₂ => mult (optimize0plus e₁) (optimize0plus e₂)
example :
Aexp.optimize0plus (.plus (.num 2)
(.plus (.num 0)
(.plus (.num 0) (.num 1))))
= .plus (.num 2) (.num 1) := ⊢ ((num 2).plus ((num 0).plus ((num 0).plus (num 1)))).optimize0plus = (num 2).plus (num 1) All goals completed! 🐙
theorem optimize0plus_sound (a : Aexp) :
a.optimize0plus.eval = a.eval := a:Aexp⊢ a.optimize0plus.eval = a.eval
induction a with
n:Nat⊢ (num n).optimize0plus.eval = (num n).eval All goals completed! 🐙
a₁:Aexpa₂:Aexpih₁:a₁.optimize0plus.eval = a₁.evalih₂:a₂.optimize0plus.eval = a₂.eval⊢ (a₁.plus a₂).optimize0plus.eval = (a₁.plus a₂).eval
cases a₁ with
a₂:Aexpih₂:a₂.optimize0plus.eval = a₂.evaln:Natih₁:(num n).optimize0plus.eval = (num n).eval⊢ ((num n).plus a₂).optimize0plus.eval = ((num n).plus a₂).eval
cases n with
a₂:Aexpih₂:a₂.optimize0plus.eval = a₂.evalih₁:(num 0).optimize0plus.eval = (num 0).eval⊢ ((num 0).plus a₂).optimize0plus.eval = ((num 0).plus a₂).eval
a₂:Aexpih₂:a₂.optimize0plus.eval = a₂.evalih₁:(num 0).optimize0plus.eval = (num 0).eval⊢ a₂.optimize0plus.eval = a₂.eval
All goals completed! 🐙
a₂:Aexpih₂:a₂.optimize0plus.eval = a₂.evaln:Natih₁:(num (n + 1)).optimize0plus.eval = (num (n + 1)).eval⊢ ((num (n + 1)).plus a₂).optimize0plus.eval = ((num (n + 1)).plus a₂).eval
a₂:Aexpih₂:a₂.optimize0plus.eval = a₂.evaln:Natih₁:(num (n + 1)).optimize0plus.eval = (num (n + 1)).eval⊢ n + 1 + a₂.optimize0plus.eval = n + 1 + a₂.eval
All goals completed! 🐙
a₂:Aexpih₂:a₂.optimize0plus.eval = a₂.evalb₁:Aexpb₂:Aexpih₁:(b₁.plus b₂).optimize0plus.eval = (b₁.plus b₂).eval⊢ ((b₁.plus b₂).plus a₂).optimize0plus.eval = ((b₁.plus b₂).plus a₂).eval
a₂:Aexpih₂:a₂.optimize0plus.eval = a₂.evalb₁:Aexpb₂:Aexpih₁:(b₁.plus b₂).optimize0plus.eval = b₁.eval + b₂.eval⊢ (b₁.plus b₂).optimize0plus.eval + a₂.optimize0plus.eval = b₁.eval + b₂.eval + a₂.eval
All goals completed! 🐙
a₂:Aexpih₂:a₂.optimize0plus.eval = a₂.evalb₁:Aexpb₂:Aexpih₁:(b₁.minus b₂).optimize0plus.eval = (b₁.minus b₂).eval⊢ ((b₁.minus b₂).plus a₂).optimize0plus.eval = ((b₁.minus b₂).plus a₂).eval
a₂:Aexpih₂:a₂.optimize0plus.eval = a₂.evalb₁:Aexpb₂:Aexpih₁:(b₁.optimize0plus.minus b₂.optimize0plus).eval = (b₁.minus b₂).eval⊢ (b₁.optimize0plus.minus b₂.optimize0plus).eval + a₂.optimize0plus.eval = (b₁.minus b₂).eval + a₂.eval
All goals completed! 🐙
a₂:Aexpih₂:a₂.optimize0plus.eval = a₂.evalb₁:Aexpb₂:Aexpih₁:(b₁.mult b₂).optimize0plus.eval = (b₁.mult b₂).eval⊢ ((b₁.mult b₂).plus a₂).optimize0plus.eval = ((b₁.mult b₂).plus a₂).eval
a₂:Aexpih₂:a₂.optimize0plus.eval = a₂.evalb₁:Aexpb₂:Aexpih₁:(b₁.optimize0plus.mult b₂.optimize0plus).eval = (b₁.mult b₂).eval⊢ (b₁.optimize0plus.mult b₂.optimize0plus).eval + a₂.optimize0plus.eval = (b₁.mult b₂).eval + a₂.eval
All goals completed! 🐙
a₁:Aexpa₂:Aexpih₁:a₁.optimize0plus.eval = a₁.evalih₂:a₂.optimize0plus.eval = a₂.eval⊢ (a₁.minus a₂).optimize0plus.eval = (a₁.minus a₂).eval
a₁:Aexpa₂:Aexpih₁:a₁.optimize0plus.eval = a₁.evalih₂:a₂.optimize0plus.eval = a₂.eval⊢ a₁.optimize0plus.eval - a₂.optimize0plus.eval = a₁.eval - a₂.eval
All goals completed! 🐙
a₁:Aexpa₂:Aexpih₁:a₁.optimize0plus.eval = a₁.evalih₂:a₂.optimize0plus.eval = a₂.eval⊢ (a₁.mult a₂).optimize0plus.eval = (a₁.mult a₂).eval
a₁:Aexpa₂:Aexpih₁:a₁.optimize0plus.eval = a₁.evalih₂:a₂.optimize0plus.eval = a₂.eval⊢ a₁.optimize0plus.eval * a₂.optimize0plus.eval = a₁.eval * a₂.eval
All goals completed! 🐙
We can use fun_induction to achieve a much shorter proof.
theorem optimize0plus_sound' (a : Aexp) :
a.optimize0plus.eval = a.eval := a:Aexp⊢ a.optimize0plus.eval = a.eval
n✝:Nat⊢ (num n✝).eval = (num n✝).evale₂✝:Aexpih1✝:e₂✝.optimize0plus.eval = e₂✝.eval⊢ e₂✝.optimize0plus.eval = ((num 0).plus e₂✝).evale₁✝:Aexpe₂✝:Aexpx✝:e₁✝ = num 0 → Falseih2✝:e₁✝.optimize0plus.eval = e₁✝.evalih1✝:e₂✝.optimize0plus.eval = e₂✝.eval⊢ (e₁✝.optimize0plus.plus e₂✝.optimize0plus).eval = (e₁✝.plus e₂✝).evale₁✝:Aexpe₂✝:Aexpih2✝:e₁✝.optimize0plus.eval = e₁✝.evalih1✝:e₂✝.optimize0plus.eval = e₂✝.eval⊢ (e₁✝.optimize0plus.minus e₂✝.optimize0plus).eval = (e₁✝.minus e₂✝).evale₁✝:Aexpe₂✝:Aexpih2✝:e₁✝.optimize0plus.eval = e₁✝.evalih1✝:e₂✝.optimize0plus.eval = e₂✝.eval⊢ (e₁✝.optimize0plus.mult e₂✝.optimize0plus).eval = (e₁✝.mult e₂✝).eval n✝:Nat⊢ (num n✝).eval = (num n✝).evale₂✝:Aexpih1✝:e₂✝.optimize0plus.eval = e₂✝.eval⊢ e₂✝.optimize0plus.eval = ((num 0).plus e₂✝).evale₁✝:Aexpe₂✝:Aexpx✝:e₁✝ = num 0 → Falseih2✝:e₁✝.optimize0plus.eval = e₁✝.evalih1✝:e₂✝.optimize0plus.eval = e₂✝.eval⊢ (e₁✝.optimize0plus.plus e₂✝.optimize0plus).eval = (e₁✝.plus e₂✝).evale₁✝:Aexpe₂✝:Aexpih2✝:e₁✝.optimize0plus.eval = e₁✝.evalih1✝:e₂✝.optimize0plus.eval = e₂✝.eval⊢ (e₁✝.optimize0plus.minus e₂✝.optimize0plus).eval = (e₁✝.minus e₂✝).evale₁✝:Aexpe₂✝:Aexpih2✝:e₁✝.optimize0plus.eval = e₁✝.evalih1✝:e₂✝.optimize0plus.eval = e₂✝.eval⊢ (e₁✝.optimize0plus.mult e₂✝.optimize0plus).eval = (e₁✝.mult e₂✝).eval All goals completed! 🐙
end Aexp
Since the Aexp.optimize0plus transformation doesn't change the value of an
Aexp, we should be able to apply it to all the Aexps that appear in a
Bexp without changing the Bexp's value. Write a function that
performs this transformation on Bexps and prove it sound. Use the
combinators we've just seen to make the proof as short and elegant as
possible.
def Bexp.optimize0plus (b : Bexp) : Bexp := sorry
theorem Bexp.optimize0plus_test1 :
Bexp.optimize0plus
(.not (.gt (.plus (.num 0) (.num 4)) (.num 8)))
= (.not (.gt (.num 4) (.num 8))) := sorry
theorem Bexp.optimize0plus_test2 :
Bexp.optimize0plus
(.and (.le (.plus (.num 0) (.num 4)) (.num 5)) (.bool true))
= (.and (.le (.num 4) (.num 5)) (.bool true)) := sorry
theorem Bexp.optimize0plus_sound (b : Bexp) :
b.optimize0plus.eval = b.eval := b:Bexp⊢ b.optimize0plus.eval = b.eval
All goals completed! 🐙
The optimization implemented by our Aexp.optimize0plus is only one of
many possible optimizations on arithmetic and boolean expressions. Write a more
sophisticated optimizer and prove it correct. (You will probably find it easiest
to start small -- add just a single, simple optimization and its correctness proof --
and build up incrementally to something more interesting.)
2.2. Evaluation as a Relation
inductive Aexp.EvalR : Aexp → Nat → Prop where
| num (n : Nat) : EvalR (.num n) n
| plus {a₁ a₂ : Aexp} {n₁ n₂ : Nat} (h₁ : EvalR a₁ n₁) (h₂ : EvalR a₂ n₂) :
EvalR (.plus a₁ a₂) (n₁ + n₂)
| minus {a₁ a₂ : Aexp} {n₁ n₂ : Nat} (h₁ : EvalR a₁ n₁) (h₂ : EvalR a₂ n₂) :
EvalR (.minus a₁ a₂) (n₁ - n₂)
| mult {a₁ a₂ : Aexp} {n₁ n₂ : Nat} (h₁ : EvalR a₁ n₁) (h₂ : EvalR a₂ n₂) :
EvalR (.mult a₁ a₂) (n₁ * n₂)
One comment on the style of this definition. We could instead have presented this relation with positional hypotheses -- no names for the premises.
namespace ArithUnnamed
inductive Aexp.EvalR : Aexp → Nat → Prop where
| num (n : Nat) : EvalR (.num n) n
| plus {a₁ a₂ : Aexp} {n₁ n₂ : Nat} : EvalR a₁ n₁ → EvalR a₂ n₂ → EvalR (.plus a₁ a₂) (n₁ + n₂)
| minus {a₁ a₂ : Aexp} {n₁ n₂ : Nat} : EvalR a₁ n₁ → EvalR a₂ n₂ → EvalR (.minus a₁ a₂) (n₁ - n₂)
| mult {a₁ a₂ : Aexp} {n₁ n₂ : Nat} : EvalR a₁ n₁ → EvalR a₂ n₂ → EvalR (.mult a₁ a₂) (n₁ * n₂)
end ArithUnnamed
It will be convenient to have an infix notation for Aexp.EvalR. We'll
write e ⇓ n to mean that arithmetic expression e evaluates to
value n. The ⇓ symbol is typed \Downarrow.
namespace Aexp
scoped notation:55 e:56 " ⇓ " n:56 => EvalR e n
2.2.1. Inference Rule Notation
Which rules are needed to prove the following?
.mult (.plus (.num 3) (.num 1)) (.num 0) ⇓ 0
(A) num and plus
(B) num only
(C) num and mult
(D) mult and plus
(E) num, mult, and plus
Show solution
(E) num, mult, and plus
Not sure if we need ⇓b, or whether we can define ⇓ overloaded. Don't understand Lean notation yet!
About Bexp.eval below: We should discuss a way to recall definitions without
having to write them out manually like this. I think a simple #print may work as an
alternative, assuming there are no namespace issues..
Here, again, is the definition of the Bexp.eval function:
def Bexp.eval (b : Bexp) : Bool :=
match b with
| bool b => b
| eq a₁ a₂ => a₁.eval == a₂.eval
| neq a₁ a₂ => a₁.eval != a₂.eval
| le a₁ a₂ => a₁.eval ≤ a₂.eval
| gt a₁ a₂ => a₁.eval > a₂.eval
| not b₁ => !eval b₁
| and b₁ b₂ => eval b₁ && eval b₂
Write out a corresponding definition of boolean evaluation as a relation in inference rule notation.
2.2.2. Equivalence of the Definitions
It is straightforward to prove that the relational and functional definitions of evaluation agree.
theorem evalR_iff_eval (a : Aexp) (n : Nat) :
a ⇓ n ↔ a.eval = n := a:Aexpn:Nat⊢ a ⇓ n ↔ a.eval = n
a:Aexpn:Nat⊢ a ⇓ n → a.eval = na:Aexpn:Nat⊢ a.eval = n → a ⇓ n
a:Aexpn:Nat⊢ a ⇓ n → a.eval = n a:Aexpn:Nath:a ⇓ n⊢ a.eval = n
induction h with
a:Aexpn✝:Natn:Nat⊢ (num n).eval = n All goals completed! 🐙
a:Aexpn:Nata₁✝:Aexpa₂✝:Aexpn₁✝:Natn₂✝:Nath₁:a₁✝ ⇓ n₁✝h₂:a₂✝ ⇓ n₂✝ih₁:a₁✝.eval = n₁✝ih₂:a₂✝.eval = n₂✝⊢ (a₁✝.plus a₂✝).eval = n₁✝ + n₂✝ a:Aexpn:Nata₁✝:Aexpa₂✝:Aexpn₁✝:Natn₂✝:Nath₁:a₁✝ ⇓ n₁✝h₂:a₂✝ ⇓ n₂✝ih₁:a₁✝.eval = n₁✝ih₂:a₂✝.eval = n₂✝⊢ a₁✝.eval + a₂✝.eval = n₁✝ + n₂✝; All goals completed! 🐙
a:Aexpn:Nata₁✝:Aexpa₂✝:Aexpn₁✝:Natn₂✝:Nath₁:a₁✝ ⇓ n₁✝h₂:a₂✝ ⇓ n₂✝ih₁:a₁✝.eval = n₁✝ih₂:a₂✝.eval = n₂✝⊢ (a₁✝.minus a₂✝).eval = n₁✝ - n₂✝ a:Aexpn:Nata₁✝:Aexpa₂✝:Aexpn₁✝:Natn₂✝:Nath₁:a₁✝ ⇓ n₁✝h₂:a₂✝ ⇓ n₂✝ih₁:a₁✝.eval = n₁✝ih₂:a₂✝.eval = n₂✝⊢ a₁✝.eval - a₂✝.eval = n₁✝ - n₂✝; All goals completed! 🐙
a:Aexpn:Nata₁✝:Aexpa₂✝:Aexpn₁✝:Natn₂✝:Nath₁:a₁✝ ⇓ n₁✝h₂:a₂✝ ⇓ n₂✝ih₁:a₁✝.eval = n₁✝ih₂:a₂✝.eval = n₂✝⊢ (a₁✝.mult a₂✝).eval = n₁✝ * n₂✝ a:Aexpn:Nata₁✝:Aexpa₂✝:Aexpn₁✝:Natn₂✝:Nath₁:a₁✝ ⇓ n₁✝h₂:a₂✝ ⇓ n₂✝ih₁:a₁✝.eval = n₁✝ih₂:a₂✝.eval = n₂✝⊢ a₁✝.eval * a₂✝.eval = n₁✝ * n₂✝; All goals completed! 🐙
a:Aexpn:Nat⊢ a.eval = n → a ⇓ n a:Aexpn:Nath:a.eval = n⊢ a ⇓ n
a:Aexp⊢ a ⇓ a.eval
induction a with
n:Nat⊢ num n ⇓ (num n).eval All goals completed! 🐙
a₁:Aexpa₂:Aexpih₁:a₁ ⇓ a₁.evalih₂:a₂ ⇓ a₂.eval⊢ a₁.plus a₂ ⇓ (a₁.plus a₂).eval All goals completed! 🐙
a₁:Aexpa₂:Aexpih₁:a₁ ⇓ a₁.evalih₂:a₂ ⇓ a₂.eval⊢ a₁.minus a₂ ⇓ (a₁.minus a₂).eval All goals completed! 🐙
a₁:Aexpa₂:Aexpih₁:a₁ ⇓ a₁.evalih₂:a₂ ⇓ a₂.eval⊢ a₁.mult a₂ ⇓ (a₁.mult a₂).eval All goals completed! 🐙
We can make the proof quite a bit shorter using more automation like we did in the previous section.
theorem evalR_iff_eval' (a : Aexp) (n : Nat) :
a ⇓ n ↔ a.eval = n := a:Aexpn:Nat⊢ a ⇓ n ↔ a.eval = n
All goals completed! 🐙
end Aexp
Write a relation Bexp.EvalR in the same style as Aexp.EvalR, and prove that
it is equivalent to Bexp.eval.
namespace Bexp
open scoped Aexp -- opens the ⇓ notation for Aexp.EvalR
inductive EvalR : Bexp → Bool → Prop where
-- FILL IN HERE
scoped notation:55 e:56 " ⇓ " b:56 => EvalR e b
theorem evalR_iff_eval (b : Bexp) (bv : Bool) :
b ⇓ bv ↔ b.eval = bv := b:Bexpbv:Bool⊢ b ⇓ bv ↔ b.eval = bv
All goals completed! 🐙
end Bexp
end Slang
2.2.3. Computational vs. Relational Definitions
Sometimes relational definitions are the only reasonable option...
namespace Slang.AevalRDivision
For example, suppose that we wanted to extend the arithmetic operations with division:
inductive Aexp where
| num (n : Nat)
| plus (a₁ a₂ : Aexp)
| minus (a₁ a₂ : Aexp)
| mult (a₁ a₂ : Aexp)
| div (a₁ a₂ : Aexp) -- NEW
Extending the definition of Aexp.eval to handle this new operation would
not be straightforward due to division being a partial operation; i.e.,
what should we return as the result of .div (.num 5) (.num 0)?
One option would be to lift the definition of Aexp.eval to return an option:
namespace Aexp
def eval (a : Aexp) : Option Nat :=
match a with
| num n => some n
| plus a₁ a₂ => match a₁.eval, a₂.eval with
| some n₁, some n₂ => some (n₁ + n₂)
| _, _ => none
| minus a₁ a₂ => match a₁.eval, a₂.eval with
| some n₁, some n₂ => some (n₁ - n₂)
| _, _ => none
| mult a₁ a₂ => match a₁.eval, a₂.eval with
| some n₁, some n₂ => some (n₁ * n₂)
| _, _ => none
| div a₁ a₂ => match a₁.eval, a₂.eval with
| _, some 0 => none
| some n₁, some n₂ => if n₂ ∣ n₁ then some (n₁ / n₂) else none
| _, _ => none
end Aexp
This definition is a lot wordier than the earlier version. There are tools to reduce this overhead, namely monads, but we will not discuss these in Software Foundations in Lean. Curious readers can learn more about them from Functional Programming in Lean.
By contrast, partiality is no problem for the relational version of the definition.
What should Aexp.eval return for .div (.num 1) (.num 0)??
inductive Aexp.EvalR : Aexp → Nat → Prop where
| num (n : Nat) : EvalR (.num n) n
| plus (a₁ a₂ : Aexp) (n₁ n₂ : Nat) (h₁ : EvalR a₁ n₁) (h₂ : EvalR a₂ n₂) :
EvalR (.plus a₁ a₂) (n₁ + n₂)
| minus (a₁ a₂ : Aexp) (n₁ n₂ : Nat) (h₁ : EvalR a₁ n₁) (h₂ : EvalR a₂ n₂) :
EvalR (.minus a₁ a₂) (n₁ - n₂)
| mult (a₁ a₂ : Aexp) (n₁ n₂ : Nat) (h₁ : EvalR a₁ n₁) (h₂ : EvalR a₂ n₂) :
EvalR (.mult a₁ a₂) (n₁ * n₂)
| div (a₁ a₂ : Aexp) (n₁ n₂ n₃ : Nat) -- NEW
(h₁ : EvalR a₁ n₁) (h₂ : EvalR a₂ n₂) (hpos : n₂ > 0) (hdiv : n₂ * n₃ = n₁) :
EvalR (.div a₁ a₂) n₃
Notice that there are some inputs (those with a divisor of 0) for which this relation does not specify an output.
end Slang.AevalRDivision
namespace Slang.AevalRExtended
Another example: a nondeterministic number generator:
As another example, suppose that we want to extend the arithmetic operations by a
nondeterministic number generator any that, when evaluated, may
yield any number. (This is not the same as making a probabilistic
choice among all numbers -- we only say which results are possible.)
inductive Aexp where
| any -- NEW
| num (n : Nat)
| plus (a₁ a₂ : Aexp)
| minus (a₁ a₂ : Aexp)
| mult (a₁ a₂ : Aexp)
Again, extending Aexp.eval would be tricky, since evaluation is now not
a deterministic function from expressions to numbers; but extending the
relation is no problem.
What should Aexp.eval do with nondeterminism??
inductive Aexp.EvalR : Aexp → Nat → Prop where
| any (n : Nat) : EvalR .any n -- NEW
| num (n : Nat) : EvalR (.num n) n
| plus (a₁ a₂ : Aexp) (n₁ n₂ : Nat) (h₁ : EvalR a₁ n₁) (h₂ : EvalR a₂ n₂) :
EvalR (.plus a₁ a₂) (n₁ + n₂)
| minus (a₁ a₂ : Aexp) (n₁ n₂ : Nat) (h₁ : EvalR a₁ n₁) (h₂ : EvalR a₂ n₂) :
EvalR (.minus a₁ a₂) (n₁ - n₂)
| mult (a₁ a₂ : Aexp) (n₁ n₂ : Nat) (h₁ : EvalR a₁ n₁) (h₂ : EvalR a₂ n₂) :
EvalR (.mult a₁ a₂) (n₁ * n₂)
end Slang.AevalRExtended
Functional: computation. Relational: expressive. Best: both, proved equivalent.