Retracts.v

(** * Library for retracts  *)

(* Author: Maximilian Wuttke *)

Require Import PslBase.Base.


(*
 * A retraction between types [A] and [B] is a tuple of two functions,
 * [f : A -> B] (called the injection function) and [g : B -> option A] (called the retract function),
 * such that the following triangle shaped diagram commutes:
 *
 *          f
 *      A -----> B
 *      |      /
 * Some |     / g
 *      |    /
 *     \|/ |/_
 *    option A
 *
 * That informally means, that the injective function [f] can be reverted by the retract function [g].
 * Foramlly, for all values [x:A] and [y = f x], then [g y = Some x].  (Or: [forall x, g (f x) = Some x].)
 *
 * The retracts should also be "tight", which means that the retract function only reverts values in
 * the image of [f]. Foramlly this means that whenever [g y = Some x], then also [y = f x]
 *
 * Altogether, we have that [forall x y, g y = Some x <-> y = f x].
 *)


Section Retract.

  Variable X Y : Type.

  Definition retract (f : X -> Y) (g : Y -> option X) := forall x y, g y = Some x <-> y = f x.

  Class Retract :=
    {
      Retr_f : X -> Y;
      Retr_g : Y -> option X;
      Retr_retr : retract Retr_f Retr_g;
    }.

End Retract.

Arguments Retr_f { _ _ _ }.
Arguments Retr_g { _ _ _ }.

Section Retract_Properties.

  Variable X Y : Type.

  Hypothesis I : Retract X Y.

  Definition retract_g_adjoint : forall x, Retr_g (Retr_f x) = Some x.
  Proof. intros. pose proof @Retr_retr _ _ I. hnf in H. now rewrite H. Qed.

  Definition retract_g_inv : forall x y, Retr_g y = Some x -> y = Retr_f x.
  Proof. intros. now apply Retr_retr. Qed.

  Lemma retract_g_surjective : forall x, { y | Retr_g y = Some x }.
  Proof. intros x. pose proof retract_g_adjoint x. cbn in H. eauto. Defined.

  Lemma retract_f_injective : forall x1 x2, Retr_f x1 = Retr_f x2 -> x1 = x2.
  Proof.
    intros x1 x2 H.
    enough (Some x1 = Some x2) by congruence.
    erewrite <- !retract_g_adjoint.
    now rewrite H.
  Qed.

  Lemma retract_g_Some x y :
    Retr_g (Retr_f x) = Some y ->
    x = y.
  Proof. now intros H % retract_g_inv % retract_f_injective. Qed.

  Lemma retract_g_None b :
    Retr_g b = None ->
    forall a, Retr_f a <> b.
  Proof.
    intros H a <-.
    enough (Retr_g (Retr_f a) = Some a) by congruence.
    apply retract_g_adjoint.
  Qed.


End Retract_Properties.


(* This tactic replaces all occurrences of [g (f x)] with [Some x] for retracts. *)
Ltac retract_adjoint :=
  match goal with
  | [ H : context [ Retr_g (Retr_f _) ] |- _ ] => rewrite retract_g_adjoint in H
  | [   |- context [ Retr_g (Retr_f _) ]     ] => rewrite retract_g_adjoint
  end.



(*
 * We can compose retractions, as shown in the following commuting diagram
 *
 *            f1        f2
 *      A --------> B --------> C
 *      |         / |         /
 *      |        /  |Some    /
 *      |       /   |       /
 *      |      /    |      /
 * Some |     / g1  |     / g2
 *      |    /      |    /
 *     \|/ |/_     \|/ |/_
 *    option A <--- option B
 *            map g1
 *
 *
 * Where [map g1] is the function that takes an option [x : option B] and applys [Some] and [g1] if it is [Some],
 * and else returns [None].
 *
 * Now [f2 ∘ f1] and [map g1 ∘ g2] gives a retract between [A] and [C].
 *)

Section ComposeRetracts.
  Variable A B C : Type.

  Definition retr_comp_f (f1 : B -> C) (f2 : A -> B) : A -> C := fun a => f1 (f2 a).
  Definition retr_comp_g (g1 : C -> option B) (g2 : B -> option A) : C -> option A :=
    fun c => match g1 c with
          | Some b => g2 b
          | None => None
          end.

  (* No instance (outside of this section), for obvious reasons... *)
  Local Instance ComposeRetract (retr1 : Retract B C) (retr2 : Retract A B) : Retract A C :=
    {|
      Retr_f := retr_comp_f Retr_f Retr_f;
      Retr_g := retr_comp_g Retr_g Retr_g;
    |}.
  Proof.
    abstract now
      unfold retr_comp_f, retr_comp_g; intros a c; split;
      [intros H; destruct (Retr_g c) as [ | ] eqn:E;
       [ apply retract_g_inv in E as ->; now apply retract_g_inv in H as ->
       | congruence
       ]
      | intros ->; now do 2 retract_adjoint
      ].
  Defined.

End ComposeRetracts.


(** We define some useful retracts. *)
Section Usefull_Retracts.

  Variable (A B C D : Type).


  (** Identity retract *)
  Global Instance Retract_id : Retract A A :=
    {|
      Retr_f a := a;
      Retr_g b := Some b;
    |}.
  Proof. abstract now hnf; firstorder congruence. Defined.


  (** Empty retract *)
  Global Instance Retract_Empty : Retract Empty_set A :=
    {|
      Retr_f e := @Empty_set_rect (fun _ => A) e;
      Retr_g b := None;
    |}.
  Proof. abstract now intros x; elim x. Defined.

  (** Eliminate the [Empty_set] from the source sum type *)
  Global Instance Retract_Empty_left `{retr: Retract A B} : Retract (A + Empty_set) B :=
    {|
      Retr_f a := match a with
                  | inl a => Retr_f a
                  | inr e => @Empty_set_rect (fun _ => B) e
                  end;
      Retr_g b := match Retr_g b with
                  | Some a => Some (inl a)
                  | None => None
                  end;
    |}.
  Proof.
    abstract now intros [ a | [] ] b; split;
      [ intros H; destruct (Retr_g b) eqn:E; inv H; now apply retract_g_inv in E
      | intros ->; now retract_adjoint
      ].
  Defined.

  Global Instance Retract_Empty_right `{retr: Retract A B} : Retract (Empty_set + A) B :=
    {|
      Retr_f a := match a with
                  | inl e => @Empty_set_rect (fun _ => B) e
                  | inr a => Retr_f a
                  end;
      Retr_g b := match Retr_g b with
                  | Some a => Some (inr a)
                  | None => None
                  end;
    |}.
  Proof.
    abstract now intros [ [] | a ] b; split;
      [ intros H; destruct (Retr_g b) eqn:E; inv H; now apply retract_g_inv in E
      | intros ->; now retract_adjoint
      ].
  Defined.


  (** We can introduce an additional [Some] and use the identity as the retract function *)
  Global Instance Retract_option `{retr: Retract A B} : Retract A (option B) :=
    {|
      Retr_f a := Some (Retr_f a);
      Retr_g ob := match ob with
                    | Some b => Retr_g b
                    | None => None
                    end;
    |}.
  Proof.
    abstract now
      split;
      [ intros H; destruct y as [b|];
        [ now apply retract_g_inv in H as ->
        | inv H
        ]
      | intros ->; now retract_adjoint
      ].
  Defined.

  (** We can introduce an additional [inl] *)

  Definition retract_inl_f (f : A -> B) : A -> (B + C) := fun a => inl (f a).
  Definition retract_inl_g (g : B -> option A) : B+C -> option A :=
    fun x => match x with
          | inl b => g b
          | inr c => None
          end.

  Global Instance Retract_inl (retrAB : Retract A B) : Retract A (B + C) :=
    {|
      Retr_f := retract_inl_f Retr_f;
      Retr_g := retract_inl_g Retr_g;
    |}.
  Proof.
    abstract now
      unfold retract_inl_f, retract_inl_g; hnf; intros x y; split;
      [ destruct y as [a|b]; [ now intros -> % retract_g_inv | congruence ]
      | intros ->; now retract_adjoint
      ].
  Defined.


  (** The same for [inr] *)

  Definition retract_inr_f (f : A -> B) : A -> (C + B) := fun a => inr (f a).
  Definition retract_inr_g (g : B -> option A) : C+B -> option A :=
    fun x => match x with
          | inr b => g b
          | inl c => None
          end.

  Global Instance Retract_inr (retrAB : Retract A B) : Retract A (C + B) :=
    {|
      Retr_f := retract_inr_f Retr_f;
      Retr_g := retract_inr_g Retr_g;
    |}.
  Proof.
    abstract now
      unfold retract_inr_f, retract_inr_g; hnf; intros x y; split;
      [ destruct y as [a|b]; [ congruence | now intros -> % retract_g_inv ]
      | intros ->; now retract_adjoint
      ].
  Defined.



  (** We can map retracts over sums, similiary as we have done with inversions *)

  Section Retract_sum.

    Definition retract_sum_f (f1: A -> C) (f2: B -> D) : A+B -> C+D :=
      fun x => match x with
            | inl a => inl (f1 a)
            | inr b => inr (f2 b)
            end.

    Definition retract_sum_g (g1: C -> option A) (g2: D -> option B) : C+D -> option (A+B) :=
      fun y => match y with
            | inl c => match g1 c with
                      | Some a => Some (inl a)
                      | None => None
                      end
            | inr d => match g2 d with
                      | Some b => Some (inr b)
                      | None => None
                      end
            end.

    Local Instance Retract_sum (retr1 : Retract A C) (retr2 : Retract B D) : Retract (A+B) (C+D) :=
      {|
        Retr_f := retract_sum_f Retr_f Retr_f;
        Retr_g := retract_sum_g Retr_g Retr_g;
      |}.
    Proof.
      abstract now
        unfold retract_sum_f, retract_sum_g; intros x y; split;
        [ intros H; destruct y as [c|d];
          [ destruct (Retr_g c) eqn:E1; inv H; f_equal; now apply retract_g_inv
          | destruct (Retr_g d) eqn:E1; inv H; f_equal; now apply retract_g_inv
          ]
        | intros ->; destruct x as [a|b]; now retract_adjoint
        ].
    Defined.

  End Retract_sum.

End Usefull_Retracts.



(* If we have a retract from [A] to [Z] and a retract from [B] to Z, in general it is not possible
 * to build a retract from [A+B] to [Z]. For example, there can be no retract from [unit+unit] to
 * [unit]. However, it is possible when the images of the injections are distint.
 *)
Section Join.

  Variable A B Z : Type.

  Variable retr1 : Retract A Z.
  Variable retr2 : Retract B Z.

  Local Arguments Retr_f {_ _} (Retract).
  Local Arguments Retr_g {_ _} (Retract).

  Definition retract_join_f s :=
    match s with
    | inl a => Retr_f retr1 a
    | inr b => Retr_f retr2 b
    end.

  Definition retract_join_g z :=
    match Retr_g retr1 z with
    | Some a => Some (inl a)
    | None =>
      match Retr_g retr2 z with
      | Some b => Some (inr b)
      | None => None
      end
    end.

  Hypothesis disjoint : forall (a : A) (b : B), Retr_f _ a <> Retr_f _ b.

  Lemma retract_join : retract retract_join_f retract_join_g.
  Proof.
    unfold retract_join_f, retract_join_g. hnf; intros s z; split.
    - destruct s as [a|b]; intros H.
      + destruct (Retr_g retr1 z) eqn:E.
        * inv H. now apply retract_g_inv in E.
        * destruct (Retr_g retr2 z) eqn:E2; inv H.
      + destruct (Retr_g retr1 z) eqn:E.
        * inv H.
        * destruct (Retr_g retr2 z) eqn:E2.
          -- inv H. now apply retract_g_inv in E2.
          -- inv H.
    - intros ->. destruct s as [a|b]; retract_adjoint. reflexivity.
      destruct (Retr_g retr1 (Retr_f retr2 b)) eqn:E.
      + exfalso. apply retract_g_inv in E. symmetry in E. now apply disjoint in E.
      + reflexivity.
  Qed.

  Local Instance Retract_join : Retract (A+B) Z := Build_Retract retract_join.

End Join.





(** More instances like [Retract_sum] for bigger sums. *)

Section MoreSums.

  Local Instance Retract_sum3 (A A' B B' C C' : Type) (retr1 : Retract A A') (retr2 : Retract B B') (retr3 : Retract C C') :
    Retract (A+B+C) (A'+B'+C') := Retract_sum (Retract_sum retr1 retr2) retr3.

  Local Instance Retract_sum4 (A A' B B' C C' D D' : Type) (retr1 : Retract A A') (retr2 : Retract B B') (retr3 : Retract C C') (retr4 : Retract D D') :
    Retract (A+B+C+D) (A'+B'+C'+D') := Retract_sum (Retract_sum (Retract_sum retr1 retr2) retr3) retr4.

  Local Instance Retract_sum5 (A A' B B' C C' D D' E E' : Type) (retr1 : Retract A A') (retr2 : Retract B B') (retr3 : Retract C C') (retr4 : Retract D D') (retr5 : Retract E E') :
    Retract (A+B+C+D+E) (A'+B'+C'+D'+E') := Retract_sum (Retract_sum (Retract_sum (Retract_sum retr1 retr2) retr3) retr4) retr5.

  Local Instance Retract_sum6 (A A' B B' C C' D D' E E' F F' : Type) (retr1 : Retract A A') (retr2 : Retract B B') (retr3 : Retract C C') (retr4 : Retract D D') (retr5 : Retract E E') (retr6 : Retract F F') :
    Retract (A+B+C+D+E+F) (A'+B'+C'+D'+E'+F') := Retract_sum (Retract_sum (Retract_sum (Retract_sum (Retract_sum retr1 retr2) retr3) retr4) retr5) retr6.

  Local Instance Retract_sum7 (A A' B B' C C' D D' E E' F F' G G' : Type) (retr1 : Retract A A') (retr2 : Retract B B') (retr3 : Retract C C') (retr4 : Retract D D') (retr5 : Retract E E') (retr6 : Retract F F') (retr7 : Retract G G') :
    Retract (A+B+C+D+E+F+G) (A'+B'+C'+D'+E'+F'+G') := Retract_sum (Retract_sum (Retract_sum (Retract_sum (Retract_sum (Retract_sum retr1 retr2) retr3) retr4) retr5) retr6) retr7.

End MoreSums.