<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
Require Import ZArith.
From mathcomp Require Import ssreflect ssrnat seq.

(* Simple Calculator *)

Module Simple.

Inductive expr : Set :=
  | Cst of Z
  | Var of nat
  | Add of expr & expr
  | Min of expr
  | Mul of expr & expr.

Fixpoint eval (env : list Z) (e : expr) : Z :=
  match e with
  | Cst x => x
  | Var n => nth 0 env n
  | Add e1 e2 => eval env e1 + eval env e2
  | Min e1 => 0-eval env e1
  | Mul e1 e2 => eval env e1 * eval env e2
  end%Z.

Inductive code : Set :=
  | Cimm of Z
  | Cget of nat
  | Cadd
  | Cmin
  | Cmul.

Fixpoint eval_code (stack : list Z) (l : list code) :=
  match l with
  | nil => stack
  | c :: l' =>
    let stack' :=
        match c, stack with
        | Cimm x, _ => x :: stack
        | Cget n, _ => nth 0 stack n :: stack
        | Cadd, x :: y :: st => x+y :: st
        | Cmin, x :: st => 0-x :: st
        | Cmul, x :: y :: st => x*y :: st
        | _, _ => nil
        end%Z
    in eval_code stack' l'
  end.

Fixpoint compile d (e : expr) : list code :=
  match e with
  | Cst x => [:: Cimm x]
  | Var n => [:: Cget (d+n)]
  | Add e1 e2 => compile d e2 ++ compile (S d) e1 ++ [:: Cadd]
  | Min e1 =>    compile d e1 ++ [:: Cmin]
  | Mul e1 e2 => compile d e2 ++ compile (S d) e1 ++ [:: Cmul]
  end.

Lemma eval_code_cat stack l1 l2 :
  eval_code stack (l1 ++ l2) = eval_code (eval_code stack l1) l2.
Proof. by elim: l1 stack => //=. Qed.

Theorem compile_correct e d stack :
  eval_code stack (compile d e) = eval (drop d stack) e :: stack.
Proof.
  elim: e d stack => //= [n|e1 IHe1 e2 IHe2|e IHe|e1 IHe1 e2 IHe2] d stack.
  by rewrite nth_drop.
  by rewrite eval_code_cat IHe2 eval_code_cat IHe1.
  by rewrite eval_code_cat IHe.
  by rewrite eval_code_cat IHe2 eval_code_cat IHe1.
Qed.

End Simple.

(* Iterating calculator *)

Module Iterator.

Inductive expr : Set :=
  | Cst of Z
  | Var of nat
  | Add of expr & expr
  | Min of expr
  | Mul of expr & expr.

Fixpoint eval (env : list Z) (e : expr) : Z :=
  match e with
  | Cst x => x
  | Var n => nth 0 env n
  | Add e1 e2 => eval env e1 + eval env e2
  | Min e1 => 0-eval env e1
  | Mul e1 e2 => eval env e1 * eval env e2
  end%Z.

Inductive cmd : Set :=
  | Assign of nat & expr  (* env[n] に結果を入れる *)
  | Seq    of cmd & cmd   (* 順番に実行 *)
  | Repeat of expr & cmd. (* n 回繰り返す *)

Fixpoint repeat_n {A : Type} (n : nat) (f : A -> A) (x : A) :=
  if n is S n' then repeat_n n' f (f x) else x.

Fixpoint eval_cmd (env : list Z) (c : cmd) : list Z :=
  match c with
  | Assign n e => set_nth 0%Z env n (eval env e)
  | Seq c1 c2 => eval_cmd (eval_cmd env c1) c2
  | Repeat e c =>
    if eval env e is Zpos n
    then repeat_n (Pos.to_nat n) (fun e => eval_cmd e c) env
    else env
  end.

Inductive code : Set :=
  | Cimm of Z
  | Cget of nat
  | Cadd
  | Cmin
  | Cmul
  | Cset of nat
  | Crep
  | Cnext.

Definition next_skip c n :=
  match c with
  | Crep => S n
  | Cnext => n - 1
  | _ => n
  end.

Fixpoint eval_code (skip : nat) (stack : list Z) (l : list code) :=
  match l with
  | nil => stack
  | c :: l' =>
    if skip is S _ then eval_code (next_skip c skip) stack l' else
    if c is Cnext then stack else
    let stack' :=
        match c, stack with
        | Cimm x, _ => x :: stack
        | Cget n, _ => nth 0 stack n :: stack
        | Cadd, x :: y :: st => x+y :: st
        | Cmin, x :: st => 0-x :: st
        | Cmul, x :: y :: st => x*y :: st
        | Cset n, x :: st => set_nth 0%Z st n x
        | Crep, Zpos n :: st =>
          repeat_n (Pos.to_nat n) (fun st => eval_code 0 st l') st
        | Crep, _ :: st => st
        | _, _ => nil
        end%Z
    in
    eval_code (next_skip c skip) stack' l'
  end.

Fixpoint compile d (e : expr) : list code :=
  match e with
  | Cst x => [:: Cimm x]
  | Var n => [:: Cget (d+n)]
  | Add e1 e2 => compile d e2 ++ compile (S d) e1 ++ [:: Cadd]
  | Min e1 =>    compile d e1 ++ [:: Cmin]
  | Mul e1 e2 => compile d e2 ++ compile (S d) e1 ++ [:: Cmul]
  end.

Fixpoint compile_cmd (c : cmd) : list code :=
  match c with
  | Assign n e => compile 0 e ++ [:: Cset n]
  | Seq c1 c2  => compile_cmd c1 ++ compile_cmd c2
  | Repeat e c => compile 0 e ++ [:: Crep] ++ compile_cmd c ++ [:: Cnext]
  end.

Definition neutral c :=
  match c with Cnext | Crep => false | _ => true end.

Inductive balanced : list code -> Prop :=
  | Bneutral : forall c, neutral c = true -> balanced [:: c]
  | Bcat : forall l1 l2, balanced l1 -> balanced l2 -> balanced (l1 ++ l2)
  | Brep : forall l, balanced l -> balanced (Crep :: l ++ [:: Cnext]).

Lemma repeat_n_eq {A:Type} n f1 f2  (st : A) :
  (forall st, f1 st = f2 st) -> repeat_n n f1 st = repeat_n n f2 st.
Proof.
  elim: n st => //= n IHn st Heq.
  by rewrite Heq IHn.
Qed.  

Lemma eval_code_cat k stack (l1 l2 : seq code) :
  balanced l1 ->
  eval_code k stack (l1 ++ l2) =
  eval_code k (eval_code k stack l1) l2.
Proof.
  move=> Hbal.
  elim: {l1} Hbal k stack l2.
      by destruct c, k.
    move=> l1 l2 Hbal1 IHl1 Hbal2 IHl2 k st l'.
    by rewrite -catA !IHl1 IHl2.
  move=> l1 Hbal IHl1 k st l'.
  destruct k, st => /=; rewrite -catA !IHl1 //.
  destruct z => //=.
  rewrite subnn.
  do 2 f_equal.
  apply repeat_n_eq => st'.
  by rewrite !IHl1.
Qed.

Hint Constructors balanced.

Lemma compile_balanced n e : balanced (compile n e).
Proof. by elim: e n => /=; auto. Qed.

Theorem compile_correct e d stack :
  eval_code 0 stack (compile d e) = eval (drop d stack) e :: stack.
Proof.
  move: d stack.
  induction e; simpl; intros; auto.
  by rewrite nth_drop.
  by rewrite eval_code_cat ?IHe2 ?eval_code_cat ?IHe1 //;
     apply compile_balanced.
  by rewrite eval_code_cat ?IHe //; apply compile_balanced.
  by rewrite eval_code_cat ?IHe2 ?eval_code_cat ?IHe1 //;
     apply compile_balanced.
Qed.

Lemma compile_cmd_balanced c : balanced (compile_cmd c).
Proof. by elim: c => /=; auto using compile_balanced. Qed.

Lemma compile_cmd_S n c stack :
  balanced c -> eval_code (S n) stack c = stack.
Proof.
  move=> Hbal.
  move: n; induction Hbal => //= n.
    by rewrite eval_code_cat ?IHHbal1.
  by rewrite eval_code_cat //=.
Qed.

Hint Resolve compile_balanced compile_cmd_balanced.

Theorem compile_cmd_correct c stack :
  eval_code 0 stack (compile_cmd c) = eval_cmd stack c.
Proof.
  move: stack.
  induction c => stack /=.
      by rewrite eval_code_cat ?compile_correct ?drop0.
    by rewrite eval_code_cat ?compile_correct ?drop0 // IHc1 IHc2.
  rewrite eval_code_cat ?compile_correct ?drop0 //.
  rewrite /= eval_code_cat //=.
  case: (eval stack e) => //.
      by apply compile_cmd_S.
    move=> p.
    rewrite compile_cmd_S //.
    apply repeat_n_eq=> st.
    by rewrite eval_code_cat //=.
  by move => _; apply compile_cmd_S.
Qed.    

End Iterator.

(* Iterating calculator: ループの長さを明示した場合 *)

Module Iterator2.

Inductive expr : Set :=
  | Cst of Z
  | Var of nat
  | Add of expr & expr
  | Min of expr
  | Mul of expr & expr.

Fixpoint eval (env : list Z) (e : expr) : Z :=
  match e with
  | Cst x => x
  | Var n => nth 0 env n
  | Add e1 e2 => eval env e1 + eval env e2
  | Min e1 => 0-eval env e1
  | Mul e1 e2 => eval env e1 * eval env e2
  end%Z.

Inductive cmd : Set :=
  | Assign of nat & expr  (* env[n] に結果を入れる *)
  | Seq    of cmd & cmd   (* 順番に実行 *)
  | Repeat of expr & cmd. (* n 回繰り返す *)

Fixpoint eval_cmd (env : list Z) (c : cmd) : list Z :=
  match c with
  | Assign n e => set_nth 0%Z env n (eval env e)
  | Seq c1 c2 => eval_cmd (eval_cmd env c1) c2
  | Repeat e c =>
    if eval env e is Zpos n
    then iter (Pos.to_nat n) (fun e => eval_cmd e c) env
    else env
  end.

Inductive code : Set :=
  | Cimm of Z
  | Cget of nat
  | Cadd
  | Cmin
  | Cmul
  | Cset of nat
  | Crep of nat   (* ループの長さ(Cnextまでの命令数) *)
  | Cnext.

Fixpoint eval_code (stack : list Z) (l : list code) :=
  match l with
  | nil => stack
  | c :: l' =>
    let stack' :=
        match c, stack with
        | Cimm x, _ => x :: stack
        | Cget n, _ => nth 0 stack n :: stack
        | Cadd, x :: y :: st => x+y :: st
        | Cmin, x :: st => 0-x :: st
        | Cmul, x :: y :: st => x*y :: st
        | Cset n, x :: st => set_nth 0%Z st n x
        | Crep _, Zpos n :: st => (* seq の iter を使う *)
          iter (Pos.to_nat n) (fun st => eval_code st l') st
        | Crep _, _ :: st => st
        | Cnext, _ => stack
        | _, _ => nil
        end%Z
    in
    match c with
    | Crep n => eval_drop n stack' l'
    | Cnext => stack'
    | _ => eval_code stack' l'
    end 
  end
with eval_drop n st (l : list code) :=  (* 相互再帰 *)
  match l, n with
  | _ :: l', 0 => eval_code st l'
  | _ :: l', S n' => eval_drop n' st l'
  | [::], _ => st
  end.

Fixpoint compile d (e : expr) : list code :=
  match e with
  | Cst x => [:: Cimm x]
  | Var n => [:: Cget (d+n)]
  | Add e1 e2 => compile d e2 ++ compile (S d) e1 ++ [:: Cadd]
  | Min e1 =>    compile d e1 ++ [:: Cmin]
  | Mul e1 e2 => compile d e2 ++ compile (S d) e1 ++ [:: Cmul]
  end.

Fixpoint compile_cmd (c : cmd) : list code :=
  match c with
  | Assign n e => compile 0 e ++ [:: Cset n]
  | Seq c1 c2  => compile_cmd c1 ++ compile_cmd c2
  | Repeat e c =>
      let l := compile_cmd c in
      compile 0 e ++ [:: Crep (length l)] ++ l ++ [:: Cnext]
  end.

Definition neutral c :=
  match c with Cnext | Crep _ => false | _ => true end.

Inductive balanced : list code -> Prop :=
  | Bneutral : forall c, neutral c = true -> balanced [:: c]
  | Bcat : forall l1 l2, balanced l1 -> balanced l2 -> balanced (l1 ++ l2)
  | Brep : forall l, balanced l ->
                     balanced (Crep (length l) :: l ++ [:: Cnext]).

Lemma eval_drop_cat st l1 l2 :
  eval_drop (length l1) st (l1 ++ Cnext :: l2) = eval_code st l2.
Proof. by induction l1. Qed.

Lemma eval_code_cat stack (l1 l2 : seq code) :
  balanced l1 ->
  eval_code stack (l1 ++ l2) =
  eval_code (eval_code stack l1) l2.
Proof.
  move=> Hbal.
  elim: {l1} Hbal stack l2.
      by destruct c.
    move=> l1 l2 Hbal1 IHl1 Hbal2 IHl2 st l'.
    by rewrite -catA !IHl1 IHl2.
  move=> l1 Hbal IHl1 st l'.
  destruct st => /=. by rewrite -catA /= !eval_drop_cat.
  destruct z => //=; rewrite -catA /= !eval_drop_cat //=.
  f_equal.
  apply eq_iter => st'.
  by rewrite !IHl1.
Qed.

Hint Constructors balanced.

Lemma compile_balanced n e : balanced (compile n e).
Proof. by elim: e n => /=; auto. Qed.

Theorem compile_correct e d stack :
  eval_code stack (compile d e) = eval (drop d stack) e :: stack.
Proof.
  move: d stack.
  induction e; simpl; intros; auto.
  by rewrite nth_drop.
  by rewrite eval_code_cat ?IHe2 ?eval_code_cat ?IHe1 //;
     apply compile_balanced.
  by rewrite eval_code_cat ?IHe //; apply compile_balanced.
  by rewrite eval_code_cat ?IHe2 ?eval_code_cat ?IHe1 //;
     apply compile_balanced.
Qed.

Lemma compile_cmd_balanced c : balanced (compile_cmd c).
Proof. by elim: c => /=; auto using compile_balanced. Qed.

Hint Resolve compile_balanced compile_cmd_balanced.

Theorem compile_cmd_correct c stack :
  eval_code stack (compile_cmd c) = eval_cmd stack c.
Proof.
  move: stack.
  induction c => stack /=.
      by rewrite eval_code_cat ?compile_correct ?drop0.
    by rewrite eval_code_cat ?compile_correct ?drop0 // IHc1 IHc2.
  rewrite eval_code_cat ?compile_correct ?drop0 //.
  rewrite /= eval_drop_cat //=.
  case: (eval stack e) => //.
  move=> p.
  apply eq_iter => st.
  by rewrite eval_code_cat //=.
Qed.    

End Iterator2.