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.
Admitted.
Definition g' : B -> A.
Admitted.
Lemma g'g : forall a, g' (g a) = a.
Admitted.
Lemma gg' : forall a, g (g' a) = a.
Admitted.
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. *)
Admitted.
```