Coq code for https://siraben.github.io/2021/06/27/classical-math-coq.html

classical-math-coq.v

(* 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.