DmxLarchey
commented
6 years ago This summary was built using the PR "improve the file a bit" page from GH I can now close this PR
File bft_spec.v:
By default, cosmetic changes (like auto -> assumption) are integrated
Require Import does not have php anymore but utils is split in several files
line 116, I did keep firstorder to instanciate instead of exists because the introduced variable name x0 might clash with previously introduced fresh names (? inntro patterns)
line 196, the infix "~p" is now defined in list_utils.v
File bt.v
All the changes integrated
Removed the dependent induction principle for btb which is not needed anymore
File php.v
Line 20, no need to give an implicit type to p which is not used anymore Line 22, incl_cons_linv moved to list_utils.v, structured proof is integrated Line 29, same for incl_app_rinv Line 66-63, incl_pres_perm_left and incl_pres_perm_right moved to list_utils.v and renamed to perm_incl_left and perm_incl_right
list_length_rect removed and replaced by new tactic induction on l as IHl with measure (length l)
Line 73, Section Permutation_tools moved to list_utils.v Line 90, did not integrate r m for Implicit Type. I make the following remark concerning the Implicit Type directive.
Remark: I view the Implicit Type directive as an indication for the type-checker (unification), not as an indication for the human reader. So I give the minimal indication that allows type-checking. I think the human reader is generally more able to guess the type than the type-checker.
Line 100, perm_in_head now in list_utils.v with updates from RM
Line 114, list_prefix now in list_utils.v but a much shorter one line proof is given as an instance of the more general list_length_split.
Line 144, list_has_dup_app_right integrates RM updates
Line 151, list_hd_eq_perm integrates RM updates but in renamed perm_list_has_dup
Line 171, incl_right_cons_choose moved in list_utils.v with RM updates
Line 172, repeat_choice_two rewritten with the inductive "Forall (eq x) m" (I find it more readable) and the proof is adapted.
Line 197, incl_right_cons_incl_or_lhd_or_perm integrates RM updates
There is a new lemma called incl_left_right_php to factorize/flatten the proof of the generalized PHP length_le_and_incl_implies_dup_or_perm
Line 216, the proof of length_le_and_incl_implies_dup_or_perm is completelly rewritten (including some of the improvements of RM) to flatten/shorten it.
Line 269, identify_duplicates_from_dup/dup_from_duplicates replaced by list_has_dup_eq_duplicates on line 58
Line 294, finite_pigeon_hole now as a very short proof
File utils.v
Line 86--120 zip et al now moved to zip.v added zip_app_left_le and zip_app_right_le from RM further simplified proofs of zip_app_left and zip_app_right.
Line 121 the proof of zip_spec: I did not import the change tactic which is only usefull for the human eye
Line 166 & 173, included the comment about map_concat and map_zip
Line 181, indeed why not the type indication here (which contradicts my above remark/statement about implicit types ;-)
Line 190, no change tactic Line 193, clear IH is unnecessary
Line 215-, section app moved to list_utils.v
Line 288-, section Forall2 moved to list_utils.v
Line 291, type info on l & m unnecessary, enforcing my above remark (don't be crazy about the inherent contradiction in human taste)
Line 294, Forall2_zip_app moved to zip.v ... names of bounded variable l[12] and m[12] is also a matter of taste ...
first just for php.v
then also changes to the other files - all quite shallow