proposition: Lemma find_just_one_aux_correct st g st1 : match find_just_one_aux st g st1 with | jNone => find_all_aux st g st1 = [::] | jOne g1 => find_all_aux st g st1 = [:: g1] | jMore g1 g2 => [/\ g1 \in find_all_aux st g st1, g2 \in find_all_aux st g st1 & g1 != g2] end.
proof: Proof. elim: st g st1 => [|[[n p] v] st IH] g [|[[n1 p1] v1] st1] //=. elim: behead p1 1 g st1 => //= [] [] bs IH1 p1 k g st1. case: find_just_one_aux (IH (update p1 k g) (update_anti_literals p1 k st1)). - move=> -> /=. case: try_just_one (IH1 p1 k.+1 g st1) => [->//|g1 ->//|]. by move=> g1 g2; rewrite !mem_merge_sudoku => [] [-> -> ->]. - move=> g1 ->. case: try_just_one (IH1 p1 k.+1 g st1) => [->//|g2 ->|]. case: eqP => [->/=|/eqP g1Dg2]; first by rewrite grid_leqn_refl. by rewrite !mem_merge_sudoku /= !inE !eqxx orbT (negPf g1Dg2). - move=> g2 g3; rewrite !mem_merge_sudoku !inE => [] [-> -> ->]. by rewrite !orbT. by move=> g2 g3; rewrite !mem_merge_sudoku !mem_cat => [] [-> -> ->]. case: find_just_one_aux (IH (update p1 k g) (update_anti_literals p1 k st1)). move=> H. by case: try_just_one (IH1 p1 k.+1 g st1) => [->|g1 ->|]. move=> s1 H. by case: try_just_one (IH1 p1 k.+1 g st1) => [->//|g2 ->|]. move=> g1 g2 [H1s H2s H3s]. by case: try_just_one (IH1 p1 k.+1 g st1) => [->//|s3 ->|]. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)