(** * Algebra of Programming, in Coq
 
   Author: Matthieu Sozeau [<sozeau@lri.fr>]
   Created: 18th July 2008.

   This development is a port of the examples from the paper
   "Algebra of Programming Using Dependent Types" 
   by Shin-Cheng Mu, Hsiang-Shang Ko and Patrick Jansson.
   The original examples can be found on the author's webpage:
   [http://www.iis.sinica.edu.tw/~scm/2008/aopa/].

   It is mostly defining an algebra on input-output relations
   and using these to algebraically specify a program. 
   Program derivation is then done by applying refinement rules until 
   a function can be extracted. The main example is an insertion
   sort derivation.
   
   The particularity of this version is that it uses typeclasses and 
   setoid-rewriting, to do transitivity reasonning when using 
   the refinement relation for example. The other differences lie in 
   the treatment of propositions using Prop and some minor syntactic
   annoyances with tuples (no direct λ-binding).
*)

Require Import List.
Require Import Setoid.
Require Import Program.

Open Scope equiv_scope.

Lemma fold_fusion {α β δ} (h : β -> δ) (f : α -> β -> β) {g : α -> δ -> δ} {z : β} 
  (push : Π a, h ∘ f a === g a ∘ h) :
  h ∘ fold_right f z === fold_right g (h z).
Proof.
  intros.
  intros x ; induction x.

    reflexivity.

    simpl.
    unfold compose at 1. simpl.
    setoid_rewrite (push a (fold_right f z x)).
    unfold compose in *. rewrite IHx. reflexivity.
Qed.

Definition rel (α β : Type) : Type := predicate [α ; β].

Notation " α <- β " := (rel β α) (at level 60).

Definition rel_compose {α β δ} (R : δ <- β) (S : β <- α) : δ <- α :=
  fun a c => exists b, S a b /\ R b c.

Infix "∙" := rel_compose (at level 40, left associativity).

Definition function {α β} (R : β <- α) := 
  Π a b b', R a b /\ R a b' -> b = b'.

Definition ℘ (α : Type) := predicate [α].

Definition power_transpose {α β} (R : β <- α) : α -> ℘ β := R.

Notation " 'Λ' R " := (power_transpose R) (at level 0).

Definition fn {α β} (f : α -> β) : β <- α :=
  λ a b, f a = b.

Definition idR {α} : α <- α := fn id.

Definition subR {α β : Type} : relation (β <- α) := predicate_implication.

Infix "≤" := subR (at level 70).

Notation " x ≥ y " := (subR y x) (at level 70, only parsing).

Instance subR_preorder : PreOrder (β <- α) subR.
Proof. intros. apply @predicate_implication_preorder. Qed.

Definition sub℘ {α : Type} : relation (℘ α) := predicate_implication.

Infix "⊆" := sub℘ (at level 70).
Notation " x ⊇ y " := (sub℘ y x) (at level 70, only parsing).

Instance subP_preorder : PreOrder (℘ α) sub℘.
Proof. intros. apply @predicate_implication_preorder. Qed.

Notation " R ⁻¹ " := (flip R) (at level 20).

Definition membership {α} : α <- ℘ α := λ pa a, pa a.

Notation " x ∈ y " := (membership y x) (at level 50).

Definition rel_product {α β δ D} (R : β <- α) (S : D <- δ) : (β * D) <- (α * δ) :=
  λ ac bd,
    let (a, c) := ac in
    let (b, d) := bd in
      R a b /\ S c d.

Infix "×" := rel_product (at level 50).

Instance rel_compose_morphism : Morphism (subR ==> subR ==> subR) (@rel_compose α β δ).
Proof.
  intros α β δ R₀ R₁ HR S₀ S₁ HS x z [y Hy].
  exists y. firstorder.
Qed.

Lemma id_intro {α β} {R : β <- α} : R ≥ R ∙ idR.
Proof. intros. intros x z [y [idr Hyz]].
  compute in idr. subst. assumption.
Qed.

Implicit Arguments fold_right [[A] [B]].

Definition foldr {α β} (f : β * α -> α) x : list β -> α := fold_right (prod_uncurry f) x.

Definition foldR {α β} (R : β <- (α * β)) (s : ℘ β) : β <- list α :=
  foldr (R ∙ (idR × membership)) s.

Definition Rmap {α β} (R : β <- α) (s : ℘ α) : ℘ β :=
  λ b, exists a, s a /\ R a b.

Lemma foldR_fusion {α β δ} (R : δ <- β) {S : β <- α * β} {T : δ <- α * δ} {u : ℘ β} {v : ℘ δ} :
  R ∙ S ≥ T ∙ (idR × R) -> Rmap R u ⊇ v -> R ∙ foldR S u ≥ foldR T v.
Proof.
  intros. intros x.
  induction x ; intros d.
  
    simpl. intros vd.
    destruct (H0 _ vd).
    exists x ; firstorder.

    simpl. intros [[a' d'] [Hfold H']].
    unfold rel_compose in IHx |- *. simpl.
    unfold rel_compose, prod_uncurry. 
    simpl in Hfold. destruct Hfold. compute in H1 ; subst a'.
    unfold impl in *.
    destruct (IHx _ H2) as [b [Hxb Rbd]].

    compute in H.
    destruct (H (a, b) d).
    exists (a, d'). firstorder.

    exists x0. split.
    exists (a, b). split. split. compute ; reflexivity. apply Hxb.
    firstorder.
    firstorder.
Qed.

Definition singleton {α} (a : α) : ℘ α :=
  λ x, x = a.

Definition nilR {α} : ℘ (list α) := singleton [].

Definition consR {α} := fn (prod_curry (@cons α)).

Lemma idR_foldR {α} : (@idR (list α)) ≥ foldR consR nilR.
Proof. intros α x. induction x. 
  compute ; auto.

  intros.
  red. intros. simpl in H.
  destruct H as [[a' b] Hb]. simpl in *. intuition.
  unfold idR, fn, id in *. subst a. 
  rewrite (IHx b H2). assumption.
Qed.

Definition pole [ PartialOrder A eqA leA ] := leA.

Infix "<=" := pole.
Notation " y >= x " := (pole x y) (only parsing).

Class [ po : PartialOrder A ] => DecidableTotalOrder :=
  partial_order_total_dec : forall x y : A, { x <= y } + { x >= y }.

Infix "<=?" := partial_order_total_dec (at level 50).

Definition coreflexive {α} (p : ℘ α) : α <- α :=
  λ a b, a = b /\ p a.

Notation " x ? " := (coreflexive x) (at level 0).

Notation "x → y" := (x -> y) (at level 90, right associativity): type_scope.

Class (( equivα : Equivalence α eqα )) => Bag (τ : Type) :=
  bag_equiv : relation τ ;
  bag_equivalence :> Equivalence τ bag_equiv ;

  empty_bag : τ ; cons_bag : α → τ → τ ;
  
  cons_bag_morphism :> Morphism (eqα ==> bag_equiv ==> bag_equiv) cons_bag ;

  bag_discr : Π a b, ~ empty_bag === cons_bag a b ;
  cons_bag_comm : Π a b w, cons_bag a (cons_bag b w) === cons_bag b (cons_bag a w).

Definition fn_abs {α} [ Equivalence β ] (f : α -> β) : β <- α :=
  λ a b, f a === b.

Section InsertionSort.
  Context [ dpo : DecidableTotalOrder α eqα (equ:=equivα) leα ].

  Definition lbound : ℘ (α * list α) :=
    λ p, 
      let (a, l) := p in
      let fix aux l := 
        match l with
          | [] => True
          | b :: xs => a <= b /\ aux xs
        end
      in aux l.

  Definition ordered : list α <- list α :=
    foldR (consR ∙ lbound ?) nilR.

  Context [ bag_impl : ! Bag equivα bag ].
  
  Definition bagify : list α -> bag :=
    fold_right cons_bag empty_bag.

  Definition permute : list α <- list α :=
    (fn_abs bagify)⁻¹ ∙ fn_abs bagify.

  Instance permute_refl : Reflexive permute.
  Proof. simpl_relation. 
    induction x ; simpl.
    exists empty_bag. 
    unfold fn_abs, flip, bagify; simpl. firstorder reflexivity.
    
    destruct IHx as [b [xb bx]].
    exists (cons_bag a b).
    unfold fn_abs, bagify in *; simpl. 
    unfold flip in *. simpl.
    rewrite bx. split ; reflexivity.
  Qed.

  Instance permute_sym : Symmetric permute.
  Proof. simpl_relation. firstorder. Qed.

  Instance permute_trans : Transitive permute.
  Proof. simpl_relation. firstorder. 
    unfold fn_abs, flip in *.
    rewrite <- H1 in H.
    rewrite <- H2 in H0.
    rewrite H0 in H.
    exists (bagify z). split ; auto. reflexivity.
  Qed.
    
  Definition sort : list α <- list α :=
    ordered ∙ permute.

  Fixpoint combine_curried (a : α) (xs : list α) : ℘ (list α) :=
    let fix combine' (a : α) (xs : list α) : ℘ (list α) :=
      match xs with
        | [] => λ ys, False
        | b :: xs => Rmap (λ zs, consR (b, zs)) (combine_curried a xs)
      end
    in
      predicate_union [list α] (consR (a, xs)) (combine' a xs).

  Definition combine : list α <- α * list α := 
    λ p, let (a, xs) := p in combine_curried a xs.

  Ltac simpl_R :=
    match goal with
      | [ H : idR ?x ?y |- _ ] => compute in H ; subst x ; simpl in *
      | [ H : consR ?x ?y |- _ ] => compute in H ; subst y ; simpl in *
      | [ H : nilR ?x |- _ ] => compute in H ; subst x ; simpl in *
    end.

  Lemma combine_permute : Π x xs l, combine_curried x xs l -> permute (x :: xs) l. 
  Proof.
    induction xs ; simpl ; intros.
    destruct H. simpl_R. reflexivity.
    inversion H.
    
    destruct H.
    simpl_R. reflexivity.
    
    destruct H as [l' [Hcomb Hcons]].
    simpl_R.
    destruct (IHxs _ Hcomb) as [bl' Hbl'].
    exists (cons_bag a bl').
    destruct Hbl' as [H0 H1].
    unfold fn_abs, flip in H0, H1 |- *. subst.
    split. simpl. 
    rewrite cons_bag_comm at 1.
    rewrite H0. reflexivity.
    simpl. rewrite H1. reflexivity.
  Qed.

  Lemma permute_cons : Π a xs ys, permute xs ys -> permute (a :: xs) (a :: ys).
  Proof.
    intros.
    destruct H as [bxs Hbxs].
    exists (cons_bag a bxs).
    destruct Hbxs.
    unfold fn_abs, flip in *.
    simpl.
    rewrite H, H0. split ; reflexivity.
  Qed.

  Lemma perm_step : permute ∙ consR ≥ combine ∙ (idR × permute).
  Proof.
    intros a al. revert a. unfold impl. induction al ; simpl. 

    intros a. firstorder. destruct x as (x, xs).
    destruct a as (y, ys).
    simpl in *. induction xs.
    destruct H. simpl_R.
    destruct H0; inversion H. 

    destruct H. simpl_R.
    destruct H0. inversion H. inversion H. 
    destruct H0. inversion H2.

    destruct a0 as [y ys].
    intros [[x xs] Hxs]. simpl in *.
    intuition. simpl_R.

    exists (x :: ys). split; [firstorder|..].

    transitivity (x :: xs) ; auto using combine_permute, permute_cons.
  Qed.

  Lemma perm_base : Rmap permute nilR ⊇ nilR.
  Proof. intros l Hl. exists []. firstorder. simpl_R.
    exists empty_bag. unfold fn_abs, flip. firstorder reflexivity.
  Qed.

  Tactic Notation "rew" ident(i) "at" int_or_var(n) :=
    setoid_rewrite <- @i at n.

  Definition perm_der : { perm : list α <- list α | permute ≥ perm }.
  Proof.
    econstructor. rew id_intro at 2. rew idR_foldR at 2.
    apply (foldR_fusion permute perm_step perm_base).
  Defined.

  Definition perm := proj1_sig perm_der.
  Definition permute_is_fold : perm ≤ permute := proj2_sig perm_der.

  Fixpoint insert (a : α) (l : list α) : list α :=
    match l with
      | [] => [a]
      | b :: xs => if a <=? b then a :: l else b :: insert a xs
    end.
  
  Lemma ins_base : Rmap ordered nilR ⊇ nilR.
  Proof. intros l Hl. simpl_R. exists []. firstorder. Qed.

  Lemma ordered_eq : Π l l', ordered l l' -> l = l'.
  Proof.
    induction l ; simpl ; intros ; try simpl_R.
    reflexivity.

    red in H. destruct H as [[a' al] H]. intuition.
    red in H0, H1 ; destruct_conjs. repeat simpl_R.
    inversion H2. program_simpl. f_equal.
    apply IHl. assumption.
  Qed.

  Lemma lbound_mon : Π a b, a <= b -> Π l, lbound (b, l) -> lbound (a, l).
  Proof.
    induction l ; simpl ; intros ; auto.
    intuition firstorder. transitivity b ; auto.
  Qed.

  Lemma lbound_insert : Π a b, a <= b -> Π l, lbound (a, l) -> lbound (a, insert b l).
  Proof.
    induction l ; simpl ; intros ; auto.
    intuition firstorder. 
    destruct (b <=? a0); intuition.
  Qed.
  
  Lemma ins_step : ordered ∙ combine ≥ fn (prod_curry insert) ∙ (idR × ordered).
  Proof. 
    intros (a,l). unfold impl. induction l ; intros l' ; simpl.

    unfold fn, rel_compose. intros [[a' l''] Hb].
    simpl in *. intuition ; repeat simpl_R. subst. exists [a']. firstorder.
    compute. exists (a',[]) ; firstorder.
    exists (a', []). firstorder.
    
    unfold rel_compose. 
    intros [[a' l''] [ordl'' insertl'']].
    unfold fn in *. simpl in *. intuition simpl_R. subst.
    destruct H0 as [[b l'''] Hb]. intuition. simpl in *.
    destruct H0 as [[b' lb'] Hb']. 
    simpl in * ; intuition. repeat simpl_R.
    red in H ; program_simpl.
    destruct (a' <=? b').
      exists (a' :: b' :: lb').
      split. compute.
      left. do 2 f_equal. red in H1.
      apply (ordered_eq _ _ H1).

      assert (Heq:=ordered_eq _ _ H1). subst.
      exists (a', b' :: lb'). split ; firstorder.
      exists (b', lb'). split ; firstorder.
      exists (b', lb') ; firstorder.
      exists (a', b' :: lb') ; firstorder.
      fold (lbound (a', lb')). apply lbound_mon with b' ; auto.

      exists (b' :: insert a' lb').
      pose (IHl (insert a' lb')).
      unfold rel_compose in r.
      destruct r. exists (a', lb'). split ; firstorder.
      assert (Heq:=ordered_eq _ _ H1) ; subst.

      destruct H.
      assert (Heq:=ordered_eq _ _ H2) ; subst.

      split.
      right. exists (insert a' lb'). split ; firstorder.
      exists (b', insert a' lb'). split ; firstorder.

      exists (b', insert a' lb'). split ; firstorder.
      apply lbound_insert ; auto.
  Qed.

  Lemma foldR_to_fold_right {A B} (f : A -> B -> B) (e : B) :
    foldR (fn (prod_curry f)) (singleton e) ≥ fn (fold_right f e).
  Proof.
    intros. intros l. unfold impl. induction l; simpl; auto.
    intros. red in H. simpl in H. subst. red. reflexivity.
    intros. red in H ; simpl in H. unfold prod_uncurry, prod_curry, rel_compose.
    exists (a, fold_right f e l). subst. firstorder.
    apply IHl. firstorder.
  Qed.

  Definition sort_der : { sort : list α -> list α | ordered ∙ permute ≥ fn sort }.
  Proof.
    econstructor.
    rew permute_is_fold at 1.
    assert(foldR combine nilR ≤ perm) by reflexivity.
    rew H at 1.
    setoid_rewrite <- (foldR_fusion ordered ins_step ins_base).
    unfold nilR.
    rew foldR_to_fold_right at 1.
    reflexivity.
  Defined.

End InsertionSort.

Extraction sort_der.