Library HighSchoolGeometry.barycentre

Require Export alignement.
Set Implicit Arguments.
Unset Strict Implicit.
Parameter barycentre : PP PP PO.

Axiom
add_PP_barycentre :
(a b : R) (A B : PO),
a + b 0
add_PP (cons a A) (cons b B) =
cons (a + b) (barycentre (cons a A) (cons b B)).

Lemma permute_barycentre :
(a b : R) (A B : PO),
a + b 0
barycentre (cons a A) (cons b B) = barycentre (cons b B) (cons a A).
intros a b A B H; try assumption.
apply conversion_PP with (a := a + b) (b := b + a); try ring; auto.
repeat rewrite <- add_PP_barycentre; auto.
RingPP.
unfold not in |- *; intros H1; apply H; auto; rewrite <- H1; ring; auto.
Qed.

Lemma barycentre_zero :
(a : R) (A B : PO), a 0 barycentre (cons a A) (cons 0 B) = A.
intros a A B H; try assumption.
apply conversion_PP with (a := a + 0) (b := a); try ring; auto.
repeat rewrite <- add_PP_barycentre; auto.
RingPP.
unfold not in |- *; intros H1; apply H; auto; rewrite <- H1; ring; auto.
replace (a + 0) with a; try ring; auto.
Qed.

Lemma bary_assoc :
(a b c : R) (A B C : PO),
a + b 0
b + c 0
a + (b + c) 0
barycentre (cons a A) (cons (b + c) (barycentre (cons b B) (cons c C))) =
barycentre (cons (a + b) (barycentre (cons a A) (cons b B))) (cons c C).
intros a b c A B C H H0 H1; try assumption.
apply conversion_PP with (a := a + (b + c)) (b := a + b + c); try ring; auto.
repeat rewrite <- add_PP_barycentre; auto.
Ringvec.
unfold not in |- *; intros H2; apply H1; auto; rewrite <- H2; ring; auto.
Qed.

Lemma homogene_barycentre :
(a b k : R) (A B : PO),
a + b 0
k 0
barycentre (cons (k × a) A) (cons (k × b) B) =
barycentre (cons a A) (cons b B).
intros a b k A B H H0; try assumption.
apply conversion_PP with (a := k × a + k × b) (b := k × (a + b)); try ring;
auto.
repeat rewrite <- add_PP_barycentre; auto.
rewrite distrib_mult_cons.
rewrite <- def_mult_PP.
repeat rewrite <- add_PP_barycentre; auto.
replace (k × a + k × b) with (k × (a + b)); try ring.
auto with ×.
replace (k × a + k × b) with (k × (a + b)); try ring.
auto with ×.
Qed.

Lemma def_vecteur_bary :
(a b : R) (A B G : PO),
a + b 0
G = barycentre (cons a A) (cons b B)
add_PP (mult_PP a (vec G A)) (mult_PP b (vec G B)) = zero.
intros.
cut (zero = mult_PP (a + b) (vec G G)); intros; auto.
rewrite H1.
apply add_PP_vecteur; auto.
rewrite (add_PP_barycentre (a:=a) (b:=b) A B); auto.
rewrite <- H0; auto.
Ringvec.
Qed.

Lemma def_vecteur_bary_rec :
(a b : R) (A B G : PO),
a + b 0
add_PP (mult_PP a (vec G A)) (mult_PP b (vec G B)) = zero
G = barycentre (cons a A) (cons b B).
unfold vec in |- *; intros.
apply conversion_PP with (a := a + b) (b := a + b); auto.
rewrite <- (add_PP_barycentre (a:=a) (b:=b) A B); auto.
replace (cons (a + b) G) with (add_PP (cons (a + b) G) zero).
rewrite <- H0.
RingPP.
RingPP.
Qed.

Lemma prop_vecteur_bary :
(a b : R) (A B G M : PO),
a + b 0
G = barycentre (cons a A) (cons b B)
add_PP (mult_PP a (vec M A)) (mult_PP b (vec M B)) =
mult_PP (a + b) (vec M G).
intros.
apply add_PP_vecteur; auto.
rewrite (add_PP_barycentre (a:=a) (b:=b) A B); auto.
rewrite <- H0; auto.
Qed.

Lemma prop_vecteur_bary_rec :
(a b : R) (A B G M : PO),
a + b 0
add_PP (mult_PP a (vec M A)) (mult_PP b (vec M B)) =
mult_PP (a + b) (vec M G) G = barycentre (cons a A) (cons b B).
unfold vec in |- *; intros.
apply conversion_PP with (a := a + b) (b := a + b); auto.
rewrite <- (add_PP_barycentre (a:=a) (b:=b) A B); auto.
cut
(add_PP (cons (- (a + b)) M) (cons (a + b) G) =
add_PP (mult_PP a (add_PP (cons (-1) M) (cons 1 A)))
(mult_PP b (add_PP (cons (-1) M) (cons 1 B))));
intros.
RingPP2 H1.
RingPP.
rewrite H0.
RingPP.
Qed.
Hint Resolve add_PP_barycentre: geo.

Lemma barycentre_alignes :
(a b : R) (A B : PO),
a + b 0 alignes A B (barycentre (cons a A) (cons b B)).
intros a b A B H; try assumption.
apply add_PP_alignes with (a := a) (b := b); auto with geo.
Qed.

Lemma colineaire_barycentre :
(k : R) (A B C : PO),
vec A C = mult_PP k (vec A B)
C = barycentre (cons (1 + - k) A) (cons k B).
unfold vec in |- *; intros.
elim
cons_inj
with
(a := 1)
(b := 1 + - k + k)
(A := C)
(B := barycentre (cons (1 + - k) A) (cons k B));
intros; auto with ×.
repeat rewrite <- add_PP_barycentre; auto.
RingPP2 H.
RingPP.
replace (1 + - k + k) with 1; try ring; auto with ×.
Qed.

Lemma alignes_barycentre :
A B C : PO,
A B
alignes A B C k : R, C = barycentre (cons k A) (cons (1 + - k) B).
unfold alignes, alignes1 in |- *; intros.
elim H0;
[ intros H1; tauto
| intros H1; elim H1; [ intros k H2; try clear H1 H0; try exact H2 ] ].
k; auto.
apply conversion_PP with (a := 1) (b := k + (1 + - k)); try ring; auto with ×.
rewrite H2; auto.
repeat rewrite <- add_PP_barycentre; auto.
replace (k + (1 + - k)) with 1; try ring; auto with ×.
Qed.
Hint Resolve barycentre_alignes prop_vecteur_bary def_vecteur_bary_rec
def_vecteur_bary homogene_barycentre barycentre_zero: geo.

Lemma existence_representant_vecteur :
A B C : PO, ex (fun D : POvec A D = vec B C :>PP).
unfold vec in |- *; intros.
(barycentre (cons (-1) B) (cons 2 (barycentre (cons 1 A) (cons 1 C)))).
pattern 1 at 2 in |- ×.
RReplace 1 (-1 + 2).
repeat rewrite <- add_PP_barycentre; auto.
RingPP.
discrR.
discrR.
Qed.

Lemma existence_representant_mult_vecteur :
(A B C : PO) (k : R),
ex (fun D : POvec A D = mult_PP k (vec B C) :>PP).
intros.
elim (classic (k = -1)); intros.
rewrite H.
elim existence_representant_vecteur with (A := A) (B := C) (C := B);
intros D H0; try clear existence_representant_vecteur;
try exact H0.
D.
rewrite H0; Ringvec.
unfold vec in |- ×.

(barycentre (cons (- k) B) (cons (1 + k) (barycentre (cons 1 A) (cons k C)))).
pattern 1 at 2 in |- ×.
RReplace 1 (- k + (1 + k)).
repeat rewrite <- add_PP_barycentre; auto.
RingPP.
unfold not in |- *; intros; apply H.
RReplace k (1 + k + -1).
rewrite H0.
ring.
RReplace (- k + (1 + k)) 1.
auto with ×.
Qed.

Lemma existence_representant_som_vecteur :
A B C D : PO,
ex (fun E : POvec A E = add_PP (vec A B) (vec C D) :>PP).
intros.
unfold vec in |- ×.
(barycentre (cons (-1) C) (cons 2 (barycentre (cons 1 B) (cons 1 D)))).
pattern 1 at 2 in |- ×.
RReplace 1 (-1 + 2).
repeat rewrite <- add_PP_barycentre; auto.
RingPP.
discrR.
RReplace (-1 + 2) 1.
discrR.
Qed.

Lemma existence_representant_comb_lin_vecteur :
(A B C D : PO) (a b : R),
ex
(fun E : PO
vec A E = add_PP (mult_PP a (vec A B)) (mult_PP b (vec C D)) :>PP).
intros.
elim
existence_representant_mult_vecteur with (A := A) (B := A) (C := B) (k := a);
intros B' H; try clear existence_representant_mult_vecteur;
rewrite <- H.
elim
existence_representant_mult_vecteur with (A := C) (B := C) (C := D) (k := b);
intros C' H0; try clear existence_representant_mult_vecteur;
rewrite <- H0.
elim
existence_representant_som_vecteur
with (A := A) (B := B') (C := C) (D := C'); intros E H1;
try clear existence_representant_som_vecteur; rewrite <- H1.
E; auto.
Qed.

Lemma distinct_mult_vecteur :
(A B C D : PO) (a : R),
A B :>PO
a 0 :>R vec C D = mult_PP a (vec A B) :>PP C D :>PO.
intros.
elim
existence_representant_mult_vecteur with (A := A) (B := A) (C := B) (k := a);
intros E H2; try clear existence_representant_mult_vecteur;
try exact H2.
cut (A E); intros.
apply distinct_egalite_vecteur with (1 := H3); auto.
rewrite H1; auto.
apply distinct_produit_vecteur with (3 := H2); auto.
Qed.

Lemma unicite_coor_bar :
(k k' : R) (A B I : PO),
A B
cons 1 I = add_PP (cons k A) (cons (1 + - k) B)
cons 1 I = add_PP (cons k' A) (cons (1 + - k') B) k = k'.
intros.
elim produit_vecteur_nul with (a := k + - k') (A := A) (B := B);
[ intros H2; try clear produit_vecteur_nul; try exact H2
| intros H2; try clear produit_vecteur_nul
| try clear produit_vecteur_nul ].
RReplace k (k + - k' + k').
rewrite H2.
ring.
absurd (A = B); auto.
VReplace (mult_PP (k + - k') (vec A B))
(add_PP (add_PP (cons k' A) (cons (1 + - k') B))
(add_PP (cons (- k) A) (cons (-1 + k) B))).
rewrite <- H1.
rewrite H0.
RingPP.
Qed.

Lemma unicite_coef_bar :
(x x0 : R) (A B : PO),
A B
1 + x 0
1 + x0 0
barycentre (cons 1 A) (cons x B) = barycentre (cons 1 A) (cons x0 B)
x = x0.
intros.
cut
(barycentre (cons (/ (1 + x) × 1) A) (cons (/ (1 + x) × x) B) =
barycentre (cons (/ (1 + x0) × 1) A) (cons (/ (1 + x0) × x0) B));
intros.
cut (1 + x = 1 + x0); intros.
RReplace x (-1 + (1 + x)).
rewrite H4.
ring.
cut (/ (1 + x) = / (1 + x0)); intros.
replace (1 + x) with (/ / (1 + x)).
rewrite H4.
auto with ×.
auto with ×.
replace (/ (1 + x)) with (/ (1 + x) × 1).
replace (/ (1 + x0)) with (/ (1 + x0) × 1).
apply
(unicite_coor_bar (k:=/ (1 + x) × 1) (k':=/ (1 + x0) × 1) (A:=A) (B:=B)
(I:=barycentre (cons (/ (1 + x) × 1) A) (cons (/ (1 + x) × x) B)));
auto.
pattern 1 at 1 in |- ×.
replace 1 with (/ (1 + x) × 1 + / (1 + x) × x).
rewrite <- add_PP_barycentre; auto.
replace (1 + - (/ (1 + x) × 1)) with (/ (1 + x) × x); auto.
auto with ×.
pattern 1 at 2 in |- ×.
replace 1 with (/ (1 + x) × (1 + x)); auto.
ring.
auto with ×.
replace (/ (1 + x) × 1 + / (1 + x) × x) with 1; auto.
auto with ×.
pattern 1 at 1 in |- ×.
replace 1 with (/ (1 + x) × (1 + x)); auto.
ring.
auto with ×.
replace (/ (1 + x) × 1 + / (1 + x) × x) with (/ (1 + x) × (1 + x)); auto.
auto with ×.
auto with ×.
rewrite H3.
pattern 1 at 1 in |- ×.
replace 1 with (/ (1 + x0) × 1 + / (1 + x0) × x0).
rewrite <- add_PP_barycentre; auto.
replace (1 + - (/ (1 + x0) × 1)) with (/ (1 + x0) × x0); auto.
pattern 1 at 2 in |- ×.
replace 1 with (/ (1 + x0) × (1 + x0)); auto.
ring.
auto with ×.
replace (/ (1 + x0) × 1 + / (1 + x0) × x0) with 1; auto.
auto with ×.
pattern 1 at 1 in |- ×.
replace 1 with (/ (1 + x0) × (1 + x0)); auto.
ring.
auto with ×.
replace (/ (1 + x0) × 1 + / (1 + x0) × x0) with (/ (1 + x0) × (1 + x0)); auto.
auto with ×.
auto with ×.
auto with ×.
ring.
rewrite homogene_barycentre.
rewrite homogene_barycentre; auto.
auto with ×.
try exact H0.
auto with ×.
Qed.

Lemma unicite_coor_bar_aux :
(A B C I : PO) (x y x' y' : R),
x x' :>R y y' :>R
cons 1 I = add_PP (add_PP (cons x A) (cons y B)) (cons (1 + - (x + y)) C)
:>PP
cons 1 I =
add_PP (add_PP (cons x' A) (cons y' B)) (cons (1 + - (x' + y')) C) :>PP
alignes A B C.
intros.
assert (vec C I = add_PP (mult_PP x (vec C A)) (mult_PP y (vec C B))).
unfold vec in |- ×.
rewrite H0; Ringvec.
assert (vec C I = add_PP (mult_PP x' (vec C A)) (mult_PP y' (vec C B))).
unfold vec in |- ×.
rewrite H1; Ringvec.
assert
(add_PP (mult_PP (x + - x') (vec C A)) (mult_PP (y + - y') (vec C B)) = zero).
VReplace zero (add_PP (vec C I) (mult_PP (-1) (vec C I))).
pattern (vec C I) at 1 in |- *; rewrite H2; rewrite H3; Ringvec.
assert (mult_PP (x + - x') (vec C A) = mult_PP (y' + - y) (vec C B)).
VReplace (mult_PP (y' + - y) (vec C B))
(add_PP (mult_PP (y' + - y) (vec C B)) zero).
rewrite <- H4; Ringvec.
elim H; [ intros H6; try clear H; try exact H6 | intros H6; try clear H ].
assert (x + - x' 0).
contrapose H6.
RReplace x' (x' + 0).
rewrite <- H; ring.
assert (alignes C B A); auto with geo.
apply colineaire_alignes with (/ (x + - x') × (y' + - y)).
VReplace (mult_PP (/ (x + - x') × (y' + - y)) (vec C B))
(mult_PP (/ (x + - x')) (mult_PP (y' + - y) (vec C B))).
rewrite <- H5; Fieldvec (x + - x').
assert (y' + - y 0).
contrapose H6.
RReplace y (y + 0).
rewrite <- H; ring.
assert (alignes C A B); auto with geo.
apply colineaire_alignes with (/ (y' + - y) × (x + - x')).
VReplace (mult_PP (/ (y' + - y) × (x + - x')) (vec C A))
(mult_PP (/ (y' + - y)) (mult_PP (x + - x') (vec C A))).
rewrite H5; Fieldvec (y' + - y).
Qed.

Lemma unicite_coor_bar2 :
(A B C I : PO) (x y x' y' : R),
¬ alignes A B C
cons 1 I = add_PP (add_PP (cons x A) (cons y B)) (cons (1 + - (x + y)) C)
:>PP
cons 1 I =
add_PP (add_PP (cons x' A) (cons y' B)) (cons (1 + - (x' + y')) C) :>PP
x = x' :>R y = y' :>R.
intros.
assert (¬ x x' ¬ y y').
apply not_or_and; auto.
contrapose H.
apply
(unicite_coor_bar_aux (A:=A) (B:=B) (C:=C) (I:=I) (x:=x) (y:=y) (x':=x')
(y':=y')); auto.
elim H2; [ intros H3 H4; try clear H2; try exact H3 ].
split; (apply NNPP; auto).
Qed.

Lemma parallelogramme_non_concours :
A B A1 B1 S : PO,
¬ alignes A A1 B
alignes A A1 S
alignes B B1 S
add_PP (cons 1 A) (cons (-1) A1) add_PP (cons 1 B) (cons (-1) B1).
intros.
contrapose H.
assert (vec A1 A = vec B1 B).
unfold vec in |- ×.
RingPP1 H2.
RingPP.
halignes H1 ipattern:k.
assert (A1 = A); auto with geo.
apply vecteur_nul_conf.
rewrite H3; rewrite H1; Ringvec.
halignes H0 ipattern:k0.
apply colineaire_alignes with (k0 + - k).
VReplace (vec A B) (add_PP (vec A S) (mult_PP (-1) (vec B S))).
rewrite H5; rewrite H4.
VReplace (vec B B1) (mult_PP (-1) (vec B1 B)).
rewrite <- H3.
Ringvec.
Qed.

Lemma concours_unique :
A B A1 B1 I J : PO,
¬ alignes A A1 B
B1 B
alignes A A1 I
alignes B1 B I alignes A A1 J alignes B1 B J I = J.
intros A B A1 B1 I J H.
unfold alignes in |- *; intros H50 H0 H1 H2 H3.
elim H3; clear H3; [ intros; tauto | unfold alignes1 in |- *; intros ].
elim H1; clear H1; [ intros; tauto | unfold alignes1 in |- *; intros ].
deroule_triangle A A1 B.
elim H2; clear H2; [ intros; tauto | unfold alignes1 in |- *; intros ].
elim H0; clear H0 H5 H4;
[ intros; tauto; clear H6 | unfold alignes1 in |- *; intros ].
elim H3; intros k0 H4; try clear H3; try exact H4.
elim H2; intros k1 H3; try clear H2; try exact H3.
elim H1; intros k2 H2; try clear H1; try exact H2.
elim H0; intros k3 H1; try clear H0; try exact H1.
elim (classic (k0 + - k2 = 0)); intros.
cut (k0 = k2); intros.
rewrite H5 in H4.
apply conversion_PP with (a := 1) (b := 1); auto.
rewrite H4; auto.
auto with ×.
replace k0 with (k2 + (k0 + - k2)); auto.
rewrite H0; ring.
ring.
cut
(cons (k0 + - k2) B =
add_PP (cons (k0 × k3 + - (k2 × k1)) A)
(cons (k0 + - k2 + - (k0 × k3 + - (k2 × k1))) A1));
intros.
assert (¬ alignes1 A A1 B); auto with geo.
absurd
(ex (fun k0 : Rcons 1 B = add_PP (cons k0 A) (cons (1 + - k0) A1)));
auto.
(/ (k0 + - k2) × (k0 × k3 + - (k2 × k1))).
apply mult_PP_regulier with (k0 + - k2); auto.
pattern 1 at 2 in |- ×.
replace 1 with ((k0 + - k2) × / (k0 + - k2)); auto.
rewrite <- distrib_mult_cons.
rewrite def_mult_PP.
replace ((k0 + - k2) × (/ (k0 + - k2) × (k0 × k3 + - (k2 × k1)))) with
(k0 × k3 + - (k2 × k1)); auto.
replace ((k0 + - k2) × 1) with (k0 + - k2); auto.
replace
((k0 + - k2) × / (k0 + - k2) + - (/ (k0 + - k2) × (k0 × k3 + - (k2 × k1))))
with (/ (k0 + - k2) × (k0 + - k2 + - (k0 × k3 + - (k2 × k1))));
auto.
replace
((k0 + - k2) × (/ (k0 + - k2) × (k0 + - k2 + - (k0 × k3 + - (k2 × k1)))))
with (1 × (k0 + - k2 + - (k0 × k3 + - (k2 × k1))));
auto.
rewrite H5.
RingPP.
replace 1 with ((k0 + - k2) × / (k0 + - k2)); auto.
ring.
auto with ×.
ring.
ring.
replace ((k0 + - k2) × (/ (k0 + - k2) × (k0 × k3 + - (k2 × k1)))) with
((k0 + - k2) × / (k0 + - k2) × (k0 × k3 + - (k2 × k1))).
replace ((k0 + - k2) × / (k0 + - k2)) with 1.
ring.
auto with ×.
ring.
auto with ×.
cut
(add_PP (cons (k0 × k2) B1) (cons (k0 × (1 + - k2)) B) =
add_PP (cons (k0 × k3) A) (cons (k0 × (1 + - k3)) A1));
intros.
cut
(add_PP (cons (k2 × k0) B1) (cons (k2 × (1 + - k0)) B) =
add_PP (cons (k2 × k1) A) (cons (k2 × (1 + - k1)) A1));
intros.
replace (cons (k0 + - k2) B) with
(add_PP (cons (k0 × (1 + - k2)) B) (cons (- (k2 × (1 + - k0))) B)).
replace (cons (k0 × k3 + - (k2 × k1)) A) with
(add_PP (cons (k0 × k3) A) (cons (- (k2 × k1)) A)).
replace (cons (k0 + - k2 + - (k0 × k3 + - (k2 × k1))) A1) with
(add_PP (cons (k0 × (1 + - k3)) A1) (cons (- (k2 × (1 + - k1))) A1)).
RingPP2 H5.
cut
(add_PP (cons (- (k2 × k0)) B1) (cons (- (k2 × (1 + - k0))) B) =
add_PP (cons (- (k2 × k1)) A) (cons (- (k2 × (1 + - k1))) A1));
intros.
RingPP2 H8.
RingPP.
replace (add_PP (cons (- (k2 × k0)) B1) (cons (- (k2 × (1 + - k0))) B)) with
(mult_PP (-1) (add_PP (cons (k2 × k0) B1) (cons (k2 × (1 + - k0)) B))).
rewrite H7.
RingPP.
RingPP.
RingPP.
RingPP.
RingPP.
rewrite distrib_mult_cons.
rewrite distrib_mult_cons.
rewrite <- H4.
rewrite H3; auto.
rewrite distrib_mult_cons.
rewrite distrib_mult_cons.
rewrite <- H2.
rewrite H1; auto.
Qed.

Lemma couple_colineaires_parallelogramme :
(A B C D : PO) (k k' : R),
A B
¬ alignes A B C
vec C D = mult_PP k (vec A B)
vec B D = mult_PP k' (vec A C) vec B D = vec A C.
unfold vec in |- *; intros.
cut
(cons 1 D =
add_PP (add_PP (cons (- k') A) (cons 1 B)) (cons (1 + - (- k' + 1)) C));
intros.
cut
(cons 1 D =
add_PP (add_PP (cons (- k) A) (cons k B)) (cons (1 + - (- k + k)) C));
intros.
cut (k = k' k = 1); intros.
elim H5; intros H6 H7; try clear H5; try exact H7.
rewrite <- H6 in H2; rewrite H7 in H2.
rewrite H2; Ringvec.
cut (- k = - k' k = 1); intros.
elim H5; intros H6 H7; try clear H5; try exact H7.
split; [ idtac | try assumption ].
replace k with (- - k).
rewrite H6; ring.
ring.
apply (unicite_coor_bar2 (A:=A) (B:=B) (C:=C) (I:=D)); auto.
RingPP2 H1.
RingPP.
RingPP2 H2.
RingPP.
Qed.