proposition: Theorem try_one_sat: forall s n c cs f, invariant ((n, c) :: cs) s -> (forall s cs1, invariant cs1 s -> length cs1 <= length cs -> match f s cs1 with None => forall s1, refine s s1 -> ~ sudoku s1 | Some s1 => sudoku s1 /\ refine s s1 end) -> match try_one s c cs f with None => forall s1, refine s s1 -> ~ sudoku s1 | Some s1 => sudoku s1 /\ refine s s1 end.
proof: Proof. intros s n c cs f H H1; generalize H; elim c; simpl; auto; clear c H. intros H s1 Hs1 H2. absurd (clause_sat nil s1). intros H3; case H3; simpl; intros k (tmp, _); auto. case H; simpl. intros _ (_, (_, tmp)); case (tmp s1); auto; clear tmp. intros tmp _; apply (tmp H2 n nil); auto with datatypes. intros (p1, z1) c1 Rec H3. assert (H: valid_lit (L p1 z1) s); auto. case H3; intros _ (V2, _). apply (V2 n (L p1 z1 :: c1)); auto with datatypes. match goal with |- context [f ?X ?Y] => assert (U1: invariant Y X); [idtac | generalize (H1 X Y U1); case (f X Y) ] end. apply invariant_clauses_update with (1 := H3). intros s1 tmp; case tmp; auto; clear tmp. apply length_clauses_update; auto. intros Hs Hs1; split; auto. apply refine_trans with (2 := Hs1); auto. apply refine_update; auto. case H3. simpl in H; case H; auto. case H3; intuition. intros H0. assert (Heq0: invariant ((n, c1) :: cs) s). apply invariant_refine with (1 := H3); auto. intros s1 Hs1 Hs2; case H0 with s1; auto. apply length_clauses_update; auto. generalize (Rec Heq0); clear Rec. case (try_one s c1 cs f); auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia