From: Claudio Sacerdoti Coen Date: Wed, 23 May 2007 13:28:22 +0000 (+0000) Subject: Automatic exploration of the theory of intuitionistic interior, closure and X-Git-Tag: make_still_working~6325 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=99ca90bf28a25fcd1cd84596c37be43c97f74e6e;p=helm.git Automatic exploration of the theory of intuitionistic interior, closure and complement. --- diff --git a/helm/software/matita/contribs/formal_topology/bin/Makefile b/helm/software/matita/contribs/formal_topology/bin/Makefile new file mode 100644 index 000000000..b02798067 --- /dev/null +++ b/helm/software/matita/contribs/formal_topology/bin/Makefile @@ -0,0 +1,2 @@ +theory_explorer: theory_explorer.ml + ocamlc -g -rectypes -o theory_explorer unix.cma theory_explorer.ml diff --git a/helm/software/matita/contribs/formal_topology/bin/formal_topology.ma b/helm/software/matita/contribs/formal_topology/bin/formal_topology.ma new file mode 100644 index 000000000..54c5a2a0b --- /dev/null +++ b/helm/software/matita/contribs/formal_topology/bin/formal_topology.ma @@ -0,0 +1,57 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/formal_topologyxxx2/". +include "logic/equality.ma". + +axiom S: Type. + +axiom leq: S → S → Prop. + +notation "hvbox(A break ⊆ B)" with precedence 59 +for @{ 'subseteq $A $B}. + +interpretation "Subseteq" 'subseteq A B = + (cic:/matita/formal_topologyxxx2/leq.con A B). + +axiom leq_refl: ∀A. A ⊆ A. +axiom leq_antisym: ∀A,B. A ⊆ B → B ⊆ A → A=B. +axiom leq_tran: ∀A,B,C. A ⊆ B → B ⊆ C → A ⊆ C. + +axiom i: S → S. + +axiom i_contrattivita: ∀A. i A ⊆ A. +axiom i_idempotenza: ∀A. i (i A) = i A. +axiom i_monotonia: ∀A,B. A ⊆ B → i A ⊆ i B. + +axiom c: S → S. + +axiom c_espansivita: ∀A. A ⊆ c A. +axiom c_idempotenza: ∀A. c (c A) = c A. +axiom c_monotonia: ∀A,B. A ⊆ B → c A ⊆ c B. + +axiom m: S → S. + +axiom m_antimonotonia: ∀A,B. A ⊆ B → m B ⊆ m A. +axiom m_saturazione: ∀A. A ⊆ m (m A). +axiom m_puntofisso: ∀A. m A = m (m (m A)). + +lemma l1: ∀A,B. i A ⊆ B → i A ⊆ i B. intros; rewrite < i_idempotenza; auto. qed. +lemma l2: ∀A,B. A ⊆ c B → c A ⊆ c B. intros; rewrite < c_idempotenza in ⊢ (? ? %); auto. qed. + +axiom th1: ∀A. c (m A) ⊆ m (i A). +axiom th2: ∀A. i (m A) ⊆ m (c A). + +(************** start of generated part *********************) + diff --git a/helm/software/matita/contribs/formal_topology/bin/theory_explorer.ml b/helm/software/matita/contribs/formal_topology/bin/theory_explorer.ml new file mode 100644 index 000000000..be1e107fb --- /dev/null +++ b/helm/software/matita/contribs/formal_topology/bin/theory_explorer.ml @@ -0,0 +1,195 @@ +(* operator *) +type op = I | C | M + +let string_of_op = + function + I -> "i" + | C -> "c" + | M -> "-" + +(* compound operator *) +type compound_operator = op list + +let string_of_cop op = + if op = [] then "id" else String.concat "" (List.map string_of_op op) + +let rec matita_of_cop v = + function + | [] -> v + | I::tl -> "i (" ^ matita_of_cop v tl ^ ")" + | C::tl -> "c (" ^ matita_of_cop v tl ^ ")" + | M::tl -> "m (" ^ matita_of_cop v tl ^ ")" + +(* representative, other elements in the equivalence class, + leq classes, geq classes *) +type equivalence_class = + compound_operator * compound_operator list * + equivalence_class list ref * equivalence_class list ref + +let string_of_equivalence_class (repr,others,leq,_) = + String.concat " = " (List.map string_of_cop (repr::others)) ^ + (if !leq <> [] then + "\n" ^ + String.concat "\n" + (List.map + (function (repr',_,_,_) -> + string_of_cop repr ^ " <= " ^ string_of_cop repr') !leq) + else + "") + +let dot_of_equivalence_class (repr,others,leq,_) = + (if others <> [] then + let eq = String.concat " = " (List.map string_of_cop (repr::others)) in + string_of_cop repr ^ "[label=\"" ^ eq ^ "\"];\n" + else "") ^ + String.concat "\n" + (List.map + (function (repr',_,_,_) -> + string_of_cop repr' ^ " -> " ^ string_of_cop repr ^ ";") !leq) + +(* set of equivalence classes *) +type set = equivalence_class list + +let string_of_set s = + String.concat "\n" (List.map string_of_equivalence_class s) + +let ps_of_set ?processing s = + let ch = open_out "xxx.dot" in + output_string ch "digraph G {\n"; + output_string ch (String.concat "\n" (List.map dot_of_equivalence_class s)); + (match processing with + None -> () + | Some (repr,rel,repr') -> + output_string ch + (string_of_cop repr' ^ " -> " ^ string_of_cop repr ^ + " [" ^ + (if rel="=" then "arrowhead=none " else "") ^ + "style=dashed];\n")); + output_string ch "}\n"; + close_out ch; + ignore (Unix.system "dot -Tps xxx.dot > xxx.ps") + +let test set rel candidate repr = + ps_of_set ~processing:(candidate,rel,repr) set; + print_string + (string_of_cop candidate ^ " " ^ rel ^ " " ^ string_of_cop repr ^ "? "); + flush stdout; + assert (Unix.system "cp formal_topology.ma xxx.ma" = Unix.WEXITED 0); + let ch = open_out_gen [Open_append] 0 "xxx.ma" in + let i = ref 0 in + List.iter + (function (repr,others,leq,_) -> + List.iter + (function repr' -> + incr i; + output_string ch + ("axiom ax" ^ string_of_int !i ^ + ": \\forall A." ^ + matita_of_cop "A" repr ^ " = " ^ matita_of_cop "A" repr' ^ ".\n"); + ) others; + List.iter + (function (repr',_,_,_) -> + incr i; + output_string ch + ("axiom ax" ^ string_of_int !i ^ + ": \\forall A." ^ + matita_of_cop "A" repr ^ " ⊆ " ^ matita_of_cop "A" repr' ^ ".\n"); + ) !leq; + ) set; + output_string ch + ("theorem foo: \\forall A." ^ matita_of_cop "A" candidate ^ " " ^ rel ^ " " ^ + matita_of_cop "A" repr ^ ". intros; auto size=6 depth=4. qed.\n"); + close_out ch; + let res = + Unix.system "../../../matitac.opt xxx.ma >> log 2>&1" = Unix.WEXITED 0 + in + print_endline (if res then "y" else "n"); + res + +let normalize candidate set = + let rec aux = + function + [] -> raise Not_found + | (repr,others,leq,geq) as eqclass :: tl -> + if test set "=" candidate repr then + (repr,others@[candidate],leq,geq)::tl + else + eqclass::(aux tl) + in + aux set +;; + +let locate ((repr,_,leq,geq) as node) set = + let rec aux = + function + [] -> () + | (repr',_,leq',geq') as node' :: tl -> + if repr = repr' then () + else if test set "⊆" repr repr' then + begin + leq := node' :: !leq; + geq' := node :: !geq' + end + else if test set "⊆" repr' repr then + begin + geq := node' :: !geq; + leq' := node :: !leq' + end ; + aux tl + in + aux set +;; + +let analyze_one i repr hecandidate (news,set) = + let candidate = hecandidate::repr in + if List.length (List.filter ((=) M) candidate) > i then + news,set + else + try + let set = normalize candidate set in + news,set + with + Not_found -> + let leq = ref [] in + let geq = ref [] in + let node = candidate,[],leq,geq in + let set = node::set in + locate node set; + candidate::news,set +;; + +let rec explore i j set news = + let rec aux news set = + function + [] -> news,set + | repr::tl -> + let news,set = + List.fold_right (analyze_one i repr) [I;C;M] (news,set) + in + aux news set tl + in + let news,set = aux [] set news in + if news = [] then + begin + print_endline ("PUNTO FISSO RAGGIUNTO! i=" ^ string_of_int i ^ " j=" ^ string_of_int j); + print_endline (string_of_set set ^ "\n----------------"); + if i < 2 then + explore (i+1) 1 set (List.map (function (repr,_,_,_) -> repr) set) + else + ps_of_set set + end + else + begin + print_endline ("NUOVA ITERAZIONE, i=" ^ string_of_int i ^ " j=" ^ string_of_int j); + print_endline (string_of_set set ^ "\n----------------"); + explore i (j+1) set news + end +in + let id = [] in + let set = [id,[],ref [], ref []] in + print_endline ("PRIMA ITERAZIONE, i=0, j=0"); + print_endline (string_of_set set ^ "\n----------------"); + ignore (Unix.system "rm -f log"); + ps_of_set set; + explore 0 1 set [id] +;; diff --git a/helm/software/matita/contribs/formal_topology/formal_topology.ma b/helm/software/matita/contribs/formal_topology/formal_topology.ma new file mode 100644 index 000000000..89ab9484c --- /dev/null +++ b/helm/software/matita/contribs/formal_topology/formal_topology.ma @@ -0,0 +1,114 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/formal_topology/". +include "logic/equality.ma". + +axiom S: Type. + +axiom leq: S → S → Prop. + +notation "hvbox(A break ⊆ B)" with precedence 59 +for @{ 'subseteq $A $B}. + +interpretation "Subseteq" 'subseteq A B = + (cic:/matita/formal_topology/leq.con A B). + +axiom leq_refl: ∀A. A ⊆ A. +axiom leq_antisym: ∀A,B. A ⊆ B → B ⊆ A → A=B. +axiom leq_tran: ∀A,B,C. A ⊆ B → B ⊆ C → A ⊆ C. + +axiom i: S → S. + +axiom i_contrattivita: ∀A. i A ⊆ A. +axiom i_idempotenza: ∀A. i (i A) = i A. +axiom i_monotonia: ∀A,B. A ⊆ B → i A ⊆ i B. + +axiom c: S → S. + +axiom c_espansivita: ∀A. A ⊆ c A. +axiom c_idempotenza: ∀A. c (c A) = c A. +axiom c_monotonia: ∀A,B. A ⊆ B → c A ⊆ c B. + +axiom m: S → S. + +axiom m_antimonotonia: ∀A,B. A ⊆ B → m B ⊆ m A. +axiom m_saturazione: ∀A. A ⊆ m (m A). +axiom m_puntofisso: ∀A. m A = m (m (m A)). + +lemma l1: ∀A,B. i A ⊆ B → i A ⊆ i B. intros; rewrite < i_idempotenza; auto. qed. +lemma l2: ∀A,B. A ⊆ c B → c A ⊆ c B. intros; rewrite < c_idempotenza in ⊢ (? ? %); auto. qed. + +theorem geq1: ∀A. i (i A) = i A. intros. auto. qed. +theorem geq2: ∀A. c (c A) = c A. intros. auto. qed. +theorem geq3: ∀A. i (i (c A)) = i (c A). intros. auto. qed. +theorem geq4: ∀A. c (c (i A)) = c (i A). intros. auto. qed. +theorem geq5: ∀A. i (c (i (c A))) = i (c A). intros. auto depth=4. qed. +theorem geq6: ∀A. c (i (c (i A))) = c (i A). intros. auto depth=4. qed. +theorem gse1: ∀A. i A ⊆ A. intros. auto. qed. +theorem gse2: ∀A. A ⊆ c A. intros. auto. qed. +theorem gse3: ∀A. i A ⊆ i (c (i A)). intros. auto. qed. +theorem gse4: ∀A. i (c (i A)) ⊆ i (c A). intros. auto. qed. +theorem gse5: ∀A. i (c (i A)) ⊆ c (i A). intros. auto. qed. +theorem gse6: ∀A. i (c A) ⊆ c (i (c A)). intros. auto. qed. +theorem gse7: ∀A. c (i A) ⊆ c (i (c A)). intros. auto. qed. +theorem gse8: ∀A. c (i (c A)) ⊆ c A. intros. auto. qed. + +axiom th1: ∀A. c (m A) ⊆ m (i A). +axiom th2: ∀A. i (m A) ⊆ m (c A). + +theorem se1: ∀A. i (c (m (c A))) ⊆ i (m (i (c A))). intros; auto. qed. +theorem se2: ∀A. i (m (i (c A))) ⊆ m (c (i (c A))). intros; auto. qed. +theorem se3: ∀A. c (i (m A)) ⊆ c (i (c (m (c A)))). intros; auto depth=4. qed. +theorem se4: ∀A. c (i (c (m (c A)))) ⊆ c (i (m (i (c A)))). intros; auto. qed. +theorem se5: ∀A. i (c (m (c A))) ⊆ c (i (c (m (c A)))). intros; auto. qed. +theorem se6: ∀A. i (m (i (c A))) ⊆ c (i (m (i (c A)))). intros; auto. qed. +theorem se7: ∀A. m (c A) ⊆ m A. intros; auto. qed. +theorem se8: ∀A. i (c (m (c A))) ⊆ i (c (m A)). intros; auto. qed. +theorem se9: ∀A. i (c (m A)) ⊆ i (m (i A)). intros; auto. qed. +theorem se10: ∀A. i (m (i (c A))) ⊆ i (m (i A)). intros; auto depth=4. qed. +theorem se11: ∀A. i (m (i A)) ⊆ m (c (i A)). intros; auto. qed. +theorem se12: ∀A. m (c (i (c A))) ⊆ m (c (i A)). intros; auto. qed. +theorem se13: ∀A. m (c A) ⊆ m (c (i (c A))). intros; auto. qed. +theorem se14: ∀A. i (c (m A)) ⊆ c (i (c (m A))). intros; auto. qed. +theorem se15: ∀A. c (i (c (m A))) ⊆ c (m A). intros; auto. qed. +theorem se16: ∀A. c (i (m (i A))) ⊆ c (m (c (i A))). intros; auto depth=4. qed. +theorem se17: ∀A. c (m (c (i A))) ⊆ m (i (c (i A))). intros; auto. qed. +theorem se18: ∀A. m (i (c A)) ⊆ m (i (c (i A))). intros; auto. qed. +theorem se19: ∀A. m (i (c (i A))) ⊆ m (i A). intros; auto. qed. +theorem se20: ∀A. c (m (c A)) ⊆ c (m A). intros; auto. qed. +theorem se21: ∀A. c (m (c A)) ⊆ c (m (c (i (c A)))). intros; auto. qed. +theorem se22: ∀A. c (m (c (i (c A)))) ⊆ m (i (c A)). intros; auto. qed. +theorem se23: ∀A. c (i (c (m (c A)))) ⊆ c (i (c (m A))). intros; auto. qed. +theorem se24: ∀A. c (i (c (m (c A)))) ⊆ c (m (c A)). intros; auto. qed. +theorem se25: ∀A. m (c A) ⊆ c (m (c A)). intros; auto. qed. +theorem se26: ∀A. c (i (m (i (c A)))) ⊆ c (i (m (c (i (c A))))). intros; auto. qed. +theorem se27: ∀A. m (c (i (c A))) ⊆ c (m (c (i (c A)))). intros; auto. qed. +theorem se28: ∀A. m (c (i A)) ⊆ c (m (c (i A))). intros; auto. qed. +theorem se29: ∀A. m A ⊆ c (m A). intros; auto. qed. +theorem se30: ∀A. i (m A) ⊆ i (c (i (m A))). intros; auto. qed. +theorem se31: ∀A. i (c (i (m A))) ⊆ c (i (m A)). intros; auto. qed. +theorem se32: ∀A. i (c (i (m A))) ⊆ i (c (m (c A))). intros; auto. qed. +theorem se33: ∀A. c (i (c (m A))) ⊆ c (i (m (i A))). intros; auto. qed. +theorem se34: ∀A. i (m (i A)) ⊆ c (i (m (i A))). intros; auto. qed. +theorem se35: ∀A. c (i (m (i (c A)))) ⊆ c (i (m (i A))). intros; auto. qed. +theorem se36: ∀A. c (m (c (i (c A)))) ⊆ c (m (c (i A))). intros; auto. qed. + +theorem th5: ∀A. i (m (c A)) = i (m A). intros; auto depth=4. qed. +theorem th6: ∀A. c (m (i A)) = m (i A). intros; auto width=2 depth=5. qed. +theorem th7: ∀A. i (m (i A)) = i (c (i (m (i A)))). intros; auto. qed. +theorem th8: ∀A. i (m (i A)) = i (m (i (c (i A)))). intros; auto. qed. +theorem th9: ∀A. i (c (m (c (i A)))) = i (m (i A)). intros; auto depth=4. qed. + +(* theorem th7: ∀A. i (m (i A)) = i (s (i A)). *) \ No newline at end of file diff --git a/helm/software/matita/contribs/formal_topology/formal_topology2.ma b/helm/software/matita/contribs/formal_topology/formal_topology2.ma new file mode 100644 index 000000000..b98865a5c --- /dev/null +++ b/helm/software/matita/contribs/formal_topology/formal_topology2.ma @@ -0,0 +1,77 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/formal_topology/". +include "logic/equality.ma". + +axiom S: Type. + +axiom comp: S → S → S. +coercion cic:/matita/formal_topology/comp.con 1. + +axiom comp_assoc: ∀A,B,C:S. A (B C) = (A B) C. + +axiom one: S. + +notation "1" with precedence 89 +for @{ 'unit }. + +interpretation "Unit" 'unit = + cic:/matita/formal_topology/one.con. + +axiom one_left: ∀A. 1 A = A. +axiom one_right: ∀A:S. A 1 = A. + +axiom eps: S. +axiom eps_idempotent: eps = eps eps. + +notation "hvbox(A break ⊆ B)" with precedence 59 +for @{ 'subseteq $A $B}. + +interpretation "Subseteq" 'subseteq A B = + (cic:/matita/logic/equality/eq.ind#xpointer(1/1) _ A + (cic:/matita/formal_topology/comp.con + cic:/matita/formal_topology/eps.con B)). + +axiom leq_refl: ∀A. A ⊆ A. +axiom leq_antisym: ∀A,B. A ⊆ B → B ⊆ A → A=B. +axiom leq_tran: ∀A,B,C. A ⊆ B → B ⊆ C → A ⊆ C. + +axiom i: S. + +axiom i_contrattivita: i ⊆ 1. +axiom i_idempotenza: i i = i. +axiom i_monotonia: ∀A,B. A ⊆ B → i A ⊆ i B. + +axiom c: S. + +axiom c_espansivita: 1 ⊆ c. +axiom c_idempotenza: c c = c. +axiom c_monotonia: ∀A,B. A ⊆ B → c A ⊆ c B. + +axiom m: S. + +axiom m_antimonotonia: ∀A,B. A ⊆ B → m B ⊆ m A. +axiom m_saturazione: 1 ⊆ m m. +axiom m_puntofisso: m = m (m m). + +theorem th1: c m ⊆ m i. intros; auto. qed. +theorem th2: ∀A. i (m A) ⊆ (m (c A)). intros; auto. qed. +theorem th3: ∀A. i A ⊆ (m (c (m A))). intros; auto. qed. +theorem th4: ∀A. c A ⊆ (m (i (m A))). intros; auto. qed. + +theorem th5: ∀A. i (m A) = i (m (c A)). intros; auto. qed. +theorem th6: ∀A. m (i A) = c (m (i A)). intros; auto. qed. + +theorem th7: ∀A. i (m (i A)) = i (s (i A)). \ No newline at end of file