Require Import String List Arith Lia.
Import ListNotations.
Open Scope list_scope.
Open Scope string_scope.

Set Implicit Arguments.
Notation var := string.


Inductive arith : Set :=
| Const (n : nat)
| Var (x : var)
| Plus (e1 e2 : arith)
| Minus (e1 e2 : arith)
| Times (e1 e2 : arith).

Coercion Const : nat >-> arith.
Coercion Var : var >-> arith.
Infix "+" := Plus : arith_scope.
Infix "-" := Minus : arith_scope.
Infix "*" := Times : arith_scope.
Delimit Scope arith_scope with arith.

Definition valuation := var -> option nat.

Definition empty : valuation := fun _ => None.
Notation "$0" := (empty).

Definition get (x:var) (v:valuation) : option nat := v x.
Notation "v $? x" := (get x v) (at level 50, left associativity).

Definition set (x:var) (n:nat) (v:valuation) : valuation := 
  fun y => 
    match string_dec x y with 
        | left H => Some n 
        | right H' => get y v
    end.
Notation "v $+ ( x , k )" :=
  (set x k v) (at level 50, left associativity).

Fixpoint interp (e : arith) (v : valuation) : nat :=
  match e with
  | Const n => n
  | Var x =>
    match get x v with
    | None => 0
    | Some n => n
    end
  | Plus e1 e2 => interp e1 v + interp e2 v
  | Minus e1 e2 => interp e1 v - interp e2 v
  | Times e1 e2 => interp e1 v * interp e2 v
  end.

Module Simple.
  Inductive cmd :=
  | Skip
  | Assign (x : var) (e : arith)
  | Sequence (c1 c2 : cmd)
  | If (e : arith) (then_ else_ : cmd)
  | While (e : arith) (body : cmd).

  Notation "x <- e" := (Assign x e%arith) (at level 75).
  Infix ";;" := Sequence (at level 76). 
  Notation "'when' e 'then' then_ 'else' else_ 'done'" :=
    (If e%arith then_ else_) (at level 75, e at level 0).
  Notation "'while' e 'loop' body 'done'" :=
    (While e%arith body) (at level 75).

  Example factorial :=
    "output" <- 1;;
    while "input" loop
      "output" <- "output" * "input";;
      "input" <- "input" - 1
    done.

  Inductive eval : valuation -> cmd -> valuation -> Prop :=
  | EvalSkip : forall v,
    eval v Skip v
  | EvalAssign : forall v x e,
    eval v (Assign x e) (v $+ (x, interp e v))
  | EvalSeq : forall v c1 v1 c2 v2,
    eval v c1 v1
    -> eval v1 c2 v2
    -> eval v (Sequence c1 c2) v2
  | EvalIfTrue : forall v e then_ else_ v',
    interp e v <> 0
    -> eval v then_ v'
    -> eval v (If e then_ else_) v'
  | EvalIfFalse : forall v e then_ else_ v',
    interp e v = 0
    -> eval v else_ v'
    -> eval v (If e then_ else_) v'
  | EvalWhileTrue : forall v e body v' v'',
    interp e v <> 0
    -> eval v body v'
    -> eval v' (While e body) v''
    -> eval v (While e body) v''
  | EvalWhileFalse : forall v e body,
    interp e v = 0
    -> eval v (While e body) v.

     
  Inductive step : valuation * cmd -> valuation * cmd -> Prop :=
  | StepAssign : forall v x e,
    step (v, Assign x e) (v $+ (x, interp e v), Skip)
  | StepSeq1 : forall v c1 c2 v' c1',
    step (v, c1) (v', c1')
    -> step (v, Sequence c1 c2) (v', Sequence c1' c2)
  | StepSeq2 : forall v c2,
    step (v, Sequence Skip c2) (v, c2)
  | StepIfTrue : forall v e then_ else_,
    interp e v <> 0
    -> step (v, If e then_ else_) (v, then_)
  | StepIfFalse : forall v e then_ else_,
    interp e v = 0
    -> step (v, If e then_ else_) (v, else_)
  | StepWhileTrue : forall v e body,
    interp e v <> 0
    -> step (v, While e body) (v, Sequence body (While e body))
  | StepWhileFalse : forall v e body,
    interp e v = 0
    -> step (v, While e body) (v, Skip).


  Inductive trc {A:Type} {R:A -> A -> Prop}: A -> A -> Prop :=
  | TrcRefl : forall x, trc x x
  | TrcFront : forall x y z
    (STEP: R x y)
    (STAR: trc y z),
      trc x z.

  Notation "R ^*" := (@trc _ R) (at level 0).

  Lemma gss:
    forall v x k, (v $+ (x,k)) $? x = Some k.
  Proof.
    intros v x k. unfold get, set.
    destruct string_dec; auto. contradiction.
  Qed.

  Lemma gso:
    forall v x y k, x <> y -> (v $+ (x,k)) $? y = v $? y.
  Proof.
    intros v x y k H. unfold get, set. destruct string_dec; auto.
    subst. contradiction.
  Qed.
  
  Theorem factorial_2_small :
    exists v, step^* ($0 $+ ("input", 2), factorial) (v, Skip)
         /\ v $? "output" = Some 2.
  Proof.
    eexists.
    split.
    - econstructor.
      { unfold factorial. repeat econstructor. }
      econstructor.
      { simpl. apply StepSeq2. }
      econstructor.
      { apply StepWhileTrue. simpl. lia. }
      econstructor.
      { repeat econstructor. }
      econstructor.
      { econstructor. apply StepSeq2. }
      econstructor.
      { repeat econstructor. }
      econstructor.
      { apply StepSeq2. }
      econstructor.
      { apply StepWhileTrue. simpl. lia. }
      econstructor.
      { repeat econstructor. }
      econstructor.
      { econstructor. apply StepSeq2. }
      econstructor.
      { repeat econstructor. }
      econstructor.
      { apply StepSeq2. }
      econstructor.
      { apply StepWhileFalse. simpl. reflexivity. }
      simpl. constructor.
    - rewrite gso.
      2: { unfold not. intros H. inversion H. }
      rewrite gss. reflexivity.
  Qed.

  Theorem eval_det :
    forall v c v1,
    eval v c v1 ->
    forall v2, eval v c v2 ->
          v1 = v2.
  Proof.
  Admitted.

  
  Theorem step_det :
    forall s out1,
    step s out1 ->
    forall out2, step s out2 ->
            out1 = out2.
  Proof.
  Admitted.


  Lemma trc_nondet:
    step^* ($0, Skip;;Skip) ($0, Skip;; Skip) /\
      step^* ($0, Skip;;Skip) ($0, Skip).
  Proof.
  Admitted.

  
  Theorem strong_progress_step:
    forall v c,
      c = Skip \/ exists v' c', step (v, c) (v', c').
  Proof.
  Admitted.

  Definition normal_form {A:Type} (R:A -> A-> Prop) (a:A) : Prop :=
    ~ exists a', R a a'.


  Theorem skip_normal_form:
    forall v c,
      c = Skip <-> normal_form step (v,c).
  Proof.
  Admitted.

  Lemma trc_nf:
    forall A (R:A -> A -> Prop) a a'
      (STAR: R^* a a')
      (NF: normal_form R a),
      a' = a.
  Proof.
  Admitted.
  
  Theorem trc_determinism:
    forall A (R:A -> A -> Prop)
      (RDET: forall a a1 a2, R a a1 -> R a a2 -> a1 = a2)
      (s f1 f2: A)
      (STAR1: R^* s f1)
      (NF1: normal_form R f1)
      (STAR2: R^* s f2)
      (NF2: normal_form R f2),
      f1 = f2.
  Proof.
  Admitted.

  Corollary multistep_determinism :
    forall v c vf1 vf2
      (STAR1: step^* (v,c) (vf1, Skip))
      (STAR2: step^* (v,c) (vf2, Skip)),
      vf1 = vf2.
  Proof.
  Admitted.

  Theorem not_normalizing:
    ~ (forall s,
        exists sfinal, step^* s sfinal /\ normal_form step sfinal).
  Proof.
  Admitted.
  
Lemma multi_step_trans:
    forall v1 c1 v2 c2 v3 c3
      (STAR1: step^* (v1,c1) (v2,c2))
      (STAR2: step^* (v2,c2) (v3,c3)),
      step^* (v1,c1) (v3,c3).
  Proof.
    intros v1 c1 v2 c2 v3 c3 STAR1 STAR2. induction STAR1; auto.
    econstructor. apply STEP.
    apply IHSTAR1. assumption.
  Qed.
  
  Require Import Coq.Program.Equality.
  
  Lemma step_star_Seq : forall v c1 c2 v' c1',
    step^* (v, c1) (v', c1')
    -> step^* (v, Sequence c1 c2) (v', Sequence c1' c2).
  Proof.
  Admitted.
  
  Theorem big_small :
    forall v c v',
      eval v c v' ->
      step^* (v, c) (v', Skip).
  Proof.
  Admitted.

  Lemma small_big_fs: forall x y,
      step x y ->
      forall v', eval (fst y) (snd y) v' ->
            eval (fst x) (snd x) v'.
  Proof.
  Admitted.
  
  Lemma small_big'' : forall v c v' c',
      step (v, c) (v', c') ->
      forall v'', eval v' c' v'' ->
             eval v c v''.
  Proof.
  Admitted.

  Lemma small_big' :
    forall v c v' c',
      step^* (v, c) (v', c') ->
      forall v'', eval v' c' v'' ->
             eval v c v''.
  Proof.
  Admitted.
  
  Theorem small_big :
    forall v c v',
       step^* (v, c) (v', Skip) ->
       eval v c v'.
  Proof.
  Admitted.
  
  Inductive context :=
  | Hole
  | CSeq (C : context) (c : cmd).

  Inductive plug : context -> cmd -> cmd -> Prop :=
  | PlugHole : forall c, plug Hole c c
  | PlugSeq : forall c C c' c2,
    plug C c c'
    -> plug (CSeq C c2) c (Sequence c' c2).

  Inductive step0 : valuation * cmd -> valuation * cmd -> Prop :=
  | Step0Assign : forall v x e,
    step0 (v, Assign x e) (v $+ (x, interp e v), Skip)
  | Step0Seq : forall v c2,
    step0 (v, Sequence Skip c2) (v, c2)
  | Step0IfTrue : forall v e then_ else_,
    interp e v <> 0
    -> step0 (v, If e then_ else_) (v, then_)
  | Step0IfFalse : forall v e then_ else_,
    interp e v = 0
    -> step0 (v, If e then_ else_) (v, else_)
  | Step0WhileTrue : forall v e body,
    interp e v <> 0
    -> step0 (v, While e body) (v, Sequence body (While e body))
  | Step0WhileFalse : forall v e body,
    interp e v = 0
    -> step0 (v, While e body) (v, Skip).

  Inductive cstep : valuation * cmd -> valuation * cmd -> Prop :=
  | CStep : forall C v c v' c' c1 c2,
      plug C c c1 ->
      step0 (v, c) (v', c') ->
      plug C c' c2 ->
      cstep (v, c1) (v', c2).

  Theorem step_cstep :
    forall v c v' c',
    step (v, c) (v', c') ->
    cstep (v, c) (v', c').
  Proof.
  Admitted.
  
  Lemma step0_step :
    forall v c v' c',
      step0 (v, c) (v', c') ->
      step (v, c) (v', c').
  Proof.
  Admitted.

  Lemma cstep_step' :
    forall C c0 c,
      plug C c0 c  ->
      forall v' c'0 v c',
        step0 (v, c0) (v', c'0) ->
        plug C c'0 c' ->
        step (v, c) (v', c').
  Proof.
  Admitted.

  Theorem cstep_step :
    forall v c v' c',
    cstep (v, c) (v', c') ->
    step (v, c) (v', c').
  Proof.
  Admitted.

  Theorem cstep_det :
    forall s out1,
    cstep s out1 ->
    forall out2, cstep s out2 ->
            out1 = out2.
  Proof.
  Admitted.


  Fixpoint simplify_arith (a:arith) : arith :=
    match a with
    | Plus a1 a2 =>
        let s1 := simplify_arith a1 in
        let s2 := simplify_arith a2 in
        match s1,s2 with
        | Const n1, Const n2 => Const (n1 + n2)
        | Const 0, e => e
        | e, Const 0 => e
        | _, _ => Plus s1 s2
        end
    | _ => a
            (* we could do other simplifications *)
    end.

  Fixpoint simplify_cmd (c:cmd) : cmd :=
    match c with
    | Skip => Skip
    | Assign v a => Assign v (simplify_arith a)
    | Sequence c1 c2 =>
        Sequence (simplify_cmd c1) (simplify_cmd c2)
    | If a c1 c2 =>
        If (simplify_arith a) (simplify_cmd c1) (simplify_cmd c2)
    | While a c1 =>
        While (simplify_arith a) (simplify_cmd c1)
    end.

  Theorem simplify_cmd_correct:
    forall s1 s2 (STAR: step^* s1 s2),
      step^* (fst s1, simplify_cmd (snd s1))
        (fst s2, simplify_cmd (snd s2)).
  Proof.
  Admitted.

  End Simple.



Module Concurrent.
  Inductive cmd :=
  | Skip
  | Assign (x : var) (e : arith)
  | Sequence (c1 c2 : cmd)
  | If (e : arith) (then_ else_ : cmd)
  | While (e : arith) (body : cmd)
  | Parallel (c1 c2 : cmd).

  Notation "x <- e" := (Assign x e%arith) (at level 75).
  (* This one changed slightly, to avoid parsing clashes. *)
  Infix ";;" := Sequence (at level 76). 
  Notation "'when' e 'then' then_ 'else' else_ 'done'" :=
    (If e%arith then_ else_) (at level 75, e at level 0).
  Notation "'while' e 'loop' body 'done'" :=
    (While e%arith body) (at level 75).
  Infix "||" := Parallel.

  Lemma gss:
    forall v x k, (v $+ (x,k)) $? x = Some k.
  Proof.
    intros v x k. unfold get, set.
    destruct string_dec; auto. contradiction.
  Qed.

  Lemma gso:
    forall v x y k, x <> y -> (v $+ (x,k)) $? y = v $? y.
  Proof.
    intros v x y k H. unfold get, set. destruct string_dec; auto.
    subst. contradiction.
  Qed.

  Inductive context :=
  | Hole
  | CSeq (C : context) (c : cmd)
  | CPar1 (C : context) (c : cmd)
  | CPar2 (c : cmd) (C : context).

  Inductive plug : context -> cmd -> cmd -> Prop :=
  | PlugHole : forall c, plug Hole c c
  | PlugSeq : forall c C c' c2,
    plug C c c'
    -> plug (CSeq C c2) c (Sequence c' c2)
  | PlugPar1 : forall c C c' c2,
    plug C c c'
    -> plug (CPar1 C c2) c (Parallel c' c2)
  | PlugPar2 : forall c C c' c1,
    plug C c c'
    -> plug (CPar2 c1 C) c (Parallel c1 c').

  Inductive step0 : valuation * cmd -> valuation * cmd -> Prop :=
  | Step0Assign : forall v x e,
    step0 (v, Assign x e) (v $+ (x, interp e v), Skip)
  | Step0Seq : forall v c2,
    step0 (v, Sequence Skip c2) (v, c2)
  | Step0IfTrue : forall v e then_ else_,
    interp e v <> 0
    -> step0 (v, If e then_ else_) (v, then_)
  | Step0IfFalse : forall v e then_ else_,
    interp e v = 0
    -> step0 (v, If e then_ else_) (v, else_)
  | Step0WhileTrue : forall v e body,
    interp e v <> 0
    -> step0 (v, While e body) (v, Sequence body (While e body))
  | Step0WhileFalse : forall v e body,
    interp e v = 0
    -> step0 (v, While e body) (v, Skip)
  | Step0Par1 : forall v c,
    step0 (v, Parallel Skip c) (v, c).

  Inductive cstep : valuation * cmd -> valuation * cmd -> Prop :=
  | CStep : forall C v c v' c' c1 c2,
    plug C c c1
    -> step0 (v, c) (v', c')
    -> plug C c' c2
    -> cstep (v, c1) (v', c2).

  Inductive trc {A:Type} {R:A -> A -> Prop}: A -> A -> Prop :=
  | TrcRefl : forall x, trc x x
  | TrcFront : forall x y z
    (STEP: R x y)
    (STAR: trc y z),
      trc x z.

  Notation "R ^*" := (@trc _ R) (at level 0).


  Definition prog :=
    ("a" <- "n";;
     "n" <- "a" + 1)
    || ("b" <- "n";;
        "n" <- "b" + 1).

  Local Hint Constructors plug step0 cstep : core.

  Theorem correctAnswer :
    forall n, exists v, cstep^* ($0 $+ ("n", n), prog) (v, Skip)
              /\ v $? "n" = Some (n + 2).
  Proof.
  Admitted.
  
  Theorem wrongAnswer :
    forall n, exists v, cstep^* ($0 $+ ("n", n), prog) (v, Skip)
              /\ v $? "n" = Some (n + 1).
  Proof.
  Admitted.
  
End Concurrent.