(* ========================================================================= *)
(* Mizar Light proof of duality in projective geometry.                      *)
(* ========================================================================= *)

let holby_prover =
  fun ths (asl,w as gl) -> ACCEPT_TAC(HOL_BY ths w) gl;;

current_prover := holby_prover;;

(* ------------------------------------------------------------------------- *)
(* To avoid adding any axioms, pick a simple model: the Fano plane.          *)
(* ------------------------------------------------------------------------- *)

let Line_INDUCT,Line_RECURSION = define_type
 "Line = Line_1 | Line_2 | Line_3 | Line_4 |
         Line_5 | Line_6 | Line_7";
;
let Point_INDUCT,Point_RECURSION = define_type
 "Point = Point_1 | Point_2 | Point_3 | Point_4 |
          Point_5 | Point_6 | Point_7";
; let Point_DISTINCT = distinctness "Point";; let Line_DISTINCT = distinctness "Line";; let fano_incidence = [1,1; 1,2; 1,3; 2,1; 2,4; 2,5; 3,1; 3,6; 3,7; 4,2; 4,4; 4,6; 5,2; 5,5; 5,7; 6,3; 6,4; 6,7; 7,3; 7,5; 7,6];; let fano_point i = mk_const("Point_"^string_of_int i,[]) and fano_line i = mk_const("Line_"^string_of_int i,[]);; let p = `p:Point` and l = `l:Line` ;; let fano_clause (i,j) = mk_conj(mk_eq(p,fano_point i),mk_eq(l,fano_line j));; (* ------------------------------------------------------------------------- *) (* Define the incidence relation "ON" from "fano_incidence" *) (* ------------------------------------------------------------------------- *) parse_as_infix("ON",(11,"right"));;
let ON = new_definition
 `(p:Point) ON (l:Line) <=>
        (p = Point_1 /\ l = Line_1) \/
        (p = Point_1 /\ l = Line_2) \/
        (p = Point_1 /\ l = Line_3) \/
        (p = Point_2 /\ l = Line_1) \/
        (p = Point_2 /\ l = Line_4) \/
        (p = Point_2 /\ l = Line_5) \/
        (p = Point_3 /\ l = Line_1) \/
        (p = Point_3 /\ l = Line_6) \/
        (p = Point_3 /\ l = Line_7) \/
        (p = Point_4 /\ l = Line_2) \/
        (p = Point_4 /\ l = Line_4) \/
        (p = Point_4 /\ l = Line_6) \/
        (p = Point_5 /\ l = Line_2) \/
        (p = Point_5 /\ l = Line_5) \/
        (p = Point_5 /\ l = Line_7) \/
        (p = Point_6 /\ l = Line_3) \/
        (p = Point_6 /\ l = Line_4) \/
        (p = Point_6 /\ l = Line_7) \/
        (p = Point_7 /\ l = Line_3) \/
        (p = Point_7 /\ l = Line_5) \/
        (p = Point_7 /\ l = Line_6)`;;
(* ------------------------------------------------------------------------- *) (* Also produce a more convenient case-by-case rewrite. *) (* ------------------------------------------------------------------------- *)
let ON_CLAUSES = 
prove (`(Point_1 ON Line_1 <=> T) /\ (Point_1 ON Line_2 <=> T) /\ (Point_1 ON Line_3 <=> T) /\ (Point_1 ON Line_4 <=> F) /\ (Point_1 ON Line_5 <=> F) /\ (Point_1 ON Line_6 <=> F) /\ (Point_1 ON Line_7 <=> F) /\ (Point_2 ON Line_1 <=> T) /\ (Point_2 ON Line_2 <=> F) /\ (Point_2 ON Line_3 <=> F) /\ (Point_2 ON Line_4 <=> T) /\ (Point_2 ON Line_5 <=> T) /\ (Point_2 ON Line_6 <=> F) /\ (Point_2 ON Line_7 <=> F) /\ (Point_3 ON Line_1 <=> T) /\ (Point_3 ON Line_2 <=> F) /\ (Point_3 ON Line_3 <=> F) /\ (Point_3 ON Line_4 <=> F) /\ (Point_3 ON Line_5 <=> F) /\ (Point_3 ON Line_6 <=> T) /\ (Point_3 ON Line_7 <=> T) /\ (Point_4 ON Line_1 <=> F) /\ (Point_4 ON Line_2 <=> T) /\ (Point_4 ON Line_3 <=> F) /\ (Point_4 ON Line_4 <=> T) /\ (Point_4 ON Line_5 <=> F) /\ (Point_4 ON Line_6 <=> T) /\ (Point_4 ON Line_7 <=> F) /\ (Point_5 ON Line_1 <=> F) /\ (Point_5 ON Line_2 <=> T) /\ (Point_5 ON Line_3 <=> F) /\ (Point_5 ON Line_4 <=> F) /\ (Point_5 ON Line_5 <=> T) /\ (Point_5 ON Line_6 <=> F) /\ (Point_5 ON Line_7 <=> T) /\ (Point_6 ON Line_1 <=> F) /\ (Point_6 ON Line_2 <=> F) /\ (Point_6 ON Line_3 <=> T) /\ (Point_6 ON Line_4 <=> T) /\ (Point_6 ON Line_5 <=> F) /\ (Point_6 ON Line_6 <=> F) /\ (Point_6 ON Line_7 <=> T) /\ (Point_7 ON Line_1 <=> F) /\ (Point_7 ON Line_2 <=> F) /\ (Point_7 ON Line_3 <=> T) /\ (Point_7 ON Line_4 <=> F) /\ (Point_7 ON Line_5 <=> T) /\ (Point_7 ON Line_6 <=> T) /\ (Point_7 ON Line_7 <=> F)`,
REWRITE_TAC[ON; Line_DISTINCT; Point_DISTINCT]);;
(* ------------------------------------------------------------------------- *) (* Case analysis theorems. *) (* ------------------------------------------------------------------------- *)
let FORALL_POINT = 
prove (`(!p. P p) <=> P Point_1 /\ P Point_2 /\ P Point_3 /\ P Point_4 /\ P Point_5 /\ P Point_6 /\ P Point_7`,
EQ_TAC THEN REWRITE_TAC[Point_INDUCT] THEN SIMP_TAC[]);;
let EXISTS_POINT = 
prove (`(?p. P p) <=> P Point_1 \/ P Point_2 \/ P Point_3 \/ P Point_4 \/ P Point_5 \/ P Point_6 \/ P Point_7`,
MATCH_MP_TAC(TAUT `(~p <=> ~q) ==> (p <=> q)`) THEN REWRITE_TAC[DE_MORGAN_THM; NOT_EXISTS_THM; FORALL_POINT]);;
let FORALL_LINE = 
prove (`(!p. P p) <=> P Line_1 /\ P Line_2 /\ P Line_3 /\ P Line_4 /\ P Line_5 /\ P Line_6 /\ P Line_7`,
EQ_TAC THEN REWRITE_TAC[Line_INDUCT] THEN SIMP_TAC[]);;
let EXISTS_LINE = 
prove (`(?p. P p) <=> P Line_1 \/ P Line_2 \/ P Line_3 \/ P Line_4 \/ P Line_5 \/ P Line_6 \/ P Line_7`,
MATCH_MP_TAC(TAUT `(~p <=> ~q) ==> (p <=> q)`) THEN REWRITE_TAC[DE_MORGAN_THM; NOT_EXISTS_THM; FORALL_LINE]);;
(* ------------------------------------------------------------------------- *) (* Hence prove the axioms by a naive case split (a bit slow but easy). *) (* ------------------------------------------------------------------------- *) let FANO_TAC = GEN_REWRITE_TAC DEPTH_CONV [FORALL_POINT; EXISTS_LINE; EXISTS_POINT; FORALL_LINE] THEN GEN_REWRITE_TAC DEPTH_CONV (basic_rewrites() @ [ON_CLAUSES; Point_DISTINCT; Line_DISTINCT]);; let AXIOM_1 = time prove (`!p p'. ~(p = p') ==> ?l. p ON l /\ p' ON l /\ !l'. p ON l' /\ p' ON l' ==> (l' = l)`, FANO_TAC);; let AXIOM_2 = time prove (`!l l'. ?p. p ON l /\ p ON l'`, FANO_TAC);; let AXIOM_3 = time prove (`?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\ ~(?l. p ON l /\ p' ON l /\ p'' ON l)`, FANO_TAC);; let AXIOM_4 = time prove (`!l. ?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\ p ON l /\ p' ON l /\ p'' ON l`, FANO_TAC);; (* ------------------------------------------------------------------------- *) (* Now the interesting bit. *) (* ------------------------------------------------------------------------- *) let AXIOM_1' = theorem "!p p' l l'. ~(p = p') /\\ p ON l /\\ p' ON l /\\ p ON l' /\\ p' ON l' ==> (l' = l)" [fix ["p:Point"; "p':Point"; "l:Line"; "l':Line"]; assume "~(p = p') /\\ p ON l /\\ p' ON l /\\ p ON l' /\\ p' ON l'" at 1; consider ["l1:Line"] st "p ON l1 /\\ p' ON l1 /\\ !l'. p ON l' /\\ p' ON l' ==> (l' = l1)" from [1] by [AXIOM_1] at 2; have "l = l1" from [1;2]; so have "... = l'" from [1;2]; qed];; let LEMMA_1 = theorem "!O. ?l. O ON l" [consider ["p:Point"; "p':Point"; "p'':Point"] st "~(p = p') /\\ ~(p' = p'') /\\ ~(p = p'') /\\ ~(?l. p ON l /\\ p' ON l /\\ p'' ON l)" by [AXIOM_3] at 1; fix ["O:Point"]; have "~(p = O) \/ ~(p' = O)" from [1]; so consider ["P:Point"] st "~(P = O)" at 2; consider ["l:Line"] st "O ON l /\\ P ON l /\\ !l'. O ON l' /\\ P ON l' ==> (l' = l)" from [2] by [AXIOM_1] at 3; thus "?l. O ON l" from [3]];; let DUAL_1 = theorem "!l l'. ~(l = l') ==> ?p. p ON l /\\ p ON l' /\\ !p'. p' ON l /\\ p' ON l' ==> (p' = p)" [otherwise consider ["l:Line"; "l':Line"] st "~(l = l') /\\ !p. p ON l /\\ p ON l' ==> ?p'. p' ON l /\\ p' ON l' /\\ ~(p' = p)" at 1; consider ["p:Point"] st "p ON l /\\ p ON l'" by [AXIOM_2] at 2; consider ["p':Point"] st "p' ON l /\\ p' ON l' /\\ ~(p' = p)" from [1;2] at 3; hence contradiction from [1;2] by [AXIOM_1']];; let DUAL_2 = theorem "!p p'. ?l. p ON l /\\ p' ON l" [fix ["p:Point"; "p':Point"]; have "?l. p ON l" by [LEMMA_1] at 1; have "(p = p') \/ ?l. p ON l /\\ p' ON l /\\ !l'. p ON l' /\\ p' ON l' ==> (l' = l)" by [AXIOM_1]; hence thesis from [1]];; let DUAL_3 = theorem "?l1 l2 l3. ~(l1 = l2) /\\ ~(l2 = l3) /\\ ~(l1 = l3) /\\ ~(?p. p ON l1 /\\ p ON l2 /\\ p ON l3)" [consider ["p1:Point"; "p2:Point"; "p3:Point"] st "~(p1 = p2) /\\ ~(p2 = p3) /\\ ~(p1 = p3) /\\ ~(?l. p1 ON l /\\ p2 ON l /\\ p3 ON l)" by [AXIOM_3] at 1; consider ["l1:Line"] st "p1 ON l1 /\\ p3 ON l1" by [DUAL_2] at 2; consider ["l2:Line"] st "p2 ON l2 /\\ p3 ON l2" by [DUAL_2] at 3; consider ["l3:Line"] st "p1 ON l3 /\\ p2 ON l3" by [DUAL_2] at 4; take ["l1"; "l2"; "l3"]; thus "~(l1 = l2) /\\ ~(l2 = l3) /\\ ~(l1 = l3)" from [1;2;3;4] at 5; otherwise consider ["q:Point"] st "q ON l1 /\\ q ON l2 /\\ q ON l3" at 6; consider ["q':Point"] st "q' ON l1 /\\ q' ON l3 /\\ !p'. p' ON l1 /\\ p' ON l3 ==> (p' = q')" from [5] by [DUAL_1] at 7; have "q = q'" from [6;7]; so have "... = p1" from [2;4;7]; hence contradiction from [1;3;6]];; let DUAL_4 = theorem "!O. ?OP OQ OR. ~(OP = OQ) /\\ ~(OQ = OR) /\\ ~(OP = OR) /\\ O ON OP /\\ O ON OQ /\\ O ON OR" [fix ["O:Point"]; consider ["OP:Line"] st "O ON OP" by [LEMMA_1] at 1; consider ["p:Point"; "p':Point"; "p'':Point"] st "~(p = p') /\\ ~(p' = p'') /\\ ~(p = p'') /\\ p ON OP /\\ p' ON OP /\\ p'' ON OP" by [AXIOM_4] at 2; have "~(p = O) \/ ~(p' = O)" from [2]; so consider ["P:Point"] st "~(P = O) /\\ P ON OP" from [2] at 3; consider ["q:Point"; "q':Point"; "q'':Point"] st "~(q = q') /\\ ~(q' = q'') /\\ ~(q = q'') /\\ ~(?l. q ON l /\\ q' ON l /\\ q'' ON l)" by [AXIOM_3] at 4; have "~(q ON OP) \/ ~(q' ON OP) \/ ~(q'' ON OP)" from [4]; so consider ["Q:Point"] st "~(Q ON OP)" at 5; consider ["l:Line"] st "P ON l /\\ Q ON l" by [DUAL_2] at 6; consider ["r:Point"; "r':Point"; "r'':Point"] st "~(r = r') /\\ ~(r' = r'') /\\ ~(r = r'') /\\ r ON l /\\ r' ON l /\\ r'' ON l" by [AXIOM_4] at 7; have "((r = P) \/ (r = Q) \/ ~(r = P) /\\ ~(r = Q)) /\\ ((r' = P) \/ (r' = Q) \/ ~(r' = P) /\\ ~(r' = Q))"; so consider ["R:Point"] st "R ON l /\\ ~(R = P) /\\ ~(R = Q)" from [7] at 8; consider ["OQ:Line"] st "O ON OQ /\\ Q ON OQ" by [DUAL_2] at 9; consider ["OR:Line"] st "O ON OR /\\ R ON OR" by [DUAL_2] at 10; take ["OP"; "OQ"; "OR"]; have "~(O ON l)" from [1;3;5;6] by [AXIOM_1']; hence "~(OP = OQ) /\\ ~(OQ = OR) /\\ ~(OP = OR) /\\ O ON OP /\\ O ON OQ /\\ O ON OR" from [1;3;5;6;8;9;10] by [AXIOM_1']];;