(************************************************************************)
(*  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é Paris Sud
 *              91405 Orsay, France *)

(** Standard instances for the sum type.*)

Set Implicit Arguments.
Unset Strict Implicit.

Require Export Coq.Program.Basics.
Require Import Prelude.Basics.
Require Import Prelude.Functor.

Definition sum_eq {A B : Setoid} : relation (A + B) :=
  fun x y =>
    match x, y with
      | inl x, inl y => x == y
      | inr x, inr y => x == y
      | _,     _     => False
    end.


Program Instance: Equivalence (@sum_eq A B).
Next Obligation.
  intro x; destruct x; simpl; reflexivity.
Qed.
Next Obligation.
  intros x y; destruct x; destruct y; simpl; (try symmetry; auto).
Qed.
Next Obligation.
  intros x y z Hxy Hyz;
    destruct x as [x|x]; destruct y as [y|y]; destruct z as [z|z]; simpl;
    try contradiction; transitivity y; auto.
Qed.

Program Definition sum_setoid (A B : Setoid) : Setoid :=
  {| car := A + B; seq := sum_eq |}.


Program Definition inlS {A B:Setoid} : A ---> sum_setoid A B := mkMap inl.
Solve Obligations using (repeat intro; auto).

Program Definition inrS {A B:Setoid} : B ---> sum_setoid A B := mkMap inr.
Solve Obligations using (repeat intro; auto).

Program Definition either {A B C}
  : (A ---> C) ---> (B ---> C) ---> sum_setoid A B ---> C :=
  mkMap3 (fun f g x => 
    match x with
      | inl a => f a
      | inr b => g b
    end).
Next Obligation.
  intros f1 f2 Hf g1 g2 Hg x y Hxy.
  destruct x; destruct y; simpl in Hxy; try contradiction; rewrite Hxy; auto.
Qed.

Print Grammar constr.
Program Instance sum_functor : Functor (sum_setoid A) := {
  fmap A B := mkMap2 (fun f x => either inlS (inrS ∙ f) x)
}.
Next Obligation.
  intros f1 f2 Hf x y Hxy.
  destruct x as [x|x]; destruct y as [y|y]; simpl in *; try contradiction; auto.
  rewrite Hxy; auto.
Qed.
Solve Obligations using (program_simpl; intro x; destruct x; reflexivity).