complement.
--- /dev/null
+theory_explorer: theory_explorer.ml
+ ocamlc -g -rectypes -o theory_explorer unix.cma theory_explorer.ml
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 *********************)
+
--- /dev/null
+(* 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]
+;;
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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
projects / helm.git / commitdiff