I'm trying to implement while_true_nonterm mentioned in .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?

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?

• coq
• theorem-proving
• lean

1 Answer 1

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