The Coq mailing list

[Cristóbal Camarero Coterillo <nakacristo AT hotmail.com>]

Some time ago I found this inductive type plus axiom of injectivity that implies False with the help of dependent_unique_choice and classic.

Inductive some {T:Type} (t:T) : Type:=
|some_single: some t
|some_more: Type -> some t-> some t.

Axiom some_inj: forall (T:Type) (x y:T), some x=some y -> x=y.

I had really expected that some being a newly introduced type, it could be made injective. I mean, it is alike if two vectors are equal they must have the same dimension.

I have attached the proof of False.

Interestingly if I use

Inductive single {T:Type} (t:T) : Type:=
|single_intro: single t.
Axiom single_inj: forall (T:Type) (x y:T), single x=single y -> x=y.

then all I get is a Universe Inconsistency, which is what I would expect in both cases.

Best regards,
--Cristóbal Camarero

Require Import Classical.
Require Import ClassicalChoice.

Definition injective (A B:Type) (f:A->B) := forall (x y:A),
 @eq B (f x) (f y) -> @eq A x y.
Definition surjective (A B:Type) (f:A->B) := forall y:B,
 @ex A (fun x:A=> @eq _ (f x) y).

Inductive cardinal:Type :=
|cardinal_intro : forall (S:Type->Prop), cardinal.

Definition cardinal_le:= fun A B:Type => @ex (A->B) (fun f:A->B => injective A B f).
(*not necessary*)
(*Definition cardinal_eq:= fun A B:Type => and (cardinal_le A B) (cardinal_le B A).*)

Inductive some {T:Type} (t:T) : Type:=
|some_single: some t
|some_more: Type -> some t-> some t.

Axiom some_inj: forall (T:Type) (x y:T), some x=some y -> x=y.

(* Using
Inductive single {T:Type} (t:T) : Type:=
|single_intro: single t.
Axiom single_inj: forall (T:Type) (x y:T), single x=single y -> x=y.
would lead to an universe inconsistency
*)

(* con tipos ordenados (y algo mas) deberia poderse hacer *)
Theorem injective_into_Type: forall (T:Type), exists f:T->Type, injective T Type f.
Proof.
intros. exists some. intros x y EQ. apply some_inj. exact EQ.
Qed.

Definition func_inverse (A B:Type) (f:A->B) (g:B->A) := forall x:A, @eq A (g (f x)) x.
Definition image (A B:Type) (f:A->B) (y:B) := @ex A (fun x:A=> @eq B (f x) y).
(*Definition map (A B:Type) (f:A->B) (S:A->Prop) (y:B) := @ex A (fun x:A=> and (S x) (@eq B (f x) y)).*)

Lemma image_trivial: forall (A B:Type) (f:A->B) (x:A), image A B f (f x).
Proof.
intros. unfold image. apply ex_intro with (x:=x). apply eq_refl.
Qed.

(*
Lemma map_trivial: forall (A B:Type) (f:A->B) (S:A->Prop) (x:A), S x -> map A B f S (f x).
Proof.
intros. unfold map. apply ex_intro with (x:=x). apply conj.
exact H. apply eq_refl.
Qed.
*)


Theorem leibnitz: forall (T:Type) (x y:T), x=y ->
forall P:T->Prop, P x -> P y.
Proof.
intros. rewrite H in H0. exact H0.
Qed.

Theorem cardinal_large: forall T:Type, cardinal_le T cardinal.
Proof.
intros.
apply ex_intro with (x:=fun t:T=> cardinal_intro (fun X:Type=> eq X (some t))).
intros x y EQ.
inversion EQ.
apply f_equal with (f:=fun t=>t (some x) ) in H0.
assert(L:=leibnitz _ _ _ H0).
assert(H: some x=some x). auto.
apply L with (P:=fun x=>x) in H.
clear EQ H0 L.
apply some_inj.
exact H.
Qed.


Theorem Cantor: forall (T:Type) (f:T->(T->Prop)), surjective T (T->Prop) f -> False.
Proof.
intros T f SUR.
specialize(SUR (fun x:T=> not (f x x) )).
revert SUR. apply ex_ind.
intros.
apply f_equal with (f:=fun t=>t x) in H.
assert(C:=classic (f x x)).
assert(L:=leibnitz _ _ _ H).
apply (L (fun t=>or t _)) in C.
assert(NF: not (f x x)).
destruct C;auto.
apply NF.
rewrite H. exact NF.
Qed.

Theorem injective_unique_preimage: forall (A B:Type) (f:A->B), injective A B f->
 forall y:B, image A B f y -> @ex A (@unique A (fun x:A=> @eq B (f x) y)).
Proof.
intros. unfold image in H0. revert H0. apply ex_ind.
intros x Hxy. apply ex_intro with (x:=x).
unfold unique. apply conj. exact Hxy.
intros. apply H. apply eq_sym in Hxy. rewrite<- Hxy. rewrite H0. apply eq_refl.
Qed.

Theorem injective_inverse: forall (A B:Type) (f:A->B) (dummy:A), injective A B f ->
 @ex (B->A) (fun g:B->A=> and (surjective B A g) (func_inverse A B f g) ).
Proof.
(* see https://proofwiki.org/wiki/Injection_has_Surjective_Left_Inverse_Mapping/Proof_1 *)
intros.
set(R:=fun (y:B) (x:A) => and (image A B f y -> @eq B (f x) y ) (not (image A B f y)->@eq A x dummy)).
assert(UC:=unique_choice B A R).
rename H into INJ.

assert(PRE:(forall x : B, @ex A (@unique A (fun y : A => R x y)))).
intros y. unfold R.
assert(IUP:=injective_unique_preimage A B f INJ y).
assert(C:=classic (image A B f y)).
revert C. apply or_ind.
intros IMAG. specialize(IUP IMAG). revert IUP. apply ex_ind.
intros x. unfold unique. apply and_rect. intros Hxy Huniquex.
apply ex_intro with (x:=x). apply conj. apply conj.
intros. exact Hxy.
intros. apply False_rect. apply H. exact IMAG.
intros x'. apply and_rect. intros. apply Huniquex. apply H. exact IMAG.
intros NIMAG. apply ex_intro with (x:=dummy).
unfold unique. apply conj. apply conj.
intros. apply False_rect. apply NIMAG. exact H.
intros. apply eq_refl.
intros x. apply and_rect. intros. apply eq_sym. apply H0. exact NIMAG.

specialize(UC PRE).
revert UC. apply ex_ind. intros g Hg.
apply ex_intro with (x:=g). apply conj.
- unfold surjective. intros x. apply ex_intro with (x:=f x).
unfold R in Hg. specialize(Hg (f x)). revert Hg. apply and_rect. intros.
apply INJ. apply H. apply image_trivial.
- unfold func_inverse. intros. unfold R in Hg. specialize(Hg (f x)).
revert Hg. apply and_rect. intros. apply INJ. apply H. apply image_trivial.
Qed.


Theorem bad: False.
Proof.
assert(H:=cardinal_large (cardinal->Prop)). destruct H as [f INJ].
assert(X:=injective_inverse _ _ f (fun x=>True) INJ).
destruct X as [g [SUR INV]].
apply Cantor with (f:=g).
exact SUR.
Qed.

Print Assumptions bad.