Skip to content
Snippets Groups Projects
Commit bd81b5b7 authored by MARCON Cecile's avatar MARCON Cecile
Browse files

refactored AGAIN se imp lse less than 100 lines now!

parent 8b60868d
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
src/LeanSupportEquivalence.v
+ 76
− 192
View file @ bd81b5b7
......@@ -549,208 +549,92 @@ Theorem support_equivalence_implies_lean_support_equivalence {s1 r1 s2 r2 : nat}
intros [bij_s bij_i bij_r bij_o bij_n bij_e bij_p control_eq parent_eq link_eq].
unfold lean_support_equivalence.
refine (
SupEq _ _ _ _ _ _ _ _ (lean b1) (lean b2)
SupEq _ _ _ _ _ _ _ _
(lean b1) (lean b2)
bij_s bij_i bij_r bij_o
bij_n
<{ bij_e | not_is_idle_eq b1 b2 bij_i bij_o bij_n bij_e bij_p link_eq }>
bij_p control_eq parent_eq _
).
clear control_eq parent_eq bij_s bij_r.
simpl.
unfold parallel.
apply functional_extensionality.
unfold funcomp;simpl. intros ipa.
unfold bij_subset_forward. simpl.
destruct ipa as [ia | pa].
- destruct ia as [ia Hia].
unfold parallel,funcomp,bij_subset_forward.
simpl.
intros ipa.
generalize (ex_intro
(fun ip' =>
get_link (bg:=b2) ip' =
get_link (bg:=b2)
(@inl _ (sigT (fun n => ordinal (Arity (get_control (bg:=b2) n))))
(exist (fun inner => In inner (ndlist i2)) ia Hia)))
(@inl _
(sigT (fun n => ordinal (Arity (get_control (bg:=b2) n))))
(exist (fun inner => In inner (ndlist i2)) ia Hia))
(erefl (get_link (bg:=b2) (@inl _
(sigT (fun n => ordinal (Arity (get_control (bg:=b2) n))))
(exist (fun inner => In inner (ndlist i2)) ia Hia))))).
intros.
destruct get_link eqn:L2.
+ generalize (ex_intro
(fun ip' =>
(get_link (bg:= b1) ip') =
(get_link (bg:= b1)
(@inl _
(@sigT (Finite.sort (get_node b1)) (fun n1 => ordinal (Arity (get_control (bg:=b1) n1))))
(exist (fun infT0 => In infT0 (ndlist i1)) ia
(@proj1 (forall _ : In ia (ndlist i2), In ia (ndlist i1))
(forall _ : In ia (ndlist i1), In ia (ndlist i2))
(@bij_subset_lemma _ _ _ _ bij_id bij_i ia) Hia)))))
(@inl _
(sigT (fun n1 => ordinal (Arity (get_control (bg:=b1) n1))))
(exist (fun infT0 => In infT0 (ndlist i1)) ia
(@proj1
(forall _ : In ia (ndlist i2), In ia (ndlist i1))
(forall _ : In ia (ndlist i1), In ia (ndlist i2))
(@bij_subset_lemma _ _ _ _ bij_id bij_i ia) Hia)))
(erefl
(get_link (bg:= b1)
(@inl _ (sigT (fun n1 => ordinal (Arity (get_control (bg:=b1) n1))))
(exist (fun infT0 => In infT0 (ndlist i1)) ia
(@proj1
(forall _ : In ia (ndlist i2), In ia (ndlist i1))
(forall _ : In ia (ndlist i1), In ia (ndlist i2))
(@bij_subset_lemma _ _ _ (fun inner => In inner (ndlist i2))
bij_id bij_i ia) Hia)))))).
(fun ip' => get_link (bg:=b2) ip' = get_link (bg:=b2) ipa) ipa (erefl (get_link (bg:=b2) ipa))).
intros.
destruct (get_link (bg:=b1)) eqn:L1.
* f_equal. destruct s3. destruct s0. apply subset_eq_compat.
simpl in L2.
simpl in L1.
rewrite <- link_eq in L2.
simpl in L2.
clear control_eq parent_eq e e0.
unfold parallel, bij_subset_forward, bij_subset_backward, bij_dep_sum_2_forward, bij_dep_sum_1_forward in L2.
simpl in L2.
unfold funcomp in L2.
rewrite L1 in L2.
inversion L2. reflexivity.
* rewrite <- link_eq in L2.
simpl in L2. exfalso.
clear control_eq parent_eq e e0.
unfold parallel, bij_subset_forward, bij_subset_backward, bij_dep_sum_2_forward, bij_dep_sum_1_forward in L2.
simpl in L2.
unfold funcomp in L2.
simpl in L2.
rewrite L1 in L2.
discriminate L2.
+ generalize (ex_intro
generalize (ex_intro
(fun ip' =>
get_link (bg:=b1) ip' =
get_link (bg:=b1)
(@inl _ (sigT (fun n1 => ordinal (Arity (get_control (bg:=b1) n1))))
(exist ((In (A:=infT))^~ i1) ia
(@proj1
(forall _ : In ia (ndlist i2), In ia (ndlist i1))
(forall _ : In ia (ndlist i1), In ia (ndlist i2))
(@bij_subset_lemma _ _ _ _ bij_id bij_i ia) Hia))))
(@inl _ (sigT (fun n1 => ordinal (Arity (get_control (bg:=b1) n1))))
(exist ((In (A:=infT))^~ i1) ia
match ipa return (sum
(sig (fun infT0 => In infT0 (ndlist i1)))
(sigT (fun n1 => ordinal (Arity (get_control (bg:=b1) n1))))) with
| inl a => @inl _ (sigT (fun n1 => ordinal (Arity (get_control (bg:=b1) n1))))
match a return (sig (fun infT0 => In infT0 (ndlist i1))) with
| exist a0 Pa => exist (fun infT0 => In infT0 (ndlist i1)) a0
(@proj1
(forall _ : In ia (ndlist i2), In ia (ndlist i1))
(forall _ : In ia (ndlist i1), In ia (ndlist i2))
(@bij_subset_lemma _ _ _ _ bij_id bij_i ia) Hia)))
(erefl
(get_link (bg:=b1)
(@inl _ (sigT (fun n1 => ordinal (Arity (get_control (bg:=b1) n1))))
(exist ((In (A:=infT))^~ i1) ia
(forall _ : In a0 (ndlist i2), In a0 (ndlist i1))
(forall _ : In a0 (ndlist i1), In a0 (ndlist i2))
(@bij_subset_lemma _ _
(fun infT0 => In infT0 (ndlist i1))
(fun inner => In inner (ndlist i2)) bij_id bij_i a0) Pa)
end
| inr c => @inr (sig (fun infT0 => In infT0 (ndlist i1))) _
(bij_dep_sum_2_forward
(fun a => bijection_inv (bij_p a))
(bij_dep_sum_1_forward (bijection_inv bij_n) c))
end)
match ipa return (sum (sig (fun infT0 => In infT0 (ndlist i1))) (sigT (fun n1 => ordinal (Arity (get_control (bg:=b1) n1))))) with
| inl a => @inl _ (sigT (fun n1 => ordinal (Arity (get_control (bg:=b1) n1))))
match a return (sig (fun infT0 => In infT0 (ndlist i1))) with
| exist a0 Pa =>
exist (fun infT0 => In infT0 (ndlist i1)) a0
(@proj1
(forall _ : In ia (ndlist i2), In ia (ndlist i1))
(forall _ : In ia (ndlist i1), In ia (ndlist i2))
(@bij_subset_lemma _ _ _ (fun inner => In inner (ndlist i2)) bij_id bij_i ia) Hia)))))).
intros.
destruct (get_link (bg:=b1)) eqn:L1.
* rewrite <- link_eq in L2.
simpl in L2. exfalso.
clear control_eq parent_eq e e0.
unfold parallel, bij_subset_forward, bij_subset_backward, bij_dep_sum_2_forward, bij_dep_sum_1_forward in L2.
simpl in L2.
unfold funcomp in L2.
simpl in L2.
rewrite L1 in L2.
discriminate L2.
* f_equal. apply subset_eq_compat.
rewrite <- link_eq in L2.
simpl in L2.
clear control_eq parent_eq e e0.
unfold parallel, bij_subset_forward, bij_subset_backward, bij_dep_sum_2_forward, bij_dep_sum_1_forward in L2.
simpl in L2.
unfold funcomp in L2.
rewrite L1 in L2.
inversion L2. reflexivity.
- generalize (ex_intro
(fun ip'' => get_link (bg:=b2) ip'' = get_link (bg:=b2) (inr pa))
(inr pa)
(erefl (get_link (bg:=b2) (inr pa)))).
intros.
destruct get_link eqn:L2.
+ generalize (ex_intro
(fun ip' =>
get_link (bg:=b1) ip' =
get_link (bg:=b1)
(inr (bij_dep_sum_2_forward
(forall _ : In a0 (ndlist i2), In a0 (ndlist i1))
(forall _ : In a0 (ndlist i1), In a0 (ndlist i2))
(@bij_subset_lemma _ _
(fun infT0 => In infT0 (ndlist i1))
(fun inner => In inner (ndlist i2)) bij_id bij_i a0) Pa)
end
| inr c => @inr (sig (fun infT0 => In infT0 (ndlist i1))) _
(bij_dep_sum_2_forward
(fun a => bijection_inv (bij_p a))
(bij_dep_sum_1_forward (bijection_inv bij_n) pa))))
(inr (bij_dep_sum_2_forward
(bij_dep_sum_1_forward (bijection_inv bij_n) c))
end
(erefl (get_link (bg:=b1)
match ipa return
(sum (sig (fun infT0 => In infT0 (ndlist i1)))
(sigT (fun n1 => ordinal (Arity (get_control (bg:=b1) n1))))) with
| inl a => @inl _ (sigT (fun n1 => ordinal (Arity (get_control (bg:=b1) n1))))
match a return (sig (fun infT0 => In infT0 (ndlist i1))) with
| exist a0 Pa => exist (fun infT0 => In infT0 (ndlist i1)) a0
(@proj1
(forall _ : In a0 (ndlist i2), In a0 (ndlist i1))
(forall _ : In a0 (ndlist i1), In a0 (ndlist i2))
(@bij_subset_lemma _ _
(fun infT0 => In infT0 (ndlist i1))
(fun inner => In inner (ndlist i2)) bij_id bij_i a0) Pa)
end
| inr c => @inr (sig (fun infT0 => In infT0 (ndlist i1))) _
(bij_dep_sum_2_forward
(fun a => bijection_inv (bij_p a))
(bij_dep_sum_1_forward (bijection_inv bij_n) pa)))
(erefl
(get_link (bg:=b1)
(inr (bij_dep_sum_2_forward
(fun a : get_node b1 => bijection_inv (bij_p a))
(bij_dep_sum_1_forward (bijection_inv bij_n) pa)))))).
(bij_dep_sum_1_forward (bijection_inv bij_n) c))
end))).
intros.
destruct (get_link (bg:= b1)) eqn:L1.
* f_equal. destruct s3. destruct s0. apply subset_eq_compat.
simpl in L2.
simpl in L1.
rewrite <- link_eq in L2.
simpl in L2.
clear control_eq parent_eq e e0.
unfold parallel, bij_subset_forward, bij_subset_backward, bij_dep_sum_2_forward, bij_dep_sum_1_forward in L2.
simpl in L2.
unfold funcomp in L2.
rewrite L1 in L2.
inversion L2. reflexivity.
* rewrite <- link_eq in L2.
simpl in L2. exfalso.
clear control_eq parent_eq e e0.
unfold parallel, bij_subset_forward, bij_subset_backward, bij_dep_sum_2_forward, bij_dep_sum_1_forward in L2.
simpl in L2.
unfold funcomp in L2.
simpl in L2.
rewrite L1 in L2.
discriminate L2.
+ generalize (ex_intro
(fun ip' =>
get_link (bg:=b1) ip' =
get_link (bg:=b1)
(inr (bij_dep_sum_2_forward
(fun a : get_node b1 => bijection_inv (bij_p a))
(bij_dep_sum_1_forward (bijection_inv bij_n) pa))))
(inr (bij_dep_sum_2_forward
(fun a : get_node b1 => bijection_inv (bij_p a))
(bij_dep_sum_1_forward (bijection_inv bij_n) pa)))
(erefl
(get_link (bg:=b1)
(inr (bij_dep_sum_2_forward
(fun a : get_node b1 => bijection_inv (bij_p a))
(bij_dep_sum_1_forward (bijection_inv bij_n) pa)))))).
intros.
destruct (get_link (bg:= b1)) eqn:L1.
* rewrite <- link_eq in L2.
simpl in L2. exfalso.
clear control_eq parent_eq e e0.
unfold parallel, bij_subset_forward, bij_subset_backward, bij_dep_sum_2_forward, bij_dep_sum_1_forward in L2.
simpl in L2.
unfold funcomp in L2.
simpl in L2.
rewrite L1 in L2.
discriminate L2.
* f_equal. apply subset_eq_compat.
simpl in L2.
simpl in L1.
rewrite <- link_eq in L2.
simpl in L2.
clear control_eq parent_eq e e0.
unfold parallel, bij_subset_forward, bij_subset_backward, bij_dep_sum_2_forward, bij_dep_sum_1_forward in L2.
simpl in L2.
unfold funcomp in L2.
rewrite L1 in L2.
inversion L2. reflexivity.
destruct get_link eqn:L2;
destruct (get_link (bg:=b1)) eqn:L1;
rewrite <- link_eq in L2; simpl in L2;
unfold parallel, bij_subset_forward, bij_subset_backward, bij_dep_sum_2_forward, bij_dep_sum_1_forward in L2;
simpl in L2; unfold funcomp in L2;
rewrite L1 in L2;
inversion L2.
* reflexivity.
* f_equal. apply subset_eq_compat. assumption.
Qed.
Theorem lean_support_equivalence_refl {s r : nat} {i o : b.n.NoDupList} (b : bigraph s i r o) :
lean_support_equivalence b b.
Proof.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment