OperadOfSets.v

Require Import FunctionalExtensionality.
Require Import List.
From Hammer Require Import Hammer.
Require Import Permutation.

From Operads Require Import Typecast.
From Operads Require Import ColoredOperads.

(* This is a modfication of the definition of compose from the 
   multiCompose.v file to eliminate dependence on vectors,
   using lists instead. The type of the arguments is also changed from type to T, the 
   collection of types inductively defined in TColoredOperads.v.*)

Fixpoint arr (ts : list Type) (t' : Type) : Type := match ts with
  | nil => t'
  | t :: ts => t -> (arr ts t') end.

Lemma arr_equation_1 {t' : Type} : arr nil t' = t'.
Proof.
reflexivity.
Qed.

Lemma arr_equation_2 {t t' : Type} {ts : list Type} : arr (t :: ts) t' = (t -> arr ts t').
Proof.
reflexivity.
Qed.

Fixpoint compose' (bs : list Type) {ci d : Type} : (ci -> d) -> (arr bs ci) -> (arr bs d) := match bs with 
  | nil => fun f g => f g
  | b :: bs => fun f g x => compose' bs f (g x) end.

Lemma compose'_equation_1 {ci d : Type} {f : ci -> d} {g : ci} : compose' nil f g = f g.
Proof.
reflexivity.
Qed.

Lemma compose'_equation_2 {ci d b : Type} {bs : list Type} {f : ci -> d} {g : arr (b :: bs) ci} : 
  compose' (b :: bs) f g = fun x => compose' bs f (g x).
Proof.
reflexivity.
Qed.

(* f : c0 -> ... -> cn-1 -> cn -> d   (* NB: d itself may be a function type *)
   g : b0 -> ... -> bm -> cn
   compose cs bs f g : c0 ... cn-1 b0 ... bm -> d
 *)
Fixpoint compose (cs : list Type) {ci d : Type} (bs : list Type) 
  : (arr cs (ci -> d)) -> (arr bs ci) -> (arr cs (arr bs d)) := match cs with
  | nil => fun f g => compose' bs f g
  | c :: cs => fun f g x => compose cs bs (f x) g end.

Lemma compose_equation_1 {ci d : Type} {bs : list Type}:
  @compose nil ci d bs = compose' bs.
Proof.
reflexivity.
Qed.

Lemma compose_equation_2 {ci d c : Type} {bs cs : list Type} {f : arr (c :: cs) (ci -> d)} {g : arr bs ci} : 
  compose (c :: cs) bs f g = fun x => compose cs bs (f x) g.
Proof.
reflexivity.
Qed.

(* This is a useful equality of types. We give it a name to refer to it in typecasts. *)
Lemma arr_append {l1 l2 : list Type} {d : Type} : arr (l1 ++ l2) d = arr l1 (arr l2 d).
Proof.
induction l1 as [|h l1 IH].
- rewrite app_nil_l. reflexivity.
- rewrite <- app_comm_cons. rewrite arr_equation_2. rewrite IH. reflexivity.
Qed.

(* And occasionally useful to apply it twice. We give this a name too. *)
Lemma double_arr_append {l1 l2 l3 : list Type} {d : Type} : 
  arr (l1 ++ l2 ++ l3) d = arr l1 (arr l2 (arr l3 d)).
Proof.
rewrite !arr_append. reflexivity.
Qed.


(*We now define the multicomposition structure as an operad. *)

(*Note that the type associated with O (d , cs) is precisely arr cs d, so we construct a 
function that reverses the arguments of arr, and use that to construct the operad.*)

Definition arr_rev (t' : Type) (ts : list Type) : Type := arr ts t'.

Definition setsOp : Operad := {| interp := arr_rev |}.

(*The units for our operad are identity functions: *)
Definition setsId (d : Type) : ( setsOp 〘 d, (d :: nil) 〙 ) := id.

(*The composition map is multicomposition as defined above.*)
(*Since the composition map is defined in terms of a product (A * B) -> C, 
and compose is defined as A -> B -> C, we need a way to translate one to the other.*)
Definition prod_map {A B C : Type} (f : A -> B -> C) (x : (A * B)) : C := f (fst x) (snd x).

(* We will also need to typecast various formulations involving the arr function. *)

(* This is the equality needed to typecast on the RHS of the composition definition: *)
Lemma insert_arr {i : nat} {d : Type} {c b : list Type} :
  arr (firstn i c) (arr b (arr (skipn (i + 1) c) d)) = arr (insert i c b) d.
Proof.
symmetry. apply double_arr_append.
Qed.

(* And this is the equality needed to typecast on the LHS: *)
Lemma fn_arr {i n : nat} {d ci : Type} {c : list Type} {l : length c = n} {n1 : 1 <= n} 
  {il : i < n} (p : lookupT i c = ci) : 
  arr (firstn i c) (ci -> (arr (skipn (i + 1) c) d)) = arr c d.
Proof.
rewrite <- arr_equation_2. rewrite <- arr_append. 
assert (ic: insert i c (ci :: nil) = c). apply (@unityRInsert unit c ci n i n1 il l p). 
assert (ii: firstn i c ++ ci :: skipn (i + 1) c = insert i c (ci :: nil)). reflexivity.
rewrite ii. rewrite ic. reflexivity.
Qed.

(* The typecast for the RHS: *)
Definition insertCast {i : nat} {d : Type} {c b : list Type}
  (e : (arr (firstn i c) (arr b (arr (skipn (i + 1) c) d)))) : 
   (setsOp 〘d,insert i c b〙).
Proof.
rewrite insert_arr in e. apply e.
Defined.

(* The typecast for one component of the LHS: *)
Definition insertCast0 {i n : nat} {d ci : Type} {c b : list Type} 
  {l : length c = n} {n1 : 1 <= n} {il : i < n} (p : lookupT i c = ci)
  (e : (setsOp 〘 d, c 〙) ) : 
  ((arr (firstn i c) (ci -> arr (skipn (i + 1) c) d)) ).
Proof.
rewrite (@fn_arr i n d ci c l n1 il p). apply e.
Defined.

(*The typecast for the full LHS:*)
Definition insertCast1 {i n : nat} {d ci : Type} {c b : list Type} 
  {l : length c = n} {n1 : 1 <= n} {il : i < n} (p : lookupT i c = ci)
  (e :  (setsOp 〘 d, c 〙) *  (setsOp 〘 ci, b 〙)) : 
   (arr (firstn i c) (ci -> arr (skipn (i + 1) c) d)) * (arr b ci) :=
(@insertCast0 i n d ci c b l n1 il p (fst e), snd e).

(* We are now ready to define the operad composition: *)
Definition setsComp (i : nat) {n : nat} {d ci : Type} {c : list Type} {b : list Type} 
  {l : length c = n} {n1 : 1 <= n} {il : i < n} {p : lookupT i c = ci} : 
  ( (setsOp 〘d,c〙) *  (setsOp 〘ci,b〙) -> 
           (setsOp 〘d,insert i c b〙)) :=    fun x => 
            insertCast ((prod_map (@compose (firstn i c) ci (arr (skipn (i + 1) c) d) b))
                (@insertCast1 i n d ci c b l n1 il p x)). 

(* Composing with an identity function returns the same function:*)
Lemma compose'_id {d : Type} {b : list Type} {g : arr b d} : compose' b (setsId d) g = g.
Proof.
induction b as [|h b IH].
- reflexivity. 
- rewrite compose'_equation_2.
  apply functional_extensionality. intros x. apply IH.
Qed.

(*The following lemmas show that the typecasts used in the operad definition are dep_typecasts, 
and therefore typecasts:*)
Lemma unityLCast_is_dept {operad : Operad} {d : Type} {c : list Type} :
  @unityLCast operad d c = dep_typecast 
        (PA := fun x => ( operad〘d,x〙))(eq:=(unityLInsert c)).
Proof.
reflexivity.
Qed.

Lemma unityLCast_is_typecast {operad : Operad}{d : Type} {c : list Type} :
  @unityLCast operad d c = typecast (DepTypeeq (PA:=(fun x => ( operad〘d,x〙))) (unityLInsert c)).
Proof.
rewrite unityLCast_is_dept. rewrite dep_typecast_is_typecast. reflexivity.
Qed.


Lemma unityRCast_is_dept {operad : Operad}{d ci:Type}{c: list Type}(n i: nat)(p: lookupT i c = ci)(q0: 1 <= n)
  (q1: i < n)(r: length c = n) :
  @unityRCast operad d ci c n i p q0 q1 r = dep_typecast (PA := fun x => (operad〘d,x〙)) 
    (eq:= (@unityRInsert unit c ci n i q0 q1 r p)).
Proof.
reflexivity.
Qed. 

Lemma unityRCast_is_typecast {operad : Operad}{d ci:Type}{c: list Type}(n i: nat)(p: lookupT i c = ci)(q0: 1 <= n)
  (q1: i < n)(r: length c = n) :
  @unityRCast operad d ci c n i p q0 q1 r = typecast (DepTypeeq (PA:= fun x => (operad〘d,x〙))
    (@unityRInsert unit c ci n i q0 q1 r p)).
Proof.
rewrite unityRCast_is_dept. rewrite dep_typecast_is_typecast. reflexivity.
Qed.

Lemma vertCast_is_dept{operad : Operad} {n m i j : nat}
          {d: Type} {a b c : list Type} {p0: 1 <= n}{p1 : 1 <= m}{p2: i < n} 
            {p3: j < m} {p4: length c = n}{p5: length b = m} :
  @vertCast operad n m i j d a b c p0 p1 p2 p3 p4 p5  = dep_typecast (PA := fun x => (operad〘d,x〙)) 
    (eq:= (vertInsert n m i j a b c p0 p1 p2 p3 p4 p5) ).
Proof.
reflexivity.
Qed.

Lemma vertCast_is_typecast{operad : Operad} {n m i j : nat}
          {d: Type} {a b c : list Type} {p0: 1 <= n}{p1 : 1 <= m}{p2: i < n} 
            {p3: j < m} {p4: length c = n}{p5: length b = m} :
  @vertCast operad n m i j d a b c p0 p1 p2 p3 p4 p5  = typecast (DepTypeeq (PA:= fun x => (operad〘d,x〙))
    (vertInsert n m i j a b c p0 p1 p2 p3 p4 p5)).
Proof.
rewrite vertCast_is_dept. rewrite dep_typecast_is_typecast. reflexivity.
Qed.

Lemma horizCast_is_dept{operad : Operad} {n m l i j : nat} {d : Type}
          {a b c : list Type} {q0 : 2 <= n} {q1 : 1<=m} {q2 : 1<=l} {p0: i<j} {p1: j<n}
          {s0 : length c = n} {s1 : length b = m} {s2 : length a = l} :
  @horizCast operad n m l i j a b c d q0 q1 q2 p0 p1 s0 s2 s1 = dep_typecast (PA:= fun x => (operad〘d,x〙))
    (eq:= @horizInsert Type n m l i j a b c q0 q1 q2 p0 p1 s0 s2 s1).
Proof.
reflexivity.
Qed.

Lemma horizCast_is_typecast{operad : Operad} {n m l i j : nat} {d : Type}
          {a b c : list Type} {q0 : 2 <= n} {q1 : 1<=m} {q2 : 1<=l} {p0: i<j} {p1: j<n}
          {s0 : length c = n} {s1 : length b = m} {s2 : length a = l} :
  @horizCast operad n m l i j a b c d q0 q1 q2 p0 p1 s0 s2 s1 = typecast (DepTypeeq  (PA:= fun x => (operad〘d,x〙))
    (@horizInsert Type n m l i j a b c q0 q1 q2 p0 p1 s0 s2 s1)).
Proof.
rewrite horizCast_is_dept. rewrite dep_typecast_is_typecast. reflexivity.
Qed.

Lemma insertCast_is_typecast {i : nat} {d : Type} {c b : list Type} :
  @insertCast i d c b = typecast insert_arr.
Proof.
reflexivity.
Qed.

Lemma insertCast0_is_typecast {i n : nat} {d ci : Type} {c b : list Type} 
  {l : length c = n} {n1 : 1 <= n} {il : i < n} {p : lookupT i c = ci} :
  @insertCast0 i n d ci c b l n1 il p = typecast 
  (eq_sym(@fn_arr i n d ci c l n1 il p)).
Proof.
reflexivity.
Qed.

(*We now lead up to showing that the left unity axiom is satisfied: *)
Lemma insertCast0_nil_is_id {d : Type} {b : list Type}: 
    @insertCast0 0 1 d d (d :: nil) b eq_refl (le_n 1) PeanoNat.Nat.lt_0_1 eq_refl = id.
Proof.
rewrite insertCast0_is_typecast. apply typecastAuto.
Qed.

(*Composition in our operad, with the operad identity in the first argument, is the identity:*)
Lemma setsComp_id {d : Type} (b : list Type) {e : (arr b d)} {eq : insert 0 (d :: nil) b = b} : 
    unityLCast( @setsComp 0 1 d d (d :: nil) b eq_refl (le_n 1) PeanoNat.Nat.lt_0_1 eq_refl 
                (setsId d, e) ) = e.
Proof.
unfold setsComp. unfold prod_map. simpl.
rewrite insertCast0_nil_is_id. rewrite compose'_id. 
rewrite unityLCast_is_typecast. rewrite insertCast_is_typecast. rewrite typecastCompose.
apply typecastSelf.
Qed.

(*The left unity axiom is satisfied:*)
Lemma sets_unityL (d : Type) (b : list Type) (e : ( setsOp 〘 d, b 〙 ) ) : 
  unityLCast(@setsComp 0 1 d d (d :: nil) b eq_refl (le_n 1) PeanoNat.Nat.lt_0_1 eq_refl (setsId d, e)) = e.
Proof.
apply setsComp_id. apply unityLInsert.
Qed.

(* Composing with an identity function in the second argument returns the same function: *)
Lemma compose_id {cs : list Type} {ci d : Type} (f : (arr cs (ci -> d))): 
    compose (d:=d) cs (ci::nil) f id = f.
Proof.
induction cs as [|h cs IH].
- rewrite compose_equation_1. apply (compose'_equation_2 (bs:=nil)).
- rewrite compose_equation_2. apply functional_extensionality. intros x. apply IH.
Qed.

(* The right unity axiom is satisfied: *)
Lemma sets_unityR (n i : nat) (d ci : Type) (c : list Type ) (p : lookupT i c = ci)(q0: 1 <= n)(q1: i < n) 
              (r: length c = n) (e : (setsOp〘d,c〙)) : 
  @unityRCast setsOp d ci c n i p q0 q1 r (@setsComp i n d ci c (ci::nil) r q0 q1 p (e, setsId ci)) = e.
Proof.
unfold setsComp. unfold prod_map. simpl. rewrite compose_id.
rewrite unityRCast_is_typecast. rewrite insertCast_is_typecast. rewrite insertCast0_is_typecast.
rewrite typecastCompose. rewrite typecastCompose.
apply typecastSelf.
Qed.

(*For the associativity axioms, we prove a series of lemmas about associativity of the compose functions.*)
(*First, compose' is associative with no intermediate types:*)
Lemma compose'assoc' {d ci bj : Type} {a : list Type}
  (f : bj -> ci) (g : (arr a bj)) (e : ci -> d) :
  compose' a e (compose' a f g) = compose' a (compose' (bj::nil) e f) g.
Proof.
induction a as [|h a IH].
- reflexivity.
- rewrite !compose'_equation_2. apply functional_extensionality. intros x. apply IH.
Qed.

(* compose' is associative with an intermediate type list: *)
Lemma compose'assoc {d ci bj : Type} {a b1 : list Type}
  (f : bj -> (arr b1 ci)) (g : arr a bj) (e : ci -> d) :
  compose' (a++b1) e (typecast (eq_sym arr_append) (compose' a f g)) = 
    typecast (eq_sym arr_append) (compose' a (compose' (bj::b1) e f) g).
Proof.
induction a as [|h a IH].
- simpl. rewrite !typecastSelf. reflexivity.
- simpl. apply functional_extensionality.  intros x.
  rewrite !(typecastFun (eq_sym arr_append)).
  apply IH.
Qed.

Lemma compose_assoc {c0 c1 b0 b1 a cb b :list Type} {d ci bj abcd : Type}
  (eqcb: cb = c0 ++ b0)
  (eqb : b = b0 ++ bj::b1)
  (eqabcd : abcd = arr b1 (arr c1 d))
  {eqf : Typeeq (arr b ci) (arr b0 (bj -> arr b1 ci))}
  {eqcef:Typeeq (arr c0 (arr b (arr c1 d))) (arr (cb) (bj -> abcd))}
  {eqcfg:Typeeq (arr b0 (arr a (arr b1 ci))) (arr (b0++a++b1) ci)}
  {eqt : Typeeq (arr c0 (arr (b0++a++b1) (arr c1 d))) (arr (cb) (arr a abcd))}
   (e : arr c0 (ci -> (arr c1 d))) (f : arr b ci) (g : arr a bj):
  compose cb a (typecast eqcef (compose c0 b e f)) g = 
      typecast eqt (compose c0 (b0++a++b1) e (typecast eqcfg (compose b0 a (typecast eqf f) g))).
Proof.
revert eqf eqcef eqcfg eqt f. rewrite eqcb. rewrite eqabcd. rewrite eqb.
intros eqf eqcef eqcfg eqt f. clear eqcb eqabcd eqb cb abcd b.
induction c0 as [|hc0 c0 IHc0].
- simpl. induction b0 as [|hb0 b0 IHb0].
  + simpl. rewrite !typecastSelf.
    retypecast eqcfg (eq_sym (@arr_append a b1 ci)). rewrite compose'assoc.
    rewrite typecastCompose. symmetry. apply typecastSelf.
  + simpl. apply functional_extensionality. intros x.
    rewrite (typecastFun (@arr_append b0 (bj::b1) (arr c1 d))).
    rewrite (typecastFun double_arr_append).
    rewrite (typecastFun (eq_sym double_arr_append)).
    rewrite (typecastFun (@arr_append b0 (bj::b1) ci)).
    apply IHb0.
- simpl. apply functional_extensionality. intros x.
  assert (eqcefI : Typeeq (arr c0 (arr (b0 ++ bj :: b1) (arr c1 d)))
                    (arr (c0 ++ b0) (bj -> arr b1 (arr c1 d)))).
    rewrite !arr_append. reflexivity.
  rewrite (typecastFun eqcefI).
  assert (eqtI : Typeeq (arr c0 (arr (b0 ++ a ++ b1) (arr c1 d)))
                  (arr (c0 ++ b0) (arr a (arr b1 (arr c1 d))))).
    rewrite !arr_append. reflexivity.
  rewrite (typecastFun eqtI).
  apply IHc0.
Qed.

(* Vertical associativity axiom is satisfied: *)
Lemma sets_vertAssoc (n m l i j : nat) (d ci bj : Type)
          (a b c : list Type) 
          (p0: 1 <= n )(p1 : 1 <= m) (p2 : 1 <= l)
          (q0 : lookupT i c = ci) (q1 : lookupT j b = bj)
          (r0: i < n)(r1: j < m) 
          (s0: length c = n)(s1: length b = m)(s2: length a = l)
          (e : (setsOp 〘d,c〙)) (f : (setsOp 〘ci, b〙)) (g : (setsOp 〘bj, a〙)): 
 @vertCast setsOp n m i j d a b c p0 p1 r0 r1 s0 s1 
        (@setsComp (i+j) (n+m-1) d bj (insert i c b) a (insertlength s0 s1 r0) (n_sum_ineq p0 p1) (i_sum_ineq r0 r1) (vertLookup q1 r0 r1 s0 s1)
              (@setsComp i n d ci c b s0 p0 r0 q0 (e, f), g)) = 
  @setsComp i n d ci c (insert j b a) s0 p0 r0 q0 (e, @setsComp j m ci bj b a s1 p1 r1 q1 (f, g)).
Proof.
unfold setsComp. unfold prod_map. simpl.
rewrite vertCast_is_typecast. rewrite !insertCast_is_typecast. rewrite !insertCast0_is_typecast.
rewrite typecastsym. rewrite typecastsym. rewrite typecastCompose. rewrite typecastCompose. rewrite typecastCompose.
apply compose_assoc.
- apply (vertH1 n m). assumption. assumption. assumption. assumption.
- assert (B' : bj::(skipn (j+1) b) = skipn j b). {
    clear q0 r0 s0 s2 e f g.
    generalize dependent b. generalize dependent m. induction j.
    - sauto.
    - intros m p1 r1 b q1 s1.
      destruct b as [| b0 b].
      + sauto.
      + rewrite skipn_cons. rewrite plus_Sn_m. rewrite skipn_cons.
        apply (IHj (pred m)). sauto. sauto. sauto. sauto. }
  rewrite B'. symmetry. apply firstn_skipn.
- rewrite <- arr_append. f_equal. 
  apply (vertH2 n m). assumption. assumption. assumption. assumption.
Qed.

(* Compose associativity lemma for the horizontal direction, with equivalences built in:*)
Lemma compose_horizAssoc {a b c c0 c0' c1 c2 c2' c0a1 c0i1 c1b2 c1j2 : list Type} {d ci cj : Type}
     (c0eq : c0' = c0)
     (c2eq : c2' = c2)
     (eqa : c0a1 = c0 ++ a ++ c1)
     (eqi : c0i1 = c0 ++ ci::c1)
     (eqb : c1b2 = c1 ++ b ++ c2)
     (eqj : c1j2 = c1 ++ cj::c2)
     (eqc : c = c0 ++ (ci::c1) ++ (cj::c2))
     {eqc0 : arr c d = arr c0 (ci -> (arr c1j2 d))}
     {eqc1 : arr c d = arr c0i1 (cj -> (arr c2 d))}
     {eqcef : arr c0 (arr a (arr c1j2 d)) = arr c0a1 (cj -> (arr c2' d))}
     {eqceg : arr c0i1 (arr b (arr c2 d)) = arr c0' (ci -> (arr c1b2 d))}
     {eqt : arr c0' (arr a (arr c1b2 d)) = arr c0a1 (arr b (arr c2' d))}
     (e : setsOp〘d,c〙)
     (f : setsOp〘ci,a〙)
     (g : setsOp 〘cj,b〙) :
  compose c0a1 b (typecast eqcef (compose c0 a (typecast eqc0 e) f)) g
  = typecast eqt (compose c0' a 
          (typecast eqceg (compose c0i1 b (typecast eqc1 e) g)) f).
Proof.
revert eqc0 eqc1 eqcef eqceg eqt e. rewrite c0eq. rewrite c2eq. rewrite eqa. rewrite eqi. rewrite eqb. rewrite eqj. rewrite eqc. 
intros eqc0 eqc1 eqcef eqceg eqt e. clear c0eq c2eq eqa eqi eqb eqj eqc c0a1 c0i1 c1b2 c1j2 c.
induction c0 as [|hc0 tc0 IHc0].
- simpl in eqc0. simpl in eqc1.
  induction a as [|ha0 a0 IHa0].
  + simpl in eqcef. simpl in eqt. simpl in eqceg. 
    simpl.
    rewrite (typecastFun (eq_sym double_arr_append)).
    rewrite typecastCompose. rewrite !typecastSelf.
    f_equal. symmetry. apply typecastFun.
  + simpl in IHa0. simpl.
    apply functional_extensionality. intros x.
    assert (eqcefI : arr a0 (arr (c1 ++ cj :: c2) d) =
                  arr (a0 ++ c1) (cj -> arr c2 d)).
      rewrite !arr_append. reflexivity.
    rewrite (typecastFun eqcefI).
    assert (eqtI : arr a0 (arr (c1 ++ b ++ c2) d) =
                arr (a0 ++ c1) (arr b (arr c2 d))).
      rewrite !arr_append. reflexivity.
    rewrite (typecastFun eqtI).
    apply IHa0.
- apply functional_extensionality. intros x. simpl.
  assert (eqcefI : arr tc0 (arr a (arr (c1 ++ cj :: c2) d)) =
                  arr (tc0 ++ a ++ c1) (cj -> arr c2 d)).
      rewrite !arr_append. reflexivity.
  rewrite (typecastFun eqcefI).
  assert (eqtI : arr tc0 (arr a (arr (c1 ++ b ++ c2) d)) =
                arr (tc0 ++ a ++ c1) (arr b (arr c2 d))).
      rewrite !arr_append. reflexivity.
  rewrite (typecastFun eqtI).
  assert (eqcegI : arr (tc0 ++ ci :: c1) (arr b (arr c2 d)) =
                  arr tc0 (ci -> arr (c1 ++ b ++ c2) d)).
      rewrite !arr_append. reflexivity.
  rewrite (typecastFun eqcegI).
  assert (eqc0I : arr (tc0 ++ (ci :: c1) ++ cj :: c2) d =
                 arr tc0 (ci -> arr (c1 ++ cj :: c2) d)).
      rewrite !arr_append. reflexivity.
  rewrite (typecastFun eqc0I).
  assert (eqc1I : arr (tc0 ++ (ci :: c1) ++ cj :: c2) d =
                 arr (tc0 ++ ci :: c1) (cj -> arr c2 d)).
      rewrite !arr_append. reflexivity.
  rewrite (typecastFun eqc1I).
  apply IHc0.
Qed.

(* Horizontal associativity axiom is satisfied:*)
Lemma sets_horizAssoc : forall (n m l i j : nat) (d ci cj : Type) 
          (a b c : list Type ) 
          (p0 : i < j)(p1 : j < n)
          (q0: 2 <= n)(q1: 1 <= m)(q2: 1 <= l) 
          (r0 : lookupT i c = ci) (r1 : lookupT j c = cj)
          (s0: length c = n)(s1: length b = m)(s2: length a = l)
          (e : setsOp〘d,c〙) (f : setsOp〘ci,a〙)
          (g : setsOp 〘cj,b〙),
        @horizCast setsOp n m l i j a b c d q0 q1 q2 p0 p1 s0 s2 s1 
        (@setsComp (l-1+j) (n+l-1) d cj (insert i c a) b (insertlength s0 s2 (PeanoNat.Nat.lt_trans i j n p0 p1))
                 (n_sum_ineq (n_ge2_ineq q0) q2) (i_addl1_ineq q2 p1) (horizLookupR p0 p1 q2 r1 s0 s2)
        (@setsComp i n d ci c a s0 (n_ge2_ineq q0) (PeanoNat.Nat.lt_trans i j n p0 p1) r0 (e, f), g)) = 
        @setsComp i (n+m-1) d ci (insert j c b) a (insertlength s0 s1 p1) (n_sum_ineq (n_ge2_ineq q0) q1) (i_trans_ineq p0 p1 q1) (horizLookupL p0 p1 r0 s0) 
        (@setsComp j n d cj c b s0 (n_ge2_ineq q0) p1 r1 (e, g), f).
Proof.
intros n m l i j d ci cj a b c p0 p1 q0 q1 q2 r0 r1 s0 s1 s2 e f g.
rewrite !horizCast_is_typecast.
unfold setsComp. unfold prod_map. simpl.
rewrite !insertCast_is_typecast. rewrite !insertCast0_is_typecast.
rewrite !typecastsym. rewrite !typecastCompose.
assert (HJ : forall L, skipn (i+1) (firstn j c) ++ L = skipn (i+1) (firstn j c ++ L)).
      intros L. rewrite skipn_app. f_equal. rewrite firstn_length. rewrite s0.
      assert (H : i + 1 - min j n = 0). sauto. rewrite H. apply skipn_O.
apply (compose_horizAssoc(c1:=skipn (i + 1) (firstn j c))).
- apply (horizH3 n m i j b c q0 q1 p0 p1 s0 s1).
- apply (horizH2 n l i j a c q0 q2 p0 p1 s0 s2).
- apply (horizH1 n l i j a c q0 q2 p0 p1 s0 s2).
- assert (H : firstn i c = firstn i (firstn j c)).
      rewrite firstn_firstn. f_equal. sauto.
  rewrite H. clear H HJ.
  assert (s4 : length (firstn j c) = j). rewrite firstn_length. sauto.
  assert (r4 : lookupT i (firstn j c) = ci). {
      clear r1 s1 s2 e f g.
      generalize dependent c.  generalize dependent ci. generalize dependent j. 
      generalize dependent n. induction i as [|i IHi].
      + intros n q0 j p0 p1 ci c r0 s0 s4. rewrite <- r0. destruct j.
        * sauto.
        * sauto.
      + intros n q0 j p0 p1 ci c r0 s0 s4. destruct c as [|h c].
        * sauto.
        * assert (H : firstn j (h :: c) = h :: firstn (pred j) c).
              assert (H' : j = S (pred j)). sauto. rewrite H'. sauto. rewrite H.
          apply (IHi (pred n)). sauto. sauto. sauto. sauto. sauto.
          rewrite firstn_length. sauto. } 
  symmetry. apply (@unityRInsert unit (firstn j c) ci j i (n_gt_ineq p0) p0 s4 r4).
- apply (horizH4 n m i j b c q0 q1 p0 p1 s0 s1).
- rewrite HJ. f_equal. symmetry. apply (@unityRInsert unit c cj n j (n_ge2_ineq q0) p1 s0 r1).
- rewrite <- app_comm_cons. rewrite HJ.
  assert (H: firstn j c ++ cj:: skipn (j+1) c = c).
      apply (@unityRInsert unit c cj n j (n_ge2_ineq q0) p1 s0 r1).
  rewrite H. symmetry.
  apply (@unityRInsert unit c ci n i (n_ge2_ineq q0) (PeanoNat.Nat.lt_trans i j n p0 p1) s0 r0).
Qed.

(*Some lemmas about isomorphism and function composition:*)
Lemma isoSelf {X : Type} : iso X X.
Proof.
exists id. exists id. split. reflexivity. reflexivity.
Qed.

Lemma isoFun {X Y Z : Type} : iso X Y -> iso (Z -> X) (Z -> Y).
Proof.
intros H. destruct H as [f H]. destruct H as [g H].
exists (fun F => (fun z => f (F z))).
exists (fun G => (fun z => g (G z))).
destruct H as [Hfg Hgf].
split.
- unfold comp. unfold comp in Hfg.
  apply functional_extensionality. intros G.
  apply functional_extensionality. intros z.
  apply (equal_f Hfg).
- unfold comp. unfold comp in Hgf.
  apply functional_extensionality. intros F.
  apply functional_extensionality. intros z.
  apply (equal_f Hgf).
Qed.

Lemma compassoc {A B C D} (f : A->B) (g: B->C) (h: C->D) : comp h (comp g f) = comp (comp h g) f.
Proof.
reflexivity.
Qed.

Lemma comp_f_id {A B} (f : A->B) : comp f id = f.
Proof.
reflexivity.
Qed.

Lemma isoTrans {X Y Z : Type} : iso X Y -> iso Y Z -> iso X Z.
Proof.
intros iXY iYZ.
destruct iXY as [fXY iXY]. destruct iYZ as [fYZ iYZ].
destruct iXY as [gXY iXY]. destruct iYZ as [gYZ iYZ].
destruct iXY as [fgXY gfXY]. destruct iYZ as [fgYZ gfYZ].
exists (comp fYZ fXY). exists (comp gXY gYZ). split.
- rewrite compassoc. rewrite <- (compassoc gXY fXY fYZ). rewrite fgXY.
  rewrite comp_f_id. apply fgYZ.
- rewrite compassoc. rewrite <- (compassoc fYZ gYZ gXY). rewrite gfYZ.
  rewrite comp_f_id. apply gfXY.
Qed.

(*Permutation axiom is satisfied:*)
Lemma setsPerm : forall (c c': list Type)(d : Type)
   (p: 1 <= length c ),
  Permutation c c' -> iso (setsOp〘d, c〙) (setsOp〘d, c'〙).
Proof.
intros c c' d l p.
induction p as [| h c c' | h h' c | c c' c'' p1 IHp1].
- apply isoSelf.
- destruct c.
  + rewrite (Permutation_nil p). apply isoSelf.
  + assert (L : 1 <= length (h::c)). sauto. apply (isoFun (IHp L)).
- exists (fun F => (fun X => (fun Y => F Y X))).
  exists (fun G => (fun Y => (fun X => G X Y))).
  split. reflexivity. reflexivity.
- assert (l' : 1 <= length c'). rewrite (Permutation_length p1) in l. apply l.
  apply (isoTrans (IHp1 l) (IHp2 l')).
Qed.

(*Final statement showing that all operad laws are satisfied:*)
Definition setsLaws : operadLaws setsOp := {|
  opId := setsId;
  operadComp := setsComp;
  unityL := sets_unityL;
  unityR := sets_unityR;
  vertAssoc := sets_vertAssoc;
  horizAssoc := sets_horizAssoc;
  perm := setsPerm |}.