proposition: Theorem valid_init_c: forall s, length s = size * size -> empty s -> valid init_c s.
proof: Proof. Proof with auto with arith. unfold init_c; intros s H H1 n c Hn l Hl. case (fold_clause_insert1 _ (fun iz => gen_row (fst iz) (snd iz))) with (1 := Hn); clear Hn. intros ((x,z), (n1, (HH1, HH2))); simpl in HH2. injection HH2; intros; subst; clear HH2. case (cross1_correct (x, z)); intros tmp _; case (tmp HH1); clear tmp HH1. intros x1 (z1, (V1, (V2, V3))); injection V3; intros; subst; clear V3. case (gen_row_correct l x1 z1). intros tmp _; case (tmp Hl); clear tmp. intros y1 (Hl1, Hy); subst. repeat (split; auto); case (in_indexes x1)... intros Hn; case (fold_clause_insert1 _ (fun iz => gen_column (fst iz) (snd iz))) with (1 := Hn); clear Hn. intros ((y,z), (n1, (HH1, HH2))); simpl in HH2. injection HH2; intros; subst; clear HH2. case (cross1_correct (y, z)); intros tmp _; case (tmp HH1); clear tmp HH1. intros y1 (z1, (V1, (V2, V3))); injection V3; intros; subst; clear V3. case (gen_column_correct l y1 z1). intros tmp _; case (tmp Hl); clear tmp. intros x1 (Hl1, Hy); subst. repeat (split; auto); case (in_indexes y1)... intros Hn; case (fold_clause_insert1 _ (fun iz => gen_rect (fst iz) (snd iz))) with (1 := Hn); clear Hn. intros ((i,z), (n1, (HH1, HH2))); simpl in HH2. injection HH2; intros; subst; clear HH2. case (cross1_correct (i, z)); intros tmp _; case (tmp HH1); clear tmp HH1. intros i1 (z1, (V1, (V2, V3))); injection V3; intros; subst; clear V3. case (gen_rect_correct l i1 z1). case (in_indexes i1)... intros tmp _; case (tmp Hl); clear tmp. intros x1 (y1, (Hl1, (Hl2, Hl3))); subst. repeat (split; auto). unfold size. repeat rewrite (Nat.mul_comm h); apply mult_lt_plus... apply div_lt... case (in_indexes i1)... unfold size. repeat rewrite (Nat.mul_comm w); apply mult_lt_plus... apply mod_lt... apply Nat.le_lt_trans with (2 := Hl2)... unfold all_cell; intros Hn; case fold_clause_insert1 with (1 := Hn); clear Hn. intros ((x, y), (n1, (HH1, HH2))); simpl in HH2. injection HH2; intros; subst; clear HH2. case (cross2_correct (Pos x y)); intros tmp _; case (tmp HH1); clear tmp HH1. intros H2 H3. case (gen_cell_correct l x y); intros tmp _; case (tmp Hl); clear tmp. intros z (V1, V2); subst. repeat (split; auto). intros HH; case HH. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia