proposition: Lemma gen_init_state_correct g : size g = hw * hw -> if gen_init_state g is some st1 then invariant st1 g else forall g1, refine g g1 -> ~ sudoku g1.
proof: Proof. revert g. rewrite /gen_init_state. suff H g g1 st p : (g1 != [::] -> valid_pos p) -> size g = hw * hw -> invariant st (grestrict p g) -> g1 = drop (pos2n p) g -> if gen_init_state_aux g1 p st is some st1 then invariant st1 g else forall g1, refine g g1 -> ~ sudoku g1. case: (hw =P 0) => [hwE|hwD0]. rewrite hwE; case=> //=; have := invariant_init. by rewrite /ginit hwE. move=> g Hs; apply: H => //. - by case: (g) Hs => //= _ s2; rewrite /valid_pos; case: hw. - rewrite grestrict00. by rewrite Hs; apply: invariant_init. by rewrite drop0. elim: g1 g st p => /= [|v g1 IH]/= g st p Hp Hs Hin Hd. rewrite grestrict_all // in Hin. rewrite -subn_eq0; apply/eqP. by rewrite -size_drop -Hd. have Hgv : get p g = v. by rewrite /get -[pos2n p]addn0 -nth_drop -Hd. have {}Hp := Hp isT. have Hv : g1 != [::] -> valid_pos (next p). case: g1 {IH}Hd => //= v1 s1 Hd _. apply: valid_pos_next => //. rewrite next_pos -Hs. case: leqP => // /drop_oversize. by rewrite -add1n -drop_drop -Hd. have Hdr : g1 = drop (pos2n (next p)) g. by rewrite next_pos -add1n -drop_drop -Hd /= drop0. have [vis|vnis] := boolP (v \in sref); last first. apply: IH => //. apply: invariant_equiv Hin; apply/refineP; split. - by rewrite grestrict_size. - by rewrite grestrict_size. - move=> p1 Hp1 Hg1. case: (leqP (pos2n p) (pos2n p1)) => Lp. rewrite grestrict_get_default // in Hg1. by case/negP: out_not_in_refl. by rewrite !grestrict_get // next_pos (leq_trans Lp). - by rewrite grestrict_size. - by rewrite grestrict_size. move=> p1 Hp1 Hg1. case: (leqP (pos2n p1) (pos2n p)) => Lp; last first. rewrite grestrict_get_default // in Hg1. by case/negP: out_not_in_refl. by rewrite next_pos. case: ltngtP Lp => // Lp1 . by rewrite !grestrict_get // next_pos (leq_trans Lp1). rewrite grestrict_get // in Hg1; last first. by rewrite next_pos Lp1. case/negP: vnis. by rewrite /get Lp1 -[pos2n _]addn0 -nth_drop -Hd in Hg1. have [His|Hnis] := boolP (in_state p v st); last first. move=> g2 Hrss2 /sudoku_def[H1su H2su H3su]. have [_ _ _ _ [_ Hin1]] := Hin. case: (Hin1 p v) => // [|p2 [H1p2 H2p2 H3p2]]. by rewrite grestrict_get_default // out_not_in_refl. have Hrps : refine (grestrict p g) g by apply: refine_grestrict. case: (get p g2 =P v); [apply/eqP|case=> //]. apply: H3su (H1p2) _. have /refineP[_ _ <-//] := Hrss2. by have /refineP[_ _ /(_ p2)<-//] := Hrps. by have /refineP[_ _ /(_ p2)<-//] := Hrps. have /refineP[_ _ <-//] := Hrss2. by rewrite Hgv. apply: IH => //. rewrite grestrict_update. have->: get p g = v. by rewrite /get -[pos2n p]addn0 -nth_drop -Hd. apply: invariant_update => //. case: leqP => // H. by rewrite drop_oversize // -ltnS -next_pos // in Hd. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)