proposition: Theorem spec2_assoc: forall p1 p2 p3, is_generic p1 p2 -> is_tangent p2 p3 -> is_generic (add p1 p2) p3 -> is_generic p1 (add p2 p3) -> add p1 (add p2 p3) = add (add p1 p2) p3.
proof: Proof. intros p1 p2; kcase p1 p2. intros p p3 _ _ (HH, _); case HH; auto. intros p3 _ _ _ p4 _ _ _ _ _ _ _ _ _ _ _ p5 (_, (_, (HH, _))); case HH; auto. intros p1 x1 y1 H1 p2 x2 y2 H2 p4 x4 y4 H4 l Hp Hp2 Hp4 Hp4b Hx Hl Hx4 Hy4 p3. generalize Hp2 Hp4b; clear Hp2 Hp4b. kcase p2 p3. intros; discriminate. intros p _ _ _ _ (_, (HH, _)); case HH; auto. intros p _ _ _ _ _ (_, (HH, _)); case HH; auto. intros p2 x2b y2b H2b p5 x5 y5 H5 l1. intros Hp2b. intros Hp5 Hp5b Hd Hl1 Hx5 Hy5 Hp2. rewrite Hp2 in Hp2b. injection Hp2b; intros HH HH1; subst y2b x2b; clear Hp2b. generalize Hp Hp5 Hp5b; clear Hp Hp5 Hp5b. kcase p1 p5. intros; discriminate. intros; discriminate. intros p _ _ _ _ _ _ _ (_,(_,(_,HH))); case HH; rewrite opp_opp; auto. intros p1 _ _ _ p5 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ (_,(_,(HH,_))); case HH; auto. intros p1 x1b y1b H1b. intros p5b x5b y5b H5b p6 x6 y6 H6 l2. intros Hp1; pattern p1 at 2; rewrite Hp1; clear Hp1. intros Hp5; pattern p5b at 2; rewrite Hp5; clear Hp5. intros Hp6 _ Hd2 Hl2 Hx6 Hy6. intros tmp; injection tmp; intros HH1 HH2; subst y1b x1b; clear tmp H1b. intros tmp; injection tmp; intros HH1 HH2; subst y5b x5b; clear tmp H5b. intros _ Hp4b _ _. generalize Hp2 Hp4 Hp4b; clear Hp2 Hp4 Hp4b. kcase p4 p2. intros; discriminate. intros; discriminate. intros p _ _ _ (_, (_, (_,HH))); case HH; rewrite opp_opp; auto. intros p3 _ _ _ p4 _ _ _ _ _ _ _ _ _ _ _ _ _ _ (_,(_,(HH, _))); case HH; auto. intros p4b x4b y4b H4b p3b x3b y3b H3b p7 x7 y7 H7 l3. intros Hp4b; pattern p4b at 2; rewrite Hp4b; clear Hp4b. intros Hp3b; pattern p3b at 2; rewrite Hp3b; clear Hp3b. intros Hp7 _ Hd3 Hl3 Hx7 Hy7. intros tmp; injection tmp; intros HH1 HH2; subst y3b x3b; clear tmp H3b. intros tmp; injection tmp; intros HH1 HH2; subst y4b x4b; clear tmp H4b. intros _ _ _. subst p6 p7; apply curve_elt_irr; clear H6 H7 H2b; apply Keq_minus_eq; clear H4 H5; subst. Time field [H1 H2]; auto; repeat split; auto. intros VV; field_simplify_eq[H1 H2] in VV. case Hd3; symmetry; apply Keq_minus_eq; field_simplify_eq [H1 H2]; auto. intros VV; field_simplify_eq[H1 H2] in VV. case Hd2; symmetry; apply Keq_minus_eq; field_simplify_eq [H1 H2]; auto. Time field [H1 H2]; auto; repeat split; auto. intros VV; field_simplify_eq[H1 H2] in VV. case Hd3; symmetry; apply Keq_minus_eq; field_simplify_eq [H1 H2]; auto. intros VV; field_simplify_eq[H1 H2] in VV. case Hd2; symmetry; apply Keq_minus_eq; field_simplify_eq [H1 H2]; auto. intros p3 x3 y3 H3 p5 x5 y5 H5 p6 x6 y6 H6 l1 Hp3 Hp5 _ _ Hd _ _ _ _ _ _. rewrite Hp3; rewrite Hp5; intros (_, (HH,_)); case Hd; injection HH; auto. Time Qed. Theorem spec3_assoc: forall p1 p2 p3, is_generic p1 p2 -> is_tangent p2 p3 -> is_generic (add p1 p2) p3 -> is_tangent p1 (add p2 p3) -> add p1 (add p2 p3) = add (add p1 p2) p3. intros p1 p2. kcase p1 p2. intros p p3 _ _ (HH, _); case HH; auto. intros p3 _ _ _ p4 _ _ _ _ _ _ _ _ _ _ _ p5 (_, (_, (HH, _))); case HH; auto. intros p1 x1 y1 H1 p2 x2 y2 H2 p4 x4 y4 H4 l Hp Hp2 Hp4 Hp4b Hx Hl Hx4 Hy4 p3. generalize Hp2 Hp4b; clear Hp2 Hp4b. kcase p2 p3. intros; discriminate. intros p _ _ _ _ (_, (HH, _)); case HH; auto. intros p _ _ _ (_ ,(_ , HH)); case HH; rewrite opp_opp; auto. intros p2 x2b y2b H2b p5 x5 y5 H5 l1. intros Hp2b. intros Hp5 Hp5b Hd Hl1 Hx5 Hy5 Hp2. rewrite Hp2 in Hp2b. injection Hp2b; intros HH HH1; subst y2b x2b; clear Hp2b H2b. generalize Hp Hp5 Hp5b; clear Hp Hp5 Hp5b. kcase p1 p5. intros; discriminate. intros; discriminate. intros p _ _ _ _ _ _ _ (_, (_,HH)); case HH; rewrite opp_opp; auto. intros p1 x1b y1b H1b. intros p6 x6 y6 H6 l2. intros Hp1; pattern p1 at 3 4; rewrite Hp1; clear Hp1. intros Hp6 _ Hd2 Hl2 Hx6 Hy6. intros tmp; injection tmp; intros HH1 HH2; subst y1b x1b; clear tmp. intros tmp; injection tmp; intros HH1 HH2. subst y5 x5; clear tmp H5. rename HH1 into Hy1; rename HH2 into Hx1. generalize Hp2 Hp4; clear Hp2 Hp4. kcase p4 p2. intros; discriminate. intros; discriminate. intros p _ _ _ _ _ _ (_, (_, (_, HH))); case HH; rewrite opp_opp; auto. intros p3 _ _ _ p4 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ (_,(_,(HH, _))); case HH; auto. intros p4b x4b y4b H4b p2b x2b y2b H2b. intros p7 x7 y7 H7 l3. intros Hp4b; pattern p4b at 2; rewrite Hp4b; clear Hp4b. intros Hp2b; pattern p2b at 2; rewrite Hp2b; clear Hp2b. intros Hp7 _ Hd1 Hl3 Hx7 Hy7. intros tmp; injection tmp; intros HH1 HH2; subst y2b x2b; clear tmp H2b. intros tmp; injection tmp; intros HH1 HH2; subst y4b x4b; clear tmp H4b. intros _ _ _ _ _ _. subst p6 p7; apply curve_elt_irr; clear H6 H7; apply Keq_minus_eq; clear H4 H1b; subst. Time field [H2]; auto; repeat split; auto; intros HH; field_simplify_eq in HH; auto. case Hx; symmetry; apply Keq_minus_eq. field_simplify_eq; auto. case Hd1; symmetry; apply Keq_minus_eq; field_simplify_eq; repeat split; auto. intros HH1; ring_simplify in HH1; auto. case Hx; symmetry; apply Keq_minus_eq. field_simplify_eq; auto. case Hd2; apply Keq_minus_eq; field_simplify_eq; auto. Time field [H2]; auto; repeat split; auto; intros HH; field_simplify_eq in HH; auto. case Hx; symmetry; apply Keq_minus_eq. field_simplify_eq; auto. case Hd1; symmetry; apply Keq_minus_eq; field_simplify_eq; repeat split; auto. intros HH1; ring_simplify in HH1; auto. case Hx; symmetry; apply Keq_minus_eq. field_simplify_eq; auto. case Hd2; apply Keq_minus_eq; field_simplify_eq; auto. intros p1b x1b y1b H1b. intros p5b x5b y5b H5b. intros p3 x3 y3 H3 l2. intros Hp1b; pattern p1b at 2 5; rewrite Hp1b; clear Hp1b. intros Hp5b; pattern p5b at 2 4; rewrite Hp5b; clear Hp5b. intros Hp3 _; rewrite Hp3; clear Hp3. intros Hx1 _ _ _. intros tmp; injection tmp; intros HH1 HH2; subst y1b x1b; clear tmp. intros tmp; injection tmp; intros HH1 HH2; subst y5b x5b; clear tmp. intros _ _ _ _ _ (_,(HH, _)); case Hx1; injection HH; auto. intros p2b x2b y2b H2b. intros p3 x3 y3 H3. intros p5 x5 y5 H5 l2. intros Hp2b; pattern p2b at 2 5; rewrite Hp2b; clear Hp2b. intros Hp3; rewrite Hp3; clear Hp3. intros _ _ Hx1 _ _ _. intros tmp; injection tmp; intros HH1 HH2; subst y2b x2b; clear tmp. intros _ _ (_,(HH, _)); case Hx1; injection HH; auto. Time Qed. Theorem add_0_l: forall p, add inf_elt p = p. Proof. auto. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith