Small-step operational semantics of Forth in Coq

forth.v

Set Warnings "-notation-overridden,-parsing".
From Coq Require Import Arith.Arith.
From Coq Require Import Arith.EqNat.
From Coq Require Import Init.Nat.
From Coq Require Import Lia.
From Coq Require Import Lists.List.
Import ListNotations.
From PLF Require Import Maps.
From PLF Require Import Smallstep.
Import Nat.

Inductive com : Type :=
| SSkip
| SSeq (c1 c2 : com)
| SPush (n : nat)
| SPlus
| SMinus
| SMult
| SDup
| SDrop
| SSwap
| SOver
| SEq0
| SNot
| SIf (c1 : com) (c2 : com)
| SWhile (c1 : com) (c2 : com)
| SDec.

Coercion SPush : nat >-> com.

Declare Custom Entry com.
Declare Scope com_scope.
Notation "<{ e }>" := e (at level 0, e custom com at level 99) : com_scope.
(* Notation "( x )" := x (in custom com, x at level 99) : com_scope. *)
Notation "x" := x (in custom com at level 0, x constr at level 0) : com_scope.
Notation "O=" := SEq0 (in custom com at level 0) : com_scope.
Notation "+" := SPlus (in custom com at level 0) : com_scope.
Notation "-" := SMinus (in custom com at level 0) : com_scope.
Notation "*" := SMult (in custom com at level 0) : com_scope.
Notation "'skip'"  := SSkip (in custom com at level 0) : com_scope.
Notation "'dup'"  := SDup (in custom com at level 0) : com_scope.
Notation "'drop'"  := SDrop (in custom com at level 0) : com_scope.
Notation "'swap'"  := SSwap (in custom com at level 0) : com_scope.
Notation "'over'"  := SOver (in custom com at level 0) : com_scope.
Notation "'not'"  := SNot (in custom com at level 0) : com_scope.
Notation "'dec'"  := SDec (in custom com at level 0) : com_scope.
Notation "x y" :=
         (SSeq x y)
           (in custom com at level 90, right associativity) : com_scope.
Notation "'if' y 'else' z 'then'" :=
         (SIf y z)
           (in custom com at level 89, y at level 99, z at level 99) : com_scope.
Notation "'begin' x 'while' y 'repeat'" :=
         (SWhile x y)
            (in custom com at level 89, x at level 99, y at level 99) : com_scope.
Open Scope com_scope.

Inductive val : Type :=
| N (n : nat)
| B (b : bool).

Coercion N : nat >-> val.
Coercion B : bool >-> val.

Definition stack := list val.

Reserved Notation " t '/' st '-->' t' '/' st' "
                  (at level 40, st at level 39, t' at level 39).

Inductive cstep : (com * stack) -> (com * stack) -> Prop :=
  | CS_Not : forall st b,
      <{ not }> / (B b :: st) --> <{ skip }> / (B (negb b) :: st)
  | CS_Eq0 : forall st (n : nat),
      <{ O= }> / (N n :: st) --> <{ skip }> / (B (n =? 0) :: st)
  | CS_Push : forall st (n : nat),
      SPush n / st --> <{ skip }> / (N n :: st)
  | CS_Dup : forall st v,
      <{ dup }> / (v :: st) --> <{ skip }> / (v :: v :: st)
  | CS_Drop : forall st v,
      <{ drop }> / (v :: st) --> <{ skip }> / st
  | CS_DSwap : forall st v1 v2,
      <{ swap }> / (v1 :: v2 :: st) --> <{ skip }> / (v2 :: v1 :: st)
  | CS_DOver : forall st v1 v2,
      <{ over }> / (v1 :: v2 :: st) --> <{ skip }> / (v2 :: v1 :: v2 :: st)
  | CS_Dec : forall st n,
      <{ dec }> / (N (S n) :: st) --> <{ skip }> / (N n :: st)
  | CS_Plus : forall st n m,
      <{ + }> / (N n :: N m :: st) --> <{ skip }> / (N (n + m) :: st)
  | CS_Minus : forall st n m,
      <{ - }> / (N n :: N m :: st) --> <{ skip }> / (N (m - n) :: st)
  | CS_Mult : forall st n m,
      <{ * }> / (N n :: N m :: st) --> <{ skip }> / (N (n * m) :: st)
  (* | CS_SeqAssoc : forall st c1 c2 c3, *)
  (*     <{ (SSeq c1 c2) c3 }> / st --> <{ c1 c2 c3 }> / st *)
  | CS_SeqFinish : forall st c2,
      <{ skip c2 }> / st --> c2 / st
  | CS_SeqStep : forall st c1 c1' st' c2,
      c1 / st --> c1' / st' ->
      <{ c1 c2 }> / st --> <{ c1' c2 }> / st'
  | CS_IfTrue : forall st c1 c2,
      <{ if c1 else c2 then }> / (B true :: st) --> c1 / st
  | CS_IfFalse : forall st c1 c2,
      <{ if c1 else c2 then }> / (B false :: st) --> c2 / st
  | CS_While : forall st c1 c2,
      <{ begin c1 while c2 repeat }> / st
      -->
      <{ c1 if c2 begin c1 while c2 repeat else skip then }> / st

  where " t '/' st '-->' t' '/' st' " := (cstep (t,st) (t',st')).

Definition cmultistep := multi cstep.

Notation " t '/' st '-->*' t' '/' st' " :=
   (multi cstep  (t,st) (t',st'))
   (at level 40, st at level 39, t' at level 39).

(** * Determinism *)
(* If a program can take a step, it must be the only step it can take. *)
Theorem stack_step_deterministic : deterministic cstep.
Proof.
  unfold deterministic.
  intros x y1 y2 H0 H1.
  generalize dependent y2.
  induction H0; intros y2 H1; inversion H1; subst; auto.
  - inversion H4.
  - inversion H0.
  - rewrite (IHcstep _ H5) in *.
    apply IHcstep in H5.
    inversion H5; subst.
    reflexivity.
Qed.

Definition square : com := <{ dup * }>.

Example square2 : forall st p, <{ 2 square p }> / st -->* p / (N 4 :: st).
Proof.
  repeat econstructor.
Qed.

Example sub53 : forall st p, <{ 5 3 - p }> / st -->* p / (N 2 :: st).
Proof.
  repeat econstructor.
Qed.

Definition down_to : com := <{ begin dup O= not while dec repeat }>.

Example down_to5 : forall st p, <{ 5 down_to p }> / st -->* p / (N 0 :: st).
Proof.
  repeat econstructor.
Qed.

Hint Resolve multi_refl : core.

Theorem down_to_correct : forall (n : nat) st p, <{ down_to p }> / (N n :: st) -->* p / (N 0 :: st).
Proof.
  induction n; intros st p.
  - repeat econstructor.
  - econstructor.
    + econstructor. econstructor.
    + eapply multi_trans with (y := (<{ down_to p }>, (N n :: st))).
      * repeat econstructor.
      * apply IHn.
Qed.


Definition factorial_body : com :=  <{ over * swap dec swap }>.

Definition factorial : com :=
  <{ 1 begin over O= not while factorial_body repeat swap drop
   }>.

Example fact0 : forall st p, <{ 0 factorial p }> / st -->* p / (N 1 :: st).
Proof.
  repeat econstructor.
Qed.

Example fact3 : forall st p, <{ 3 factorial p }> / st -->* p / (N 6 :: st).
Proof.
  repeat econstructor.
Qed.

Theorem factorial_body_spec : forall (n acc : nat) st p,
                                 <{ factorial_body p }> / (N acc :: N (S n) :: st)
                            -->* <{ p }> / (N (S n * acc) :: N n :: st).
Proof.
  repeat econstructor.
Qed.

Theorem factorial_correct :
  forall (n : nat) st p, <{ factorial p }> / (N n :: st) -->* p / (N (fact n) :: st).
Proof.
  induction n; intros st p.
  - repeat econstructor.
  - Admit.
Admitted.