Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
(* https://coq-math-problems.github.io/Problem4/ *)
Definition inj {X Y} (f : X -> Y) := forall x x', f x = f x' -> x = x'.
Definition surj {X Y} (f : X -> Y) := forall y, {x : X | f x = y}.
Definition left_inv {X Y} (g : Y -> X) (f : X -> Y) := forall x, g (f x) = x.
Definition right_inv {X Y} (g : Y -> X) (f : X -> Y) := left_inv f g.
Fixpoint Fin (n : nat) : Set :=
match n with
| 0 => Empty_set
| S m => unit + Fin m
end.
Definition narrow {n} (f : Fin (S n) -> Fin (S n)) : Fin n -> Fin n :=
fun x => match f (inr x) with
| inl _ => match f (inl tt) with
| inl _ => (match n as n0 return (Fin n0 -> Fin n0) with
| 0 => fun x0 => x0
| S n0 => fun _ => inl tt
end) x
| inr ftt => ftt
end
| inr fx => fx
end.
Ltac immediate_x :=
match goal with H : ?f ?x = ?y |- {x | ?f x = ?y } => eexists; apply H end.
Ltac solve_using_injectivity :=
match goal with
H1 : ?f _ = ?y, H2 : ?f _ = ?y, finj : inj ?f |- _ =>
specialize (finj _ _ (eq_trans H1 (eq_sym H2))); congruence
end.
Tactic Notation "destruct_fin" constr(x) := destruct x as [[] |] eqn:?.
Tactic Notation "destruct_fin" constr(x) "as" ident(a) := destruct x as [[] | a] eqn:?.
Ltac simpl_all_matches_with :=
try (match goal with
| _ : context [match ?f ?X with | inl _ => _ | inr _ => _ end] |- _ =>
destruct_fin (f X); subst
| |- context [match ?f ?X with | inl _ => _ | inr _ => _ end] =>
destruct_fin (f X); subst
end; simpl_all_matches_with).
Ltac solve_it :=
try immediate_x;
unfold narrow in *; fold Fin in *;
simpl_all_matches_with; try immediate_x; try solve_using_injectivity.
Lemma narrow_inj {n} (f : Fin (S n) -> Fin (S n)) (finj : inj f) :
inj (narrow f).
Proof. intros x x' En. solve_it. Qed.
Theorem inj_implies_surj {n} {f : Fin n -> Fin n} : inj f -> surj f.
Proof.
intros finj y.
induction n.
- contradiction y.
- specialize (IHn (narrow f) (narrow_inj f finj)).
destruct_fin y as y'; [| specialize (IHn y') as [x En]].
+ destruct_fin (f (inl tt)) as fl; [| specialize (IHn fl) as [? ?]]; solve_it.
+ solve_it.
Qed.
Definition inv {X Y} (f : X -> Y) (fsurj : surj f) :
{g : Y -> X & inj g & right_inv g f}.
exists (fun y => let (x, _) := fsurj y in x).
- intros y y' ?; destruct (fsurj y), (fsurj y'); congruence.
- intros x; now destruct (fsurj x).
Defined.
Lemma right_inv_inj {X Y} {f : X -> Y} {g : Y -> X} :
right_inv g f -> inj g.
Proof. intros rinv y y' Hg. rewrite <-(rinv y), <-(rinv y'). now f_equal. Qed.
Lemma surj_left_inv {X Y} {f : X -> Y} {g : Y -> X} :
surj f -> left_inv g f -> right_inv g f.
Proof. intros fsurj glinv y. destruct (fsurj y); subst. now f_equal. Qed.
Theorem surj_implies_inj {n} {f : Fin n -> Fin n} (fsurj : surj f) : inj f.
Proof.
destruct (inv f fsurj) as [g ginj flinv]; unfold right_inv in flinv.
exact (right_inv_inj (surj_left_inv (inj_implies_surj ginj) flinv)).
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment