bunfold tact

src/Composition.v

@@ -76,6 +76,14 @@ Lemma arity_comp_left_neutral : forall {s i r o}
   Qed.
 
 
+Ltac bigraph_unfold := 
+  unfold funcomp, parallel, sequence, rearrange, extract1, bij_rew_forward, sum_shuffle, bij_join_port_backward, bij_dep_sum_1_forward, bij_dep_sum_2_forward,eq_rect_r, bij_subset_forward, permut_list_forward, bij_rew, bijection_inv.
+
+
+Tactic Notation "bunfold" := bigraph_unfold.
+
+
+
 Theorem bigraph_comp_left_neutral : forall {s i r o} 
   (b : bigraph s i r o), 
   support_equivalence (bigraph_id r o <<o>> b) b.
@@ -96,40 +104,20 @@ Theorem bigraph_comp_left_neutral : forall {s i r o}
     intro x.
     reflexivity. 
   + apply functional_extensionality.
-    destruct x as [n1 | s1]; rewrite bij_rew_id; rewrite bij_rew_id;simpl.
-    - unfold funcomp, parallel, sequence,rearrange,extract1,bij_rew_forward. 
-      destruct get_parent; try reflexivity. 
-      rewrite <- eq_rect_eq. reflexivity.
-    - unfold funcomp, parallel. Check eq_rect_eq.
-      simpl. 
-      unfold rearrange. simpl. 
-      destruct get_parent; try reflexivity.
-      f_equal. unfold bij_rew_forward. 
-      rewrite <- eq_rect_eq. reflexivity.
+    destruct x as [n1 | s1]; rewrite bij_rew_id; rewrite bij_rew_id;simpl;
+      bunfold;
+      destruct get_parent; try reflexivity; 
+      rewrite <- eq_rect_eq; reflexivity.
   + apply functional_extensionality.
     destruct x as [(v1, (k1, Hvk1)) | [name]]; simpl.
-    - unfold parallel, sum_shuffle, choice, funcomp.
-      simpl.
-      unfold bij_join_port_backward, bij_dep_sum_2_forward, bijection_inv, bij_dep_sum_1_forward.
-      simpl.
-      unfold bij_rew_forward, eq_rect_r, funcomp.
-      simpl.
-      unfold rearrange,  extract1, bij_subset_forward.
-      simpl.
-    (*
-        erewrite eq_rect_pi.
-        erewrite (eq_rect_pi (x := v1)).
-    *)
+    - bunfold. simpl.
+      bunfold.
       rewrite <- eq_rect_eq.
       rewrite <- eq_rect_eq.
       destruct get_link; try reflexivity.
       * apply f_equal. destruct s0. apply subset_eq_compat. reflexivity.
     
-    - unfold funcomp.
-      simpl. 
-      unfold bij_list_forward, bij_list_backward', bij_subset_forward, bij_subset_backward, parallel, sum_shuffle, choice, funcomp. 
-      simpl.
-      unfold rearrange. simpl.
+    - bunfold. simpl.
       rewrite <- (innername_proof_irrelevant b i0).
       destruct get_link; try reflexivity.
       * apply f_equal. destruct s0. apply subset_eq_compat. reflexivity.
@@ -428,7 +416,7 @@ Theorem bigraph_comp_congruence : forall
       * unfold bij_rew_forward. 
       erewrite eq_rect_compose.
       erewrite eq_rect_compose.
-      instantiate (1 := Logic.eq_sym eqxy). 
+      instantiate (1 := (Logic.eq_sym eqs1r3)). 
       destruct get_parent; try reflexivity.
     - rewrite <- big_parent_eq34.
       rewrite <- big_parent_eq12.

src/LeanSupportEquivalence.v

@@ -22,7 +22,6 @@ From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
 From mathcomp Require Import path div.
 
-
 Import ListNotations.
 
 (** This module implements lean-support equivalence between two bigraphs