proposition: Theorem get_rect x y s : x < size -> y < size -> get (Pos x y) s = nth (mod x h * w + mod y w) (rect (div x h * h + div y w) s) out.
proof: Proof. Proof with auto with arith. intros H1 H2; unfold get, rect; simpl. generalize (h_pos _ H1); intros U1. generalize (w_pos _ H1); intros U2. assert (F1: div y w < h). apply div_lt; rewrite Nat.mul_comm... repeat (rewrite (fun x => Nat.mul_comm x h)); rewrite mod_mult_comp... rewrite div_mult_comp, (mod_small (div y w) h), (div_is_0 (div y w) h), Nat.add_0_r... match goal with |- context [take_and_jump _ _ _ (jump ?X _)] => replace (x * size + y) with (X + (mod x h * size + mod y w)) end. 2: { apply sym_equal. pattern x at 1; rewrite (div_mod_correct x h)... pattern y at 1; rewrite (div_mod_correct y w)... lia. } rewrite jump_add. match goal with |- context [jump ?X s] => generalize (jump X s) end. intros l; rewrite <- jump_nth; generalize l; clear l. generalize (mod_lt x h U1). generalize (mod x h). cut (w <= size). - generalize size; intros m. intros U3 n; generalize h; elim n; simpl... + clear n H1 H2 U1. intros h1; case h1; simpl... * intros HH; contradict HH... * intros n1 _ l. case (Nat.le_gt_cases (length l) (mod y w)); intros H1. ++ rewrite jump_too_far. ** rewrite take_and_jump_nil. rewrite <- app_nil_end. apply sym_equal; apply take_nth... ** pose proof (mod_lt y w). lia. ++ rewrite nth_app_l. ** apply sym_equal; apply take_nth... left; apply mod_lt... ** case (Nat.le_gt_cases (length l) w); intros H2. *** rewrite length_take_small... *** rewrite length_take... apply mod_lt... + intros n1 Rec h1; case h1; simpl. * intros HH; contradict HH... * intros h2 HH l. case (Nat.le_gt_cases (length l) w); intros H3. ++ rewrite nth_app_r. ** rewrite length_take_small, jump_too_far... *** rewrite take_and_jump_nil. repeat rewrite nth_default... apply Nat.le_trans with (1 := H3)... *** apply Nat.le_trans with (1 := H3)... ** rewrite length_take_small... ++ rewrite nth_app_r. ** rewrite length_take... repeat rewrite <- Nat.add_assoc; rewrite (Nat.add_comm w), Nat.add_sub... rewrite jump_nth, jump_add, <- jump_nth... ** rewrite length_take... - unfold size; nia. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia