proposition: Theorem find_one_aux_sat: forall n s cs, length cs <= length n -> invariant cs s -> match find_one_aux n s cs with None => forall s1, refine s s1 -> ~ sudoku s1 | Some s1 => sudoku s1 /\ refine s s1 end.
proof: Proof. intros n; elim n; simpl; clear n. intros s cs; case cs; simpl; auto; clear cs. intros _ H; case H; clear H. intros _ (_, (H0, H1)); split. case (H1 s). split; auto. intros _ tmp; apply tmp; clear tmp. intros n2 c2 Hn2; case Hn2. split; auto. intros p l H; contradict H; auto with arith. intros _ c H s cs; case cs; clear cs. intros _ (_, (H0, (H1, H2))); split. case (H2 s). split; auto. intros _ tmp; apply tmp; clear tmp. intros n2 c2 Hn2; case Hn2. split; auto. intros (n1, c1); case c1; simpl. intros cs1 H0 (H1, (H2, (H3, H4))) s1 Hs1 Hs2. absurd (clause_sat nil s1). intros HH; case HH; simpl; intuition. case (H4 s1); auto. intros tmp _; apply (tmp Hs2 n1); auto with datatypes. intros (p, z) c2 cs1 H0 H1. match goal with |- context [find_one_aux ?X ?Y ?Z] => assert (tmp1: length Z <= length c); [ idtac | assert (tmp2: invariant Z Y); [ idtac | generalize (H Y Z tmp1 tmp2); case (find_one_aux X Y Z) ] ] end; try clear tmp1 tmp2. apply Nat.le_trans with (length cs1); auto with arith. apply length_clauses_update; auto. apply invariant_clauses_update with (1 := H1); auto. intros s1 (Hs1, Hs2); split; auto. apply refine_trans with (2 := Hs2). apply refine_update; auto. case H1; intros _ (V2, _). assert (Heq: valid_clause (L p z :: c2) s). apply (V2 n1); auto with datatypes. case (Heq (L p z)); auto with datatypes. case H1; intuition. intros H2. match goal with |- context [try_one ?X ?Y ?Z ?T] => generalize (try_one_sat X n1 Y Z T); case (try_one X Y Z T); auto end. intros s1 fRec; apply fRec; auto with arith. apply invariant_refine with (1 := H1); auto. intros; apply H; auto with arith. apply Nat.le_trans with (1 := H4); auto with arith. intros HH s1 Hs1 Hs2; case HH with s1; auto. apply invariant_refine with (1 := H1); auto. intros; apply H; auto. apply Nat.le_trans with (1 := H4); auto with arith. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia