proposition: Theorem gen_rect_sat: forall i z s, length s = size * size -> i < size -> (clause_sat (gen_rect i z) s <-> In z (rect i s)).
proof: Proof. Proof with auto with arith. intros i z s H H0. assert (V1: 0 < h) by (generalize H0; unfold size; lia). assert (V2: 0 < w) by (generalize H0; unfold size; lia). generalize mod_lt div_lt; intros aux1 aux2. split. intros (l, (Hl1, Hl2)). case (gen_rect_correct l i z)... intros tmp _; case (tmp Hl1); auto; clear tmp Hl1. intros i1 (j1, (H1, (H2, H3))). subst; simpl in Hl2. rewrite get_rect in Hl2. assert (Eq: div (h * div i h + i1) h * h + div (w * mod i h + j1) w = i). repeat rewrite div_mult_comp... rewrite (div_is_0 i1 h)... rewrite (div_is_0 j1 w)... pose proof (div_mod_correct i h). lia. subst z; rewrite Eq; apply nth_In. apply Nat.le_lt_trans with ((h - 1) * w + (w - 1))... apply Nat.add_le_mono. apply Nat.mul_le_mono_r... match goal with |- mod ?X ?Y <= ?T => generalize (mod_lt X Y V1); auto with arith end. case h; auto with arith; intros; simpl minus; repeat rewrite Nat.sub_0_r... match goal with |- mod ?X ?Y <= ?T => generalize (mod_lt X Y V2); auto with arith end. case w; auto with arith; intros; simpl minus; repeat rewrite Nat.sub_0_r... rewrite length_rect... replace size with ((h - 1) * w + w)... pattern w at 2; rewrite <- Nat.mul_1_l; rewrite <- Nat.mul_add_distr_r. rewrite Nat.sub_add... unfold size; repeat rewrite (Nat.mul_comm h); apply mult_lt_plus... unfold size; repeat rewrite (Nat.mul_comm w); apply mult_lt_plus... intros H1; red. case (in_ex_nth _ z 0 (rect i s)); intros tmp _ ; case (tmp H1); clear tmp H1. intros j (Hj1, Hj2). exists (L (Pos (div i h * h + div j w) (mod i h * w + mod j w)) z); simpl. split. match goal with |- In ?l (gen_rect ?i ?z) => case (gen_rect_correct l i z); auto; intros _ tmp; apply tmp; clear tmp end. exists (div j w); exists (mod j w); repeat split... f_equal. f_equal. rewrite (Nat.mul_comm h)... rewrite (Nat.mul_comm w)... apply div_lt; rewrite (Nat.mul_comm w); rewrite length_rect in Hj1... rewrite Hj2. rewrite get_rect. f_equal; auto; [idtac | f_equal]... rewrite length_rect in Hj1... rewrite (Nat.mul_comm (div i h)); rewrite (Nat.mul_comm (mod i h)); repeat rewrite mod_mult_comp... rewrite mod_small. rewrite mod_small. apply sym_equal; apply div_mod_correct... apply mod_lt... apply div_lt... rewrite (Nat.mul_comm w)... rewrite (Nat.mul_comm (div i h)); rewrite (Nat.mul_comm (mod i h)); repeat rewrite div_mult_comp... rewrite (fun x y => div_is_0 (div x y))... rewrite (fun x y => div_is_0 (mod x y))... pose proof (div_mod_correct i h). lia. apply div_lt... rewrite (Nat.mul_comm w)... rewrite length_rect in Hj1... unfold size; rewrite (Nat.mul_comm h); apply mult_lt_plus... apply div_lt... rewrite (Nat.mul_comm w); rewrite length_rect in Hj1... unfold size; apply mult_lt_plus... Qed.
imports: List UList Permutation Div OrderedList ListOp Lia