計算機ソフトウェア工学をCoqでやってみた

hoare.v

Require Import Arith Relations FunctionalExtensionality.

(* 変数の識別子 *)
Definition id := nat.

(* 状態 *)
Definition state := id -> nat.

Definition beq_id : id -> id -> bool := beq_nat.
Definition X := 0.
Definition Y := 1.
Definition empty_state : state := fun _ => 0.

(* 算術式 *)
Inductive aexp : Set :=
| ANum : nat -> aexp
| AVar : id -> aexp
| APlus : aexp -> aexp -> aexp
| AMinus : aexp -> aexp -> aexp
| AMult : aexp -> aexp -> aexp.

(* 算術式の評価文脈 *)
Inductive aeval_context : Set :=
| ACHole : aeval_context
| ACPlusL : aeval_context -> aexp -> aeval_context
| ACPlusR : nat -> aeval_context -> aeval_context
| ACMinusL : aeval_context -> aexp -> aeval_context
| ACMinusR : nat -> aeval_context -> aeval_context
| ACMultL : aeval_context -> aexp -> aeval_context
| ACMultR : nat -> aeval_context -> aeval_context.

(* e_aの穴をi_aで置き換える *)
Fixpoint subst_aexp e_a i_a :=
  match e_a with
    | ACHole => i_a
    | ACPlusL e_a' a => APlus (subst_aexp e_a' i_a) a
    | ACPlusR n e_a' => APlus (ANum n) (subst_aexp e_a' i_a)
    | ACMinusL e_a' a => AMinus (subst_aexp e_a' i_a) a
    | ACMinusR n e_a' => AMinus (ANum n) (subst_aexp e_a' i_a)
    | ACMultL e_a' a => AMult (subst_aexp e_a' i_a) a
    | ACMultR n e_a' => AMult (ANum n) (subst_aexp e_a' i_a)
  end.

(* 算術式の操作的意味論 *)
Inductive aeval_step : aexp * state -> aexp * state -> Prop :=
| A_Var :
    forall e_a x st,
      aeval_step
        (subst_aexp e_a (AVar x), st)
        (subst_aexp e_a (ANum (st x)), st)
| A_Plus :
    forall e_a n1 n2 st,
      aeval_step
        (subst_aexp e_a (APlus (ANum n1) (ANum n2)), st)
        (subst_aexp e_a (ANum (n1 + n2)), st)
| A_Minus :
    forall e_a n1 n2 st,
      aeval_step
        (subst_aexp e_a (AMinus (ANum n1) (ANum n2)), st)
        (subst_aexp e_a (ANum (n1 - n2)), st)
| A_Mult : 
    forall e_a n1 n2 st,
      aeval_step
        (subst_aexp e_a (APlus (ANum n1) (ANum n2)), st)
        (subst_aexp e_a (ANum (n1 * n2)), st).

(* ブール式 *)
Inductive bexp : Set :=
| BTrue : bexp
| BFalse : bexp
| BEq : aexp -> aexp -> bexp
| BLeq : aexp -> aexp -> bexp
| BNot : bexp -> bexp
| BAnd : bexp -> bexp -> bexp.

(* ブール式の評価文脈 *)
Inductive beval_context : Set :=
| BCHole : beval_context
| BCNot : beval_context -> beval_context
| BCAndL : beval_context -> bexp -> beval_context
| BCAndR : bool -> beval_context -> beval_context.

(* e_bの穴をi_bで置き換える *)
Fixpoint subst_bexp e_b i_b :=
  match e_b with
    | BCHole => i_b
    | BCNot e_b' => BNot (subst_bexp e_b' i_b)
    | BCAndL e_b' b => BAnd (subst_bexp e_b' i_b) b
    | BCAndR t e_b' => BAnd (if t then BTrue else BFalse) (subst_bexp e_b' i_b)
  end.

(* ブール式の操作的意味論 *)
Inductive beval_step : bexp * state -> bexp * state -> Prop :=
| B_Eq :
    forall e_b n1 n2 t st,
      t = (if le_lt_dec n1 n2 then BTrue else BFalse) ->
      beval_step
        (subst_bexp e_b (BEq (ANum n1) (ANum n2)), st)
        (subst_bexp e_b t, st)
| B_EqL :
    forall e_b a1 a2 a1' st st',
      aeval_step (a1, st) (a1', st') ->
      beval_step
        (subst_bexp e_b (BEq a1 a2), st)
        (subst_bexp e_b (BEq a1' a2), st')
| B_EqR :
    forall e_b n1 a2 a2' st st',
      aeval_step (a2, st) (a2', st') ->
      beval_step
        (subst_bexp e_b (BEq (ANum n1) a2), st)
        (subst_bexp e_b (BEq (ANum n1) a2'), st')
| B_Leq :
    forall e_b n1 n2 t st,
      t = (if le_lt_dec n1 n2 then BTrue else BFalse) ->
      beval_step
        (subst_bexp e_b (BLeq (ANum n1) (ANum n2)), st)
        (subst_bexp e_b t, st)
| B_LeqL :
    forall e_b a1 a2 a1' st st',
      aeval_step (a1, st) (a1', st') ->
      beval_step
        (subst_bexp e_b (BLeq a1 a2), st)
        (subst_bexp e_b (BLeq a1' a2), st')
| B_LeqR :
    forall e_b n1 a2 a2' st st',
      aeval_step (a2, st) (a2', st') ->
      beval_step
        (subst_bexp e_b (BLeq (ANum n1) a2), st)
        (subst_bexp e_b (BLeq (ANum n1) a2'), st')
| B_NotT :
    forall e_b st,
      beval_step
        (subst_bexp e_b (BNot BTrue), st)
        (subst_bexp e_b BFalse, st)
| B_NotF :
    forall e_b st,
      beval_step
        (subst_bexp e_b (BNot BFalse), st)
        (subst_bexp e_b BTrue, st)
| B_And :
    forall e_b t1 t2 t st,
      t = match t1, t2 with
            | BTrue, BTrue => BTrue
            | _, _ => BFalse
          end ->
      beval_step
        (subst_bexp e_b (BAnd t1 t2), st)
        (subst_bexp e_b t, st).

(* プログラム *)
Inductive com : Set :=
| CSkip : com
| CAss : id -> aexp -> com
| CSeq : com -> com -> com
| CIf : bexp -> com -> com -> com
| CWhile : bexp -> com -> com.

(* プログラムの評価文脈 *)
Inductive ceval_context : Set :=
| CCHole : ceval_context
| CCSeq : ceval_context -> com -> ceval_context.

(* e_cの穴をi_cで置き換える *)
Fixpoint subst_com e_c i_c :=
  match e_c with
    | CCHole => i_c
    | CCSeq e_c' c => CSeq (subst_com e_c' i_c) c
  end.

Definition update (st : state) x n : state :=
  fun y => 
    if beq_id x y then n
    else st y.

(* プログラムの表示的意味論 *)
Inductive ceval_step : com * state -> com * state -> Prop :=
| C_Skip : 
    forall e_c c st,
      ceval_step
        (subst_com e_c (CSeq CSkip c), st)
        (subst_com e_c c, st)
| C_AssignN :
    forall e_c x n st,
      ceval_step
        (subst_com e_c (CAss x (ANum n)), st)
        (subst_com e_c CSkip, update st x n)
| C_AssignA :
    forall e_c x a a' st st',
      aeval_step (a, st) (a', st') ->
      ceval_step
        (subst_com e_c (CAss x a), st)
        (subst_com e_c (CAss x a'), st')
| C_IfT :
    forall e_c c0 c1 st,
      ceval_step
        (subst_com e_c (CIf BTrue c0 c1), st)
        (subst_com e_c c0, st)
| C_IfF :
    forall e_c c0 c1 st,
      ceval_step
        (subst_com e_c (CIf BFalse c0 c1), st)
        (subst_com e_c c1, st)
| C_IfB :
    forall e_c b b' c0 c1 st st',
      beval_step (b, st) (b', st') ->
      ceval_step
        (subst_com e_c (CIf b c0 c1), st)
        (subst_com e_c (CIf b' c0 c1), st')
| C_Wh :
    forall e_c b c st,
      ceval_step
        (subst_com e_c (CWhile b c), st)
        (subst_com e_c (CIf b (CSeq c (CWhile b c)) CSkip), st).

Definition Euclid :=
  CWhile
    (BNot (BEq (AVar X) (AVar Y)))
    (CIf
       (BLeq (AVar X) (AVar Y))
       (CAss Y (AMinus (AVar Y) (AVar X)))
       (CAss X (AMinus (AVar X) (AVar Y)))).

(* 教科書38ページ、例4.1の簡約列 *)
Definition S := 3.
Definition Sum :=
  CWhile
    (BLeq (ANum 1) (AVar X))
    (CSeq
       (CAss S (APlus (AVar S) (AVar X)))
       (CAss X (AMinus (AVar X) (ANum 1)))).
Goal
  clos_refl_trans _
    ceval_step
    (Sum, update (update empty_state X 2) S 0)
    (CSkip, update (update empty_state X 0) S 3).
Proof.
  eapply rt_trans.
    eapply rt_step.
    replace Sum with (subst_com CCHole Sum) by auto.
    constructor.
  eapply rt_trans.
    eapply rt_step.
    constructor.
    replace (BLeq (ANum 1) (AVar X)) with 
      (subst_bexp BCHole (BLeq (ANum 1) (AVar X))) by auto.
    apply B_LeqR.
    replace (AVar X) with (subst_aexp ACHole (AVar X)) by auto.
    constructor.
  eapply rt_trans.
    eapply rt_step.
    constructor.
    constructor.
    simpl.
    reflexivity.
  eapply rt_trans.
    eapply rt_step.
    constructor.
  eapply rt_trans.
    eapply rt_step.
    simpl.
    replace 
      (CSeq
         (CSeq (CAss S (APlus (AVar S) (AVar X)))
               (CAss X (AMinus (AVar X) (ANum 1))))
         (CWhile (BLeq (ANum 1) (AVar X))
                 (CSeq (CAss S (APlus (AVar S) (AVar X)))
                       (CAss X (AMinus (AVar X) (ANum 1)))))) with
    (subst_com 
       (CCSeq
          (CCSeq CCHole
                 (CAss X (AMinus (AVar X) (ANum 1))))
          (CWhile (BLeq (ANum 1) (AVar X))
                  (CSeq (CAss S (APlus (AVar S) (AVar X)))
                        (CAss X (AMinus (AVar X) (ANum 1))))))
       (CAss S (APlus (AVar S) (AVar X)))) by auto.
    constructor.
    replace (APlus (AVar S) (AVar X)) with
      (subst_aexp (ACPlusL ACHole (AVar X)) (AVar S)) by auto.
    constructor.
  eapply rt_trans.
    eapply rt_step.
    constructor.
    unfold update.
    simpl.
    replace (APlus (ANum 0) (AVar X)) with
      (subst_aexp (ACPlusR 0 ACHole) (AVar X)) by auto.
    constructor.
  eapply rt_trans.
    eapply rt_step.
    constructor.
    simpl.
    replace (APlus (ANum 0) (ANum 2)) with
      (subst_aexp ACHole (APlus (ANum 0) (ANum 2))) by auto.
    constructor.
  eapply rt_trans.
    eapply rt_step.
    constructor.
  eapply rt_trans.
    eapply rt_step.
    simpl.
    replace
      (CSeq (CSeq CSkip (CAss X (AMinus (AVar X) (ANum 1))))
            (CWhile (BLeq (ANum 1) (AVar X))
                    (CSeq (CAss S (APlus (AVar S) (AVar X)))
                          (CAss X (AMinus (AVar X) (ANum 1)))))) with
      (subst_com
         (CCSeq CCHole
                (CWhile (BLeq (ANum 1) (AVar X))
                        (CSeq (CAss S (APlus (AVar S) (AVar X)))
                              (CAss X (AMinus (AVar X) (ANum 1))))))
         (CSeq CSkip (CAss X (AMinus (AVar X) (ANum 1))))) by auto.
    constructor.
  eapply rt_trans.
    eapply rt_step.
    constructor.
    replace (AMinus (AVar X) (ANum 1)) with
      (subst_aexp (ACMinusL ACHole (ANum 1)) (AVar X)) by auto.
    constructor.
  eapply rt_trans.
    eapply rt_step.
    constructor.
    unfold update.
    simpl.
    replace (AMinus (ANum 2) (ANum 1)) with
      (subst_aexp ACHole (AMinus (ANum 2) (ANum 1))) by auto.
    constructor.
  eapply rt_trans.
    eapply rt_step.
    constructor.
  eapply rt_trans.
    eapply rt_step.
    simpl.
    replace 
     (CSeq CSkip
        (CWhile (BLeq (ANum 1) (AVar X))
           (CSeq (CAss S (APlus (AVar S) (AVar X)))
              (CAss X (AMinus (AVar X) (ANum 1)))))) with
     (subst_com CCHole (CSeq CSkip
        (CWhile (BLeq (ANum 1) (AVar X))
           (CSeq (CAss S (APlus (AVar S) (AVar X)))
              (CAss X (AMinus (AVar X) (ANum 1))))))) by auto.
    constructor.
  eapply rt_trans.
    eapply rt_step.
    constructor.
  eapply rt_trans.
    eapply rt_step.
    constructor.
    replace (BLeq (ANum 1) (AVar X)) with
      (subst_bexp BCHole (BLeq (ANum 1) (AVar X))) by auto.
    apply B_LeqR.
    replace (AVar X) with (subst_aexp ACHole (AVar X)) by auto.
    constructor.
  eapply rt_trans.
    eapply rt_step.
    constructor.
    constructor.
    simpl.
    reflexivity.
  eapply rt_trans.
    eapply rt_step.
    constructor.
  eapply rt_trans.
    eapply rt_step.
    simpl.
    replace
      (CSeq
         (CSeq (CAss S (APlus (AVar S) (AVar X)))
               (CAss X (AMinus (AVar X) (ANum 1))))
         (CWhile (BLeq (ANum 1) (AVar X))
                 (CSeq (CAss S (APlus (AVar S) (AVar X)))
                       (CAss X (AMinus (AVar X) (ANum 1)))))) with
    (subst_com 
       (CCSeq
          (CCSeq CCHole
                 (CAss X (AMinus (AVar X) (ANum 1))))
          (CWhile (BLeq (ANum 1) (AVar X))
                  (CSeq (CAss S (APlus (AVar S) (AVar X)))
                        (CAss X (AMinus (AVar X) (ANum 1))))))
       (CAss S (APlus (AVar S) (AVar X)))) by auto.
    constructor.
    replace (APlus (AVar S) (AVar X)) with
      (subst_aexp (ACPlusL ACHole (AVar X)) (AVar S)) by auto.
    constructor.
  eapply rt_trans.
    eapply rt_step.
    constructor.
    unfold update.
    simpl.
    replace (APlus (ANum 2) (AVar X)) with
      (subst_aexp (ACPlusR 2 ACHole) (AVar X)) by auto.
    constructor.
  eapply rt_trans.
    eapply rt_step.
    constructor.
    simpl.
    replace (APlus (ANum 2) (ANum 1)) with
      (subst_aexp ACHole (APlus (ANum 2) (ANum 1))) by auto.
    constructor.
  eapply rt_trans.
    eapply rt_step.
    constructor.
  eapply rt_trans.
    eapply rt_step.
    simpl.
    replace
      (CSeq (CSeq CSkip (CAss X (AMinus (AVar X) (ANum 1))))
            (CWhile (BLeq (ANum 1) (AVar X))
                    (CSeq (CAss S (APlus (AVar S) (AVar X)))
                          (CAss X (AMinus (AVar X) (ANum 1)))))) with
      (subst_com
         (CCSeq CCHole
                (CWhile (BLeq (ANum 1) (AVar X))
                        (CSeq (CAss S (APlus (AVar S) (AVar X)))
                              (CAss X (AMinus (AVar X) (ANum 1))))))
         (CSeq CSkip (CAss X (AMinus (AVar X) (ANum 1))))) by auto.
    constructor.
  eapply rt_trans.
    eapply rt_step.
    constructor.
    replace (AMinus (AVar X) (ANum 1)) with
      (subst_aexp (ACMinusL ACHole (ANum 1)) (AVar X)) by auto.
    constructor.
  eapply rt_trans.
    eapply rt_step.
    constructor.
    unfold update.
    simpl.
    replace (AMinus (ANum 1) (ANum 1)) with
      (subst_aexp ACHole (AMinus (ANum 1) (ANum 1))) by auto.
    constructor.
  eapply rt_trans.
    eapply rt_step.
    constructor.
  eapply rt_trans.
    eapply rt_step.
    simpl.
    replace 
     (CSeq CSkip
        (CWhile (BLeq (ANum 1) (AVar X))
           (CSeq (CAss S (APlus (AVar S) (AVar X)))
              (CAss X (AMinus (AVar X) (ANum 1)))))) with
     (subst_com CCHole (CSeq CSkip
        (CWhile (BLeq (ANum 1) (AVar X))
           (CSeq (CAss S (APlus (AVar S) (AVar X)))
              (CAss X (AMinus (AVar X) (ANum 1))))))) by auto.
    constructor.
  eapply rt_trans.
    eapply rt_step.
    constructor.
  eapply rt_trans.
    eapply rt_step.
    constructor.
    replace (BLeq (ANum 1) (AVar X)) with
      (subst_bexp BCHole (BLeq (ANum 1) (AVar X))) by auto.
    apply B_LeqR.
    replace (AVar X) with (subst_aexp ACHole (AVar X)) by auto.
    constructor.
  eapply rt_trans.
    eapply rt_step.
    constructor.
    constructor.
    simpl.
    reflexivity.
  eapply rt_step.
    Print ceval_step.
    replace
 (update
    (fun y : id =>
     if match y with
        | 0 => false
        | 1 => false
        | 2 => false
        | 3 => true
        | Datatypes.S (Datatypes.S (Datatypes.S (Datatypes.S _))) => false
        end
     then 3
     else
      if match y with
         | 0 => true
         | Datatypes.S _ => false
         end
      then 1
      else
       if match y with
          | 0 => false
          | 1 => false
          | 2 => false
          | 3 => true
          | Datatypes.S (Datatypes.S (Datatypes.S (Datatypes.S _))) => false
          end
       then 2
       else
        if match y with
           | 0 => false
           | 1 => false
           | 2 => false
           | 3 => true
           | Datatypes.S (Datatypes.S (Datatypes.S (Datatypes.S _))) => false
           end
        then 0
        else
         if match y with
            | 0 => true
            | Datatypes.S _ => false
            end
         then 2
         else empty_state y) X 0) with (update (update empty_state X 0) S 3).
    constructor.
    unfold update.
    apply functional_extensionality.
    intros.
    destruct x.
      reflexivity.

      destruct x.
        reflexivity.

        destruct x.
          reflexivity.

          destruct x.
            reflexivity.
            reflexivity.
Qed.