Skip to content

Instantly share code, notes, and snippets.

@siraben
Created July 11, 2021 03:32
Show Gist options
  • Save siraben/19b2c77b105f02799ca29c03e7790d6b to your computer and use it in GitHub Desktop.
Save siraben/19b2c77b105f02799ca29c03e7790d6b to your computer and use it in GitHub Desktop.
(* Coq code for https://siraben.github.io/2021/06/27/classical-math-coq.html *)
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.
Module NaiveInjective.
Definition injective {A B} (f : A -> B) :=
forall a' a'', a' <> a'' -> f a' <> f a''.
Section FirstAttempt.
Lemma P_2_1 {A B} (f : A -> B) (s : A) :
(exists g, left_inverse f g) <-> injective f.
Proof.
unfold left_inverse, injective.
split; intros H.
- intros a' a'' eq. destruct H as [g Hg].
congruence.
-
Abort.
End FirstAttempt.
Section ImageDecidable.
(* Property of decidability of being in the image *)
Definition im_dec {A} {B} (f : A -> B) :=
forall b, { a | f a = b } + ~ (exists a, f a = b).
(* If being in the image of an injective function f is decidable, it
has a left inverse. *)
Lemma injective_left_inverse {A B} (s : A) (f : A -> B) :
im_dec f -> injective f -> { g | left_inverse f g }.
Proof.
unfold im_dec, injective; intros dec inj.
exists (fun b => match dec b with inl (exist _ a _) => a | inr _ => s end).
intros a'; destruct (dec (f a')) as [[a Ha] | contra].
Abort.
End ImageDecidable.
End NaiveInjective.
Section GeneralizedInjective.
(* New definition of injective *)
Definition injective {A B} (f : A -> B) :=
forall a' a'', f a' = f a'' -> a' = a''.
(* Book's definition *)
Definition injective' {A B} (f : A -> B) :=
forall a' a'', a' <> a'' -> f a' <> f a''.
(* Property of decidability of being in the image *)
Definition im_dec {A} {B} (f : A -> B) :=
forall b, { a | f a = b } + ~ (exists a, f a = b).
(* injective generalizes injective' *)
Theorem injective_injective' : forall {A B} (f : A -> B),
injective f -> injective' f.
Proof. cbv; auto. Qed.
Lemma injective_left_inverse {A B} (s : A) (f : A -> B) :
im_dec f -> injective f -> { g | left_inverse f g }.
Proof.
unfold injective, left_inverse, im_dec.
intros dec inj.
(* It's decidable to check if b is in the image or not *)
exists (fun b => match dec b with inl (exist _ a _) => a | inr _ => s end).
intros a'.
destruct (dec (f a')) as [[a Ha] | contra].
- apply inj; auto.
- exfalso. apply contra. exists a'; auto.
Defined.
Section ComputationalContent.
Definition eq_dec A := forall (a1 a2 : A), a1 = a2 \/ a1 <> a2.
Lemma nat_eq_dec : eq_dec nat.
Proof.
unfold eq_dec.
induction a1; destruct a2; auto.
destruct (IHa1 a2); auto using f_equal.
Qed.
Definition succ (n : nat) := S n.
Definition pred' : nat -> nat.
Proof.
refine (fun n => _ (injective_left_inverse 0 succ _ _)).
- intros H. destruct H as [g Hg]. exact (g n).
- unfold im_dec.
induction b.
+ right. intros H. destruct H; discriminate.
+ left. refine (exist _ b _). reflexivity.
- unfold injective. intros a' a'' H. inversion H; auto.
Defined.
Eval compute in (pred' 1000). (* => 999 *)
(* Exercise (3 stars)
Define `double n = n + n` and derive its left-inverse in a similar
manner. You'll need to prove that being in the image of `double` is
decidable and that it's injective.
*)
End ComputationalContent.
Section NaiveImpliesLEM.
Require Import ProofIrrelevance.
Lemma inj_left_inverse_implies_lem :
(forall {A B} (f : A -> B), A -> injective f -> exists g, left_inverse f g)
-> (forall (P : Prop), P \/ ~ P).
Proof.
unfold left_inverse. intros H P.
set (f := fun a : P + True => match a with | inl _ => inl I | inr _ => inr I end).
pose proof (H _ _ f (inr I)).
assert (Hf : injective f).
{
unfold injective; intros.
destruct a', a''; try discriminate.
- f_equal. apply proof_irrelevance.
- destruct t, t0. reflexivity.
}
specialize (H0 Hf).
destruct H0 as [g Hg].
destruct (g (inl I)) eqn:E; auto. right.
intros a. destruct t.
replace (inl I) with (f (inl a)) in E by auto.
rewrite Hg in E. inversion E.
Qed.
End NaiveImpliesLEM.
End GeneralizedInjective.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment