proposition: Theorem gen_init_clauses_valid: forall s, length s = size * size -> valid (gen_init_clauses s) s.
proof: Proof. Proof with auto with arith. assert (Eq: forall s1 s p cs, length s = size * size -> s1 = jump (pos2n p) s -> valid_pos p -> ordered cs -> valid cs (prestrict p s) -> valid (gen_init_clauses_aux s1 p cs) s). intros s1; elim s1; clear s1; unfold gen_init_clauses_aux; lazy beta; fold gen_init_clauses_aux... intros s p cs H H0 H1 H2 H3; rewrite prestrict_all in H3... case (Nat.le_gt_cases (length s) (pos2n p))... intros H4; absurd (length (jump (pos2n p) s) = length (@nil nat)). generalize (length_jump _ (pos2n p) s). rewrite <- H0; simpl. intros H5; assert (Eq1: length s = pos2n p)... contradict H4; rewrite Eq1... f_equal... intros a s1; case s1; clear s1. intros Rec s p cs H0 H1 H2 H3 H4. 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 H1; try discriminate... case (In_dec eq_nat a ref_list); intros H5. unfold gen_init_clauses_aux; lazy beta; fold gen_init_clauses_aux. replace s with (prestrict (next p) s). rewrite prestrict_update... replace (get p s) with a. apply clauses_update_valid... simpl; split... rewrite prestrict_get_default... apply out_not_in_refl. apply anti_literals_ordered. intros; apply anti_literals_in... unfold get; rewrite <- H1... 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 <- H1; simpl; rewrite next_pos... rewrite next_pos in H6... simpl. intros n c Hn (p1, z1) Hl; simpl. case (H4 n c Hn (L p1 z1))... intros U1 (U2, U3); split... case (Nat.le_gt_cases (pos2n p) (pos2n p1)); intros V1. unfold get; rewrite <-(Nat.sub_add (pos2n p) (pos2n p1)); auto with arith. rewrite Nat.add_comm, jump_add; rewrite <- H1. case (pos2n p1 - pos2n p); simpl... intros n1; rewrite jump_nil; simpl; apply out_not_in_refl. rewrite <- (prestrict_get s p1 p)... intros b s1 Rec s p cs H0 H1 H2 H3 H4. assert (F0: b :: s1 = jump (pos2n (next p)) s). rewrite next_pos. replace (S (pos2n p)) with ((pos2n p) + 1). rewrite jump_add; rewrite <- H1; 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 H5. apply Rec... apply valid_pos_next... rewrite <- H0... apply clauses_update_ordered... apply anti_literals_ordered. rewrite prestrict_update... replace (get p s) with a. apply clauses_update_valid... simpl; split... rewrite prestrict_get_default... apply out_not_in_refl. apply anti_literals_ordered. intros; apply anti_literals_in... unfold get; rewrite <- H1... apply Rec... apply valid_pos_next... rewrite <- H0... intros n c Hn (p1, z1) Hl; simpl. case (H4 n c Hn (L p1 z1))... intros U1 (U2, U3); split... case (Nat.le_gt_cases (pos2n (next p)) (pos2n p1)); intros V1. rewrite prestrict_get_default... apply out_not_in_refl. rewrite prestrict_get... case (le_lt_eq_dec (pos2n p1) (pos2n p)); try intros V2. rewrite next_pos in V1... rewrite prestrict_get in U1... assert (p1 = p); try (subst p1). apply valid_pos_eq... unfold get; rewrite <- H1... intros s Hs. case (le_lt_eq_dec 0 size); auto with arith; intros V1. unfold gen_init_clauses; apply Eq; simpl... apply init_c_ordered. destruct s... simpl in Hs. lia. rewrite prestrict_0; apply valid_init_c. rewrite <- Hs; apply mk_0_length. apply empty_mk_0. generalize Hs. rewrite <- V1; case s; simpl... intros _; unfold gen_init_clauses; simpl. apply valid_init_c. rewrite <- V1... apply empty_nil. intros; discriminate. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia