proposition: Theorem find_all_aux_sat: forall n s cs, length cs <= length n -> length s = size * size -> valid cs s -> ordered cs -> olist _ (lexico _ test) (find_all_aux n s cs) /\ (forall s1, In s1 (find_all_aux n s cs) -> refine s s1 /\ sat cs s1) /\ (forall s1, refine s s1 -> sudoku s1 -> sat cs s1 -> (exists s2, refine s2 s1 /\ In s2 (find_all_aux n s cs))).
proof: Proof. Proof with auto with arith datatypes. intros n; elim n; clear n. intros s cs; case cs; simpl; auto; clear cs. intros _ H H0 HH1; split... apply olist_one. split... intros s1 [H2 | H2]; subst. split... red... intros n2 c2; simpl; intros HH; case HH. case H2. intros s1 H1 H2 H3; exists s... intros p l H; contradict H... intros a n Rec s cs; case cs; clear cs. simpl; intros _ H0; split... apply olist_one... split... simpl; intros s1 [Hs1 | Hs1]; subst. split... split... intros n2 c2; intros HH; case HH. case Hs1. intros s1 Hs1 Hs2 Hs3; exists s... intros (n1, c1) cs; case c1; unfold find_all_aux; lazy beta; fold find_all_aux. intros H H0 HH1; split... apply olist_nil. split... simpl; intros s1 Hl; case Hl. intros s1 _ _ H2; case (H2 n1 nil)... intros x (tmp, _); case tmp. intros l c2 H0 H1 H2 HH1; simpl in H0. case (try_all_sat s n1 (l :: c2) cs (find_all_aux n))... intros n3 c3 Hn3; apply (HH1 n3)... intros s1 cs1 Hs1 Hs2 Hs3 Hs4 Hs5 Hs6. case (Rec s1 cs1)... apply Nat.le_trans with (1 := Hs1)... intros H3 (H4, H5). split... split... intros s2 HH; case (H4 s2)... intros s2 V1 V2 V3; case (H5 s2)... intros s3 (V4, V5); exists s3; split... intros V1 (V2, V3). split... split... intros s1 V4 V5 V6; case (V3 s1)... intros s2 (V7, V8); exists s2... Qed.
imports: List UList Permutation Div OrderedList ListOp Lia