Skip to content

Instantly share code, notes, and snippets.

# siraben/classical-math-coq.v

Created July 11, 2021 03:32
Show Gist options
• Save siraben/19b2c77b105f02799ca29c03e7790d6b to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 (* 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.
to join this conversation on GitHub. Already have an account? Sign in to comment