(*
  https://github.com/coq-community/semantics/blob/master/little.v
*)
Require Import List String.
Import ListNotations.

(*
ρ: env
e: expr
b: bool
i: instr

ρ := (var, val)::ρ | ∅
e := var | val | e+e (only addition possible)
b := e < e  (only < possible. But what about true,false??
i := skip  (empty program. Does nothing. noop)
   | x:=e (assignment to var)
   | i;i
   | while b do i done  (loop)

All values are nat
 *)

Require Import String.

Inductive aexpr : Type :=
| Anum : nat -> aexpr
| Avar : string -> aexpr
| Aplus : aexpr -> aexpr -> aexpr.

Inductive bexpr : Type :=
| Lt : aexpr -> aexpr -> bexpr.

Inductive instr : Type :=
| Skip : instr
| Let : string -> aexpr -> instr
| Seq : instr -> instr -> instr
| While : bexpr -> instr -> instr.

Definition env : Type := list (string * nat).

Inductive aeval : env -> aexpr -> nat -> Prop :=
  (* ρ ⊢ n → n *)
| AEnum : forall (en:env) (n:nat),
    aeval en (Anum n) n
  (* ((var, val)::ρ) ⊢ (var → val) *)
| AEvar : forall (en:env) (val:nat) (var:string),
    aeval ((var,val)::en)%list (Avar var) val   (* Found! *)
  (* var1 ≠ var2
     → (ρ ⊢ (var1 → val1))
     → (((var2,val2)::ρ) ⊢ (var2 → val2))
  *)
| AEvarOther : forall (en:env) (val1 val2:nat) (var1 var2:string),
    var1 <> var2
    -> aeval en (Avar var1) val1
      -> aeval ((var2,val2)::en)%list (Avar var1) val1 (* Even if we had another variable added to the env. *)
  (*
    (ρ ⊢ (e1 → val1))
     → (ρ ⊢ (e2 → val2))
     → (ρ ⊢ (e1 + e2) → (val1 + val2))
   *)
| AEplus : forall (en:env) (e1 e2 : aexpr) (val1 val2 : nat),
    aeval en e1 val1
    -> aeval en e2 val2
    -> aeval en (Aplus e1 e2) (val1 + val2).

Inductive beval : env -> bexpr -> bool -> Prop :=
  (*
  val1 < val2
  → (ρ ⊢ (e1 → val1))
  → (ρ ⊢ (e2 → val2))
  → (ρ ⊢ ((e1 < e2) → true))
   *)
| BEltLeft : forall (en:env) (val1 val2 : nat) (e1 e2 : aexpr),
    (val1 < val2)
    -> aeval en e1 val1
    -> aeval en e2 val2
    -> beval en (Lt e1 e2) true
  (*
  ¬(val1 < val2)
  → (ρ ⊢ (e1 → val1))
  → (ρ ⊢ (e2 → val2))
  → (ρ ⊢ ((e1 < e2) → false))
   *)
| BEltRight : forall (en:env) (val1 val2 : nat) (e1 e2 : aexpr),
    (val2 >= val2)
    -> aeval en e1 val1
    -> aeval en e2 val2
    -> beval en (Lt e1 e2) false.

Inductive envupdate : env -> string -> nat -> env -> Prop :=
(* Update a variable *)
| EnvUpdNew : forall (en:env) (var:string) (val:nat),
    envupdate en var val ((var,val)::en)
(* New variable *)
| EnvUpdOld : forall (en1 en2:env) (var1 var2:string) (val1 val2:nat),
    envupdate en1 var1 val1 en2
    -> var1 <> var2
    (* en2 already has var1 *)
    -> envupdate ((var2,val2)::en1) var1 val1 ((var2,val2)::en2).

Inductive instrevalBS : env -> instr -> env -> Prop :=
| IEBSSkip : forall (en:env), instrevalBS en Skip en
| IEBSLet : forall (en en':env) (var:string) (val:nat) (ae:aexpr),
    aeval en ae val
    -> envupdate en var val en'
    -> instrevalBS en (Let var ae) en'
      (*
    -> envupdate en var val en'
    -> instrevalBS en (Let var ae) en'
       *)
| IEBSSeq : forall (en en1 en2:env) (i1 i2:instr),
    (instrevalBS en i1 en1)
    -> (instrevalBS en1 i2 en2)
    -> instrevalBS en (Seq i1 i2) en2
| IEBSWhileT : forall (en eni enw:env) (i:instr) (be:bexpr),
    beval en be true
    -> instrevalBS en i eni
    -> instrevalBS eni (While be i) enw
    -> instrevalBS en (While be i) enw
| IEBSWhileF : forall (en eni enw:env) (i:instr) (be:bexpr),
    beval en be false
    -> instrevalBS en (While be i) en.


Inductive instrevalSS : env -> instr -> instr -> env -> Prop :=
| IESSLet : forall (en en':env) (var:string) (val:nat) (ae:aexpr),
    aeval en ae val
    -> envupdate en var val en'
    -> instrevalSS en (Let var ae) Skip en'
| IESSSeqOne : forall (en:env) (i:instr),
    instrevalSS en (Seq Skip i) i en
(* i1 reduces to i1' and i1' to i2. Then i1 reduces to i2 *)
(* both i1 and i1' result it en'
   then both i1;i2 and i1';i2 result in en'
 *)
| IESSSeqMany : forall (en en':env) (i1 i1' i2:instr),
    instrevalSS en i1 i1' en'
    -> instrevalSS en (Seq i1 i2) (Seq i1' i2) en'
(* XXX: Only aexpr can be bound to vars, okay. But how can we say that env doesn't change after a while loop??? *)
| IESSWhileT : forall (en:env) (i:instr) (be:bexpr),
    beval en be true
    -> instrevalSS en (While be i) (Seq i (While be i)) en
| IESSWhileF : forall (en:env) (i:instr) (be:bexpr),
    beval en be false
    (* Says that 'give me (While be i), I'll give you skip' *)
    -> instrevalSS en (While be i) Skip en.

Fixpoint lookup (en:env) (var:string) : option nat :=
  match en with
  | []%list => None
  | (x::xs)%list =>
      let '(var', val') := x in
      if (String.eqb var' var) then
        Some val'
      else
        lookup xs var
  end.

Definition bind (A B:Type) (x:option A) (f:A->option B) : option B :=
  match x with
  | None => None
  | Some x' => f x'
  end.
Arguments bind {A B}.

(* XXX: Evaluate aexpr ?? *)
Fixpoint af (en:env) (ae:aexpr) : option nat :=
  match ae with
  | Avar var => lookup en var
  | Anum n => Some n
  | Aplus e1 e2 =>
      bind (af en e1)
      (fun x => 
       bind (af en e2) (fun y => Some(x+y)))
  end.

Example en1 : env := [("x"%string, 2)]%list.
Example en2 : env := [("x"%string, 2); ("y"%string, 3)]%list.
Example ae1 : aexpr := (Aplus (Avar "x"%string) (Avar "y"%string)).

Compute (lookup en1 "x"%string).  (* Some 2 *)
Compute (lookup en1 "a"%string).  (* None *)
Compute (af en1 (Anum 3)).
Compute (af en2 ae1).

Definition bf (en:env) (b:bexpr) : option bool :=
  match b with
  | Lt e1 e2 =>
      bind (af en e1) (fun x =>
        bind (af en e2) (fun y => Some (Nat.ltb x y)))
  end.

(* Only update existing vars. Won't add new vars to env *)
Fixpoint updatefn (en:env) (var:string) (val:nat) : option env :=
  match en with
  | []%list => None
  | ((var',val')::ens)%list =>
      if (string_dec var var') then
        Some ((var, val)::ens)%list
      else
        bind (updatefn ens var val)
          (fun x => Some ((var',val')::x)%list)
      (*
      match (String.eqb var var') with
      | true => Some ((var, val)::ens)%list
      | false =>
          bind (updatefn ens var val)
          (fun x => Some ((var',val')::x)%list)
      end
       *)
  end.
Compute en2.
Compute updatefn en2 "y"%string 5.

Check list nat -> Prop.
Check (list nat) -> Prop.
Check list (nat -> Prop).

Inductive assert : Type :=
| AssertBool (b:bexpr)
| AssertNot (a:assert)
| AssertConj (a1 a2:assert)
| AssertPred (s:string) (n:nat).

Inductive condition : Type :=
| Condition (a1 a2 : assert).

Definition eq_O (n:nat) : {n=O}+{n<>O}.
Proof.
  case n.
  - left.
    reflexivity.
  - right.
    discriminate.
Restart.
  case n.
  auto.
  right.
  discriminate.
Qed.


Definition eq_skip (i:instr) : {i=Skip}+{i<>Skip}.
Proof.
  case i.
  - left.
    reflexivity.
  - intros.
    right.
    discriminate.
  - intros.
    right.
    discriminate.
  - intros.
    right.
    discriminate.
Restart.
  (* [auto] takes care of the simple goal which needed [left] tactic *)
  case i; auto; right; discriminate.
Qed.

Inductive integer : Set :=
| Int (n:nat) : integer.

(*
Goal
  forall (var varname:nat),
    Int var = Int varname.
Proof.
  intros.
  discriminate.
 *)

Goal
  forall (n1 n2:nat),
  Int n1 = Int n2 -> n1 = n2.
Proof.
  intros.
  induction n1.
  - .
  discriminate.

Lemma aeval_lookup :
  forall (en:env) (e:aexpr) (n:nat) (var:string),
  aeval en e n
  -> e = (Avar var)
  -> lookup en var = Some n.
Proof.
  intros en e n varname H.
  induction H.
  - intro H1.
    induction en.
    + discriminate.
    + rewrite <- IHen.
      discriminate.
  - intro H1.
    induction en.
    + 


(*

Fixpoint aeval (en:env) (e:aexpr) : option nat :=
  match e with
  | Avar var => lookup en var
  | Anum n => Some n
  | Aplus e1 e2 =>
     match (aeval en e1) with
     | None => None
     | Some val1 =>
         match (aeval en e2) with
         | None => None
         | Some val2 => Some (val1 + val2)
         end
     end
  end.

Definition beval (en:env) (e:bexpr) : option bool :=
  match e with
  | Lt ae1 ae2 =>
     match (aeval en ae1) with
     | None => None
     | Some val1 =>
         match (aeval en ae2) with
         | None => None
         | Some val2 => Some (Nat.ltb val1 val2)
         end
     end
  end.

Check (lookup []%list "a"%string = Some 3).
Print eq.
Check eq_refl.

Lemma lookup_aeval : forall (en:env) (var:string) (val:nat),
  (lookup en var = Some val) -> aeval en (Avar var) val.
Proof.
  intros.
  apply (AEvar en H).

    (match H with
     | eqrefl val' => val'
     | None => None
     end)
  ).
Qed.

Fixpoint instreval (en:env) (i:instr) : env :=
  match i with
  | Let var ae =>
      let res := (aeval en ae) in
      match res with
      | None => en
      | Some val => ((var,val)::en)%list
      end
  | Seq i1 i2 =>
      let en' := (instreval en i1) in
      (instreval en' i2)
  | While be i' =>
      match (beval en be) with
      | None => en
      | Some true => instreval en (Seq i' (While be i'))
      | Some false => en
      end
  end.
 *)

(*
Inductive var : Set := string.
Inductive val : Set := nat.

Inductive expr : Set :=
| Var : var -> expr
| Val : val -> expr
| Add : expr -> expr -> expr.

Inductive boolean : Set :=
| Lt : expr -> expr -> boolean.

Inductive instr : Set :=
| Skip : instr
| Let : var -> expr -> instr
| Seq : instr -> instr -> instr
| While : bool -> instr -> instr.

Inductive env : Set :=
| Empty : env
| NewVar : var * val -> env.

(*
ρ ⊢ n → n
(var, val)::ρ ⊢ var → val
 *)

Inductive eval : env -> expr -> val -> Prop :=
| ValEval : forall (en:env) (n:expr), 
 *)