proposition: Theorem init_c_sat: forall s, length s = size * size -> (sat init_c s <-> (forall i, i < size -> incl ref_list (row i s)) /\ (forall i, i < size -> incl ref_list (column i s)) /\ (forall i, i < size -> incl ref_list (rect i s)) /\ (forall p, valid_pos p -> In (get p s) ref_list)).
proof: Proof. Proof with auto. intros s H0; unfold init_c; split. intros H; repeat split. intros i Hi z Hz. case (gen_row_sat i z s); auto; intros tmp _; apply tmp; clear tmp. case (H (length (gen_row i z)) (gen_row i z)); auto; clear H. replace (gen_row i z) with ((fun iz => gen_row (fst iz) (snd iz)) (i,z))... apply fold_clause_insert3 with (f := (fun iz => gen_row (fst iz) (snd iz))); simpl... case (cross1_correct (i, z)); auto; intros _ tmp; apply tmp; clear tmp. exists i; exists z; repeat split; simpl... case (in_indexes i)... intros l (Hl1, Hl2); exists l... intros i Hi z Hz. case (gen_column_sat i z s); auto; intros tmp _; apply tmp; clear tmp. case (H (length (gen_column i z)) (gen_column i z)); auto; clear H. apply fold_clause_insert2 with (f := (fun iz => gen_row (fst iz) (snd iz)))... replace (gen_column i z) with ((fun iz => gen_column (fst iz) (snd iz)) (i,z))... apply fold_clause_insert3 with (f := (fun iz => gen_column (fst iz) (snd iz))); simpl... case (cross1_correct (i, z)); auto; intros _ tmp; apply tmp; clear tmp. exists i; exists z; repeat split; simpl... case (in_indexes i)... intros l (Hl1, Hl2); exists l... intros i Hi z Hz. case (gen_rect_sat i z s); auto; intros tmp _; apply tmp; clear tmp. case (H (length (gen_rect i z)) (gen_rect i z)); auto; clear H. apply fold_clause_insert2 with (f := (fun iz => gen_row (fst iz) (snd iz)))... apply fold_clause_insert2 with (f := (fun iz => gen_column (fst iz) (snd iz)))... replace (gen_rect i z) with ((fun iz => gen_rect (fst iz) (snd iz)) (i,z))... apply fold_clause_insert3 with (f := (fun iz => gen_rect (fst iz) (snd iz))); simpl... case (cross1_correct (i, z)); auto; intros _ tmp; apply tmp; clear tmp. exists i; exists z; repeat split; simpl... case (in_indexes i)... intros l (Hl1, Hl2); exists l... case (all_cell_sat s); auto; intros tmp _; apply tmp; clear tmp. intros n c H1. case (H n c)... apply fold_clause_insert2 with (f := (fun iz => gen_row (fst iz) (snd iz)))... apply fold_clause_insert2 with (f := (fun iz => gen_column (fst iz) (snd iz)))... apply fold_clause_insert2 with (f := (fun iz => gen_rect (fst iz) (snd iz)))... intros l (Hl1, Hl2); exists l... intros (H1, (H2, (H3, H4))). intros n c Hn. match goal with H : In ?X (fold_right ?Y ?Z ?T) |- _ => case (fold_clause_insert1 _ (fun iz => gen_row (fst iz) (snd iz)) _ _ _ Hn); clear H end. intros ((i, z), (n1, (Hn1, Hn2))). injection Hn2; clear Hn2; intros; subst. case (cross1_correct (i, z))... intros tmp _; case tmp; auto; clear tmp Hn1. intros i1 (z1, (V1, (V2, V3))); injection V3; intros; subst; clear V3. case (gen_row_sat i1 z1 s)... case (in_indexes i1)... intros _ tmp; apply tmp; clear tmp. apply H1... case (in_indexes i1)... intros H; match goal with H : In ?X (fold_right ?Y ?Z ?T) |- _ => case (fold_clause_insert1 _ (fun iz => gen_column (fst iz) (snd iz)) _ _ _ H); clear H end. intros ((i, z), (n1, (Hn1, Hn2))). injection Hn2; clear Hn2; intros; subst. case (cross1_correct (i, z))... intros tmp _; case tmp; auto; clear tmp Hn1. intros i1 (z1, (V1, (V2, V3))); injection V3; intros; subst; clear V3. case (gen_column_sat i1 z1 s)... case (in_indexes i1)... intros _ tmp; apply tmp; clear tmp. apply H2... case (in_indexes i1)... intros H; match goal with H : In ?X (fold_right ?Y ?Z ?T) |- _ => case (fold_clause_insert1 _ (fun iz => gen_rect (fst iz) (snd iz)) _ _ _ H); clear H end. intros ((i, z), (n1, (Hn1, Hn2))). injection Hn2; clear Hn2; intros; subst. case (cross1_correct (i, z))... intros tmp _; case tmp; auto; clear tmp Hn1. intros i1 (z1, (V1, (V2, V3))); injection V3; intros; subst; clear V3. case (gen_rect_sat i1 z1 s)... case (in_indexes i1)... intros _ tmp; apply tmp; clear tmp. apply H3... case (in_indexes i1)... intros H; case (all_cell_sat s). intros _ tmp; apply (tmp H4 n c)... Qed.
imports: List UList Permutation Div OrderedList ListOp Lia