Merge pull request #1428 from andreaslyn/infinitary-universal-algebra

Algebra operations

_CoqProject

@@ -124,6 +124,7 @@ theories/Spaces/Finite/Fin.v
 theories/Spaces/Finite/FinNat.v
 theories/Spaces/Finite/FinInduction.v
 theories/Spaces/Finite/Finite.v
+theories/Spaces/Finite/FinSeq.v
 theories/Spaces/Finite/Tactics.v
 theories/Spaces/Finite.v
 
@@ -352,6 +353,7 @@ theories/Spectra/Coinductive.v
 
 theories/Algebra/Universal/Algebra.v
 theories/Algebra/Universal/Homomorphism.v
+theories/Algebra/Universal/Operation.v
 
 #
 #   Algebra

theories/Algebra/Universal/Operation.v

@@ -0,0 +1,220 @@
+(** This file continues the development of algebra [Operation]. It
+    gives a way to construct operations using (conventional) curried
+    functions, and shows that such curried operations are equivalent
+    to the uncurried operations [Operation]. *)
+
+Require Export HoTT.Algebra.Universal.Algebra.
+
+Require Import
+  HoTT.Basics
+  HoTT.Types
+  HoTT.DProp
+  HoTT.Spaces.Finite
+  HoTT.Spaces.Nat
+  HoTT.Spaces.Finite.FinSeq.
+
+Import notations_algebra.
+
+(** Functions [head_dom'] and [head_dom] are used to get the first
+    element of a nonempty operation domain [a : forall i, A (ss i)]. *)
+
+Monomorphic Definition head_dom' {σ} (A : Carriers σ) (n : nat)
+  : forall (N : n > 0) (ss : FinSeq n (Sort σ)) (a : forall i, A (ss i)),
+    A (fshead' n N ss)
+  := match n with
+     | 0 => fun N ss _ => Empty_rec N
+     | n'.+1 => fun N ss a => a fin_zero
+     end.
+
+Monomorphic Definition head_dom {σ} (A : Carriers σ) {n : nat}
+  (ss : FinSeq n.+1 (Sort σ)) (a : forall i, A (ss i))
+  : A (fshead ss)
+  := head_dom' A n.+1 tt ss a.
+
+(** Functions [tail_dom'] and [tail_dom] are used to obtain the tail
+    of an operation domain [a : forall i, A (ss i)]. *)
+
+Monomorphic Definition tail_dom' {σ} (A : Carriers σ) (n : nat)
+  : forall (ss : FinSeq n (Sort σ)) (a : forall i, A (ss i)) (i : Fin (pred n)),
+    A (fstail' n ss i)
+  := match n with
+     | 0 => fun ss _ i => Empty_rec i
+     | n'.+1 => fun ss a i => a (fsucc i)
+     end.
+
+Monomorphic Definition tail_dom {σ} (A : Carriers σ) {n : nat}
+  (ss : FinSeq n.+1 (Sort σ)) (a : forall i, A (ss i))
+  : forall i, A (fstail ss i)
+  := tail_dom' A n.+1 ss a.
+
+(** Functions [cons_dom'] and [cons_dom] to add an element to
+    the front of a given domain [a : forall i, A (ss i)]. *)
+
+Monomorphic Definition cons_dom' {σ} (A : Carriers σ) {n : nat}
+  : forall (i : Fin n) (ss : FinSeq n (Sort σ)) (N : n > 0),
+    A (fshead' n N ss) -> (forall i, A (fstail' n ss i)) -> A (ss i)
+  := fin_ind
+      (fun n i =>
+        forall (ss : Fin n -> Sort σ) (N : n > 0),
+        A (fshead' n N ss) -> (forall i, A (fstail' n ss i)) -> A (ss i))
+      (fun n' => fun _ z => match z with tt => fun x _ => x end)
+      (fun n' i' _ => fun _ _ _ xs => xs i').
+
+Definition cons_dom {σ} (A : Carriers σ)
+  {n : nat} (ss : FinSeq n.+1 (Sort σ))
+  (x : A (fshead ss)) (xs : forall i, A (fstail ss i))
+  : forall i : Fin n.+1, A (ss i)
+  := fun i => cons_dom' A i ss tt x xs.
+
+(** The empty domain: *)
+
+Definition nil_dom {σ} (A : Carriers σ) (ss : FinSeq 0 (Sort σ))
+  : forall i : Fin 0, A (ss i)
+  := Empty_ind (A o ss).
+
+(** A specialization of [Operation] to finite [Fin n] arity. *)
+
+Definition FiniteOperation {σ : Signature} (A : Carriers σ)
+  {n : nat} (ss : FinSeq n (Sort σ)) (t : Sort σ) : Type
+  := Operation A {| Arity := Fin n; sorts_dom := ss; sort_cod := t |}.
+
+(** A type of curried operations
+<<
+CurriedOperation A [s1, ..., sn] t := A s1 -> ... -> A sn -> A t.
+>> *)
+
+Fixpoint CurriedOperation {σ} (A : Carriers σ) {n : nat}
+  : (FinSeq n (Sort σ)) -> Sort σ -> Type
+  := match n with
+     | 0 => fun ss t => A t
+     | n'.+1 =>
+        fun ss t => A (fshead ss) -> CurriedOperation A (fstail ss) t
+     end.
+
+(** Function [operation_uncurry] is used to uncurry an operation
+<<
+operation_uncurry A [s1, ..., sn] t (op : CurriedOperation A [s1, ..., sn] t)
+  : FiniteOperation A [s1, ..., sn] t
+  := fun (x1 : A s1, ..., xn : A xn) => op x1 ... xn
+>>
+See [equiv_operation_curry] below. *)
+
+Fixpoint operation_uncurry {σ} (A : Carriers σ) {n : nat}
+  : forall (ss : FinSeq n (Sort σ)) (t : Sort σ),
+    CurriedOperation A ss t -> FiniteOperation A ss t
+  := match n with
+     | 0 => fun ss t op _ => op
+     | n'.+1 =>
+        fun ss t op a =>
+          operation_uncurry A (fstail ss) t (op (a fin_zero)) (a o fsucc)
+     end.
+
+Local Example computation_example_operation_uncurry
+  : forall
+      (σ : Signature) (A : Carriers σ) (n : nat) (s1 s2 t : Sort σ)
+      (ss := (fscons s1 (fscons s2 fsnil)))
+      (op : CurriedOperation A ss t) (a : forall i, A (ss i)),
+    operation_uncurry A ss t op
+    = fun a => op (a fin_zero) (a (fsucc fin_zero)).
+Proof.
+  reflexivity.
+Qed.
+
+(** Function [operation_curry] is used to curry an operation
+<<
+operation_curry A [s1, ..., sn] t (op : FiniteOperation A [s1, ..., sn] t)
+  : CurriedOperation A [s1, ..., sn] t
+  := fun (x1 : A s1) ... (xn : A xn) => op (x1, ..., xn)
+>>
+See [equiv_operation_curry] below. *)
+
+Fixpoint operation_curry {σ} (A : Carriers σ) {n : nat} 
+  : forall (ss : FinSeq n (Sort σ)) (t : Sort σ),
+    FiniteOperation A ss t -> CurriedOperation A ss t
+  := match n with
+     | 0 => fun ss t op => op (Empty_ind _)
+     | n'.+1 =>
+        fun ss t op x =>
+          operation_curry A (fstail ss) t (op o cons_dom A ss x)
+     end.
+
+Local Example computation_example_operation_curry
+  : forall
+      (σ : Signature) (A : Carriers σ) (n : nat) (s1 s2 t : Sort σ)
+      (ss := (fscons s1 (fscons s2 fsnil)))
+      (op : FiniteOperation A ss t)
+      (x1 : A s1) (x2 : A s2),
+    operation_curry A ss t op
+    = fun x1 x2 => op (cons_dom A ss x1 (cons_dom A _ x2 (nil_dom A _))).
+Proof.
+  reflexivity.
+Qed.
+
+Lemma expand_cons_dom' {σ} (A : Carriers σ) (n : nat)
+  : forall (i : Fin n) (ss : FinSeq n (Sort σ)) (N : n > 0)
+           (a : forall i, A (ss i)),
+    cons_dom' A i ss N (head_dom' A n N ss a) (tail_dom' A n ss a) = a i.
+Proof.
+  intro i.
+  induction i using fin_ind; intros ss N a.
+  - unfold cons_dom'.
+    rewrite compute_fin_ind_fin_zero.
+    by destruct N.
+  - unfold cons_dom'.
+    by rewrite compute_fin_ind_fsucc.
+Qed.
+
+Lemma expand_cons_dom `{Funext} {σ} (A : Carriers σ)
+  {n : nat} (ss : FinSeq n.+1 (Sort σ)) (a : forall i, A (ss i))
+  : cons_dom A ss (head_dom A ss a) (tail_dom A ss a) = a.
+Proof.
+  funext i.
+  apply expand_cons_dom'.
+Defined.
+
+Lemma path_operation_curry_to_cunurry `{Funext} {σ} (A : Carriers σ)
+  {n : nat} (ss : FinSeq n (Sort σ)) (t : Sort σ)
+  : operation_uncurry A ss t o operation_curry A ss t == idmap.
+Proof.
+  intro a.
+  induction n as [| n IHn].
+  - funext d. refine (ap a _). apply path_contr.
+  - funext a'.
+    refine (ap (fun x => x _) (IHn _ _) @ _).
+    refine (ap a _).
+    apply expand_cons_dom.
+Qed.
+
+Lemma path_operation_uncurry_to_curry `{Funext} {σ} (A : Carriers σ)
+  {n : nat} (ss : FinSeq n (Sort σ)) (t : Sort σ)
+  : operation_curry A ss t o operation_uncurry A ss t == idmap.
+Proof.
+  intro a.
+  induction n; [reflexivity|].
+  funext x.
+  refine (_ @ IHn (fstail ss) (a x)).
+  refine (ap (operation_curry A (fstail ss) t) _).
+  funext a'.
+  simpl.
+  unfold cons_dom, cons_dom'.
+  rewrite compute_fin_ind_fin_zero.
+  refine (ap (operation_uncurry A (fstail ss) t (a x)) _).
+  funext i'.
+  now rewrite compute_fin_ind_fsucc.
+Qed.
+
+Global Instance isequiv_operation_curry `{Funext} {σ} (A : Carriers σ)
+  {n : nat} (ss : FinSeq n (Sort σ)) (t : Sort σ)
+  : IsEquiv (operation_curry A ss t).
+Proof.
+  srapply isequiv_adjointify.
+  - apply operation_uncurry.
+  - apply path_operation_uncurry_to_curry.
+  - apply path_operation_curry_to_cunurry.
+Defined.
+
+Definition equiv_operation_curry `{Funext} {σ} (A : Carriers σ)
+  {n : nat} (ss : FinSeq n (Sort σ)) (t : Sort σ)
+  : FiniteOperation A ss t <~> CurriedOperation A ss t
+  := Build_Equiv _ _ (operation_curry A ss t) _.
+

theories/Spaces/Finite.v

@@ -1,4 +1,5 @@
-
 Require Export Finite.Fin.
+Require Export Finite.FinNat.
+Require Export Finite.FinInduction.
 Require Export Finite.Finite.
 Require Export Finite.Tactics.

theories/Spaces/Finite/Fin.v

@@ -15,7 +15,7 @@ Local Open Scope nat_scope.
 
 (** A *finite set* is a type that is merely equivalent to the canonical finite set determined by some natural number.  There are many equivalent ways to define the canonical finite sets, such as [{ k : nat & k < n}]; we instead choose a recursive one. *)
 
-Fixpoint Fin (n : nat) : Type
+Fixpoint Fin (n : nat) : Type0
   := match n with
        | 0 => Empty
        | S n => Fin n + Unit
@@ -112,14 +112,14 @@ Proof.
     + rewrite path_fin_fsucc_incl, path_nat_fin_incl.
       apply IHn.
     + reflexivity.
-Qed.
+Defined.
 
 Lemma path_nat_fin_zero {n} : fin_to_nat (@fin_zero n) = 0.
 Proof.
   induction n as [|n' IHn].
   - reflexivity.
   - trivial.
-Qed.
+Defined.
 
 Lemma path_nat_fin_last {n} : fin_to_nat (@fin_last n) = n.
 Proof.

theories/Spaces/Finite/FinInduction.v

@@ -11,7 +11,7 @@ Definition fin_ind (P : forall n : nat, Fin n -> Type)
   {n : nat} (k : Fin n)
   : P n k.
 Proof.
-  refine (transport (P n) (homot_fin_to_finnat_to_fin k) _).
+  refine (transport (P n) (path_fin_to_finnat_to_fin k) _).
   refine (finnat_ind (fun n u => P n (finnat_to_fin u)) _ _ _).
   - intro. apply z.
   - intros n' u c. apply s. exact c.
@@ -23,7 +23,7 @@ Lemma compute_fin_ind_fin_zero (P : forall n : nat, Fin n -> Type)
   : fin_ind P z s fin_zero = z n.
 Proof.
   unfold fin_ind.
-  generalize (homot_fin_to_finnat_to_fin (@fin_zero n)).
+  generalize (path_fin_to_finnat_to_fin (@fin_zero n)).
   induction (path_fin_to_finnat_fin_zero n)^.
   intro p.
   by induction (hset_path2 1 p).
@@ -36,13 +36,13 @@ Lemma compute_fin_ind_fsucc (P : forall n : nat, Fin n -> Type)
   : fin_ind P z s (fsucc k) = s n k (fin_ind P z s k).
 Proof.
   unfold fin_ind.
-  generalize (homot_fin_to_finnat_to_fin (fsucc k)).
+  generalize (path_fin_to_finnat_to_fin (fsucc k)).
   induction (path_fin_to_finnat_fsucc k)^.
   intro p.
   refine (ap (transport (P n.+1) p) (compute_finnat_ind_succ _ _ _ _) @ _).
   generalize dependent p.
-  induction (homot_fin_to_finnat_to_fin k).
-  induction (homot_fin_to_finnat_to_fin k)^.
+  induction (path_fin_to_finnat_to_fin k).
+  induction (path_fin_to_finnat_to_fin k)^.
   intro p.
   now induction (hset_path2 1 p).
 Defined.
@@ -51,4 +51,20 @@ Definition fin_rec (B : nat -> Type)
   : (forall n : nat, B n.+1) -> (forall (n : nat), Fin n -> B n -> B n.+1) ->
     forall {n : nat}, Fin n -> B n
   := fin_ind (fun n _ => B n).
-
+
+Lemma compute_fin_rec_fin_zero (B : nat -> Type)
+  (z : forall n : nat, B n.+1)
+  (s : forall (n : nat) (k : Fin n), B n -> B n.+1) (n : nat)
+  : fin_rec B z s fin_zero = z n.
+Proof.
+  apply (compute_fin_ind_fin_zero (fun n _ => B n)).
+Defined.
+
+Lemma compute_fin_rec_fsucc (B : nat -> Type)
+  (z : forall n : nat, B n.+1)
+  (s : forall (n : nat) (k : Fin n), B n -> B n.+1)
+  {n : nat} (k : Fin n)
+  : fin_rec B z s (fsucc k) = s n k (fin_rec B z s k).
+Proof.
+  apply (compute_fin_ind_fsucc (fun n _ => B n)).
+Defined.

theories/Spaces/Finite/FinNat.v

@@ -79,7 +79,8 @@ Proof.
                    (hset_path2 1 (@path_succ_finnat n u u.2)) idpath).
 Defined.
 
-Definition is_bounded_fin_to_nat {n} (k : Fin n) : fin_to_nat k < n.
+Monomorphic Definition is_bounded_fin_to_nat {n} (k : Fin n)
+  : fin_to_nat k < n.
 Proof.
   induction n as [| n IHn].
   - elim k.
@@ -90,10 +91,10 @@ Proof.
     + apply leq_refl.
 Defined.
 
-Definition fin_to_finnat {n} (k : Fin n) : FinNat n
+Monomorphic Definition fin_to_finnat {n} (k : Fin n) : FinNat n
   := (fin_to_nat k; is_bounded_fin_to_nat k).
 
-Fixpoint finnat_to_fin {n : nat} : FinNat n -> Fin n
+Monomorphic Fixpoint finnat_to_fin {n : nat} : FinNat n -> Fin n
   := match n with
      | 0 => fun u => Empty_rec u.2
      | n.+1 => fun u =>
@@ -160,7 +161,7 @@ Proof.
   - exact (ap fsucc IHn).
 Defined.
 
-Lemma homot_finnat_to_fin_to_finnat {n : nat} (u : FinNat n)
+Lemma path_finnat_to_fin_to_finnat {n : nat} (u : FinNat n)
   : fin_to_finnat (finnat_to_fin u) = u.
 Proof.
   induction n as [| n IHn].
@@ -173,7 +174,7 @@ Proof.
       exact (ap S (IHn (x; h))..1).
 Defined.
 
-Lemma homot_fin_to_finnat_to_fin {n : nat} (k : Fin n)
+Lemma path_fin_to_finnat_to_fin {n : nat} (k : Fin n)
   : finnat_to_fin (fin_to_finnat k) = k.
 Proof.
   induction n as [| n IHn].
@@ -187,5 +188,5 @@ Defined.
 
 Definition equiv_fin_finnat (n : nat) : Fin n <~> FinNat n
   := equiv_adjointify fin_to_finnat finnat_to_fin
-      homot_finnat_to_fin_to_finnat
-      homot_fin_to_finnat_to_fin.
+      path_finnat_to_fin_to_finnat
+      path_fin_to_finnat_to_fin.