ArbitraryArity

Gaëtan Gilbert edited this page Feb 8, 2018 · 5 revisions

Here's an example showing how to define and work with functions taking a variable number of arguments.

(* Defines the type of a function X^n -> Y. *)
Fixpoint n_args (X Y:Type) (n:nat) : Type :=
  match n with
  | 0 => Y
  | S m => X -> (n_args X Y m)
  end.

(* Composition of a function X^n -> Y with a function Y -> Z. *)
Fixpoint n_args_range_fun {n:nat} {X Y Z:Type} :
  (Y->Z) -> (n_args X Y n) -> (n_args X Z n) :=
  fun f =>
    match n as n' return (n_args X Y n' -> n_args X Z n') with
    | 0 => fun g => f g
    | S n0 => fun g x => n_args_range_fun f (g x)
    end.
(* Eval compute in (@n_args_range_fun 3). *)

(* Composition of a function Y^n -> Z with a function X -> Y. *)
Fixpoint n_args_dom_fun {n:nat} {X Y Z:Type} :
  (n_args Y Z n) -> (X->Y) -> (n_args X Z n) :=
  match n as n' return (n_args Y Z n' -> (X -> Y) -> n_args X Z n') with
  | 0 => fun z _ => z
  | S n0 => fun f g x => n_args_dom_fun (f (g x)) g
  end.
(* Eval compute in (@n_args_dom_fun 3). *)

(* Composition of a function X^n -> Y with the diagonal map X -> X^n. *)
Fixpoint duplicate_arg {n:nat} {X Y:Type} :
  (n_args X Y n) -> X -> Y :=
  match n as n' return (n_args X Y n' -> X -> Y) with
  | 0 => fun y _ => y
  | S n0 => fun f x => duplicate_arg (f x) x
  end.
(* Eval compute in (@duplicate_args 3). *)

(* Composition of a function X^n -> Y with a function X -> Y -> Z to get
   a function X^(n+1) -> Z. *)
Definition curry_first_arg {n:nat} {X Y Z:Type} :
  (X->Y->Z) -> (n_args X Y n) -> (n_args X Z (S n)) :=
  fun f g x => n_args_range_fun (f x) g.
(* Eval compute in (@curry_first_arg 3). *)

(* Composition of a function X^n -> Y with a function Y -> X -> Z to get
   a function X^(n+1) -> Z. *)
Fixpoint curry_last_arg {n:nat} {X Y Z:Type} {struct n} :
  (Y->X->Z) -> (n_args X Y n) -> (n_args X Z (S n)) :=
  fun f =>
    match n as n' return (n_args X Y n' -> n_args X Z (S n')) with
    | 0 => fun g x => f g x
    | S n0 => fun g x => curry_last_arg f (g x)
    end.
(* Eval compute in (@curry_last_arg 3). *)

(* Translate from a function Y -> X^n -> Z to X^n -> Y -> Z.
   In the other direction you can use n_args_range_fun to compose
   X^n -> Y -> Z with evaluation at y for a given y:Y. *)
Fixpoint bring_dep_inside {n:nat} {X Y Z:Type} :
  (Y -> (n_args X Z n)) -> (n_args X (Y->Z) n) :=
  match n as n' return ((Y -> n_args X Z n') -> n_args X (Y->Z) n') with
  | 0 => fun f => f
  | S n0 => fun f x0 => bring_dep_inside (fun y:Y => f y x0)
  end.
(* Eval compute in (@bring_dep_inside 3). *)

(* Composition of a function Y^n -> Z with n functions X -> Y. *)
Fixpoint n_args_dom_funs {n:nat} {X Y Z:Type} {struct n} :
  (n_args Y Z n) -> (n_args (X->Y) (n_args X Z n) n) :=
  match n as n' return (n_args Y Z n' -> n_args (X->Y) (n_args X Z n') n') with
  | 0 => fun z => z
  | S n0 => fun f g0 => bring_dep_inside
                      (fun x0:X => n_args_dom_funs (f (g0 x0)))
  end.
(* Eval compute in (@n_args_dom_funs 3). *)

Lemma n_args_add: forall (X Y:Type) (n m:nat),
    n_args X (n_args X Y m) n = n_args X Y (n+m).
Proof.
  induction n.
  trivial.
  intros.
  simpl.
  rewrite IHn.
  reflexivity.
Defined.

(* Defines the type of an operator on X of a given arity. *)
Definition operator (X:Type) (arity:nat) : Type := n_args X X arity.

Require Export Relation_Definitions.
Require Export RelationClasses.

Generalizable Variables eqv.

(* Extensional equality of two functions X^n -> Y. *)
Fixpoint n_args_equiv {X Y:Type} {n:nat} `{Equivalence Y eqv} :
  relation (n_args X Y n) :=
  match n as m return (relation (n_args X Y m)) with
  | 0 => eqv
  | S m => fun op1 op2 => forall x:X, n_args_equiv (op1 x) (op2 x)
  end.
(* Eval compute in (fun X Y => (@n_args_equiv X Y 3)). *)

Instance n_args_equiv_equiv: forall (X Y:Type) (n:nat) `{Equivalence Y eqv},
    Equivalence (@n_args_equiv X Y n _ _).
Proof.
  intros.
  induction n.
  simpl.
  trivial.
  simpl.
  constructor.
  red; intros op x.
  reflexivity.
  red; intros op1 op2 ? x.
  symmetry; trivial.
  red; intros op1 op2 op3 ? ? x.
  etransitivity; eauto.
Qed.

Require Export Morphisms.

(* Signature which asserts the properness of an operator of arity n over R. *)
Fixpoint operator_signature {X:Type} (R:relation X) (n:nat) :
  relation (operator X n) :=
  match n with
  | 0 => R%signature
  | S m => (R ==> operator_signature R m)%signature
  end.

(* Example of this: define an arbitrary variety of algebras. *)
Class AlgebraSignature (Operation:Type) : Type :=
| Arity : Operation -> nat.

Section algebra_signature.
  Context `{AlgebraSignature}.

  (* Unfortunately, we can't make an inductive constructor of type
   forall op:Operation, operator (abstract_term vars) (Arity op), so we
   go through an intermediate vector type and then define that constructor
   later... *)
  Inductive abstract_term (vars:Type) : Type :=
  | var_term: vars -> abstract_term vars
  | op_term_vect: forall op:Operation,
      abstract_term_vector vars (Arity op) -> abstract_term vars

  with abstract_term_vector (vars:Type) : nat -> Type :=
       | term_vector_nil: abstract_term_vector vars 0
       | term_vector_cons: forall {n:nat}, abstract_term vars ->
                                    abstract_term_vector vars n ->
                                    abstract_term_vector vars (S n).

  Fixpoint make_vect_aux {vars:Type} (n:nat) {X} (f:abstract_term_vector vars n -> X)
    : n_args (abstract_term vars) X n :=
    match n as n' return ((abstract_term_vector vars n' -> X) ->
                          n_args (abstract_term vars) X n') with
    | 0 => fun f => f (term_vector_nil vars)
    | S m =>
      fun f (t:abstract_term vars) =>
        @make_vect_aux vars m _ (fun v => f (term_vector_cons vars t v))
    end f.

  Definition make_vect {vars:Type} (n:nat) :
    n_args (abstract_term vars) (abstract_term_vector vars n) n :=
    make_vect_aux n (fun t:abstract_term_vector vars n => t).
  (* Eval compute in (fun vars => @make_vect_aux vars 3). *)
  (* Eval compute in (fun vars => @make_vect vars 3). *)

  Definition op_term {vars:Type} (op:Operation) :
    operator (abstract_term vars) (Arity op) :=
    make_vect_aux (Arity op) (op_term_vect vars op).

  Fixpoint evaluate {X:Type} {vars:Type}
           (vals: vars -> X) (ops: forall op:Operation, operator X (Arity op))
           (t: abstract_term vars) {struct t} : X :=
    match t with
    | var_term _ v => vals v
    | op_term_vect _ op v => vector_evaluate vals ops v (ops op)
    end

  with vector_evaluate
         {X:Type} {vars:Type}
         (vals: vars -> X) (ops: forall op:Operation, operator X (Arity op))
         {n:nat} (v:abstract_term_vector vars n) (top_op: operator X n)
         {struct v} : X :=
         match v in (abstract_term_vector _ m) return (operator X m -> X) with
         | term_vector_nil _ => fun op => op
         | term_vector_cons _ hd tl =>
           fun op => vector_evaluate vals ops tl (op (evaluate vals ops hd))
         end top_op.

End algebra_signature.

Class AlgebraSpec : Type :=
  { Operation: Type;
    signature:> AlgebraSignature Operation;
    Identity: Type;
    IdentityVariable: Identity -> Type;
    IdentityTerms: forall ident:Identity,
        abstract_term (IdentityVariable ident) *
        abstract_term (IdentityVariable ident) }.

Require Export SetoidClass.

Class Algebra (A:Type) `{Setoid A} `{AlgebraSpec} : Type :=
  { ops: forall op:Operation, operator A (Arity op);
    op_proper:> forall op:Operation,
        Proper (operator_signature equiv (Arity op)) (ops op);
    identity_holds:
      forall (ident:Identity) (vars: IdentityVariable ident -> A),
        evaluate vars ops (fst (IdentityTerms ident)) ==
        evaluate vars ops (snd (IdentityTerms ident)) }.

Generalizable Variables A B.

Class AlgebraHom `{AlgebraSpec} `{Setoid A} `{!Algebra A}
      `{Setoid B} `{!Algebra B} (f:A->B) : Prop :=
| respects_ops: forall op:Operation,
    n_args_equiv (n_args_range_fun f (ops op))
                 (n_args_dom_fun (ops op) f).

Inductive no_vars : Set := .

Inductive one_var : Set := var1_x.

Inductive two_vars : Set := var2_x | var2_y.

Inductive three_vars : Set := var3_x | var3_y | var3_z.

About var_term.
Arguments var_term {Operation H vars} _.

(* Example constructing groups as an instance of a variety of algebras.
   Defining the identities is still a bit cumbersome... *)
Section groups_example.

  Inductive GroupOp : Set := GroupMult | GroupInv | GroupId.

  Instance GroupSignature : AlgebraSignature GroupOp :=
    fun (op:GroupOp) => match op with
                     | GroupMult => 2
                     | GroupInv => 1
                     | GroupId => 0
                     end.

  Inductive GroupIdentity : Set :=
    GroupIdLeft | GroupIdRight | GroupInvLeft | GroupInvRight | GroupAssoc.

  Instance GroupSpec : AlgebraSpec :=
    { Operation := GroupOp;
      Identity := GroupIdentity;
      IdentityVariable :=
        fun ident => match ident with
                  | GroupIdLeft => one_var
                  | GroupIdRight => one_var
                  | GroupInvLeft => one_var
                  | GroupInvRight => one_var
                  | GroupAssoc => three_vars
                  end
    }.
  Proof.
  (* IdentityTerms *)
  destruct ident.
  (* GroupIdLeft *)
  exact ( (op_term GroupMult (op_term GroupId) (var_term var1_x),
           var_term var1_x) ).
  (* GroupIdRight *)
  exact ( (op_term GroupMult (var_term var1_x) (op_term GroupId),
           var_term var1_x) ).
  (* GroupInvLeft *)
  exact ( (op_term GroupMult (op_term GroupInv (var_term var1_x))
                   (var_term var1_x),
           op_term GroupId) ).
  (* GroupInvRight *)
  exact ( (op_term GroupMult (var_term var1_x)
                   (op_term GroupInv (var_term var1_x)),
           var_term var1_x) ).
  (* GroupAssoc *)
  exact ( (op_term GroupMult (var_term var3_x)
                   (op_term GroupMult (var_term var3_y) (var_term var3_z)),
           op_term GroupMult
                   (op_term GroupMult (var_term var3_x) (var_term var3_y))
                   (var_term var3_z)) ).
  Defined.

  Generalizable Variables G.

  Class Group (G:Type) `{Setoid G} : Type :=
  | group_structure:> Algebra G.

  Context `{Group G}.

  Definition group_mult : G -> G -> G := ops GroupMult.

  Definition group_inv: G -> G := ops GroupInv.

  Definition group_id: G := ops GroupId.

  Lemma group_mult_proper: Proper (equiv ==> equiv ==> equiv) group_mult.
  Proof.
    exact (op_proper GroupMult).
  Qed.

  Lemma group_mult_assoc: forall x y z:G,
      group_mult x (group_mult y z) ==
      group_mult (group_mult x y) z.
  Proof.
    intros.
    exact (identity_holds
             GroupAssoc
             (fun v:three_vars =>
                match v with
                | var3_x => x | var3_y => y | var3_z => z
                end)).
  Qed.

End groups_example.
Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.