CPDT Chap5 のプログラムの非停止性のサンプルの実装と証明を分けてみた。

Chap5.v

Definition reg := nat.
Definition label := nat.

Inductive instr : Set :=
| Imm :reg -> nat -> instr
| Copy : reg -> reg -> instr
| Jmp : label -> instr
| Jnz : reg -> label -> instr.

Definition regs := reg -> nat.

Require Import Arith.
Definition set (rs : regs) (r : reg) (v : nat) : regs :=
  fun r' => if beq_nat r r' then v else rs r'.

Definition exec (pc : label) (rs : regs) (inst :instr): (label * regs) :=
  match inst with
    | Imm r n => ((S pc), (set rs r n))
    | Copy r1 r2 => ((S pc), (set rs r1 (rs r2)))
    | Jmp pc' => (pc', rs)
    | Jnz r pc' => 
      match rs r with
        | O => ((S pc), rs)
        | S _ => (pc', rs)
      end
  end.
      
Lemma exec_total : forall pc rs i,
  exists pc', exists rs', exec pc rs i =  (pc', rs').
  Hint Constructors instr.
  destruct i;  simpl;  eauto.
  case_eq (rs r);  eauto.
Qed.

Section safe.
  Variable prog: label -> instr.
  CoInductive safe : label -> regs -> Prop :=
    | Step : forall pc r pc' r',
      exec pc r (prog pc) = (pc', r')
      -> safe pc' r'
      -> safe pc r.
  Theorem always_safe : forall pc rs,
    safe pc rs.
    cofix;intros;
      destruct (exec_total pc rs (prog pc)) as [? [? ?]];
        econstructor; eauto.
    Qed.
End safe.

Print always_safe.