proposition: Lemma mem_find_all g g1 : size g = hw * hw -> (g1 \in find_all g) = refine g g1 && sudoku g1.
proof: Proof. move=> Hs; rewrite /find_all. case: gen_init_state (gen_init_state_correct Hs) => [|/(_ g1)]; last first. by rewrite in_nil ;case: refine => //= /(_ isT); case: sudoku. move=> st. elim: st g Hs {1 3 5}st (leqnn (size st)) => /= [|_ n IH] g Hs. case=> // _ /invariant_nil Hu. rewrite inE; apply/eqP/andP=> [->|[Hr1 Hs1]]. by split => //; apply: refine_refl. by apply/sym_equal/sudoku_refine_id. case=> [_ /invariant_nil Hu|[[n1 p1] v1] st] /=. rewrite inE; apply/eqP/andP=> [->|[Hr1 Hs1]]. by split => //; apply: refine_refl. by apply/sym_equal/sudoku_refine_id. rewrite ltnS => stLn Hin. have Hp1 : valid_pos p1. have [_ [_ Hin1] _ _ _ _] := Hin. by apply: Hin1 => /=; rewrite inE eqxx. suff : (behead v1) = drop 1 v1 -> ( refine g g1 -> sudoku g1 -> get p1 g1 >= 1 -> g1 \in try_all (behead v1) p1 1 g st (find_all_aux n) ) /\ ( g1 \in try_all (behead v1) p1 1 g st (find_all_aux n) -> refine g g1 /\ sudoku g1 ). rewrite drop1 => /(_ (refl_equal _)) [H1 H2]. apply/idP/andP=> // [] [H3 H4]. apply: H1 => //. have /sudoku_def[_ H5 _] := H4. case: get (H5 _ Hp1) => //=. by rewrite mem_iota. elim: behead 1 => /= [k Hdr|kb bs IH1 k Hdr]; split. - move=> /refineP[H1rss1 H2rss1 H3rss1] /sudoku_def[H1su H2su H3su] kLg. have [p3 [H1p3 H2p3 H3p3]] : exists p3, [/\ valid_pos p3, get p3 g \in sref & (p1, get p1 g1) \in anti_literals (p3, get p3 g)]. have [H1 H2 H3 H4 [H5 H6]] := Hin; apply: H6 => //. - by apply: H2su. - by rewrite H3 //= inE eqxx. rewrite in_state_cons; last by case: Hin. by rewrite /in_val -(subnK kLg) addnC -nth_drop -Hdr nth_nil. rewrite in_nil; rewrite (H3rss1 p3) // in H3p3. by have /eqP[] := (H3su _ _ _ H1p3 H3p3). - by rewrite in_nil. - move=> Hrss1 Hsu kLg. case: kb Hdr => Hdr. case: ltngtP kLg => // [kLg | kE] _. rewrite mem_merge_sudoku mem_cat; apply/orP; right. case: (IH1 k.+1) => [|IH11 IH12]. by rewrite -add1n -drop_drop -Hdr /= drop0. by apply: IH11. rewrite mem_merge_sudoku mem_cat; apply/orP; left. rewrite IH //. - rewrite Hsu andbT. apply/refineP; split => //. + by rewrite size_update. + by case/refineP : Hrss1. move=> p2 Hp2. case: (p2 =P p1) => [->|/eqP p2Dp1]. by rewrite update_get. rewrite update_diff_get // => HH. by have /refineP[_ _ <-] := Hrss1. - by rewrite size_update. - by rewrite size_update_anti_literals. have <- := @rm_state_cons n1 p1 v1 st; last by case: Hin. apply: invariant_update => //. rewrite in_state_cons //; last by case: Hin. by rewrite /in_val -[k]addn0 -nth_drop -Hdr. case: (IH1 k.+1) => [|IH11 IH12]. by rewrite -add1n -drop_drop -Hdr /= drop0. apply: IH11 => //. case: ltngtP kLg => // kE. have /refineP[H1rss1 H2rss1 H3rss1] := Hrss1. have /sudoku_def[H1su H2su H3su] := Hsu. have [p3 [H1p3 H2p3 H3p3]] : exists p3, [/\ valid_pos p3, get p3 g \in sref & (p1, get p1 g1) \in anti_literals (p3, get p3 g)]. have [H1 H2 H3 H4 [H5 H6]] := Hin; apply: H6 => //. - by apply: H2su. - by rewrite H3 //= inE eqxx. rewrite in_state_cons; last by case: Hin. by rewrite /in_val -kE -[k]addn0 -nth_drop -Hdr. rewrite (H3rss1 p3) // in H3p3. by have /eqP[] := (H3su _ _ _ H1p3 H3p3). case: kb Hdr => Hdr. rewrite mem_merge_sudoku mem_cat => /orP[]. rewrite IH //. - move=>/andP[Hr Hu]; split=> //. apply: refine_trans Hr. apply: refine_update => //. have [_ _ Hin1 _ _] := Hin. by rewrite Hin1 //= in_cons eqxx. - by rewrite size_update. - by rewrite size_update_anti_literals. have <- := @rm_state_cons n1 p1 v1 st; last by case: Hin. apply: invariant_update => //. rewrite in_state_cons //; last by case: Hin. by rewrite /in_val -[k]addn0 -nth_drop -Hdr. case: (IH1 k.+1) => [|IH11 IH12]. by rewrite -add1n -drop_drop -Hdr /= drop0. by apply: IH12. case: (IH1 k.+1) => [|IH11 IH12]. by rewrite -add1n -drop_drop -Hdr /= drop0. by apply: IH12. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)