on pp

src/AbstractBigraphs.v

@@ -262,7 +262,8 @@ Definition merge {n:nat} : bigraph n EmptyNDL 1 EmptyNDL.
   
 Definition big_1 := @merge 0.
 
-Definition symmetry_big (m:nat) (X:NoDupList) (n:nat) (Y:NoDupList) :
+Definition symmetry_big (m:nat) (X:NoDupList) (n:nat) (Y:NoDupList) 
+  {dis:X#Y}:
   bigraph (m+n) (X ∪ Y) (m+n) (X ∪ Y).
   Proof. 
     eapply (@Big (m+n) (X ∪ Y) (m+n) (X ∪ Y)

src/Composition.v

@@ -231,104 +231,67 @@ Theorem bigraph_comp_assoc : forall {s1 i1 r1 o1 s2 r2 r3 i2 o2 s3 i3 o3}
   Qed.
 End C2.
 
-(** Congruence of composition *)
-Definition arity_comp_congruence_forward 
-  {s1 i1 r1 o1 s2 i2 r2 o2 s3 r3 r4 i3 o3 s4 i4 o4} 
-  {p13 : PermutationinfTs (ndlist i1) (ndlist o3)}
-  {p24 : PermutationinfTs (ndlist i2) (ndlist o4)}
-  {eqs1r3 : MyEqNat s1 r3} {eqs2r4 : MyEqNat s2 r4}
-  (b1 : bigraph s1 i1 r1 o1) 
-  (b2 : bigraph s2 i2 r2 o2) 
-  (b3 : bigraph s3 i3 r3 o3) 
-  (b4 : bigraph s4 i4 r4 o4) 
-  (bij_n12 : bijection ((get_node b1)) ((get_node b2))) (bij_n34 : bijection ((get_node b3)) ((get_node b4)))
-  (bij_p12 : forall (n1 : (get_node b1)), bijection ('I_(Arity (get_control (bg:=b1) n1))) ('I_(Arity (get_control (bg:=b2) (bij_n12 n1)))))
-  (bij_p34 : forall (n3 : (get_node b3)), bijection ('I_(Arity (get_control (bg:=b3) n3))) ('I_(Arity (get_control (bg:=b4) (bij_n34 n3)))))
-  (n13 : (get_node (b1 <<o>> b3))) :
-  ('I_ (Arity (get_control (bg:=b1 <<o>> b3) n13))) -> 
-  ('I_ (Arity (get_control (bg:=b2 <<o>> b4) ((bij_n12 <+> bij_n34) n13)))).
+Definition bij_congruence_forward
+  {n1 n2 n3 n4} {c1 c2 c3 c4} 
+  (bij_n12 : bijection (n1) (n2)) (bij_n34 : bijection (n3) (n4))
+  (bij_p12 : forall (n' : n1), bijection ('I_(Arity (c1 n'))) ('I_(Arity (c2 (bij_n12 n')))))
+  (bij_p34 : forall (n' : n3), bijection ('I_(Arity (c3 n'))) ('I_(Arity (c4 (bij_n34 n'))))):
+  forall n' : n1 + n3,
+  'I_(Arity (join (c1) (c3) n')) ->
+  'I_(Arity (join (c2) (c4)
+    ((bij_n12 <+> bij_n34) n'))).
   Proof. (*s1 = r3*) (*s2 = r4*)
-  destruct n13 as [n1 | n3].
-  + simpl. exact (bij_p12 n1).
-  + exact (bij_p34 n3).
-  Defined.
+  destruct n' as [n' | n'].
+  + exact (bij_p12 n').
+  + exact (bij_p34 n').
+  Defined. (*TODO : is it join? is it |||?*)
 
-Definition arity_comp_congruence_backward
-  {s1 i1 r1 o1 s2 i2 r2 o2 s3 r3 r4 i3 o3 s4 i4 o4} 
-  {p13 : PermutationinfTs (ndlist i1) (ndlist o3)}
-  {p24 : PermutationinfTs (ndlist i2) (ndlist o4)}
-  {eqs1r3 : MyEqNat s1 r3} {eqs2r4 : MyEqNat s2 r4}
-  (b1 : bigraph s1 i1 r1 o1) 
-  (b2 : bigraph s2 i2 r2 o2) 
-  (b3 : bigraph s3 i3 r3 o3) 
-  (b4 : bigraph s4 i4 r4 o4) 
-  (bij_n12 : bijection ((get_node b1)) ((get_node b2))) (bij_n34 : bijection ((get_node b3)) ((get_node b4)))
-  (bij_p12 : forall (n1 : (get_node b1)), bijection ('I_(Arity (get_control (bg:=b1) n1))) ('I_(Arity (get_control (bg:=b2) (bij_n12 n1)))))
-  (bij_p34 : forall (n3 : (get_node b3)), bijection ('I_(Arity (get_control (bg:=b3) n3))) ('I_(Arity (get_control (bg:=b4) (bij_n34 n3)))))
-  (n13 : (get_node (b1 <<o>> b3))) :
-  ('I_(Arity (get_control (bg:=b2 <<o>> b4) ((bij_n12 <+> bij_n34) n13)))) -> 
-  ('I_(Arity (get_control (bg:=b1 <<o>> b3) n13))).
+
+Definition bij_congruence_backward
+  {n1 n2 n3 n4} {c1 c2 c3 c4} 
+  (bij_n12 : bijection (n1) (n2)) (bij_n34 : bijection (n3) (n4))
+  (bij_p12 : forall (n' : n1), bijection ('I_(Arity (c1 n'))) ('I_(Arity (c2 (bij_n12 n')))))
+  (bij_p34 : forall (n' : n3), bijection ('I_(Arity (c3 n'))) ('I_(Arity (c4 (bij_n34 n'))))):
+  forall n' : n1 + n3,
+  'I_(Arity (join c2 c4
+    ((bij_n12 <+> bij_n34) n'))) ->
+  'I_(Arity (join c1 c3 n')).
   Proof.
-  destruct n13 as [n1 | n3].
-  + exact (backward (bij_p12 n1)).
-  + exact (backward (bij_p34 n3)).
+  destruct n' as [n' | n'].
+  + exact (backward (bij_p12 n')).
+  + exact (backward (bij_p34 n')).
   Defined.
 
-Lemma arity_comp_congruence : forall 
-  {s1 i1 r1 o1 s2 i2 r2 o2 s3 r3 r4 i3 o3 s4 i4 o4} 
-  {p13 : PermutationinfTs (ndlist i1) (ndlist o3)}
-  {p24 : PermutationinfTs (ndlist i2) (ndlist o4)}
-  {eqs1r3 : MyEqNat s1 r3} {eqs2r4 : MyEqNat s2 r4}
-  (b1 : bigraph s1 i1 r1 o1) 
-  (b2 : bigraph s2 i2 r2 o2) 
-  (b3 : bigraph s3 i3 r3 o3) 
-  (b4 : bigraph s4 i4 r4 o4) 
-  (bij_n12 : bijection ((get_node b1)) ((get_node b2))) (bij_n34 : bijection ((get_node b3)) ((get_node b4)))
-  (bij_p12 : forall (n1 : (get_node b1)), bijection ('I_(Arity (get_control (bg:=b1) n1))) ('I_(Arity (get_control (bg:=b2) (bij_n12 n1)))))
-  (bij_p34 : forall (n3 : (get_node b3)), bijection ('I_(Arity (get_control (bg:=b3) n3))) ('I_(Arity (get_control (bg:=b4) (bij_n34 n3)))))
-  (n13 : (get_node (b1 <<o>> b3))),
+Lemma bij_congruence : forall 
+  {n1 n2 n3 n4} {c1 c2 c3 c4} 
+  (bij_n12 : bijection (n1) (n2)) 
+  (bij_n34 : bijection (n3) (n4))
+  (bij_p12 : 
+    forall (n' : n1), bijection ('I_(Arity (c1 n'))) ('I_(Arity (c2 (bij_n12 n')))))
+  (bij_p34 : 
+    forall (n' : n3), bijection ('I_(Arity (c3 n'))) ('I_(Arity (c4 (bij_n34 n'))))),
+  forall n' : n1 + n3,
   bijection 
-  ('I_(Arity (get_control (bg:=b1 <<o>> b3) n13))) 
-  ('I_(Arity (get_control (bg:=b2 <<o>> b4) ((bij_n12 <+> bij_n34) n13)))).
+  'I_(Arity ((join c1 c3) n'))
+  'I_(Arity ((join c2 c4)
+    ((bij_n12 <+> bij_n34) n'))).
   Proof.
-  intros until n13.
+  intros until n'.
   apply (mkBijection _ _ 
-    (arity_comp_congruence_forward b1 b2 b3 b4 bij_n12 bij_n34 bij_p12 bij_p34 n13) (arity_comp_congruence_backward b1 b2 b3 b4 bij_n12 bij_n34 bij_p12 bij_p34 n13)).
-  + destruct n13 as [n1 | n3]; simpl.
-    - rewrite <- (fob_id _ _ (bij_p12 n1)).
+    (bij_congruence_forward bij_n12 bij_n34 bij_p12 bij_p34 n') 
+    (bij_congruence_backward bij_n12 bij_n34 bij_p12 bij_p34 n')).
+  + destruct n' as [n' | n']; simpl.
+    - rewrite <- (fob_id _ _ (bij_p12 n')).
       reflexivity.
-    - rewrite <- (fob_id _ _ (bij_p34 n3)).
+    - rewrite <- (fob_id _ _ (bij_p34 n')).
       reflexivity.
-  + destruct n13 as [n1 | n3]; simpl.
-    - rewrite <- (bof_id _ _ (bij_p12 n1)).
+  + destruct n' as [n' | n']; simpl.
+    - rewrite <- (bof_id _ _ (bij_p12 n')).
       reflexivity.
-    - rewrite <- (bof_id _ _ (bij_p34 n3)).
+    - rewrite <- (bof_id _ _ (bij_p34 n')).
       reflexivity.
   Defined.
 
-
-Lemma arity_comp_congruence' : forall 
-  {s1 i1 r1 o1 s2 i2 r2 o2 s3 r3 r4 i3 o3 s4 i4 o4} 
-  {p13 : PermutationinfTs (ndlist i1) (ndlist o3)}
-  {p24 : PermutationinfTs (ndlist i2) (ndlist o4)}
-  {eqs1r3 : MyEqNat s1 r3} {eqs2r4 : MyEqNat s2 r4}
-  (b1 : bigraph s1 i1 r1 o1) 
-  (b2 : bigraph s2 i2 r2 o2) 
-  (b3 : bigraph s3 i3 r3 o3) 
-  (b4 : bigraph s4 i4 r4 o4) 
-  (bij_n12 : bijection ((get_node b1)) ((get_node b2))) (bij_n34 : bijection ((get_node b3)) ((get_node b4)))
-  (bij_p12 : forall (n1 : (get_node b1)), bijection ('I_(Arity (get_control (bg:=b1) n1))) ('I_(Arity (get_control (bg:=b2) (bij_n12 n1)))))
-  (bij_p34 : forall (n3 : (get_node b3)), bijection ('I_(Arity (get_control (bg:=b3) n3))) ('I_(Arity (get_control (bg:=b4) (bij_n34 n3)))))
-  (n13 : (get_node (b1 <<o>> b3))),
-  Arity (get_control (bg:=b1 <<o>> b3) n13) =
-  Arity (get_control (bg:=b2 <<o>> b4) ((bij_n12 <+> bij_n34) n13)).
-  intros.
-  destruct n13; bunfold; simpl; bunfold.
-  f_equal.
-  specialize (bij_p12 s0).
-  
-   Admitted.
-
 Theorem bigraph_comp_congruence : forall 
   { s1 i1 r1 o1 s2 i2 r2 o2 s3 r3 r4 i3 o3 s4 i4 o4} 
   { p13 : PermutationinfTs (ndlist i1) (ndlist o3)}
@@ -358,7 +321,7 @@ Theorem bigraph_comp_congruence : forall
     (bij_o12)
     (bij_n12 <+> bij_n34)
     (bij_e12 <+> bij_e34)
-    (arity_comp_congruence b1 b2 b3 b4 _ _ bij_p12 bij_p34)
+    (fun n => bij_congruence bij_n12 bij_n34 bij_p12 bij_p34 n)
   );
   subst_ eqs1r3. 
   + apply functional_extensionality.

src/Disjointness.v

+Set Warnings "-notation-overridden, -notation-overriden, -masking-absolute-infT".
+
+Require Import Coq.Lists.List.
+Require Import Coq.Program.Equality.
+Require Import Bijections.
+Require Import MyBasics.
+
+Require Import FunctionalExtensionality.
+Require Import ProofIrrelevance.
+
+Require Import Coq.Sorting.Permutation.
+Require Import Coq.Classes.CRelationClasses.
+
+From mathcomp Require Import all_ssreflect.
+
+
+Import ListNotations.
+Require Import Names.
+
+
+Definition np : InfType.
+Module n := infTs np.
+Import np.
+
+
+End DisjointM.
\ No newline at end of file

src/LinkAxioms.v

@@ -31,7 +31,7 @@ Import tp c leb eb b b.n b.s n s.
 Set Typeclasses Unique Instances.
 Set Typeclasses Iterative Deepening.
 
-
+(******************* 1 ***********************)
 Lemma sub_eq_id : forall x, 
   support_equivalence
     (substitution (OneelNDL x) x)
@@ -71,6 +71,8 @@ Lemma sub_eq_id : forall x,
     - elim H.
   Qed.
 
+
+(******************* 2 ***********************)
 Definition bij_void_edges: forall x, 
   bijection
     (get_edge (lean (closure x <<o>> substitution EmptyNDL x)))
@@ -132,7 +134,7 @@ Lemma closure_o_subst_neutral : forall x,
   Qed.
 
   
-(*Note that a closure /x ◦ G may create an idle edge, if x is an idle name of G. Intuitively idle edges are ‘invisible’, and indeed we shall see later how to ignore them.*)
+(******************* 3 ***********************)
 Lemma closure_o_sub_eq_closure : forall x y, 
   support_equivalence
     (closure y <<o>> substitution (OneelNDL x) y)
@@ -161,20 +163,8 @@ Lemma closure_o_sub_eq_closure : forall x y,
   Qed. 
 
 Set Typeclasses Debug.
-Class NotIn (x : infT) (l : list infT) := notin_proof : ~ In x l.
-
-#[export] Instance disj_OneEl (n:infT) (l : NoDupList) (not_in : NotIn n l):
-  DisjointinfTs l (OneelNDL n).
-  Proof.
-  constructor.
-  intros n' Hn' H'.
-  simpl in H'. destruct H'.
-  - subst n. contradiction.
-  - apply H.
-  Qed.
-
-(*choose, either not in becomes a class, or it does not and bc it's a prop typeclass does not find it*)
 
+(******************* 4 ***********************)
 Lemma link_axiom_4 {y z X} {Y:NoDupList}  {disYX: Y # X} {disyY : NotIn y Y}: 
   support_equivalence
     (substitution (Y ∪ (OneelNDL y)) z <<o>> 

src/MyEqNat.v

@@ -16,14 +16,20 @@ Ltac subst_ H :=
   reflexivity. 
   Qed.
 
-(* #[export] Instance MyEqNat_add {s1 s2 r3 r4} (eqs2r4 : MyEqNat s2 r4) (eqs1r3 : MyEqNat s1 r3) : 
+#[export] Instance MyEqNat_add {s1 s2 r3 r4} 
+  (eqs2r4 : MyEqNat s2 r4) (eqs1r3 : MyEqNat s1 r3) : 
   MyEqNat (s1 + s2) (r3 + r4).
   Proof. 
   subst_ eqs1r3.
   subst_ eqs2r4. reflexivity.
   Qed.
 
-#[export] Instance MyEqNat_add_bis {s1 r3 s2 r4} (eqs2r4 : MyEqNat s2 r4) (eqs1r3 : MyEqNat s1 r3) : 
+Definition myEqNatproof {mI mJ mK:nat} : 
+  MyEqNat 
+  (mI + mK + mJ) (mI + (mJ + mK)).
+  Proof. auto. symmetry. rewrite addnC. rewrite addnCAC. reflexivity. Qed.
+
+(*#[export] Instance MyEqNat_add_bis {s1 r3 s2 r4} (eqs2r4 : MyEqNat s2 r4) (eqs1r3 : MyEqNat s1 r3) : 
   MyEqNat (s1 + s2) (r3 + r4).
   Proof. 
   subst_ eqs2r4.

src/PlaceAxioms.v

@@ -34,12 +34,12 @@ Set Typeclasses Iterative Deepening.
 
 Lemma place_axiom_join_sym1_1 : 
   support_equivalence
-    (join_big <<o>> symmetry_big 1 EmptyNDL 1 EmptyNDL)
+    (join_big <<o>> @symmetry_big 1 EmptyNDL 1 EmptyNDL _)
     join_big.
   Proof.
   apply (
     SupEq _ _ _ _ _ _ _ _
-      (join_big <<o>> symmetry_big 1 EmptyNDL 1 EmptyNDL)
+      (join_big <<o>> @symmetry_big 1 EmptyNDL 1 EmptyNDL _)
       join_big
       (erefl) (*s*)
       (permutation_id _) (*i*)

src/Symmetries.v

@@ -45,13 +45,13 @@ Lemma arity_of_void : forall n n',
 
   Theorem symmetry_eq_id : forall m:nat, forall X:NoDupList, 
     support_equivalence 
-    (symmetry_big m X 0 EmptyNDL)
+      (@symmetry_big m X 0 EmptyNDL _)
       (bigraph_id m X). 
     Proof.
       intros m X.
       apply (
         SupEq _ _ _ _ _ _ _ _  
-        (symmetry_big m X 0 EmptyNDL)
+          (@symmetry_big m X 0 EmptyNDL _)
           (bigraph_id m X)
           (addn0 m) (*s*)
           (fun (name : infT) => right_empty X name) (*i*)
@@ -108,21 +108,20 @@ Definition commute_plus_MyEqNat : forall m n,
     MyEqNat (m + n) (n + m).
     Proof. intros. apply addnC. Qed.
 
-Theorem id_eq_compo_symmetries : forall m n:nat, forall X Y:NoDupList, 
+  Theorem id_eq_compo_symmetries (m n:nat) (X Y:NoDupList) {dis:X#Y}:
     support_equivalence 
       (bigraph_composition 
         (p:=permutation_union_commutePN X Y) 
         (eqsr := commute_plus_MyEqNat m n)
-      (symmetry_big m X n Y) 
-      (symmetry_big n Y m X))
+        (@symmetry_big m X n Y _) 
+        (@symmetry_big n Y m X (disjoint_commutes dis)))
       (bigraph_id (m + n) (X ∪ Y)). 
     Proof.
-    intros m n X Y.
       eapply (
         SupEq (n + m) (m + n) (m + n) (m + n) (Y ∪ X) (X ∪ Y) (X ∪ Y) (X ∪ Y)  
           (bigraph_composition (p:=permutation_union_commutePN X Y) (eqsr := commute_plus_MyEqNat m n)
-          (symmetry_big m X n Y) 
-          (symmetry_big n Y m X))
+            (@symmetry_big m X n Y _) 
+            (@symmetry_big n Y m X _))
           (bigraph_id (m + n) (X ∪ Y))
           (addnC n m) (*s*)
           (permutation_union_commute Y X) (*i*)
@@ -130,9 +129,7 @@ Theorem id_eq_compo_symmetries : forall m n:nat, forall X Y:NoDupList,
           (permutation_id (X ∪ Y)) (*o*)
           bij_void_sum_neutral (*n*)
           bij_void_sum_neutral (*e*)
-        (fun n' => match n' with 
-        | inl v => bij_rew ((@of_void _) v)
-        | inr v => bij_rew ((@of_void _) v) end )
+          (fun n' => bij_rew (arity_join_left_neutral _ n'))
         ). 
       + apply functional_extensionality.
         intros [].
@@ -173,24 +170,20 @@ Section S3.
   Theorem arity_join_commutes {n1 n2} {c1 c2} :
     forall n : void + (n1 + n2),
     Arity (join (of_void Kappa) (join c1 c2) n) =
-  Arity (join (join c2 c1) (of_void Kappa)
-    match n with
-    | inl v => match v return (n2 + n1 + void) with end
-    | inr (inl a) => inl (inr a)
-    | inr (inr b) => inl (inl b)
-    end).
+    Arity (join (join c2 c1) (of_void Kappa)(bij_void_A_B n)).
     Proof. 
       intros [[]|[nf|ng]];
       reflexivity.
     Qed.
 
 
-Theorem symmetry_commutes_with_tp {si0 ri1 sj0 rj1:nat} {ii0 oi1 ij0 oj1:NoDupList}
+  Theorem symmetry_commutes_with_tp 
+    {si0 ri1 sj0 rj1:nat} {ii0 oi1 ij0 oj1:NoDupList}
     {disi: ii0#ij0} {diso: oi1#oj1}: 
     forall f:bigraph si0 ii0 ri1 oi1, 
     forall g:bigraph sj0 ij0 rj1 oj1,
     support_equivalence 
-    ((symmetry_big ri1 oi1 rj1 oj1) 
+      ((@symmetry_big ri1 oi1 rj1 oj1 _) 
         <<o>> (f ⊗ g))
       (bigraph_composition 
         (p:=permutation_union_commutePN ij0 ii0) (eqsr := commute_plus_MyEqNat sj0 si0)
@@ -198,13 +191,13 @@ Theorem symmetry_commutes_with_tp {si0 ri1 sj0 rj1:nat} {ii0 oi1 ij0 oj1:NoDupLi
           (dis_i := disjoint_commutes disi)
           (dis_o := disjoint_commutes diso) 
           g f)
-      (symmetry_big si0 ii0 sj0 ij0)).
+        (@symmetry_big si0 ii0 sj0 ij0 _)).
     Proof.
       intros.
       apply (
         SupEq _ _ _ _ _ _ _ _
           (bigraph_composition 
-          (symmetry_big ri1 oi1 rj1 oj1) 
+            (@symmetry_big ri1 oi1 rj1 oj1 _) 
             (f ⊗ g))
           (bigraph_composition 
             (p:=permutation_union_commutePN ij0 ii0) 
@@ -213,7 +206,7 @@ Theorem symmetry_commutes_with_tp {si0 ri1 sj0 rj1:nat} {ii0 oi1 ij0 oj1:NoDupLi
               (dis_i := disjoint_commutes disi)
               (dis_o := disjoint_commutes diso) 
               g f)
-          (symmetry_big si0 ii0 sj0 ij0))
+            (@symmetry_big si0 ii0 sj0 ij0 _))
           (erefl) (*s*)
           (permutation_id (ii0 ∪ ij0)) (*i*)
           (addnC ri1 rj1) (*r*)
@@ -279,14 +272,14 @@ Theorem symmetry_commutes_with_tp {si0 ri1 sj0 rj1:nat} {ii0 oi1 ij0 oj1:NoDupLi
           destruct get_link as [|[o' Ho']]; try reflexivity;
           f_equal; apply subset_eq_compat; reflexivity.
         - destruct (in_dec EqDecN i' ii0); destruct (in_dec EqDecN i' ij0).
-        * exfalso. destruct disi as [disi]. apply (disi i' i0 i1).
+          * exfalso. apply (disi i' i0 i1).
           * destruct (in_dec EqDecN i' ii0).
-          ** rewrite <- (innername_proof_irrelevant f i1). 
+            ** rewrite (innername_proof_irrelevant f _ i0). 
             destruct get_link as [|[o' Ho']]; try reflexivity. 
             *** f_equal. apply subset_eq_compat. reflexivity.
             ** contradiction.
           * destruct (in_dec EqDecN i' ij0).
-          ** rewrite <- (innername_proof_irrelevant g i1). 
+            ** rewrite (innername_proof_irrelevant g _ i0). 
             destruct get_link as [|[o' Ho']]; try reflexivity. 
             *** f_equal. apply subset_eq_compat. reflexivity.
             ** contradiction.
@@ -295,90 +288,89 @@ Theorem symmetry_commutes_with_tp {si0 ri1 sj0 rj1:nat} {ii0 oi1 ij0 oj1:NoDupLi
 End S3.
 
 Section S4.
-Lemma MyPN {mI mJ mK:nat} {XI XJ XK:NoDupList}
-  {disIJ : XI # XJ} {disKJ : XK # XJ} {disIK : XI # XK}:
-  permutation 
-    (XI ∪ XK ∪ XJ)
-    (XI ∪ (XJ ∪ XK)).
+
+Theorem commute_in_sum : forall mI mJ mK, mI + mJ + mK = mI + mK + mJ.
+  Proof. intros. rewrite addnCAC. rewrite addnC. apply addnA. Qed.
+Theorem commute_in_union : forall XI XJ XK, 
+  permutation (XI ∪ XJ ∪ XK) (XI ∪ XK ∪ XJ).
   Proof. 
-    simpl.
     intros; split; intros; apply in_app_iff in H; destruct H.
     - apply in_app_iff in H; destruct H.
     apply in_app_iff; auto.
     apply in_app_iff; auto.
-    right.
     apply in_app_iff; auto.
-    - apply in_app_iff; auto.
-    right.
+    left.
+    apply in_app_iff; auto.
     apply in_app_iff; auto.
     - apply in_app_iff; auto.
     left.
     apply in_app_iff; auto.
-    -  apply in_app_iff in H; destruct H;
+    - apply in_app_iff in H; destruct H.
+    apply in_app_iff; auto.
+    left.
+    apply in_app_iff; auto.
     apply in_app_iff; auto.
+    - apply in_app_iff; auto. 
     left.
     apply in_app_iff; auto.
   Qed.
 
-(* #[export] Instance permutation_s4 {mI mJ mK:nat} {XI XJ XK:NoDupList}
-  {disIJ : XI # XJ} {disKJ : XK # XJ} {disIK : XI # XK} :
-  PermutationinfTs
+(* Lemma MyPN' {mI mJ mK:nat} {XI XJ XK:NoDupList}
+  {disIJ : XI # XJ} {disJK : XJ # XK} {disIK : XI # XK}:
+  permutation 
     (XI ∪ XK ∪ XJ)
     (XI ∪ (XJ ∪ XK)).
   Proof.
-  constructor. 
-  apply (@MyPN mI mJ mK XI XJ XK disIJ _ _).
-  Qed.   *)
-
-Definition myEqNatproof {mI mJ mK:nat} : MyEqNat 
-  (mI + mK + mJ) (mI + (mJ + mK)).
-  Proof. auto. symmetry. rewrite addnC. rewrite addnCAC. reflexivity. Qed.
-
-Theorem commute_in_sum : forall mI mJ mK, mI + mJ + mK = mI + mK + mJ.
-  Proof. intros. rewrite addnCAC. rewrite addnC. apply addnA. Qed.
-Theorem commute_in_union : forall XI XJ XK, 
-  permutation (XI ∪ XJ ∪ XK) (XI ∪ XK ∪ XJ).
-  Proof. 
+    simpl.
     intros; split; intros; apply in_app_iff in H; destruct H.
     - apply in_app_iff in H; destruct H.
     apply in_app_iff; auto.
     apply in_app_iff; auto.
-    apply in_app_iff; auto.
-    left.
-    apply in_app_iff; auto.
+    right.
     apply in_app_iff; auto.
     - apply in_app_iff; auto.
-    left.
-    apply in_app_iff; auto.
-    - apply in_app_iff in H; destruct H.
+    right.
     apply in_app_iff; auto.
+    - apply in_app_iff; auto.
     left.
     apply in_app_iff; auto.
+    -  apply in_app_iff in H; destruct H;
     apply in_app_iff; auto.
-    - apply in_app_iff; auto. 
     left.
     apply in_app_iff; auto.
   Qed.
 
+Theorem symmetry_commutes_with_tp_s4 {mI mJ mK:nat} {XI XJ XK:NoDupList}
+  {disIJ : XI # XJ} {disJK : XJ # XK} {disIK : XI # XK}:
+  support_equivalence 
+    (@symmetry_big (mI+mJ) (XI ∪ XJ) mK XK _)
+    (bigraph_composition 
+      (p := P_NP ((MyPN' (mI:=mI) (mJ:=mJ) (mK:=mK)))) 
+      (eqsr:= myEqNatproof)
+      (bigraph_tensor_product 
+        (dis_i := disj_app_left disIJ (disjoint_commutes disJK))
+        (dis_o := disj_app_left disIJ (disjoint_commutes disJK))
+        (@symmetry_big mI XI mK XK _) 
+        (bigraph_id mJ XJ))
+      ((bigraph_id mI XI) ⊗ (@symmetry_big mJ XJ mK XK _))). *)
   
+(* Set Typeclasses Debug. *)
 Theorem symmetry_commutes_with_tp_s4 {mI mJ mK:nat} {XI XJ XK:NoDupList}
   {disIJ : XI # XJ} {disKJ : XK # XJ} {disIK : XI # XK}:
   support_equivalence
-    (symmetry_big (mI+mJ) (XI ∪ XJ) mK XK)
+    (@symmetry_big (mI+mJ) (XI ∪ XJ) mK XK (disj_app_left _ (disj_commute disKJ) ))
     (bigraph_composition
-      (p := P_NP ((MyPN (mI:=mI) (mJ:=mJ) (mK:=mK)))) 
+      (p:= permutation_s4)
       (eqsr:=myEqNatproof)
-      ((symmetry_big mI XI mK XK) ⊗ (bigraph_id mJ XJ))
-      ((bigraph_id mI XI) ⊗ (symmetry_big mJ XJ mK XK))).
+      ((@symmetry_big mI XI mK XK _) ⊗ (bigraph_id mJ XJ)) 
+      ((bigraph_id mI XI) ⊗ (@symmetry_big mJ XJ mK XK (disj_commute disKJ)))).
   Proof.
   apply (
     SupEq _ _ _ _ _ _ _ _
-      (symmetry_big (mI+mJ) (XI ∪ XJ) mK XK)
+      (@symmetry_big (mI+mJ) (XI ∪ XJ) mK XK _)
       (bigraph_composition 
-      (p := P_NP (_)) 
-      (eqsr:= myEqNatproof)
-        ((symmetry_big mI XI mK XK) ⊗ (bigraph_id mJ XJ))
-        ((bigraph_id mI XI) ⊗ (symmetry_big mJ XJ mK XK)))
+        ((@symmetry_big mI XI mK XK _) ⊗ (bigraph_id mJ XJ))
+        ((bigraph_id mI XI) ⊗ (@symmetry_big mJ XJ mK XK _)))
       (esym (addnA mI mJ mK)) (*s*)
       unionA (*i*)
       (commute_in_sum mI mJ mK) (*r*)
@@ -478,16 +470,16 @@ Theorem symmetry_commutes_with_tp_s4 {mI mJ mK:nat} {XI XJ XK:NoDupList}
 End S4.
 
 Section SymmetryAxiom.
-Lemma symmetry_axiom : forall m n X Y, 
+Lemma symmetry_axiom {m n X Y} {dis:X#Y}: 
   support_equivalence 
-    (symmetry_big m EmptyNDL n EmptyNDL ⊗ bigraph_id 0 (X ∪ Y))
-    (symmetry_big m X n Y) .
+    (@symmetry_big m EmptyNDL n EmptyNDL _ ⊗ bigraph_id 0 (X ∪ Y))
+    (@symmetry_big m X n Y _) .
   Proof.
   intros. 
   apply (
     SupEq _ _ _ _ _ _ _ _
-      (symmetry_big m EmptyNDL n EmptyNDL ⊗ bigraph_id 0 (X ∪ Y))
-      (symmetry_big m X n Y)
+      (@symmetry_big m EmptyNDL n EmptyNDL _ ⊗ bigraph_id 0 (X ∪ Y))
+      (@symmetry_big m X n Y _)
       ((addn0 (m+n))) (*s*)
       (permutation_id _) (*i*)
       ((addn0 (m+n))) (*r*)

src/TensorProduct.v

@@ -29,13 +29,13 @@ Module c := CompositionBigraphs s n.
 Import c leb eb b b.n b.s n s. 
 
 
+
 Set Typeclasses Unique Instances.
 Set Typeclasses Iterative Deepening.
 
 
 Definition FiniteParent_tensorproduct
   {s1 r1 s2 r2 : nat} {i1 o1 i2 o2 : NoDupList}
-  {dis_i : i1 # i2} {dis_o : o1 # o2}
   {b1 : bigraph s1 i1 r1 o1} {b2 : bigraph s2 i2 r2 o2} : 
   FiniteParent 
     (((bij_id <+> bij_ord_sum) <o> 
@@ -115,7 +115,7 @@ Theorem bigraph_tp_left_neutral : forall {s i r o} (b : bigraph s i r o),
       * destruct s0. f_equal. apply subset_eq_compat. reflexivity. 
   Qed.
 
-  (*TODO REDO THIS PROOF*)
+
 Theorem bigraph_tp_right_neutral : forall {s i r o} (b : bigraph s i r o), 
   support_equivalence (b ⊗ ∅) b.
   Proof.
@@ -158,21 +158,6 @@ End M2.
 
 (** Section on associativity of tensor product*)
 Section M1.
-Lemma arity_tp_assoc : 
-  forall {s1 i1 r1 o1 s2 i2 r2 o2 s3 i3 r3 o3} 
-  {dis_i12 : i1 # i2} {dis_i23 : i2 # i3} {dis_i13 : i1 # i3}
-  {dis_o12 : o1 # o2} {dis_o23 : o2 # o3} {dis_o13 : o1 # o3}
-  (b1 : bigraph s1 i1 r1 o1) (b2 : bigraph s2 i2 r2 o2) (b3 : bigraph s3 i3 r3 o3) n12_3,
-  Arity (get_control (bg:=(b1 ⊗ b2) ⊗ b3) n12_3) 
-  = 
-  Arity (get_control (bg:=b1 ⊗ (b2 ⊗ b3)) (bij_sum_assoc n12_3)).
-  Proof.
-  intros until n12_3.
-  destruct n12_3 as [[n1 | n2] | n3].
-  + reflexivity.
-  + reflexivity.
-  + reflexivity.
-  Qed.
 
 
 Theorem bigraph_tp_assoc : 
@@ -279,62 +264,6 @@ End M1.
 
 
 (** Congruence of TP*)
-Definition arity_tp_congruence_forward 
-  {s1 i1 r1 o1 s2 i2 r2 o2 s3 i3 r3 o3 s4 i4 r4 o4} 
-  {dis_i13 : i1 # i3} {dis_o13 : o1 # o3}
-  {dis_i24 : i2 # i4} {dis_o24 : o2 # o4}
-  (b1 : bigraph s1 i1 r1 o1) (b2 : bigraph s2 i2 r2 o2) (b3 : bigraph s3 i3 r3 o3) (b4 : bigraph s4 i4 r4 o4)
-  (bij_n12 : bijection ((get_node b1)) ((get_node b2))) (bij_n34 : bijection ((get_node b3)) ((get_node b4)))
-  (bij_p12 : forall (n1 : (get_node b1)), bijection ('I_(Arity (get_control (bg:= b1) n1))) ('I_(Arity (get_control (bg:= b2) (bij_n12 n1)))))
-  (bij_p34 : forall (n3 : (get_node b3)), bijection ('I_(Arity (get_control (bg:=b3) n3))) ('I_(Arity (get_control (bg:=b4) (bij_n34 n3)))))
-  (n13 : (get_node (b1 ⊗ b3))) :
-  ('I_(Arity (get_control (bg:=b1 ⊗ b3) n13))) -> ('I_(Arity (get_control (bg:=b2 ⊗ b4) ((bij_n12 <+> bij_n34) n13)))).
-  Proof.
-  destruct n13 as [n1 | n3].
-  + exact (bij_p12 n1).
-  + exact (bij_p34 n3).
-  Defined.
-
-Definition arity_tp_congruence_backward 
-  {s1 i1 r1 o1 s2 i2 r2 o2 s3 i3 r3 o3 s4 i4 r4 o4} 
-  {dis_i13 : i1 # i3} {dis_o13 : o1 # o3}
-  {dis_i24 : i2 # i4} {dis_o24 : o2 # o4}
-  (b1 : bigraph s1 i1 r1 o1) (b2 : bigraph s2 i2 r2 o2) (b3 : bigraph s3 i3 r3 o3) (b4 : bigraph s4 i4 r4 o4)
-  (bij_n12 : bijection ((get_node b1)) ((get_node b2))) (bij_n34 : bijection ((get_node b3)) ((get_node b4)))
-  (bij_p12 : forall (n1 : (get_node b1)), bijection ('I_(Arity (get_control (bg:= b1) n1))) ('I_(Arity (get_control (bg:= b2) (bij_n12 n1)))))
-  (bij_p34 : forall (n3 : (get_node b3)), bijection ('I_(Arity (get_control (bg:=b3) n3))) ('I_(Arity (get_control (bg:=b4) (bij_n34 n3)))))
-  (n13 : (get_node (b1 ⊗ b3))) :
-  ('I_(Arity (get_control (bg:=b2 ⊗ b4) ((bij_n12 <+> bij_n34) n13)))) -> ('I_(Arity (get_control (bg:=b1 ⊗ b3) n13))).
-  Proof.
-  destruct n13 as [n1 | n3].
-  + exact (backward (bij_p12 n1)).
-  + exact (backward (bij_p34 n3)).
-  Defined.
-
-Lemma arity_tp_congruence : 
-  forall {s1 i1 r1 o1 s2 i2 r2 o2 s3 i3 r3 o3 s4 i4 r4 o4} 
-  {dis_i13 : i1 # i3} {dis_o13 : o1 # o3}
-  {dis_i24 : i2 # i4} {dis_o24 : o2 # o4}
-  (b1 : bigraph s1 i1 r1 o1) (b2 : bigraph s2 i2 r2 o2) (b3 : bigraph s3 i3 r3 o3) (b4 : bigraph s4 i4 r4 o4)
-  (bij_n12 : bijection ((get_node b1)) ((get_node b2))) (bij_n34 : bijection ((get_node b3)) ((get_node b4)))
-  (bij_p12 : forall (n1 : (get_node b1)), bijection ('I_(Arity (get_control (bg:= b1) n1))) ('I_(Arity (get_control (bg:= b2) (bij_n12 n1)))))
-  (bij_p34 : forall (n3 : (get_node b3)), bijection ('I_(Arity (get_control (bg:=b3) n3))) ('I_(Arity (get_control (bg:=b4) (bij_n34 n3)))))
-  (n13 : (get_node (b1 ⊗ b3))),
-  bijection ('I_(Arity (get_control (bg:=b1 ⊗ b3) n13))) ('I_(Arity (get_control (bg:=b2 ⊗ b4) ((bij_n12 <+> bij_n34) n13)))).
-  Proof.
-  intros until n13.
-  apply (mkBijection _ _ (arity_tp_congruence_forward b1 b2 b3 b4 bij_n12 bij_n34 bij_p12 bij_p34 n13) (arity_tp_congruence_backward b1 b2 b3 b4 bij_n12 bij_n34 bij_p12 bij_p34 n13)).
-  + destruct n13 as [n1 | n3]; simpl.
-    - rewrite <- (fob_id _ _ (bij_p12 n1)).
-      reflexivity.
-    - rewrite <- (fob_id _ _ (bij_p34 n3)).
-      reflexivity.
-  + destruct n13 as [n1 | n3]; simpl.
-    - rewrite <- (bof_id _ _ (bij_p12 n1)).
-      reflexivity.
-    - rewrite <- (bof_id _ _ (bij_p34 n3)).
-      reflexivity.
-  Defined.
 
 Theorem congruence_imp_dis_i : 
   forall {s1 i1 r1 o1 s2 i2 r2 o2 s3 i3 r3 o3 s4 i4 r4 o4} 
@@ -406,7 +335,7 @@ Theorem bigraph_tp_congruence :
     (union_cong bij_o12 bij_o34)
     (bij_n12 <+> bij_n34)
     (bij_e12 <+> bij_e34)
-    (arity_tp_congruence b1 b2 b3 b4 bij_n12 bij_n34 bij_p12 bij_p34) 
+    (fun n => bij_congruence bij_n12 bij_n34 bij_p12 bij_p34 n) 
     ).
   + apply functional_extensionality.
     destruct x as [n2' | n4']; simpl.
@@ -560,54 +489,34 @@ Theorem bigraph_comp_tp_dist : forall {s1 i1 r1 o1 s2 i2 r3 r4 r2 o2 s3 i3 o3 s4
         destruct get_link; try reflexivity.
         **** apply f_equal. destruct s0. apply subset_eq_compat. reflexivity.
     - destruct (in_dec EqDecN i' i3).
-      * destruct get_link; try reflexivity.
-      destruct s0 as [n npf]. 
-      destruct (in_dec EqDecN n i1).
+      * destruct get_link as [|[o' Ho']]; try reflexivity.
+      destruct (in_dec EqDecN o' i1).
       *** symmetry.
       rewrite <- (innername_proof_irrelevant b1 i6).
-      destruct get_link; try reflexivity.
-      apply f_equal. destruct s0. apply subset_eq_compat. reflexivity.
-      *** exfalso. apply n0.
+      destruct get_link as [|[o'' Ho'']]; try reflexivity.
+      apply f_equal. apply subset_eq_compat. reflexivity.
+      *** exfalso. apply n.
       destruct p13 as [p13].
       destruct p24 as [p24].
-      unfold permutation in p13. destruct (p13 n). apply H0. apply npf.
-      * unfold permutation_distributive, permut_list_forward.
-      set (Hn := 
-        match
-          in_app_or_m_nod_dup i3 i4 i'
-            (match
-              i3 as n0 return ((In i' n0 -> ~ In i' i4) -> In i' (app_merge n0 i4) -> ~ In i' n0 -> NoDup n0)
-            with
-            | {| ndlist := ndlist0; nd := nd0 |} =>
-                fun (_ : In i' ndlist0 -> ~ In i' i4) (_ : In i' (app_merge ndlist0 i4)) (_ : ~ In i' ndlist0) =>
-                nd0
-            end (dis_i34 i') i0 n)
-            (match i4 as n0 return ((In i' i3 -> ~ In i' n0) -> In i' (app_merge i3 n0) -> NoDup n0) with
-            | {| ndlist := ndlist0; nd := nd0 |} =>
-                fun (_ : In i' i3 -> ~ In i' ndlist0) (_ : In i' (app_merge i3 ndlist0)) => nd0
-            end (dis_i34 i') i0) i0
-        with
-        | inl i1 => False_ind (In i' i4) (n i1)
-        | inr i1 => i1
-        end).
-      rewrite <- (innername_proof_irrelevant b4 Hn).
-      destruct get_link; try reflexivity; clear Hn. 
-      destruct s0 as [n' npf']. 
-      destruct (in_dec EqDecN n' i1).
-      *** exfalso. set (dis_i12' := dis_i12). unfold Disjoint in dis_i12'. specialize (dis_i12' n'). apply dis_i12'; try assumption.
+      unfold permutation in p13. destruct (p13 o'). apply H0. apply Ho'.
+      * rewrite <- (innername_proof_irrelevant b4 (not_in_first_imp_in_second i3 i4 i' i0 n)).
+      destruct get_link as[|[o' Ho']]; try reflexivity. 
+      destruct (in_dec EqDecN o' i1).
+      *** exfalso. set (dis_i12' := dis_i12). unfold Disjoint in dis_i12'. specialize (dis_i12' o'). apply dis_i12'; try assumption.
       destruct p24 as [p24].
-      unfold permutation in p24. destruct (p24 n'). apply H0; assumption.
+      unfold permutation in p24. destruct (p24 o'). apply H0; assumption.
       *** rewrite <- (innername_proof_irrelevant b2
           (proj1 (@bij_subset_lemma _ _
           (fun infT0 => In infT0 (ndlist i2))
           (fun outer => In outer (ndlist o4)) 
-          bij_id (PN_P p24) n') npf')).
+          bij_id (PN_P p24) o') Ho')).
       destruct get_link; try reflexivity.
       apply f_equal. destruct s0. apply subset_eq_compat. reflexivity.
   Qed.
 End M3.
 
 (** Small lemma about the merge bigraph*)
+(*TODO si j'en parle*)
 Theorem merge_well_defined : forall n, 
   support_equivalence
     (@merge (n+1))