proposition: Theorem try_all_sat: forall s n c cs f, valid ((n, c) :: cs) s -> length s = size * size -> ordered cs -> (forall s cs1, length cs1 <= length cs -> length s = size * size -> valid cs1 s -> ordered cs1 -> (forall s2, refine s s2 -> sat cs1 s2 -> sat cs s2) -> (forall s2, refine s s2 -> sudoku s2 -> sat cs s2 -> sat cs1 s2) -> olist _ (lexico _ test) (f s cs1) /\ (forall s1, In s1 (f s cs1) -> refine s s1 /\ sat cs s1) /\ (forall s1, refine s s1 -> sudoku s1 -> sat cs s1 -> exists s2, In s2 (f s cs1) /\ refine s2 s1) ) -> olist _ (lexico _ test) (try_all s c cs f) /\ (forall s1, In s1 (try_all s c cs f) -> refine s s1 /\ sat ((n, c) :: cs) s1) /\ (forall s1, refine s s1 -> sudoku s1 -> sat ((n, c) :: cs) s1 -> exists s2, In s2 (try_all s c cs f) /\ refine s2 s1).
proof: Proof. Proof with auto with datatypes. intros s n c cs f H0 VV VV1 H; generalize H0; elim c; simpl; clear c H0. intros H0; split... apply olist_nil. split... intros s1 HH; case HH. intros s1 _ _ Hs1. assert (F0: clause_sat nil s1). apply (Hs1 n)... case F0; simpl; intuition. intros (p, z) c1 Rec H0. case Rec... intros n2 c2; simpl; intros [Hn2 | Hn2]. injection Hn2; intros; subst; clear Hn2. assert (F1: valid_clause (L p z :: c2) s). apply (H0 n2)... intros l Hl; apply (F1 l)... apply (H0 n2)... intros Rec1 (Rec2, Rec3). assert (F1: valid_lit (L p z) s). assert (F2: valid_clause (L p z :: c1) s). apply (H0 n)... apply F2... case (H (update p z s) (clauses_update (L p z) (anti_literals (L p z)) cs)). apply length_clauses_update. rewrite length_update... apply clauses_update_valid... apply anti_literals_ordered. intros; apply anti_literals_in... intros n2 c2 Hn2; apply (H0 n2)... apply clauses_update_ordered... apply anti_literals_ordered. intros s2 HH HH0. apply clauses_update_sat with (4 := HH0)... apply anti_literals_ordered. simpl; case HH; intros _ (_, tmp); rewrite <- tmp... apply update_get... apply valid_pos2n... case F1; intuition. case F1; intuition. rewrite update_get... case F1; intuition. apply valid_pos2n... case F1; intuition. intros s2 HH HH0 HH1. apply clauses_update_sat_rev... apply anti_literals_ordered. simpl; case HH; intros _ (_, tmp); rewrite <- tmp... apply update_get... apply valid_pos2n... case F1; intuition. case F1; intuition. rewrite update_get... case F1; intuition. apply valid_pos2n... case F1; intuition. intros l Hl Hl1; case (anti_literals_sat p z s2)... case F1; intuition. simpl; case HH; intros _ (_, tmp); rewrite <- tmp... apply update_get... apply valid_pos2n... case F1; intuition. case F1; intuition. rewrite update_get... case F1; intuition. apply valid_pos2n... case F1; intuition. exists l... intros H1 (H2, H3). split... unfold merges; apply merge_olist... intros; apply lexico_trans... exact test_trans. intros; apply test_anti_sym... exact test_compat_l. intros; apply lexico_anti_sym... intros; apply test_anti_sym... intros; apply lexico_exact with (weight := test)... exact test_exact. split... unfold merges; intros s1 Hs1; case merge_inv with (1 := Hs1); clear Hs1; intros Hs1... case (H2 s1)... intros U1 U2; split... apply refine_trans with (2 := U1)... apply refine_update... case F1; intuition. intros n2 c2; simpl; intros [Hn2 | Hn2]. injection Hn2; intros; subst; clear Hn2. exists (L p z); split; auto with datatypes; simpl. case U1; intros _ (_, tmp); rewrite <- tmp; auto with arith; clear tmp. apply update_get... apply valid_pos2n... case F1; intuition. case F1; intuition. rewrite update_get... case F1; intuition. apply valid_pos2n... case F1; intuition. apply (U2 n2)... case (Rec2 s1); auto; clear Rec2; intros U1 U2. split... intros n2 c2; simpl; intros [Hn2 | Hn2]. injection Hn2; intros; subst; clear Hn2. assert (F2: clause_sat c1 s1). apply (U2 n2)... case F2; intros l (Hl1, Hl2). exists l... apply (U2 n2)... intros s1 Hs1 Hs2 Hs3. assert (F2: clause_sat (L p z :: c1) s1). apply (Hs3 n)... case F2; intros l (Hl1, Hl2); simpl in Hl1; case Hl1; clear Hl1; intros Hl1; subst. case (H3 s1)... split... rewrite length_update... split... case Hs1; intuition. intros p1 Hp1. case (pos_dec p p1); intros HH1. subst p1; rewrite update_get... apply valid_pos2n... rewrite update_diff_get... case Hs1; intuition. case F1; intuition. intros n2 c2 Hn2; apply (Hs3 n2)... intros s2 (Hs4, Hs5). exists s2; split... unfold merges; apply merge_incl_l... case (Rec3 s1)... intros n2 c2; simpl; intros [Hn2 | Hn2]. injection Hn2; intros; subst; clear Hn2. exists l... apply (Hs3 n2)... intros s3 (Hs4, Hs5); exists s3; split... unfold merges; apply merge_incl_r... intros; apply lexico_exact with (weight := test)... exact test_exact. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia