proposition: Lemma chain_gen_OK : forall s:signature, OK s (chain_gen s).
proof: Proof. intro s; functional induction chain_gen s. - split; [apply F1_correct | apply F1_proper]. - split; [apply F3_correct | apply F3_proper]. - generalize (exact_log2_spec _ _ e2);intro; subst i; split; [apply Fexp2_correct | apply Fexp2_proper]. - destruct IHc, IHc0. generalize (N_pos_div_eucl_divides _ _ _ e3); intro eq_i. split. + cbn. rewrite <- eq_i at 1 ; apply Fcompose_correct;auto. + pattern i at 1 ; rewrite <- eq_i at 1; apply Fcompose_proper;auto. - pattern i at 1; replace i with (gamma i * (N2pos q) + N2pos _r). + destruct IHc, IHc0;split. * apply KFF_correct;auto. simpl; simpl in H. replace (gamma i) with (N2pos _r + (gamma i - N2pos _r)) at 1. apply H. 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 KFF_proper;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]. - destruct IHc; split. + apply FK_correct; auto with chains. + apply FK_proper; auto with chains. - destruct IHc, IHc0;split. + 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. + apply FFK_proper;auto with chains. - destruct IHc, IHc0; split. + red; replace (p+d) with (p * N2pos q + N2pos _r). * apply KFK_correct;auto with chains. red in H; replace (N2pos _r + (p - N2pos _r))%positive with p in H. apply H. 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; clear H H0 H1 H2. 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. } + apply KFK_proper; auto with chains. Qed.
imports: Coq(Inverse_Image Inclusion Wf_nat NArith Arith PArith Recdef Wf_nat Lexicographic_Product Lia) additions(Addition_Chains Compatibility More_on_positive Wf_transparent Dichotomy BinaryStrat) Coq(Lia)