<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 Extraction.
From mathcomp Require Import all_ssreflect.

(* 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 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 Iterator.

(* While calculator *)

Module While.

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   (* 順番に実行 *)
  | While  of nat & cmd.  (* env[n] が0になるまで繰り返す *)

Section limited.
Variable h : nat.

Fixpoint iter_until0 h n f (env : list Z) :=
  if nth 0%Z env n is Z0 then Some env
  else if h is h.+1 then obind (iter_until0 h n f) (f env) else None.

Fixpoint eval_cmd (c : cmd) (env : list Z) : option (list Z) :=
  match c with
  | Assign n e => Some (set_nth 0%Z env n (eval env e))
  | Seq c1 c2 => obind (eval_cmd c2) (eval_cmd c1 env)
  | While n c1 => iter_until0 h n (eval_cmd c1) env
  end.

Inductive code : Set :=
  | Cimm of Z
  | Cget of nat
  | Cadd
  | Cmin
  | Cmul
  | Cset of nat
  | Cwhl of nat & nat  (* 監視する変数とループの長さ(Cnextまでの命令数) *)
  | Cnext.

Fixpoint eval_code (l : list code) (stack : list Z) : option (list Z) :=
  match l with
  | nil => Some stack
  | c :: l' =>
    let ev := eval_code l' in
    match c, stack with
    | Cimm x, _ => ev (x :: stack)
    | Cget n, _ => ev (nth 0 stack n :: stack)
    | Cadd, x :: y :: st => ev (x+y :: st)
    | Cmin, x :: st => ev (0-x :: st)
    | Cmul, x :: y :: st => ev (x*y :: st)
    | Cset n, x :: st => ev (set_nth 0%Z st n x)
    | Cwhl n len, _ =>
      obind (eval_drop len l')
            (iter_until0 h n ev stack)
    | Cnext, _ => Some stack
    | _, _ => None
    end%Z
  end
with eval_drop n l st :=  (* 相互再帰 *)
  match l, n with
  | _ :: l', 0 => eval_code l' st
  | _ :: l', S n' => eval_drop n' l' st
  | [::], _ => None
  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
  | While n c =>
      let l := compile_cmd c in
      [:: Cwhl n (length l)] ++ l ++ [:: Cnext]
  end.

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

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

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

Lemma eq_iter_until0 n f g :
  f =1 g -> iter_until0 h n f =1 iter_until0 h n g.
Proof.
  move=> Efg.
  elim: h => //= h' IH st.
  case: (nth _ _ _) => // _; rewrite Efg; by case: (g st).
Qed.

Lemma eval_code_cat stack (l1 l2 : seq code) :
  balanced l1 ->
  eval_code (l1 ++ l2) stack =
  obind (eval_code l2) (eval_code l1 stack).
Proof.
  move=> Hbal.
  elim: {l1} Hbal stack l2.
      by destruct c => //= _ [|a[]].
    move=> l1 l2 Hbal1 IHl1 Hbal2 IHl2 st l'.
    rewrite -catA !IHl1.
    by case: (eval_code l1 st) => //=.
  move=> len l1 Hbal IHl1 st l' /=.
  set lhs := iter_until0 _ _ _ _.
  set rhs := iter_until0 _ _ _ _.
  have -> : lhs = rhs.
    apply eq_iter_until0 => st'.
    rewrite -catA !IHl1.
    by case: (eval_code l1 st').
  case: rhs => //= a.
  by rewrite -catA /= !eval_drop_cat.
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 (compile d e) stack = Some (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 (compile_cmd c) stack = eval_cmd c stack.
Proof.
  move: stack.
  induction c => stack /=.
      by rewrite eval_code_cat ?compile_correct ?drop0.
    rewrite eval_code_cat ?compile_correct ?drop0 // IHc1.
    by case: (eval_cmd c1 stack).
  rewrite (eq_iter_until0 _ _ (eval_cmd c)).
    case: (iter_until0 _ _ _ _) => //= st.
    by rewrite eval_drop_cat.
  move=> st.
  rewrite eval_code_cat // IHc.
  by case: (eval_cmd c st).
Qed.    

End limited.
End While.