Hoare Logic

4. Equiv: Program Equivalence🔗

open scoped HasEval MyGetElem Com

4.1. Behavioral Equivalence🔗

4.1.1. Definitions🔗

def Aexp.Equiv (a₁ a₂ : Aexp) : Prop := ∀ (st : State), a₁.eval st = a₂.eval st def Bexp.Equiv (b₁ b₂ : Bexp) : Prop := ∀ (st : State), b₁.eval st = b₂.eval st

We'll also define a notation for Equiv:

class Equiv (α : Type) where equiv : α → α → Prop infix:70 " ≃ " => Equiv.equiv -- you can type `≃` as \equiv instance : Equiv Aexp where equiv := Aexp.Equiv instance : Equiv Bexp where equiv := Bexp.Equiv @[simp] theorem Aexp.equiv_notation {a₁ a₂ : Aexp} : a₁.Equiv a₂ ↔ a₁ ≃ a₂ := a₁:Aexpa₂:Aexp⊢ a₁.Equiv a₂ ↔ a₁ ≃ a₂ All goals completed! 🐙 @[simp] theorem Aexp.equiv_def {a₁ a₂ : Aexp} : a₁ ≃ a₂ ↔ ∀ (st : State), a₁.eval st = a₂.eval st := a₁:Aexpa₂:Aexp⊢ a₁ ≃ a₂ ↔ ∀ (st : State), eval st a₁ = eval st a₂ All goals completed! 🐙 @[simp] theorem Bexp.equiv_notation {b₁ b₂ : Bexp} : b₁.Equiv b₂ ↔ b₁ ≃ b₂ := b₁:Bexpb₂:Bexp⊢ b₁.Equiv b₂ ↔ b₁ ≃ b₂ All goals completed! 🐙 @[simp] theorem Bexp.equiv_def {b₁ b₂ : Bexp} : b₁ ≃ b₂ ↔ ∀ (st : State), b₁.eval st = b₂.eval st := b₁:Bexpb₂:Bexp⊢ b₁ ≃ b₂ ↔ ∀ (st : State), eval st b₁ = eval st b₂ All goals completed! 🐙 example : aexp { X - X } ≃ aexp { 0 } := ⊢ aexp {X - X} ≃ aexp {0} All goals completed! 🐙 example : bexp { X - X = 0 } ≃ bexp { true } := ⊢ bexp {X - X = 0} ≃ bexp {true} All goals completed! 🐙 def Com.Equiv (c₁ c₂ : Com) : Prop := ∀ {st st' : State}, (st =[ c₁ ]=> st') ↔ (st =[ c₂ ]=> st') instance : Equiv Com where equiv := Com.Equiv @[simp] theorem Com.equiv_notation {c₁ c₂ : Com} : c₁.Equiv c₂ ↔ c₁ ≃ c₂ := c₁:Comc₂:Com⊢ c₁.Equiv c₂ ↔ c₁ ≃ c₂ All goals completed! 🐙 @[simp] theorem Com.equiv_def {c₁ c₂ : Com} : c₁ ≃ c₂ ↔ ∀ {st st' : State}, (st =[ c₁ ]=> st') ↔ (st =[ c₂ ]=> st') := c₁:Comc₂:Com⊢ c₁ ≃ c₂ ↔ ∀ {st st' : State}, (st =[ ~c₁ ]=> st') ↔ st =[ ~c₂ ]=> st' All goals completed! 🐙

4.1.2. Simple Examples🔗

namespace Com theorem declaration uses `sorry`skip_left {c : Com} : imp { skip; c } ≃ c := c:Com⊢ imp {skip; ~c} ≃ c All goals completed! 🐙
Exercise★★(skip_right)

Prove that adding a skip after a command also results in an equivalent program.

theorem declaration uses `sorry`skip_right {c : Com} : imp { c; skip } ≃ c := c:Com⊢ imp {~c; skip} ≃ c All goals completed! 🐙
theorem if_true_simple {c₁ c₂ : Com} : imp {if (true) {c₁} else {c₂}} ≃ c₁ := c₁:Comc₂:Com⊢ imp {if (true) {~c₁} else {~c₂}} ≃ c₁ c₁:Comc₂:Com⊢ ∀ {st st' : State}, (st =[ if (true) {~c₁} else {~c₂} ]=> st') ↔ st =[ ~c₁ ]=> st' c₁:Comc₂:Comst:Statest':State⊢ (st =[ if (true) {~c₁} else {~c₂} ]=> st') ↔ st =[ ~c₁ ]=> st' c₁:Comc₂:Comst:Statest':State⊢ (st =[ if (true) {~c₁} else {~c₂} ]=> st') → st =[ ~c₁ ]=> st'c₁:Comc₂:Comst:Statest':State⊢ (st =[ ~c₁ ]=> st') → st =[ if (true) {~c₁} else {~c₂} ]=> st' c₁:Comc₂:Comst:Statest':State⊢ (st =[ if (true) {~c₁} else {~c₂} ]=> st') → st =[ ~c₁ ]=> st' c₁:Comc₂:Comst:Statest':Stateh:st =[ if (true) {~c₁} else {~c₂} ]=> st'⊢ st =[ ~c₁ ]=> st' inversion h with | ifTrue hb hc => All goals completed! 🐙 | ifFalse hb hc => All goals completed! 🐙 c₁:Comc₂:Comst:Statest':State⊢ (st =[ ~c₁ ]=> st') → st =[ if (true) {~c₁} else {~c₂} ]=> st' c₁:Comc₂:Comst:Statest':Stateh:st =[ ~c₁ ]=> st'⊢ st =[ if (true) {~c₁} else {~c₂} ]=> st' c₁:Comc₂:Comst:Statest':Stateh:st =[ ~c₁ ]=> st'⊢ Bexp.eval st (bexp {true}) = true All goals completed! 🐙 theorem if_true {b : Bexp} {c₁ c₂ : Com} (hb : b ≃ bexp {true}) : imp {if (b) {c₁} else {c₂}} ≃ c₁ := b:Bexpc₁:Comc₂:Comhb:b ≃ bexp {true}⊢ imp {if (~b) {~c₁} else {~c₂}} ≃ c₁ b:Bexpc₁:Comc₂:Comhb:b ≃ bexp {true}⊢ ∀ {st st' : State}, (st =[ if (~b) {~c₁} else {~c₂} ]=> st') ↔ st =[ ~c₁ ]=> st' b:Bexpc₁:Comc₂:Comhb:b ≃ bexp {true}st:Statest':State⊢ (st =[ if (~b) {~c₁} else {~c₂} ]=> st') ↔ st =[ ~c₁ ]=> st' b:Bexpc₁:Comc₂:Comhb:b ≃ bexp {true}st:Statest':State⊢ (st =[ if (~b) {~c₁} else {~c₂} ]=> st') → st =[ ~c₁ ]=> st'b:Bexpc₁:Comc₂:Comhb:b ≃ bexp {true}st:Statest':State⊢ (st =[ ~c₁ ]=> st') → st =[ if (~b) {~c₁} else {~c₂} ]=> st' b:Bexpc₁:Comc₂:Comhb:b ≃ bexp {true}st:Statest':State⊢ (st =[ if (~b) {~c₁} else {~c₂} ]=> st') → st =[ ~c₁ ]=> st' b:Bexpc₁:Comc₂:Comhb:b ≃ bexp {true}st:Statest':Stateh:st =[ if (~b) {~c₁} else {~c₂} ]=> st'⊢ st =[ ~c₁ ]=> st' b:Bexpc₁:Comc₂:Comhb:b ≃ bexp {true}st:Statest':Statehb✝:Bexp.eval st b = truehc✝:c₁.EvalR st st'⊢ st =[ ~c₁ ]=> st'b:Bexpc₁:Comc₂:Comhb:b ≃ bexp {true}st:Statest':Statehb✝:Bexp.eval st b = falsehc✝:c₂.EvalR st st'⊢ st =[ ~c₁ ]=> st' b:Bexpc₁:Comc₂:Comhb:b ≃ bexp {true}st:Statest':Statehb✝:Bexp.eval st b = truehc✝:c₁.EvalR st st'⊢ st =[ ~c₁ ]=> st'b:Bexpc₁:Comc₂:Comhb:b ≃ bexp {true}st:Statest':Statehb✝:Bexp.eval st b = falsehc✝:c₂.EvalR st st'⊢ st =[ ~c₁ ]=> st' All goals completed! 🐙 b:Bexpc₁:Comc₂:Comhb:b ≃ bexp {true}st:Statest':State⊢ (st =[ ~c₁ ]=> st') → st =[ if (~b) {~c₁} else {~c₂} ]=> st' b:Bexpc₁:Comc₂:Comhb:b ≃ bexp {true}st:Statest':Stateh:st =[ ~c₁ ]=> st'⊢ st =[ if (~b) {~c₁} else {~c₂} ]=> st' b:Bexpc₁:Comc₂:Comhb:b ≃ bexp {true}st:Statest':Stateh:st =[ ~c₁ ]=> st'⊢ Bexp.eval st b = true All goals completed! 🐙 theorem while_false {b : Bexp} {c : Com} (hb : b ≃ bexp {false}) : imp {while (b) {c}} ≃ imp {skip} := b:Bexpc:Comhb:b ≃ bexp {false}⊢ imp {while (~b) {~c}} ≃ imp {skip} b:Bexpc:Comhb:b ≃ bexp {false}⊢ ∀ {st st' : State}, (st =[ while (~b) {~c} ]=> st') ↔ st =[ skip ]=> st' b:Bexpc:Comhb:b ≃ bexp {false}st:Statest'':State⊢ (st =[ while (~b) {~c} ]=> st'') ↔ st =[ skip ]=> st'' b:Bexpc:Comhb:b ≃ bexp {false}st:Statest'':State⊢ (st =[ while (~b) {~c} ]=> st'') → st =[ skip ]=> st''b:Bexpc:Comhb:b ≃ bexp {false}st:Statest'':State⊢ (st =[ skip ]=> st'') → st =[ while (~b) {~c} ]=> st'' b:Bexpc:Comhb:b ≃ bexp {false}st:Statest'':State⊢ (st =[ while (~b) {~c} ]=> st'') → st =[ skip ]=> st'' b:Bexpc:Comhb:b ≃ bexp {false}st:Statest'':Stateh:st =[ while (~b) {~c} ]=> st''⊢ st =[ skip ]=> st'' inversion h with | whileFalse => All goals completed! 🐙 | whileTrue st' hb' hc hloop => All goals completed! 🐙 b:Bexpc:Comhb:b ≃ bexp {false}st:Statest'':State⊢ (st =[ skip ]=> st'') → st =[ while (~b) {~c} ]=> st'' b:Bexpc:Comhb:b ≃ bexp {false}st:Statest'':Stateh:st =[ skip ]=> st''⊢ st =[ while (~b) {~c} ]=> st'' b:Bexpc:Comhb:b ≃ bexp {false}st:State⊢ st =[ while (~b) {~c} ]=> st b:Bexpc:Comhb:b ≃ bexp {false}st:State⊢ Bexp.eval st b = false All goals completed! 🐙 theorem declaration uses `sorry`while_true_nonterm {b : Bexp} {c : Com} {st st' : State} (hb : b ≃ bexp {true}) : ¬ st =[ while (b) {c} ]=> st' := b:Bexpc:Comst:Statest':Statehb:b ≃ bexp {true}⊢ ¬st =[ while (~b) {~c} ]=> st' All goals completed! 🐙 -- `heq` says that different commands are equal theorem declaration uses `sorry`loop_unrolling {b : Bexp} {c : Com} : imp { while (b) {c} } ≃ imp { if (b) {c} else {skip}; while (b) {c} } := b:Bexpc:Com⊢ imp {while (~b) {~c}} ≃ imp {if (~b) {~c} else {skip}; while (~b) {~c}} All goals completed! 🐙 theorem identity_assignment {X : Ident} : imp { X := X } ≃ imp { skip } := X:Ident⊢ imp {X := X} ≃ imp {skip} X:Ident⊢ ∀ {st st' : State}, (st =[ X := X ]=> st') ↔ st =[ skip ]=> st' X:Identst:Statest':State⊢ (st =[ X := X ]=> st') ↔ st =[ skip ]=> st' X:Identst:Statest':State⊢ (st =[ X := X ]=> st') → st =[ skip ]=> st'X:Identst:Statest':State⊢ (st =[ skip ]=> st') → st =[ X := X ]=> st' X:Identst:Statest':State⊢ (st =[ X := X ]=> st') → st =[ skip ]=> st' X:Identst:Statest':Stateh:st =[ X := X ]=> st'⊢ st =[ skip ]=> st' inversion h with | asgn n h => X:Identst:State⊢ st =[ skip ]=> X →ₜ Aexp.eval st (aexp {X}) ; st X:Identst:State⊢ st =[ skip ]=> st All goals completed! 🐙 X:Identst:Statest':State⊢ (st =[ skip ]=> st') → st =[ X := X ]=> st' X:Identst:Statest':Stateh:st =[ skip ]=> st'⊢ st =[ X := X ]=> st' X:Identst:State⊢ st =[ X := X ]=> st X:Identst:Stateh':st =[ X := X ]=> X →ₜ st[X] ; st⊢ st =[ X := X ]=> st All goals completed! 🐙

4.2. Properties of Behavior Equivalence🔗

4.2.1. Behavioral Equivalence is an Equivalence🔗

end Com theorem Aexp.equiv_refl (a : Aexp) : a ≃ a := a:Aexp⊢ a ≃ a All goals completed! 🐙 theorem Aexp.equiv_symm {a₁ a₂ : Aexp} (h : a₁ ≃ a₂) : a₂ ≃ a₁ := a₁:Aexpa₂:Aexph:a₁ ≃ a₂⊢ a₂ ≃ a₁ All goals completed! 🐙 theorem Aexp.equiv_trans {a₁ a₂ a₃ : Aexp} (h₁ : a₁ ≃ a₂) (h₂ : a₂ ≃ a₃) : a₁ ≃ a₃ := a₁:Aexpa₂:Aexpa₃:Aexph₁:a₁ ≃ a₂h₂:a₂ ≃ a₃⊢ a₁ ≃ a₃ All goals completed! 🐙 theorem Bexp.equiv_refl {b : Bexp} : b ≃ b := b:Bexp⊢ b ≃ b All goals completed! 🐙 theorem Bexp.equiv_symm {b₁ b₂ : Bexp} (h : b₁ ≃ b₂) : b₂ ≃ b₁ := b₁:Bexpb₂:Bexph:b₁ ≃ b₂⊢ b₂ ≃ b₁ All goals completed! 🐙 theorem Bexp.equiv_trans {b₁ b₂ b₃ : Bexp} (h₁ : b₁ ≃ b₂) (h₂ : b₂ ≃ b₃) : b₁ ≃ b₃ := b₁:Bexpb₂:Bexpb₃:Bexph₁:b₁ ≃ b₂h₂:b₂ ≃ b₃⊢ b₁ ≃ b₃ All goals completed! 🐙 theorem Com.equiv_refl {c : Com} : c ≃ c := c:Com⊢ c ≃ c All goals completed! 🐙 theorem Com.equiv_symm {c₁ c₂ : Com} (h : c₁ ≃ c₂) : c₂ ≃ c₁ := c₁:Comc₂:Comh:c₁ ≃ c₂⊢ c₂ ≃ c₁ All goals completed! 🐙 theorem Com.equiv_trans {c₁ c₂ c₃ : Com} (h₁ : c₁ ≃ c₂) (h₂ : c₂ ≃ c₃) : c₁ ≃ c₃ := c₁:Comc₂:Comc₃:Comh₁:c₁ ≃ c₂h₂:c₂ ≃ c₃⊢ c₁ ≃ c₃ All goals completed! 🐙

4.2.2. Behavioral Equivalence is a Congruence🔗

theorem Com.congruence_asgn {x : Ident} {a a' : Aexp} (ha : a ≃ a') : imp {x := a} ≃ imp {x := a'} := x:Identa:Aexpa':Aexpha:a ≃ a'⊢ imp {x := ~a} ≃ imp {x := ~a'} x:Identa:Aexpa':Aexpha:a ≃ a'⊢ ∀ {st st' : State}, (st =[ x := ~a ]=> st') ↔ st =[ x := ~a' ]=> st' x:Identa:Aexpa':Aexpha:a ≃ a'st:Statest':State⊢ (st =[ x := ~a ]=> st') ↔ st =[ x := ~a' ]=> st' x:Identa:Aexpa':Aexpha:a ≃ a'st:Statest':State⊢ (st =[ x := ~a ]=> st') → st =[ x := ~a' ]=> st'x:Identa:Aexpa':Aexpha:a ≃ a'st:Statest':State⊢ (st =[ x := ~a' ]=> st') → st =[ x := ~a ]=> st' x:Identa:Aexpa':Aexpha:a ≃ a'st:Statest':State⊢ (st =[ x := ~a ]=> st') → st =[ x := ~a' ]=> st'x:Identa:Aexpa':Aexpha:a ≃ a'st:Statest':State⊢ (st =[ x := ~a' ]=> st') → st =[ x := ~a ]=> st' x:Identa:Aexpa':Aexpha:a ≃ a'st:Statest':State⊢ (st =[ x := ~a' ]=> st') → st =[ x := ~a ]=> st' x:Identa:Aexpa':Aexpha:a ≃ a'st:Statest':Stateh:st =[ x := ~a' ]=> st'⊢ st =[ x := ~a ]=> st' inversion h with | asgn n h => x:Identa:Aexpa':Aexpha:a ≃ a'st:State⊢ st =[ x := ~a ]=> x →ₜ Aexp.eval st a' ; st x:Identa:Aexpa':Aexpha:a ≃ a'st:State⊢ Aexp.eval st a = Aexp.eval st a' All goals completed! 🐙 theorem declaration uses `sorry`Com.congruence_while {b b' : Bexp} {c c' : Com} (hb : b ≃ b') (hc : c ≃ c') : imp {while (b) {c}} ≃ imp {while (b') {c'}} := b:Bexpb':Bexpc:Comc':Comhb:b ≃ b'hc:c ≃ c'⊢ imp {while (~b) {~c}} ≃ imp {while (~b') {~c'}} All goals completed! 🐙

4.3. Program Transformation🔗

def Aexp.TransSound (trans : Aexp → Aexp) : Prop := ∀ (a : Aexp), a ≃ (trans a) @[simp] theorem Aexp.transSound_def {trans : Aexp → Aexp} : TransSound trans ↔ ∀ (a : Aexp), a ≃ (trans a) := trans:Aexp → Aexp⊢ TransSound trans ↔ ∀ (a : Aexp), a ≃ trans a All goals completed! 🐙 def Bexp.TransSound (trans : Bexp → Bexp) : Prop := ∀ (b : Bexp), b ≃ (trans b) @[simp] theorem Bexp.transSound_def {trans : Bexp → Bexp} : TransSound trans ↔ ∀ (b : Bexp), b ≃ (trans b) := trans:Bexp → Bexp⊢ TransSound trans ↔ ∀ (b : Bexp), b ≃ trans b All goals completed! 🐙 def Com.TransSound (trans : Com → Com) : Prop := ∀ (c : Com), c ≃ (trans c) @[simp] theorem Com.transSound_def {trans : Com → Com} : TransSound trans ↔ ∀ (c : Com), c ≃ (trans c) := trans:Com → Com⊢ TransSound trans ↔ ∀ (c : Com), c ≃ trans c All goals completed! 🐙

4.3.1. The Constant-Folding Transformation🔗

def Aexp.foldConstants (a : Aexp) : Aexp := match a with | .num n => .num n | .id x => .id x | aexp { ~a₁ + ~a₂ } => match a₁.foldConstants, a₂.foldConstants with | .num n₁, .num n₂ => .num (n₁ + n₂) | a₁', a₂' => aexp { ~a₁' + ~a₂' } | aexp { ~a₁ - ~a₂ } => match a₁.foldConstants, a₂.foldConstants with | .num n₁, .num n₂ => .num (n₁ - n₂) | a₁', a₂' => aexp { ~a₁' - ~a₂' } | aexp { ~a₁ * ~a₂ } => match a₁.foldConstants, a₂.foldConstants with | .num n₁, .num n₂ => .num (n₁ * n₂) | a₁', a₂' => aexp { ~a₁' * ~a₂' } @[simp] theorem Aexp.foldConstants_num (n : Nat) : (Aexp.num n).foldConstants = .num n := rfl @[simp] theorem Aexp.foldConstants_id (x : Ident) : (Aexp.id x).foldConstants = .id x := rfl theorem Aexp.foldConstants_cases (a₁ a₂ : Aexp) : (∃ n₁ n₂, a₁.foldConstants = .num n₁ ∧ a₂.foldConstants = .num n₂) ∨ (aexp {a₁ + a₂}).foldConstants = (aexp {~a₁.foldConstants + ~a₂.foldConstants}) ∧ (aexp {a₁ - a₂}).foldConstants = (aexp {~a₁.foldConstants - ~a₂.foldConstants}) ∧ (aexp {a₁ * a₂}).foldConstants = (aexp {~a₁.foldConstants * ~a₂.foldConstants}) := a₁:Aexpa₂:Aexp⊢ (∃ n₁ n₂, a₁.foldConstants = num n₁ ∧ a₂.foldConstants = num n₂) ∨ aexp {~a₁ + ~a₂}.foldConstants = aexp {~a₁.foldConstants + ~a₂.foldConstants} ∧ aexp {~a₁ - ~a₂}.foldConstants = aexp {~a₁.foldConstants - ~a₂.foldConstants} ∧ aexp {~a₁ * ~a₂}.foldConstants = aexp {~a₁.foldConstants * ~a₂.foldConstants} cases ha₁ : a₁.foldConstants with a₁:Aexpa₂:Aexpn₁:Natha₁:a₁.foldConstants = num n₁⊢ (∃ n₁_1 n₂, num n₁ = num n₁_1 ∧ a₂.foldConstants = num n₂) ∨ aexp {~a₁ + ~a₂}.foldConstants = aexp {~(num n₁) + ~a₂.foldConstants} ∧ aexp {~a₁ - ~a₂}.foldConstants = aexp {~(num n₁) - ~a₂.foldConstants} ∧ aexp {~a₁ * ~a₂}.foldConstants = aexp {~(num n₁) * ~a₂.foldConstants} cases ha₂ : a₂.foldConstants with a₁:Aexpa₂:Aexpn₁:Natha₁:a₁.foldConstants = num n₁n₂:Natha₂:a₂.foldConstants = num n₂⊢ (∃ n₁_1 n₂_1, num n₁ = num n₁_1 ∧ num n₂ = num n₂_1) ∨ aexp {~a₁ + ~a₂}.foldConstants = aexp {~(num n₁) + ~(num n₂)} ∧ aexp {~a₁ - ~a₂}.foldConstants = aexp {~(num n₁) - ~(num n₂)} ∧ aexp {~a₁ * ~a₂}.foldConstants = aexp {~(num n₁) * ~(num n₂)} a₁:Aexpa₂:Aexpn₁:Natha₁:a₁.foldConstants = num n₁n₂:Natha₂:a₂.foldConstants = num n₂⊢ ∃ n₁_1 n₂_1, num n₁ = num n₁_1 ∧ num n₂ = num n₂_1 All goals completed! 🐙 a₁:Aexpa₂:Aexpn₁:Natha₁:a₁.foldConstants = num n₁a₁✝:Aexpa₂✝:Aexpha₂:a₂.foldConstants = aexp {~a₁✝ * ~a₂✝}⊢ (∃ n₁_1 n₂, num n₁ = num n₁_1 ∧ aexp {~a₁✝ * ~a₂✝} = num n₂) ∨ aexp {~a₁ + ~a₂}.foldConstants = aexp {~(num n₁) + ~a₁✝ * ~a₂✝} ∧ aexp {~a₁ - ~a₂}.foldConstants = aexp {~(num n₁) - ~a₁✝ * ~a₂✝} ∧ aexp {~a₁ * ~a₂}.foldConstants = aexp {~(num n₁) * (~a₁✝ * ~a₂✝)}a₁:Aexpa₂:Aexpn₁:Natha₁:a₁.foldConstants = num n₁a₁✝:Aexpa₂✝:Aexpha₂:a₂.foldConstants = aexp {~a₁✝ - ~a₂✝}⊢ (∃ n₁_1 n₂, num n₁ = num n₁_1 ∧ aexp {~a₁✝ - ~a₂✝} = num n₂) ∨ aexp {~a₁ + ~a₂}.foldConstants = aexp {~(num n₁) + (~a₁✝ - ~a₂✝)} ∧ aexp {~a₁ - ~a₂}.foldConstants = aexp {~(num n₁) - (~a₁✝ - ~a₂✝)} ∧ aexp {~a₁ * ~a₂}.foldConstants = aexp {~(num n₁) * (~a₁✝ - ~a₂✝)}a₁:Aexpa₂:Aexpn₁:Natha₁:a₁.foldConstants = num n₁a₁✝:Aexpa₂✝:Aexpha₂:a₂.foldConstants = aexp {~a₁✝ + ~a₂✝}⊢ (∃ n₁_1 n₂, num n₁ = num n₁_1 ∧ aexp {~a₁✝ + ~a₂✝} = num n₂) ∨ aexp {~a₁ + ~a₂}.foldConstants = aexp {~(num n₁) + (~a₁✝ + ~a₂✝)} ∧ aexp {~a₁ - ~a₂}.foldConstants = aexp {~(num n₁) - (~a₁✝ + ~a₂✝)} ∧ aexp {~a₁ * ~a₂}.foldConstants = aexp {~(num n₁) * (~a₁✝ + ~a₂✝)}a₁:Aexpa₂:Aexpn₁:Natha₁:a₁.foldConstants = num n₁x✝:Identha₂:a₂.foldConstants = aexp {x✝}⊢ (∃ n₁_1 n₂, num n₁ = num n₁_1 ∧ aexp {x✝} = num n₂) ∨ aexp {~a₁ + ~a₂}.foldConstants = aexp {~(num n₁) + x✝} ∧ aexp {~a₁ - ~a₂}.foldConstants = aexp {~(num n₁) - x✝} ∧ aexp {~a₁ * ~a₂}.foldConstants = aexp {~(num n₁) * x✝} All goals completed! 🐙 a₁:Aexpa₂:Aexpa₁✝:Aexpa₂✝:Aexpha₁:a₁.foldConstants = aexp {~a₁✝ * ~a₂✝}⊢ (∃ n₁ n₂, aexp {~a₁✝ * ~a₂✝} = num n₁ ∧ a₂.foldConstants = num n₂) ∨ aexp {~a₁ + ~a₂}.foldConstants = aexp {~a₁✝ * ~a₂✝ + ~a₂.foldConstants} ∧ aexp {~a₁ - ~a₂}.foldConstants = aexp {~a₁✝ * ~a₂✝ - ~a₂.foldConstants} ∧ aexp {~a₁ * ~a₂}.foldConstants = aexp {~a₁✝ * ~a₂✝ * ~a₂.foldConstants}a₁:Aexpa₂:Aexpa₁✝:Aexpa₂✝:Aexpha₁:a₁.foldConstants = aexp {~a₁✝ - ~a₂✝}⊢ (∃ n₁ n₂, aexp {~a₁✝ - ~a₂✝} = num n₁ ∧ a₂.foldConstants = num n₂) ∨ aexp {~a₁ + ~a₂}.foldConstants = aexp {~a₁✝ - ~a₂✝ + ~a₂.foldConstants} ∧ aexp {~a₁ - ~a₂}.foldConstants = aexp {~a₁✝ - ~a₂✝ - ~a₂.foldConstants} ∧ aexp {~a₁ * ~a₂}.foldConstants = aexp {(~a₁✝ - ~a₂✝) * ~a₂.foldConstants}a₁:Aexpa₂:Aexpa₁✝:Aexpa₂✝:Aexpha₁:a₁.foldConstants = aexp {~a₁✝ + ~a₂✝}⊢ (∃ n₁ n₂, aexp {~a₁✝ + ~a₂✝} = num n₁ ∧ a₂.foldConstants = num n₂) ∨ aexp {~a₁ + ~a₂}.foldConstants = aexp {~a₁✝ + ~a₂✝ + ~a₂.foldConstants} ∧ aexp {~a₁ - ~a₂}.foldConstants = aexp {~a₁✝ + ~a₂✝ - ~a₂.foldConstants} ∧ aexp {~a₁ * ~a₂}.foldConstants = aexp {(~a₁✝ + ~a₂✝) * ~a₂.foldConstants}a₁:Aexpa₂:Aexpx✝:Identha₁:a₁.foldConstants = aexp {x✝}⊢ (∃ n₁ n₂, aexp {x✝} = num n₁ ∧ a₂.foldConstants = num n₂) ∨ aexp {~a₁ + ~a₂}.foldConstants = aexp {x✝ + ~a₂.foldConstants} ∧ aexp {~a₁ - ~a₂}.foldConstants = aexp {x✝ - ~a₂.foldConstants} ∧ aexp {~a₁ * ~a₂}.foldConstants = aexp {x✝ * ~a₂.foldConstants} All goals completed! 🐙
Note to developers (Niklas Halonen @xhalo32)

Make sure we have explained what named cases hypotheses does (cases ha₁ : a₁.foldConstants in the above proof).

example : (aexp { (1 + 2) * X }).foldConstants = (aexp { 3 * X }) := ⊢ aexp {(1 + 2) * X}.foldConstants = aexp {3 * X} All goals completed! 🐙 example : (aexp { X - ((0 * 6) + Y) }).foldConstants = (aexp { X - (0 + Y) }) := ⊢ aexp {X - (0 * 6 + Y)}.foldConstants = aexp {X - (0 + Y)} All goals completed! 🐙 def Bexp.foldConstants (b : Bexp) : Bexp := match b with | bexp { true } => bexp { true } | bexp { false } => bexp { false } | bexp { ~a₁ = ~a₂ } => match a₁.foldConstants, a₂.foldConstants with | .num n₁, .num n₂ => if n₁ = n₂ then bexp { true } else bexp {false} | a₁', a₂' => bexp { a₁' = a₂' } | bexp { ~a₁ ≠ ~a₂ } => match a₁.foldConstants, a₂.foldConstants with | .num n₁, .num n₂ => if n₁ ≠ n₂ then bexp { true } else bexp {false} | a₁', a₂' => bexp { a₁' ≠ a₂' } | bexp { ~a₁ ≤ ~a₂ } => match a₁.foldConstants, a₂.foldConstants with | .num n₁, .num n₂ => if n₁ ≤ n₂ then bexp { true } else bexp {false} | a₁', a₂' => bexp { a₁' ≤ a₂' } | bexp { ~a₁ > ~a₂ } => match a₁.foldConstants, a₂.foldConstants with | .num n₁, .num n₂ => if n₁ > n₂ then bexp { true } else bexp {false} | a₁', a₂' => bexp { a₁' > a₂' } | bexp { ¬ ~b₁ } => match b₁.foldConstants with | bexp { true } => bexp { false } | bexp { false } => bexp { true } | b₁' => bexp { ¬ b₁' } | bexp { ~b₁ ∧ ~b₂ } => match b₁.foldConstants, b₂.foldConstants with | bexp { true }, bexp { true } => bexp { true } | bexp { true }, bexp { false } => bexp { false } | bexp { false }, bexp { true } => bexp { false } | bexp { false }, bexp { false } => bexp { false } | b₁', b₂' => bexp { b₁' ∧ b₂' } @[simp] theorem Bexp.foldConstants_true : (bexp { true }).foldConstants = (bexp { true }) := rfl @[simp] theorem Bexp.foldConstants_false : (bexp { false }).foldConstants = (bexp { false }) := rfl theorem Bexp.foldConstants_comp (a₁ a₂ : Aexp) : (∃ n₁ n₂, a₁.foldConstants = .num n₁ ∧ a₂.foldConstants = .num n₂) ∨ (bexp {~a₁ = ~a₂}).foldConstants = (bexp {~a₁.foldConstants = ~a₂.foldConstants}) ∧ (bexp {~a₁ ≠ ~a₂}).foldConstants = (bexp {~a₁.foldConstants ≠ ~a₂.foldConstants}) ∧ (bexp {~a₁ ≤ ~a₂}).foldConstants = (bexp {~a₁.foldConstants ≤ ~a₂.foldConstants}) ∧ (bexp {~a₁ > ~a₂}).foldConstants = (bexp {~a₁.foldConstants > ~a₂.foldConstants}) := a₁:Aexpa₂:Aexp⊢ (∃ n₁ n₂, a₁.foldConstants = Aexp.num n₁ ∧ a₂.foldConstants = Aexp.num n₂) ∨ bexp {~a₁ = ~a₂}.foldConstants = bexp {~a₁.foldConstants = ~a₂.foldConstants} ∧ bexp {~a₁ ≠ ~a₂}.foldConstants = bexp {~a₁.foldConstants ≠ ~a₂.foldConstants} ∧ bexp {~a₁ ≤ ~a₂}.foldConstants = bexp {~a₁.foldConstants ≤ ~a₂.foldConstants} ∧ bexp {~a₁ > ~a₂}.foldConstants = bexp {~a₁.foldConstants > ~a₂.foldConstants} cases ha₁ : a₁.foldConstants with a₁:Aexpa₂:Aexpn₁:Natha₁:a₁.foldConstants = Aexp.num n₁⊢ (∃ n₁_1 n₂, Aexp.num n₁ = Aexp.num n₁_1 ∧ a₂.foldConstants = Aexp.num n₂) ∨ bexp {~a₁ = ~a₂}.foldConstants = bexp {~(Aexp.num n₁) = ~a₂.foldConstants} ∧ bexp {~a₁ ≠ ~a₂}.foldConstants = bexp {~(Aexp.num n₁) ≠ ~a₂.foldConstants} ∧ bexp {~a₁ ≤ ~a₂}.foldConstants = bexp {~(Aexp.num n₁) ≤ ~a₂.foldConstants} ∧ bexp {~a₁ > ~a₂}.foldConstants = bexp {~(Aexp.num n₁) > ~a₂.foldConstants} cases ha₂ : a₂.foldConstants with a₁:Aexpa₂:Aexpn₁:Natha₁:a₁.foldConstants = Aexp.num n₁n₂:Natha₂:a₂.foldConstants = Aexp.num n₂⊢ (∃ n₁_1 n₂_1, Aexp.num n₁ = Aexp.num n₁_1 ∧ Aexp.num n₂ = Aexp.num n₂_1) ∨ bexp {~a₁ = ~a₂}.foldConstants = bexp {~(Aexp.num n₁) = ~(Aexp.num n₂)} ∧ bexp {~a₁ ≠ ~a₂}.foldConstants = bexp {~(Aexp.num n₁) ≠ ~(Aexp.num n₂)} ∧ bexp {~a₁ ≤ ~a₂}.foldConstants = bexp {~(Aexp.num n₁) ≤ ~(Aexp.num n₂)} ∧ bexp {~a₁ > ~a₂}.foldConstants = bexp {~(Aexp.num n₁) > ~(Aexp.num n₂)} a₁:Aexpa₂:Aexpn₁:Natha₁:a₁.foldConstants = Aexp.num n₁n₂:Natha₂:a₂.foldConstants = Aexp.num n₂⊢ ∃ n₁_1 n₂_1, Aexp.num n₁ = Aexp.num n₁_1 ∧ Aexp.num n₂ = Aexp.num n₂_1 All goals completed! 🐙 a₁:Aexpa₂:Aexpn₁:Natha₁:a₁.foldConstants = Aexp.num n₁a₁✝:Aexpa₂✝:Aexpha₂:a₂.foldConstants = aexp {~a₁✝ * ~a₂✝}⊢ (∃ n₁_1 n₂, Aexp.num n₁ = Aexp.num n₁_1 ∧ aexp {~a₁✝ * ~a₂✝} = Aexp.num n₂) ∨ bexp {~a₁ = ~a₂}.foldConstants = bexp {~(Aexp.num n₁) = ~a₁✝ * ~a₂✝} ∧ bexp {~a₁ ≠ ~a₂}.foldConstants = bexp {~(Aexp.num n₁) ≠ ~a₁✝ * ~a₂✝} ∧ bexp {~a₁ ≤ ~a₂}.foldConstants = bexp {~(Aexp.num n₁) ≤ ~a₁✝ * ~a₂✝} ∧ bexp {~a₁ > ~a₂}.foldConstants = bexp {~(Aexp.num n₁) > ~a₁✝ * ~a₂✝}a₁:Aexpa₂:Aexpn₁:Natha₁:a₁.foldConstants = Aexp.num n₁a₁✝:Aexpa₂✝:Aexpha₂:a₂.foldConstants = aexp {~a₁✝ - ~a₂✝}⊢ (∃ n₁_1 n₂, Aexp.num n₁ = Aexp.num n₁_1 ∧ aexp {~a₁✝ - ~a₂✝} = Aexp.num n₂) ∨ bexp {~a₁ = ~a₂}.foldConstants = bexp {~(Aexp.num n₁) = ~a₁✝ - ~a₂✝} ∧ bexp {~a₁ ≠ ~a₂}.foldConstants = bexp {~(Aexp.num n₁) ≠ ~a₁✝ - ~a₂✝} ∧ bexp {~a₁ ≤ ~a₂}.foldConstants = bexp {~(Aexp.num n₁) ≤ ~a₁✝ - ~a₂✝} ∧ bexp {~a₁ > ~a₂}.foldConstants = bexp {~(Aexp.num n₁) > ~a₁✝ - ~a₂✝}a₁:Aexpa₂:Aexpn₁:Natha₁:a₁.foldConstants = Aexp.num n₁a₁✝:Aexpa₂✝:Aexpha₂:a₂.foldConstants = aexp {~a₁✝ + ~a₂✝}⊢ (∃ n₁_1 n₂, Aexp.num n₁ = Aexp.num n₁_1 ∧ aexp {~a₁✝ + ~a₂✝} = Aexp.num n₂) ∨ bexp {~a₁ = ~a₂}.foldConstants = bexp {~(Aexp.num n₁) = ~a₁✝ + ~a₂✝} ∧ bexp {~a₁ ≠ ~a₂}.foldConstants = bexp {~(Aexp.num n₁) ≠ ~a₁✝ + ~a₂✝} ∧ bexp {~a₁ ≤ ~a₂}.foldConstants = bexp {~(Aexp.num n₁) ≤ ~a₁✝ + ~a₂✝} ∧ bexp {~a₁ > ~a₂}.foldConstants = bexp {~(Aexp.num n₁) > ~a₁✝ + ~a₂✝}a₁:Aexpa₂:Aexpn₁:Natha₁:a₁.foldConstants = Aexp.num n₁x✝:Identha₂:a₂.foldConstants = aexp {x✝}⊢ (∃ n₁_1 n₂, Aexp.num n₁ = Aexp.num n₁_1 ∧ aexp {x✝} = Aexp.num n₂) ∨ bexp {~a₁ = ~a₂}.foldConstants = bexp {~(Aexp.num n₁) = x✝} ∧ bexp {~a₁ ≠ ~a₂}.foldConstants = bexp {~(Aexp.num n₁) ≠ x✝} ∧ bexp {~a₁ ≤ ~a₂}.foldConstants = bexp {~(Aexp.num n₁) ≤ x✝} ∧ bexp {~a₁ > ~a₂}.foldConstants = bexp {~(Aexp.num n₁) > x✝} All goals completed! 🐙 a₁:Aexpa₂:Aexpa₁✝:Aexpa₂✝:Aexpha₁:a₁.foldConstants = aexp {~a₁✝ * ~a₂✝}⊢ (∃ n₁ n₂, aexp {~a₁✝ * ~a₂✝} = Aexp.num n₁ ∧ a₂.foldConstants = Aexp.num n₂) ∨ bexp {~a₁ = ~a₂}.foldConstants = bexp {~a₁✝ * ~a₂✝ = ~a₂.foldConstants} ∧ bexp {~a₁ ≠ ~a₂}.foldConstants = bexp {~a₁✝ * ~a₂✝ ≠ ~a₂.foldConstants} ∧ bexp {~a₁ ≤ ~a₂}.foldConstants = bexp {~a₁✝ * ~a₂✝ ≤ ~a₂.foldConstants} ∧ bexp {~a₁ > ~a₂}.foldConstants = bexp {~a₁✝ * ~a₂✝ > ~a₂.foldConstants}a₁:Aexpa₂:Aexpa₁✝:Aexpa₂✝:Aexpha₁:a₁.foldConstants = aexp {~a₁✝ - ~a₂✝}⊢ (∃ n₁ n₂, aexp {~a₁✝ - ~a₂✝} = Aexp.num n₁ ∧ a₂.foldConstants = Aexp.num n₂) ∨ bexp {~a₁ = ~a₂}.foldConstants = bexp {~a₁✝ - ~a₂✝ = ~a₂.foldConstants} ∧ bexp {~a₁ ≠ ~a₂}.foldConstants = bexp {~a₁✝ - ~a₂✝ ≠ ~a₂.foldConstants} ∧ bexp {~a₁ ≤ ~a₂}.foldConstants = bexp {~a₁✝ - ~a₂✝ ≤ ~a₂.foldConstants} ∧ bexp {~a₁ > ~a₂}.foldConstants = bexp {~a₁✝ - ~a₂✝ > ~a₂.foldConstants}a₁:Aexpa₂:Aexpa₁✝:Aexpa₂✝:Aexpha₁:a₁.foldConstants = aexp {~a₁✝ + ~a₂✝}⊢ (∃ n₁ n₂, aexp {~a₁✝ + ~a₂✝} = Aexp.num n₁ ∧ a₂.foldConstants = Aexp.num n₂) ∨ bexp {~a₁ = ~a₂}.foldConstants = bexp {~a₁✝ + ~a₂✝ = ~a₂.foldConstants} ∧ bexp {~a₁ ≠ ~a₂}.foldConstants = bexp {~a₁✝ + ~a₂✝ ≠ ~a₂.foldConstants} ∧ bexp {~a₁ ≤ ~a₂}.foldConstants = bexp {~a₁✝ + ~a₂✝ ≤ ~a₂.foldConstants} ∧ bexp {~a₁ > ~a₂}.foldConstants = bexp {~a₁✝ + ~a₂✝ > ~a₂.foldConstants}a₁:Aexpa₂:Aexpx✝:Identha₁:a₁.foldConstants = aexp {x✝}⊢ (∃ n₁ n₂, aexp {x✝} = Aexp.num n₁ ∧ a₂.foldConstants = Aexp.num n₂) ∨ bexp {~a₁ = ~a₂}.foldConstants = bexp {x✝ = ~a₂.foldConstants} ∧ bexp {~a₁ ≠ ~a₂}.foldConstants = bexp {x✝ ≠ ~a₂.foldConstants} ∧ bexp {~a₁ ≤ ~a₂}.foldConstants = bexp {x✝ ≤ ~a₂.foldConstants} ∧ bexp {~a₁ > ~a₂}.foldConstants = bexp {x✝ > ~a₂.foldConstants} All goals completed! 🐙 theorem Bexp.foldConstants_unary (b : Bexp) : (b.foldConstants = (bexp { true }) ∨ b.foldConstants = (bexp { false })) ∨ (bexp { ¬b }).foldConstants = (bexp { ¬(b.foldConstants)}) := b:Bexp⊢ (b.foldConstants = bexp {true} ∨ b.foldConstants = bexp {false}) ∨ bexp {¬ ~b}.foldConstants = bexp {¬ ~b.foldConstants} cases hb : b.foldConstants with b:Bexpb':Boolhb:b.foldConstants = bool b'⊢ (bool b' = bexp {true} ∨ bool b' = bexp {false}) ∨ bexp {¬ ~b}.foldConstants = bexp {¬ ~(bool b')} All goals completed! 🐙 b:Bexpb₁✝:Bexpb₂✝:Bexphb:b.foldConstants = bexp {~b₁✝ ∧ ~b₂✝}⊢ (bexp {~b₁✝ ∧ ~b₂✝} = bexp {true} ∨ bexp {~b₁✝ ∧ ~b₂✝} = bexp {false}) ∨ bexp {¬ ~b}.foldConstants = bexp {¬ (~b₁✝ ∧ ~b₂✝)}b:Bexpb✝:Bexphb:b.foldConstants = bexp {¬ ~b✝}⊢ (bexp {¬ ~b✝} = bexp {true} ∨ bexp {¬ ~b✝} = bexp {false}) ∨ bexp {¬ ~b}.foldConstants = bexp {¬ ¬ ~b✝}b:Bexpa₁✝:Aexpa₂✝:Aexphb:b.foldConstants = bexp {~a₁✝ > ~a₂✝}⊢ (bexp {~a₁✝ > ~a₂✝} = bexp {true} ∨ bexp {~a₁✝ > ~a₂✝} = bexp {false}) ∨ bexp {¬ ~b}.foldConstants = bexp {¬ (~a₁✝ > ~a₂✝)}b:Bexpa₁✝:Aexpa₂✝:Aexphb:b.foldConstants = bexp {~a₁✝ ≤ ~a₂✝}⊢ (bexp {~a₁✝ ≤ ~a₂✝} = bexp {true} ∨ bexp {~a₁✝ ≤ ~a₂✝} = bexp {false}) ∨ bexp {¬ ~b}.foldConstants = bexp {¬ (~a₁✝ ≤ ~a₂✝)}b:Bexpa₁✝:Aexpa₂✝:Aexphb:b.foldConstants = bexp {~a₁✝ ≠ ~a₂✝}⊢ (bexp {~a₁✝ ≠ ~a₂✝} = bexp {true} ∨ bexp {~a₁✝ ≠ ~a₂✝} = bexp {false}) ∨ bexp {¬ ~b}.foldConstants = bexp {¬ (~a₁✝ ≠ ~a₂✝)}b:Bexpa₁✝:Aexpa₂✝:Aexphb:b.foldConstants = bexp {~a₁✝ = ~a₂✝}⊢ (bexp {~a₁✝ = ~a₂✝} = bexp {true} ∨ bexp {~a₁✝ = ~a₂✝} = bexp {false}) ∨ bexp {¬ ~b}.foldConstants = bexp {¬ (~a₁✝ = ~a₂✝)} All goals completed! 🐙 theorem Bexp.foldConstants_binary (b₁ : Bexp) (b₂ : Bexp) : ((b₁.foldConstants = (bexp { true }) ∨ b₁.foldConstants = (bexp { false })) ∧ (b₂.foldConstants = (bexp { true }) ∨ b₂.foldConstants = (bexp { false }))) ∨ (bexp {b₁ ∧ b₂}).foldConstants = (bexp {b₁.foldConstants ∧ b₂.foldConstants}) := b₁:Bexpb₂:Bexp⊢ (b₁.foldConstants = bexp {true} ∨ b₁.foldConstants = bexp {false}) ∧ (b₂.foldConstants = bexp {true} ∨ b₂.foldConstants = bexp {false}) ∨ bexp {~b₁ ∧ ~b₂}.foldConstants = bexp {~b₁.foldConstants ∧ ~b₂.foldConstants} cases hb₁ : b₁.foldConstants with b₁:Bexpb₂:Bexpb₁':Boolhb₁:b₁.foldConstants = bool b₁'⊢ (bool b₁' = bexp {true} ∨ bool b₁' = bexp {false}) ∧ (b₂.foldConstants = bexp {true} ∨ b₂.foldConstants = bexp {false}) ∨ bexp {~b₁ ∧ ~b₂}.foldConstants = bexp {~(bool b₁') ∧ ~b₂.foldConstants} cases hb₂ : b₂.foldConstants with b₁:Bexpb₂:Bexpb₁':Boolhb₁:b₁.foldConstants = bool b₁'b₂':Boolhb₂:b₂.foldConstants = bool b₂'⊢ (bool b₁' = bexp {true} ∨ bool b₁' = bexp {false}) ∧ (bool b₂' = bexp {true} ∨ bool b₂' = bexp {false}) ∨ bexp {~b₁ ∧ ~b₂}.foldConstants = bexp {~(bool b₁') ∧ ~(bool b₂')} All goals completed! 🐙 b₁:Bexpb₂:Bexpb₁':Boolhb₁:b₁.foldConstants = bool b₁'b₁✝:Bexpb₂✝:Bexphb₂:b₂.foldConstants = bexp {~b₁✝ ∧ ~b₂✝}⊢ (bool b₁' = bexp {true} ∨ bool b₁' = bexp {false}) ∧ (bexp {~b₁✝ ∧ ~b₂✝} = bexp {true} ∨ bexp {~b₁✝ ∧ ~b₂✝} = bexp {false}) ∨ bexp {~b₁ ∧ ~b₂}.foldConstants = bexp {~(bool b₁') ∧ ~b₁✝ ∧ ~b₂✝}b₁:Bexpb₂:Bexpb₁':Boolhb₁:b₁.foldConstants = bool b₁'b✝:Bexphb₂:b₂.foldConstants = bexp {¬ ~b✝}⊢ (bool b₁' = bexp {true} ∨ bool b₁' = bexp {false}) ∧ (bexp {¬ ~b✝} = bexp {true} ∨ bexp {¬ ~b✝} = bexp {false}) ∨ bexp {~b₁ ∧ ~b₂}.foldConstants = bexp {~(bool b₁') ∧ ¬ ~b✝}b₁:Bexpb₂:Bexpb₁':Boolhb₁:b₁.foldConstants = bool b₁'a₁✝:Aexpa₂✝:Aexphb₂:b₂.foldConstants = bexp {~a₁✝ > ~a₂✝}⊢ (bool b₁' = bexp {true} ∨ bool b₁' = bexp {false}) ∧ (bexp {~a₁✝ > ~a₂✝} = bexp {true} ∨ bexp {~a₁✝ > ~a₂✝} = bexp {false}) ∨ bexp {~b₁ ∧ ~b₂}.foldConstants = bexp {~(bool b₁') ∧ ~a₁✝ > ~a₂✝}b₁:Bexpb₂:Bexpb₁':Boolhb₁:b₁.foldConstants = bool b₁'a₁✝:Aexpa₂✝:Aexphb₂:b₂.foldConstants = bexp {~a₁✝ ≤ ~a₂✝}⊢ (bool b₁' = bexp {true} ∨ bool b₁' = bexp {false}) ∧ (bexp {~a₁✝ ≤ ~a₂✝} = bexp {true} ∨ bexp {~a₁✝ ≤ ~a₂✝} = bexp {false}) ∨ bexp {~b₁ ∧ ~b₂}.foldConstants = bexp {~(bool b₁') ∧ ~a₁✝ ≤ ~a₂✝}b₁:Bexpb₂:Bexpb₁':Boolhb₁:b₁.foldConstants = bool b₁'a₁✝:Aexpa₂✝:Aexphb₂:b₂.foldConstants = bexp {~a₁✝ ≠ ~a₂✝}⊢ (bool b₁' = bexp {true} ∨ bool b₁' = bexp {false}) ∧ (bexp {~a₁✝ ≠ ~a₂✝} = bexp {true} ∨ bexp {~a₁✝ ≠ ~a₂✝} = bexp {false}) ∨ bexp {~b₁ ∧ ~b₂}.foldConstants = bexp {~(bool b₁') ∧ ~a₁✝ ≠ ~a₂✝}b₁:Bexpb₂:Bexpb₁':Boolhb₁:b₁.foldConstants = bool b₁'a₁✝:Aexpa₂✝:Aexphb₂:b₂.foldConstants = bexp {~a₁✝ = ~a₂✝}⊢ (bool b₁' = bexp {true} ∨ bool b₁' = bexp {false}) ∧ (bexp {~a₁✝ = ~a₂✝} = bexp {true} ∨ bexp {~a₁✝ = ~a₂✝} = bexp {false}) ∨ bexp {~b₁ ∧ ~b₂}.foldConstants = bexp {~(bool b₁') ∧ ~a₁✝ = ~a₂✝} All goals completed! 🐙 b₁:Bexpb₂:Bexpb₁✝:Bexpb₂✝:Bexphb₁:b₁.foldConstants = bexp {~b₁✝ ∧ ~b₂✝}⊢ (bexp {~b₁✝ ∧ ~b₂✝} = bexp {true} ∨ bexp {~b₁✝ ∧ ~b₂✝} = bexp {false}) ∧ (b₂.foldConstants = bexp {true} ∨ b₂.foldConstants = bexp {false}) ∨ bexp {~b₁ ∧ ~b₂}.foldConstants = bexp {(~b₁✝ ∧ ~b₂✝) ∧ ~b₂.foldConstants}b₁:Bexpb₂:Bexpb✝:Bexphb₁:b₁.foldConstants = bexp {¬ ~b✝}⊢ (bexp {¬ ~b✝} = bexp {true} ∨ bexp {¬ ~b✝} = bexp {false}) ∧ (b₂.foldConstants = bexp {true} ∨ b₂.foldConstants = bexp {false}) ∨ bexp {~b₁ ∧ ~b₂}.foldConstants = bexp {¬ ~b✝ ∧ ~b₂.foldConstants}b₁:Bexpb₂:Bexpa₁✝:Aexpa₂✝:Aexphb₁:b₁.foldConstants = bexp {~a₁✝ > ~a₂✝}⊢ (bexp {~a₁✝ > ~a₂✝} = bexp {true} ∨ bexp {~a₁✝ > ~a₂✝} = bexp {false}) ∧ (b₂.foldConstants = bexp {true} ∨ b₂.foldConstants = bexp {false}) ∨ bexp {~b₁ ∧ ~b₂}.foldConstants = bexp {~a₁✝ > ~a₂✝ ∧ ~b₂.foldConstants}b₁:Bexpb₂:Bexpa₁✝:Aexpa₂✝:Aexphb₁:b₁.foldConstants = bexp {~a₁✝ ≤ ~a₂✝}⊢ (bexp {~a₁✝ ≤ ~a₂✝} = bexp {true} ∨ bexp {~a₁✝ ≤ ~a₂✝} = bexp {false}) ∧ (b₂.foldConstants = bexp {true} ∨ b₂.foldConstants = bexp {false}) ∨ bexp {~b₁ ∧ ~b₂}.foldConstants = bexp {~a₁✝ ≤ ~a₂✝ ∧ ~b₂.foldConstants}b₁:Bexpb₂:Bexpa₁✝:Aexpa₂✝:Aexphb₁:b₁.foldConstants = bexp {~a₁✝ ≠ ~a₂✝}⊢ (bexp {~a₁✝ ≠ ~a₂✝} = bexp {true} ∨ bexp {~a₁✝ ≠ ~a₂✝} = bexp {false}) ∧ (b₂.foldConstants = bexp {true} ∨ b₂.foldConstants = bexp {false}) ∨ bexp {~b₁ ∧ ~b₂}.foldConstants = bexp {~a₁✝ ≠ ~a₂✝ ∧ ~b₂.foldConstants}b₁:Bexpb₂:Bexpa₁✝:Aexpa₂✝:Aexphb₁:b₁.foldConstants = bexp {~a₁✝ = ~a₂✝}⊢ (bexp {~a₁✝ = ~a₂✝} = bexp {true} ∨ bexp {~a₁✝ = ~a₂✝} = bexp {false}) ∧ (b₂.foldConstants = bexp {true} ∨ b₂.foldConstants = bexp {false}) ∨ bexp {~b₁ ∧ ~b₂}.foldConstants = bexp {~a₁✝ = ~a₂✝ ∧ ~b₂.foldConstants} All goals completed! 🐙 example : (bexp { true ∧ ¬( false ∧ true) }).foldConstants = (bexp { true }) := ⊢ bexp {true ∧ ¬ (false ∧ true)}.foldConstants = bexp {true} All goals completed! 🐙 example : (bexp { (X = Y) ∧ ( 0 = (2 - (1 + 1))) }).foldConstants = (bexp { (X = Y) ∧ true }) := ⊢ bexp {X = Y ∧ 0 = 2 - (1 + 1)}.foldConstants = bexp {X = Y ∧ true} All goals completed! 🐙 def Com.foldConstants (c : Com) : Com := match c with | imp { skip } => imp { skip } | imp { x := ~a } => imp { x := ~a.foldConstants } | imp { c₁ ; c₂ } => imp { c₁.foldConstants ; c₂.foldConstants } | imp { if (b) { c₁ } else { c₂ }} => match b.foldConstants with | bexp { true } => c₁.foldConstants | bexp { false } => c₂.foldConstants | b' => imp { if (b') {c₁.foldConstants} else { c₂.foldConstants}} | imp { while (b) {c}} => match b.foldConstants with | bexp { true } => imp { while (true) { skip }} | bexp { false } => imp { skip } | b' => imp { while (b') {c.foldConstants}} example : (imp { X := 4 + 5; Y := X - 3; if ((X - Y) = (2 + 4)) {skip} else {Y := 0}; if (0 ≤ (4 - (2 - 1))) {Y := 0} else {skip}; while (Y = 0) {X := X+1} }).foldConstants = (imp { X := 9; Y := X - 3; if ((X - Y) = 6) {skip} else {Y := 0}; Y := 0; while (Y = 0) {X := X+1} }) := ⊢ imp {X := 4 + 5; Y := X - 3; if (X - Y = 2 + 4) {skip} else {Y := 0}; if (0 ≤ 4 - (2 - 1)) {Y := 0} else {skip}; while (Y = 0) {X := X + 1}}.foldConstants = imp {X := 9; Y := X - 3; if (X - Y = 6) {skip} else {Y := 0}; Y := 0; while (Y = 0) {X := X + 1}} All goals completed! 🐙

4.3.2. Soundness of Constant Folding🔗

theorem Aexp.foldConstants_sound : TransSound Aexp.foldConstants := ⊢ TransSound foldConstants a:Aexpst:State⊢ eval st a = eval st a.foldConstants induction a with st:Staten:Nat⊢ eval st (num n) = eval st (num n).foldConstants st:Statex:Ident⊢ eval st (aexp {x}) = eval st aexp {x}.foldConstants st:Statex:Ident⊢ eval st (aexp {x}) = eval st aexp {x}.foldConstantsst:Staten:Nat⊢ eval st (num n) = eval st (num n).foldConstants All goals completed! 🐙 st:Statea₁:Aexpa₂:Aexpa₁_ih✝:eval st a₁ = eval st a₁.foldConstantsa₂_ih✝:eval st a₂ = eval st a₂.foldConstants⊢ eval st (aexp {~a₁ * ~a₂}) = eval st aexp {~a₁ * ~a₂}.foldConstantsst:Statea₁:Aexpa₂:Aexpa₁_ih✝:eval st a₁ = eval st a₁.foldConstantsa₂_ih✝:eval st a₂ = eval st a₂.foldConstants⊢ eval st (aexp {~a₁ - ~a₂}) = eval st aexp {~a₁ - ~a₂}.foldConstantsst:Statea₁:Aexpa₂:Aexpa₁_ih✝:eval st a₁ = eval st a₁.foldConstantsa₂_ih✝:eval st a₂ = eval st a₂.foldConstants⊢ eval st (aexp {~a₁ + ~a₂}) = eval st aexp {~a₁ + ~a₂}.foldConstants cases Aexp.foldConstants_cases a₁ a₂ with st:Statea₁:Aexpa₂:Aexpa₁_ih✝:eval st a₁ = eval st a₁.foldConstantsa₂_ih✝:eval st a₂ = eval st a₂.foldConstantsh:∃ n₁ n₂, a₁.foldConstants = num n₁ ∧ a₂.foldConstants = num n₂⊢ eval st (aexp {~a₁ * ~a₂}) = eval st aexp {~a₁ * ~a₂}.foldConstantsst:Statea₁:Aexpa₂:Aexpa₁_ih✝:eval st a₁ = eval st a₁.foldConstantsa₂_ih✝:eval st a₂ = eval st a₂.foldConstantsh:∃ n₁ n₂, a₁.foldConstants = num n₁ ∧ a₂.foldConstants = num n₂⊢ eval st (aexp {~a₁ - ~a₂}) = eval st aexp {~a₁ - ~a₂}.foldConstantsst:Statea₁:Aexpa₂:Aexpa₁_ih✝:eval st a₁ = eval st a₁.foldConstantsa₂_ih✝:eval st a₂ = eval st a₂.foldConstantsh:∃ n₁ n₂, a₁.foldConstants = num n₁ ∧ a₂.foldConstants = num n₂⊢ eval st (aexp {~a₁ + ~a₂}) = eval st aexp {~a₁ + ~a₂}.foldConstants st:Statea₁:Aexpa₂:Aexpa₁_ih✝:eval st a₁ = eval st a₁.foldConstantsa₂_ih✝:eval st a₂ = eval st a₂.foldConstantsn₁:Natn₂:Nath₁:a₁.foldConstants = num n₁h₂:a₂.foldConstants = num n₂⊢ eval st (aexp {~a₁ * ~a₂}) = eval st aexp {~a₁ * ~a₂}.foldConstants All goals completed! 🐙 st:Statea₁:Aexpa₂:Aexpa₁_ih✝:eval st a₁ = eval st a₁.foldConstantsa₂_ih✝:eval st a₂ = eval st a₂.foldConstantsh:aexp {~a₁ + ~a₂}.foldConstants = aexp {~a₁.foldConstants + ~a₂.foldConstants} ∧ aexp {~a₁ - ~a₂}.foldConstants = aexp {~a₁.foldConstants - ~a₂.foldConstants} ∧ aexp {~a₁ * ~a₂}.foldConstants = aexp {~a₁.foldConstants * ~a₂.foldConstants}⊢ eval st (aexp {~a₁ * ~a₂}) = eval st aexp {~a₁ * ~a₂}.foldConstantsst:Statea₁:Aexpa₂:Aexpa₁_ih✝:eval st a₁ = eval st a₁.foldConstantsa₂_ih✝:eval st a₂ = eval st a₂.foldConstantsh:aexp {~a₁ + ~a₂}.foldConstants = aexp {~a₁.foldConstants + ~a₂.foldConstants} ∧ aexp {~a₁ - ~a₂}.foldConstants = aexp {~a₁.foldConstants - ~a₂.foldConstants} ∧ aexp {~a₁ * ~a₂}.foldConstants = aexp {~a₁.foldConstants * ~a₂.foldConstants}⊢ eval st (aexp {~a₁ - ~a₂}) = eval st aexp {~a₁ - ~a₂}.foldConstantsst:Statea₁:Aexpa₂:Aexpa₁_ih✝:eval st a₁ = eval st a₁.foldConstantsa₂_ih✝:eval st a₂ = eval st a₂.foldConstantsh:aexp {~a₁ + ~a₂}.foldConstants = aexp {~a₁.foldConstants + ~a₂.foldConstants} ∧ aexp {~a₁ - ~a₂}.foldConstants = aexp {~a₁.foldConstants - ~a₂.foldConstants} ∧ aexp {~a₁ * ~a₂}.foldConstants = aexp {~a₁.foldConstants * ~a₂.foldConstants}⊢ eval st (aexp {~a₁ + ~a₂}) = eval st aexp {~a₁ + ~a₂}.foldConstants All goals completed! 🐙

An equivalent version using the fun_induction tactic would look simpler:

theorem Aexp.foldConstants_sound' : TransSound Aexp.foldConstants := ⊢ TransSound foldConstants a:Aexpst:State⊢ eval st a = eval st a.foldConstants st:Staten✝:Nat⊢ eval st (num n✝) = eval st (num n✝)st:Statex✝:Ident⊢ eval st (aexp {x✝}) = eval st (aexp {x✝})st:Statea₁✝:Aexpa₂✝:Aexpn₁✝:Natn₂✝:Natx✝¹:a₂✝.foldConstants = num n₂✝x✝:a₁✝.foldConstants = num n₁✝ih2✝:eval st a₁✝ = eval st a₁✝.foldConstantsih1✝:eval st a₂✝ = eval st a₂✝.foldConstants⊢ eval st (aexp {~a₁✝ + ~a₂✝}) = eval st (num (n₁✝ + n₂✝))st:Statea₁✝:Aexpa₂✝:Aexpx✝:∀ (n₁ n₂ : Nat), a₁✝.foldConstants = num n₁ → a₂✝.foldConstants = num n₂ → Falseih2✝:eval st a₁✝ = eval st a₁✝.foldConstantsih1✝:eval st a₂✝ = eval st a₂✝.foldConstants⊢ eval st (aexp {~a₁✝ + ~a₂✝}) = eval st (aexp {~a₁✝.foldConstants + ~a₂✝.foldConstants})st:Statea₁✝:Aexpa₂✝:Aexpn₁✝:Natn₂✝:Natx✝¹:a₂✝.foldConstants = num n₂✝x✝:a₁✝.foldConstants = num n₁✝ih2✝:eval st a₁✝ = eval st a₁✝.foldConstantsih1✝:eval st a₂✝ = eval st a₂✝.foldConstants⊢ eval st (aexp {~a₁✝ - ~a₂✝}) = eval st (num (n₁✝ - n₂✝))st:Statea₁✝:Aexpa₂✝:Aexpx✝:∀ (n₁ n₂ : Nat), a₁✝.foldConstants = num n₁ → a₂✝.foldConstants = num n₂ → Falseih2✝:eval st a₁✝ = eval st a₁✝.foldConstantsih1✝:eval st a₂✝ = eval st a₂✝.foldConstants⊢ eval st (aexp {~a₁✝ - ~a₂✝}) = eval st (aexp {~a₁✝.foldConstants - ~a₂✝.foldConstants})st:Statea₁✝:Aexpa₂✝:Aexpn₁✝:Natn₂✝:Natx✝¹:a₂✝.foldConstants = num n₂✝x✝:a₁✝.foldConstants = num n₁✝ih2✝:eval st a₁✝ = eval st a₁✝.foldConstantsih1✝:eval st a₂✝ = eval st a₂✝.foldConstants⊢ eval st (aexp {~a₁✝ * ~a₂✝}) = eval st (num (n₁✝ * n₂✝))st:Statea₁✝:Aexpa₂✝:Aexpx✝:∀ (n₁ n₂ : Nat), a₁✝.foldConstants = num n₁ → a₂✝.foldConstants = num n₂ → Falseih2✝:eval st a₁✝ = eval st a₁✝.foldConstantsih1✝:eval st a₂✝ = eval st a₂✝.foldConstants⊢ eval st (aexp {~a₁✝ * ~a₂✝}) = eval st (aexp {~a₁✝.foldConstants * ~a₂✝.foldConstants}) st:Staten✝:Nat⊢ eval st (num n✝) = eval st (num n✝)st:Statex✝:Ident⊢ eval st (aexp {x✝}) = eval st (aexp {x✝})st:Statea₁✝:Aexpa₂✝:Aexpn₁✝:Natn₂✝:Natx✝¹:a₂✝.foldConstants = num n₂✝x✝:a₁✝.foldConstants = num n₁✝ih2✝:eval st a₁✝ = eval st a₁✝.foldConstantsih1✝:eval st a₂✝ = eval st a₂✝.foldConstants⊢ eval st (aexp {~a₁✝ + ~a₂✝}) = eval st (num (n₁✝ + n₂✝))st:Statea₁✝:Aexpa₂✝:Aexpx✝:∀ (n₁ n₂ : Nat), a₁✝.foldConstants = num n₁ → a₂✝.foldConstants = num n₂ → Falseih2✝:eval st a₁✝ = eval st a₁✝.foldConstantsih1✝:eval st a₂✝ = eval st a₂✝.foldConstants⊢ eval st (aexp {~a₁✝ + ~a₂✝}) = eval st (aexp {~a₁✝.foldConstants + ~a₂✝.foldConstants})st:Statea₁✝:Aexpa₂✝:Aexpn₁✝:Natn₂✝:Natx✝¹:a₂✝.foldConstants = num n₂✝x✝:a₁✝.foldConstants = num n₁✝ih2✝:eval st a₁✝ = eval st a₁✝.foldConstantsih1✝:eval st a₂✝ = eval st a₂✝.foldConstants⊢ eval st (aexp {~a₁✝ - ~a₂✝}) = eval st (num (n₁✝ - n₂✝))st:Statea₁✝:Aexpa₂✝:Aexpx✝:∀ (n₁ n₂ : Nat), a₁✝.foldConstants = num n₁ → a₂✝.foldConstants = num n₂ → Falseih2✝:eval st a₁✝ = eval st a₁✝.foldConstantsih1✝:eval st a₂✝ = eval st a₂✝.foldConstants⊢ eval st (aexp {~a₁✝ - ~a₂✝}) = eval st (aexp {~a₁✝.foldConstants - ~a₂✝.foldConstants})st:Statea₁✝:Aexpa₂✝:Aexpn₁✝:Natn₂✝:Natx✝¹:a₂✝.foldConstants = num n₂✝x✝:a₁✝.foldConstants = num n₁✝ih2✝:eval st a₁✝ = eval st a₁✝.foldConstantsih1✝:eval st a₂✝ = eval st a₂✝.foldConstants⊢ eval st (aexp {~a₁✝ * ~a₂✝}) = eval st (num (n₁✝ * n₂✝))st:Statea₁✝:Aexpa₂✝:Aexpx✝:∀ (n₁ n₂ : Nat), a₁✝.foldConstants = num n₁ → a₂✝.foldConstants = num n₂ → Falseih2✝:eval st a₁✝ = eval st a₁✝.foldConstantsih1✝:eval st a₂✝ = eval st a₂✝.foldConstants⊢ eval st (aexp {~a₁✝ * ~a₂✝}) = eval st (aexp {~a₁✝.foldConstants * ~a₂✝.foldConstants}) All goals completed! 🐙

4.4. Soundness of (0 + n) Elimination, Redux🔗

4.5. Proving Inequivalence🔗

Next, let's look at some programs that are not equivalent.

Suppose that c₁ is a command of the form

  X := a₁; Y := a₂

and c₂ is the command

       X := a₁; Y := a₂'

where a₂' is formed by substituting a₁ for all occurrences of X in a₂.

For example, c₁ and c₂ might be:

       c₁  =  (X := 42 + 53;
               Y := Y + X)
       c₂  =  (X := 42 + 53;
               Y := Y + (42 + 53))

Clearly, this particular c₁ and c₂ are equivalent. Is this true in general?

More formally, here is the function that substitutes an arithmetic expression u for each occurrence of a given variable x in another expression a:

def Aexp.subst (x : String) (u : Aexp) (a : Aexp) : Aexp := match a with | Aexp.num n => Aexp.num n | Aexp.id x' => if x = x' then u else Aexp.id x' | (aexp { ~a₁ + ~a₂ }) => (aexp { ~(Aexp.subst x u a₁) + ~(Aexp.subst x u a₂) }) | (aexp { ~a₁ - ~a₂ }) => (aexp { ~(Aexp.subst x u a₁) - ~(Aexp.subst x u a₂) }) | (aexp { ~a₁ * ~a₂ }) => (aexp { ~(Aexp.subst x u a₁) * ~(Aexp.subst x u a₂) }) example : Aexp.subst X (aexp { 42 + 53 }) (aexp { Y + X }) = (aexp { Y + (42 + 53) }) := ⊢ Aexp.subst X (aexp {42 + 53}) (aexp {Y + X}) = aexp {Y + (42 + 53)} All goals completed! 🐙

And here is the property we are interested in, expressing the claim that commands c₁ and c₂ as described above are always equivalent.

def SubstEquivProperty : Prop := ∀ (x₁ x₂ : String) (a₁ a₂ : Aexp), (imp { x₁ := a₁; x₂ := a₂ }) ≃ (imp { x₁ := a₁; x₂ := ~(Aexp.subst x₁ a₁ a₂) })

Sadly, the property does not always hold.

Here is a counterexample:

  X := X + 1; Y := X

If we perform the substitution, we get

  X := X + 1; Y := X + 1

which clearly isn't equivalent.

theorem subst_inequiv : ¬ SubstEquivProperty := ⊢ ¬SubstEquivProperty ⊢ ¬∀ (x₁ x₂ : String) (a₁ a₂ : Aexp), imp {x₁ := ~a₁; x₂ := ~a₂} ≃ imp {x₁ := ~a₁; x₂ := ~(Aexp.subst x₁ a₁ a₂)} contra:∀ (x₁ x₂ : String) (a₁ a₂ : Aexp), imp {x₁ := ~a₁; x₂ := ~a₂} ≃ imp {x₁ := ~a₁; x₂ := ~(Aexp.subst x₁ a₁ a₂)}⊢ False /- Here is the counterexample: assuming that `SubstEquivProperty` holds allows us to prove that these two programs are equivalent... -/ contra:∀ (x₁ x₂ : String) (a₁ a₂ : Aexp), imp {x₁ := ~a₁; x₂ := ~a₂} ≃ imp {x₁ := ~a₁; x₂ := ~(Aexp.subst x₁ a₁ a₂)}c₁:Com := imp {X := X + 1; Y := X}⊢ False contra:∀ (x₁ x₂ : String) (a₁ a₂ : Aexp), imp {x₁ := ~a₁; x₂ := ~a₂} ≃ imp {x₁ := ~a₁; x₂ := ~(Aexp.subst x₁ a₁ a₂)}c₁:Com := imp {X := X + 1; Y := X}c₂:Com := imp {X := X + 1; Y := X + 1}⊢ False contra:∀ (x₁ x₂ : String) (a₁ a₂ : Aexp), imp {x₁ := ~a₁; x₂ := ~a₂} ≃ imp {x₁ := ~a₁; x₂ := ~(Aexp.subst x₁ a₁ a₂)}c₁:Com := imp {X := X + 1; Y := X}c₂:Com := imp {X := X + 1; Y := X + 1}h:c₁ ≃ c₂⊢ False c₁:Com := imp {X := X + 1; Y := X}c₂:Com := imp {X := X + 1; Y := X + 1}h:c₁ ≃ c₂⊢ False /- ... allows us to show that the command `c₂` can terminate in two different final states: st₁ = (Y →ₜ 1 ; X →ₜ 1) st₂ = (Y →ₜ 2 ; X →ₜ 1). -/ c₁:Com := imp {X := X + 1; Y := X}c₂:Com := imp {X := X + 1; Y := X + 1}h:c₁ ≃ c₂st₁:TotalMap Ident Nat := Y →ₜ 1 ; X →ₜ 1⊢ False c₁:Com := imp {X := X + 1; Y := X}c₂:Com := imp {X := X + 1; Y := X + 1}h:c₁ ≃ c₂st₁:TotalMap Ident Nat := Y →ₜ 1 ; X →ₜ 1st₂:TotalMap Ident Nat := Y →ₜ 2 ; X →ₜ 1⊢ False c₁:Com := imp {X := X + 1; Y := X}c₂:Com := imp {X := X + 1; Y := X + 1}h:c₁ ≃ c₂st₁:TotalMap Ident Nat := Y →ₜ 1 ; X →ₜ 1st₂:TotalMap Ident Nat := Y →ₜ 2 ; X →ₜ 1h₁:∅ =[ ~c₁ ]=> st₁⊢ False c₁:Com := imp {X := X + 1; Y := X}c₂:Com := imp {X := X + 1; Y := X + 1}h:c₁ ≃ c₂st₁:TotalMap Ident Nat := Y →ₜ 1 ; X →ₜ 1st₂:TotalMap Ident Nat := Y →ₜ 2 ; X →ₜ 1h₁:∅ =[ ~c₁ ]=> st₁h₂:∅ =[ ~c₂ ]=> st₂⊢ False -- Finally, we use the fact that evaluation is deterministic to obtain a contradiction. c₁:Com := imp {X := X + 1; Y := X}c₂:Com := imp {X := X + 1; Y := X + 1}h:c₁ ≃ c₂st₁:TotalMap Ident Nat := Y →ₜ 1 ; X →ₜ 1st₂:TotalMap Ident Nat := Y →ₜ 2 ; X →ₜ 1h₂:∅ =[ ~c₂ ]=> st₂h₁:∅ =[ ~c₂ ]=> st₁⊢ False c₁:Com := imp {X := X + 1; Y := X}c₂:Com := imp {X := X + 1; Y := X + 1}h:c₁ ≃ c₂st₁:TotalMap Ident Nat := Y →ₜ 1 ; X →ₜ 1st₂:TotalMap Ident Nat := Y →ₜ 2 ; X →ₜ 1h₁:∅ =[ ~c₂ ]=> st₁h₂:st₁ = st₂⊢ False c₁:Com := imp {X := X + 1; Y := X}c₂:Com := imp {X := X + 1; Y := X + 1}h:c₁ ≃ c₂st₁:TotalMap Ident Nat := Y →ₜ 1 ; X →ₜ 1st₂:TotalMap Ident Nat := Y →ₜ 2 ; X →ₜ 1h₁:∅ =[ ~c₂ ]=> st₁h₂:st₁ = st₂contra:st₁[Y] = st₂[Y]⊢ False c₁:Com := imp {X := X + 1; Y := X}c₂:Com := imp {X := X + 1; Y := X + 1}h:c₁ ≃ c₂st₁:TotalMap Ident Nat := Y →ₜ 1 ; X →ₜ 1st₂:TotalMap Ident Nat := Y →ₜ 2 ; X →ₜ 1h₁:∅ =[ ~c₂ ]=> st₁h₂:st₁ = st₂contra:1 = 2⊢ False All goals completed! 🐙

4.6. Extended Exercise: Nondeterministic Imp🔗

4.7. Additional Exercises🔗

Source revision: 9cc9a7b, committed 2026-09-28 19:09 UTC