Skip to content

Instantly share code, notes, and snippets.

@pedrominicz
Last active April 9, 2020 02:20
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save pedrominicz/0d9004b82713d9244b762eb250b9c808 to your computer and use it in GitHub Desktop.
Save pedrominicz/0d9004b82713d9244b762eb250b9c808 to your computer and use it in GitHub Desktop.
Injection, surjection, and inverses in Coq.
(* https://www.reddit.com/r/logic/comments/fxjypn/what_is_not_constructive_in_this_proof/ *)
Definition injective {A B} (f : A -> B) := forall a1 a2, f a1 = f a2 -> a1 = a2.
Definition injective' {A B} (f : A -> B) := forall a1 a2, a1 <> a2 -> f a1 <> f a2.
Theorem injective_injective' : forall {A B} (f : A -> B),
injective f -> injective' f.
Proof. unfold injective, injective'. auto. Qed.
(*
`eq_dec` is derivable for any _pure_ algebraic data type, that is, for any
algebraic data type that do not containt any functions. For such data types an
`eq_dec` proof could be automatically derived by, for example, a machanism
similar to Haskell's `deriving`.
Given functional extensionality, `eq_dec` is derivable for functions with
finite domain and undecidable otherwise.
*)
Definition eq_dec A := forall (a1 a2 : A), a1 = a2 \/ a1 <> a2.
Lemma False_eq_dec : eq_dec False.
Proof. unfold eq_dec. contradiction. Qed.
Lemma nat_eq_dec : eq_dec nat.
Proof.
unfold eq_dec.
induction a1; destruct a2; auto.
destruct (IHa1 a2); auto using f_equal.
Qed.
Theorem injective'_injective : forall {A B} (f : A -> B),
eq_dec A -> injective' f -> injective f.
Proof.
unfold injective, injective', not.
intros A B f dec H a1 a2 eq.
destruct (dec a1 a2).
- assumption.
- exfalso. apply (H a1 a2); assumption.
Qed.
Definition surjective {A B} (f : A -> B) := forall b, exists a, f a = b.
Definition bijective {A B} (f : A -> B) := injective f /\ surjective f.
Definition left_inverse {A B} (f : A -> B) g := forall a, g (f a) = a.
Definition right_inverse {A B} (f : A -> B) g := forall b, f (g b) = b.
Definition inverse {A B} (f : A -> B) g := left_inverse f g /\ right_inverse f g.
Theorem left_inverse_injective : forall {A B} (f : A -> B),
(exists g, left_inverse f g) -> injective f.
Proof.
unfold injective, left_inverse.
intros A B f [g H] a1 a2 eq.
apply f_equal with (f := g) in eq.
repeat rewrite H in eq.
assumption.
Qed.
(*
`im_dec` is automatically derivable for functions with finite domain.
*)
Definition im_dec {A} {B} (f : A -> B) := forall b, { a | f a = b } + ~(exists a, f a = b).
Lemma not_im_dec : forall {A} (P : ~A), im_dec P.
Proof. constructor. contradiction. Qed.
Theorem injective_left_inverse : forall {A B} (a : A) (f : A -> B),
im_dec f -> injective f -> exists g, left_inverse f g.
Proof.
unfold injective, left_inverse.
intros A B a f dec H.
exists (fun b => match dec b with inl (exist _ a _) => a | inr _ => a end).
intros a'.
destruct (dec (f a')).
- destruct s. auto.
- exfalso. apply n. exists a'. reflexivity.
Qed.
Theorem right_inverse_surjective : forall {A B} (f : A -> B),
(exists g, right_inverse f g) -> surjective f.
Proof.
unfold right_inverse, surjective.
intros A B f [g H] b.
exists (g b).
apply H.
Qed.
Theorem surjective_right_inverse : forall {A B} (f : A -> B),
(forall b, { a | f a = b }) -> exists g, right_inverse f g.
Proof.
unfold right_inverse, surjective.
intros A B f g.
exists (fun b => proj1_sig (g b)).
intros.
destruct (g b) as [a H].
assumption.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment