(* ********************************************** *)
(* Types and Semantics for Programming Languages  *)
(* ********************************************** *)

(* Place an X in front of the appropriate statement *)
(* [ ]  I have done Problems 1 and 2 *)
(* [ ]  I have done Problems 1 and 3 *)


Require Import Coq.Bool.Bool.
Require Import Coq.Arith.Arith.
Require Import Coq.Arith.EqNat.
Require Import Coq.Lists.List.
Import ListNotations.
Require Export Maps.

(* ********************************************** *)
(* Problem 1 *)
(* ********************************************** *)

Inductive pal {X} : list X -> Prop :=
  | pal_empty : pal []
  | pal_unit : forall x, pal [x]
  | pal_step : forall x xs, pal xs -> pal ([x] ++ xs ++ [x]).

Theorem app_rev_distr' : forall (X : Type) (xs ys : list X),
  rev (xs ++ ys) = rev ys ++ rev xs.
Proof.
  intros X xs ys. induction xs.
  - simpl. rewrite -> app_nil_r. reflexivity.
  - simpl. rewrite -> IHxs. rewrite <- app_assoc. reflexivity.
Qed.  

Theorem pal_rev : forall (X : Type) (xs : list X), 
  pal xs -> rev xs = xs.
Proof. 
  intros. induction H. 
  - reflexivity.
  - reflexivity.
  - rewrite -> rev_app_distr. rewrite -> rev_app_distr.
    simpl.  rewrite -> IHpal. reflexivity. 
Qed.

(* ********************************************** *)
(* Problem 2 *)
(* ********************************************** *)

(* States *)

Definition state := total_map nat.

Definition empty_state : state :=
  t_empty 0.

Definition X : id := Id 0.
Definition Y : id := Id 1.
Definition Z : id := Id 2.

(* Arithmetic and boolean expressions *)

Inductive aexp : Type :=
  | ANum : nat -> aexp
  | AId : id -> aexp
  | APlus : aexp -> aexp -> aexp
  | AMinus : aexp -> aexp -> aexp
  | AMult : aexp -> aexp -> aexp.

Inductive bexp : Type :=
  | BTrue : bexp
  | BFalse : bexp
  | BEq : aexp -> aexp -> bexp
  | BLe : aexp -> aexp -> bexp
  | BNot : bexp -> bexp
  | BAnd : bexp -> bexp -> bexp.

Fixpoint aeval (st : state) (a : aexp) : nat :=
  match a with
  | ANum n => n
  | AId x => st x
  | APlus a1 a2 => (aeval st a1) + (aeval st a2)
  | AMinus a1 a2  => (aeval st a1) - (aeval st a2)
  | AMult a1 a2 => (aeval st a1) * (aeval st a2)
  end.

Fixpoint beval (st : state) (b : bexp) : bool :=
  match b with
  | BTrue       => true
  | BFalse      => false
  | BEq a1 a2   => beq_nat (aeval st a1) (aeval st a2)
  | BLe a1 a2   => leb (aeval st a1) (aeval st a2)
  | BNot b1     => negb (beval st b1)
  | BAnd b1 b2  => andb (beval st b1) (beval st b2)
  end.

(* Commands *)

Inductive com : Type :=
  | CSkip : com
  | CAss : id -> aexp -> com
  | CSeq : com -> com -> com
  | CIf : bexp -> com -> com -> com
  | CWhile : bexp -> com -> com
  | CGuard : bexp -> com -> bexp -> com -> com.

Notation "'SKIP'" :=
  CSkip.
Notation "x '::=' a" :=
  (CAss x a) (at level 60).
Notation "c1 ;; c2" :=
  (CSeq c1 c2) (at level 80, right associativity).
Notation "'IFB' b 'THEN' c1 'ELSE' c2 'FI'" :=
  (CIf b c1 c2) (at level 80, right associativity).
Notation "'WHILE' b 'DO' c 'END'" :=
  (CWhile b c) (at level 80, right associativity).
(* !!! *)
Notation "'DO' b1 'THEN' c1 'OR' b2 'THEN' c2 'OD'" := 
  (CGuard b1 c1 b2 c2) (at level 80, right associativity).

(* Evaluation relation *)

Reserved Notation "c1 '/' st '\\' st'" (at level 40, st at level 39).

Inductive ceval : com -> state -> state -> Prop :=
  | E_Skip : forall st,
      SKIP / st \\ st
  | E_Ass  : forall st a1 n x,
      aeval st a1 = n ->
      (x ::= a1) / st \\ (t_update st x n)
  | E_Seq : forall c1 c2 st st' st'',
      c1 / st  \\ st' ->
      c2 / st' \\ st'' ->
      (c1 ;; c2) / st \\ st''
  | E_IfTrue : forall st st' b c1 c2,
      beval st b = true ->
      c1 / st \\ st' ->
      (IFB b THEN c1 ELSE c2 FI) / st \\ st'
  | E_IfFalse : forall st st' b c1 c2,
      beval st b = false ->
      c2 / st \\ st' ->
      (IFB b THEN c1 ELSE c2 FI) / st \\ st'
  | E_WhileEnd : forall b st c,
      beval st b = false ->
      (WHILE b DO c END) / st \\ st
  | E_WhileLoop : forall st st' st'' b c,
      beval st b = true ->
      c / st \\ st' ->
      (WHILE b DO c END) / st' \\ st'' ->
      (WHILE b DO c END) / st \\ st''
  (* !!! *)
  | E_GuardEnd : forall st b1 c1 b2 c2,
      beval st b1 = false ->
      beval st b2 = false ->
      (DO b1 THEN c1 OR b2 THEN c2 OD) / st \\ st
  | E_GuardLoop1 : forall st st' st'' b1 c1 b2 c2,
      beval st b1 = true ->
      c1 / st \\ st' ->
      (DO b1 THEN c1 OR b2 THEN c2 OD) / st' \\ st'' ->
      (DO b1 THEN c1 OR b2 THEN c2 OD) / st \\ st'' 
  | E_GuardLoop2 : forall st st' st'' b1 c1 b2 c2,
      beval st b2 = true ->
      c2 / st \\ st' ->
      (DO b1 THEN c1 OR b2 THEN c2 OD) / st' \\ st'' ->
      (DO b1 THEN c1 OR b2 THEN c2 OD) / st \\ st'' 

  where "c '/' st '\\' st'" := (ceval c st st').

(* Assertions *)

Definition Assertion := state -> Prop.

Definition assert_implies (P Q : Assertion) : Prop :=
  forall st, P st -> Q st.

Notation "P ->> Q" :=
  (assert_implies P Q) (at level 80) : hoare_spec_scope.
Open Scope hoare_spec_scope.

Notation "P <<->> Q" :=
  (P ->> Q /\ Q ->> P) (at level 80) : hoare_spec_scope.

(* Hoare triples *)

Definition hoare_triple
           (P:Assertion) (c:com) (Q:Assertion) : Prop :=
  forall st st',
       c / st \\ st'  ->
       P st  ->
       Q st'.

Notation "{{ P }}  c  {{ Q }}" :=
  (hoare_triple P c Q) (at level 90, c at next level)
  : hoare_spec_scope.

(* Assertions *)

Definition bassn b : Assertion :=
  fun st => (beval st b = true).

Lemma bexp_eval_true : forall b st,
  beval st b = true -> (bassn b) st.
Proof.
  intros b st Hbe.
  unfold bassn. assumption.  Qed.

Lemma bexp_eval_false : forall b st,
  beval st b = false -> ~ ((bassn b) st).
Proof.
  intros b st Hbe contra.
  unfold bassn in contra.
  rewrite -> contra in Hbe. inversion Hbe.  Qed.

(* Assignment *)

(*
             ------------------------------ (hoare_asgn)
             {{Q [X |-> a]}} X::=a {{Q}}
*)


Definition assn_sub X a P : Assertion :=
  fun (st : state) =>
    P (t_update st X (aeval st a)).

Notation "P [ X |-> a ]" := (assn_sub X a P) (at level 10).

Theorem hoare_asgn : forall Q X a,
  {{Q [X |-> a]}} (X ::= a) {{Q}}.
Proof.
  unfold hoare_triple.
  intros Q X a st st' HE HQ.
  inversion HE. subst.
  unfold assn_sub in HQ. assumption.  Qed.

(* Consequence *)

(*
                {{P'}} c {{Q'}}
                   P ->> P'
                   Q' ->> Q
         -----------------------------   (hoare_consequence)
                {{P}} c {{Q}}
*)

Theorem hoare_consequence_pre : forall (P P' Q : Assertion) c,
  {{P'}} c {{Q}} ->
  P ->> P' ->
  {{P}} c {{Q}}.
Proof.
  intros P P' Q c Hhoare Himp.
  intros st st' Hc HP. apply (Hhoare st st'). 
  assumption. apply Himp. assumption. Qed.

Theorem hoare_consequence_post : forall (P Q Q' : Assertion) c,
  {{P}} c {{Q'}} ->
  Q' ->> Q ->
  {{P}} c {{Q}}.
Proof.
  intros P Q Q' c Hhoare Himp.
  intros st st' Hc HP. 
  apply Himp.
  apply (Hhoare st st'). 
  assumption. assumption. Qed.

Theorem hoare_consequence : forall (P P' Q Q' : Assertion) c,
  {{P'}} c {{Q'}} ->
  P ->> P' ->
  Q' ->> Q ->
  {{P}} c {{Q}}.
Proof.
  intros P P' Q Q' c Hht HPP' HQ'Q.
  apply hoare_consequence_pre with (P' := P').
  apply hoare_consequence_post with (Q' := Q').
  assumption. assumption. assumption.  Qed.

(* Skip *)

(*
             --------------------  (hoare_skip)
             {{ P }} SKIP {{ P }}
*)

Theorem hoare_skip : forall P,
     {{P}} SKIP {{P}}.
Proof.
  intros P st st' H HP. inversion H. subst.
  assumption.  Qed.

(* Sequencing *)

(*
               {{ P }} c1 {{ Q }} 
               {{ Q }} c2 {{ R }}
              ---------------------  (hoare_seq)
              {{ P }} c1;;c2 {{ R }}
*)

Theorem hoare_seq : forall P Q R c1 c2,
     {{Q}} c2 {{R}} ->
     {{P}} c1 {{Q}} ->
     {{P}} c1;;c2 {{R}}.
Proof.
  intros P Q R c1 c2 H1 H2 st st' H12 Pre.
  inversion H12; subst.
  apply (H1 st'0 st'); try assumption.
  apply (H2 st st'0); assumption. Qed.

(* Conditional *)

(*
              {{P /\  b}} c1 {{Q}}
              {{P /\ ~b}} c2 {{Q}}
      ------------------------------------  (hoare_if)
      {{P}} IFB b THEN c1 ELSE c2 FI {{Q}} 
*)

Theorem hoare_if : forall P Q b c1 c2,
  {{fun st => P st /\ bassn b st}} c1 {{Q}} ->
  {{fun st => P st /\ ~(bassn b st)}} c2 {{Q}} ->
  {{P}} (IFB b THEN c1 ELSE c2 FI) {{Q}}.
Proof.
  intros P Q b c1 c2 HTrue HFalse st st' HE HP.
  inversion HE; subst. 
  - (* b is true *)
    apply (HTrue st st'). 
      assumption. 
      split. assumption. 
             apply bexp_eval_true. assumption.
  - (* b is false *)
    apply (HFalse st st'). 
      assumption. 
      split. assumption.
             apply bexp_eval_false. assumption. Qed.

(* While *)

(*
               {{P /\ b}} c {{P}}
        -----------------------------------  (hoare_while)
        {{P}} WHILE b DO c END {{P /\ ~b}}
    The proposition [P] is called an _invariant_ of the loop.
*)

Lemma hoare_while : forall P b c,
  {{fun st => P st /\ bassn b st}} c {{P}} ->
  {{P}} WHILE b DO c END {{fun st => P st /\ ~ (bassn b st)}}.
Proof.
  intros P b c Hhoare st st' He HP.
  remember (WHILE b DO c END) as wcom eqn:Heqwcom.
  induction He; try (inversion Heqwcom); subst; clear Heqwcom.
  - (* E_WhileEnd *)
    split. assumption. apply bexp_eval_false. assumption.
  - (* E_WhileLoop *)
    apply IHHe2. reflexivity.
    apply (Hhoare st st'). assumption.
      split. assumption. apply bexp_eval_true. assumption.
Qed.

(* While *)

(*
               {{P /\ b}} c {{P}}
        -----------------------------------  (hoare_while)
        {{P}} WHILE b DO c END {{P /\ ~b}}
    The proposition [P] is called an _invariant_ of the loop.
*)

Lemma hoare_guard : forall P b1 c1 b2 c2,
  {{fun st => P st /\ bassn b1 st}} c1 {{P}} ->
  {{fun st => P st /\ bassn b2 st}} c2 {{P}} ->
  {{P}} DO b1 THEN c1 OR b2 THEN c2 OD {{fun st => P st /\ ~ (bassn b1 st) /\ ~(bassn b2 st)}}.
Proof.
  intros P b1 c1 b2 c2 H1 H2 st st' HG HP.
  remember (DO b1 THEN c1 OR b2 THEN c2 OD) as gcom eqn:Heq.
  induction HG; try (inversion Heq); subst; clear Heq.
  - (* E_GuardEnd *)
    split. assumption. split.
    + apply bexp_eval_false. assumption.
    + apply bexp_eval_false. assumption.
  - (* E_GuardLoop1 *)
    apply IHHG2. reflexivity. apply (H1 st st'). assumption.
    split. assumption. apply bexp_eval_true. assumption.
  - (* E_GuardLoop2 *)
    apply IHHG2. reflexivity. apply (H2 st st'). assumption.
    split. assumption. apply bexp_eval_true. assumption.
Qed.


(* ********************************************** *)
(* Problem 3 *)
(* ********************************************** *)

(* Types *)

Inductive ty : Type := 
  | TBool  : ty 
  | TArrow : ty -> ty -> ty
  (* !!! *)
  | TLift : ty -> ty.

(* Terms *)

Inductive tm : Type :=
  | tvar : id -> tm
  | tapp : tm -> tm -> tm
  | tabs : id -> ty -> tm -> tm
  | ttrue : tm
  | tfalse : tm
  | tif : tm -> tm -> tm -> tm
  (* !!! *)
  | tdelay : tm -> tm
  | tforce : tm -> tm.

(* Values *)

Inductive value : tm -> Prop :=
  | v_abs : forall x T t,
      value (tabs x T t)
  | v_true : 
      value ttrue
  | v_false : 
      value tfalse
  (* !!! *)
  | v_delay : forall t,
      value (tdelay t).

Hint Constructors value.

(* Substitution *)

Reserved Notation "'[' x ':=' s ']' t" (at level 20).

Fixpoint subst (x:id) (s:tm) (t:tm) : tm :=
  match t with
  | tvar x' => 
      if beq_id x x' then s else t
  | tabs x' T t1 => 
      tabs x' T (if beq_id x x' then t1 else ([x:=s] t1)) 
  | tapp t1 t2 => 
      tapp ([x:=s] t1) ([x:=s] t2)
  | ttrue => 
      ttrue
  | tfalse => 
      tfalse
  | tif t1 t2 t3 => 
      tif ([x:=s] t1) ([x:=s] t2) ([x:=s] t3)
  (* !!! *)
  | tdelay t =>
      tdelay ([x:=s]t)
  | tforce t =>
      tforce ([x:=s]t)
  end

where "'[' x ':=' s ']' t" := (subst x s t).

(* Evaluation relation *)

Reserved Notation "t1 '==>' t2" (at level 40).

Inductive step : tm -> tm -> Prop :=
  | ST_AppAbs : forall x T t12 v2,
         value v2 ->
         (tapp (tabs x T t12) v2) ==> [x:=v2]t12
  | ST_App1 : forall t1 t1' t2,
         t1 ==> t1' ->
         tapp t1 t2 ==> tapp t1' t2
  | ST_App2 : forall v1 t2 t2',
         value v1 ->
         t2 ==> t2' -> 
         tapp v1 t2 ==> tapp v1  t2'
  | ST_IfTrue : forall t1 t2,
      (tif ttrue t1 t2) ==> t1
  | ST_IfFalse : forall t1 t2,
      (tif tfalse t1 t2) ==> t2
  | ST_If : forall t1 t1' t2 t3,
      t1 ==> t1' ->
      (tif t1 t2 t3) ==> (tif t1' t2 t3)
  (* !!! *)
  | ST_ForceDelay : forall t,
      (tforce (tdelay t)) ==> t
  | ST_Force : forall t t',
      t ==> t' ->
      (tforce t) ==> (tforce t')

where "t1 '==>' t2" := (step t1 t2).

Hint Constructors step.

(* Contexts *)

Definition context := partial_map ty.

(* Typing relation *)

Reserved Notation "Gamma '|-' t '\in' T" (at level 40).
    
Inductive has_type : context -> tm -> ty -> Prop :=
  | T_Var : forall Gamma x T,
      Gamma x = Some T ->
      Gamma |- tvar x \in T
  | T_Abs : forall Gamma x T11 T12 t12,
      update Gamma x T11 |- t12 \in T12 ->
      Gamma |- tabs x T11 t12 \in TArrow T11 T12
  | T_App : forall T11 T12 Gamma t1 t2,
      Gamma |- t1 \in TArrow T11 T12 ->
      Gamma |- t2 \in T11 ->
      Gamma |- tapp t1 t2 \in T12
  | T_True : forall Gamma,
       Gamma |- ttrue \in TBool
  | T_False : forall Gamma,
       Gamma |- tfalse \in TBool
  | T_If : forall t1 t2 t3 T Gamma,
       Gamma |- t1 \in TBool ->
       Gamma |- t2 \in T ->
       Gamma |- t3 \in T ->
       Gamma |- tif t1 t2 t3 \in T
  (* !!! *)
  | T_Delay : forall t T Gamma,
       Gamma |- t \in T ->
       Gamma |- tdelay t \in TLift T
  | T_Force : forall t T Gamma,
       Gamma |- t \in TLift T ->
       Gamma |- tforce t \in T

where "Gamma '|-' t '\in' T" := (has_type Gamma t T).

Hint Constructors has_type.

(* Canonical Forms *)

Lemma canonical_forms_bool : forall t,
  empty |- t \in TBool ->
  value t ->
  (t = ttrue) \/ (t = tfalse).
Proof.
  intros t HT HVal.
  inversion HVal; intros; subst; try inversion HT; auto.
Qed.

Lemma canonical_forms_fun : forall t T1 T2,
  empty |- t \in (TArrow T1 T2) ->
  value t ->
  exists x u, t = tabs x T1 u.
Proof.
  intros t T1 T2 HT HVal.
  inversion HVal; intros; subst; try inversion HT; subst; auto.
  exists x. exists t0.  auto.
Qed.

(* !!! *)

Lemma canonical_forms_lift : forall (t1 t2 : tm) T,
  empty |- t1 \in (TLift T) ->
  value t1 ->
  exists t2, (empty |- t2 \in T) /\ (t1 = tdelay t2).
Proof.
  intros t1 t2 T HT HVal.
  inversion HVal; intros; subst; try inversion HT; subst; auto.
  exists t. split. assumption. reflexivity.
Qed.

   
(* Progress, by induction on type derivation *)

Theorem progress : forall t T, 
     empty |- t \in T ->
     value t \/ exists t', t ==> t'.

Proof with eauto.
  intros t T Ht.
  remember (@empty ty) as Gamma.
  induction Ht; subst Gamma...
  - (* T_Var *)
    (* contradictory: variables cannot be typed in an
       empty context *)
    inversion H.

  - (* T_App *)
    (* [t] = [t1 t2].  Proceed by cases on whether [t1] is a
       value or steps... *)
    right. destruct IHHt1...
    + (* t1 is a value *)
      destruct IHHt2...
      * (* t2 is also a value *)
        assert (exists x0 t0, t1 = tabs x0 T11 t0).
        eapply canonical_forms_fun; eauto.
        destruct H1 as [x0 [t0 Heq]]. subst.
        exists ([x0:=t2]t0)...

      * (* t2 steps *)
        inversion H0 as [t2' Hstp]. exists (tapp t1 t2')...

    + (* t1 steps *)
      inversion H as [t1' Hstp]. exists (tapp t1' t2)...

  - (* T_If *)
    right. destruct IHHt1...

    + (* t1 is a value *)
      destruct (canonical_forms_bool t1); subst; eauto.

    + (* t1 also steps *)
      inversion H as [t1' Hstp]. exists (tif t1' t2 t3)...

  (* !!! *)
  - (* T_Force *)
    right. destruct IHHt...
    + (* t is a value *)
        assert (exists t1, empty |- t1 \in T /\ t = tdelay t1).
        eapply canonical_forms_lift; eauto.
        destruct H0 as [t1 [Ht1 Heq]]. subst...
    + (* t steps *)
        inversion H as [t' Hstp]. exists (tforce t')...
        
Qed.