proposition: Lemma sudoku_def g : reflect [/\ size g = hw * hw, forall p, valid_pos p -> get p g \in sref & forall p1 p2 z, valid_pos p1 -> (p2, z) \in anti_literals (p1, get p1 g) -> get p2 g != z] (sudoku g).
proof: Proof. apply: (iffP and4P) => [[/eqP Hs /forallP Hr /forallP Hc /forallP Hre]| [Hs Hv Ha]]; split => //=. - move=> [x y] /andP[/= Hx Hy]. by rewrite -(perm_mem (Hr (Ordinal Hx))) /= get_row // mem_nth // size_row. - move=> [x1 y1] [x2 y2] z /andP[/= x1Lhw y1Lhw]. have h_pos := h_pos x1Lhw; have w_pos := w_pos x1Lhw. rewrite !mem_cat => /or3P[] /mapP[/= z1]; rewrite mem_filter => /andP[y1Dz1 z1I] [-> -> ->]. + have z1Lhw : z1 < hw by rewrite mem_iota in z1I. rewrite !get_row //. apply: contra y1Dz1 => /eqP Hnth; apply/eqP. have /uniqP : uniq (row x1 g). by rewrite (perm_uniq (Hr (Ordinal x1Lhw))) sref_uniq. by move/(_ out); apply; rewrite -?topredE /= ?size_row. + have z1Lhw : z1 < hw by rewrite mem_iota in z1I. rewrite !get_column //. apply: contra y1Dz1 => /eqP Hnth; apply/eqP. have /uniqP : uniq (column y1 g). by rewrite (perm_uniq (Hc (Ordinal y1Lhw))) sref_uniq. by move/(_ out); apply; rewrite -?topredE /= ?size_column. rewrite mem_cross in z1I; have /andP[Hz11 Hz12] := z1I. rewrite !get_rect // ?hw_divhMD ?hw_divwMD //. rewrite !divnMDl // !modnMDl // (divn_small Hz11) addn0. rewrite (divn_small Hz12) addn0. rewrite (modn_small Hz11) (modn_small Hz12). case: z1 y1Dz1 {z1I}Hz11 Hz12 => x3 y3 /= y1Dz1 x3Lh y3Lw. apply: contra y1Dz1 => /eqP Hnth; apply/eqP. suff ->: (x3, y3) = (x1 %% h, y1 %% w) by rewrite /shift /= -!divn_eq. suff He: x3 * w + y3 = x1 %% h * w + y1 %% w. rewrite -[x3]addn0 -(divn_small y3Lw) -divnMDl // He divnMDl // divn_small ?ltn_mod // addn0. by rewrite -(modn_small y3Lw) -(modnMDl x3 y3) He modnMDl modn_mod. have y1wLh := hw_divw y1Lhw. have /uniqP : uniq (rect (x1 %/ h * h + y1 %/ w) g). by rewrite (perm_uniq (Hre (Ordinal (hw_divhMD x1Lhw y1wLh)))) sref_uniq. move/(_ out); apply => //=; rewrite -?topredE /= ?size_rect //. + by rewrite /hw; nia. + by apply :hw_divhMD. + by apply: hw_modwMDmod. by apply: hw_divhMD. - by apply/eqP. - apply/forallP => /= [] [x xLhw] /=. suff Hi : row x g =i sref. apply: uniq_perm sref_uniq _ => //. by rewrite (eq_uniq _ Hi) ?sref_uniq // size_row // size_sref. case (@uniq_min_size _ (row x g) sref) => //. + apply/(uniqP out) => y1 y2. rewrite -?topredE /= size_row // => y1Lhw y2Lhw. rewrite -!get_row //; case: (y1 =P y2) => // /eqP y1Dy2 Hg. have [] := negP (Ha (x, y1) (x, y2) (get (x, y1) g) _ _); last by apply/eqP. by rewrite /valid_pos /= xLhw. rewrite mem_cat; apply/orP; left. apply: map_f. by rewrite mem_filter y1Dy2 mem_iota. + move=> i /(nthP out)[y]; rewrite size_row // => yLhw. rewrite -get_row // => <-. by apply: Hv; rewrite /valid_pos /= xLhw. by rewrite size_sref size_row. - apply/forallP => /= [] [y yLhw] /=. suff Hi : column y g =i sref. apply: uniq_perm sref_uniq _ => //. by rewrite (eq_uniq _ Hi) ?sref_uniq // size_column // size_sref. case (@uniq_min_size _ (column y g) sref) => //. + apply/(uniqP out) => x1 x2. rewrite -?topredE /= size_column // => x1Lhw x2Lhw. rewrite -!get_column //; case: (x1 =P x2) => // /eqP x1Dx2 Hg. have [] := negP (Ha (x1, y) (x2, y) (get (x1, y) g) _ _); last by apply/eqP. by rewrite /valid_pos /= x1Lhw. rewrite !mem_cat; apply/orP; right; apply/orP; left. apply: map_f. by rewrite mem_filter x1Dx2 mem_iota. + move=> i /(nthP out)[x]; rewrite size_column // => xLhw. rewrite -get_column // => <-. by apply: Hv; rewrite /valid_pos /= xLhw. by rewrite size_sref size_column. apply/forallP => /= [] [i iLhw] /=. suff Hi : rect i g =i sref. apply: uniq_perm sref_uniq _ => //. by rewrite (eq_uniq _ Hi) ?sref_uniq // size_rect // size_sref. have h_pos := h_pos iLhw; have w_pos := w_pos iLhw. case (@uniq_min_size _ (rect i g) sref) => //. - apply/(uniqP out) => j1 j2. rewrite -?topredE /= size_rect // => j1Lhw j2Lhw. rewrite -!get_rect_rev //; case: (j1 =P j2) => // /eqP j1Dj2 Hg. set p1 := (_, _) in Hg; set p2 := (_, _) in Hg. have [] := negP (Ha p1 p2 (get p1 g) _ _); last by apply/eqP. apply/andP; split=> /=; first by rewrite hw_divhMD // hw_divw. by apply: hw_modwMDmod. rewrite !mem_cat; apply/orP; right; apply/orP; right. rewrite !divnMDl // [(_ %/ _) %/ _]divn_small; last by rewrite ltn_divLR. rewrite addn0 [(_ %% _) %/ _]divn_small ?ltn_mod // addn0. have -> : p2 = shift (j2 %/ w, j2 %% w) (i %/ h * h) (i %% h * w). by apply/eqP; rewrite xpair_eqE !eqn_add2l // !eqxx. apply: map_f; rewrite mem_filter; apply/andP; split => /=. rewrite xpair_eqE /= !eqn_add2l. apply: contra j1Dj2 => /andP[/eqP Hj1 /eqP Hj2]. by rewrite (divn_eq j1 w) Hj1 Hj2 -divn_eq. by rewrite mem_cross /= ltn_mod w_pos hw_divw. - move=> j /(nthP out)[k]; rewrite size_rect // => kLhw. rewrite -get_rect_rev // => <-. apply: Hv; apply/andP; split => /=; first by rewrite hw_divhMD // hw_divw. by apply: hw_modwMDmod. by rewrite size_sref size_rect. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)