(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* Certified Haskell Prelude.
 * Author: Matthieu Sozeau
 * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
 *              91405 Orsay, France *)

(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)

Require Export Coq.Program.Program.
Require Export Coq.Logic.FunctionalExtensionality.
Require Export Morphisms Setoid Classes.Equivalence.
Require Export Prelude.Laws.

Open Scope equiv_scope.
Open Scope program_scope.

Open Local Scope signature_scope.

Ltac feq f g :=
  match f with
    | ?f ?x =>
      match g with
        | f ?y => try setoid_replace x with y ; try reflexivity
        | ?g x => feq f g
        | ?g ?y => feq f g ; try setoid_replace x with y ; try reflexivity
        | _ => idtac
      end
    | _ => idtac
  end.

Ltac fequal :=
  match goal with
    [ |- ?R ?f ?g ] => feq f g ; try reflexivity
  end.

Require Import RelationClasses.

Obligation Tactic := try typeclasses eauto || program_simplify.

Instance respectful_eq_default α `{ PER β eqβ } :
  PER (pointwise_relation α eqβ)%signature | 2.
Proof. simpl_relation. constructor; simpl_relation.
  symmetry ; auto.
  transitivity (y a); firstorder.
Qed.

(* Instance respectful_per_default `{ PER α eqα, PER β eqβ ] : *)
(*   PER (α -> β) (eqα ==> eqβ)%signature | 1. *)
(* Proof. simpl_relation. Qed. *)

Structure Setoid := mkSetoid {
  car :> Type ;
  seq :> relation car ;
  equiv : Equivalence seq }.

Instance seq_equiv : Equivalence (seq A).
  apply equiv.
Defined.
  

Implicit Arguments seq [[s]].

Infix "==" := seq (at level 70).
Notation "(==)" := seq.

Definition eq_setoid α := mkSetoid α eq _.

Notation " 'substitute' H 'in' p " := (@eq_rect _ _ _ p _ H) (at level 10).

Definition sub_setoid (A B : Setoid) : Prop :=
  let 'mkSetoid car seq equiv := A in
  let 'mkSetoid car' seq' equiv' := B in
    { H : car' = car & subrelation seq (substitute H in seq') }.

Class SubSetoid (A B : Setoid) :=
  sub_setoid_subrelation : sub_setoid A B.

(* Definition Map (A B : Setoid) := *)
(*   { fn : A -> B | Morphism (seq ==> seq) fn }. *)

Record Map (A B : Setoid) := mkMap {
  Map_fn :> A -> B ;
  Map_Mor : Proper (seq ==> seq) Map_fn }.

Implicit Arguments Map_fn [[A] [B]].
Implicit Arguments mkMap [[A] [B]].

Infix "-->" := Map (at level 55, right associativity).

About mkMap.


(* Program Definition Map_fn {A B} (m : A --> B) : A -> B := m. *)

(* Coercion Map_fn : Map >-> Funclass. *)

Instance Map_respect {A B} (m : Map A B) : Proper (seq ==> seq) m.
Proof. intros A B [m Hm] ; exact Hm. Defined.

Definition respectfulS (α β : Setoid) : relation (Map α β) :=
  pointwise_relation α β.

Infix "===>" := respectfulS (at level 90).

Ltac pauto := simpl in * ; eauto with relations.

Instance Map_respectful_equiv α β : @Equivalence (Map α β) (α ===> β)%signature.
Proof with simpl in * ; pauto.
  constructor ; red ; unfold respectful ; simpl in *.
  intros [f morf] x...
  intros [f morf] [g morg] Hxy x...
  symmetry ; apply Hxy.
  intros [f morf] [g morg] [h morh]...
  intros Hfg Hgh x.
  transitivity (g x)...
Qed.
About mkMap.

Definition proper_map_equiv (A B : Setoid) (f : A -> B) : relation (Proper (A ==> B) f) :=
  fun p q => True.

Instance mkMap_morph {A B : Setoid} : Proper 
  (forall_relation (fun f : A -> B => proper_map_equiv A B f ==> (A ===> B))) (@mkMap A B).
Proof. intros. intro f. intros px py _. intro. simpl. reflexivity. Qed.

Definition respectfulT {A B : Type} (R : A -> A -> Type) (R' : B -> B -> Type) := 
  fun f g => forall x y, R x y -> R' (f x) (g y).
Definition relationT (A : Type) := A -> A -> Type.
Definition forall_relationT {A : Type} {B : A -> Type} (sig : Π a : A, relation (B a)) : relation (Π x : A, B x) :=
  λ f g, Π a : A, sig a (f a) (g a).

Definition dep_relation {A : Type} {B : A -> Type} (R : relationT A) 
  (R' : forall a a', R a a' -> B a -> B a' -> Prop) : relationT (Π x : A, B x) :=
  λ f g, Π (a a' : A) (Ha : R a a'), R' a a' Ha (f a) (g a').

(*
Instance mkMap_morph2 {A B : Setoid} : 
  (dep_relation (A ==> B) (fun a a' H f g => iff ==> (A ===> B))) (@mkMap A B) (@mkMap A B).
Proof. intros. intro f. intros px py _. intro. simpl. reflexivity. Qed.
*)

Notation "'mkMap' f" := (@mkMap _ _ f _) (at level 0).

Instance subrelation_respectfulS {A B : Setoid} : subrelation (A ===> B) (A ==> B).
Proof.
  intros A B f g Hfg x y Hxy.  rewrite Hxy. apply Hfg.
Qed.

Instance subrelation_respectfulS' {A B : Setoid} : @subrelation (A --> B) (A ==> B) (A ===> B).
Proof.
  intros A B f g Hfg x. apply Hfg. reflexivity.
Qed.
  
Instance Map_fn_morphism {A B} : Proper ((A ===> B) ==> A ==> B) Map_fn.
Proof. intros A B [m Hm] [m' Hm'] Hmm'. simpl. red. do 2 red in Hmm'. simpl in *. 
  intros. rewrite H. apply Hmm'. Qed.

Program Definition MapS (α β : Setoid) : Setoid :=
  mkSetoid _ (α ===> β) _.

Canonical Structure MapS.

Infix "--->" := MapS (at level 55, right associativity).

Program Definition mkMap2 {A B C : Setoid} (Map_fn : A -> B -> C) 
  (P : Proper (A ==> B ==> C) Map_fn) : A ---> B ---> C :=
  mkMap (fun a => mkMap (fun b => Map_fn a b)).

  Next Obligation. 
    intros b b' Hbb'. rewrite Hbb'. reflexivity.
  Qed.

  Next Obligation. 
    intros a a' Haa' b. simpl. rewrite Haa'. reflexivity.
  Qed.

Notation "'mkMap2' f" := (@mkMap2 _ _ _ f _) (at level 0).

Program Definition mkMap3 {A B C D : Setoid} (Map_fn : A -> B -> C -> D) 
  {P : Proper (A ==> B ==> C ==> D) Map_fn} : A ---> B ---> C ---> D :=
  mkMap (fun a => mkMap2 (fun b c => Map_fn a b c)).

  Next Obligation. 
    intros b b' Hbb' c c' Hcc'. rewrite Hbb', Hcc'. reflexivity.
  Qed.

  Next Obligation. 
    intros a a' Haa' b c. simpl. rewrite Haa'. reflexivity.
  Qed.

Notation "'mkMap3' f" := (@mkMap3 _ _ _ _ f _) (at level 0).

Program Definition MapS_fn α β (f : α ---> β) : α -> β := f.

Notation " ^ x " := (MapS_fn x) (at level 0).

Program Definition idS {A : Setoid} : A --> A := mkMap id.

Program Definition composeS {α β δ : Setoid} (f : β --> δ) (g : α --> β) : α --> δ := 
  mkMap (f ∘ g).

Open Scope equiv_scope.

Ltac simpl_respect := 
  let rec arrow :=
    let tac :=
      let x := fresh "x" in
      let y := fresh "y" in 
      let H := fresh "Hxy" in
        intros x y H ; arrow ; try (rewrite H)
     in
      match goal with
        | [ |- (?X ==> ?Y)%signature _ _ ] => tac
        | [ |- (?X ===> ?Y)%signature _ _ ] => 
          let x := fresh "x" in intros x ; arrow
        | [ |- _ ] => simpl ; repeat clear_subset_proofs
      end
    in 
    match goal with
      | [ |- Proper _ _ ] => red ; arrow
      | _ => arrow
    end.

Ltac simpl_morph := 
  let one_simple := simpl_respect ; fequal in
  let rec aux :=
    match goal with
      | [ |- (_ ==> _)%signature _ _ ] => one_simple ; aux
      | [ |- (_ ===> _)%signature _ _ ] => one_simple ; aux
      | [ |- Proper _ _ ] => one_simple ; aux
      | _ => idtac
    end
  in aux.

Instance composeS_mor : Proper ((β ===> δ) ==> (α ===> β) ==> (α ===> δ)) (@composeS α β δ).
Proof. intros. simpl_morph. Qed.

Program Definition composeM {α β δ : Setoid} : (β ---> δ) ---> (α ---> β) ---> (α ---> δ) :=
  mkMap2 composeS.

  Next Obligation. intros g g' Hgg'. intros f f' Hff'.
    rewrite Hff', Hgg'.
    reflexivity.
  Qed.

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

Lemma composeS_assoc {A B C D : Setoid} (f : A ---> B) (g : B ---> C) (h : C ---> D) 
  : h ∙ g ∙ f == h ∙ (g ∙ f).
Proof.
  intros A B C D [f Hf] [g Hg] [h Hh]. simpl.
  unfold composeS. simpl. intros a. reflexivity.
Qed.

Lemma composeS_unit_right {A B : Setoid} (f : A ---> B) : f ∙ idS == f.
Proof.
  intros A B [f Hf]. unfold composeS. simpl. 
  intros a. reflexivity.
Qed.


Lemma composeS_unit_left {A B : Setoid} (f : A ---> B) : idS ∙ f == f.
Proof.
  intros A B [f Hf]. unfold composeS. simpl. 
  intros a. reflexivity.
Qed.

Program Definition applyS {A B : Setoid} (x : A) : (A ---> B) --> B :=
  mkMap (fun f => f x).

  Next Obligation. intros f f' Hff'. 
    setoid_rewrite Hff'. reflexivity.
  Qed.

Program Definition applyM {A B : Setoid} : A ---> (A ---> B) ---> B :=
  mkMap (fun x => applyS x).

  Next Obligation. intros a a' Haa'.
    unfold applyS. simpl. intros f. simpl.
    setoid_rewrite Haa'. reflexivity.
  Qed.

Program Definition flipS {A B C : Setoid} : (A ---> B ---> C) ---> B ---> A ---> C :=
  mkMap3 (fun f b a => f a b).

  Next Obligation. intros f f' Hff' b b' Hbb' a a' Haa'. simpl. 
    now rewrite Haa', Hbb', Hff'.
  Qed.

Program Definition constS {A B : Setoid} : A ---> B ---> A :=
  mkMap2 const.

  Next Obligation. intros a a' Aa b b' Bb. unfold const. auto. Qed.

Definition setoid_pointwise_relation {α β : Setoid} : relation (α --> β) :=
  pointwise_relation α β.

Instance setoid_pointwise {α β : Setoid} :
  @PER (α --> β) (@setoid_pointwise_relation α β)%signature | 2.

(* Set Printing All. Print setoid_pointwise. About PER_s *)
(* Proof. unfold setoid_pointwise_relation. simpl_relation.  *)
(*   constructor; red ; intros. *)
(*   symmetry ; auto. *)
(*   transitivity y; firstorder. *)
(* Qed. *)

Infix "=∙=" := setoid_pointwise_relation (at level 60).

Inductive option_eq {A : Setoid} : relation (option A) :=
| option_eq_Some :> Proper (A ==> option_eq) Some
| option_eq_None :> Proper option_eq None.
Print Instances Proper.
Hint Resolve @option_eq_Some @option_eq_None : typeclass_instances.

Instance option_eq_refl : Reflexive (@option_eq A).
  red; intros; destruct x; constructor; reflexivity.
Qed.
Instance option_eq_symmetric : Symmetric (@option_eq A).
  red; intros; destruct H; constructor; auto with relations.
Qed.

Program Instance option_eq_trans : Transitive (@option_eq A).

  Next Obligation.
    induction H; depelim H0. constructor. now transitivity y.
    constructor.
  Qed.

Program Definition option_setoid (A : Setoid) : Setoid :=
  {| car := option A ; seq := option_eq |}.

  Next Obligation. constructor; typeclasses eauto. Qed.

Program Definition NoneS {A:Setoid} : option_setoid A :=
  None.

Program Definition SomeS {A:Setoid} : A ---> option_setoid A :=
  mkMap (fun a => Some a).

  Next Obligation. simpl_morph. Qed.