(* AUTEURS / AUTHORS :                          *)
(* Judicaël Courant,   Jean-François Monin      *)
(* VERIMAG, Université Joseph Fourier, Grenoble *)
(*                                         2006 *)

(* $Id: Separable.v,v 1.5 2006/07/14 16:50:56 monin Exp $ *)

(* We need decidable equalities *)

(* Motivation:
   - proof unicity makes using {x|P x} simpler and cleaner
     (don't need magic proof irrelevance)
   - proofs of decidibility of equality on A (and others things such as lt)
     are linear in the size of A (instead of quadratic)
*)

Require Import RelProps.

(* ---------------------------------------------------------------- *)

Set Implicit Arguments.

Section sec_comp.
Variable A : Set.
Variable lt : A -> A -> Prop.

Inductive cmptype (x y : A) : Set :=
  | Clt : lt x y -> cmptype x y
  | Ceq : x = y -> cmptype x y
  | Cgt : lt y x -> cmptype x y
.

Definition total := forall x y, cmptype x y. 

End sec_comp.

Unset Implicit Arguments.

Ltac solve_cmptype := 
  (apply Clt; simpl; solve [intuition]) ||
  (apply Ceq; simpl; reflexivity) ||
  (apply Cgt; simpl; solve [intuition]) || idtac.

Ltac destruct_cmptype := intro; subst; solve_cmptype.

(* ---------------------------------------------------------------- *)

(* OBSOLÈTE -> A FAIRE : virer separable *)
Definition separable (A:Set) := forall (x y: A), {x=y}+{x<>y}.

Ltac rew_sig :=
  match goal with
  | [ E: exist ?p ?a ?pa = _ |- context f [?a] ] => 
     let fa := context f [proj1_sig (exist p a pa)] in 
     change fa; rewrite E
  end.

Ltac false_hyp :=  match goal with [ F: False |- _] => case F end.

Section sec_sep.

Variable A: Set.
Variable P: A -> Prop.
Hypothesis sepA: separable A.
Hypothesis uniq_proof: forall x (p q: P x), p=q.

Definition inherits_sep : separable {a:A | P a}.
red; destruct x as [a pa]; destruct y as [b pb]. 
case (sepA a b). 
   intro; subst. left. rewrite (uniq_proof b pa pb). reflexivity.
   intros ab; right. intro e; apply ab. rew_sig. simpl. reflexivity.
Defined.

End sec_sep.

(* utility *)
Remark uniq_True: forall t1 t2 : True, t1 = t2.
intros s1 s2; case s1; case s2; reflexivity. 
Qed.

Remark uniq_False: forall f1 f2 : False, f1 = f2.
intro f; case f.
Qed.

(* Warning: disjuncts must be incompatible *)
Inductive True_False : Prop -> Type :=
  | TF_True : True_False True
  | TF_False : True_False False
  | TF_conj : 
       forall p q, 
       True_False p -> True_False q -> True_False (p /\ q)
  | TF_disj : 
       forall p q, 
       True_False p -> True_False q -> (p -> q -> False) ->
       True_False (p \/ q)
.

Hint Resolve TF_True TF_False TF_conj : sep_db.

Remark uniq_True_False : 
  forall p, True_False p -> forall x y: p, x = y.
induction 1. 
  exact uniq_True.
  exact uniq_False.
  intros (x1,x2) (y1,y2). rewrite (IHX1 x1 y1); rewrite (IHX2 x2 y2); reflexivity.
  intros [x | x] [y | y].
    rewrite (IHX1 x y); reflexivity.
    case (f x y).
    case (f y x).
    rewrite (IHX2 x y); reflexivity.
Qed.

Remark dec_True_False : forall p, True_False p -> {p} + {~p}.
induction 1; intuition.
Qed.

Implicit Arguments uniq_True_False.

Definition prop_True_False A (P: A->Prop) := forall (x: A), True_False (P x).
Definition rel_True_False A (R: A->A->Prop) := forall (x y: A), True_False (R x y).
Implicit Arguments prop_True_False [A].
Implicit Arguments rel_True_False [A].

(* ---------------------------------------------------------------- *)

Set Implicit Arguments.

Record sortable : Type := mksrt {
  X : Set;

  ueq : X -> X -> Prop;
  ult : X -> X -> Prop;

  ueq_True_False : rel_True_False ueq;
  ueq_equal : is_equal ueq;
  ueq_refl : reflexive ueq;

  ult_True_False : rel_True_False ult;
  ult_ueq_False : incompatibles ult ueq;
  ult_trans : transitive ult;
  ult_total : total ult
}.

Notation "| A |" := (X A) (at level 80).

Ltac subs_ueq :=
   match goal with
   | [ U: ueq ?A ?x ?y |- _ ] =>
        generalize (ueq_equal A x y U); let E := fresh in intro E; subst
   end.


Section sec_def_monot.

Variable A B : sortable.
Variable f : |A| -> |B| .
Definition monot := forall x y, ult A x y -> ult B (f x) (f y).

End sec_def_monot.

Implicit Arguments monot [A B].

Inductive monot_fun (A B: sortable) : Set :=
  MF : forall (f: |A| -> |B|), monot f -> monot_fun A B. 
Implicit Arguments MF [A B].

Definition app_monot A B (f: monot_fun A B) (x : |A|) := 
  match f with | MF f _ => f x end.
Implicit Arguments app_monot [A B].

Section sec_comp_monot.

Variable A B C : sortable.
Variable f : |A| -> |B| .
Variable g : |B| -> |C| .
Hypothesis mf : monot f.
Hypothesis mg : monot g.

Lemma monot_comp : monot (fun x => g (f x)).
intros x y lxy. apply mg. apply mf. assumption.
Qed.

End sec_comp_monot.


Unset Implicit Arguments.

(* ---------------------------------------------------------------- *)

Section sec_such_that.

Variable A: Set.
Variable P: A -> Prop.
Variable R: A -> A -> Prop.
Hypothesis P_True_False : prop_True_False P. 
Hypothesis R_True_False : rel_True_False R. 

Theorem uniq_2: rel_unique R.
intros x y. apply (uniq_True_False (R_True_False x y)).
Qed.

(* *)

Definition urel_sig (s1 s2: {x:A | P x}) : Prop :=
  let (x1, _) := s1 in let (x2, _) := s2 in R x1 x2.

Theorem urel_sig_True_False : rel_True_False urel_sig.
red. destruct x; destruct y; simpl; auto.
Qed.

(* *)

Theorem urel_sig_equal : is_equal R -> is_equal urel_sig.
red. intros R_equal (x1,p1) (x2,p2). simpl. intro r. generalize p1 p2; clear p1 p2. 
rewrite (R_equal _ _ r). intros p1 p2. rewrite (uniq_True_False (P_True_False x2) p1 p2). 
reflexivity.
Qed.

Theorem urel_sig_refl : reflexive R -> reflexive urel_sig.
red. destruct x; simpl; trivial. 
Qed.

Theorem urel_sig_trans : transitive R -> transitive urel_sig.
red. intros tr (x,px) (y,py) (z,pz); simpl. exact (tr x y z).
Qed.

Theorem urel_sig_total : total R -> total urel_sig.
red. intros to (x,px) (y,py). case (to x y); intro C. 
  apply Clt. assumption. 
  apply Ceq. generalize py; clear py. case C; clear C y; intro py. 
    case (uniq_True_False (P_True_False x) px py). reflexivity.
  apply Cgt; assumption. 
Qed.

(* *)

Variable Q: A -> A -> Prop.

Theorem nueq_irrefl : reflexive R -> incompatibles Q R -> irreflexive Q.
unfold incompatibles; unfold irreflexive. intros R_refl QPF x Qxx. eauto. 
Qed.

Theorem uniq_sep: is_equal R -> reflexive R -> separable A.
red. intros er rr x y. case (dec_True_False (R x y)); auto.
  right; intro e; subst; auto. 
Qed.

End sec_such_that.

Implicit Arguments uniq_2 [A R].
Implicit Arguments uniq_sep [A R].
Implicit Arguments urel_sig [A].
Implicit Arguments urel_sig_True_False [A R].
Implicit Arguments urel_sig_equal [A P R].
Implicit Arguments urel_sig_refl [A P R].
Implicit Arguments nueq_irrefl [A R Q].

Theorem urel_sig_incomp : 
  forall (A:Set) (P:A->Prop) (Q R: A -> A -> Prop),
  incompatibles Q R -> incompatibles (urel_sig P Q) (urel_sig P R).
intros A' P Q R incomp (x1,p1) (x2,p2); simpl. exact (incomp x1 x2). 
Qed.

Implicit Arguments urel_sig_incomp [A P Q R].

(* *)

Definition relativize_sortable :
  forall (s: sortable) (P: |s| -> Prop), prop_True_False P -> sortable.
destruct s as [Y ueqY ultY]. simpl. intros P pTF. 
apply (mksrt (X:={x : Y | P x}) (ueq:=urel_sig P ueqY) (ult:=urel_sig P ultY)).
  apply urel_sig_True_False; assumption.
  apply urel_sig_equal; assumption. 
  apply urel_sig_refl; assumption. 
  apply urel_sig_True_False; assumption. 
  apply urel_sig_incomp; assumption. 
  apply urel_sig_trans; assumption. 
  apply urel_sig_total; assumption. 
Defined.


(* ---------------------------------------------------------------- *)
(* Basic example 1: natural numbers *)

Fixpoint ueq_nat (n m:nat) {struct n}: Prop :=
  match n, m with
  | O, O => True
  | S n, S m => ueq_nat n m
  | _, _ => False
  end.

Lemma ueq_nat_True_False : rel_True_False ueq_nat.
red. induction x; destruct y; simpl; intuition.
Qed.

Lemma ueq_nat_equal : is_equal ueq_nat. 
red. induction x; destruct y; simpl; intro; reflexivity || false_hyp || idtac.
rewrite (IHx y); auto.
Qed.

Lemma ueq_nat_refl : reflexive ueq_nat.
red; induction x; simpl; auto.
Qed.

Theorem uniq_ueq_nat : rel_unique ueq_nat.
exact (uniq_2 ueq_nat_True_False).
Qed.

Theorem nat_sep : separable nat.
exact (uniq_sep ueq_nat_True_False ueq_nat_equal ueq_nat_refl).
Qed.

(* ---------------------------------------------------------------- *)
(* Other version of lt *)

Fixpoint ult_nat (n m:nat) {struct n}: Prop :=
  match n, m with
  | O, S _ => True
  | S n, S m => ult_nat n m
  | _, _ => False
  end.

Theorem ult_nat_True_False : rel_True_False ult_nat.
red. induction x; destruct y; simpl; intuition.
Qed.

Theorem uniq_ult_nat : rel_unique ult_nat.
exact (uniq_2 ult_nat_True_False).
Qed.

Require Import Arith.

Theorem lns_lt : forall n m, ult_nat n m -> lt n m.
induction n; destruct m; simpl; intros; false_hyp || auto with arith.
Qed.

Theorem lt_lns : forall n m, lt n m -> ult_nat n m.
induction n; destruct m; simpl; intros; false_hyp || auto with arith.
  apply (lt_irrefl O); assumption.
  apply (lt_n_O (S n)); assumption.
Qed.

Theorem ult_nat_trans : transitive ult_nat. 
red; intros. apply lt_lns. apply lt_trans with y; apply lns_lt; assumption. 
Qed.

Lemma ult_ueq_nat_False : incompatibles ult_nat ueq_nat.
red. induction x; destruct y; simpl; intuition. eauto.
Qed.

Theorem ult_nat_irrefl : irreflexive ult_nat.
intros n. apply (nueq_irrefl ueq_nat_refl ult_ueq_nat_False).
Qed.

Theorem ult_nat_total : total ult_nat.
red. induction x; destruct y; solve_cmptype.
case (IHx y); destruct_cmptype.
Qed.

(* *)

Definition Snat :=
   mksrt ueq_nat_True_False ueq_nat_equal ueq_nat_refl 
         ult_nat_True_False ult_ueq_nat_False ult_nat_trans ult_nat_total.

(* ---------------------------------------------------------------- *)

Set Implicit Arguments.

Section sec_injection.

Variable A : Set.
Variable BS : sortable.
Variable i : A -> |BS| .
Variable s : |BS| -> A .
Hypothesis i_injective : forall x, s (i x) = x.

Remark is_injective : forall x y, i x = i y -> x = y.
intros x y E.
pattern x; rewrite <- i_injective.
pattern y; rewrite <- i_injective.
rewrite E. reflexivity.
Qed.

Remark is_surjective : forall x, exists y, s y = x.
intro x. exists (i x). apply i_injective. 
Qed.

Definition ueq_inj x1 x2 := ueq BS (i x1) (i x2).
Definition ult_inj x1 x2 := ult BS (i x1) (i x2).

Lemma ueq_inj_True_False : rel_True_False ueq_inj. 
intros x1 x2. apply (ueq_True_False BS (i x1) (i x2)). 
Qed.

Lemma ult_inj_True_False : rel_True_False ult_inj. 
intros x1 x2. apply (ult_True_False BS (i x1) (i x2)). 
Qed.

Lemma ueq_inj_equal : is_equal ueq_inj.
intros x1 x2 u. case (i_injective x1). case (i_injective x2). 
case (ueq_equal BS (i x1) (i x2) u). reflexivity.
Qed.

Lemma ueq_inj_refl : reflexive ueq_inj.
intro x. exact (ueq_refl BS (i x)). 
Qed. 

Lemma ult_ueq_inj_False : incompatibles ult_inj ueq_inj.
intros x1 x2. unfold ult_inj, ueq_inj.
apply (ult_ueq_False BS (i x1) (i x2)).
Qed.

Lemma ult_inj_trans : transitive ult_inj.
intros x1 x2 x3. unfold ult_inj, ueq_inj. apply (ult_trans BS (i x1) (i x2) (i x3)).
Qed.

Lemma ult_inj_total :  total ult_inj.
intros x1 x2. case (ult_total BS (i x1) (i x2)); intro c.
  apply Clt; assumption. 
  apply Ceq. apply is_injective; assumption. 
  apply Cgt; assumption. 
Qed.

Definition Sinject :=
   mksrt ueq_inj_True_False ueq_inj_equal ueq_inj_refl 
         ult_inj_True_False ult_ueq_inj_False ult_inj_trans ult_inj_total.

End sec_injection.

Implicit Arguments Sinject [A i s].

Section sec_inj_to_nat.

Variable A: Set.
Variable nat_of: A -> nat .
Variable of_nat: nat -> A.
Hypothesis inject : forall x, of_nat (nat_of x) = x.

Definition mksrt_from_nat := Sinject Snat inject.

End sec_inj_to_nat.

Implicit Arguments mksrt_from_nat [A nat_of of_nat].

Unset Implicit Arguments.

(*
Implicit Arguments ueqn [A].
Implicit Arguments ueqn_equal [A nat_of of_nat].
Implicit Arguments ueqn_refl [A].
Implicit Arguments inj_sep [A nat_of of_nat].
Implicit Arguments mksrt_from_nat [A nat_of of_nat].

Section sec_inj_to_nat.

Variable A: Set.
Variable nat_of: A -> nat.
Variable of_nat: nat -> A.
Hypothesis inject : forall (x: A), of_nat (nat_of x) = x.

Remark is_injective : forall (x y: A), nat_of x = nat_of y -> x = y.
intros x y E.
pattern x; rewrite <- inject.
pattern y; rewrite <- inject.
rewrite E. reflexivity.
Qed.

Definition ueqn (x y:A) := ueq_nat (nat_of x) (nat_of y).

Theorem ueqn_True_False : rel_True_False ueqn. 
red. intros. unfold ueqn. apply ueq_nat_True_False. 
Qed.

Lemma ueqn_equal : is_equal ueqn.
unfold ueqn. intros x y e. apply is_injective. apply ueq_nat_equal. exact e. 
Qed.

Lemma ueqn_refl : reflexive ueqn.
intro x. unfold ueqn. apply ueq_nat_refl.
Qed.

Theorem uniq_ueqn : rel_unique ueqn.
exact (uniq_2 ueqn_True_False).
Qed.

Theorem inj_sep : separable A.
exact (uniq_sep ueqn_True_False ueqn_equal ueqn_refl).
Qed.

(* *)

Definition ultn (x y:A) := ult_nat (nat_of x) (nat_of y).

Theorem ultn_True_False : rel_True_False ultn. 
red. intros. unfold ultn. apply ult_nat_True_False. 
Qed.

Theorem ultn_ueqn_False : incompatibles ultn ueqn.
red; unfold ultn; unfold ueqn. intros. eapply ult_ueq_nat_False; eauto. 
Qed.

Theorem ultn_trans : transitive ultn. 
red; unfold ultn. intros. eapply ult_nat_trans; eauto.
Qed.

Theorem ultn_total : total ultn. 
red; unfold ultn. intros. case (ult_nat_total (nat_of x) (nat_of y)); intro c. 
  apply Clt; assumption. 
  apply Ceq. apply is_injective; assumption. 
  apply Cgt; assumption. 
Qed.

(* *)

Definition mksrt_from_nat :=
   mksrt ueqn_True_False ueqn_equal ueqn_refl 
         ultn_True_False ultn_ueqn_False ultn_trans ultn_total.

End sec_inj_to_nat.

Unset Implicit Arguments.

Implicit Arguments ueqn [A].
Implicit Arguments ueqn_equal [A nat_of of_nat].
Implicit Arguments ueqn_refl [A].
Implicit Arguments inj_sep [A nat_of of_nat].
Implicit Arguments mksrt_from_nat [A nat_of of_nat].
*)

(* ---------------------------------------------------------------- *)
(* Example for inherits_sep, just for fun and illustration purposes *)

Fixpoint is_even (n:nat) : Prop :=
  match n with
  | O => True
  | S O => False
  | S (S n) => is_even n
  end.

Theorem is_even_True_False : prop_True_False is_even.
red. fix 1. 
intro n; case n; clear n; simpl; intuition.
case n; clear n;  [intuition | idtac].
    intros n. apply (is_even_True_False n). 
Qed.

Theorem uniq_is_even : forall n (E1 E2: is_even n), E1=E2.
intro n.
exact (uniq_True_False (is_even_True_False n)).
Qed.

Definition even := {n:nat | is_even n}.

Definition even_sep : separable even. 
unfold even. apply inherits_sep. 
  exact nat_sep. 
  exact uniq_is_even.
Defined.

(* ---------------------------------------------------------------- *)
(* Basic example 2: Booleans *)

Definition nat_of_bool (b: bool) : nat :=
  match b with
  | true => 3
  | false => 1
  end.

Definition bool_of_nat (n: nat) : bool :=
  match n with
  | 3 => true
  | 1 => false
  | _ => false
  end.

Lemma inject_nat_bool : forall (x:bool), bool_of_nat (nat_of_bool x) = x.
destruct x; reflexivity. 
Qed.

(* *)

Definition Sbool := mksrt_from_nat inject_nat_bool.

(* projections *)

Definition ueq_bool : bool -> bool -> Prop := ueq Sbool.  

Theorem ueq_bool_True_False : rel_True_False ueq_bool.
exact (ueq_True_False Sbool).
Qed.

Lemma ueq_bool_equal : is_equal ueq_bool.
exact (ueq_equal Sbool).
Qed.

Lemma ueq_bool_refl : reflexive ueq_bool.
exact (ueq_refl Sbool). 
Qed.

(* more or less obsolete *)
(*
Theorem uniq_ueq_bool : rel_unique ueq_bool. 
exact (uniq_ueqn (s:nat_of_bool).
Qed.

Theorem bool_sep : separable bool.
exact (inj_sep inject_nat_bool).
Qed.
*)