# Compute a bijection (A <~> B) from a bijection (option A <~> option B)

This is a self-contained puzzle that came up while formalizing some combinatorics.

Take an invertible function `f : option A -> option B`, its inverse `f'`, and the assumptions formalizing that they’re inverses.

Problem: Construct a bijection between `A` and `B`.

``````Section PUZZLE.

Context {A B : Type}.
Context (f : option A -> option B).
Context (f' : option B -> option A).
Context (f'f : forall oa, f' (f oa) = oa).
Context (ff' : forall ob, f (f' ob) = ob).

Definition g : A -> B.

Definition g' : B -> A.

Lemma g'g : forall a, g' (g a) = a.

Lemma gg' : forall a, g (g' a) = a.

End PUZZLE.
``````

Defining some plausible candidates for `g` and `g'` isn’t too hard using dependent types, but I can’t seem to prove the lemmas. My attempt is below.

Is it provable? Would it work better with different definitions?

``````(* What I have so far. *)
Section PUZZLE.

Context {A B : Type}.
Context (f : option A -> option B).
Context (f' : option B -> option A).
Context (f'f : forall a, f' (f a) = a).
Context (a : A).

(* The two directions are symmetric, so we will define one and close the section to generalize it and get the other way for free. *)

Section CONTRA.

Context (fSome : f' None = Some a).
Context (fNone : f' None = None).

Definition swap_contra : False :=
match fSome in eq _ r return (r = None -> False) -> False with
| eq_refl => fun k => k fNone
end (fun fNone' =>
match fNone' in eq _ r return
match r with
| None => _
| Some _ => True
end
with
| eq_refl => I
end).

End CONTRA.

Definition swap : B :=
match f (Some a) as x return f' x = Some a -> B with
| Some b => fun _ => b
| None => fun fSome =>
match f None as x return f' x = None -> B with
| Some b => fun _ => b
| None => fun fNone => match swap_contra fSome fNone with end
end (f'f None)
end (f'f (Some a)).

End PUZZLE.

Lemma inv_swap :
forall A B (f : option A -> option B) (f' : option B -> option A)
(f'f : forall a, f' (f a) = a)
(ff' : forall b, f (f' b) = b)
(a : A),
swap f' f ff' (swap f f' f'f a) = a.
Proof.
intros. unfold swap at 1.
(* Here I would like to destruct but it's not allowed, for dependently typed reasons. *)
``````
2 Likes

I would do it as follows:

1. if `f None = None` then the result follows because `f` itself induces a bijection `A -> B`.
2. In general, prove that for any `x : option A` there is a bijection `h : option A -> option B` such that `h x = None` (for example, the function that is the identity everywhere, except that it swaps `x` and `None`).
3. Take `h` as in 2) so that `h (f None) = None`, then `hf None = None` and by 1) it follows that it induces the desired bijection.

Cheers,
Nicolás

(sorry if perhaps your question is more subtle – I don’t yet understand dependent types very well) Very nice puzzle! You can solve it by making the definition slightly less dependent:

``````Section PUZZLE.

Context {A B : Type}.
Context (f : option A -> option B).
Context (f' : option B -> option A).
Context (f'f : forall a, f' (f a) = a).
Context (a : A).

(* The two directions are symmetric, so we will define one and close the section to generalize it and get the other way for free. *)

Section CONTRA2.

Context (fSome : f (Some a) = None).
Context (fNone : f None = None).

Definition swap_contra2 : False.
Proof. congruence. Qed.

End CONTRA2.

Definition option_cases (X : Type) (o : option X) :
{ x | o = Some x } + { o = None }.
Proof. destruct o eqn:E; eauto. Defined.

Definition swap : B.
Proof.
destruct (option_cases _ (f (Some a))) as [ (x&Ho1) | Ho1].
- apply x.
- destruct (option_cases _ (f None)) as [ (y&Ho2) | Ho2].
+ apply y.
+ exfalso. eapply swap_contra2; eauto.
Defined.

End PUZZLE.

(* The rest is easy *)
Lemma inv_swap :
forall A B (f : option A -> option B) (f' : option B -> option A)
(f'f : forall a, f' (f a) = a)
(ff' : forall b, f (f' b) = b)
(a : A),
swap f' f ff' (swap f f' f'f a) = a.
Proof.
intros. unfold swap at 1.
destruct (option_cases A (f' (Some (swap f f' f'f a)))) as [ (x&Ho1) | Ho1].
- unfold swap in Ho1.
destruct (option_cases B (f (Some a))) as [ (y&Ho2) | Ho2].
+ congruence.
+ destruct (option_cases B (f None)) as [ (z&Ho3) | Ho3].
* congruence.
* congruence.
- destruct (option_cases A (f' None)) as [(y&Ho2) | Ho2].
+ unfold swap in Ho1.
destruct (option_cases B (f (Some a))) as [(z&Ho3) | Ho3].
* congruence.
* congruence.
+ congruence.
Qed.
``````
2 Likes

Nice solution! Thanks!

@nojb This step is the nontrivial one:

1. `f None = None` then the result follows because `f` itself induces a bijection `A -> B`.

The difficulty is to express the bijection `A -> B` as a Coq function. We can apply `f` to get an `option B` but we can’t get the `B` out easily. That requires dependent types, which also make proofs difficult because they prevent `destruct` from working.

A different encoding of functions might make it easier to reason about functions as graphs (e.g., using `A -> B -> Prop`), but it’s also less direct.

I would like to stress that point. Defining the bijection as a Coq function is not that difficult; just write it (almost) as if you were writing it in another functional language. (See below.) The actual difficulty lies in dependent pattern-matching (which, as you point out, impedes tactic like `destruct`). That is why @mwuttke97’s use of `option_cases` is critical. It removes any occurrence of dependent pattern-matching from the definition. That trick needs to be publicized more often, as it is a systematic way of solving this kind of issue.

``````Lemma f_Some_None x : f None = None -> f (Some x) = None -> B.
Proof. congruence. Qed.

Definition g (x : A) :=
match f (Some x) as o return _ = o -> B with
| Some y => fun _ => y
| None =>
match f None with
| Some y => fun _ _ => y
| None => f_Some_None x
end eq_refl
end eq_refl.
``````

Thinking back about I wrote, it might seem like I am saying that it is impossible to prove the version with dependent pattern-matching or that tactics like `destruct` cannot be used in such a proof. So, to clear any potential misconception, here is the corresponding proof.

``````Lemma gg' x : g (g' x) = x.
Proof.
unfold g'.
generalize (f'_Some_None x) (ff' (Some x)).
destruct (f' (Some x)) as [x'|] ; intros K H'.
- unfold g.
generalize (f_Some_None x').
now rewrite H'.
- generalize (ff' None).
destruct (f' None) as [x'|] ; intros H.
+ unfold g.
generalize (f_Some_None x').
now rewrite H, H'.