proposition: Theorem sudoku_refine_id: forall s1 s2, sudoku s1 -> refine s1 s2 -> s1 = s2.
proof: Proof. Proof with auto with arith. intros s1 s2 H (H1, (H2, H3)). apply list_nth_eq with (r := out). rewrite H2... intros n; case (Nat.le_gt_cases (length s1) n); intros H4. repeat rewrite nth_default... rewrite H2; rewrite <- H1... replace n with (pos2n (Pos (div n size) (mod n size))). repeat rewrite (fun l x => (jump_nth nat l (pos2n x))). unfold get in H3; apply H3... split... apply div_lt... rewrite <- H1... apply mod_lt... generalize H4; rewrite H1; case size... intros HH; contradict HH... assert (F1: div n size < size)... apply div_lt... rewrite <- H1... assert (F2: mod n size < size)... apply mod_lt... generalize H4; rewrite H1; case size; simpl... intros tmp; contradict tmp... case H; intros _ (HH, _). apply Permutation_in with (l := row (div n size) s1)... unfold row. match goal with |- (In ?X ?Y) => case (in_ex_nth _ X out Y); intros _ tmp; apply tmp; clear tmp; exists (mod n size); split; auto end. rewrite length_take... apply Nat.add_le_mono_l with (div n size * size). repeat rewrite (fun x y => Nat.add_comm (x * y)). rewrite <- length_jump; rewrite H1. pattern size at 1; rewrite <- Nat.mul_1_l; rewrite <- Nat.mul_add_distr_r. apply Nat.mul_le_mono_r... apply Nat.mul_le_mono_r... simpl pos2n. rewrite jump_add; rewrite <- jump_nth. apply sym_equal; apply take_nth... simpl; apply sym_equal; apply div_mod_correct. generalize H4; rewrite H1; case size; simpl... intros tmp; contradict tmp... Qed.
imports: List UList Permutation Div OrderedList ListOp Lia