diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,742 +1,743 @@ ABY3_Protocols ADS_Functor AI_Planning_Languages_Semantics AODV AOT AVL-Trees AWN Abortable_Linearizable_Modules Abs_Int_ITP2012 Abstract-Hoare-Logics Abstract-Rewriting Abstract_Completeness Abstract_Soundness Ackermanns_not_PR Actuarial_Mathematics Adaptive_State_Counting Affine_Arithmetic Aggregation_Algebras Akra_Bazzi Algebraic_Numbers Algebraic_VCs Allen_Calculus Amicable_Numbers Amortized_Complexity AnselmGod Applicative_Lifting Approximation_Algorithms Architectural_Design_Patterns Aristotles_Assertoric_Syllogistic Arith_Prog_Rel_Primes ArrowImpossibilityGS Attack_Trees Auto2_HOL Auto2_Imperative_HOL AutoFocus-Stream Automated_Stateful_Protocol_Verification Automatic_Refinement AxiomaticCategoryTheory BDD BD_Security_Compositional BNF_CC BNF_Operations BTree Balog_Szemeredi_Gowers Banach_Steinhaus Belief_Revision Bell_Numbers_Spivey BenOr_Kozen_Reif Berlekamp_Zassenhaus Bernoulli Bertrands_Postulate Bicategory BinarySearchTree Binary_Code_Imprimitive Binding_Syntax_Theory Binomial-Heaps Binomial-Queues BirdKMP Birkhoff_Finite_Distributive_Lattices Blue_Eyes Bondy Boolean_Expression_Checkers Boolos_Curious_Inference Boolos_Curious_Inference_Automated Bounded_Deducibility_Security Buchi_Complementation Budan_Fourier Buffons_Needle Buildings BytecodeLogicJmlTypes C2KA_DistributedSystems CAVA_Automata CAVA_LTL_Modelchecker CCS CHERI-C_Memory_Model CISC-Kernel CRDT CRYSTALS-Kyber CSP_RefTK CVP_Hardness CYK CZH_Elementary_Categories CZH_Foundations CZH_Universal_Constructions CakeML CakeML_Codegen Call_Arity Card_Equiv_Relations Card_Multisets Card_Number_Partitions Card_Partitions Cartan_FP Case_Labeling Catalan_Numbers Category Category2 Category3 Cauchy Cayley_Hamilton Certification_Monads Chandy_Lamport Chord_Segments Circus Clean Clique_and_Monotone_Circuits ClockSynchInst Closest_Pair_Points CoCon CoSMeDis CoSMed CofGroups Coinductive Coinductive_Languages Collections Combinable_Wands Combinatorial_Enumeration_Algorithms Combinatorics_Words Combinatorics_Words_Graph_Lemma Combinatorics_Words_Lyndon CommCSL Commuting_Hermitian Comparison_Sort_Lower_Bound Compiling-Exceptions-Correctly Complete_Non_Orders Completeness Complex_Bounded_Operators Complex_Geometry Complx ComponentDependencies ConcurrentGC ConcurrentIMP Concurrent_Ref_Alg Concurrent_Revisions Conditional_Simplification Conditional_Transfer_Rule Consensus_Refined Constructive_Cryptography Constructive_Cryptography_CM Constructor_Funs Containers Cook_Levin CoreC++ Core_DOM Core_SC_DOM Correctness_Algebras Cotangent_PFD_Formula Count_Complex_Roots CryptHOL CryptoBasedCompositionalProperties Cubic_Quartic_Equations DFS_Framework DOM_Components DPRM_Theorem DPT-SAT-Solver DataRefinementIBP Datatype_Order_Generator Decl_Sem_Fun_PL Decreasing-Diagrams Decreasing-Diagrams-II Dedekind_Real Deep_Learning Delta_System_Lemma Density_Compiler Dependent_SIFUM_Refinement Dependent_SIFUM_Type_Systems Depth-First-Search Derangements Deriving Descartes_Sign_Rule Design_Theory Dict_Construction Differential_Dynamic_Logic Differential_Game_Logic Digit_Expansions Dijkstra_Shortest_Path Diophantine_Eqns_Lin_Hom Dirichlet_L Dirichlet_Series DiscretePricing Discrete_Summation DiskPaxos Distributed_Distinct_Elements Dominance_CHK DynamicArchitectures Dynamic_Tables E_Transcendental Echelon_Form EdmondsKarp_Maxflow Edwards_Elliptic_Curves_Group Efficient-Mergesort Elliptic_Curves_Group_Law Encodability_Process_Calculi Epistemic_Logic Equivalence_Relation_Enumeration Ergodic_Theory Error_Function Euler_MacLaurin Euler_Partition Eval_FO Example-Submission Expander_Graphs Extended_Finite_State_Machine_Inference Extended_Finite_State_Machines FFT FLP FOL-Fitting FOL_Axiomatic FOL_Harrison FOL_Seq_Calc1 FOL_Seq_Calc2 FOL_Seq_Calc3 FO_Theory_Rewriting FSM_Tests Factor_Algebraic_Polynomial Factored_Transition_System_Bounding Falling_Factorial_Sum Farkas FeatherweightJava Featherweight_OCL Fermat3_4 FileRefinement FinFun Finger-Trees Finite-Map-Extras Finite_Automata_HF Finite_Fields Finitely_Generated_Abelian_Groups First_Order_Terms First_Welfare_Theorem Fishburn_Impossibility Fisher_Yates Fishers_Inequality Flow_Networks Floyd_Warshall Flyspeck-Tame FocusStreamsCaseStudies Forcing Formal_Puiseux_Series Formal_SSA Formula_Derivatives Foundation_of_geometry Fourier Free-Boolean-Algebra Free-Groups Frequency_Moments Fresh_Identifiers FunWithFunctions FunWithTilings Functional-Automata Functional_Ordered_Resolution_Prover Furstenberg_Topology GPU_Kernel_PL Gabow_SCC GaleStewart_Games Gale_Shapley Game_Based_Crypto Gauss-Jordan-Elim-Fun Gauss_Jordan Gauss_Sums Gaussian_Integers GenClock General-Triangle Generalized_Counting_Sort Generic_Deriving Generic_Join GewirthPGCProof Girth_Chromatic Given_Clause_Loops GoedelGod Goedel_HFSet_Semantic Goedel_HFSet_Semanticless Goedel_Incompleteness Goodstein_Lambda GraphMarkingIBP Graph_Saturation Graph_Theory Green Groebner_Bases Groebner_Macaulay Gromov_Hyperbolicity Grothendieck_Schemes Group-Ring-Module HOL-CSP HOLCF-Prelude HRB-Slicing Hahn_Jordan_Decomposition Hales_Jewett Heard_Of Hello_World HereditarilyFinite Hermite Hermite_Lindemann Hidden_Markov_Models Higher_Order_Terms HoareForDivergence Hoare_Time Hood_Melville_Queue HotelKeyCards Huffman Hybrid_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Systems_VCs HyperCTL HyperHoareLogic Hyperdual IEEE_Floating_Point IFC_Tracking IMAP-CRDT IMO2019 IMP2 IMP2_Binary_Heap IMP_Compiler IMP_Compiler_Reuse IP_Addresses Imperative_Insertion_Sort Implicational_Logic Impossible_Geometry Incompleteness Incredible_Proof_Machine Independence_CH Inductive_Confidentiality Inductive_Inference InfPathElimination InformationFlowSlicing InformationFlowSlicing_Inter Integration Interpolation_Polynomials_HOL_Algebra Interpreter_Optimizations Interval_Arithmetic_Word32 Intro_Dest_Elim Involutions2Squares Iptables_Semantics Irrational_Series_Erdos_Straus Irrationality_J_Hancl Irrationals_From_THEBOOK IsaGeoCoq IsaNet Isabelle_C Isabelle_Marries_Dirac Isabelle_Meta_Model Jacobson_Basic_Algebra Jinja JinjaDCI JinjaThreads JiveDataStoreModel Jordan_Hoelder Jordan_Normal_Form KAD KAT_and_DRA KBPs KD_Tree Key_Agreement_Strong_Adversaries Khovanskii_Theorem Kleene_Algebra Kneser_Cauchy_Davenport Knights_Tour Knot_Theory Knuth_Bendix_Order Knuth_Morris_Pratt Koenigsberg_Friendship Kruskal Kuratowski_Closure_Complement LLL_Basis_Reduction LLL_Factorization LOFT LP_Duality LTL LTL_Master_Theorem LTL_Normal_Form LTL_to_DRA LTL_to_GBA Lam-ml-Normalization LambdaAuth LambdaMu Lambda_Free_EPO Lambda_Free_KBOs Lambda_Free_RPOs Lambert_W Landau_Symbols Laplace_Transform Latin_Square LatticeProperties Launchbury Laws_of_Large_Numbers Lazy-Lists-II Lazy_Case Lehmer Lifting_Definition_Option Lifting_the_Exponent LightweightJava LinearQuantifierElim Linear_Inequalities Linear_Programming Linear_Recurrences Liouville_Numbers List-Index List-Infinite List_Interleaving List_Inversions List_Update LocalLexing Localization_Ring Locally-Nameless-Sigma Logging_Independent_Anonymity Lowe_Ontological_Argument Lower_Semicontinuous Lp Lucas_Theorem MDP-Algorithms MDP-Rewards MFMC_Countable MFODL_Monitor_Optimized MFOTL_Monitor MSO_Regex_Equivalence Markov_Models Marriage Mason_Stothers Matrices_for_ODEs Matrix Matrix_Tensor Matroids Max-Card-Matching Maximum_Segment_Sum Median_Method Median_Of_Medians_Selection Menger Mereology Mersenne_Primes Metalogic_ProofChecker MiniML MiniSail Minimal_SSA Minkowskis_Theorem Minsky_Machines Modal_Logics_for_NTS Modular_Assembly_Kit_Security Modular_arithmetic_LLL_and_HNF_algorithms Monad_Memo_DP Monad_Normalisation MonoBoolTranAlgebra MonoidalCategory Monomorphic_Monad MuchAdoAboutTwo Multi_Party_Computation Multirelations Multiset_Ordering_NPC Multitape_To_Singletape_TM Myhill-Nerode Name_Carrying_Type_Inference Nano_JSON Nash_Williams Nat-Interval-Logic Native_Word Nested_Multisets_Ordinals Network_Security_Policy_Verification Neumann_Morgenstern_Utility No_FTL_observers No_FTL_observers_Gen_Rel Nominal2 Noninterference_CSP Noninterference_Concurrent_Composition Noninterference_Generic_Unwinding Noninterference_Inductive_Unwinding Noninterference_Ipurge_Unwinding Noninterference_Sequential_Composition NormByEval Nullstellensatz Number_Theoretic_Transform Octonions OpSets Open_Induction Optics Optimal_BST Orbit_Stabiliser Order_Lattice_Props Ordered_Resolution_Prover Ordinal Ordinal_Partitions Ordinals_and_Cardinals Ordinary_Differential_Equations PAC_Checker PAL PAPP_Impossibility PCF PLM POPLmark-deBruijn PSemigroupsConvolution Package_logic Padic_Field Padic_Ints Pairing_Heap Paraconsistency Parity_Game Partial_Function_MR Partial_Order_Reduction Password_Authentication_Protocol Pell Perfect-Number-Thm Perron_Frobenius Physical_Quantities Pi_Calculus Pi_Transcendental Planarity_Certificates Pluennecke_Ruzsa_Inequality Poincare_Bendixson Poincare_Disc Polynomial_Factorization Polynomial_Interpolation Polynomials Pop_Refinement Posix-Lexing Possibilistic_Noninterference Power_Sum_Polynomials Pratt_Certificate Prefix_Free_Code_Combinators Presburger-Automata Prim_Dijkstra_Simple Prime_Distribution_Elementary Prime_Harmonic_Series Prime_Number_Theorem Priority_Queue_Braun Priority_Search_Trees Probabilistic_Noninterference Probabilistic_Prime_Tests Probabilistic_System_Zoo Probabilistic_Timed_Automata Probabilistic_While Probability_Inequality_Completeness Program-Conflict-Analysis Progress_Tracking Projective_Geometry Projective_Measurements Promela Proof_Strategy_Language PropResPI Propositional_Logic_Class Propositional_Proof_Systems Prpu_Maxflow PseudoHoops Psi_Calculi Ptolemys_Theorem Public_Announcement_Logic QHLProver QR_Decomposition Quantales Quantifier_Elimination_Hybrid Quasi_Borel_Spaces Quaternions Query_Optimization Quick_Sort_Cost RIPEMD-160-SPARK ROBDD RSAPSS Ramsey-Infinite Random_BSTs Random_Graph_Subgraph_Threshold Randomised_BSTs Randomised_Social_Choice Rank_Nullity_Theorem Real_Impl Real_Power Real_Time_Deque Recursion-Addition Recursion-Theory-I Refine_Imperative_HOL Refine_Monadic RefinementReactive Regex_Equivalence Registers Regression_Test_Selection Regular-Sets Regular_Algebras Regular_Tree_Relations Relation_Algebra Relational-Incorrectness-Logic Relational_Disjoint_Set_Forests Relational_Forests Relational_Method Relational_Minimum_Spanning_Trees Relational_Paths Rensets Rep_Fin_Groups ResiduatedTransitionSystem Residuated_Lattices Resolution_FOL Rewrite_Properties_Reduction Rewriting_Z Ribbon_Proofs Risk_Free_Lending Robbins-Conjecture Robinson_Arithmetic Root_Balanced_Tree Roth_Arithmetic_Progressions Routing Roy_Floyd_Warshall SATSolverVerification SCC_Bloemen_Sequential SC_DOM_Components SDS_Impossibility SIFPL SIFUM_Type_Systems SPARCv8 Safe_Distance Safe_OCL Safe_Range_RC Saturation_Framework Saturation_Framework_Extensions Sauer_Shelah_Lemma Schutz_Spacetime +Schwartz_Zippel Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL Separation_Logic_Unbounded SequentInvertibility Shadow_DOM Shadow_SC_DOM Shivers-CFA ShortestPath Show Sigma_Commit_Crypto Signature_Groebner Simpl Simple_Clause_Learning Simple_Firewall Simplex Simplicial_complexes_and_boolean_functions SimplifiedOntologicalArgument Skew_Heap Skip_Lists Slicing Sliding_Window_Algorithm Smith_Normal_Form Smooth_Manifolds Solidity Sophomores_Dream Sort_Encodings Source_Coding_Theorem SpecCheck Special_Function_Bounds Splay_Tree Sqrt_Babylonian Stable_Matching Stalnaker_Logic Statecharts Stateful_Protocol_Composition_and_Typing Stellar_Quorums Stern_Brocot Stewart_Apollonius Stirling_Formula Stochastic_Matrices Stone_Algebras Stone_Kleene_Relation_Algebras Stone_Relation_Algebras Store_Buffer_Reduction Stream-Fusion Stream_Fusion_Code StrictOmegaCategories Strong_Security Sturm_Sequences Sturm_Tarski Stuttering_Equivalence Subresultants Subset_Boolean_Algebras SumSquares Sunflowers SuperCalc Suppes_Theorem Surprise_Paradox Symmetric_Polynomials Syntax_Independent_Logic Synthetic_Completeness Szemeredi_Regularity Szpilrajn TESL_Language TLA Tail_Recursive_Functions Tarskis_Geometry Taylor_Models Three_Circles Timed_Automata Topological_Semantics Topology TortoiseHare Transcendence_Series_Hancl_Rucki Transformer_Semantics Transition_Systems_and_Automata Transitive-Closure Transitive-Closure-II Transitive_Models Treaps Tree-Automata Tree_Decomposition Triangle Trie Turans_Graph_Theorem Twelvefold_Way Two_Generated_Word_Monoids_Intersection Tycon Types_Tableaus_and_Goedels_God Types_To_Sets_Extension UPF UPF_Firewall UTP Undirected_Graph_Theory Universal_Hash_Families Universal_Turing_Machine UpDown_Scheme VYDRA_MDL Valuation Van_Emde_Boas_Trees Van_der_Waerden VectorSpace VeriComp Verified-Prover Verified_SAT_Based_AI_Planning VerifyThis2018 VerifyThis2019 Vickrey_Clarke_Groves Virtual_Substitution VolpanoSmith WHATandWHERE_Security WOOT_Strong_Eventual_Consistency WebAssembly Weight_Balanced_Trees Weighted_Arithmetic_Geometric_Mean Weighted_Path_Order Well_Quasi_Orders Wetzels_Problem Winding_Number_Eval Word_Lib WorkerWrapper X86_Semantics XML Youngs_Inequality ZFC_in_HOL Zeta_3_Irrational Zeta_Function pGCL diff --git a/thys/Schwartz_Zippel/ROOT b/thys/Schwartz_Zippel/ROOT new file mode 100644 --- /dev/null +++ b/thys/Schwartz_Zippel/ROOT @@ -0,0 +1,14 @@ +chapter AFP + +session Schwartz_Zippel (AFP) = "HOL-Probability" + + options [timeout = 1800] + sessions + Skip_Lists + Factor_Algebraic_Polynomial + Jordan_Normal_Form + theories + Schwartz_Zippel + Rand_Perfect_Matching + document_files + "root.tex" + "root.bib" diff --git a/thys/Schwartz_Zippel/Rand_Perfect_Matching.thy b/thys/Schwartz_Zippel/Rand_Perfect_Matching.thy new file mode 100644 --- /dev/null +++ b/thys/Schwartz_Zippel/Rand_Perfect_Matching.thy @@ -0,0 +1,637 @@ +section \A Probabilistic Test for Perfect Matchings\ +theory Rand_Perfect_Matching imports + Schwartz_Zippel + Jordan_Normal_Form.Determinant +begin + +text \ + We use a simple representation of bipartite graphs (with same no. vertices) + @{term [show_types] \V :: nat\}, @{term [show_types] \E :: (nat \ nat) list\} + where \V\ is the number of vertices in each partition and \(x,y) \ E\ represents an edge + between vertex \x\ in the left partition and vertex \y\ in the right partition. +\ + +definition is_matching:: + "(nat \ nat) list \ (nat \ nat) list \ bool" + where "is_matching E match \ + set match \ set E \ + distinct (map fst match) \ + distinct (map snd match)" + +definition has_perfect_matching:: + "nat \ (nat \ nat) list \ bool" + where "has_perfect_matching V E \ + (\match. is_matching E match \ length match = V)" + +(* The polynomial matrix *) +definition adj_mat::"nat \ (nat \ nat) list \ + int mpoly mat" + where "adj_mat V E = + mat V V (\(i,j). + if (i,j) \ set E then Var (i*V+j) else 0)" + +lemma adj_mat_square[simp]: + shows + "dim_row (adj_mat V E) = V" + "dim_col (adj_mat V E) = V" + unfolding adj_mat_def + by auto + +lemma perfect_match_set_map_fst: + assumes "set E \ {0.. {0.. set (map fst E)" + using assms(2) unfolding is_matching_def + by auto + moreover have "... \ {0.. {0.. set (map fst match)" + by (metis assms(2) assms(3) card_atLeastLessThan card_subset_eq diff_zero distinct_card finite_atLeastLessThan is_matching_def length_map) + show ?thesis using 1 2 by auto +qed + +lemma perfect_match_set_map_snd: + assumes "set E \ {0.. {0.. set (map snd E)" + using assms(2) unfolding is_matching_def + by auto + moreover have "... \ {0.. {0.. set (map snd match)" + by (metis assms(2) assms(3) card_atLeastLessThan card_subset_eq diff_zero distinct_card finite_atLeastLessThan is_matching_def length_map) + show ?thesis using 1 2 by auto +qed + +lemma is_matching_permutes: + assumes "set E \ {0.. {0..i. i < V \ (i, f i) \ set E" +proof - + have fV: "set (map fst match) = {0..i. if i < V then the (map_of match i) else i)" + have "distinct (map snd match)" + using assms(2) is_matching_def by auto + from inj_on_map_of'[OF this] + have "inj_on (the \ map_of match) {0..x. x < V \ + \y. y < V \ map_of match x = Some y" + proof - + fix x + assume "x < V" + then obtain xy where xy: "xy \ set match" "fst xy = x" + using fV that unfolding atLeastLessThan_iff list.set_map + by (metis atLeastLessThan_iff image_iff zero_le) + then have "snd xy < V" using sV + by auto + have "map_of match x = Some (snd xy)" + using assms(2) is_matching_def xy(1) xy(2) by auto + show "\ymap_of match x = Some (snd xy)\ \snd xy < V\) + qed + then have 2: "f \ {0.. {0.. (i, f i) \ set E" for i + unfolding f_def + using \\x. x < V \ \y assms(2) is_matching_def by fastforce + + show ?thesis using that 1 2 by auto +qed + +lemma Var_not_0: + shows"Var x \ (0::'a::idom mpoly)" + by (simp add: Var_altdef) + +(* Copied from Missing_Polynomial.sum_monom_0_iff *) +lemma sum_monom_0_iff: + assumes fin: "finite S" + and g: "\i j. i \ S \ j \ S \ g i = g j \ i = j" + shows "sum (\ i. MPoly_Type.monom (g i) (f i)) S = 0 \ (\ i \ S. f i = 0)" (is "?l = ?r") +proof - + { + assume "\ ?r" + then obtain i where i: "i \ S" and fi: "f i \ 0" by auto + let ?g = "\ i. MPoly_Type.monom (g i) (f i)" + have "MPoly_Type.coeff (sum ?g S) (g i) = + f i + sum (\ j. MPoly_Type.coeff (?g j) (g i)) (S - {i})" + by (simp add: More_MPoly_Type.coeff_monom sum.remove[OF fin i]) + also have "sum (\ j. MPoly_Type.coeff (?g j) (g i)) (S - {i}) = 0" + by (smt (verit, ccfv_threshold) DiffE More_MPoly_Type.coeff_monom assms(2) i insert_iff sum.neutral when_simps(2)) + finally have "MPoly_Type.coeff (sum ?g S) (g i) \ 0" using fi by auto + hence "\ ?l" + by fastforce + } + thus ?thesis by auto +qed + +lemma prod_Var: + assumes"finite S" + shows "prod (\i. Var(f i)) S = + MPoly_Type.monom (sum (\i. monomial 1 (f i)) S) 1" + using assms +proof (induction S) + case empty + then show ?case + by auto +next + case (insert x F) + then show ?case + by (auto simp add: Var_altdef MPoly_Type.mult_monom) +qed + +lemma det_adj_mat: + shows "det (adj_mat V E) = + (\p | p permutes {0..i. + monomial 1 (i * V + p i)) {0..i < V. (i,p i) \ set E then + of_int (sign p) + else 0))" + unfolding det_def + by (force intro!: sum.cong simp add: adj_mat_def prod_Var monom_uminus sign_def) + +lemma vars_prod_Var: + assumes "finite S" + shows"vars (prod Var S) = S" + apply (subst prod_Var[OF assms]) + apply (subst vars_monom_keys) + subgoal + by simp + apply (subst keys_sum[OF assms]) + by auto + +lemma prod_Var_eq: + assumes "finite S" "finite T" + assumes "prod Var S = prod Var T" + shows "S = T" + using assms vars_prod_Var + by metis + +lemma pair_enc_eq: + assumes " a * V + b = c * V + d" + assumes "b < V" "d < V" + shows "b = (d::nat)" + by (metis Euclidean_Division.div_eq_0_iff add_right_cancel assms(1) assms(2) assms(3) diff_add_inverse div_mult_self3 mult_eq_0_iff) + +lemma sum_monomial_eq: + assumes"f permutes {0..i = 0..i = 0..i. i * V + f i) {0..i. i * V + g i) {0..i. monomial (1::nat) (i * V + f i)) {0..i. monomial (1::nat)(i * V + g i)) {0..i. Var(i * V + f i)) {0..i. Var(i * V + g i)) {0..i. i * V + f i) ` {0..i. i * V + g i) ` {0..i. i * V + f i) ` {0..i. i * V + g i) ` {0..i. f i = g i" + proof - + fix i + have " i < V \ i \ V" by auto + moreover { + assume iV:"i < V" + then have fiV:"f i < V" + using iV assms(1) permutes_less(1) by blast + have "(i * V + f i) \ ((\i. i * V + g i) ` {0.. V" + have "f i = g i" using assms(1-2) + by (metis atLeastLessThan_iff calculation(2) permutes_others) + } + ultimately show "f i = g i" by auto + qed + thus ?thesis by auto +qed + +lemma perfect_matching_det: + assumes "set E \ {0.. {0.. 0" +proof - + have det: "det (adj_mat V E) = + (\p | p permutes {0..i. + monomial 1 (i * V + p i)) {0..i < V. (i,p i) \ set E then + of_int (sign p) + else 0))" + unfolding det_adj_mat + by auto + from is_matching_permutes[OF assms(1-3)] + obtain p where p: "p permutes {0..i. i < V \ (i, p i) \ set E" by auto + then have iV: "i < V \ + adj_mat V E $$ (i, p i) \ 0" for i + unfolding adj_mat_def + by (subst index_mat) (auto simp add: Var_not_0) + have *: "of_int (sign p) * (\i = 0.. 0" + by (rule ccontr) (use iV in auto) + + have "det (adj_mat V E) \ 0" + unfolding det + apply (subst sum_monom_0_iff) + subgoal + by (auto intro!: finite_permutations) + subgoal + by (auto intro!: sum_monomial_eq) + subgoal + using p by (auto intro!: sum_monomial_eq) + done + thus ?thesis by auto +qed + +lemma det_perfect_matching: + assumes "set E \ {0.. {0.. 0" + obtains match where + "is_matching E match" + "length match = V" +proof - + have det: "det (adj_mat V E) = + (\p | p permutes {0..i = 0.. 0" using assms(2) by auto + then obtain p where p: "p permutes {0..i = 0.. 0" + by (metis (no_types, lifting) mem_Collect_eq sum.not_neutral_contains_not_neutral) + have "\i. i < V \ adj_mat V E $$ (i, p i) \ 0" + using p(2) + by simp + then have iV: "\i. i < V \ (i, p i) \ set E" + unfolding adj_mat_def + by (smt (verit, del_insts) index_mat(1) p(1) permutes_less(1) prod.simps(2)) + + define match where "match = map (\i. (i,p i)) [0.. set E" + using iV unfolding match_def + by auto + show ?thesis using that 1 2 3 + unfolding is_matching_def by auto +qed + +lemma has_perfect_matching_iff: + assumes "set E \ {0.. {0.. det (adj_mat V E) \ 0" + by (metis assms det_perfect_matching has_perfect_matching_def perfect_matching_det) + +lemma sum_when_1: + assumes "finite S" "x \ S" + shows "(\xa\S. 1 when xa = x) = 1" + by (simp add: assms(1) assms(2) when_def) + +lemma total_degree_monom: + assumes "finite S" + shows "total_degree (MPoly_Type.monom (sum (\i. monomial (Suc 0) i) S) c) = + (if c = 0 then 0 else card S)" +proof - + have "(\x\keys (sum (monomial (Suc 0)) S). \xa\S. Suc 0 when xa = x) = card S" + using assms by (subst keys_sum) (auto simp add: when_def) + thus ?thesis + unfolding MPoly_Type.monom_def by (simp add: total_degree.abs_eq lookup_sum single.rep_eq) +qed + + +lemma total_degree_geI: + assumes "m \ keys (mapping_of p)" "(\v\keys m. lookup m v) \ n" + shows "total_degree p \ n" +proof - + have "n \ Max (insert 0 ((\x. sum (lookup x) (keys x)) ` keys (mapping_of p)))" + using assms by (subst Max_ge_iff) auto + thus ?thesis + by (simp add: total_degree_def) +qed + +lemma total_degree_0_iff: "total_degree p = 0 \ vars p = {}" +proof + assume "total_degree p = 0" + show "vars p = {}" + proof safe + fix x assume "x \ vars p" + then obtain m where m: "m \ keys (mapping_of p)" "lookup m x > 0" + unfolding vars_def by blast + from m have "x \ keys m" + by (simp add: in_keys_iff) + note m(2) + also have "lookup m x \ (\v\keys m. lookup m v)" + by (rule member_le_sum) (use \x \ keys m\ in auto) + also have "\ \ total_degree p" + by (intro total_degree_geI) (use m(1) in auto) + finally show "x \ {}" + using \total_degree p = 0\ by simp + qed +next + assume "vars p = {}" + hence "keys (mapping_of p) \ {0}" + by (simp add: subset_eq vars_def) + also have "(\m. sum (lookup m) (keys m)) ` {0} = {0}" + by auto + finally have *: "insert 0 ((\m. sum (lookup m) (keys m)) ` keys (mapping_of p)) = {0}" + by fast + show "total_degree p = 0" + unfolding total_degree_def map_fun_def id_def o_def * by simp +qed + +lemma total_degree_0E: "total_degree p = 0 \ (\c. p = Const c \ P) \ P" + unfolding total_degree_0_iff using vars_empty_iff[of p] by blast + +lemma total_degree_ex: + assumes "p \ 0" + shows "\m. m \ keys (mapping_of p) \ (\v\keys m. lookup m v) = total_degree p" +proof (cases "total_degree p = 0") + case True + thus ?thesis + using assms by (auto elim!: total_degree_0E simp: Const.rep_eq keys_Const\<^sub>0) +next + case False + have "total_degree p \ insert 0 ((\x. sum (lookup x) (keys x)) ` keys (mapping_of p))" + unfolding total_degree_def map_fun_def o_def id_def by (rule Max_in) auto + with False show ?thesis + by auto +qed + +lemma coeff_times_const_left [simp]: "MPoly_Type.coeff (Const c * p) m = c * MPoly_Type.coeff p m" + by (metis Symmetric_Polynomials.coeff_smult smult_conv_mult_Const) + +lemma total_degree_times_const_left: "total_degree (Const c * p) \ total_degree p" +proof (cases "Const c * p = 0") + case False + then obtain m where m: + "m \ keys (mapping_of (Const c * p))" "sum (lookup m) (keys m) = total_degree (Const c * p)" + using total_degree_ex by blast + have "MPoly_Type.coeff (Const c * p) m \ 0" + using m(1) coeff_keys by blast + hence "MPoly_Type.coeff p m \ 0" + by auto + hence "m \ keys (mapping_of p)" + using coeff_keys by blast + with m(2) show ?thesis + by (intro total_degree_geI[of m]) auto +qed auto + +lemma total_degree_of_Const [simp]: "total_degree (Const x) = 0" + by (simp add: total_degree_0_iff) + +lemma total_degree_of_int [simp]: "total_degree (of_int x) = 0" + by (metis monom_of_int mpoly_monom_0_eq_Const total_degree_of_Const) + +lemma total_degree_det_adj_mat: "total_degree (det (adj_mat V E)) \ V" +proof - + have fp:"finite {p. p permutes {0..p | p permutes {0..i. + monomial (Suc 0) (i * V + p i)) {0..i < V. (i,p i) \ set E then + of_int (sign p) + else 0))" (is "_ = (\p | p permutes {0.. V" if p: "p permutes {0..i. i * V + p i) {0..i. i * V + p i)`{0..i set E then sign p else 0))" + by (subst sum.reindex[OF inj]) auto + also have "\ \ V" + by (subst total_degree_monom) (simp_all add: card_image[OF inj]) + finally show ?thesis . + qed + + have "total_degree (det(adj_mat V E)) \ + Max ((total_degree \ ?f) `{p. p permutes{0.. V" + apply (intro Max.boundedI) + subgoal + using fp by blast + subgoal + unfolding permutes_def by force + subgoal + using * by force + done + ultimately show ?thesis + by auto +qed + +lemma arith: + assumes "i < V" + assumes "j < (V::nat)" + shows "i * V + j < V^2" + by (smt (verit, ccfv_SIG) Euclidean_Division.div_eq_0_iff add.right_neutral assms(1) + assms(2) div_less_iff_less_mult div_mult_self3 le_add1 le_add_same_cancel1 + order_trans_rules(21) power2_eq_square) + +lemma vars_det_adj_mat: + shows"vars (det (adj_mat V E)) \ {0..p | p permutes {0..i = 0..p. p permutes {0.. + vars (of_int (sign p) * + (\i = 0.. {0.. + vars (adj_mat V E $$ (i, p i)) \ {0..i = 0.. + vars (\i = 0.. (\i\{0.. {0..i = 0.. {0.. + (\p \ {p. p permutes {0..i = 0.. int) \ + nat \ + (nat \ nat) list \ + int mat" + where "int_adj_mat f V E = + mat V V (\(i,j). + if (i,j) \ set E then f (i* V + j) else 0)" + +lemma map_mat_prod_def: + shows"map_mat f A \ + Matrix.mat (dim_row A) (dim_col A) + (\(i,j). f (A $$ (i,j)))" + by (smt (verit, best) cong_mat map_mat_def split_conv) + +lemma int_adj_mat: + shows"int_adj_mat f V E = + map_mat (insertion f) (adj_mat V E)" + unfolding adj_mat_def int_adj_mat_def + map_mat_prod_def + by auto + +lemma det_int_adj_mat: + shows"det(int_adj_mat f V E) = + insertion f (det (adj_mat V E))" + unfolding int_adj_mat + by (subst comm_ring_hom.hom_det) (auto simp add:comm_ring_hom_insertion) + +definition test_perfect_matching :: "int \ nat \ (nat \ nat) list \ bool pmf" + where "test_perfect_matching n V E = + do { + f \ Pi_pmf ({0..i. pmf_of_set {0::int.. 0) + }" + +theorem test_perfect_matching_false_positive: + assumes "set E \ {0.. {0..has_perfect_matching V E" + shows "pmf (test_perfect_matching n V E) True = 0" +proof - + have "det (adj_mat V E) = 0" + using assms(1) assms(2) has_perfect_matching_iff by blast + thus ?thesis + unfolding test_perfect_matching_def pmf_eq_0_set_pmf det_int_adj_mat + by auto +qed + +lemma test_perfect_matching_true_negative: + assumes "set E \ {0.. {0..has_perfect_matching V E" + shows "pmf (test_perfect_matching n V E) False = 1" + by (metis assms(1) assms(2) pmf_True_conv_False right_minus_eq test_perfect_matching_false_positive) + +theorem test_perfect_matching_false_negative: + assumes "n > 0" and "V > 0" + assumes "set E \ {0.. {0.. 1 / n" +proof - + have d: "det (adj_mat V E) \ 0" + using assms(3-4) has_perfect_matching_iff by blast + have "pmf (test_perfect_matching n V E) False = + prob_space.prob (test_perfect_matching n V E) {False}" + by (simp add: pmf.rep_eq) + moreover have "... = + prob_space.prob + (map_pmf (\f. det (int_adj_mat f V E) \ 0) + (Pi_pmf.Pi_pmf {0..2} 0 (\i. pmf_of_set {0..2} 0 (\i. pmf_of_set {0.. real V / card{0.. 1/n" + using assms(1) by force + ultimately show ?thesis by auto +qed + +end diff --git a/thys/Schwartz_Zippel/Schwartz_Zippel.thy b/thys/Schwartz_Zippel/Schwartz_Zippel.thy new file mode 100644 --- /dev/null +++ b/thys/Schwartz_Zippel/Schwartz_Zippel.thy @@ -0,0 +1,500 @@ +section \The Schwartz-Zippel Lemma\ +theory Schwartz_Zippel imports + Factor_Algebraic_Polynomial.Poly_Connection + Polynomials.MPoly_Type + Skip_Lists.Pi_pmf +begin + +text \This theory formalizes the Schwartz-Zippel lemma + for multivariate polynomials (@{type mpoly}). \ + +lemma schwartz_zippel_uni: + fixes P :: "('a::idom) Polynomial.poly" + fixes S :: "'a set" + assumes "finite S" "S \ {}" + assumes "Polynomial.degree P \ d" + assumes "P \ 0" + shows "measure_pmf.prob (pmf_of_set S) {r. poly P r = 0} \ real d / card S" +proof - + have 1: " ({r. poly P r = 0} \ S) = {r. poly P r = 0 \ r \ S}" + by auto + have 2: "prob_space.prob (pmf_of_set S) {r. poly P r = 0} = + prob_space.prob (pmf_of_set S) {r. poly P r = 0 \ r \ S}" + by (metis (full_types) "1" assms(1) assms(2) measure_Int_set_pmf set_pmf_of_set) + have card: "card {r. poly P r = 0 \ r \ S} \ d" + using poly_roots_degree assms(3) assms(4) by (smt (verit) Collect_mono_iff card_mono le_trans poly_roots_finite) + have inter: "S \ {r. poly P r = 0 \ r \ S} = + {r. poly P r = 0 \ r \ S} " + by auto + + have prob:"prob_space.prob (pmf_of_set S) {r. poly P r = 0 \ r \ S} \ real d / card S" + by (simp add: assms(1) assms(2) assms(4) card inter measure_pmf_of_set divide_right_mono) + + thus "prob_space.prob (pmf_of_set S) {r. poly P r = 0 } \ real d / card S " + by (simp add: 2) +qed + +(* Copied from degree_mpoly_to_mpoly_poly *) +(* TODO: cleanup possible duplication? *) +lemma degree_mpoly_to_poly [simp]: + assumes "vars p = {x}" + shows "Polynomial.degree (mpoly_to_poly x p) = MPoly_Type.degree p x" +proof (rule antisym) + show "Polynomial.degree (mpoly_to_poly x p) \ MPoly_Type.degree p x" + proof (intro Polynomial.degree_le allI impI) + fix i assume i: "i > MPoly_Type.degree p x" + have "poly.coeff (mpoly_to_poly x p) i = + (\m. 0 when lookup m x = i)" + unfolding coeff_mpoly_to_mpoly_poly using i + by (metis (no_types, lifting) Sum_any.cong Sum_any.neutral coeff_mpoly_to_poly degree_geI leD lookup_single_eq when_neq_zero) + also have "\ = 0" + by simp + finally show "poly.coeff (mpoly_to_poly x p) i = 0" . + qed +next + show "Polynomial.degree (mpoly_to_poly x p) \ MPoly_Type.degree p x" + proof (cases "p = 0") + case False + then obtain m where m: "MPoly_Type.coeff p m \ 0" "lookup m x = MPoly_Type.degree p x" + using monom_of_degree_exists by blast + show "Polynomial.degree (mpoly_to_poly x p) \ MPoly_Type.degree p x" + proof (rule Polynomial.le_degree) + have "0 \ MPoly_Type.coeff p m" + using m by auto + have "poly.coeff (mpoly_to_poly x p) (MPoly_Type.degree p x) = + MPoly_Type.coeff p (monomial (MPoly_Type.degree p x) x)" + unfolding coeff_mpoly_to_poly by auto + also have "monomial (MPoly_Type.degree p x) x = m" + unfolding m(2)[symmetric] using assms coeff_notin_vars m(1) + by (intro keys_subset_singleton_imp_monomial) blast + finally show "poly.coeff (mpoly_to_poly x p) (MPoly_Type.degree p x) \ 0" + using m by auto + qed + qed auto +qed + +(* TODO Move *) +lemma total_degree_add: "total_degree (x + y) \ max (total_degree x) (total_degree y)" +proof - + define h :: "(nat \\<^sub>0 nat) \ nat" where "h = (\m. sum (lookup m) (keys m))" + have "insert 0 (h ` keys (mapping_of (x + y))) \ + insert 0 (h ` (keys (mapping_of x) \ keys (mapping_of y)))" + unfolding plus_mpoly.rep_eq + by (intro Set.insert_mono image_mono Poly_Mapping.keys_add) + also have "\ = insert 0 (h ` keys (mapping_of x)) \ + insert 0 (h ` keys (mapping_of y))" + by (simp add: image_Un) + finally have "Max (insert 0 (h ` keys (mapping_of (x + y)))) \ Max \" + by (intro Max_mono) simp_all + also have "?this \ ?thesis" + unfolding total_degree_def map_fun_def o_def id_def h_def [symmetric] + by (subst Max_Un [symmetric]; simp) + finally show ?thesis . +qed + +(* TODO Move *) +lemma total_degree_sum: + assumes "finite S" + shows"total_degree (sum f S) \ + Max ((total_degree \ f) ` S)" + using assms +proof (induction S) + case empty + then show ?case + by auto +next + case (insert x F) + show ?case + proof (cases "F = {}") + case False + have "total_degree (f x + sum f F) \ + max (total_degree (f x)) (total_degree (sum f F))" + using total_degree_add by blast + moreover have "... \ + max (total_degree (f x)) (Max ((total_degree \ f) ` F))" + using local.insert(3) by linarith + also have "\ = (Max ((total_degree \ f) ` insert x F))" + using insert False by simp + finally show ?thesis + using insert.hyps by simp + qed simp_all +qed + +(* TODO Move *) +lemma coeff_mpoly_to_mpoly_poly_restrict: + shows "coeff (mpoly_to_mpoly_poly x P) i = + sum (\m. + MPoly_Type.monom (remove_key x m) + (MPoly_Type.coeff P m) when lookup m x = i) + (Poly_Mapping.keys (mapping_of P))" + unfolding coeff_mpoly_to_mpoly_poly + by (auto intro!: Sum_any.expand_superset simp: coeff_keys) + +lemma Max_le_Max: + assumes "A \ {}" + assumes "finite A" "finite B" + assumes "\a. a \ A \ \b. b \ B \ a \ b" + shows "Max A \ Max B" +proof - + from assms have "B \ {}" + by blast + thus ?thesis + using assms by (intro Max.boundedI) (auto simp: Max_ge_iff) +qed + +lemma sum_lookup_remove_key: + "sum (lookup (remove_key x y)) (keys (remove_key x y)) + lookup y x = + sum (lookup y) (keys y)" +proof - + have "sum (lookup y) (keys y) = + sum (lookup y) (keys (remove_key x y + monomial (lookup y x) x))" + by (subst (2) remove_key_sum [of x, symmetric]) auto + also have "keys (remove_key x y + monomial (lookup y x) x) = + keys (remove_key x y) \ keys (monomial (lookup y x) x)" + by (subst keys_add) (auto simp flip: remove_key_keys) + also have "sum (lookup y) \ = sum (lookup y) (keys (remove_key x y)) + + sum (lookup y) (keys (monomial (lookup y x) x))" + by (subst sum.union_disjoint) (auto simp flip: remove_key_keys) + also have "sum (lookup y) (keys (remove_key x y)) = + sum (lookup (remove_key x y)) (keys (remove_key x y))" + by (intro sum.cong) (auto simp: remove_key_lookup when_def simp flip: remove_key_keys) + also have "sum (lookup y) (keys (monomial (lookup y x) x)) = + sum (lookup y) {x}" + by (intro sum.mono_neutral_cong_left) auto + also have "\ = lookup y x" + by simp + finally show ?thesis .. +qed + +lemma total_degree_nonzero: + assumes "P \ 0" + shows "total_degree P = + Max ((\x. sum (lookup x) (keys x)) ` keys (mapping_of P))" + unfolding total_degree_def by (auto simp: assms) + +lemma poly_mapping_eq_iff: "(m = m') \ (\i. lookup m i = lookup m' i)" + by (auto intro: poly_mapping_eqI) + +(* TODO: move *) +lemma total_degree_coeff_mpoly_to_mpoly_poly: + assumes "coeff (mpoly_to_mpoly_poly x P) i \ 0" + shows "total_degree (coeff (mpoly_to_mpoly_poly x P) i) + i \ total_degree P" +proof - + have P: "P \ 0" + using assms by force + + have nonempty: "keys + (mapping_of(poly.coeff (mpoly_to_mpoly_poly x P) i)) \ {}" + using assms by auto + + have *: " + {y. \xa\keys (mapping_of P) \ {xa. lookup xa x = i} \ {x. MPoly_Type.coeff P x \ 0}. y = sum (lookup xa) (keys xa)} \ + (insert 0 + ((\y. sum (lookup y) (keys y)) ` keys (mapping_of P)))" + by auto + + have "total_degree (coeff (mpoly_to_mpoly_poly x P) i) + i = + (MAX x\keys (mapping_of (poly.coeff (mpoly_to_mpoly_poly x P) i)). + sum (lookup x) (keys x)) + i" + by (subst total_degree_nonzero) (use assms in auto) + moreover have "... = + (MAX x\keys (mapping_of (poly.coeff (mpoly_to_mpoly_poly x P) i)). + sum (lookup x) (keys x) + i)" + by (subst Max_add_commute[symmetric]) (use assms in auto) + moreover have "... = + (MAX x\\xa\keys (mapping_of P) \ + {xa. lookup xa x = i} \ + {x. MPoly_Type.coeff P x \ 0}. + {remove_key x xa}. + sum (lookup x) (keys x) + i)" + unfolding coeff_mpoly_to_mpoly_poly_restrict + unfolding MPoly_Type.degree_def mapping_of_sum[symmetric] + apply (subst keys_sum) + subgoal by simp + subgoal for i j + apply (simp add: zero_mpoly.rep_eq poly_mapping_eq_iff remove_key_lookup when_def) + apply metis + done + subgoal + by (auto simp add: if_distrib zero_mpoly.rep_eq when_def) + done + moreover have "... = + Max {y. \xa\keys (mapping_of P) \ {xa. lookup xa x = i} \ + {x. MPoly_Type.coeff P x \ 0}. + y = sum (lookup (remove_key x xa)) (keys (remove_key x xa)) + lookup xa x}" + by (intro arg_cong[where f = Max]) auto + moreover have "... = + Max {y. \xa\keys (mapping_of P) \ {xa. lookup xa x = i} \ + {x. MPoly_Type.coeff P x \ 0}. + y = sum (lookup xa) (keys xa)}" + by (subst sum_lookup_remove_key) auto + + moreover have "... \ + Max (insert 0 + ((\y. sum (lookup y) (keys y)) ` keys (mapping_of P)))" + apply (intro Max_mono[OF *]) + subgoal + using nonempty unfolding coeff_mpoly_to_mpoly_poly_restrict + by (force elim!: sum.not_neutral_contains_not_neutral) + subgoal + by simp + done + moreover have "... = total_degree P" + unfolding total_degree_def by auto + ultimately show ?thesis by auto +qed + +(* TODO: move *) +lemma degree_le_total_degree: + shows "MPoly_Type.degree P x \ total_degree P" + unfolding total_degree_def degree.rep_eq map_fun_def o_def id_def +proof (rule Max.boundedI; safe?) + fix k + assume k: "k \ keys (mapping_of P)" + have "x \ keys k \ x \ keys k" by auto + moreover { + assume "x \ keys k" + then have "lookup k x \ sum (lookup k) (keys k)" + by (simp add: sum.remove) + then have "lookup k x + \ Max (insert 0 ((\x. sum (lookup x) (keys x)) ` keys (mapping_of P)))" + using k + by (smt (verit, ccfv_SIG) Max_ge dual_order.trans finite_imageI finite_insert finite_keys image_subset_iff subset_insertI) + } + moreover { + assume "x \ keys k" + then have "lookup k x = 0" + by (simp add: in_keys_iff) + then have "lookup k x + \ Max (insert 0 ((\x. sum (lookup x) (keys x)) ` keys (mapping_of P)))" + by linarith + } + ultimately show "lookup k x + \ Max (insert 0 ((\x. sum (lookup x) (keys x)) ` keys (mapping_of P)))" by auto +qed auto + +(* TODO: move *) +lemma insertion_update: + shows "insertion (f(x := r)) P = poly (map_poly (insertion f) (mpoly_to_mpoly_poly x P)) r" + by (subst insertion_mpoly_to_mpoly_poly[symmetric,where \ = "f"]) auto + +(* TODO: move? *) +lemma measure_pmf_prob_dependent_product_bound: + assumes "countable A" "\i. countable (B i)" + assumes "\a. a \ A \ measure_pmf.prob N (B a) \ r" + shows "measure_pmf.prob (pair_pmf M N) (Sigma A B) \ measure_pmf.prob M A * r" +proof - + have "measure_pmf.prob (pair_pmf M N) (Sigma A B) = (\\<^sub>a(a, b)\Sigma A B. pmf M a * pmf N b)" + by (auto intro!: infsetsum_cong simp add: measure_pmf_conv_infsetsum pmf_pair) + moreover have "\ = (\\<^sub>aa\A. \\<^sub>ab\B a. pmf M a * pmf N b)" + proof (subst infsetsum_Sigma) + show "(\(a, b). pmf M a * pmf N b) abs_summable_on Sigma A B" + unfolding case_prod_unfold + by (metis (no_types, lifting) SigmaE abs_summable_on_cong pmf_abs_summable pmf_pair prod.sel) + qed (use assms in auto) + moreover have "... = (\\<^sub>aa\A. pmf M a * (measure_pmf.prob N (B a)))" + by (simp add: infsetsum_cmult_right measure_pmf_conv_infsetsum pmf_abs_summable) + moreover have "... \ (\\<^sub>aa\A. pmf M a * r)" + proof (rule infsetsum_mono) + show "(\a. pmf M a * measure_pmf.prob N (B a)) abs_summable_on A" + proof (rule abs_summable_on_comparison_test') + show "norm (pmf M x * measure_pmf.prob N (B x)) \ pmf M x * 1" for x + unfolding norm_mult by (intro mult_mono) auto + qed auto + qed (auto intro: mult_mono assms) + moreover have"... = r * (\\<^sub>aa\A. pmf M a)" + by (simp add: infsetsum_cmult_left pmf_abs_summable) + moreover have"... = measure_pmf.prob M A * r" + by (simp add: measure_pmf_conv_infsetsum) + ultimately show ?thesis + by linarith +qed + +(* TODO: move? *) +lemma measure_pmf_prob_dependent_product_bound': + assumes "countable (A \ set_pmf M)" "\i. countable (B i \ set_pmf N)" + assumes "\a. a \ A \ set_pmf M \ measure_pmf.prob N (B a \ set_pmf N) \ r" + shows "measure_pmf.prob (pair_pmf M N) (Sigma A B) \ measure_pmf.prob M A * r" +proof - + have *: "Sigma A B \ (set_pmf M \ set_pmf N) = + Sigma (A \ set_pmf M) (\i. B i \ set_pmf N)" + by auto + + have "measure_pmf.prob (pair_pmf M N) (Sigma A B) = + measure_pmf.prob (pair_pmf M N) (Sigma (A \ set_pmf M) (\i. B i \ set_pmf N))" + by (metis * measure_Int_set_pmf set_pair_pmf) + moreover have "... \ + measure_pmf.prob M (A \ set_pmf M) * r" + using measure_pmf_prob_dependent_product_bound[OF assms(1-3)] + by auto + moreover have "... = measure_pmf.prob M A * r" + by (simp add: measure_Int_set_pmf) + ultimately show ?thesis by linarith +qed + +(* TODO: move? *) +lemma finite_set_pmf_Pi_pmf: + assumes "finite A" + assumes "\x. x \ A \ finite (set_pmf (p x))" + shows "finite (set_pmf (Pi_pmf A def p))" +proof - + from set_Pi_pmf_subset'[OF assms(1)] + have 1: "set_pmf (Pi_pmf.Pi_pmf A def p) + \ Pi_pmf.PiE_dflt A def (set_pmf \ p)" + by fastforce + have 2: "finite ..." + by (intro finite_PiE_dflt) (use assms in auto) + show ?thesis using 1 2 + using finite_subset by auto +qed + +theorem schwartz_zippel: + fixes P :: "('a::idom) mpoly" + fixes S :: "'a set" + assumes S: "finite S" "S \ {}" + assumes V: "finite V" + assumes P: "total_degree P \ d" "P \ 0" "vars P \ V" + shows "measure_pmf.prob (Pi_pmf V 0 (\i. pmf_of_set S)) {f. insertion f P = 0} \ real d / card S" + using V P +proof (induction V arbitrary: P d) + case empty + then show ?case + by (metis (mono_tags, lifting) Collect_empty_eq divide_nonneg_nonneg insertion_Const lead_coeff_eq_0_iff measure_empty of_nat_0_le_iff subset_empty vars_empty_iff) +next + case (insert x V) + have "x \ vars P \ x \ vars P" by auto + moreover { + assume x: "x \ vars P" + have *: "prob_space.prob (Pi_pmf V 0 (\i. pmf_of_set S)) {f. insertion f P = 0} \ real d / card S " + by (smt (verit) Collect_cong Diff_insert2 Diff_insert_absorb \x \ vars P\ diff_shunt_var insert.IH insert.prems(3) insert_Diff_single local.insert(2) local.insert(4) local.insert(5) subset_insertI) + + have inser: "Pi_pmf V 0 (\i. pmf_of_set S) = + map_pmf (\f. f(x := 0)) ((Pi_pmf.Pi_pmf (insert x V) 0 (\i. pmf_of_set S)))" + by (metis Diff_insert_absorb Pi_pmf.Pi_pmf_remove finite_insert local.insert(1) local.insert(2) local.insert(6) ) + + have f_aux: "insertion (f(x := 0)) P = 0 \ insertion f P = 0" for f + by (metis x array_rules(4) insertion_irrelevant_vars) + have f: "(\f. f(x := 0))-`{f. insertion f P = 0 \ f x = 0} = {f. insertion f P = 0}" + by (simp add: f_aux) + + have "prob_space.prob ((Pi_pmf.Pi_pmf (insert x V) 0 (\i. pmf_of_set S))) + {f. insertion f P = 0} = prob_space.prob (Pi_pmf V 0 (\i. pmf_of_set S)) {f. insertion f P = 0 }" + using inser f by fastforce + moreover have "... \ real d / card S" + by (simp add: *) + ultimately have ?case + by linarith + } + moreover { + assume x: "x \ vars P" + define px where "px = mpoly_to_mpoly_poly x P" + define q where "q = Polynomial.lead_coeff px" + + have xnV: "x \ V" + by (simp add: local.insert(2)) + + have split: "{f. insertion f P = 0} \ + {f. insertion f q = 0} \ + {f. insertion f q \ 0 \ insertion f P = 0}" (is "_ \ ?E2 \ ?E12") by blast + + obtain l where l: "MPoly_Type.degree P x = l" by simp + + have ld: "l \ d" + using l degree_le_total_degree le_trans local.insert(4) by blast + + (* Prove Pr(?E2) \ (d - l) / |S| *) + + have varq: "vars q \ V" + by (metis x dual_order.trans insert.prems(3) px_def q_def subset_insert_iff vars_coeff_mpoly_to_mpoly_poly) + + have dl: "degree (mpoly_to_mpoly_poly x P) = l" + by (simp add: l) + have qnz: "q \ 0" + unfolding q_def + by (metis degree_0 degree_eq_0_iff dl l leading_coeff_neq_0 px_def x) + + have "total_degree P \ + degree (mpoly_to_mpoly_poly x P) + + total_degree (Polynomial.lead_coeff (mpoly_to_mpoly_poly x P))" + by (metis Groups.add_ac(2) px_def q_def qnz total_degree_coeff_mpoly_to_mpoly_poly) + + then have tdq: "total_degree q \ d-l" + using local.insert(4) px_def q_def dl by force + + from insert.IH[OF tdq qnz varq] + have *: "measure_pmf.prob (Pi_pmf V 0 (\i. pmf_of_set S)) {f. insertion f q = 0} \ real (d-l) /real (card S)" by auto + + have inser: "Pi_pmf V 0 (\i. pmf_of_set S) = + map_pmf (\f. f(x := 0)) ((Pi_pmf.Pi_pmf (insert x V) 0 (\i. pmf_of_set S)))" + by (metis Diff_insert_absorb Pi_pmf.Pi_pmf_remove finite_insert local.insert(1) local.insert(2) local.insert(6) ) + + have aux: "insertion (f(x := 0)) q = 0 \ insertion f q = 0" for f + by (metis \vars q \ V\ array_rules(4) insertion_irrelevant_vars local.insert(2) subsetD) + have "(\f. f(x := 0))-`{f. insertion f q = 0 \ f x = 0} = {f. insertion f q = 0}" + by (simp add: aux) + + then have "prob_space.prob (Pi_pmf.Pi_pmf (insert x V) 0 (\i. pmf_of_set S)) {f. insertion f q = 0} = + prob_space.prob (map_pmf (\f. f(x := 0)) (Pi_pmf.Pi_pmf (insert x V) 0 (\i. pmf_of_set S))) {f. insertion f q = 0 \ f x = 0}" + using local.insert(6) by force + moreover have "... = prob_space.prob (Pi_pmf V 0 (\i. pmf_of_set S)) {f. insertion f q = 0 }" + using inser by fastforce + + ultimately have e2: "measure_pmf.prob (Pi_pmf.Pi_pmf (insert x V) 0 (\i. pmf_of_set S)) ?E2 \ (d - l) / card S" + using * by presburger + + have ib: "prob_space.prob (pmf_of_set S) {r. poly (map_poly (insertion f) px) r = 0} + \ real l / real (card S)" if "insertion f q \ 0" for f + proof (rule schwartz_zippel_uni[OF S]) + show "Polynomial.degree (map_poly (insertion f) px) \ l" + unfolding px_def using that dl degree_map_poly_le by blast + show "map_poly (insertion f) px \ 0" + by (metis Ring_Hom_Poly.degree_map_poly degree_0 degree_eq_0_iff dl l px_def q_def that x) + qed + + have insertion_upd: "insertion (f(x := r)) q = insertion f q" for f r + by (metis array_rules(4) insertion_irrelevant_vars local.insert(2) subsetD varq) + + then have *: "{y. insertion ((fst y)(x := snd y)) q \ 0 \ + insertion ((fst y)(x := snd y)) P = 0} = + Sigma {f. insertion f q \ 0} (\f. {r. insertion (f(x := r)) P = 0})" + by auto + + have "measure_pmf.prob (Pi_pmf.Pi_pmf (insert x V) 0 (\i. pmf_of_set S)) ?E12 = + measure_pmf.prob (pair_pmf (Pi_pmf.Pi_pmf V 0 (\i. pmf_of_set S)) (pmf_of_set S)) + ((\(f, y). f(x := y)) -` {f. insertion f q \ 0 \ insertion f P = 0})" + by (subst Pi_pmf.Pi_pmf_insert) + (use xnV insert in \auto simp add: pair_commute_pmf[of "pmf_of_set S"] + case_prod_unfold * px_def insertion_update[symmetric]\) + also have "(\(f, y). f(x := y)) -` {f. insertion f q \ 0 \ insertion f P = 0} = + Sigma {f. insertion f q \ 0} (\f. {r. poly (map_poly (insertion f) px) r = 0})" + by (auto simp: Sigma_def case_prod_unfold insertion_upd px_def simp flip: insertion_update) + + also have "measure_pmf.prob (pair_pmf (Pi_pmf.Pi_pmf V 0 (\i. pmf_of_set S)) (pmf_of_set S)) ... \ + measure_pmf.prob (Pi_pmf.Pi_pmf V 0 (\i. pmf_of_set S)) {f. insertion f q \ 0} * + (real l / real (card S))" + by (intro measure_pmf_prob_dependent_product_bound') (auto simp: ib measure_Int_set_pmf) + also have "... \ real l / real (card S)" + by (intro mult_left_le_one_le) auto + finally have e12: "measure_pmf.prob (Pi_pmf.Pi_pmf (insert x V) 0 (\i. pmf_of_set S)) ?E12 \ l / card S" . + + have "measure_pmf.prob (Pi_pmf.Pi_pmf (insert x V) 0 (\i. pmf_of_set S)) {f. insertion f P = 0} \ + measure_pmf.prob (Pi_pmf.Pi_pmf (insert x V) 0 (\i. pmf_of_set S)) ({f. insertion f q = 0} \ {f. insertion f q \ 0 \ insertion f P = 0})" + by (intro measure_pmf.finite_measure_mono) (use split in auto) + + moreover have " ... \ + measure_pmf.prob (Pi_pmf.Pi_pmf (insert x V) 0 (\i. pmf_of_set S)) ?E2 + + measure_pmf.prob (Pi_pmf.Pi_pmf (insert x V) 0 (\i. pmf_of_set S)) ?E12" + by (auto intro!: measure_pmf.finite_measure_subadditive) + moreover have "... \ (d-l) / card S + l / card S" + using e2 e12 by auto + + moreover have "... \ real d / card S" + by (simp add: ld diff_divide_distrib of_nat_diff) + + ultimately have ?case + by linarith + } + ultimately show ?case by auto +qed + +end diff --git a/thys/Schwartz_Zippel/document/root.bib b/thys/Schwartz_Zippel/document/root.bib new file mode 100644 --- /dev/null +++ b/thys/Schwartz_Zippel/document/root.bib @@ -0,0 +1,55 @@ +@misc{history, + title = {The Curious History of the {Schwartz-Zippel} Lemma}, + url = {https://rjlipton.wpcomstaging.com/2009/11/30/the-curious-history-of-the-schwartz-zippel-lemma/}, + author = {Richard Lipton}, + year = {2009}, + note = {Accessed on Apr 21, 2023} +} + +@article{DBLP:journals/jacm/Schwartz80, + author = {Jacob T. Schwartz}, + title = {Fast Probabilistic Algorithms for Verification of Polynomial Identities}, + journal = {J. {ACM}}, + volume = {27}, + number = {4}, + pages = {701--717}, + year = {1980}, + skipurl = {https://doi.org/10.1145/322217.322225}, + skipdoi = {10.1145/322217.322225}, + timestamp = {Wed, 14 Nov 2018 10:35:24 +0100}, + biburl = {https://dblp.org/rec/journals/jacm/Schwartz80.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@article{DBLP:journals/ipl/DemilloL78, + author = {Richard A. DeMillo and + Richard J. Lipton}, + title = {A Probabilistic Remark on Algebraic Program Testing}, + journal = {Inf. Process. Lett.}, + volume = {7}, + number = {4}, + pages = {193--195}, + year = {1978}, + skipurl = {https://doi.org/10.1016/0020-0190(78)90067-4}, + skipdoi = {10.1016/0020-0190(78)90067-4}, + timestamp = {Sun, 02 Jun 2019 21:07:03 +0200}, + biburl = {https://dblp.org/rec/journals/ipl/DemilloL78.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{DBLP:conf/eurosam/Zippel79, + author = {Richard Zippel}, + editor = {Edward W. Ng}, + title = {Probabilistic algorithms for sparse polynomials}, + booktitle = {EUROSAM}, + series = {LNCS}, + volume = {72}, + pages = {216--226}, + publisher = {Springer}, + skipyear = {1979}, + skipurl = {https://doi.org/10.1007/3-540-09519-5\_73}, + doi = {10.1007/3-540-09519-5\_73}, + timestamp = {Fri, 17 Jul 2020 16:12:47 +0200}, + biburl = {https://dblp.org/rec/conf/eurosam/Zippel79.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} diff --git a/thys/Schwartz_Zippel/document/root.tex b/thys/Schwartz_Zippel/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/Schwartz_Zippel/document/root.tex @@ -0,0 +1,33 @@ +\documentclass[11pt,a4paper]{article} +\usepackage[T1]{fontenc} +\usepackage{isabelle,isabellesym} +\usepackage{amsmath} +\usepackage{amsthm} +\usepackage{amssymb} +\usepackage{pdfsetup} + +\urlstyle{rm} +\isabellestyle{it} + +\begin{document} + +\title{Formalization of the Schwartz-Zippel Lemma} +\author{Sunpill Kim and Yong Kiam Tan} +\maketitle +\begin{abstract} +This short entry formalizes a version of the Schwartz-Zippel lemma for probabilistic (multivariate) polynomial identity testing. +The entry includes a textbook example using the lemma to test for perfect matchings in a bipartite graph. +The lemma is attributed to several independent authors, including Schwartz~\cite{DBLP:journals/jacm/Schwartz80}, Zippel~\cite{DBLP:conf/eurosam/Zippel79}, and DeMillo and Lipton~\cite{DBLP:journals/ipl/DemilloL78}; a historical perspective is given by Lipton~\cite{history}. +\end{abstract} + +\tableofcontents + +\input{session} +\bibliographystyle{abbrv} +\bibliography{root} +\end{document} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: