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 type class Equiv, so that these relations (and the one for commands, below) can all be written with the notation ≃.

class Equiv (α : Type) where equiv : α → α → Prop infix:70 " ≃ " => Equiv.equiv -- you can type `≃` as \simeq 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! 🐙
Quiz

Are these two programs equivalent?

X := 1;
Y := 2

and

Y := 2;
X := 1

(A) Yes (B) No (C) Not sure

Quiz

What about these?

X := 1;
Y := 2

and

X := 2;
Y := 1

(A) Yes (B) No (C) Not sure

Quiz

What about these?

while (1 ≤ X) {
  X := X + 1
}

and

while (2 ≤ X) {
  X := X + 1
}

(A) Yes (B) No (C) Not sure

Quiz

These?

while (true) {
  while (false) { X := X + 1 }
}

and

while (false) {
  while (true) { X := X + 1 }
}

(A) Yes (B) No (C) Not sure

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! 🐙 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 : bexp {true} ≃ b ) : imp {if (b) {c₁} else {c₂}} ≃ c₁ := b:Bexpc₁:Comc₂:Comhb:bexp {true} ≃ b⊢ imp {if (b) {c₁} else {c₂}} ≃ c₁ b:Bexpc₁:Comc₂:Comhb:bexp {true} ≃ b⊢ ∀ {st st' : State}, (st =[ if (b) {c₁} else {c₂} ]=> st') ↔ st =[ c₁ ]=> st' b:Bexpc₁:Comc₂:Comhb:bexp {true} ≃ bst:Statest':State⊢ (st =[ if (b) {c₁} else {c₂} ]=> st') ↔ st =[ c₁ ]=> st' b:Bexpc₁:Comc₂:Comhb:bexp {true} ≃ bst:Statest':State⊢ (st =[ if (b) {c₁} else {c₂} ]=> st') → st =[ c₁ ]=> st'b:Bexpc₁:Comc₂:Comhb:bexp {true} ≃ bst:Statest':State⊢ (st =[ c₁ ]=> st') → st =[ if (b) {c₁} else {c₂} ]=> st' b:Bexpc₁:Comc₂:Comhb:bexp {true} ≃ bst:Statest':State⊢ (st =[ if (b) {c₁} else {c₂} ]=> st') → st =[ c₁ ]=> st' b:Bexpc₁:Comc₂:Comhb:bexp {true} ≃ bst:Statest':Stateh:st =[ if (b) {c₁} else {c₂} ]=> st'⊢ st =[ c₁ ]=> st' b:Bexpc₁:Comc₂:Comhb:bexp {true} ≃ bst:Statest':Statehb✝:Bexp.eval st b = truehc✝:c₁.EvalR st st'⊢ st =[ c₁ ]=> st'b:Bexpc₁:Comc₂:Comhb:bexp {true} ≃ bst:Statest':Statehb✝:Bexp.eval st b = falsehc✝:c₂.EvalR st st'⊢ st =[ c₁ ]=> st' b:Bexpc₁:Comc₂:Comhb:bexp {true} ≃ bst:Statest':Statehb✝:Bexp.eval st b = truehc✝:c₁.EvalR st st'⊢ st =[ c₁ ]=> st'b:Bexpc₁:Comc₂:Comhb:bexp {true} ≃ bst:Statest':Statehb✝:Bexp.eval st b = falsehc✝:c₂.EvalR st st'⊢ st =[ c₁ ]=> st' All goals completed! 🐙 b:Bexpc₁:Comc₂:Comhb:bexp {true} ≃ bst:Statest':State⊢ (st =[ c₁ ]=> st') → st =[ if (b) {c₁} else {c₂} ]=> st' b:Bexpc₁:Comc₂:Comhb:bexp {true} ≃ bst:Statest':Stateh:st =[ c₁ ]=> st'⊢ st =[ if (b) {c₁} else {c₂} ]=> st' b:Bexpc₁:Comc₂:Comhb:bexp {true} ≃ bst: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 := ~(.id x) } ≃ imp { skip } := x:Ident⊢ imp {x := ~(Aexp.id x)} ≃ imp {skip} x:Ident⊢ ∀ {st st' : State}, (st =[ x := ~(Aexp.id x) ]=> st') ↔ st =[ skip ]=> st' x:Identst:Statest':State⊢ (st =[ x := ~(Aexp.id x) ]=> st') ↔ st =[ skip ]=> st' x:Identst:Statest':State⊢ (st =[ x := ~(Aexp.id x) ]=> st') → st =[ skip ]=> st'x:Identst:Statest':State⊢ (st =[ skip ]=> st') → st =[ x := ~(Aexp.id x) ]=> st' x:Identst:Statest':State⊢ (st =[ x := ~(Aexp.id x) ]=> st') → st =[ skip ]=> st' x:Identst:Statest':Stateh:st =[ x := ~(Aexp.id x) ]=> st'⊢ st =[ skip ]=> st' inversion h with | asgn n h => x:Identst:State⊢ st =[ skip ]=> x →ₜ Aexp.eval st (Aexp.id x) ; st x:Identst:State⊢ st =[ skip ]=> st All goals completed! 🐙 x:Identst:Statest':State⊢ (st =[ skip ]=> st') → st =[ x := ~(Aexp.id x) ]=> st' x:Identst:Statest':Stateh:st =[ skip ]=> st'⊢ st =[ x := ~(Aexp.id x) ]=> st' x:Identst:State⊢ st =[ x := ~(Aexp.id x) ]=> st x:Identst:Stateh':st =[ x := ~(Aexp.id x) ]=> x →ₜ st[x] ; st⊢ st =[ x := ~(Aexp.id x) ]=> st All goals completed! 🐙

4.2. Properties of Behavioral Equivalence🔗

4.2.1. Behavioral Equivalence is an Equivalence🔗

end Com @[refl] theorem Aexp.equiv_refl (a : Aexp) : a ≃ a := a:Aexp⊢ a ≃ a All goals completed! 🐙 @[symm] 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! 🐙 @[refl] theorem Bexp.equiv_refl {b : Bexp} : b ≃ b := b:Bexp⊢ b ≃ b All goals completed! 🐙 @[symm] 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! 🐙 @[refl] theorem Com.equiv_refl {c : Com} : c ≃ c := c:Com⊢ c ≃ c All goals completed! 🐙 @[symm] 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), (trans a) ≃ a @[simp] theorem Aexp.transSound_def {trans : Aexp → Aexp} : TransSound trans ↔ ∀ (a : Aexp), (trans a) ≃ a := trans:Aexp → Aexp⊢ TransSound trans ↔ ∀ (a : Aexp), trans a ≃ a All goals completed! 🐙 def Bexp.TransSound (trans : Bexp → Bexp) : Prop := ∀ (b : Bexp), (trans b) ≃ b @[simp] theorem Bexp.transSound_def {trans : Bexp → Bexp} : TransSound trans ↔ ∀ (b : Bexp), (trans b) ≃ b := trans:Bexp → Bexp⊢ TransSound trans ↔ ∀ (b : Bexp), trans b ≃ b All goals completed! 🐙 def Com.TransSound (trans : Com → Com) : Prop := ∀ (c : Com), (trans c) ≃ c @[simp] theorem Com.transSound_def {trans : Com → Com} : TransSound trans ↔ ∀ (c : Com), (trans c) ≃ c := trans:Com → Com⊢ TransSound trans ↔ ∀ (c : Com), trans c ≃ 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 = id x✝⊢ (∃ n₁_1 n₂, num n₁ = num n₁_1 ∧ id x✝ = num n₂) ∨ aexp {a₁ + a₂}.foldConstants = aexp {~(num n₁) + ~(id x✝)} ∧ aexp {a₁ - a₂}.foldConstants = aexp {~(num n₁) - ~(id x✝)} ∧ aexp {a₁ * a₂}.foldConstants = aexp {~(num n₁) * ~(id 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 = id x✝⊢ (∃ n₁ n₂, id x✝ = num n₁ ∧ a₂.foldConstants = num n₂) ∨ aexp {a₁ + a₂}.foldConstants = aexp {~(id x✝) + ~a₂.foldConstants} ∧ aexp {a₁ - a₂}.foldConstants = aexp {~(id x✝) - ~a₂.foldConstants} ∧ aexp {a₁ * a₂}.foldConstants = aexp {~(id x✝) * ~a₂.foldConstants} All goals completed! 🐙
Note to developers (Niklas Halonen @xhalo32)

Make sure we have explained what named cases hypotheses do (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.id x✝⊢ (∃ n₁_1 n₂, Aexp.num n₁ = Aexp.num n₁_1 ∧ Aexp.id x✝ = Aexp.num n₂) ∨ bexp {a₁ = a₂}.foldConstants = bexp {~(Aexp.num n₁) = ~(Aexp.id x✝)} ∧ bexp {a₁ ≠ a₂}.foldConstants = bexp {~(Aexp.num n₁) ≠ ~(Aexp.id x✝)} ∧ bexp {a₁ ≤ a₂}.foldConstants = bexp {~(Aexp.num n₁) ≤ ~(Aexp.id x✝)} ∧ bexp {a₁ > a₂}.foldConstants = bexp {~(Aexp.num n₁) > ~(Aexp.id 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.id x✝⊢ (∃ n₁ n₂, Aexp.id x✝ = Aexp.num n₁ ∧ a₂.foldConstants = Aexp.num n₂) ∨ bexp {a₁ = a₂}.foldConstants = bexp {~(Aexp.id x✝) = ~a₂.foldConstants} ∧ bexp {a₁ ≠ a₂}.foldConstants = bexp {~(Aexp.id x✝) ≠ ~a₂.foldConstants} ∧ bexp {a₁ ≤ a₂}.foldConstants = bexp {~(Aexp.id x✝) ≤ ~a₂.foldConstants} ∧ bexp {a₁ > a₂}.foldConstants = bexp {~(Aexp.id 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.foldConstants = eval st a induction a with st:Staten:Nat⊢ eval st (num n).foldConstants = eval st (num n) st:Statex:Ident⊢ eval st (id x).foldConstants = eval st (id x) st:Statex:Ident⊢ eval st (id x).foldConstants = eval st (id x)st:Staten:Nat⊢ eval st (num n).foldConstants = eval st (num n) All goals completed! 🐙 st:Statea₁:Aexpa₂:Aexpa₁_ih✝:eval st a₁.foldConstants = eval st a₁a₂_ih✝:eval st a₂.foldConstants = eval st a₂⊢ eval st aexp {a₁ * a₂}.foldConstants = eval st (aexp {a₁ * a₂})st:Statea₁:Aexpa₂:Aexpa₁_ih✝:eval st a₁.foldConstants = eval st a₁a₂_ih✝:eval st a₂.foldConstants = eval st a₂⊢ eval st aexp {a₁ - a₂}.foldConstants = eval st (aexp {a₁ - a₂})st:Statea₁:Aexpa₂:Aexpa₁_ih✝:eval st a₁.foldConstants = eval st a₁a₂_ih✝:eval st a₂.foldConstants = eval st a₂⊢ eval st aexp {a₁ + a₂}.foldConstants = eval st (aexp {a₁ + a₂}) -- `plus`, `minus`, and `mult` follow from the IH and the observation that -- `(aexp {a₁ + a₂}).eval st = a₁.eval st + a₂.eval st -- = (Aexp.num (a₁.eval st + a₂.eval st)).eval st` -- (and similarly for `minus`/`-` and `mult`/`*`). cases Aexp.foldConstants_cases a₁ a₂ with st:Statea₁:Aexpa₂:Aexpa₁_ih✝:eval st a₁.foldConstants = eval st a₁a₂_ih✝:eval st a₂.foldConstants = eval st a₂h:∃ n₁ n₂, a₁.foldConstants = num n₁ ∧ a₂.foldConstants = num n₂⊢ eval st aexp {a₁ * a₂}.foldConstants = eval st (aexp {a₁ * a₂})st:Statea₁:Aexpa₂:Aexpa₁_ih✝:eval st a₁.foldConstants = eval st a₁a₂_ih✝:eval st a₂.foldConstants = eval st a₂h:∃ n₁ n₂, a₁.foldConstants = num n₁ ∧ a₂.foldConstants = num n₂⊢ eval st aexp {a₁ - a₂}.foldConstants = eval st (aexp {a₁ - a₂})st:Statea₁:Aexpa₂:Aexpa₁_ih✝:eval st a₁.foldConstants = eval st a₁a₂_ih✝:eval st a₂.foldConstants = eval st a₂h:∃ n₁ n₂, a₁.foldConstants = num n₁ ∧ a₂.foldConstants = num n₂⊢ eval st aexp {a₁ + a₂}.foldConstants = eval st (aexp {a₁ + a₂}) st:Statea₁:Aexpa₂:Aexpa₁_ih✝:eval st a₁.foldConstants = eval st a₁a₂_ih✝:eval st a₂.foldConstants = eval st a₂n₁:Natn₂:Nath₁:a₁.foldConstants = num n₁h₂:a₂.foldConstants = num n₂⊢ eval st aexp {a₁ * a₂}.foldConstants = eval st (aexp {a₁ * a₂}) All goals completed! 🐙 st:Statea₁:Aexpa₂:Aexpa₁_ih✝:eval st a₁.foldConstants = eval st a₁a₂_ih✝:eval st a₂.foldConstants = eval st a₂h: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₂}.foldConstants = eval st (aexp {a₁ * a₂})st:Statea₁:Aexpa₂:Aexpa₁_ih✝:eval st a₁.foldConstants = eval st a₁a₂_ih✝:eval st a₂.foldConstants = eval st a₂h: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₂}.foldConstants = eval st (aexp {a₁ - a₂})st:Statea₁:Aexpa₂:Aexpa₁_ih✝:eval st a₁.foldConstants = eval st a₁a₂_ih✝:eval st a₂.foldConstants = eval st a₂h: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₂}.foldConstants = eval st (aexp {a₁ + a₂}) 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.foldConstants = eval st a st:Staten✝:Nat⊢ eval st (num n✝) = eval st (num n✝)st:Statex✝:Ident⊢ eval st (id x✝) = eval st (id x✝)st:Statea₁✝:Aexpa₂✝:Aexpn₁✝:Natn₂✝:Natx✝¹:a₂✝.foldConstants = num n₂✝x✝:a₁✝.foldConstants = num n₁✝ih2✝:eval st a₁✝.foldConstants = eval st a₁✝ih1✝:eval st a₂✝.foldConstants = eval st a₂✝⊢ eval st (num (n₁✝ + n₂✝)) = eval st (aexp {a₁✝ + a₂✝})st:Statea₁✝:Aexpa₂✝:Aexpx✝:∀ (n₁ n₂ : Nat), a₁✝.foldConstants = num n₁ → a₂✝.foldConstants = num n₂ → Falseih2✝:eval st a₁✝.foldConstants = eval st a₁✝ih1✝:eval st a₂✝.foldConstants = eval st a₂✝⊢ eval st (aexp {~a₁✝.foldConstants + ~a₂✝.foldConstants}) = eval st (aexp {a₁✝ + a₂✝})st:Statea₁✝:Aexpa₂✝:Aexpn₁✝:Natn₂✝:Natx✝¹:a₂✝.foldConstants = num n₂✝x✝:a₁✝.foldConstants = num n₁✝ih2✝:eval st a₁✝.foldConstants = eval st a₁✝ih1✝:eval st a₂✝.foldConstants = eval st a₂✝⊢ eval st (num (n₁✝ - n₂✝)) = eval st (aexp {a₁✝ - a₂✝})st:Statea₁✝:Aexpa₂✝:Aexpx✝:∀ (n₁ n₂ : Nat), a₁✝.foldConstants = num n₁ → a₂✝.foldConstants = num n₂ → Falseih2✝:eval st a₁✝.foldConstants = eval st a₁✝ih1✝:eval st a₂✝.foldConstants = eval st a₂✝⊢ eval st (aexp {~a₁✝.foldConstants - ~a₂✝.foldConstants}) = eval st (aexp {a₁✝ - a₂✝})st:Statea₁✝:Aexpa₂✝:Aexpn₁✝:Natn₂✝:Natx✝¹:a₂✝.foldConstants = num n₂✝x✝:a₁✝.foldConstants = num n₁✝ih2✝:eval st a₁✝.foldConstants = eval st a₁✝ih1✝:eval st a₂✝.foldConstants = eval st a₂✝⊢ eval st (num (n₁✝ * n₂✝)) = eval st (aexp {a₁✝ * a₂✝})st:Statea₁✝:Aexpa₂✝:Aexpx✝:∀ (n₁ n₂ : Nat), a₁✝.foldConstants = num n₁ → a₂✝.foldConstants = num n₂ → Falseih2✝:eval st a₁✝.foldConstants = eval st a₁✝ih1✝:eval st a₂✝.foldConstants = eval st a₂✝⊢ eval st (aexp {~a₁✝.foldConstants * ~a₂✝.foldConstants}) = eval st (aexp {a₁✝ * a₂✝}) st:Staten✝:Nat⊢ eval st (num n✝) = eval st (num n✝)st:Statex✝:Ident⊢ eval st (id x✝) = eval st (id x✝)st:Statea₁✝:Aexpa₂✝:Aexpn₁✝:Natn₂✝:Natx✝¹:a₂✝.foldConstants = num n₂✝x✝:a₁✝.foldConstants = num n₁✝ih2✝:eval st a₁✝.foldConstants = eval st a₁✝ih1✝:eval st a₂✝.foldConstants = eval st a₂✝⊢ eval st (num (n₁✝ + n₂✝)) = eval st (aexp {a₁✝ + a₂✝})st:Statea₁✝:Aexpa₂✝:Aexpx✝:∀ (n₁ n₂ : Nat), a₁✝.foldConstants = num n₁ → a₂✝.foldConstants = num n₂ → Falseih2✝:eval st a₁✝.foldConstants = eval st a₁✝ih1✝:eval st a₂✝.foldConstants = eval st a₂✝⊢ eval st (aexp {~a₁✝.foldConstants + ~a₂✝.foldConstants}) = eval st (aexp {a₁✝ + a₂✝})st:Statea₁✝:Aexpa₂✝:Aexpn₁✝:Natn₂✝:Natx✝¹:a₂✝.foldConstants = num n₂✝x✝:a₁✝.foldConstants = num n₁✝ih2✝:eval st a₁✝.foldConstants = eval st a₁✝ih1✝:eval st a₂✝.foldConstants = eval st a₂✝⊢ eval st (num (n₁✝ - n₂✝)) = eval st (aexp {a₁✝ - a₂✝})st:Statea₁✝:Aexpa₂✝:Aexpx✝:∀ (n₁ n₂ : Nat), a₁✝.foldConstants = num n₁ → a₂✝.foldConstants = num n₂ → Falseih2✝:eval st a₁✝.foldConstants = eval st a₁✝ih1✝:eval st a₂✝.foldConstants = eval st a₂✝⊢ eval st (aexp {~a₁✝.foldConstants - ~a₂✝.foldConstants}) = eval st (aexp {a₁✝ - a₂✝})st:Statea₁✝:Aexpa₂✝:Aexpn₁✝:Natn₂✝:Natx✝¹:a₂✝.foldConstants = num n₂✝x✝:a₁✝.foldConstants = num n₁✝ih2✝:eval st a₁✝.foldConstants = eval st a₁✝ih1✝:eval st a₂✝.foldConstants = eval st a₂✝⊢ eval st (num (n₁✝ * n₂✝)) = eval st (aexp {a₁✝ * a₂✝})st:Statea₁✝:Aexpa₂✝:Aexpx✝:∀ (n₁ n₂ : Nat), a₁✝.foldConstants = num n₁ → a₂✝.foldConstants = num n₂ → Falseih2✝:eval st a₁✝.foldConstants = eval st a₁✝ih1✝:eval st a₂✝.foldConstants = eval st a₂✝⊢ eval st (aexp {~a₁✝.foldConstants * ~a₂✝.foldConstants}) = eval st (aexp {a₁✝ * a₂✝}) All goals completed! 🐙

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

4.4. 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, these 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 : Ident) (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₂ : Ident) (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₂ : Ident) (a₁ a₂ : Aexp), imp {x₁ := a₁; x₂ := a₂} ≃ imp {x₁ := a₁; x₂ := ~(Aexp.subst x₁ a₁ a₂)} contra:∀ (x₁ x₂ : Ident) (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₂ : Ident) (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₂ : Ident) (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₂ : Ident) (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.5. Extended Exercise: Nondeterministic Imp🔗

4.6. Additional Exercises🔗

Source revision: e85fe77, committed 2026-10-06 21:16 UTC