```
Require Import Utf8 Lia.
Set Implicit Arguments.
Definition fin n := { i | i < n }.
Definition bijection A B := ∃ (f: A → B) (g: B → A), (∀ x, g (f x) = x) ∧ (∀ y, f (g y) = y).
Theorem bijection_between_fins n m: bijection (fin n) (fin m) → n = m.
Proof.
Admitted.
```

How to prove the theorem? Any suggestions?

My approach was such that I reached situation with hypothesis `bijection (S n) (S m)`

and goal `bijection n m`

, but I got lost when I tried to destruct the first bijection and define explicit functions `f`

and `g`

for the second (probably because I'm muddle headed).

For now my try is unsuccesful. Even if it would work the potential result is going to be something disgusting...

Is there some different way to define bijection between types, maybe?

from `f : fin (S n) -> fin (S m)`

first try to define `f_ : fin n -> nat`

, to be used as the first component of the eventual function `f' : fin n -> fin m`

.

I agree with @zaa, a direct proof seems nasty: you'd have to reorder the range of `f`

appropriately.

stdpp has a proof of this theorem that seems to bypass this step altogether: https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/finite.v#L152-153.

I haven't studied the proof in detail, but here's an idea (which might relate to what is going on): trychotomy lets you decide whether `n < m`

, `n = m`

or `m < n`

; if `n = m`

we're done, else we can proceed by contradiction. `bijection`

is symmetric (exercise), so without loss of generality we can focus on `n < m -> bijection (fin n) (fin m) -> False`

.

OTOH, what's left is essentially a variant of the pigeonhole theorem (also available in that file, and left as an exercise in https://softwarefoundations.cis.upenn.edu/lf-current/IndProp.html with a different formulation)

On top of rearranging the range, you’d also have to prove that two subset types are equal (in the section/retraction equations), which is quite a lot of pain! Although in this case you should be lucky because I think you can prove that `n < m`

has at most one proof.

Thank you! I will go study the proof of stdpp.

@Meven Lennon-Bertrand ah, you mean the elements of subset types are equal

I agree, but that’s a lemma you want anyway to use this `fin`

, IMHO.

I think it’s true as you say, but if it isn’t, you can always turn to `Nat.ltb i n = true`

or similar constructions (in stdpp we write `bool_decide (i < n) = true`

); proof irrelevance there is provable. But I haven’t learned these tricks from, say, software foundations.

foo.v

here is a 150 line + stdlib proof

considering stdpp uses

```
Class Finite A `{EqDecision A} := {
enum : list A;
(* [NoDup] makes it easy to define the cardinality of the type. *)
NoDup_enum : NoDup enum;
elem_of_enum x : x ∈ enum
}.
```

its proof is probably similar but less adhoc

Bas Spitters has marked this topic as resolved.

Bas Spitters has marked this topic as unresolved.

Gaëtan Gilbert said:

here is a 150 line + stdlib proof

But it’s a proof for `Fin.t`

, right? This is likely easier than `fin`

defined as a subset type? But indeed you probably want to use that finite type rather than the subset one, if possible

not especially hard to go between

```
Definition fin n := { i | i < n }.
Lemma fin_fin'_bij n : @Bijective (Fin.t n) (fin n) (@to_nat n).
Proof.
exists (fun x:fin n => of_nat_lt (proj2_sig x)).
split.
- apply of_nat_to_nat_inv.
- intros x. rewrite to_nat_of_nat. destruct x;reflexivity.
Qed.
```

@Meven Lennon-Bertrand mathcomp uses a subset type to replace `vector`

, why not for `fin`

?

yet another "first-order" `fin`

encoding: https://github.com/uwplse/StructTact/blob/master/theories/Fin.v

Hm, I guess the argument for subset types is that you get to reuse the theory on the base type + arbitrary tactics to solve the obligations...

zaa has marked this topic as resolved.

zaa has marked this topic as unresolved.

Once again, big thank you for your answers, especially Gaëtan Gilbert.

Anyway, the nasty way of proving the theorem (which still fascinates me but I can't make to work) is messing with my brain and making me very frustrated. :\ :D Is there some way to put the bounty on direct proof (the nasty one) of the following theorem? I have more important things (studies, exam tomorrow etc.) to do for now and I'm ready to pay some money for the proof. I really hope this isn't impolite or smth.

(Proof irrelevance for `le`

can be assumed without proof because it can be found on the internet, I believe. And there's the "transparent assert" tactic, which could be useful: `Tactic Notation "transparent" "assert" "(" ident(H) ":" open_constr(type) ")" := refine (let H := (_: type) in _).`

I have forgotten where I have found this one, but it was Internet too. )

```
Require Import Utf8 Lia.
Set Implicit Arguments.
Definition fin n := { i | i < n }.
Definition bijection A B := ∃ (f: A → B) (g: B → A), (∀ x, g (f x) = x) ∧ (∀ y, f (g y) = y).
Theorem bijection_between_fins_aux n m: bijection (fin (S n)) (fin (S m)) → bijection (fin n) (fin m).
Proof.
Admitted.
```

(with `Notation "X <~> Y" := (bijection X Y)`

)

it should be easy to prove `(fin (S n)) <~> option (fin n)`

the problem then reduces to `(option A <~> option B) -> A <~> B`

which came up on coq club a while ago

I don't remember if a proof ever got posted

we could even generalize further to `((A + B) <~> (A + C)) -> B <~> C`

(with `option A <~> unit + A`

)

EDIT actually that only works with finite A so the option theorem is more primitive

I am two tiny `admit`

s away from proving the theorem with the direct/nasty approach and hope to finish before falling asleep. If I'm successful this night, I will post cleared up version of the proof tomorrow evening.

It's done... now clearing up the unholy mess.

```
Require Import Utf8 Lia Arith.
Set Implicit Arguments.
Definition fin n := { i | i < n }.
Definition bijection A B := ∃ (f: A → B) (g: B → A), (∀ x, g (f x) = x) ∧ (∀ y, f (g y) = y).
Theorem le_PI n m (A B: le n m): A = B.
Proof.
Admitted.
Coercion fin_proj1 n (f: fin n) := proj1_sig f.
Theorem fin_aux n (f1 f2: fin n): fin_proj1 f1 = fin_proj1 f2 → f1 = f2.
Proof.
intros. destruct f1, f2. simpl in *. subst. f_equal. apply le_PI.
Qed.
Tactic Notation "transparent" "assert" "(" ident(H) ":" open_constr(type) ")" :=
refine (let H := (_: type) in _).
Theorem bijection_between_fins_aux n m: bijection (fin (S n)) (fin (S m)) → bijection (fin n) (fin m).
Proof.
intros [f [g [H H0]]].
transparent assert (f0:(fin n → fin m)). Unshelve.
2:{ intros [x Hx]. assert (x < S n) by auto. assert (n < S n) by auto.
exists (if le_lt_dec (f (exist _ n H2)) (f (exist _ x H1))
then f (exist _ x H1) - 1
else f (exist _ x H1)).
destruct le_lt_dec.
+ abstract (
remember (f (exist _ x H1)) as W; remember (f (exist _ n H2)) as W0;
destruct W, W0; simpl in *;
assert (x0 ≠ 0) by (
intro; subst; assert (x1 = 0) by abstract lia; subst; clear l;
assert (l0 = l1) by apply le_PI; subst;
rewrite HeqW in HeqW0; assert (x ≠ n) by abstract lia;
assert (exist (λ i, i < S n) x H1 ≠ exist _ n H2) by (intro; apply H3; inversion H4; auto);
assert (f (exist _ x H1) ≠ f (exist _ n H2)) by (intro; apply H4; rewrite <- H; rewrite <- H at 1; f_equal; auto);
auto);
abstract lia).
+ abstract (destruct (f (exist _ x H1)), (f (exist _ n _)); simpl in *; abstract lia). }
transparent assert (g0:(fin m → fin n)). Unshelve.
2:{ clear f0. intros [x Hx]. assert (x < S m) by auto.
assert (n < S n) by auto. assert (S x < S m) by intuition.
exists (if le_lt_dec (f (exist _ n H2)) x
then g (exist _ (S x) H3)
else g (exist _ x H1)).
destruct le_lt_dec.
+ abstract (
assert (g (exist _ (S x) H3) ≠ exist _ n H2) by (intro; rewrite <- H4, H0 in l; simpl in l; abstract lia);
assert (fin_proj1 (g (exist _ (S x) H3)) ≠ n) by (intro; apply H4; apply fin_aux; simpl; auto);
assert (fin_proj1 (g (exist _ (S x) H3)) < S n) by (destruct (g (exist _ _ _)); simpl; auto);
abstract lia).
+ abstract (
assert (g (exist _ x H1) ≠ exist _ n H2) by (intro; rewrite <- H4, H0 in l; simpl in l; abstract lia);
assert (fin_proj1 (g (exist _ x H1)) ≠ n) by (intro; apply H4; apply fin_aux; simpl; rewrite <- H5; auto);
assert (fin_proj1 (g (exist _ x H1)) < S n) by (destruct (g (exist _ _ _)); simpl; auto);
abstract lia). }
exists f0, g0; unfold f0, g0; clear f0 g0. split; intros.
* destruct x. apply fin_aux. simpl. repeat destruct le_lt_dec.
++ assert (let w := fin_proj1 (f (exist _ x (le_S (S x) n l))) in w = 0 ∨ w > 0) by abstract lia.
destruct H1.
** rewrite H1 in l0. assert (fin_proj1 (f (exist _ n (le_n (S n)))) = 0) by abstract lia.
assert (f (exist (λ i, i < S n) x (le_S (S x) n l)) = f (exist _ n (le_n (S n)))).
{ assert (0 < S m) by abstract lia.
assert (f (exist _ x (le_S (S x) n l)) = exist _ 0 H3).
{ apply fin_aux. rewrite H1. auto. }
assert (f (exist _ n (le_n (S n))) = exist _ 0 H3).
{ apply fin_aux. rewrite H2. auto. }
congruence. }
assert (x = n).
{ assert (exist (λ i, i < S n) x (le_S (S x) n l) = exist _ n (le_n (S n))).
{ rewrite <- H. rewrite <- H at 1. f_equal. auto. }
inversion H4. auto. }
abstract lia.
** assert (S (f (exist _ x (le_S (S x) n l)) - 1) = f (exist _ x (le_S (S x) n l))) by abstract lia.
assert (∀ (w: fin (S n)) (H: f w > 0) (H0: S (f w - 1) < S m), g (exist _ (S (f w - 1)) H0) = w).
{ intros. assert (S (fin_proj1 (f w) - 1) = fin_proj1 (f w)) by abstract lia.
rewrite <- (H w). f_equal. apply fin_aux. simpl. auto. }
rewrite H3. auto. auto.
++ exfalso. assert (fin_proj1 (f (exist _ x (le_S (S x) n l))) = fin_proj1 (f (exist _ n (le_n (S n))))) by abstract lia.
assert (f (exist _ x (le_S (S x) n l)) = f (exist _ n (le_n (S n)))).
{ apply fin_aux. auto. }
assert (exist (λ i, i < S n) x (le_S (S x) n l) = exist _ n (le_n (S n))).
{ rewrite <- H. rewrite <- H at 1. f_equal. auto. }
inversion H3. abstract lia.
++ exfalso. assert (fin_proj1 (f (exist _ n (le_n (S n)))) = fin_proj1 (f (exist _ x (le_S (S x) n l)))) by abstract lia.
assert (f (exist _ n (le_n (S n))) = f (exist _ x (le_S (S x) n l))).
{ apply fin_aux; auto. }
assert (exist (λ i, i < S n) n (le_n (S n)) = exist _ x (le_S (S x) n l)).
{ rewrite <- H. rewrite <- H at 1. f_equal. auto. }
inversion H3. abstract lia.
++ clear l0. assert (∀ (w: fin (S n)) (H: fin_proj1 (f w) < S m), g (exist _ (fin_proj1 (f w)) H) = w).
{ intros. rewrite <- H. f_equal. apply fin_aux. simpl. auto. }
rewrite H1. simpl. auto.
* assert (∀ (w: fin (S m)) (H: fin_proj1 (g w) < S n), f (exist _ (fin_proj1 (g w)) H) = w).
{ intros. rewrite <- H0. f_equal. apply fin_aux. simpl. auto. }
destruct y. apply fin_aux. simpl. repeat destruct le_lt_dec.
++ rewrite H1. simpl. abstract lia.
++ exfalso. rewrite H1 in l0. simpl in l0. abstract lia.
++ exfalso. rewrite H1 in l0. simpl in l0. abstract lia.
++ rewrite H1. simpl. auto.
Qed.
Theorem bijection_between_fins n m: bijection (fin n) (fin m) → n = m.
Proof.
revert n. induction m.
+ intros n [f [g [H H0]]]. destruct n; auto. exfalso. destruct (f (exist _ n (le_n (S n)))). abstract lia.
+ destruct n.
- intros [f [g [H H0]]]. destruct (g (exist _ m (le_n (S m)))). abstract lia.
- intros. f_equal. apply IHm. apply (bijection_between_fins_aux H).
Qed.
```

Now I can sleep peacefully. Will buy myself an ice-cream tomorrow, probably.

zaa has marked this topic as resolved.

Proof of `(option A <~> option B) -> A <~> B`

if anyone needs one

```
Definition option_get {A} (o:option A) (H:o <> None) : A.
Proof.
destruct o;auto.
exfalso. apply H;reflexivity.
Defined.
Lemma option_get_ok {A} (x:A) o (H:o=Some x) H' : option_get o H' = x.
Proof.
unfold option_get.
destruct o;congruence.
Qed.
Lemma option_get_carac {A} o H : o = Some (@option_get A o H).
Proof.
unfold option_get.
destruct o;congruence.
Qed.
Module IsMap.
Section S.
Context {A B} (f:option A -> option B) g (Hfg:forall y, f (g y) = y) (Hgf:forall x, g (f x) = x).
Hypothesis fNone : f None = None.
Lemma gNone : g None = None.
Proof.
congruence.
Qed.
Lemma fSome x : f (Some x) <> None.
Proof.
congruence.
Qed.
Lemma gSome y : g (Some y) <> None.
Proof.
congruence.
Qed.
Definition F (x:A) : B := option_get _ (fSome x).
(* this produces
match f (Some x) as o return (o <> None -> B) with
| Some a => fun _ : Some a <> None => a
| None => fun H : None <> None => False_rect B (H eq_refl)
end (fSome x)
we may be tempted instead to do
match f (Some x) as o return (f (Some x) = o -> B) with
| Some a => fun _ : f (Some x) = Some a => a
| None => fun H : f (Some x) = None => False_rect B (fSome H)
end eq_refl
however I cannnot find a way to prove anything about the later for abstract f
(trying to destruct (f (Some x)) while that match appears in the goal fails)
*)
Definition G (y:B) : A := option_get _ (gSome y).
Lemma F_carac x y (H:f (Some x) = Some y) : F x = y.
Proof.
unfold F.
apply option_get_ok.
exact H.
Qed.
Lemma G_carac y x (H:g (Some y) = Some x) : G y = x.
Proof.
unfold G.
apply option_get_ok.
exact H.
Qed.
Lemma FG y : F (G y) = y.
Proof.
destruct (g (Some y)) as [x|] eqn:Hgy;try congruence.
destruct (f (Some x)) as [y'|] eqn:Hfx;try congruence.
rewrite (G_carac _ _ Hgy),(F_carac _ _ Hfx).
congruence.
Qed.
Lemma GF x : G (F x) = x.
Proof.
destruct (f (Some x)) as [y|] eqn:Hfx;try congruence.
destruct (g (Some y)) as [x'|] eqn:Hgy;try congruence.
rewrite (F_carac _ _ Hfx),(G_carac _ _ Hgy).
congruence.
Qed.
Lemma f_carac x : f x = option_map F x.
Proof.
destruct x as [x|];simpl;auto.
destruct (f (Some x)) as [y|] eqn:Hfx;try congruence.
f_equal;symmetry.
apply F_carac;assumption.
Qed.
Lemma g_carac y : g y = option_map G y.
Proof.
destruct y as [y|];simpl;try apply gNone.
destruct (g (Some y)) as [x|] eqn:Hgy;try congruence.
f_equal;symmetry.
apply G_carac;assumption.
Qed.
End S.
End IsMap.
Module IsSwap.
Section S.
Context {A B} (f:option A -> option B) g (Hfg:forall y, f (g y) = y) (Hgf:forall x, g (f x) = x).
Hypothesis (fNone:f None <> None).
Definition yNone := option_get _ fNone.
Lemma gNone : g None <> None.
Proof.
congruence.
Qed.
Definition xNone := option_get _ gNone.
Definition F (x:A) : B :=
match f (Some x) with
| Some y => y
| None => yNone
end.
Definition G (y:B) : A :=
match g (Some y) with
| Some x => x
| None => xNone
end.
Lemma f_xNone : f (Some xNone) = None.
Proof.
unfold xNone.
rewrite <-option_get_carac;congruence.
Qed.
Lemma g_yNone : g (Some yNone) = None.
Proof.
unfold yNone.
rewrite <-option_get_carac;congruence.
Qed.
Lemma F_xNone : F xNone = yNone.
Proof.
unfold F.
rewrite f_xNone.
reflexivity.
Qed.
Lemma G_yNone : G yNone = xNone.
Proof.
unfold G.
rewrite g_yNone.
reflexivity.
Qed.
Lemma FG y : F (G y) = y.
Proof.
unfold G.
destruct (g (Some y)) as [x|] eqn:Hgy.
- unfold F.
destruct (f (Some x)) as [y'|] eqn:Hfx;congruence.
- rewrite F_xNone.
pose proof (option_get_carac _ fNone).
unfold yNone. congruence.
Qed.
Lemma GF x : G (F x) = x.
Proof.
unfold F.
destruct (f (Some x)) as [y|] eqn:Hfx.
- unfold G.
destruct (g (Some y)) as [x'|] eqn:Hgy;congruence.
- rewrite G_yNone.
pose proof (option_get_carac _ gNone).
unfold xNone. congruence.
Qed.
End S.
End IsSwap.
Section S.
Context {A B} (f:option A -> option B) g (Hfg:forall y, f (g y) = y) (Hgf:forall x, g (f x) = x).
Definition fNone : {f None = None} + {f None <> None}.
Proof.
destruct (f None);constructor;congruence.
Defined.
Definition F := match fNone with left H => IsMap.F f g Hgf H | right H => IsSwap.F f H end.
Definition G := match fNone with left H => IsMap.G f g Hfg H | right H => IsSwap.G f g Hfg H end.
Lemma FG y : F (G y) = y.
Proof.
unfold F,G;destruct fNone.
- apply IsMap.FG.
- apply IsSwap.FG.
Qed.
Lemma GF x : G (F x) = x.
Proof.
unfold F,G;destruct fNone.
- apply IsMap.GF.
- apply IsSwap.GF.
(* Hgf doesn't appear in the goal but is needed by IsSwap.GF
(because IsSwap.F and G have asymetric variable usage) *)
exact Hgf.
Qed.
End S.
```

Last updated: Jan 28 2023 at 06:30 UTC