Repository navigation
The release updates coq-fcsl-pcm to rocq-9.3/mathcomp-2.6.0.
It also contains a number of new and modified definitions and lemmas,
outlined below.
core/axioms.v:
inj_sval, cast, castE, icast, Tag, inj_tagT, inj_tagK,
inj_pair, inj_some.
core/pred.v:
In_rcons, In_rev, In_filter, In_map, mapPP, pmap_none, In_pmap,
pmapPP, map_pmap, eq_In_pmap, filter_Uniq, map_Uniq,
map_inj_In_Uniq, cat_Uniq, pmap_Uniq, pmap_filter_Uniq.
core/prelude.v:
inj_prod, inj_rcons, ord_neq, inj_indx, inj_ith, inj_indxE,
pmap_comp, pmap_map, pmap_some, filter_pmapE, Prefix_consE, PrefixE,
Prefix_size, Prefix_size', Prefix_catE, Prefix_catLE, Prefix_catP,
Prefix0s, Prefixs2, jmEK', jmE1.
core/seqext.v:
inj_cons, inj_consE, revE, rev_eqseq, inj_rev, catl_cancel,
catr_cancel, hasN_count, hasN_filter, count_filter0, count_pmap0,
hasN_pmap, count_rcons, has_first_split, has_last_split,
count1_split, count_splitE, pmap_rcons, pmap_rev, sorted_cat,
iotaDr, revA, permeq_filterC, filter_subseq_in, perm_subseq,
rcons_subseq, split_subseq, subset_catL, has_filterI, filter_sub,
filter_in, inj_index, head_mem, prefix_sub, prefix_subT, prefix_cat,
prefix_catl, prefix_catP, suffix_cat, suffix_catl, suffix_catP,
suffix_sub, disjointPR, disjointPL, prefix_disjT, subseq_permD,
map_subseq_inj, map_image_subseq, pmap_subseq, filter_subset,
index_pmap, index_pmap_inj, sorted_subset_subseq_irr,
sorted_subset_subseq_asym, sorted_ord_index, merge_eq,
merge_sort_push_eq, sort_eq, prefixes, prefixes0, prefixesT,
prefixesE, uniq_prefixes, map_f_prefixes, mem_map_prefix,
map_image_prefix, map_f_prefixes, map_image_prefixes, subseqs,
subseqs0, subseqsE, subseq_f_prefix, map_subseqs, map_image_subseqs,
suffx, suffxE, filter_cons_inv, filter_cat_inv, filter_rcons_inv,
map_cons_inv, map_cat_inv, map_rcons_inv, pmap_cons_inv,
pmap_cat_inv, pmap_rcons_inv, interleave, Prefix_interleave,
interleave0, interleave0E, interleaveC, interleaveA,
interleave_mask, interleave_seq, interleaves0, interleave0s,
interleave_seq_cons_cat, interleave_seq_permI, interleave_seq_perm
core/seqperm.v:
perm_consE, pperm_cat_consE, pperm_rcons_cons, pperm_pmap,
pperm_Uniq, pperm_uniq, pperm_merge, pperm_merge_sort_push,
pperm_sort, In_merge, In_merge_sort_push, In_sort, mem_merge,
mem_merge_sort_push, merge_lt_le, merge_sort_push_lt_le,
merge_sort_push_uniq, sort_lt_le.
core/useqord.v:
sle_mem2, sorted_slt_sle, sorted_slt_subseq, sorted_slt,
sorted_sle_subseq, slt_sorted, slt_sortedI, slt_sortedE, subseq_eq,
sle_sortedI, slt_findlast, slt_filterlast, has_first, prefixes_mono,
slt_map, slt_map_inj, sle_map, sle_map_inj, slt_pmap, slt_pmap_inj,
sle_pmap, sle_pmap_inj
core/uslice.v:
eqsl_prefix, prefix_eqsl, uniq_filt_uxou, uniq_filt_uoxu.
pcm/morphism.v:
big_pfjoin, inj_psub, inj_valx.
pcm/natmap.v:
sorted_leq_dom0, sorted_ltn_dom0, lastkeyN0, freshN1, oexlt_subdom,
oexle_subdom, oexltFK, oexleFK, oexltFKD, oexleFKD, slt_oexle,
slt_oexlt, sle_oexlt, sle_oexle.
pcm/natmodmap.v:
sum_dom_range, over_umfiltk, oevr, oevr_cat, oevr_cons, oevr_rcons,
oevr_join, perm_oevr, oevr_join2, oexler_umfiltk, oexler, oexler0,
oexler_cat, oexler_join, oexltr_umfiltk, oexltr, oexltr0,
oexltr_join, perm_oexle1, perm_oexle2, perm_oexleL, perm_oexleR,
sumrD, all_presums, end_sum, end_presum, consistently_oexle.
pcm/unionmap.v:
domUnEX, dom_subseqL, dom_subseqR, dom_subsetL, dom_subsetR,
slt_domE, slt_domI, slt_dom, sle_domE, sle_domI, sle_dom,
dom_maskUnL, dom_maskUnR, disjointDC, domUnL_predC, domUnR_predC,
inj_upd, assocs0E, In_assocs_fun, sorted_assocs, uniq_assocs,
range_perm, Uniq_rangeE, Uniq_rangeUn, In_big_range, rangeUnE,
mem_big_range, um_inj, um_mono_slt, um_slt_mono, um_mono_inj,
uminj_find, ummono_sltI, ummono_inj_sltI, ummono_sltP,
ummono_inj_sltP, omf_subdomT, path_omf, omf_subseq, omf_subseqT,
assocs_omf, range_omf, omf_disj, umfilt_subT, umfilt_sub0,
range_umfilt, subseq_range_umfilt, umfiltk_subT, umfiltv_subT,
umfiltk_sub0, umfiltv_sub0, umfiltk_dpredU, assocs_mf,
assocs_nil_inv, assocs_cons_inv, assocs_cat_inv, assocs_rcons_inv,
range_nil_inv, range_cons_inv, range_cat_inv, range_rcons_inv,
assocs_filterUnL, assocs_filterUnR, assocs_maskUn,
assocs_interleave, range_interleave, dom_maskUn, dom_interleave,
map_interleave_seq, assocs_interleave_seq, range_interleave_seq,
dom_interleave_seq, oevFKD, oev_subdom, oev_subdomL, oev_subdomR,
inj_invert, eq_in_umallb, kvseq, kvseq_nil, kvseq_cons, kvseq_cat,
kvseq_helper', valid_kvseq, kvseq_uniq, kvseq_all, dom_kvseqE,
size_dom_kvseq, In_kvseq, assocs_kvseq, kvseq_pperm, kvseq_assocs,
valid_kvseq_pmap_inj, valid_kvseq_map_inj, mf_kvseq,
omap_some_kvseq, mapv_kvseq, kvseq_assocs_mf, omf_kvseq,
kvseq_assocs_omf.