I'm trying to implement while_true_nonterm mentioned in https://softwarefoundations.cis.upenn.edu/current/plf-current/Equiv.html.
I have implemented imp language as follows:
import Mathlib.Data.Nat.Basic
import Mathlib.Tactic
-- A `state` can be modeled as a function mapping variable names
-- to values (e.g., natural numbers in this tutorial)
def state := String -> ℕ
-- Retrive the value of a variable in the state
def get (st: state) (x : String) : ℕ := st x
-- Update the state with a new value for a variable
def set (st: state) (x : String) (v: ℕ) : state :=
fun y => if y = x then v else st y
-- Syntax of commands
inductive com: Type
| skip: com -- nop
| assign (x : String) (a: ℕ) : com -- x := a
| seq (c1 c2 : com) : com -- c1; c2
| if_ (b : Bool) (c1 c2 : com) : com -- if b then c1 else c2
| while (b : Bool) (c : com) : com -- while b do c
-- inductive definitions in Lean come with an important implicit principle:
-- ** the only ways to construct proofs of the inductive relation are through its constructors.
-- State transition
inductive ceval : com -> state -> state -> Prop
| E_Skip : ∀ (st : state),
ceval com.skip st st
| E_Assign : ∀ (st : state) (x : String) (n : ℕ),
ceval (com.assign x n) st (set st x n)
| E_Seq : ∀ (c1 c2 : com) (st st' st'' : state),
ceval c1 st st' →
ceval c2 st' st'' →
ceval (com.seq c1 c2) st st''
| E_IfTrue : ∀ (st st' : state) (b : Bool) (c1 c2 : com),
b = true → ceval c1 st st' → ceval (com.if_ b c1 c2) st st'
| E_IfFalse : ∀ (st st' : state) (b : Bool) (c1 c2 : com),
b = false → ceval c2 st st' → ceval (com.if_ b c1 c2) st st'
| E_WhileFalse : ∀ (st : state) (b : Bool) (c : com),
b = false → ceval (com.while b c) st st
| E_WhileTrue : ∀ (st st' st'' : state) (b : Bool) (c : com),
b = true → ceval c st st' → ceval (com.while b c) st' st'' → ceval (com.while b c) st st''
Now, I'm trying to prove while_true_nonterm, which states that if the loop condition is always true, then it never terminates.
Here's my current draft:
theorem while_true_nonterm:
∀ (b : Bool) (c : com) (st st' : state),
b = true → ¬(ceval (com.while b c) st st') := by
intros b c st st' htrue hceval
cases hceval
case E_WhileFalse hfalse =>
rw[hfalse] at htrue
contradiction
case E_WhileTrue st'' htrue' hc hw =>
I'm stuck at this point and not sure how to proceed. Any suggestions?
Your code is very Rocq-like, so, to start with, here is a version that would be more idiomatic in Lean (mostly using a capitalized case for types, a snake case for constructors, and transforming propositions of the form ∀ b : Bool, b = true → P[b] into P[true]):
def State := String -> Nat
-- Retrive the value of a variable in the state
def get (st: State) (x : String) : Nat := st x
-- Update the state with a new value for a variable
def set (st: State) (x : String) (v: Nat) : State :=
fun y => if y = x then v else st y
-- Syntax of commands
inductive Command : Type where
| skip -- nop
| assign (x : String) (a: Nat) -- x := a
| seq (c1 c2 : Command) -- c1; c2
| if_ (b : Bool) (c1 c2 : Command) -- if b then c1 else c2
| while (b : Bool) (c : Command) -- while b do c
-- inductive definitions in Lean come with an important implicit principle:
-- ** the only ways to construct proofs of the inductive relation are through its constructors.
-- State transition
inductive Eval : Command -> State -> State -> Prop where
| skip (st : State) : Eval .skip st st
| assign (st : State) (x : String) (n : Nat) : Eval (.assign x n) st (set st x n)
| seq (c₁ c₂ : Command) (st₁ st₂ st₃ : State) :
Eval c₁ st₁ st₂ → Eval c₂ st₂ st₃ → Eval (.seq c₁ c₂) st₁ st₃
| if_true (st₁ st₂ : State) (c₁ c₂ : Command) : Eval c₁ st₁ st₂ → Eval (.if_ true c₁ c₂) st₁ st₂
| if_false (st₁ st₂ : State) (c₁ c₂ : Command) : Eval c₂ st₁ st₂ → Eval (.if_ false c₁ c₂) st₁ st₂
| while_false (st : State) (c : Command) :
Eval (.while false c) st st
| while_true (st₁ st₂ st₃ : State) (c : Command) :
Eval c st₁ st₂ → Eval (.while true c) st₂ st₃ → Eval (.while true c) st₁ st₃
Then, the theorem itself can be proven by induction. The informal reasoning is: to show that a while true loop cannot terminate, assume that it can, and, by induction, prove that you can derive a contradiction. By case analysis, there is only one way such a program could evaluate, and that's by first terminating the while true loop, and then performing an evaluation step. But, by induction hypothesis, having a while true loop terminating is absurd. This is actually much more concise in Lean:
theorem while_true_nonterm : ∀ c st₁ st₂, ¬ Eval (.while true c) st₁ st₂ := by
intros c st₁ st₂ h
generalize e : Command.while true c = c' at h
induction h <;> cases e
next ih =>
apply ih
rfl