(**************************************************************)
(*   Copyright Dominique Larchey-Wendling *                 *)
(*                                                            *)
(*                             * Affiliation LORIA -- CNRS  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

Require Import List Arith Lia.

From Undecidability.Shared.Libs.DLW.Utils
  Require Import utils_tac utils_list utils_nat
                 fin_base.

From Undecidability.Shared.Libs.DLW.Vec
  Require Import pos vec.

Set Implicit Arguments.

(* This files gathers all constructivelly valid choice principles *)

(* This is standart constructive strong choice, no finiteness assumptions here *)

Theorem constructive_choice X (T : X Type) (R : x, T x Prop) :
          ( x, sig (R x))
        { f : x, T x | x, R x (f x) }.
Proof.
  intros f.
  exists ( x proj1_sig (f x)).
  intros x; apply (proj2_sig (f x)).
Qed.

Theorem constructive_choice' X Y (R : X Y Prop) :
          ( x, sig (R x))
        { f | x, R x (f x) }.
Proof.
  apply constructive_choice.
Qed.

Theorem constructive_dep_choice X Y (P : X Prop) (R : X Y Prop) :
          ( x, P x sig (R x))
        { f : x, P x Y | x Hx, R x (f x Hx) }.
Proof.
  intros f.
  exists ( x Hx proj1_sig (f x Hx)).
  intros x Hx; apply (proj2_sig (f x Hx)).
Qed.

Fact list_reif_t X Y (R : X Y Prop) l :
          ( x, In x l sig (R x))
        { f | x (Hx : In x l), R x (f x Hx) }.
Proof. apply constructive_dep_choice. Qed.

Fact pos_reif_t X n (R : pos n X Prop) : ( p, { x | R p x }) { f | p, R p (f p) }.
Proof. apply constructive_choice. Qed.

Fact vec_reif_t X n (R : pos n X Prop) : ( p, sig (R p)) { v | p, R p (vec_pos v p) }.
Proof.
  intros H.
  apply pos_reif_t in H.
  destruct H as (f & Hf).
  exists (vec_set_pos f).
  intro; rewrite vec_pos_set; trivial.
Qed.

(* Now weak choice principles that assume some finiteness and discreteness *)

Section finite_discrete_choice.

  Variable (X Y : Type) (R : X Y Prop)
           (X_discrete : x y : X, { x = y } + { x y }).

  Theorem list_discrete_choice l :
            ( x, In x l ex (R x))
          f, x (Hx : In x l), R x (f x Hx).
  Proof.
    induction l as [ | x l IHl ]; intros Hl.
    + exists ( x (Hx : @In X x nil) False_rect Y Hx).
      intros _ [].
    + destruct (Hl x) as (y & Hy); simpl; auto.
      destruct IHl as (f & Hf).
      * intros; apply Hl; simpl; auto.
      * assert ( z, In z (x::l) x z In z l) as .
        { intros z [ | ] ?; tauto. }
        exists ( z Hz
          match X_discrete x z with
            | left _ y
            | right H f z ( _ Hz H)
          end).
        intros z Hz.
        destruct (X_discrete x z); subst; auto.
  Qed.

  Fact finite_discrete_choice :
         finite X
       ( x, ex (R x)) f, x, R x (f x).
  Proof.
    intros (l & Hl) H.
    destruct list_discrete_choice with (l := l) as (f & Hf); auto.
    exists ( x f x (Hl x)); auto.
  Qed.

End finite_discrete_choice.

Local Hint Resolve finite_t_pos finite_t_finite : core.

Fact pos_reification X n (R : pos n X Prop) : ( p, x, R p x) f, p, R p (f p).
Proof.
  apply finite_discrete_choice; auto.
  apply pos_eq_dec.
Qed.

Notation pos_reif := pos_reification.

Fact vec_reif X n (R : pos n X Prop) : ( p, ex (R p)) v, p, R p (vec_pos v p).
Proof.
  intros H.
  apply pos_reification in H.
  destruct H as (f & Hf).
  exists (vec_set_pos f).
  intro; rewrite vec_pos_set; trivial.
Qed.

Section finite_t_dec_choose_one.

  (* This compares to Constructive Epsilon but here over a finite type
      instead of nat *)

  Variable (X : Type) (P Q : X Prop)
           (HX : finite_t X)
           (HQ : fin_t Q)
           (Pdec : x, { P x } + { P x }).

  Fact list_dec_choose_one l : ( x, In x l P x) { x | In x l P x }.
  Proof.
    clear HX Q HQ.
    induction l as [ | x l IHl ]; intros H.
    + exfalso; destruct H as (_ & [] & _).
    + destruct (Pdec x) as [ | ].
      * exists x; simpl; auto.
      * destruct IHl as (y & & ).
        - destruct H as (y & [ | Hy ] & ?); firstorder.
        - exists y; simpl; auto.
  Qed.

  Fact fin_t_dec_choose_one :
         ( x, Q x P x) { x | Q x P x }.
  Proof.
    revert HQ; intros (l & Hl) H.
    destruct (list_dec_choose_one l) as (x & & ).
    + destruct H as (x & ? & ?); exists x; rewrite Hl; auto.
    + exists x; rewrite Hl; auto.
  Qed.

  Fact finite_t_dec_choose_one : ex P sig P.
  Proof.
    clear Q HQ.
    revert HX; intros (l & Hl) H.
    destruct (list_dec_choose_one l) as (x & & ); firstorder.
  Qed.

End finite_t_dec_choose_one.

(* Reification of a total relation into a function,
    ie this is relational choice over a finite co-domain
    with a decidable relation *)

Definition finite_t_dec_choice X Y (R : X Y Prop) :
        finite_t Y
      ( x y, { R x y } + { R x y })
      ( x, ex (R x))
      { f | x, R x (f x) }.
Proof.
  intros .
  exists ( x proj1_sig (finite_t_dec_choose_one ( x) ( x))).
  intros x; apply (proj2_sig (finite_t_dec_choose_one ( x) ( x))).
Qed.

Fact pos_dec_reif n (P : pos n Prop) (HP : p, { P p } + { P p }) : ex P sig P.
Proof. apply finite_t_dec_choose_one; auto. Qed.

(* This is needed to reify a computable binary relation representing a unary function
    into an actual function *)

Fact pos_dec_rel2fun n (R : pos n pos n Prop) :
         ( a b, { R a b } + { R a b })
       ( p, ex (R p)) { f | p, R p (f p) }.
Proof. apply finite_t_dec_choice; auto. Qed.