Library cube
Require Import Cring ssreflect ssrfun ssrbool eqtype ssrnat finset bigop.
Require Import seq choice fintype tuple div zmodp ssralg ssrnum.
Local Open Scope ring_scope.
Import GRing.Theory.
Section Cube.
(* Comme Coq ne connait rien en géométrie on doit commencer par définir *)
(* les notions de base de géométrie *)
(* Le corps des coordonées *)
Variable R : numFieldType.
(* Pour pouvoir décider les équations sur R *)
Lemma Rsth : Setoid_Theory R (@eq R).
Global Instance Roperators:
@Ring_ops R 0%R 1%R +%R *%R (fun x y => x - y)%R -%R (@eq R).
Global Instance Rring: (@Ring _ _ _ _ _ _ _ _ Roperators).
Global Instance Rcring: (Cring (Rr:=Rring)).
(* Un petit test *)
Fact test (x y : R) : (x - y) * (x + y) = x * x - y * y.
(******************************************************************************)
(* POINT *)
(******************************************************************************)
Inductive point := Point of R & R & R.
(* On a besoin de l'égalité sur les points : p1 == p2 *)
Definition eq_point p1 p2 :=
let: Point x1 y1 z1 := p1 in
let: Point x2 y2 z2 := p2 in [&& x1 == x2, y1 == y2 & z1 == z2].
Lemma eq_pointP : Equality.axiom eq_point.
Canonical point_eqMixin := EqMixin eq_pointP.
Canonical point_eqType := Eval hnf in EqType point point_eqMixin.
(******************************************************************************)
(* LIGNE *)
(******************************************************************************)
(* Définition d'une ligne : deux points distincts *)
Inductive line := Line (p1 p2 : point) of (p1 != p2).
(* x1 / y1, x2 / y2 et z1 / z2 sont proportionnels *)
Definition proportional (x1 y1 x2 y2 x3 y3 : R) :=
[&& x1 * y2 == y1 * x2, x1 * y3 == y1 * x3 & x2 * y3 == y2 * x3].
Lemma proportionalP (x1 y1 x2 y2 x3 y3 : R) :
reflect (exists k, (x1, x2, x3) = (k * y1, k * y2, k * y3) \/
(y1, y2, y3) = (k * x1, k * x2, k * x3))
(proportional x1 y1 x2 y2 x3 y3).
Lemma proportionalNZP (x1 y1 x2 y2 x3 y3 : R) (NZ : (x1, x2, x3) != 0) :
reflect (exists k , (y1, y2, y3) = (k * x1, k * x2, k * x3))
(proportional x1 y1 x2 y2 x3 y3).
Lemma proportional_id x y z : proportional x x y y z z.
Lemma proportionalC x1 y1 x2 y2 x3 y3 :
proportional x1 y1 x2 y2 x3 y3 = proportional y1 x1 y2 x2 y3 x3.
Lemma proportional_trans x1 y1 z1 x2 y2 z2 x3 y3 z3 (PNZ : (y1, y2, y3) != 0) :
proportional x1 y1 x2 y2 x3 y3 -> proportional y1 z1 y2 z2 y3 z3 ->
proportional x1 z1 x2 z2 x3 z3.
(* Un point est sur la line : p \in l *)
Definition on_line (l : line) (p : point) :=
let: Line (Point x1 y1 z1) (Point x2 y2 z2) _ := l in
let : Point x3 y3 z3 := p in
proportional (x1 - x2) (x1 - x3) (y1 - y2) (y1 - y3) (z1 - z2) (z1 - z3).
Canonical on_line_predType := mkPredType on_line.
(* Deux lignes parallèles : l1 /l l2 *)
Definition lpar l1 l2 :=
let: Line (Point x1 y1 z1) (Point x2 y2 z2) _ := l1 in
let: Line (Point x3 y3 z3) (Point x4 y4 z4) _ := l2 in
proportional (x1 - x2) (x3 - x4) (y1 - y2) (y3 - y4) (z1 - z2) (z3 - z4).
Notation " l1 /[l]/ l2 " := (lpar l1 l2) (at level 10).
Lemma lpar_id l : l /[l]/ l.
Lemma lparC l1 l2 : l1 /[l]/ l2 = l2 /[l]/ l1.
Lemma lpar_trans l1 l2 l3 : l1 /[l]/ l2 -> l2 /[l]/ l3 -> l1 /[l]/ l3.
(******************************************************************************)
(* PLAN *)
(******************************************************************************)
Inductive plane := Plane (a b c d : R) of (a, b, c) != (0, 0, 0).
(* Pour l'appartenance d'un point à un plan: p \on P *)
Definition on_plane pl p :=
let: Point x y z := p in
let: Plane a b c d _ := pl in a * x + b * y + c * z == d.
Notation "p \on pl" := (on_plane pl p) (at level 10).
(* Deux plans parallèles : P1 /p/ P2 *)
Definition ppar p1 p2 :=
let: Plane a1 b1 c1 d1 _ := p1 in
let: Plane a2 b2 c2 d2 _ := p2 in proportional a1 a2 b1 b2 c1 c2.
Notation " p1 /[p]/ p2 " := (ppar p1 p2) (at level 10).
Lemma ppar_id p : p /[p]/ p.
Lemma pparC p1 p2 : p1 /[p]/ p2 = p2 /[p]/ p1.
Lemma ppar_trans p1 p2 p3 : p1 /[p]/ p2 -> p2 /[p]/ p3 -> p1 /[p]/ p3.
(* Appartenance d'une ligne à un plan : l \in P *)
Definition l_on_plane (pl : plane) l :=
let: Line p1 p2 _ := l in (on_plane pl p1) && (on_plane pl p2).
Canonical l_on_plane_predType := mkPredType l_on_plane.
Lemma l_on_planeE (p1 p2 : point) (L : p1 != p2) (P : plane) :
p1 \on P -> p2 \on P -> Line L \in P.
(* L'intersection d'un plan avec deux plans parallèles donne deux lignes *)
(* parallèles *)
Lemma par_2_plane (p1 p2 p3 : plane) (l1 l2 : line) :
l1 \in p1 -> l1 \in p3 -> l2 \in p2 -> l2 \in p3 ->
~~ p1 /[p]/ p3 -> p1 /[p]/ p2 -> l1 /[l]/ l2.
(******************************************************************************)
(* CUBE *)
(******************************************************************************)
(* les faces sont numérotées de 0 à 5 *)
Definition face := 'I_6.
(* Appartenance à une face du cube (les faces sont numérotées de 0 à 5) *)
Definition on_face (f : face) p :=
let: Point x y z := p in
if f == 0%N :> nat then [&& x == 0, 0 <= y <= 1 & 0 <= z <= 1] else
if f == 1%N :> nat then [&& x == 1, 0 <= y <= 1 & 0 <= z <= 1] else
if f == 2%N :> nat then [&& y == 0, 0 <= x <= 1 & 0 <= z <= 1] else
if f == 3%N :> nat then [&& y == 1, 0 <= x <= 1 & 0 <= z <= 1] else
if f == 4%N :> nat then [&& z == 0, 0 <= x <= 1 & 0 <= y <= 1] else
[&& z == 1, 0 <= x <= 1 & 0 <= y <= 1].
Canonical on_face_predType := mkPredType on_face.
(* Plans associés aux faces du cube (les faces sont numérotées de 0 à 5) *)
Fact Px : (1,0,0) != (0,0,0) :> R * R * R.
Fact Py : (0,1,0) != (0,0,0) :> R * R * R.
Fact Pz : (0,0,1) != (0,0,0) :> R * R * R.
Definition face_plane (f : face) :=
if f == 0%N :> nat then Plane 0 Px else
if f == 1%N :> nat then Plane 1 Px else
if f == 2%N :> nat then Plane 0 Py else
if f == 3%N :> nat then Plane 1 Py else
if f == 4%N :> nat then Plane 0 Pz else
Plane 1 Pz.
Notation "`P[ i ]" := (face_plane i).
(* Appartenir à une face s'est bien appartenir au plan correspondant *)
Lemma app_face_place p f : p \in f -> p \on `P[f].
(* Propriété clé : si on prend au moins 4 faces du cube, il y a en a au moins *)
(* deux qui sont parallèles *)
Lemma count_exist : forall (T : Type) (t : T) (a : pred T) (s : seq T),
(1 < count a s -> exists i, exists j,
[/\ i < size s, j < size s, a (nth t s i), a (nth t s j) & i != j])%N.
Lemma par_face_place n (t : n.+4.-tuple face) :
exists i, exists j, `P[tnth t i] /[p]/ `P[tnth t j] && (i != j).
(******************************************************************************)
(* POLYGONE INSCRIT *)
(******************************************************************************)
(* Notre plan de coupe *)
Variable P : plane.
(* fonction next sur les indices pour avoir la circularité *)
Definition next n : 'I_n -> 'I_n :=
if n is n1.+1 then fun i => inZp i.+1 else id.
Lemma nextE n (i : 'I_n.+2) : next i = i + 1.
(* Définition du polygone inscrit *)
Inductive ipolygon n := IPolygon (t: n.-tuple point) of
[&&
(* tous les points appartiennent au plan *)
[forall i, tnth t i \on P],
(* les points sont 2 à 2 distincts *)
[forall i, forall j, (i != j) ==> (tnth t i != tnth t j)] &
(* un point et son successeur appartiennent toujours à une face qui *)
(* n'est pas parallèle au plan de coupe *)
[forall i, exists f : face,
[&& tnth t i \in f, tnth t (next i) \in f & ~~ `P[f] /[p]/ P ]]
].
(* Fonction d'accès des points du polygone *)
Definition ipoint n (ip : ipolygon n) i :=
let: IPolygon t _ := ip in tnth t i.
(* Fonction d'accès des lignes du polygone *)
Lemma ipoint_diff n (ip : ipolygon n.+2) i : ipoint ip i != ipoint ip (next i).
Lemma ipoint_on_p n (ip : ipolygon n.+2) i : ipoint ip i \on P.
Definition iline n (ip : ipolygon n.+2) i := Line (ipoint_diff ip i).
Lemma ipoint_iline n (ip : ipolygon n.+2) i : ipoint ip i \in iline ip i.
Lemma ipoint_iline_next n (ip : ipolygon n.+2) i :
ipoint ip (next i) \in iline ip i.
Lemma iline_in_p n (ip : ipolygon n.+2) i : iline ip i \in P.
(* Tout polygone inscrit de plus de 4 points à au moins deux lignes *)
(* parallèles , on ne peut donc pas avoir de pentagone régulier! *)
Lemma ipolygon_par n (ip : ipolygon n.+4) :
exists i, exists j, iline ip i /[l]/ (iline ip j) && (i != j).
End Cube.
Require Import seq choice fintype tuple div zmodp ssralg ssrnum.
Local Open Scope ring_scope.
Import GRing.Theory.
Section Cube.
(* Comme Coq ne connait rien en géométrie on doit commencer par définir *)
(* les notions de base de géométrie *)
(* Le corps des coordonées *)
Variable R : numFieldType.
(* Pour pouvoir décider les équations sur R *)
Lemma Rsth : Setoid_Theory R (@eq R).
Global Instance Roperators:
@Ring_ops R 0%R 1%R +%R *%R (fun x y => x - y)%R -%R (@eq R).
Global Instance Rring: (@Ring _ _ _ _ _ _ _ _ Roperators).
Global Instance Rcring: (Cring (Rr:=Rring)).
(* Un petit test *)
Fact test (x y : R) : (x - y) * (x + y) = x * x - y * y.
(******************************************************************************)
(* POINT *)
(******************************************************************************)
Inductive point := Point of R & R & R.
(* On a besoin de l'égalité sur les points : p1 == p2 *)
Definition eq_point p1 p2 :=
let: Point x1 y1 z1 := p1 in
let: Point x2 y2 z2 := p2 in [&& x1 == x2, y1 == y2 & z1 == z2].
Lemma eq_pointP : Equality.axiom eq_point.
Canonical point_eqMixin := EqMixin eq_pointP.
Canonical point_eqType := Eval hnf in EqType point point_eqMixin.
(******************************************************************************)
(* LIGNE *)
(******************************************************************************)
(* Définition d'une ligne : deux points distincts *)
Inductive line := Line (p1 p2 : point) of (p1 != p2).
(* x1 / y1, x2 / y2 et z1 / z2 sont proportionnels *)
Definition proportional (x1 y1 x2 y2 x3 y3 : R) :=
[&& x1 * y2 == y1 * x2, x1 * y3 == y1 * x3 & x2 * y3 == y2 * x3].
Lemma proportionalP (x1 y1 x2 y2 x3 y3 : R) :
reflect (exists k, (x1, x2, x3) = (k * y1, k * y2, k * y3) \/
(y1, y2, y3) = (k * x1, k * x2, k * x3))
(proportional x1 y1 x2 y2 x3 y3).
Lemma proportionalNZP (x1 y1 x2 y2 x3 y3 : R) (NZ : (x1, x2, x3) != 0) :
reflect (exists k , (y1, y2, y3) = (k * x1, k * x2, k * x3))
(proportional x1 y1 x2 y2 x3 y3).
Lemma proportional_id x y z : proportional x x y y z z.
Lemma proportionalC x1 y1 x2 y2 x3 y3 :
proportional x1 y1 x2 y2 x3 y3 = proportional y1 x1 y2 x2 y3 x3.
Lemma proportional_trans x1 y1 z1 x2 y2 z2 x3 y3 z3 (PNZ : (y1, y2, y3) != 0) :
proportional x1 y1 x2 y2 x3 y3 -> proportional y1 z1 y2 z2 y3 z3 ->
proportional x1 z1 x2 z2 x3 z3.
(* Un point est sur la line : p \in l *)
Definition on_line (l : line) (p : point) :=
let: Line (Point x1 y1 z1) (Point x2 y2 z2) _ := l in
let : Point x3 y3 z3 := p in
proportional (x1 - x2) (x1 - x3) (y1 - y2) (y1 - y3) (z1 - z2) (z1 - z3).
Canonical on_line_predType := mkPredType on_line.
(* Deux lignes parallèles : l1 /l l2 *)
Definition lpar l1 l2 :=
let: Line (Point x1 y1 z1) (Point x2 y2 z2) _ := l1 in
let: Line (Point x3 y3 z3) (Point x4 y4 z4) _ := l2 in
proportional (x1 - x2) (x3 - x4) (y1 - y2) (y3 - y4) (z1 - z2) (z3 - z4).
Notation " l1 /[l]/ l2 " := (lpar l1 l2) (at level 10).
Lemma lpar_id l : l /[l]/ l.
Lemma lparC l1 l2 : l1 /[l]/ l2 = l2 /[l]/ l1.
Lemma lpar_trans l1 l2 l3 : l1 /[l]/ l2 -> l2 /[l]/ l3 -> l1 /[l]/ l3.
(******************************************************************************)
(* PLAN *)
(******************************************************************************)
Inductive plane := Plane (a b c d : R) of (a, b, c) != (0, 0, 0).
(* Pour l'appartenance d'un point à un plan: p \on P *)
Definition on_plane pl p :=
let: Point x y z := p in
let: Plane a b c d _ := pl in a * x + b * y + c * z == d.
Notation "p \on pl" := (on_plane pl p) (at level 10).
(* Deux plans parallèles : P1 /p/ P2 *)
Definition ppar p1 p2 :=
let: Plane a1 b1 c1 d1 _ := p1 in
let: Plane a2 b2 c2 d2 _ := p2 in proportional a1 a2 b1 b2 c1 c2.
Notation " p1 /[p]/ p2 " := (ppar p1 p2) (at level 10).
Lemma ppar_id p : p /[p]/ p.
Lemma pparC p1 p2 : p1 /[p]/ p2 = p2 /[p]/ p1.
Lemma ppar_trans p1 p2 p3 : p1 /[p]/ p2 -> p2 /[p]/ p3 -> p1 /[p]/ p3.
(* Appartenance d'une ligne à un plan : l \in P *)
Definition l_on_plane (pl : plane) l :=
let: Line p1 p2 _ := l in (on_plane pl p1) && (on_plane pl p2).
Canonical l_on_plane_predType := mkPredType l_on_plane.
Lemma l_on_planeE (p1 p2 : point) (L : p1 != p2) (P : plane) :
p1 \on P -> p2 \on P -> Line L \in P.
(* L'intersection d'un plan avec deux plans parallèles donne deux lignes *)
(* parallèles *)
Lemma par_2_plane (p1 p2 p3 : plane) (l1 l2 : line) :
l1 \in p1 -> l1 \in p3 -> l2 \in p2 -> l2 \in p3 ->
~~ p1 /[p]/ p3 -> p1 /[p]/ p2 -> l1 /[l]/ l2.
(******************************************************************************)
(* CUBE *)
(******************************************************************************)
(* les faces sont numérotées de 0 à 5 *)
Definition face := 'I_6.
(* Appartenance à une face du cube (les faces sont numérotées de 0 à 5) *)
Definition on_face (f : face) p :=
let: Point x y z := p in
if f == 0%N :> nat then [&& x == 0, 0 <= y <= 1 & 0 <= z <= 1] else
if f == 1%N :> nat then [&& x == 1, 0 <= y <= 1 & 0 <= z <= 1] else
if f == 2%N :> nat then [&& y == 0, 0 <= x <= 1 & 0 <= z <= 1] else
if f == 3%N :> nat then [&& y == 1, 0 <= x <= 1 & 0 <= z <= 1] else
if f == 4%N :> nat then [&& z == 0, 0 <= x <= 1 & 0 <= y <= 1] else
[&& z == 1, 0 <= x <= 1 & 0 <= y <= 1].
Canonical on_face_predType := mkPredType on_face.
(* Plans associés aux faces du cube (les faces sont numérotées de 0 à 5) *)
Fact Px : (1,0,0) != (0,0,0) :> R * R * R.
Fact Py : (0,1,0) != (0,0,0) :> R * R * R.
Fact Pz : (0,0,1) != (0,0,0) :> R * R * R.
Definition face_plane (f : face) :=
if f == 0%N :> nat then Plane 0 Px else
if f == 1%N :> nat then Plane 1 Px else
if f == 2%N :> nat then Plane 0 Py else
if f == 3%N :> nat then Plane 1 Py else
if f == 4%N :> nat then Plane 0 Pz else
Plane 1 Pz.
Notation "`P[ i ]" := (face_plane i).
(* Appartenir à une face s'est bien appartenir au plan correspondant *)
Lemma app_face_place p f : p \in f -> p \on `P[f].
(* Propriété clé : si on prend au moins 4 faces du cube, il y a en a au moins *)
(* deux qui sont parallèles *)
Lemma count_exist : forall (T : Type) (t : T) (a : pred T) (s : seq T),
(1 < count a s -> exists i, exists j,
[/\ i < size s, j < size s, a (nth t s i), a (nth t s j) & i != j])%N.
Lemma par_face_place n (t : n.+4.-tuple face) :
exists i, exists j, `P[tnth t i] /[p]/ `P[tnth t j] && (i != j).
(******************************************************************************)
(* POLYGONE INSCRIT *)
(******************************************************************************)
(* Notre plan de coupe *)
Variable P : plane.
(* fonction next sur les indices pour avoir la circularité *)
Definition next n : 'I_n -> 'I_n :=
if n is n1.+1 then fun i => inZp i.+1 else id.
Lemma nextE n (i : 'I_n.+2) : next i = i + 1.
(* Définition du polygone inscrit *)
Inductive ipolygon n := IPolygon (t: n.-tuple point) of
[&&
(* tous les points appartiennent au plan *)
[forall i, tnth t i \on P],
(* les points sont 2 à 2 distincts *)
[forall i, forall j, (i != j) ==> (tnth t i != tnth t j)] &
(* un point et son successeur appartiennent toujours à une face qui *)
(* n'est pas parallèle au plan de coupe *)
[forall i, exists f : face,
[&& tnth t i \in f, tnth t (next i) \in f & ~~ `P[f] /[p]/ P ]]
].
(* Fonction d'accès des points du polygone *)
Definition ipoint n (ip : ipolygon n) i :=
let: IPolygon t _ := ip in tnth t i.
(* Fonction d'accès des lignes du polygone *)
Lemma ipoint_diff n (ip : ipolygon n.+2) i : ipoint ip i != ipoint ip (next i).
Lemma ipoint_on_p n (ip : ipolygon n.+2) i : ipoint ip i \on P.
Definition iline n (ip : ipolygon n.+2) i := Line (ipoint_diff ip i).
Lemma ipoint_iline n (ip : ipolygon n.+2) i : ipoint ip i \in iline ip i.
Lemma ipoint_iline_next n (ip : ipolygon n.+2) i :
ipoint ip (next i) \in iline ip i.
Lemma iline_in_p n (ip : ipolygon n.+2) i : iline ip i \in P.
(* Tout polygone inscrit de plus de 4 points à au moins deux lignes *)
(* parallèles , on ne peut donc pas avoir de pentagone régulier! *)
Lemma ipolygon_par n (ip : ipolygon n.+4) :
exists i, exists j, iline ip i /[l]/ (iline ip j) && (i != j).
End Cube.
This page has been generated by coqdoc