Require Import Coq.Logic.Classical_Prop.
Require Import Coq.Strings.String.
Require Import Coq.ZArith.ZArith.
Require Import Coq.micromega.Psatz.
Require Import Coq.Classes.Morphisms.
Require Import Coq.Sorting.Permutation.
Require Import Coq.Lists.List. Import ListNotations.
Require Import SetsClass.SetsClass. Import SetsNotation.
Require Import PV.Monad.
Require Import PV.Kleene.
Require Import PV.FixedPoint.
Require Import PV.MonadHoare.
Local Open Scope Z.
Local Open Scope list.

Import Monad
       MonadNotation
       SetMonadExamples0
       SetMonadExamples2
       SetMonadExamples3
       SetMonadHoare
       KleeneFix Sets_CPO.
Local Open Scope monad.

(************)
(** 习题：  *)
(************)

(** 请证明下面程序的性质。*)

Definition body_count (n: Z) (x: Z): SetMonad.M (ContinueOrBreak Z Z) :=
  choice
    (assume (x < n);; continue (x + 1))
    (assume (~ (x < n));; break x).

Definition count (n: Z): SetMonad.M Z :=
  repeat_break (body_count n) 0.

Theorem functional_correctness_count:
  forall n,
    0 < n ->
    Hoare (count n) (fun x => x = n).
Admitted. (* 请删除这一行_[Admitted]_并填入你的证明，以_[Qed]_结束。 *)


(************)
(** 习题：  *)
(************)

(** 请证明下面程序的性质。*)

Definition body_slow_div (n m: Z):
  Z * Z -> SetMonad.M (ContinueOrBreak (Z * Z) (Z * Z)) :=
  fun '(x, y) =>
    choice
      (assume (x < n);; break (x, y))
      (assume (~ (x < n));; continue (x - n, y + 1)).

Definition slow_div (n m: Z): SetMonad.M (Z * Z) :=
  repeat_break (body_slow_div n m) (m, 0).

Theorem functional_correctness_slow_div:
  forall n m,
    0 < n ->
    0 <= m ->
    Hoare (slow_div n m)
          (fun '(x, y) => x + n * y = m /\ 0 <= x < n).
Admitted. (* 请删除这一行_[Admitted]_并填入你的证明，以_[Qed]_结束。 *)


(************)
(** 习题：  *)
(************)

Definition insertion_body (x: Z):
  list Z * list Z -> SetMonad.M (ContinueOrBreak (list Z * list Z) (list Z)) :=
  fun '(l1, l2) =>
    match l2 with
    | nil => break (l1 ++ [x])
    | cons y l2' =>
        choice
          (assume (x <= y);; break (l1 ++ [x] ++ l2))
          (assume (y <= x);; continue (l1 ++ [y], l2'))
    end.

Definition insertion (x: Z) (l: list Z): SetMonad.M (list Z) :=
  repeat_break (insertion_body x) (nil, l).

Theorem insertion_perm:
  forall x l,
    Hoare
      (insertion x l)
      (fun l0 => Permutation (l ++ [x]) l0).
Admitted. (* 请删除这一行_[Admitted]_并填入你的证明，以_[Qed]_结束。 *)

Theorem insertion_incr:
  forall x l,
    incr l ->
    Hoare
      (insertion x l)
      (fun l0 => incr l0).
Admitted. (* 请删除这一行_[Admitted]_并填入你的证明，以_[Qed]_结束。 *)

(************)
(** 习题：  *)
(************)

Definition ins_sort (l: list Z) :=
  list_iter insertion l nil.

Theorem ins_sort_perm:
  forall L,
    Hoare
      (ins_sort L)
      (fun l => Permutation L l).
Admitted. (* 请删除这一行_[Admitted]_并填入你的证明，以_[Qed]_结束。 *)

Theorem ins_sort_incr:
  forall L,
    Hoare
      (ins_sort L)
      (fun l => incr l).
Admitted. (* 请删除这一行_[Admitted]_并填入你的证明，以_[Qed]_结束。 *)

Theorem functional_correctness_ins_sort:
  forall L,
    Hoare
      (ins_sort L)
      (fun l => Permutation L l /\ incr l).
Proof.
  intros.
  apply Hoare_conjunct.
  + apply ins_sort_perm.
  + apply ins_sort_incr.
Qed.