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.
if f None = None then the result follows because f itself induces a bijection A -> B.
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).
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.
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.
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'.
+ contradict H'.
now rewrite H.
Qed.
