(************************************************************************)
(*  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        *)
(************************************************************************)

(** * Boolean predicates instances of preorder.

   Author: Matthieu Sozeau <sozeau@lri.fr>
   Institution: LRI, CNRS UMR 8623 - Université Paris Sud
                91405 Orsay, France 

*)

Require Export Order.Lattice.
Require Import Coq.Program.Tactics.

Instance bool_pred_setoid : Equivalence (A -> bool) (fun f g => forall x, f x = g x).
Proof.
  intros. 
  constructor ; reduce_goal; subst* ; order.
  rewrite H ; rewrite H0 ; reflexivity.
Qed.

Definition bool_pred_ord {A} (f g : A -> bool) :=
  forall x, implb (f x) (g x) = true.

Program Instance bool_pred_preorder : PreOrder _ (bool_pred_ord (A:=A)).

  Next Obligation.
  Proof.
    unfold bool_pred_ord, implb ; intros.

    destruct (x x0) ; auto.
  Qed.

  Next Obligation.
  Proof.
    unfold bool_pred_ord, implb in * ; intros.
    pose (H x0) as H' ; pose (H0 x0) as H''.
    clear H H0.
    destruct (x x0) ; auto.
    destruct (y x0) ; auto.
    discriminate.
  Qed.

Program Instance bool_pred_partial_order : PartialOrder bool_pred_setoid (bool_pred_preorder (A:=A)).

  Next Obligation.
  Proof.
    unfold bool_pred_ord, implb ; intros.

(*     (* Possibly improved if we can rewrite under dependent foralls _and_ matches/if *) *)
(*     setoid_rewrite H at 1. *)
(*     change (all (fun x1 => (if x x1 then x0 x1 else true) = true) <->  *)
(*       all (fun x1 => (if y x1 then y0 x1 else true) = true)). *)
(*     setoid_rewrite H at 1. *)

    split; intros H.
    reduce.
    split ; intros x1.
    rewrite <- H. destruct (x x1) ; auto.
    rewrite <- H. destruct (x x1) ; auto.
    
    red in H. firstorder. specialize (H x1) ; specialize (H0 x1).
    destruct (x x1) ; auto.
    destruct (x0 x1) ; auto.
  Qed.

Instance false_infimum : Infimum _ (fun x : A => false).
Proof.
  do 2 red ; intros.
  intro. refl.
Qed.

Instance true_supremum : Supremum _ (fun x : A => true).
Proof.
  do 2 red ; intros.
  intro. destruct (x x0) ; refl.
Qed.

Definition subset_orb {A} (sub : subset (A -> bool)) (x : A) : bool :=
  (** FIXME: must range over sub, add a foldable or something similar. *)
  true.

Definition bool_pred_least_upper_bound A (sub : subset (A -> bool)) :
  least_upper_bound sub (fun x => subset_orb sub x).
Proof.
  split ; red ; intros.
Admitted.