tp cong simpl

src/AbstractBigraphs.v

@@ -229,7 +229,7 @@ Search (_ -> Prop).
 Check pred. *)
 
 Definition pred' T := T -> bool.
-Check pred'. 
+(* Check pred'.  *)
 Definition permutationbig (n : nat) : bigraph n EmptyNDL n EmptyNDL. 
   Proof. 
   apply (@Big n EmptyNDL n EmptyNDL

src/Bijections.v

@@ -752,7 +752,6 @@ Theorem bij_inv_comp : forall {A B C} (bij_AB : bijection A B) (bij_BC : bijecti
   Qed.
 End BijCompose.
 
-Locate parallel.
 Definition bij_sum_compose : forall {A B C D : Type}, bijection A B -> bijection C D -> bijection (A+C) (B+D).
   Proof.
     intros A B C D bij_AB bij_CD.

src/Composition.v

@@ -199,6 +199,16 @@ Lemma arity_comp_assoc :
   destruct n12_3 as [[n1 | n2] | n3]; reflexivity.
   Qed.
 
+Lemma arity_join_assoc {n1 n2 n3} {c1 c2 c3}:
+  forall n12_3:n1 + n2 + n3, 
+  Arity ((join (join c1 c2) c3) n12_3) = 
+  Arity ((join c1 (join c2 c3)) (bij_sum_assoc n12_3)).
+  Proof. (*s1=r2*) (*s2 = r3*)
+  intros until n12_3. 
+  destruct n12_3 as [[n_1 | n_2] | n_3]; reflexivity.
+  Qed.
+
+
 Theorem bigraph_comp_assoc : forall {s1 i1 r1 o1 s2 r2 r3 i2 o2 s3 i3 o3} 
   { pi1 : PermutationinfTs (ndlist i1) (ndlist o2)}
   { pi2 : PermutationinfTs (ndlist i2) (ndlist o3)}
@@ -218,7 +228,7 @@ Theorem bigraph_comp_assoc : forall {s1 i1 r1 o1 s2 r2 r3 i2 o2 s3 i3 o3}
     (permutation_id o1)
     bij_sum_assoc
     bij_sum_assoc
-    (fun n12_3 => bij_rew  (arity_comp_assoc b1 b2 b3 n12_3))
+    (fun n12_3 => bij_rew  (arity_join_assoc n12_3))
   ). 
   + apply functional_extensionality.
     destruct x as [n1 | [n2 | n3]]; reflexivity.

src/ListSpec.v

@@ -15,14 +15,12 @@ Fixpoint onto {T : Type} (l : list T) : list { e : T | In e l } :=
   | h :: t => (exist _ h (in_eq h t)) :: (map (cons_type h t) (onto t))
   end. 
   
-Check in_eq. Check in_cons.
 (* Search (list ?T -> list (sig  _)). *)
 Lemma onto_nil {T : Type} : @onto T nil = nil. Proof. reflexivity. Qed.
 
 Lemma onto_cons {T : Type} (e : T) (l : list T) :
   onto (e :: l) = exist _ e (in_eq e l) :: map (cons_type _ _) (onto l).
 Proof. reflexivity. Qed.
-Print onto_cons.
 
 Lemma onto_correct {T : Type} (l : list T) (e : { x : T | In x l}) : In e (onto l).
 Proof.

src/Names.v

@@ -59,7 +59,7 @@ Axiom constructive_definite_description :
     (exists x, P x) -> { x : A | P x }.
 
 (* Set Printing All.  *)
-Print constructive_definite_description.
+(* Print constructive_definite_description. *)
 
 Definition freshinfT' : list infT -> infT.
  intros.
@@ -357,7 +357,7 @@ Theorem in_app_merge_trans {l1 l2 l3 : list infT} : forall a,
       + apply in_right_list. assumption.
   Defined.
 
-Theorem in_app_merge_transi {l1 l2 l3 : list infT} : forall a,
+Theorem unionA {l1 l2 l3 : list infT} : forall a,
   In a (app_merge (app_merge l1 l2) l3) <-> In a (app_merge l1 (app_merge l2 l3)).
   Proof.
       intros. split.
@@ -371,6 +371,7 @@ Theorem in_app_merge_transi {l1 l2 l3 : list infT} : forall a,
       + apply in_right_list. apply in_right_list. assumption.
       - apply in_app_merge_trans.
   Defined.
+  (*TODO: do I need to define or Qed enough?*)
 
 Definition reflinfTs {r} : forall infT : infT,
   In infT r <-> In infT r.
@@ -693,16 +694,16 @@ Definition tr_permutation {i1 i2 i3} :
     ++ apply in_right_list. assumption.
   Defined.
 
-Lemma app_merge_cong {i1 i2 i3 i4}:  
+Lemma union_cong {i1 i2 i3 i4}:  
   permutation i1 i2 -> permutation i3 i4 -> 
   permutation (app_merge i1 i3) (app_merge i2 i4).
   Proof.
   intros H12 H34.
   split; intros H.
-  - apply in_app_iff in H. destruct H.
+  - apply in_app_or_m in H. destruct H.
   + apply H12 in H. apply in_left_list. apply H.
   + apply H34 in H. apply in_right_list. apply H.
-  - apply in_app_iff in H. destruct H.
+  - apply in_app_or_m in H. destruct H.
   + apply H12 in H. apply in_left_list. apply H.
   + apply H34 in H. apply in_right_list. apply H.
   Qed.

src/ParallelProduct.v

@@ -619,9 +619,9 @@ Theorem bigraph_pp_congruence : forall {s1 i1 r1 o1 s2 i2 r2 o2 s3 i3 r3 o3 s4 i
   destruct Heqb3b4 as (bij_s34, bij_i34, bij_r34, bij_o34, bij_n34, bij_e34, bij_p34, big_control_eq34, big_parent_eq34, big_link_eq34).
   apply (SupEq _ _ _ _ _ _ _ _ (b1 || b3) (b2 || b4)
     (f_equal2_plus _ _ _ _ bij_s12 bij_s34)
-    (app_merge_cong bij_i12 bij_i34)
+    (union_cong bij_i12 bij_i34)
     (f_equal2_plus _ _ _ _ bij_r12 bij_r34)
-    (app_merge_cong bij_o12 bij_o34)
+    (union_cong bij_o12 bij_o34)
     (bij_n12 <+> bij_n34)
     (bij_e12 <+> bij_e34)
     (arity_pp_congruence b1 b2 b3 b4 bij_n12 bij_n34 bij_p12 bij_p34) 
@@ -730,7 +730,7 @@ Theorem bigraph_pp_congruence : forall {s1 i1 r1 o1 s2 i2 r2 o2 s3 i3 r3 o3 s4 i
         (@bij_subset_lemma (Equality.sort infT) (Equality.sort infT)
         (fun infT0 : Equality.sort infT => In infT0 (app_merge (ndlist i1) (ndlist i3)))
         (fun inner : Equality.sort infT => In inner (app_merge (ndlist i2) (ndlist i4)))
-        bij_id (app_merge_cong bij_i12 bij_i34)  i24) i0) n)).
+        bij_id (union_cong bij_i12 bij_i34)  i24) i0) n)).
       rewrite <- (innername_proof_irrelevant b1 Hi24).
       symmetry.
       rewrite <- (innername_proof_irrelevant b1 Hi24).

src/Sorting.v

@@ -543,8 +543,8 @@ Theorem join_meet_thm2 : forall y x : string, join_string x (meet_string x y) =
 
 
 (* Theorem meet_eq : forall x y : string, (x <= y)%O = (meet_string x y == x). *) 
-Check pred string.
-Print pred.
+(* Check pred string.
+Print pred. *)
 Definition subdef : pred string -> nat -> option string. Admitted. 
 
 Theorem string_has_choice : hasChoice.axioms_ string.