Boolean expressions of counter programs

Expressions of counter programs (Turing.CounterProgram.Expr) compute natural numbers. A Boolean value b is represented by b.toNat, so comparisons, connectives, finite conjunctions and disjunctions, and conditionals are again expressions. Each lemma below states the value of a combinator from the values of its arguments, in the form e.eval regs = b.toNat for Boolean results. Digits in a radix are expressions too (Turing.CounterProgram.Expr.ofDigits).

Main definitions

• Turing.CounterProgram.Expr.ltB, Turing.CounterProgram.Expr.eqB: comparisons.
• Turing.CounterProgram.Expr.notB, Turing.CounterProgram.Expr.andB, Turing.CounterProgram.Expr.orB, Turing.CounterProgram.Expr.allB, Turing.CounterProgram.Expr.anyB: connectives.
• Turing.CounterProgram.Expr.iteB: a conditional on a Boolean expression.
• Turing.CounterProgram.Expr.ofDigits: the number with given digits in a radix.

Main results

• Turing.CounterProgram.Expr.eval_ltB, Turing.CounterProgram.Expr.eval_eqB, Turing.CounterProgram.Expr.eval_andB, …: the values of the combinators.
• Turing.CounterProgram.Expr.eval_ofDigits: the value of a number given by digits.

def Turing.CounterProgram.Expr.ltB (a b : Expr) : Expr

1 if a < b, 0 otherwise.

def Turing.CounterProgram.Expr.notB (a : Expr) : Expr

The negation of a Boolean expression.

def Turing.CounterProgram.Expr.andB (a b : Expr) : Expr

The conjunction of Boolean expressions.

def Turing.CounterProgram.Expr.orB (a b : Expr) : Expr

The disjunction of Boolean expressions.

def Turing.CounterProgram.Expr.eqB (a b : Expr) : Expr

1 if a = b, 0 otherwise.

def Turing.CounterProgram.Expr.allB (l : List Expr) : Expr

The conjunction of a list of Boolean expressions.

def Turing.CounterProgram.Expr.anyB (l : List Expr) : Expr

The disjunction of a list of Boolean expressions.

def Turing.CounterProgram.Expr.iteB (c a b : Expr) : Expr

The value of a if the Boolean expression c holds, of b otherwise.

def Turing.CounterProgram.Expr.ofDigits (B : Expr) (l : List Expr) : Expr

The number with the digits l, least significant first, in the radix B.

@[simp]

theorem Turing.CounterProgram.Expr.eval_ltB {regs : List ℕ} {a b : Expr} : eval regs (a.ltB b) = (decide (eval regs a < eval regs b)).toNat

theorem Turing.CounterProgram.Expr.eval_notB {regs : List ℕ} {a : Expr} {p : Bool} (ha : eval regs a = p.toNat) : eval regs a.notB = (!p).toNat

theorem Turing.CounterProgram.Expr.eval_andB {regs : List ℕ} {a b : Expr} {p q : Bool} (ha : eval regs a = p.toNat) (hb : eval regs b = q.toNat) : eval regs (a.andB b) = (p && q).toNat

theorem Turing.CounterProgram.Expr.eval_orB {regs : List ℕ} {a b : Expr} {p q : Bool} (ha : eval regs a = p.toNat) (hb : eval regs b = q.toNat) : eval regs (a.orB b) = (p || q).toNat

@[simp]

theorem Turing.CounterProgram.Expr.eval_eqB {regs : List ℕ} {a b : Expr} : eval regs (a.eqB b) = (decide (eval regs a = eval regs b)).toNat

theorem Turing.CounterProgram.Expr.eval_allB {regs : List ℕ} {l : List Expr} {f : List Bool} (h : List.Forall₂ (fun (e : Expr) (p : Bool) => eval regs e = p.toNat) l f) : eval regs (allB l) = (f.all id).toNat

theorem Turing.CounterProgram.Expr.eval_anyB {regs : List ℕ} {l : List Expr} {f : List Bool} (h : List.Forall₂ (fun (e : Expr) (p : Bool) => eval regs e = p.toNat) l f) : eval regs (anyB l) = (f.any id).toNat

theorem Turing.CounterProgram.Expr.eval_allB_map {regs : List ℕ} {ι : Type u_1} (l : List ι) (e : ι → Expr) (f : ι → Bool) (h : ∀ i ∈ l, eval regs (e i) = (f i).toNat) : eval regs (allB (List.map e l)) = (l.all f).toNat

A conjunction over a list, from the values of the conjuncts.

theorem Turing.CounterProgram.Expr.eval_anyB_map {regs : List ℕ} {ι : Type u_1} (l : List ι) (e : ι → Expr) (f : ι → Bool) (h : ∀ i ∈ l, eval regs (e i) = (f i).toNat) : eval regs (anyB (List.map e l)) = (l.any f).toNat

A disjunction over a list, from the values of the disjuncts.

theorem Turing.CounterProgram.Expr.eval_allB_ofFn {regs : List ℕ} {m : ℕ} (e : Fin m → Expr) (f : Fin m → Bool) (h : ∀ (i : Fin m), eval regs (e i) = (f i).toNat) : eval regs (allB (List.ofFn e)) = ((List.ofFn f).all id).toNat

A conjunction over the elements of Fin m, from the values of the conjuncts.

theorem Turing.CounterProgram.Expr.eval_iteB {regs : List ℕ} {a b c : Expr} {p : Bool} (hc : eval regs c = p.toNat) : eval regs (c.iteB a b) = if p = true then eval regs a else eval regs b

@[simp]

theorem Turing.CounterProgram.Expr.eval_ofDigits {regs : List ℕ} (B : Expr) (l : List Expr) : eval regs (B.ofDigits l) = Nat.ofDigits (eval regs B) (List.map (fun (e : Expr) => eval regs e) l)