]> matita.cs.unibo.it Git - helm.git/commitdiff
Automatic exploration of the theory of intuitionistic interior, closure and
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 23 May 2007 13:28:22 +0000 (13:28 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 23 May 2007 13:28:22 +0000 (13:28 +0000)
complement.

helm/software/matita/contribs/formal_topology/bin/Makefile [new file with mode: 0644]
helm/software/matita/contribs/formal_topology/bin/formal_topology.ma [new file with mode: 0644]
helm/software/matita/contribs/formal_topology/bin/theory_explorer.ml [new file with mode: 0644]
helm/software/matita/contribs/formal_topology/formal_topology.ma [new file with mode: 0644]
helm/software/matita/contribs/formal_topology/formal_topology2.ma [new file with mode: 0644]

diff --git a/helm/software/matita/contribs/formal_topology/bin/Makefile b/helm/software/matita/contribs/formal_topology/bin/Makefile
new file mode 100644 (file)
index 0000000..b027980
--- /dev/null
@@ -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 (file)
index 0000000..54c5a2a
--- /dev/null
@@ -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 (file)
index 0000000..be1e107
--- /dev/null
@@ -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 (file)
index 0000000..89ab948
--- /dev/null
@@ -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 (file)
index 0000000..b98865a
--- /dev/null
@@ -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