(* Pierre Casteran (with the help of Hugo Herbelin and Benjamin Werner *) (* Hilbert's epsilon *) Require Import Classical. Require Import ChoiceFacts. Require Import Compare_dec. Require Export ClassicalEpsilon. Set Implicit Arguments. Lemma ex_unique_introduction : forall (A:Type)(P:A->Prop), (exists x, P x) -> (forall a b, P a -> P b -> a = b)-> exists! x, P x. Proof. intros. case (unique_existence P). destruct 1. split;auto. case H;intros x0 Hx0. exists x0;auto. case H1. split;auto. Qed. Ltac ex_unique_intro := match goal with [ |- ex (unique ?P) ] => apply ex_unique_introduction end. (* OK from here *) Theorem epsilon_ind : forall (A:Type)(i : inhabited A)(P:A->Prop) (Q:A->Prop), (exists x, P x)-> (forall x : A, P x -> Q x) -> Q (epsilon i P). Proof. intros A a P Q exP P_Q. apply P_Q. apply epsilon_spec; assumption. Qed. Theorem epsilon_equiv : forall (A:Type)(i : inhabited A)(P:A->Prop), (exists x, P x)<-> P (epsilon i P). Proof. split. intros; apply epsilon_ind; auto. exists (epsilon i P); auto. Qed. (* Hilbert's definition of forall *) Definition tau (A:Type)(i:inhabited A)(P:A->Prop) := epsilon i (fun y => ~ (P y)). Lemma forall_def : (forall P, P \/ ~ P) -> forall (A:Type)(i:inhabited A)(P:A->Prop), (forall y, P y) <-> P (tau i P). Proof. intros class A a P; split. auto. intros H y . case (class (P y));auto. intro Hy. revert H. pattern (tau a P). unfold tau;apply epsilon_ind;auto. exists y;auto. tauto. Qed. (* Definite description operator *) (* Definition iota (A:Type)(a : A)(P: A-> Prop) : A := epsilon a (unique P). *) Definition iota (A:Type)(i : inhabited A)(P: A-> Prop) : A := epsilon i (unique P). Lemma iota_e : forall (A:Type) (i: inhabited A) (P : A -> Prop), ex (unique P) -> unique P (iota i P). Proof. intros A a P H; unfold iota. apply epsilon_ind;auto. Qed. Lemma iota_e_weak : forall (A:Type) (i: inhabited A) (P : A -> Prop), ex (unique P) -> P (iota i P). Proof. intros. case (iota_e i H). auto. Qed. Theorem iota_ind : forall (A:Type)(i: inhabited A)(P:A->Prop) (Q:A->Prop), (forall b : A, unique P b -> Q b) -> ex (unique P) -> Q (iota i P). Proof. intros A a P Q H (x,H0). apply H. apply iota_e. exists x;auto. Qed. Theorem iota_ind_weak : forall (A:Type)(i: inhabited A)(P:A->Prop) (Q:A->Prop), (forall b : A, P b -> Q b) -> ex (unique P) -> Q (iota i P). Proof. intros. apply H. apply iota_e_weak. auto. Qed. Ltac epsilon_elim_aux := match goal with [ |- (?P (epsilon (A:=?X) ?a ?Q))] => apply epsilon_ind; auto 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 ?w ?d) => change (P v); epsilon_elim_aux end)) | [ |- (?P (?k ?arg ?arg1))] => (let v := eval cbv zeta beta delta [k] in (k arg arg1) in (match v with (epsilon ?w ?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 ?w ?d) => change (P v); epsilon_elim_aux end)) end. Ltac iota_elim_aux := match goal with [ |- (?P (iota (A:=?X) ?i ?Q))] => apply iota_ind; auto 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 ?w ?d) => change (P v); iota_elim_aux end)) | [ |- (?P (?k ?arg ?arg1))] => (let v := eval cbv zeta beta delta [k] in (k arg arg1) in (match v with (iota ?w ?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 ?w ?d) => change (P v); iota_elim_aux end)) end. Lemma iota_parameter_rw : forall (A:Type)(a b:inhabited A)(P:A-> Prop), (ex (unique P)) -> iota a P = iota b P. Proof. intros. pattern (iota a P). iota_elim. pattern (iota b P). iota_elim. intros b0 H0 b1 H1. revert H;intros (x,(Hx,H')). transitivity x;auto. symmetry;auto. red in H1;decompose [and] H1. auto. red in H0;decompose [and] H0. auto. Qed. (** Structures for descriptions and specifications *) (** The operators "some" and "the" correspond to epsilon and iota applied to the proof they expect *) Definition select(A:Type)(P:A->Prop)(pi:exists x, P x) : A := proj1_sig (constructive_indefinite_description P pi). Implicit Arguments select [A P]. Definition select_the (A:Type)(P:A->Prop) (pi:exists! x, P x) : A := proj1_sig (constructive_indefinite_description (unique P) pi). Implicit Arguments select_the [A P]. Lemma select_e : forall (A:Type)(P:A->Prop)(pi:exists x, P x), P (select pi). Proof. intros. unfold select. case (constructive_indefinite_description P pi). auto. Qed. Implicit Arguments select_e [A P]. Theorem select_ind :forall (A:Type)(P Q:A->Prop) (pi:exists x, P x), (forall a, P a -> Q a) -> Q (select pi). Proof. intros. apply H ;apply select_e. Qed. Theorem select_the_e : forall (A:Type)(P:A->Prop) (pi:exists! x, P x), unique P (select_the pi). Proof. unfold select_the. intros. case (constructive_indefinite_description (unique P) pi);auto. Qed. Implicit Arguments select_the_e [A P]. Theorem select_the_ind : forall (A:Type)(P Q:A->Prop) (pi:ex (unique P)), (forall b, unique P b -> Q b) -> Q (select_the pi). Proof. intros A P Q pi H;apply H. apply select_the_e. Qed. Implicit Arguments select_the_ind [A P]. Theorem select_the_rw : forall (A:Type)(P:A->Prop) (pi:exists! x, P x) b, P b -> b= select_the pi. Proof. intros A P pi b Hb. case pi; intros x (Px,Eqx). unfold select_the. case (constructive_indefinite_description (unique P) (ex_intro (unique (fun x0 : A => P x0)) x (conj Px Eqx))). simpl;firstorder. Qed. Implicit Arguments select_the_rw [A P]. Ltac select_the_elim_aux := match goal with [ |- (?Q (select_the ?d))] => apply select_the_ind (* generalize (select_the w d) (select_the_e w d) *) end. Ltac select_the_elim := select_the_elim_aux || match goal with [ |- (?P ?k)] => (let v := eval cbv beta zeta delta [k] in k in (match v with (select_the ?d) => change (P v); select_the_elim_aux end)) end. Ltac select_elim_aux := match goal with [ |- (?P (select ?d))] => generalize (select d) (select_e d); simpl end. Ltac select_elim := select_elim_aux || match goal with [ |- (?P ?k)] => (let v := eval cbv beta zeta delta [k] in k in (match v with (select ?d) => change (P v); select_elim_aux end)) end. Ltac hilbert_e := select_the_elim || select_elim || iota_elim || epsilon_elim . Tactic Notation "epsilon_e" constr(T) "at" integer(n) := pattern T at n; hilbert_e. Tactic Notation "epsilon_e" constr(T) := pattern T ; hilbert_e. (* introduction tactics *) Ltac select_i P := refine (select (P:=P) _). Ltac select_the_i P := refine (select_the (P:=P) _). (** Building partial functions *) Definition functional(A B : Type) (R: A -> B -> Prop ) := forall x y , R x y -> forall z, R x z -> y = z. Implicit Arguments functional [A B]. Section AB_fixed. Variables A B: Type. (** description of some partial function by a Domain and a binary relation *) (* this representation is still unused : move to trash ???? *) Definition choice_fun (i : inhabited B)(DA : A->Prop)(R:A->B->Prop)(a:A):= (epsilon i (fun (b':B) => DA a /\ R a b')). Definition iota_fun (b : inhabited B)(DA : A->Prop)(R:A->B->Prop)(a:A):= (iota b (fun (b':B) => DA a /\ R a b')). Lemma choice_fun_e : forall i : inhabited B, forall (DA : A->Prop)(R:A->B->Prop)(a:A), (exists d : B, R a d) -> DA a -> R a (choice_fun i DA R a). Proof. intros. unfold choice_fun. pattern (epsilon i (fun b : B => DA a /\ R a b)). epsilon_elim. intros. case H;intuition. exists x;auto. tauto. Qed. Lemma choice_fun_ind : forall i : inhabited B, forall (P : A->Prop)(Q R:A->B->Prop)(a x:A), (exists d : B, R a d) -> a = x -> P a -> (forall b, P a -> R a b -> Q a b) -> Q x (choice_fun i P R a). Proof. intros. subst x. apply H2. auto. apply choice_fun_e;auto. Qed. (** a partial function equipped with a proof of its partial correctness *) Definition the_fun (i : inhabited B)(D : A->Prop)(R:A->B->Prop) (pi : forall a, D a -> exists! b, R a b): A -> B := fun a:A => iota i (fun (b:B) => D a /\ R a b). (** same stuff but without unicity of the result *) Definition some_fun (i : inhabited B)(D : A->Prop)(R:A->B->Prop) (pi : forall a, D a -> exists b: B, R a b) : A -> B := fun a:A => epsilon i (fun (b:B) => D a /\ R a b). Lemma iota_fun_e : forall b : inhabited B, forall (DA : A->Prop)(R:A->B->Prop)(a:A), (ex (unique (R a))) -> DA a -> unique (R a) (iota_fun b DA R a). Proof. intros. unfold iota_fun. pattern (iota b (fun b' : B => DA a /\ R a b')). iota_elim. case H;intros. case H2; auto. case H;intros. case H4;auto. case H;intros. split. auto. intros. case H6. firstorder. case H. intros x (e,u). exists x. split;auto. firstorder. Qed. Lemma iota_fun_ind : forall b : inhabited B, forall (P : A->Prop)(Q R:A->B->Prop)(a x:A), a = x -> (ex (unique (R a))) -> P a -> (forall b, P a -> unique (R a) b -> Q a b) -> Q x (iota_fun b P R a). Proof. intros. subst x. apply H2. auto. apply iota_fun_e. case H0;intros d (Hd,Hd'). exists d;auto. auto. red. auto. auto. Qed. Lemma iota_fun_rw : forall b: inhabited B, forall (P : A->Prop)(R:A->B->Prop)(a:A)(b':B), (ex (unique ( R a))) -> P a -> R a b' -> b'= (iota_fun b P R a). Proof. intros. unfold iota_fun. pattern (iota b (fun b0 : B => P a /\ R a b0)). iota_elim. case H;intros d (Hd,Hd'). intuition. transitivity d;auto. symmetry;auto. red in H2. firstorder. firstorder. Qed. Theorem the_fun_e : forall (b :inhabited B)(P: A-> Prop)(R:A->B->Prop) (pi : forall a, P a -> ex (unique (R a))) (a:A), P a -> R a (the_fun b P R pi a) . Proof. intros b P R pi a H. unfold the_fun. pattern (iota b (fun b0 : B => P a /\ R a b0)). iota_elim. case (pi a H). intros x (Hx,H'x). firstorder. firstorder. Qed. Theorem some_fun_e : forall (i : inhabited B)(P: A-> Prop)(R:A->B->Prop) (pi : forall a, P a -> exists b0: B, R a b0) (a:A), P a -> R a (some_fun i P R pi a) . Proof. intros i P R pi a H. unfold some_fun. pattern (epsilon i (fun b0 : B => P a /\ R a b0)). epsilon_elim. case (pi a H). intros x Hx. exists x. split;auto. destruct 1;auto. Qed. Theorem the_fun_rw : forall (b : inhabited B)(P: A-> Prop)(R:A->B->Prop) (pi : forall a, P a -> ex (unique ( R a))) (a:A)(b0:B), P a -> R a b0 -> b0= (the_fun b P R pi a) . Proof. intros b P R pi a b0 H H0. unfold the_fun. pattern (iota b (fun b1 : B => P a /\ R a b1)). iota_elim. firstorder. case (pi a H). intros x (Hx,H'x). exists x. firstorder. Qed. Theorem the_fun_ind : forall (b : inhabited B)(P: A-> Prop)(Q R:A->B->Prop) (pi : forall a, P a -> ex (unique (R a))) (a x:A), P a -> a = x -> (forall b0, P a -> unique (R a) b0 -> Q a b0) -> Q x (the_fun b P R pi a) . Proof. intros. subst x. apply H1. auto. case (pi a H). destruct 1. split. eapply the_fun_e. auto. intros. replace x' with x. symmetry;apply (the_fun_rw b P R pi a);auto. auto. Qed. Theorem some_fun_ind : forall (i : inhabited B)(P: A-> Prop)(Q R:A->B->Prop) (pi : forall a, P a -> exists b: B, R a b) (a x:A), a = x -> P a -> (forall b0, P a -> R a b0 -> Q a b0) -> Q x (some_fun i P R pi a) . Proof. intros. subst x. apply H1. auto. eapply some_fun_e. auto. Qed. End AB_fixed. (** tactic for building a partial function *) Opaque the_fun some_fun. Ltac the_fun_i P R:= refine (the_fun _ P R _). Ltac some_fun_i P R:= refine (some_fun _ P R _). Ltac the_fun_elim := match goal with [ |- (?Q ?a (?f ?t)) ] => (let v := eval cbv beta zeta delta [f] in f in (match v with (the_fun ?i ?P ?R ?d) => change (Q a (v t)); apply the_fun_ind ; auto end)) end. Ltac some_fun_elim := match goal with [ |- (?Q ?a (?f ?t)) ] => (let v := eval cbv beta zeta delta [f] in f in (match v with (some_fun ?i ?P ?R ?d) => change (Q a (v t)); apply some_fun_ind ; auto end)) end. Ltac iota_fun_elim := match goal with [ |- (?Q ?a (?f ?t)) ] => (let v := eval cbv beta zeta delta [f] in f in (match v with (iota_fun ?i ?P ?R ) => change (Q a (v t)); apply iota_fun_ind ; auto end)) end. Ltac choice_fun_elim := match goal with [ |- (?Q ?a (?f ?t)) ] => (let v := eval cbv beta zeta delta [f] in f in (match v with (choice_fun ?i ?P ?R ) => change (Q a (v t)); apply choice_fun_ind ; auto end)) end. Ltac pfun_e := choice_fun_elim || iota_fun_elim || some_fun_elim || the_fun_elim. Ltac partial_fun_e arg result := pattern arg, result;pfun_e. Ltac iota_fun_rewrite := match goal with [ |- (?f ?x = ?y) ] => (let v := eval cbv beta zeta delta [f] in f in (match v with (iota_fun ?i ?P ?R ) => change (v x = y);symmetry; apply iota_fun_rw; auto end)) end. Ltac the_fun_rewrite := match goal with [ |- (?f ?x = ?y) ] => (let v := eval cbv beta zeta delta [f] in f in (match v with (the_fun ?i ?P ?R ?d ) => change (v x = y);symmetry; apply the_fun_rw; auto end)) end. Section definite_description. (* from Benjamin *) (* Epsilon and definite description *) (* A quite strong version *) Lemma dd'' : forall (A:Type)(B:A->Type) (R:forall x:A, B x -> Prop), (forall x: A, inhabited (B x)) -> (sigT (fun f : forall x:A, B x => (forall x:A, (exists y:B x, R x y) -> R x (f x)))). Proof. intros A B R i. exists (fun (x:A) => (epsilon (i x) (fun y => (R x y)))). intros x [y ry]. apply (epsilon_ind). exists y; trivial. auto. Qed. (* A weaker version *) Lemma dd' : forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop), (forall x, inhabited (B x)) -> (forall x:A, exists y : B x, R x y ) -> sigT (fun f : forall x:A, B x => (forall x:A, R x (f x))). Proof. intros. case (dd'' B R H). intros. exists x. intros;apply r. auto. Qed. End definite_description. Definition epsilon_extensionality := forall (A:Type)(i: inhabited A)(P Q:A->Prop), (forall a, P a <-> Q a) -> epsilon i P = epsilon i Q. (* Theorem epsilon_ext : predicate_extensionality -> epsilon_extensionality. *) Definition restricted_epsilon_extensionality := forall (A:Type)(i: inhabited A)(P Q:A->Prop), (forall a, P a <-> Q a) -> ex P -> epsilon i P = epsilon i Q. Lemma inhabited_bool : inhabited bool. constructor. exact true. Qed. Lemma or_to_sumbool : forall P Q : Prop, P \/ Q -> {P}+{Q}. Proof. intros P Q H. pose (y := epsilon inhabited_bool (fun b => b=true /\ P \/ b=false /\ Q)). case_eq y. intro eg. left. generalize eg;pattern y; hilbert_e. case H. exists true;auto. exists false;auto. destruct 1. tauto. case H0;intros; subst x; discriminate. intro eg;right. generalize eg;pattern y; hilbert_e. case H. exists true;auto. exists false;auto. destruct 1. intro; subst x. case H0. discriminate 1. tauto. Qed. Lemma iota_rw : forall (A:Type)(a: inhabited A)(P:A->Prop)(x:A), unique P x -> iota a P = x. Proof. intros. case H ;intros H1 H2. symmetry;apply H2;auto. epsilon_e (iota a P). firstorder. exists x;firstorder. Qed. Opaque epsilon. Definition unspec (A:Type)(i:inhabited A) := epsilon i (fun x => True). Lemma quasi_classic : forall (A:Type), A + (A->False). Proof. intro A;case (or_to_sumbool (classic (inhabited A))). intro i; left;exact (epsilon i (fun a =>True)). intro H;right;intro a. case H. constructor. auto. Qed.