Skip to content

Commit 3231e08

Browse files
AnoudAlshnakatAnoudAlshnakat
committed
correcntess of merge done with no cheats
1 parent 3562f08 commit 3231e08

File tree

1 file changed

+143
-106
lines changed

1 file changed

+143
-106
lines changed

‎hol/bdd_gen_mergeScript.sml‎

Lines changed: 143 additions & 106 deletions
Original file line numberDiff line numberDiff line change
@@ -30,34 +30,6 @@ val _ = new_theory "bdd_gen_merge";
3030

3131

3232

33-
34-
Definition mergable_def:
35-
mergable ((r,edges,labels):('a,'b)BDD) n n' =
36-
(n≠n' ∧ ALOOKUP edges n = ALOOKUP edges n' ∧
37-
ALOOKUP labels n = ALOOKUP labels n' ∧ ALOOKUP labels n' ≠ NONE )
38-
End
39-
40-
41-
42-
Definition merge_edges_def:
43-
merge_edges (edges:edges) n n' =
44-
MAP (\(a,b,c). ( a, if (b=n' ∧ c=n') then (n,n)
45-
else if (b=n') then (n,c)
46-
else if (c=n') then (b,n)
47-
else (b,c))) edges
48-
End
49-
50-
51-
52-
Definition merge_def:
53-
merge ((r,edges,labels):('a,'b)BDD) n n' =
54-
let edges' = merge_edges (edges:edges) n n' in
55-
let edges'' = ADELKEY n' edges' in
56-
let labels' = ADELKEY n' labels in
57-
(r,edges'',labels')
58-
End
59-
60-
6133

6234
Theorem merge_lookup_none:
6335
∀ edges n n' n''.
@@ -472,56 +444,33 @@ Proof
472444
,
473445

474446
PairCases_on ‘x'’ >> gvs[] >>
447+
475448
Cases_on ‘ALOOKUP mv x’ >> gvs[] >> Cases_on ‘x'’ >> gvs[] >|[
476449

477450
(* true case *)
478451
(* is it a merged nodes i.e. (nr≠x'0) or not (nr=x'0) ... we started with non merged nodes *)
479452
Cases_on ‘nr=x'0’ >> gvs[] >|[
480453

481454
Cases_on ‘ALOOKUP edges nr’ >> gvs[] >|[
482-
483-
assume_tac mergable_correct_leaf >>
484-
last_x_assum (strip_assume_tac o (Q.SPECL [‘labels’,‘nr’,‘r’, ‘edges’, ‘n'’,
485-
‘n’, ‘mv’, ‘b’])) >>
486-
455+
487456
‘n'≠nr’ by metis_tac[merge_edges_res] >>
488-
gvs[]
489-
457+
metis_tac[mergable_correct_leaf]
490458
,
491459

492460
Cases_on ‘x'’ >> gvs[] >>
493-
494-
subgoal ‘∃pred x'. ALOOKUP labels nr = SOME (non_termn (SOME x',pred))’ >-
495-
(
496-
‘MEM nr (dom_range_edges edges)’ by imp_res_tac lookup_edges_in_domain >>
497-
imp_res_tac WF_imp_non_leaf_lbl >> gvs[]
498-
) >>
461+
‘MEM nr (dom_range_edges edges)’ by imp_res_tac lookup_edges_in_domain >>
462+
‘∃pred x'. ALOOKUP labels nr = SOME (non_termn (SOME x',pred))’ by
463+
(imp_res_tac WF_imp_non_leaf_lbl >> gvs[]) >>
499464

500465
gvs[] >>
466+
subgoal ‘THE (INDEX_OF x' vars_consumed) < THE (INDEX_OF x vars_consumed)’ >-
467+
(imp_res_tac ordered_for_two_labels) >>
501468

502469

503-
subgoal ‘THE (INDEX_OF x' vars_consumed) < THE (INDEX_OF x vars_consumed)’ >-(
504-
rgs[Once BDD_ordered_def] >>
505-
first_x_assum (strip_assume_tac o (Q.SPECL [‘n''’,‘nr’,‘nl’])) >>
506-
gvs[order_hold_def] >>
507-
508-
gvs[consumed_dom_bdd_def] >>
509-
res_tac >>
510-
imp_res_tac MEM_INDEX_OF >>
511-
512-
last_x_assum (strip_assume_tac o (Q.SPECL [‘i'’, ‘i’])) >>
513-
gvs[]
514-
) >>
515-
516-
gvs[] >>
517470
first_x_assum (strip_assume_tac o (Q.SPECL [‘INDEX_OF (x':string) (vars_consumed: string list)’])) >>
518-
gvs[] >>
519-
520-
first_x_assum (strip_assume_tac o (Q.SPECL [‘x'’, ‘vars_consumed’])) >>
521-
gvs[] >>
522-
523-
524-
first_x_assum (strip_assume_tac o (Q.SPECL [‘r’, ‘edges’, ‘labels’, ‘n’, ‘n'’, ‘nr’, ‘r'’, ‘q’, ‘pred'’, ‘mv’, ‘b’])) >>
471+
rgs[PULL_FORALL] >>
472+
first_x_assum (strip_assume_tac o (Q.SPECL [‘x'’, ‘vars_consumed’, ‘r’, ‘edges’, ‘labels’, ‘n’, ‘n'’,
473+
‘nr’, ‘r'’, ‘q’, ‘pred'’, ‘mv’, ‘b’])) >>
525474
gvs[] >>
526475

527476
‘n'≠nr’ by metis_tac[merge_edges_res] >>
@@ -544,6 +493,7 @@ Proof
544493
‘ALOOKUP edges n' = NONE’ by (metis_tac [merge_lookup_none]) >>
545494
simp[Once EQ_SYM_EQ, Once BDD_sem_cases]
546495
,
496+
547497
PairCases_on ‘x'’ >> gvs[] >>
548498
‘∃x'. ALOOKUP edges n = SOME x'’ by (imp_res_tac merge_lookup_exists >> gvs[]) >>
549499
PairCases_on ‘x'’ >> gvs[] >>
@@ -562,69 +512,155 @@ Proof
562512
‘∃ x'' p''. ALOOKUP labels n = SOME (non_termn (SOME x'',p'')) ’ by metis_tac[WF_imp_non_leaf_lbl] >>
563513
gvs[]
564514
,
565-
566-
Cases_on ‘ALOOKUP mv x'’ >> gvs[] >|[
567-
568-
gvs[mv_dom_bdd_def, lookup_is_some_def] >>
569-
res_tac >> gvs[]
570-
,
571-
572-
Cases_on ‘x''’ >> gvs[] >|[
515+
516+
(* ($var$(x'0'),x'1'') = (nl_old,nr_old)
517+
(x'0,$var$(x'1')) = (n1,n2) *)
518+
rename1 ‘SOME (nl_old,nr_old) = ALOOKUP edges n'’ >>
519+
rename1 ‘ALOOKUP (merge_edges edges n n') n = SOME (n1,n2)’ >>
520+
subgoal ‘∃ bool . ALOOKUP mv x' = SOME bool’>-
521+
(gvs[mv_dom_bdd_def, lookup_is_some_def] >> res_tac >> gvs[]) >>
573522

574-
(* true *)
575-
‘n' ≠ n'' ∧ nl ≠ n''’ by (imp_res_tac lookup_edges_not_parent >> gvs[]) >>
523+
Cases_on ‘bool’ >> (
576524

577-
qpat_x_assum ‘SOME ($var$(x'0'),x'1'') = ALOOKUP edges n'’ (fn thm => assume_tac (SIMP_RULE (srw_ss()) [Once EQ_SYM_EQ] thm)) >>
578-
‘n' ≠ $var$(x'0') ∧ n' ≠ x'1''’ by (imp_res_tac lookup_edges_not_parent >> gvs[]) >>
525+
(* true and false sub branches, same solution*)
526+
‘n' ≠ n'' ∧ nl ≠ n''’ by (imp_res_tac lookup_edges_not_parent >> gvs[]) >>
527+
528+
qpat_x_assum ‘SOME (nl_old,nr_old) = ALOOKUP edges n'’
529+
(fn thm => assume_tac (SIMP_RULE (srw_ss()) [Once EQ_SYM_EQ] thm)) >>
530+
‘n' ≠ nl_old∧ n' ≠ nr_old’ by (imp_res_tac lookup_edges_not_parent >> gvs[]) >>
579531

580-
(* we need to show that x'0 = $var$(x'0') *)
581-
‘ALOOKUP edges n = SOME ($var$(x'0'),x'1'')’ by gvs[] >>
582-
‘n ≠ $var$(x'0') ∧ n ≠ x'1''’ by (imp_res_tac lookup_edges_not_parent >> gvs[]) >>
583-
‘x'0 = $var$(x'0')’ by imp_res_tac merge_replaces_stays_same >>
532+
(* we need to show that n1 = nl_old *)
533+
‘ALOOKUP edges n = SOME (nl_old,nr_old)’ by gvs[] >>
534+
‘n ≠ nl_old ∧ n ≠ nr_old’ by (imp_res_tac lookup_edges_not_parent >> gvs[]) >>
535+
‘n1 = nl_old’ by imp_res_tac merge_replaces_stays_same >>
584536
rgs[] >>
585537
simp[Once EQ_SYM_EQ, Once BDD_sem_cases] >>
586538

587539

588540
subgoal ‘THE (INDEX_OF x' vars_consumed) < THE (INDEX_OF x vars_consumed)’ >-
589-
(
590-
rgs[Once BDD_ordered_def] >>
591-
first_x_assum (strip_assume_tac o (Q.SPECL [‘n''’,‘n'’,‘nl’])) >>
592-
gvs[order_hold_def] >>
593-
594-
gvs[consumed_dom_bdd_def] >>
595-
res_tac >>
596-
imp_res_tac MEM_INDEX_OF >>
541+
(imp_res_tac ordered_for_two_labels) >>
597542

598-
first_x_assum (strip_assume_tac o (Q.SPECL [‘i’, ‘i'’])) >>
599-
gvs[]
600-
601-
) >>
602-
603-
gvs[] >>
543+
604544
first_x_assum (strip_assume_tac o (Q.SPECL [‘INDEX_OF (x':string) (vars_consumed: string list)’])) >>
605-
gvs[] >>
606-
first_x_assum (strip_assume_tac o (Q.SPECL [‘x'’, ‘vars_consumed’])) >>
607-
gvs[] >>
608-
first_x_assum (strip_assume_tac o (Q.SPECL [‘r’, ‘edges’, ‘labels’, ‘n’, ‘n'’, ‘n’, ‘x'1''’, ‘x'0’, ‘r'’, ‘mv’, ‘b’])) >>
545+
gvs[PULL_FORALL] >>
546+
first_x_assum (strip_assume_tac o (Q.SPECL [‘x'’, ‘vars_consumed’, ‘r’, ‘edges’, ‘labels’, ‘n’,
547+
‘n'’, ‘n’, ‘nr_old’, ‘n1’, ‘r'’, ‘mv’, ‘b’])) >>
609548
rgs[] >>
610549

611550
gvs[Once BDD_sem_cases] >>
612-
simp[Once BDD_sem_cases] >> gvs[ALOOKUP_ADELKEY]
613-
,
551+
simp[Once BDD_sem_cases] >>
552+
gvs[ALOOKUP_ADELKEY]
553+
)
554+
]
555+
]
556+
]
557+
]
558+
,
559+
560+
(* false case: removed comments, similar proof *)
561+
Cases_on ‘nl=x'1’ >> gvs[] >|[
562+
563+
Cases_on ‘ALOOKUP edges nl’ >> gvs[] >|[
564+
565+
‘n'≠nl’ by metis_tac[merge_edges_res] >>
566+
metis_tac[mergable_correct_leaf]
567+
,
568+
569+
Cases_on ‘x'’ >> gvs[] >>
570+
‘MEM nl (dom_range_edges edges)’ by imp_res_tac lookup_edges_in_domain >>
571+
‘∃pred x'. ALOOKUP labels nl = SOME (non_termn (SOME x',pred))’ by
572+
(imp_res_tac WF_imp_non_leaf_lbl >> gvs[]) >>
573+
574+
gvs[] >>
575+
subgoal ‘THE (INDEX_OF x' vars_consumed) < THE (INDEX_OF x vars_consumed)’ >-
576+
(imp_res_tac ordered_for_two_labels) >>
577+
578+
579+
first_x_assum (strip_assume_tac o (Q.SPECL [‘INDEX_OF (x':string) (vars_consumed: string list)’])) >>
580+
rgs[PULL_FORALL] >>
581+
first_x_assum (strip_assume_tac o (Q.SPECL [‘x'’, ‘vars_consumed’, ‘r’, ‘edges’, ‘labels’, ‘n’, ‘n'’,
582+
‘nl’, ‘r'’, ‘q’, ‘pred'’, ‘mv’, ‘b’])) >>
583+
gvs[] >>
584+
585+
‘n'≠nl’ by metis_tac[merge_edges_res] >>
586+
gvs[]
587+
]
588+
,
589+
590+
(* we are working with a parent of a node that it's children gotten merged *)
591+
gvs[mergable_def] >>
592+
593+
(* we know that the parent's children are not random,
594+
before merge should be n' and after merge should be n *)
595+
‘x'1 = n ∧ nl = n' ’ by (imp_res_tac merge_parent_change >> metis_tac[]) >>
596+
rgs[] >>
597+
598+
simp[Once BDD_sem_cases] >> gvs[ALOOKUP_ADELKEY] >>
599+
Cases_on ‘ALOOKUP (merge_edges edges n n') n’ >> gvs[] >|[
600+
601+
‘ALOOKUP edges n' = NONE’ by (metis_tac [merge_lookup_none]) >>
602+
simp[Once EQ_SYM_EQ, Once BDD_sem_cases]
603+
,
604+
605+
PairCases_on ‘x'’ >> gvs[] >>
606+
‘∃x'. ALOOKUP edges n = SOME x'’ by (imp_res_tac merge_lookup_exists >> gvs[]) >>
607+
PairCases_on ‘x'’ >> gvs[] >>
608+
Cases_on ‘ALOOKUP labels n'’ >> gvs[] >>
609+
Cases_on ‘x'’ >> gvs[] >|[
610+
611+
‘∃pair. ALOOKUP edges n = SOME pair’ by metis_tac [merge_lookup_exists] >>
612+
‘∃ x'' p''. ALOOKUP labels n = SOME (non_termn (SOME x'',p'')) ’ by metis_tac[WF_imp_non_leaf_lbl] >>
613+
gvs[]
614+
,
615+
616+
Cases_on ‘p’ >> gvs[] >>
617+
Cases_on ‘q’ >> gvs[] >|[
618+
619+
‘∃pair. ALOOKUP edges n = SOME pair’ by metis_tac [merge_lookup_exists] >>
620+
‘∃ x'' p''. ALOOKUP labels n = SOME (non_termn (SOME x'',p'')) ’ by metis_tac[WF_imp_non_leaf_lbl] >>
621+
gvs[]
622+
,
614623

615-
cheat
624+
rename1 ‘SOME (nl_old,nr_old) = ALOOKUP edges n'’ >>
625+
rename1 ‘ALOOKUP (merge_edges edges n n') n = SOME (n1,n2)’ >>
626+
subgoal ‘∃ bool . ALOOKUP mv x' = SOME bool’>-
627+
(gvs[mv_dom_bdd_def, lookup_is_some_def] >> res_tac >> gvs[]) >>
616628

629+
Cases_on ‘bool’ >> (
617630

618-
]
619-
]
631+
(* true and false sub branches, same solution*)
632+
‘n' ≠ n'' ∧ nr ≠ n''’ by (imp_res_tac lookup_edges_not_parent >> gvs[]) >>
633+
634+
qpat_x_assum ‘SOME (nl_old,nr_old) = ALOOKUP edges n'’
635+
(fn thm => assume_tac (SIMP_RULE (srw_ss()) [Once EQ_SYM_EQ] thm)) >>
636+
‘n' ≠ nl_old∧ n' ≠ nr_old’ by (imp_res_tac lookup_edges_not_parent >> gvs[]) >>
637+
638+
(* we need to show that n1 = nl_old *)
639+
‘ALOOKUP edges n = SOME (nl_old,nr_old)’ by gvs[] >>
640+
‘n ≠ nl_old ∧ n ≠ nr_old’ by (imp_res_tac lookup_edges_not_parent >> gvs[]) >>
641+
‘n1 = nl_old’ by imp_res_tac merge_replaces_stays_same >>
642+
rgs[] >>
643+
simp[Once EQ_SYM_EQ, Once BDD_sem_cases] >>
644+
645+
646+
subgoal ‘THE (INDEX_OF x' vars_consumed) < THE (INDEX_OF x vars_consumed)’ >-
647+
(imp_res_tac ordered_for_two_labels) >>
648+
649+
650+
first_x_assum (strip_assume_tac o (Q.SPECL [‘INDEX_OF (x':string) (vars_consumed: string list)’])) >>
651+
gvs[PULL_FORALL] >>
652+
first_x_assum (strip_assume_tac o (Q.SPECL [‘x'’, ‘vars_consumed’, ‘r’, ‘edges’, ‘labels’, ‘n’,
653+
‘n'’, ‘n’, ‘nr_old’, ‘n1’, ‘r'’, ‘mv’, ‘b’])) >>
654+
rgs[] >>
655+
656+
gvs[Once BDD_sem_cases] >>
657+
simp[Once BDD_sem_cases] >>
658+
gvs[ALOOKUP_ADELKEY]
659+
)
620660
]
621661
]
622-
]
623-
624-
662+
]
625663
]
626-
,
627-
cheat
628664

629665
]
630666
]
@@ -792,6 +828,7 @@ QED
792828
(* *)
793829
(*******************************************************)
794830

831+
(* move to genScript *)
795832
Definition eleminatble_def:
796833
eleminatble ((r,edges,labels):('a,'b)BDD) n n' =
797834
(n≠n' ∧ ALOOKUP edges n' = SOME (n,n) )

0 commit comments

Comments
 (0)