proposition: Theorem anti_literals_sat: forall p z s, sudoku s -> valid_pos p -> get p s = z -> ~ clause_sat (anti_literals (L p z)) s.
proof: Proof. Proof with auto with arith. generalize ref_list_ulist; intros Eq1. intros (x, y) z s; simpl; intros H1 (U1, U2) H2 (l, (H3, H4)). assert (U3: 0 < h). generalize U1; unfold size; case h; simpl... intros tmp; contradict tmp... assert (U4: 0 < w). generalize U1; unfold size; case w; simpl... rewrite Nat.mul_0_r; intros tmp; contradict tmp... generalize div_lt; intros U5. generalize mod_lt; intros U6. repeat match goal with H: In ?X (clause_merge ?Y ?Z) |- _ => case (clause_merge_in X Y Z); intros tmp _; case (tmp H); clear tmp H; auto; intros H end. case H1; clear H1; intros V1 (V2, _). case (gen_row_correct l x z); intros tmp _; case tmp; auto; clear tmp. apply (rm_incl _ lit_test) with (l1 := L (Pos x y) z::nil) (l2 := gen_row x z)... intros y1 (H5, H6); subst l. simpl in H4; absurd (y = y1). intros H7; apply (rm_not_in _ lit_test) with (a := L (Pos x y) z) (l1 := L (Pos x y) z::nil) (l2 := gen_row x z); subst; auto with datatypes. exact lit_test_trans. intros; apply lit_test_anti_sym. exact lit_test_exact. apply olist_one. apply gen_row_ordered. apply nth_ulist with (a := 0) (l := row x s)... rewrite length_row... rewrite length_row... apply ulist_perm with ref_list... apply Permutation_sym... repeat rewrite <- get_row; try rewrite H2... case H1; clear H1; intros V1 (_, (V2, _)). case (gen_column_correct l y z); intros tmp _; case tmp; auto; clear tmp. apply (rm_incl _ lit_test) with (l1 := L (Pos x y) z::nil) (l2 := gen_column y z)... intros x1 (H5, H6); subst l. simpl in H4; absurd (x = x1). intros H7; apply (rm_not_in _ lit_test) with (a := L (Pos x y) z) (l1 := L (Pos x y) z::nil) (l2 := gen_column y z); subst; auto with datatypes. exact lit_test_trans. intros; apply lit_test_anti_sym. exact lit_test_exact. apply olist_one. apply gen_column_ordered. apply nth_ulist with (a := 0) (l := column y s)... rewrite length_column... rewrite length_column... apply ulist_perm with ref_list... apply Permutation_sym... repeat rewrite <- get_column; try rewrite H2... case (gen_rect_correct l (div x h * h + div y w) z). apply rect_aux1... intros tmp _; case tmp; auto; clear tmp. apply (rm_incl _ lit_test) with (l1 := L (Pos x y) z::nil)... intros x1 (y1, (H5, (H6, H7))); subst l. simpl in H4. match type of H4 with get (Pos ?X ?Y) _ = _ => generalize H3 H4; clear H3 H4; replace (Pos X Y) with (Pos (h * div x h + x1) (w * div y w + y1)); [intros H3 H4 | idtac] end. match type of H4 with get (Pos ?X ?Y) _ = _ => assert (X = x /\ Y = y) end. apply rect_aux2... unfold size; rewrite (Nat.mul_comm w); apply mult_lt_plus... apply div_lt; rewrite Nat.mul_comm... rewrite get_rect in H4... rewrite get_rect in H2... generalize H4; clear H4. repeat rewrite (fun x => Nat.mul_comm x h). repeat ((rewrite mod_mult_comp || rewrite div_mult_comp); auto). rewrite (div_is_0 x1 h)... rewrite (div_is_0 y1 w)... repeat rewrite Nat.add_0_r. intros H4. apply nth_ulist with (a:= 0) (l := rect (div x h * h + div y w) s). rewrite length_rect... unfold size; apply mult_lt_plus... unfold size; rewrite (Nat.mul_comm h); apply mult_lt_plus... apply div_lt; rewrite Nat.mul_comm... case H1... rewrite length_rect... unfold size; apply mult_lt_plus... unfold size; rewrite (Nat.mul_comm h); apply mult_lt_plus... apply div_lt; rewrite Nat.mul_comm... case H1... apply ulist_perm with ref_list. apply Permutation_sym; case H1... intros _ (_, (_, tmp)); apply tmp; clear tmp. unfold size; rewrite (Nat.mul_comm h); apply mult_lt_plus... apply div_lt; rewrite Nat.mul_comm... apply ref_list_ulist. repeat rewrite (fun x => Nat.mul_comm x h). unfold out in H4; rewrite H4... repeat rewrite (Nat.mul_comm h)... unfold size; repeat rewrite (Nat.mul_comm h); apply mult_lt_plus... unfold size; rewrite (Nat.mul_comm w); apply mult_lt_plus... apply div_lt; rewrite Nat.mul_comm... repeat rewrite div_mult_comp; auto with arith. rewrite (div_is_0 x1); auto with arith. rewrite (div_is_0 y1); auto with arith. case H; clear H; intros V1 V2; rewrite V1 in H3; rewrite V2 in H3. match goal with H:(In ?X _) |- _ => apply (rm_not_in _ lit_test) with (a := X) (l1 := X::nil) (l2 := gen_rect (div x h * h + div y w) z); auto with datatypes end. exact lit_test_trans. intros; apply lit_test_anti_sym. exact lit_test_exact. apply olist_one. apply gen_rect_ordered. repeat rewrite (fun x => Nat.mul_comm x h). repeat ((rewrite mod_mult_comp || rewrite div_mult_comp); auto). rewrite (div_is_0 (div y w) h)... rewrite (mod_small (div y w) h)... apply div_lt; rewrite (Nat.mul_comm w)... apply div_lt; rewrite (Nat.mul_comm w)... case (gen_cell_correct l x y); auto; intros tmp; case tmp; auto; clear tmp. apply (rm_incl _ lit_test) with (l1 := L (Pos x y) z::nil) (l2 := gen_cell (Pos x y))... intros z1 (H5, H6); subst l. intros H7. simpl in H4. apply (rm_not_in _ lit_test) with (a := L (Pos x y) z) (l1 := L (Pos x y) z::nil) (l2 := gen_cell (Pos x y)); subst; auto with datatypes. exact lit_test_trans. intros; apply lit_test_anti_sym. exact lit_test_exact. apply olist_one. apply gen_cell_ordered. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia