proposition: Theorem invariant_gen_init_clauses: forall s, length s = size * size -> invariant (gen_init_clauses s) s.
proof: Proof. Proof with auto with arith. assert (forall s s1 cs p, valid_pos p -> length s = size * size -> invariant cs (prestrict p s) -> s1 = jump (pos2n p) s -> invariant (gen_init_clauses_aux s1 p cs) s). intros s s1; generalize s; elim s1; auto; clear s s1. intros s cs p H H0 H1 H2; rewrite prestrict_all in H1... case (Nat.le_gt_cases (length s) (pos2n p))... intros H3; absurd (length (jump (pos2n p) s) = length (@nil nat)). generalize (length_jump _ (pos2n p) s). rewrite <- H2; simpl. intros H4; assert (Eq1: length s = pos2n p)... contradict H3; rewrite Eq1... f_equal... intros a s1; unfold gen_init_clauses_aux; lazy beta; fold gen_init_clauses_aux; case s1; clear s1. intros Rec s cs p H0 H1 H2 H3. assert (F1: pos2n p < length s). case (Nat.le_gt_cases (length s) (pos2n p)); auto; intros H5. rewrite (jump_too_far _ (pos2n p) s) in H3; try discriminate... unfold gen_init_clauses_aux; lazy beta; fold gen_init_clauses_aux. case (In_dec eq_nat a ref_list); intros H5. replace s with (prestrict (next p) s). rewrite prestrict_update... replace (get p s) with a. apply invariant_clauses_update1... simpl; split... rewrite prestrict_get_default... apply out_not_in_refl. unfold get; rewrite <- H3... rewrite next_pos... apply prestrict_all... case (Nat.le_gt_cases (length s) (pos2n (next p))); auto; intros H6. rewrite (length_jump nat (pos2n p)). rewrite <- H3; simpl; rewrite next_pos... rewrite next_pos in H6... apply invariant_equiv with (prestrict p s)... split... rewrite prestrict_length... split... intros p1 Hp1. case (Nat.le_gt_cases (pos2n p) (pos2n p1)); intros Hp2. rewrite prestrict_get_default; auto; intros HH; contradict HH; apply out_not_in_refl. rewrite prestrict_get... split... split... rewrite prestrict_length... intros p1 Hp1. case (Nat.le_gt_cases (pos2n p) (pos2n p1)); intros Hp2. intros HH; contradict HH; unfold get. rewrite <-(Nat.sub_add (pos2n p) (pos2n p1)); auto with arith; rewrite Nat.add_comm, jump_add; rewrite <- H3; case (pos2n p1 - pos2n p); simpl; auto; intros; rewrite jump_nil; apply out_not_in_refl. rewrite prestrict_get... intros b s1 Rec s cs p H0 H1 H2 H3. assert (F0: b :: s1 = jump (pos2n (next p)) s). rewrite next_pos. replace (S (pos2n p)) with ((pos2n p) + 1). rewrite jump_add; rewrite <- H3; simpl... rewrite Nat.add_comm... assert (F1: pos2n (next p) < length s). case (Nat.le_gt_cases (length s) (pos2n (next p))); auto; intros H5. rewrite (jump_too_far _ (pos2n (next p)) s) in F0; try discriminate... case (In_dec eq_nat a ref_list); intros H4. apply Rec... apply valid_pos_next... rewrite <- H1... rewrite prestrict_update... replace (get p s) with a. apply invariant_clauses_update1... split; [idtac | split]... rewrite prestrict_get_default... apply out_not_in_refl. unfold get; rewrite <- H3... apply Rec... apply valid_pos_next... rewrite <- H1... apply invariant_equiv with (prestrict p s)... split... rewrite prestrict_length... split... rewrite prestrict_length... intros p1 Hp1. case (Nat.le_gt_cases (pos2n p) (pos2n p1)); intros Hp2. rewrite prestrict_get_default; auto; intros HH; contradict HH; apply out_not_in_refl. rewrite prestrict_get... rewrite prestrict_get... rewrite next_pos... split... rewrite prestrict_length... split... rewrite prestrict_length... intros p1 Hp1. case (Nat.le_gt_cases (pos2n p) (pos2n p1)); intros Hp2. case le_lt_eq_dec with (1 := Hp2); clear Hp2; intros Hp2; subst. intros HH; contradict HH; rewrite prestrict_get_default... apply out_not_in_refl. rewrite next_pos... rewrite prestrict_get... unfold get; rewrite <- Hp2; rewrite <- H3; simpl. intros HH; case H4... rewrite <- Hp2; rewrite next_pos... repeat rewrite prestrict_get... rewrite next_pos... case (le_lt_eq_dec 0 size); auto with arith; intros H1. intros s Hs; unfold gen_init_clauses; apply H; simpl... rewrite prestrict_0. apply invariant_init_c. rewrite mk_0_length... apply empty_mk_0. rewrite <- H1; simpl. intros s; case s; simpl. intros _; unfold gen_init_clauses; simpl. apply invariant_init_c. rewrite <- H1... apply empty_nil. intros; discriminate. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia