Library Iota

Set Implicit Arguments.

Definition inhabited (A:Type) := exists a:A, True.

Parameter epsilon : forall (A:Type), inhabited A -> (A->Prop) -> A.

Definition iota (A:Type)(inh : inhabited A)(P: A-> Prop) :=
   epsilon inh (fun x => P x /\ forall y, P y -> x = y).

Inductive defined (A:Type)(P:A->Prop) : A -> Prop :=
 defined_intro : forall inh , (exists a, P a) ->
                     (forall a b, P a -> P b -> a = b) ->
                     defined P (iota inh P).

Section AFC.
  Variables (A:Type)(R:A->A->Prop).
  Hypothesis H : forall x, exists y, R x y.

 Remark inhab : forall x, inhabited (sigT (R x)).
 Proof.
  intro x; case (H x);intros.
  exists (existT _ x0 H0).
  trivial.
 Qed.
 
 Let pi1 := fun (x:A) (s:sigT (R x)) => match s with (existT w _) => w end.
 
 Let phi := (fun x => epsilon (inhab x) (fun (s:(sigT (R x))) => R x (pi1 s))).

 Lemma afc : exists f, forall x, R x (f x).
 Proof.
  exists (fun x => match (phi x) with (existT z _) => z end).
  intro;case (phi x);auto.
 Qed.
End AFC.

Definition epsilonax (A:Type) (inh:inhabited A):=
                   forall (P : A -> Prop),
                     (exists a, P a) ->
                     P (epsilon inh P).

 

Definition iotax (A:Type) (inh:inhabited A):=
                   forall (P : A -> Prop),
                     (exists a, P a) ->
                     (forall a b, P a -> P b -> a = b) ->
                     P (iota inh P).

Theorem epsilon_ind :
   forall (A:Type)(i:inhabited A)(HH:epsilonax i)(P:A->Prop)
          (Q:A->Prop), (exists a:A, P a)->
                       (forall a : A, P a -> Q a) ->
                       (Q (epsilon i P)).
Proof.
 intros A i H P Q exP P_Q.
 apply P_Q.
 apply H; assumption.
Qed.

Theorem epsilon_iota : forall (A:Type)(inh: inhabited A),
                  epsilonax inh -> iotax inh.
Proof.
  red; intros A inh eax P exP unicityP.
  unfold iota;apply epsilon_ind; auto.
  case exP; intros a Ha;exists a;auto.
  tauto.
Qed.

  
  
 

Ltac iota_elim_aux :=
  match goal with [ |- (?P (iota (A:=?X) ?inh ?Q))] =>
    let HH := fresh "Iota" in
       (assert (HH:iotax inh);[auto|generalize (iota inh Q) (HH Q)])
  end.

Ltac iota_elim := iota_elim_aux ||
  match goal with
  [ |- (?P (?k ?arg))] =>
   (let v := eval cbv zeta beta delta [k] in (k arg) in
     (match v with (iota ?inh ?d) => change (P v); iota_elim_aux end))
 | [ |- (?P ?k)] =>
   (let v := eval cbv zeta beta delta [k] in k in
     (match v with (iota ?inh ?d) => change (P v); iota_elim_aux end))
  end.

Theorem iota_ind :
   forall (A:Type)(i:inhabited A)(HH:iotax i)(P:A->Prop)
          (Q:A->Prop), (exists a:A, P a)->
                       (forall a a':A, P a -> P a' -> a=a') ->
                       (forall a : A, P a -> Q a) ->
                       (Q (iota i P)).
Proof.
  intros.
  apply H1.
  apply HH;auto.
Qed.

Ltac epsilon_elim_aux :=
  match goal with [ |- (?P (epsilon (A:=?X) ?inh ?Q))] =>
    let HH := fresh "Epsilon" in
       (assert (HH:epsilonax inh);[auto|generalize (epsilon inh Q) (HH Q)])
  end.

Ltac epsilon_elim := epsilon_elim_aux ||
  match goal with [ |- (?P (?k ?d))] =>
   (let v := eval cbv zeta beta delta [k] in (k d) in
     (match v with (epsilon ?inh ?d) => change (P v); epsilon_elim_aux end))
  | [ |- (?P ?k)] =>
   (let v := eval cbv zeta beta delta [k] in k in
     (match v with (epsilon ?inh ?d) => change (P v); epsilon_elim_aux end))
  end.

Section A_fixed.
  Variable A : Type.
  Hypothesis inh : inhabited A.
  Hint Unfold iotax epsilonax.
 

Record def (pred: A -> Prop): Type := {
  def_iotax : iotax inh;
  def_ex : exists d, pred d;
  def_unic : forall d d', pred d ->
                          pred d' ->
             d = d'
}.

Record choice(pred : A-> Prop) : Type := {
  choice_ax : epsilonax inh;
  choice_ex : exists d, pred d
}.

Definition the (pred : A->Prop)(d:def pred) :=
   iota inh pred.

Definition some (pred : A->Prop)(c : choice pred) :=
  epsilon inh pred.

Theorem the_ok : forall (pred:A->Prop)(d:def pred), pred (the d).
Proof.
 destruct d;simpl.
 unfold the;simpl.
 auto.
 apply def_iotax0; auto.
Qed.

Theorem the_rw : forall (pred:A->Prop)(d:def pred) a, pred a -> a = the d.
Proof.
 intros p d;case d.
 simpl;intros.
 unfold the;simpl.
 apply def_unic0.
 auto.
 apply def_iotax0.
 auto.
 auto.
Qed.

Theorem some_ok : forall (pred:A->Prop)(c:choice pred), pred (some c).
Proof.
  destruct c as [ax exP];simpl.
  unfold some;simpl; auto.
  apply ax;auto.
Qed.

End A_fixed.

tactics for using definitions

Ltac the_elim_aux :=
  match goal with [ |- (?P (the ?d))] =>
    generalize (the d) (the_ok d); simpl
  end.

Ltac the_elim := the_elim_aux ||
  match goal with [ |- (?P ?k)] =>
   (let v := eval cbv beta zeta delta [k] in k in
     (match v with (the ?d) => change (P v); the_elim_aux end))
  end.

Ltac def_tac := apply Build_def .

Ltac define inh P :=
   assert (d : def inh P);[ def_tac | exact (the d)];auto.

Ltac some_elim_aux :=
  match goal with [ |- (?P (some ?d))] =>
    generalize (some d) (some_ok d); simpl
  end.

Ltac some_elim := some_elim_aux ||
  match goal with [ |- (?P ?k)] =>
   (let v := eval cbv beta zeta delta [k] in k in
     (match v with (some ?d) => change (P v); some_elim_aux end))
  end.

Ltac choice_tac := apply Build_choice .

Ltac choose inh P :=
   assert (d : choice inh P);[ choice_tac| exact (some d)];auto.

Section AB_fixed.

 
  Variables A B: Type.
  Hint Unfold iotax.

 
Record choice_defun (DA: A -> Prop)(R : A -> B -> Prop) : Type := {
  choice_defun_inh : inhabited B;
  choice_defun_epsax : epsilonax choice_defun_inh;
  choice_defun_ex : forall d, DA d -> exists d', R d d'}.

Record defun (DA: A -> Prop)(R : A -> B -> Prop) : Type := {
  fun_inh : inhabited B;
  fun_iotax : iotax fun_inh;
  fun_ex : forall d, DA d -> exists d', R d d';
  fun_u : forall d d' d'', DA d -> R d d' -> R d d'' -> d' = d''}.

Definition iota_fun (inhB : inhabited B)(DA : A->Prop)(R:A->B->Prop)(a:A):=
      (iota inhB (fun (b:B) => DA a /\ R a b)).

Definition choice_fun (inhB : inhabited B)(DA : A->Prop)(R:A->B->Prop)(a:A):=
      (epsilon inhB (fun (b:B) => DA a /\ R a b)).

Lemma choice_fun_ok : forall inhB : inhabited B,
   epsilonax inhB ->
  forall (DA : A->Prop)(R:A->B->Prop)(a:A),
   (exists d : B, R a d) ->
   DA a -> R a (choice_fun inhB DA R a).
Proof.
 intros.
 unfold choice_fun.
 pattern (epsilon inhB (fun b : B => DA a /\ R a b)).
 epsilon_elim.
 intros.
 case H2;intuition.
 case H0;intros.
 exists x;auto.
Qed.

Lemma iota_fun_ok : forall inhB : inhabited B,
   iotax inhB ->
  forall (DA : A->Prop)(R:A->B->Prop)(a:A),
   (exists d : B, R a d) ->
   (forall d d', R a d -> R a d' -> d = d') ->
   DA a -> R a (iota_fun inhB DA R a).
Proof.
 intros.
 unfold iota_fun.
 pattern (iota inhB (fun b : B => DA a /\ R a b)).
 iota_elim.
 intros.
 case H3;intuition.
 case H0;intros.
 exists x;auto.
Qed.

Definition make_defun (inhB : inhabited B)(iotaB : iotax inhB)
                      (P:A->Prop)
                      (R:A -> B -> Prop)
                      (e : forall d, P d -> exists d',
                                 R d d')
                     (u: forall d d' d'',
                      P d -> R d d' -> R d d'' -> d' = d'') : defun P R.
 intros.
 exact (Build_defun P R iotaB e u).
Defined.

Definition make_choice_defun (inhB : inhabited B)(eB : epsilonax inhB)
                      (P:A->Prop)
                      (R:A -> B -> Prop)
                      (e : forall d, P d -> exists d',
                                 R d d')
                       : choice_defun P R.
 intros.
 exact (Build_choice_defun P R eB e).
Defined.

Definition some_fun (P: A-> Prop)(R:A->B->Prop)
              (d:choice_defun P R) := choice_fun (choice_defun_inh d) P R.

Definition the_fun (P: A-> Prop)(R:A->B->Prop)
              (d:defun P R) := iota_fun (fun_inh d) P R.

Theorem choice_defun_ok : forall (P: A-> Prop)(R:A->B->Prop)
              (d:choice_defun P R) (x:A), P x -> R x (some_fun d x).
Proof.
 intros P R d; case d.
 intros.
 unfold some_fun.
 unfold choice_fun.
 simpl.
 pattern (epsilon choice_defun_inh0 (fun b : B => P x /\ R x b)).
 epsilon_elim.
 intros.
 auto.
  case H0.
  case (choice_defun_ex0 x);intros.
 auto.
 exists x0;auto.
 auto.
Qed.

Theorem defun_ok : forall (P: A-> Prop)(R:A->B->Prop)
              (d:defun P R) (x:A), P x -> R x (the_fun d x).
Proof.
 intros P R d; case d.
 intros.
 unfold the_fun.
 unfold iota_fun.
 simpl.
 pattern (iota fun_inh0 (fun b : B => P x /\ R x b)).
 iota_elim.
 intros.
 auto.
 case H0.
 case (fun_ex0 x);intros.
 auto.
 exists x0;auto.
 intuition.
 eauto.
 auto.
Qed.

End AB_fixed.

 
Ltac choice_defun_elim_aux :=
match goal with [ |- (?P (some_fun ?d ?t)) ] =>
 (generalize (some_fun d t) (choice_defun_ok d t);
 simpl ;
    let H := fresh "H'" in
           let P := fresh in
             let U := fresh "y" in
             ( intro U ;

 match goal with [ |- (?A -> ?B) -> ?C ] =>
       (assert (H : A);[try auto | intro P; generalize (P H)]) end)
  
    )
end.

Ltac defun_elim_aux :=
match goal with [ |- (?P (the_fun ?d ?t)) ] =>
 (generalize (the_fun d t) (defun_ok d t);
 simpl ;
    let H := fresh "H'" in
           let P := fresh in
             let U := fresh "y" in
             ( intro U ;

 match goal with [ |- (?A -> ?B) -> ?C ] =>
       (assert (H : A);[try auto | intro P; generalize (P H)]) end)
  
    )
end.

Ltac defun_elim :=
 defun_elim_aux ||
   (match goal with [ |- (?P (?f ?t)) ] =>
   (let g := eval cbv beta zeta delta [f ] in f in
    (match g with (the_fun ?d) =>
    change (P (g t)) ; defun_elim_aux end)) end).

Ltac choice_defun_elim :=
 choice_defun_elim_aux ||
   (match goal with [ |- (?P (?f ?t)) ] =>
   (let g := eval cbv beta zeta delta [f ] in f in
    (match g with (some_fun ?d) =>
    change (P (g t)) ; choice_defun_elim_aux end)) end).

Ltac iota_fun_elim_aux :=
let IO := fresh "Iota" in
  match goal with
    [ |- (?Q (iota_fun (B:= ?Y) ?I ?P ?R ?t)) ] =>
        (assert (IO: iotax I);[auto
                        | generalize (iota_fun I P R t) (iota_fun_ok IO P R t);
                          simpl ;
    let H := fresh "H'" in
           let P := fresh in
             let U := fresh "y" in
               let H0 := fresh "H" in
                  let H1 := fresh "H" in
                     let H2 := fresh "H" in
                       let H3 := fresh "H" in
              (intro U; match goal with [ |- (?A -> ?B -> ?C -> ?D) -> ?G]
                              => intro H0; assert (H:C);[auto |
                                              assert (H1:A);[auto |
                                                   assert (H2 : B);[auto |
                                                       assert (H3:D);[auto|idtac]]]] end)]) end.

Ltac iota_fun_elim :=
 iota_fun_elim_aux ||
   (match goal with [ |- (?Q (?f ?t)) ] =>
   (let g := eval cbv beta zeta delta [f ] in f in
    (match g with (iota_fun ?I ?P ?R ) =>
    change (Q (g t)) ; iota_fun_elim_aux end)) end).

Ltac iota_e := the_elim || defun_elim || iota_elim || iota_fun_elim.

Ltac epsilon_e := some_elim || epsilon_elim || choice_defun_elim.

Ltac fun_define inh P R :=
  assert (d : defun P R);[(apply make_defun with inh ;auto)| exact (the_fun d)].

Hint Resolve epsilon_iota.

 
 
 

Index
This page has been generated by coqdoc