both.v

Require Import List.
Import ListNotations.
Definition head := hd_error.
Definition tail := tl.
Definition len  := length.

(* make the type parameter "invisible" to the user,
   e.g. the type of 'len' is
      list ?1 -> nat
   where ?1 will be inferred from the context. *)
Arguments head {A} _.
Arguments tail {A} _.
Arguments len  {A} _.

Module NotationBoth.
  (* like (***) from Control.Arrow specialized to functions *)
  Definition aaa a b a' b' (f : a -> b) (g : a' -> b')
    : (a * a') -> (b * b')
    := (fun x => (f (fst x), g (snd x))).

  Notation "f *** g" := (aaa _ _ _ _ f g) (at level 0).

  Eval compute in (head *** len) ([1;2], [tt]).

  Notation "'both' f" := (f *** f) (at level 0).

  Eval compute in both head ([1;2], [tt]).
  (* = (Some 1, Some tt)
     : option nat * option unit *)
  
  Eval compute in both len ([1;2], [tt]).
  (* = (2, 1)
     : nat * nat *)
  
  Eval compute in both tail ([1;2], [tt]).
  (* = ([2], [])
     : list nat * list unit *)
End NotationBoth.


(* make the functions "visibly polymorphic" again,
   e.g. the type of 'len' will be
      forall a, list a -> nat
   now. *)
Arguments head [A] _.
Arguments tail [A] _.
Arguments len  [A] _.

Module FunctionBoth.
  Section Def.
    Variables dom cod : Type -> Type.
    
    Variable f : forall a, dom a -> cod a.
    
    Definition both a a' : dom a * dom a' -> cod a * cod a'
      := fun x => (f _ (fst x), f _ (snd x)).
  End Def.
    
  Check both.
  (* both
     : forall dom cod : Type -> Type,
       (forall a : Type, dom a -> cod a) ->
       forall a a' : Type, dom a * dom a' -> cod a * cod a' *)
  Arguments both {_ _} _ {_ _} _.
  Print Implicit both.
  (* Arguments dom, cod, a, a' are implicit and maximally inserted *)

  Eval compute in both head ([1;2], [tt]).
  (* = (Some 1, Some tt)
     : option nat * option unit *)
  
  Eval compute in both len ([1;2], [tt]).
  (* = (2, 1)
     : (fun _ : Type => nat) nat * (fun _ : Type => nat) unit *)
  
  Eval compute in both tail ([1;2], [tt]).
  (* = ([2], [])
     : list nat * list unit *)
  
(* ******************************************************* *)
  
  Section Defaaa.
    Variables dom1 cod1 dom2 cod2 : Type -> Type.
    Variables (f : forall a, dom1 a -> cod1 a)
              (g : forall a, dom2 a -> cod2 a).
    
    Definition aaa a a' : dom1 a * dom2 a' -> cod1 a * cod2 a'
      := (fun x => (f _ (fst x), g _ (snd x))).
  End Defaaa.
  
  Check aaa.
  (* aaa
     : forall dom1 cod1 dom2 cod2 : Type -> Type,
       (forall a : Type, dom1 a -> cod1 a) ->
       (forall a : Type, dom2 a -> cod2 a) ->
       forall a a' : Type, dom1 a * dom2 a' -> cod1 a * cod2 a'  *)
  Arguments aaa {_ _ _ _} _ _ {_ _} _.
  
  Eval compute in aaa head tail ([1;2], [tt]).
  (* = (Some 1, [])
     : option nat * list unit   *)
  Eval compute in aaa head len ([1;2], [tt]).
  (* = (Some 1, 1)
     : option nat * (fun _ : Type => nat) unit   *)
  
  Section Def2.
    Variable dom cod : Type -> Type.
    Variable f : forall a, dom a -> cod a.
    
    Definition both2 a a' : dom a * dom a' -> cod a * cod a'
      := aaa f f.
  End Def2.

  Arguments both2 {_ _} _ {_ _} _.

  Check @both.
  Lemma both_both2 : @both = @both2.
  Proof. reflexivity. Qed.
End FunctionBoth.