proposition: Lemma chain_gen_OK : forall s:signature, OK s (chain_gen s).
proof: Proof. intro s; functional induction chain_gen s. red. - cbn. apply F1_correct. - cbn; apply F3_correct. - cbn; rewrite (exact_log2_spec _ _ e2). apply F2q_correct. - cbn. generalize (N_pos_div_eucl_divides _ _ _ e3); intro eq_i. rewrite <- eq_i at 1; apply correct_app. + apply IHc. + apply IHc0. - cbn; pattern i at 1; replace i with (gamma i * (N2pos q) + N2pos _r). + cbn in *. * apply KFF_correct;auto. replace (gamma i) with (N2pos _r + (gamma i - N2pos _r)) at 1. -- apply IHc. -- rewrite Pplus_minus;auto with chains. apply Pos.lt_gt; rewrite N2pos_lt_switch2. generalize (N.pos_div_eucl_remainder i (N.pos (gamma i) )); rewrite e3; simpl;auto with chains. destruct _r; [ contradiction | auto with chains]. + apply N_pos_div_eucl_rest; auto with chains. destruct _r;try contradiction; auto with chains. apply (div_gamma_pos _ _ _ e3); auto with chains. apply pos_gt_3;auto with chains. destruct (exact_log2 i); [contradiction | reflexivity]. - apply FK_correct, IHc. - cbn in *; red; replace (p + d)%positive with (p * N2pos q)%positive. * apply FFK_correct; auto with chains. * generalize (N.pos_div_eucl_spec (p + d) (N.pos p)); rewrite e1; rewrite N.add_0_r ; intro H3; case_eq (q * N.pos p)%N. intro H4; rewrite H4 in H3 ; discriminate. intros p0 H4; rewrite H4 in H3; injection H3; intro H5; rewrite H5. N2pos_destruct q q. injection H4;auto with chains. rewrite Pos.mul_comm; auto with chains. - cbn; red; replace (p+d) with (p * N2pos q + N2pos _r). + apply KFK_correct;auto with chains. cbn in *; replace (N2pos _r + (p - N2pos _r))%positive with p in IHc. apply IHc. rewrite Pplus_minus; auto. generalize (N.pos_div_eucl_remainder (p + d) (N.pos p)); rewrite e1; cbn; intro H3. apply Pos.lt_gt; rewrite N2pos_lt_switch2;auto with chains. destruct _r; [contradiction | auto with chains]. + generalize (N.pos_div_eucl_spec (p + d) (N.pos p)). rewrite e1; intros H3. case_eq q. { intro; generalize (pos_div_eucl_quotient_pos _ _ _ _ e1). destruct 1;auto with chains. rewrite pos2N_inj_add; apply N.le_add_r. } { intros p0 Hp0;subst q; cbn; destruct _r; [ contradiction | ]. simpl; simpl in H3; injection H3. rewrite Pos.mul_comm; auto with chains. } Qed.
imports: Coq(List PArith Relations Lia) additions(Monoid_def Monoid_instances Strategies) Coq(Recdef Wf_nat) additions(More_on_positive Pow Euclidean_Chains Dichotomy BinaryStrat) Coq(NArith)