-
Notifications
You must be signed in to change notification settings - Fork 1
/
construction_lemmas_2.v
144 lines (117 loc) · 2.95 KB
/
construction_lemmas_2.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
(***************************************************************************)
(* Formalization of the Chou, Gao and Zhang's decision procedure. *)
(* Julien Narboux (Julien@narboux.fr) *)
(* LIX/INRIA FUTURS 2004-2006 *)
(* University of Strasbourg 2008-2009 *)
(***************************************************************************)
Require Export area_elimination_lemmas.
Theorem on_inter_line_parallel_ex: forall P Q R U V:Point,
~(parallel P Q U V) ->
exists Y:Point, (parallel Y R P Q) /\ (Col Y U V).
Proof with Geometry.
intros.
assert (P<>Q).
unfold not;intro.
assert (parallel P Q U V).
subst P.
Geometry.
intuition.
cases_col R P Q.
assert {Y : Point | Col Y P Q /\ Col Y U V}.
apply inter_llex...
DecompEx H2 Y.
exists Y.
intuition idtac.
cut (parallel P Q R Y).
Geometry.
unfold parallel,S4.
replace (S P R Q) with (- S R P Q).
2:symmetry;Geometry.
replace (S P Q Y) with (S Y P Q).
2:symmetry;Geometry.
rewrite H1.
rewrite H2.
ring.
assert ({Y':Point | (parallel P Q R Y') /\ R<>Y'}).
apply euclid_parallel_existence_strong...
DecompExAnd H2 Y'.
suppose (~ parallel Y' R U V).
assert {Y:Point | (Col Y Y' R) /\ (Col Y U V) }.
eapply inter_llex...
DecompExAnd H3 Y.
exists Y.
split;try assumption.
cut (parallel P Q R Y).
Geometry.
eapply col_par_par.
apply H5.
assumption.
Geometry.
unfold not;intro.
assert (parallel P Q U V).
eapply parallel_transitivity;eauto.
Geometry.
intuition.
Qed.
Theorem on_inter_parallel_parallel_ex_aux: forall P Q R U V W:Point,
~(parallel P Q U V) ->
{Y:Point | (parallel Y R P Q) /\ (parallel Y W U V)}.
Proof with Geometry.
intros.
assert (P<>Q).
unfold not;intro.
assert (parallel P Q U V).
subst P.
Geometry.
intuition.
assert (U<>V).
unfold not;intro.
assert (parallel P Q U V).
subst U.
Geometry.
intuition.
assert ({R':Point | (parallel P Q R R') /\ R<>R'}).
apply euclid_parallel_existence_strong...
DecompExAnd H2 R'.
assert ({W':Point | (parallel U V W W') /\ W<>W'}).
apply euclid_parallel_existence_strong...
DecompExAnd H2 W'.
assert {Y : Point | Col Y R R' /\ Col Y W W'}.
apply inter_llex...
unfold not;intro.
assert (parallel R R' U V).
eapply parallel_transitivity.
apply H7.
Geometry.
Geometry.
assert (parallel P Q U V).
eapply parallel_transitivity;apply H5 || Geometry .
intuition.
DecompExAnd H2 Y.
exists Y.
split.
cut (parallel P Q R Y).
Geometry.
eapply col_par_par.
apply H5.
Geometry.
Geometry.
cut (parallel U V W Y).
Geometry.
eapply col_par_par.
apply H7.
Geometry.
Geometry.
Qed.
Lemma on_inter_parallel_parallel_ex : forall P Q R U V W:Point,
~ parallel P Q U V -> ~ Col R U V ->
{Y :Point | (on_inter_parallel_parallel Y R P Q W U V)}.
Proof.
intros.
assert ({Y:Point | (parallel Y R P Q) /\ (parallel Y W U V)}).
apply on_inter_parallel_parallel_ex_aux;auto.
elim H1;intros Y HY;use HY;clear H1.
exists Y.
unfold on_inter_parallel_parallel.
repeat split;auto with Geom.
Qed.