msort.thy

theory
  msort
imports
  Main
  Classes.Classes
begin

datatype 'a msort = Seg "'a × 'a" | Empty | Fail

instantiation msort :: (ord) monoid
begin

definition neutral_msort: "neutral_msort ≡ Empty"

fun mult_msort where
  "mult_msort _ Fail = Fail" |
  "mult_msort Fail _ = Fail" |
  "mult_msort a Empty = a" |
  "mult_msort Empty a = a" |
  "mult_msort (Seg (a, b)) (Seg (c, d)) =
     (if b ≤ c then Seg (a, d) else Fail)"

instance proof
  fix a b c :: "'a msort"
  show "(a ⊗ b) ⊗ c = a ⊗ (b ⊗ c)"
    by (case_tac a; case_tac b; case_tac c; auto)
  show "𝟭 ⊗ a = a"
    unfolding neutral_msort by (case_tac a; auto)
  show "a ⊗ 𝟭 = a"
    unfolding neutral_msort by (case_tac a; auto)
qed

end

fun sorted :: "('a::preorder) list ⇒ bool" where
  "sorted (a # b # l) = (a ≤ b ∧ sorted (b # l))" |
  "sorted _ = True"

definition msort_fold :: "('a::ord) list ⇒ 'a msort" where
  "msort_fold l ≡ foldr (⊗) (map (λa. Seg (a, a)) l) 𝟭"

lemma sorted_imp_seg:
  fixes a :: "'a::preorder" and l :: "'a list"
  shows "sorted (a # l) ⟹ ∃b. msort_fold (a # l) = Seg (a, b)"
proof (induction "a # l" arbitrary: a l rule: sorted.induct)
  case (1 a b l)
  thus ?case unfolding msort_fold_def by auto
next
  case "2_1"
next
  case ("2_2" a)
  show ?case unfolding msort_fold_def using neutr by auto
qed

lemma fold_empty_nil:
  fixes l :: "('a::preorder) list"
  shows "msort_fold l = Empty ⟹ l = []"
proof (induction l rule: sorted.induct)
  case (1 a b l)
  show ?case
  proof (cases "msort_fold (b # l)")
    case (Seg s)
    thus ?thesis
      using "1.prems"
      unfolding msort_fold_def
      by (case_tac s; simp split: if_split_asm)
  next
    case Empty
    thus ?thesis using "1.IH" by blast
  next
    case Fail
    thus ?thesis using "1.prems" unfolding msort_fold_def by auto
  qed
next
  case "2_1" show ?case by blast
next
  case ("2_2" a)
  thus ?case
    using neutr [of "Seg (a, a)"]
    unfolding msort_fold_def by auto
qed

lemma seg_imp_sorted:
  fixes a b c :: "'a::preorder" and l :: "'a list"
  shows "msort_fold (a # l) = Seg (b, c) ⟹
    sorted (a # l)"
proof (induction "a # l" arbitrary: a b c l rule: sorted.induct)
  case (1 a b l c d)
  let ?m = "msort_fold (b # l)"
  have A: "?m ≠ Empty" using fold_empty_nil by blast
  have B: "?m ≠ Fail"
    using "1.prems"
    unfolding msort_fold_def
    by auto
  from A B have C: "sorted (b # l)"
    using "1.hyps"
    by (case_tac ?m; auto)
  have "¬ a ≤ b ⟹ Seg (a, a) ⊗ Seg (b, b) = Fail"
    by auto
  hence "⋀m. ¬ a ≤ b ⟹ Seg (a, a) ⊗ (Seg (b, b) ⊗ m) = Fail"
    using assoc [of "Seg (a, a)" "Seg (b, b)"]
    by (case_tac m; auto)
  thus ?case
    using "1.prems" C
    unfolding msort_fold_def
    by (case_tac "a ≤ b"; auto)
next
  case "2_1"
next
  case ("2_2" a) thus ?case by auto
qed

theorem sorted_not_fail_iff:
  fixes l :: "('a::preorder) list"
  shows "sorted l = (msort_fold l ≠ Fail)"
proof (cases l)
  case Nil
  thus ?thesis
    unfolding neutral_msort msort_fold_def
    by auto
next
  case (Cons a l)
  thus ?thesis
    using sorted_imp_seg [of a l] seg_imp_sorted [of a l]
    using fold_empty_nil [of "a # l"]
    by (case_tac "msort_fold (a # l)"; auto)
qed

end

msort.v

Require Import OrderedType.
Require Import Recdef.

Module Sorted (A : OrderedType).
  Import A.

  Function sorted (l : list t) {measure length l} : Prop :=
    match l with
    | a :: b :: l' => (lt a b \/ eq a b) /\ sorted (b :: l')
    | _ => True
    end.
  Proof. eauto. Qed.

End Sorted.

Class MonoidDot (A : Type) := monoid_dot : A -> A -> A.
Class MonoidOne (A : Type) := monoid_one : A.

Declare Scope M_scope.
Infix "*" := monoid_dot: M_scope.
Notation "1" := monoid_one: M_scope.
Open Scope M_scope.

Class Semigroup {A : Type} (dot : MonoidDot A) : Prop :=
  { dot_assoc : forall a b c : A, a * (b * c) = (a * b) * c }.

Class Monoid `(M : Semigroup) (one : MonoidOne A) : Prop :=
  { one_left : forall a : A, 1 * a = a;
    one_right : forall a : A, a * 1 = a }.

Inductive msort {A : Type} : Type :=
| seg : A * A -> msort
| empty : msort
| fail : msort.

Module MSort (A : OrderedType).
  Import A.
  Module M := OrderedTypeFacts A.

  Instance MSortDot : MonoidDot msort :=
    fun x y =>
      match x, y with
      | _, fail => fail
      | fail, _ => fail
      | _, empty => x
      | empty, _ => y
      | seg (a, b), seg (c, d) =>
        match compare b c with GT _ => fail | _ => seg (a, d) end
      end.

  Instance MSortOne : MonoidOne (@msort t) := empty.

  Ltac msort_assoc_auto :=
    unfold monoid_dot, MSortDot;
    repeat match goal with
           | |- context [ let (_, _) := ?p in _ ] => destruct p
           end;
    repeat match goal with
           | |- context [ match (compare ?a ?b) with _ => _ end ] =>
             let H := fresh in
             let H0 := fresh in
             case_eq (compare a b); intros H H0; clear H0
           end;
    auto;
    match goal with
    | H : lt ?a ?b, H0 : lt ?b ?a |- _ => contradict (M.lt_le H H0)
    | H : eq ?a ?b, H0 : lt ?b ?a |- _ => contradict (M.eq_not_gt H H0)
    end.

  Instance MSortSemigroup : Semigroup MSortDot.
  Proof.
    split. intros a b c.
    induction a; induction b; induction c; msort_assoc_auto.
  Qed.

  Instance MSortMonoid : Monoid MSortSemigroup MSortOne.
  Proof.
    split; intro a; unfold monoid_dot, monoid_one, MSortDot, MSortOne;
      destruct a as [p| | ]; try destruct p; reflexivity.
  Qed.

  Definition msort_fold (l : list t) : msort :=
    fold_right (fun a r => seg (a, a) * r) 1 l.

  Module S := Sorted A. Import S.

  Lemma sorted_imp_seg : forall (a : t) (l : list t),
      sorted (a :: l) -> (exists b : t, msort_fold (a :: l) = seg (a, b)).
  Proof.
    intros a l. remember (a :: l) as l'. revert a l Heql'.
    functional induction (sorted l'); intros.
    - destruct H. assert (b :: l' = b :: l'). 1:reflexivity.
      specialize (IHP b l' H1 H0). inversion Heql'. rewrite <- H3.
      clear a0 H0 H1 H3 Heql'. destruct IHP as [c]. exists c.
      unfold msort_fold in *. simpl in *. rewrite H0.
      unfold monoid_dot, MSortDot. destruct H.
      + pose proof (M.elim_compare_lt H). destruct H1. rewrite H1. reflexivity.
      + pose proof (M.elim_compare_eq H). destruct H1. rewrite H1. reflexivity.
    - destruct l; try destruct l; try inversion y; inversion Heql'.
      unfold msort_fold. simpl. exists a. apply one_right.
  Qed.

  Lemma fold_empty_nil : forall (l : list t), msort_fold l = empty -> l = nil.
  Proof.
    intro l. destruct l; intros. 1:reflexivity.
    case_eq (msort_fold l); intros; unfold msort_fold in H, H0; simpl in H, H0;
      rewrite H0 in H; unfold monoid_dot, MSortDot in H.
    + destruct p. destruct (compare t0 t1); inversion H.
    + inversion H.
    + inversion H.
  Qed.

  Lemma seg_imp_sorted : forall (a : t) (l : list t),
      (exists b c : t, msort_fold (a :: l) = seg (b, c)) -> sorted (a :: l).
  Proof.
    intros a l. remember (a :: l) as l'. revert a l Heql'.
    functional induction (sorted l'); intros.
    - assert (b :: l' = b :: l'). 1:reflexivity. specialize (IHP b l' H0).
      clear a0 l H0 Heql'. destruct H as [c H]. destruct H as [d H].
      assert (exists c d : t, msort_fold (b :: l') = seg (c, d)).
      + case_eq (msort_fold (b :: l')); intros.
        * destruct p. exists t0, t1. reflexivity.
        * apply fold_empty_nil in H0. inversion H0.
        * unfold msort_fold in H, H0. simpl in H, H0. rewrite H0 in H.
          unfold monoid_dot, MSortDot in H. inversion H.
      + specialize (IHP H0). clear H0. split. 2:assumption.
        unfold msort_fold in H. simpl in H. rewrite dot_assoc in H.
        assert (seg (a, a) * seg (b, b) = seg (a, b)).
        * case_eq (seg (a, a) * seg (b, b)); intros; rewrite H0 in H;
            unfold monoid_dot, MSortDot in H0; destruct (compare a b);
              inversion H0; try reflexivity.
          remember (msort_fold l') as m. unfold msort_fold in Heqm.
          rewrite <- Heqm in H. unfold monoid_dot, MSortDot in H.
          destruct m; inversion H.
        * clear l' c d H IHP. unfold monoid_dot, MSortDot in H0.
          case_eq (compare a b); intros; rewrite H in H0; inversion H0;
            [left | right]; assumption.
    - destruct l; try inversion Heql'. trivial.
  Qed.

  Theorem sorted_not_fail_iff :
    forall l : list t, sorted l <-> (msort_fold l <> fail).
  Proof.
    intro l. destruct l as [|a l].
    - remember nil as l. functional induction (sorted l). 1:inversion Heql.
      unfold msort_fold, monoid_one, MSortOne, not. simpl.
      split; intros; [inversion H0 | trivial].
    - split; unfold not; intros.
      + pose proof (sorted_imp_seg a l H). destruct H1. rewrite H1 in H0.
        inversion H0.
      + case_eq (msort_fold (a :: l)); intros.
        * destruct p. assert (exists b c : t, msort_fold (a :: l) = seg (b, c)).
          1:exists t0, t1; assumption. apply (seg_imp_sorted a l H1).
        * apply fold_empty_nil in H0. inversion H0.
        * specialize (H H0). inversion H.
  Qed.

End MSort.

msort_1.thy

theory
  msort_1
imports
  Main
  Classes.Classes
begin

datatype 'a msort = Seg "'a \<times> 'a" | Empty | Fail

instantiation msort :: (ord) monoid
begin

definition neutral_msort: "neutral_msort \<equiv> Empty"

fun mult_msort where
  "mult_msort _ Fail = Fail" |
  "mult_msort Fail _ = Fail" |
  "mult_msort a Empty = a" |
  "mult_msort Empty a = a" |
  "mult_msort (Seg (a, b)) (Seg (c, d)) =
     (if b \<le> c then Seg (a, d) else Fail)"

instance proof
  fix a b c :: "'a msort"
  show "(a \<otimes> b) \<otimes> c = a \<otimes> (b \<otimes> c)"
    by (case_tac a; case_tac b; case_tac c; auto)
  show "\<one> \<otimes> a = a"
    unfolding neutral_msort by (case_tac a; auto)
  show "a \<otimes> \<one> = a"
    unfolding neutral_msort by (case_tac a; auto)
qed

end

fun sorted :: "('a::preorder) list \<Rightarrow> bool" where
  "sorted (a # b # l) = (a \<le> b \<and> sorted (b # l))" |
  "sorted _ = True"

definition msort_fold :: "('a::ord) list \<Rightarrow> 'a msort" where
  "msort_fold l \<equiv> foldr (\<otimes>) (map (\<lambda>a. Seg (a, a)) l) \<one>"

lemma sorted_imp_seg:
  fixes a :: "'a::preorder" and l :: "'a list"
  shows "sorted (a # l) \<Longrightarrow> \<exists>b. msort_fold (a # l) = Seg (a, b)"
proof (induction "a # l" arbitrary: a l rule: sorted.induct)
  case (1 a b l)
  thus ?case unfolding msort_fold_def by auto
next
  case "2_1"
next
  case ("2_2" a)
  show ?case unfolding msort_fold_def using neutr by auto
qed

lemma fold_empty_nil:
  fixes l :: "('a::preorder) list"
  shows "msort_fold l = Empty \<Longrightarrow> l = []"
proof (induction l rule: sorted.induct)
  case (1 a b l)
  show ?case
  proof (cases "msort_fold (b # l)")
    case (Seg s)
    thus ?thesis
      using "1.prems"
      unfolding msort_fold_def
      by (case_tac s; simp split: if_split_asm)
  next
    case Empty
    thus ?thesis using "1.IH" by blast
  next
    case Fail
    thus ?thesis using "1.prems" unfolding msort_fold_def by auto
  qed
next
  case "2_1" show ?case by blast
next
  case ("2_2" a)
  thus ?case
    using neutr [of "Seg (a, a)"]
    unfolding msort_fold_def by auto
qed

lemma seg_imp_sorted:
  fixes a b c :: "'a::preorder" and l :: "'a list"
  shows "msort_fold (a # l) = Seg (b, c) \<Longrightarrow>
    sorted (a # l)"
proof (induction "a # l" arbitrary: a b c l rule: sorted.induct)
  case (1 a b l c d)
  let ?m = "msort_fold (b # l)"
  have A: "?m \<noteq> Empty" using fold_empty_nil by blast
  have B: "?m \<noteq> Fail"
    using "1.prems"
    unfolding msort_fold_def
    by auto
  from A B have C: "sorted (b # l)"
    using "1.hyps"
    by (case_tac ?m; auto)
  have "\<not> a \<le> b \<Longrightarrow> Seg (a, a) \<otimes> Seg (b, b) = Fail"
    by auto
  hence "\<And>m. \<not> a \<le> b \<Longrightarrow> Seg (a, a) \<otimes> (Seg (b, b) \<otimes> m) = Fail"
    using assoc [of "Seg (a, a)" "Seg (b, b)"]
    by (case_tac m; auto)
  thus ?case
    using "1.prems" C
    unfolding msort_fold_def
    by (case_tac "a \<le> b"; auto)
next
  case "2_1"
next
  case ("2_2" a) thus ?case by auto
qed

theorem sorted_not_fail_iff:
  fixes l :: "('a::preorder) list"
  shows "sorted l = (msort_fold l \<noteq> Fail)"
proof (cases l)
  case Nil
  thus ?thesis
    unfolding neutral_msort msort_fold_def
    by auto
next
  case (Cons a l)
  thus ?thesis
    using sorted_imp_seg [of a l] seg_imp_sorted [of a l]
    using fold_empty_nil [of "a # l"]
    by (case_tac "msort_fold (a # l)"; auto)
qed

end