(* Final Exam *)
(* Your name and matric number *REQUIRED FOR CREDIT* : *)

(* Instructions: 
    
    Please replace the "admit" tactics below with other tactics.  There
    are a few places (such as your name and matric number above)
    where you are required to put in a short amount of text.
    
    There are five problems here, of which you need to do any four.
    There is no extra credit, so once you have solved four problems
    then turn your attention to the written part of the exam.  Each problem
    is worth 9 points.
    
    I have included several hints and other proofs that you could examine
    to understand how to do the proofs that you have to do.
    
    The modal logic and Hoare logic setups are the same as in 
    HW5 and HW10.  Hopefully that should help you understand what
    is going on quickly.
    
    Banned tactics: the following tactics do too much work for this 
    assignment, so don't use them if you want credit for the problem:
      firstorder, intuition, admit

    You may use auto, tauto, congruence, etc.

    You can use previous problems to prove later ones by using the
    "apply" or "rewrite" tactics.  You can even do this if you do not how 
    to solve the previous problem (e.g., if it is still admit) and you will get 
    credit for the later problem if that proof is correct.

    DON'T FORGET TO PUT YOUR NAME AND MATRIC NUMBER
    AT THE TOP OF THE FILE.
    
*)

(* The following lines are similar to "#include" in C; just keep them here *)
Require Import Classical.
Require Import BinInt.
Require Import Peano_dec.
Require Import ZArith.
Axiom dep_extensionality:
 forall (A: Type) (B: A -> Type) (f g : forall x: A, B x),  (forall x, f x = g x) -> f = g.
Implicit Arguments dep_extensionality.
Lemma extensionality:
 forall (A B: Type) (f g : A -> B),  (forall x, f x = g x) -> f = g.
Proof. intros; apply dep_extensionality; auto. Qed.
Implicit Arguments extensionality.
Tactic Notation "extensionality" := 
  (match goal with | |- ?f = ?g => apply (extensionality f g); intro end).
Tactic Notation "extensionality" ident(x) := 
  (match goal with | |- ?f = ?g => apply (extensionality f g); intro x end).
Require Import Omega.
Axiom prop_ext: ClassicalFacts.prop_extensionality.
Implicit Arguments prop_ext.
Tactic Notation "spec" hyp(H) :=
  match type of H with ?a -> _ => 
    let H1 := fresh in (assert (H1: a); [|generalize (H H1); clear H H1; intro H]) end.
Tactic Notation "spec" hyp(H) constr(a) :=
  (generalize (H a); clear H; intro H). 
Tactic Notation "spec" hyp(H) constr(a) constr(b) :=
  (generalize (H a b); clear H; intro H).
 Tactic Notation "spec" hyp(H) constr(a) constr(b) constr(c) :=
  (generalize (H a b c); clear H; intro H).
Tactic Notation "spec" hyp(H) constr(a) constr(b) constr(c) constr(d) :=
  (generalize (H a b c d); clear H; intro H).
Tactic Notation "spec" hyp(H) constr(a) constr(b) constr(c) constr(d) constr(e) :=
  (generalize (H a b c d e); clear H; intro H).
Tactic Notation "LEM" constr(P) :=
  (destruct (classic (P))).
Ltac detach H :=
  match goal with [ H : (?X -> ?Y) |- _ ] =>
    cut Y; [ clear H; intro H | apply H; clear H ]
  end.
(* end #include section *)

(* *********************************************************************** *)

Module Induction.

Inductive Tree : Type :=
 | Leaf : Tree
 | OneBranch : forall t : Tree, Tree
 | TwoBranch : forall t1 t2 : Tree, Tree.

Fixpoint countLeaf (t : Tree) : nat :=
 match t with
  | Leaf => 1
  | OneBranch t => countLeaf t
  | TwoBranch t1 t2 => countLeaf t1 + countLeaf t2
 end.

(* Find the "leftmost" leaf in the tree and replace it with another tree *)
Fixpoint insert_subtree (A B : Tree) : Tree :=
 match A with
  | Leaf => B
  | OneBranch t => OneBranch (insert_subtree t B)
  | TwoBranch t1 t2 => TwoBranch (insert_subtree t1 B) t2
 end.

(* Hint: you may use the "replace" tactic to substitute one expression 
    for another; for example, to replace the expression 
    "countLeaf t1 + countLeaf t2" with the expression 
    "countLeaf t2 + countLeaf t1", use:
replace (countLeaf t1 + countLeaf t2) with (countLeaf t2 + countLeaf t1).
    This will add a new goal, which is to prove the equality (which can
    usually be done with auto, omega, etc.)
*)
Lemma insert_removes_one_leaf: forall t1 t2 : Tree,
  countLeaf t1 + countLeaf t2 = S (countLeaf (insert_subtree t1 t2)).
Proof.
  admit.
Qed.

End Induction.

(* *********************************************************************** *)

Module FirstOrderLogic.

Parameter term : Type.

Lemma FOL_Thm: forall (P Q : term -> Prop) (R : term -> term -> Prop),
  (forall t, P t -> R t t \/ ~Q t) ->
    (forall t1 t2, R t1 t2 -> (P t1 /\ ~ Q t1) \/ (~P t2 /\ Q t2)) ->
      (exists t, P t) -> 
        exists t, ~ Q t.
Proof.
  admit.
Qed.

End FirstOrderLogic.

(* *********************************************************************** *)

Module ModalLogic.

Parameter world : Type.
Parameter R : world -> world -> Prop.
Definition pred : Type := world -> Prop.

Definition forces (w : world) (phi : pred) : Prop :=
  phi w.
Notation "w ||- phi" := (forces w phi) (at level 30).

Definition valid (phi : pred) : Prop :=
  forall w, w ||- phi.
Notation "|-- phi" := (valid phi) (at level 30).

Definition Top : pred :=
  fun w => True.

Definition Bot : pred :=
  fun w => False.

Definition And (P1 P2 : pred) : pred :=
  fun w => (w ||- P1) /\ (w ||- P2).
Notation "P && Q" := (And P Q).

Definition Or (P1 P2 : pred) : pred :=
  fun w => (w ||- P1) \/ (w ||- P2).
Notation "P || Q" := (Or P Q).

Definition Impl (P1 P2 : pred) : pred :=
  fun w => (w ||- P1) -> (w ||- P2).
Notation "P ---> Q" := (Impl P Q) (at level 20, right associativity).

Lemma EQ_pred : forall P Q,
(forall w, w ||- P <-> w ||- Q) -> P = Q.
Proof.
  intros.
  unfold pred.
  apply extensionality.
  intro.
  apply prop_ext.
  spec H x.
  tauto.
Qed.
Tactic Notation "EQ_pred" :=
  (intros; apply EQ_pred; intro w).

Definition Dbl_Impl (P1 P2 : pred) : pred :=
  (P1 ---> P2) && (P2 ---> P1).
Notation "P <--> Q" := (Dbl_Impl P Q) (at level 20).

Definition Not (P : pred) : pred :=
  P ---> Bot.

Lemma modal_LEM : forall P,
  |-- (P || Not P).
Proof.
  intros.
  intro.
  LEM (w ||- P).
  left.
  trivial.
  right.
  trivial.
Qed.
Tactic Notation "ML_LEM" constr(w) constr(P) :=
  (destruct (modal_LEM (P) (w))).

Lemma modal_NNPP: forall P,
  P = Not (Not P).
Proof.
  EQ_pred.
  ML_LEM w P.
  split; auto.
  repeat intro.
  contradiction H1.
  split; intro.
  contradiction H.
  contradiction H0.
Qed.

Definition Box (P : pred) : pred :=
  fun w => forall w', R w w' -> (w' ||- P).
Notation "[] P" := (Box P) (at level 15).

Definition Diamond (P : pred) : pred :=
  fun w => exists w', R w w' /\ (w' ||- P).
Notation "<> P" := (Diamond P) (at level 15).

(* Let's assume that R is symmetric *)
Hypothesis B : forall w1 w2, R w1 w2 -> R w2 w1.

Lemma B_rule : forall P,
|-- P ---> [] <> P.
Proof.
  admit.
Qed.

Lemma B_Modal_Fact: forall P1 P2,
|-- [] (P1 && [] P2) ---> [] [] (P2 && <> P1).
Proof.
  admit.
Qed.

End ModalLogic.

(* *********************************************************************** *)

Module HoareLogic.

Definition var : Type := nat.
Definition num : Type := Z.

Inductive nExpr : Type :=
  | Num: forall n : num, nExpr
  | Var: forall v : var, nExpr
  | nNeg: forall ne : nExpr, nExpr
  | Plus: forall ne1 ne2 : nExpr, nExpr
  | Minus: forall ne1 ne2 : nExpr, nExpr
  | Times: forall ne1 ne2 : nExpr, nExpr.

Definition ctx : Type := var -> num.

(* This piece of black magic makes the "*" be the type-level product 
    operator, as opposed to the multiplacation operator on nums. *)
Open Local Scope Z_scope.
(* Obviously, since it is black magic, don't remove it! :-) *)

Fixpoint neEval (g : ctx) (ne : nExpr) : num :=
  match ne with
   | Num n => n
   | Var x => g x
   | nNeg ne => 0 - (neEval g ne)
   | Plus ne1 ne2 => (neEval g ne1) + (neEval g ne2)
   | Minus ne1 ne2 => (neEval g ne1) - (neEval g ne2)
   | Times ne1 ne2 => (neEval g ne1) * (neEval g ne2)
  end.

Inductive bExpr : Type :=
  | T : bExpr
  | F : bExpr
  | bNeg : forall be : bExpr, bExpr
  | And : forall be1 be2 : bExpr, bExpr
  | Or : forall be1 be2 : bExpr, bExpr
  | LT : forall ne1 ne2 : nExpr, bExpr.

Fixpoint beEval (g : ctx) (be : bExpr) : Prop :=
  match be with
   | T => True
   | F => False
   | bNeg be => ~(beEval g be)
   | And be1 be2 => (beEval g be1) /\ (beEval g be2)
   | Or be1 be2 => (beEval g be1) \/ (beEval g be2)
   | LT ne1 ne2 => (neEval g ne1) < (neEval g ne2)
  end.

(* This restores the operators to the usual meanings *)
Close Local Scope Z_scope.
Open Local Scope type_scope.
(* Again, don't remove this or the script will break in strange ways. *)

Inductive Coms : Type :=
  | Assign : forall (x : var) (e: nExpr), Coms
  | Seq : forall c1 c2 : Coms, Coms
  | If : forall (b : bExpr) (c1 c2 : Coms), Coms
  | While : forall (b : bExpr) (c : Coms), Coms.

Inductive ctl : Type :=
  | kStop : ctl
  | kSeq : forall (c : Coms) (k : ctl), ctl.

Definition state : Type := ctx * ctl.

Definition upd_ctx (g : ctx) (x : var) (n : num) : ctx :=
  fun x' => if eq_nat_dec x x' then n else g x'.

Inductive step : state -> state -> Prop :=
  | stepA: forall g x e n k g',
      n = neEval g e ->
      g' = upd_ctx g x n ->
      step (g, kSeq (Assign x e) k) (g', k)
  | stepS: forall g c1 c2 k,
      step (g, kSeq (Seq c1 c2) k) (g, kSeq c1 (kSeq c2 k))
  | stepI1: forall g b c1 c2 k,
      beEval g b ->
      step (g, kSeq (If b c1 c2) k) (g, kSeq c1 k)
  | stepI2: forall g b c1 c2 k,
      ~beEval g b ->
      step (g, kSeq (If b c1 c2) k) (g, kSeq c2 k)
  | stepW1: forall g b c k,
      beEval g b ->
      step (g, kSeq (While b c) k) (g, kSeq c (kSeq (While b c) k))
  | stepW2: forall g b c k,
      ~beEval g b ->
      step (g, kSeq (While b c) k) (g, k).

Inductive stepstar : state -> state -> Prop :=
  | stepsZ: forall s, 
    stepstar s s
  | stepsS: forall s s' s'',
    step s s' ->
    stepstar s' s'' ->
    stepstar s s''.

Definition assertion : Type := ctx -> Prop.

Definition assertAnd (P Q : assertion) : assertion :=
  fun g => P g /\ Q g.
Notation "P && Q" := (assertAnd P Q).

Definition Implies (P Q: assertion) : Prop :=
  forall g, P g -> Q g.
Notation "P |-- Q" := (Implies P Q) (at level 30).

Definition assertbEval (b : bExpr) : assertion :=
  fun g => beEval g b.
Notation "[ b ]" := (assertbEval b).

Definition assertReplace (x : var) (e : nExpr) (psi : assertion) : assertion :=
  fun g => psi (upd_ctx g x (neEval g e)).
Notation "[ x => e @ psi ]" := (assertReplace x e psi).

Definition HTuple (pre : assertion) (c : Coms) (post : assertion) : Prop :=
  forall g, 
    pre g ->
      forall g', 
        stepstar (g, kSeq c kStop) (g', kStop) ->
          post g'.

Lemma HT_Conj : forall pre1 pre2 c post1 post2,
  HTuple pre1 c post1 ->
  HTuple pre2 c post2 ->
  HTuple (pre1 && pre2) c (post1 && post2).
Proof.
  admit.
Qed.

End HoareLogic.