diff options
Diffstat (limited to 'Semestr 3/pf/lista5')
28 files changed, 0 insertions, 782 deletions
diff --git a/Semestr 3/pf/lista5/proof/Makefile b/Semestr 3/pf/lista5/proof/Makefile deleted file mode 100644 index 0f64038..0000000 --- a/Semestr 3/pf/lista5/proof/Makefile +++ /dev/null @@ -1,22 +0,0 @@ -SOURCES = logic.ml logic.mli proof.mli proof.ml logic.mllib -CMFILES = logic.cma logic.cmi proof.cmi -.PHONY: all clean build - -all: logic.cma logic.cmi proof.cmi - -build: $(SOURCES) - rm -f $(CMFILES) - ocamlbuild logic.cma - -logic.cma: build - cp _build/$@ $@ - -logic.cmi: build - cp _build/$@ $@ - -proof.cmi: build - cp _build/$@ $@ - -clean: - rm -f $(CMFILES) - ocamlbuild -clean diff --git a/Semestr 3/pf/lista5/proof/README b/Semestr 3/pf/lista5/proof/README deleted file mode 100644 index 5fda955..0000000 --- a/Semestr 3/pf/lista5/proof/README +++ /dev/null @@ -1,30 +0,0 @@ -Szablon do listy 5 z Programowania funkcyjnego w grupach mabi, mbu, ppo i efes. - -Zarówno plik README, jak i źródła wykorzystują kodowanie znaków UTF-8. -Jeśli nie wyświetlają się one dobrze na Twoim komputerze, zadbaj o to, -by Twój edytor używał kodowania znaków UTF-8. Jeśli Twój edytor tego -nie potrafi, zmień edytor. - -Pliki logic.mli, logic.ml, proof.mli, proof.ml definiują bibliotekę, -którą łatwo skompilować poleceniem - -$ make - -Pliki logic.mli i logic.ml to szablon listy 4, więc należy je zastąpić -rozwiązaniami tej listy. - -Żeby moduły definiowane przez tą bibliotekę były widoczne w interpreterze, -należy przekazać plik logic.cma jako parametr do interpretera: - -$ utop logic.cma - -Jeśli masz problemy ze skompilowaniem biblioteki, możesz zawsze skompilować ją -ręcznie, choć nie jest to najwygodniejsza metoda: - -$ ocamlc -c logic.mli -$ ocamlc -c logic.ml -$ ocamlc -c proof.mli -$ ocamlc -c proof.ml -$ ocamlc -a -o logic.cma logic.cmo proof.cmo - -Pamiętaj, że po każdej zmianie należy przekompilować bibliotekę. diff --git a/Semestr 3/pf/lista5/proof/_build/_digests b/Semestr 3/pf/lista5/proof/_build/_digests deleted file mode 100644 index ccd3d21..0000000 --- a/Semestr 3/pf/lista5/proof/_build/_digests +++ /dev/null @@ -1,14 +0,0 @@ -"Rule: ocaml: mllib & cmo* -> cma (%=logic )": "\140\207$\221\162s\006\158\014\193x\211\213\214?\207" -"Rule: ocaml dependencies mli (%=proof )": "[]+Z#ML\231B<\205\129iN)F" -"Resource: /mnt/c/Users/franc/Documents/pf/lista5/proof/logic.ml": "\150B>+\t\250\189\162{\249\180\159\247\254\227|" -"Rule: ocaml dependencies ml (%=logic )": "\189H\162<i\136\029\211n.\248\139\156L\019\131" -"Resource: /mnt/c/Users/franc/Documents/pf/lista5/proof/logic.mli": "\144T\172\t\250\250\t\020qGU\157\247\251M\b" -"Resource: /mnt/c/Users/franc/Documents/pf/lista5/proof/proof.ml": "w\002pJ9\208\200;\2479Mu\163u\t\227" -"Rule: ocaml: ml & cmi -> cmo (%=logic )": " L\147\\Y\152\139<e\236\027\014pm\030\017" -"Rule: ocaml: mli -> cmi (%=proof )": "\223\208\252\178\001\197b\158\237w\007\216\152\174\015\172" -"Resource: /mnt/c/Users/franc/Documents/pf/lista5/proof/proof.mli": ";\002\022\169V-\145\129\138\nkd\248\164\253\188" -"Rule: ocaml: ml & cmi -> cmo (%=proof )": "\159\157\219\164\172\158\006.\150\138\167;/\182\b\163" -"Rule: ocaml: mli -> cmi (%=logic )": "\170\192\216\b\023\138!\200EW\017\002\179\007fC" -"Resource: /mnt/c/Users/franc/Documents/pf/lista5/proof/logic.mllib": ",2\194\127\202\253h\245\152ps`\018\195l\230" -"Rule: ocaml dependencies mli (%=logic )": "|\128\193\029\172\176V6EV\145\157\148J\007\232" -"Rule: ocaml dependencies ml (%=proof )": "\151?\155\014\169[\138~\179\016\005\026v\021O\"" diff --git a/Semestr 3/pf/lista5/proof/_build/_log b/Semestr 3/pf/lista5/proof/_build/_log deleted file mode 100644 index 283f2b6..0000000 --- a/Semestr 3/pf/lista5/proof/_build/_log +++ /dev/null @@ -1,20 +0,0 @@ -### Starting build. -# Target: logic.mli.depends, tags: { extension:mli, file:logic.mli, ocaml, ocamldep, quiet, traverse } -/home/fmalinka/.opam/4.11.1/bin/ocamldep.opt -modules logic.mli > logic.mli.depends # cached -# Target: logic.cmi, tags: { byte, compile, extension:mli, file:logic.mli, interf, ocaml, quiet, traverse } -/home/fmalinka/.opam/4.11.1/bin/ocamlc.opt -c -o logic.cmi logic.mli # cached -# Target: logic.ml.depends, tags: { extension:ml, file:logic.ml, ocaml, ocamldep, quiet, traverse } -/home/fmalinka/.opam/4.11.1/bin/ocamldep.opt -modules logic.ml > logic.ml.depends -# Target: proof.mli.depends, tags: { extension:mli, file:proof.mli, ocaml, ocamldep, quiet, traverse } -/home/fmalinka/.opam/4.11.1/bin/ocamldep.opt -modules proof.mli > proof.mli.depends # cached -# Target: proof.cmi, tags: { byte, compile, extension:mli, file:proof.mli, interf, ocaml, quiet, traverse } -/home/fmalinka/.opam/4.11.1/bin/ocamlc.opt -c -o proof.cmi proof.mli # cached -# Target: proof.ml.depends, tags: { extension:ml, file:proof.ml, ocaml, ocamldep, quiet, traverse } -/home/fmalinka/.opam/4.11.1/bin/ocamldep.opt -modules proof.ml > proof.ml.depends # cached -# Target: proof.cmo, tags: { byte, compile, extension:cmo, extension:ml, file:proof.cmo, file:proof.ml, implem, ocaml, quiet, traverse } -/home/fmalinka/.opam/4.11.1/bin/ocamlc.opt -c -o proof.cmo proof.ml # cached -# Target: logic.cmo, tags: { byte, compile, extension:cmo, extension:ml, file:logic.cmo, file:logic.ml, implem, ocaml, quiet, traverse } -/home/fmalinka/.opam/4.11.1/bin/ocamlc.opt -c -o logic.cmo logic.ml -# Target: logic.cma, tags: { byte, extension:cma, file:logic.cma, library, link, ocaml, quiet, traverse } -/home/fmalinka/.opam/4.11.1/bin/ocamlc.opt -a logic.cmo proof.cmo -o logic.cma -# Compilation successful. diff --git a/Semestr 3/pf/lista5/proof/_build/logic.cma b/Semestr 3/pf/lista5/proof/_build/logic.cma Binary files differdeleted file mode 100644 index 2040e52..0000000 --- a/Semestr 3/pf/lista5/proof/_build/logic.cma +++ /dev/null diff --git a/Semestr 3/pf/lista5/proof/_build/logic.cmi b/Semestr 3/pf/lista5/proof/_build/logic.cmi Binary files differdeleted file mode 100644 index d9d951f..0000000 --- a/Semestr 3/pf/lista5/proof/_build/logic.cmi +++ /dev/null diff --git a/Semestr 3/pf/lista5/proof/_build/logic.cmo b/Semestr 3/pf/lista5/proof/_build/logic.cmo Binary files differdeleted file mode 100644 index 7fcc4f9..0000000 --- a/Semestr 3/pf/lista5/proof/_build/logic.cmo +++ /dev/null diff --git a/Semestr 3/pf/lista5/proof/_build/logic.ml b/Semestr 3/pf/lista5/proof/_build/logic.ml deleted file mode 100644 index 27140d5..0000000 --- a/Semestr 3/pf/lista5/proof/_build/logic.ml +++ /dev/null @@ -1,61 +0,0 @@ -type formula = False | Var of string | Imp of formula * formula - -let rec string_of_formula f = - match f with - False -> "⊥" - | Var str -> str - | Imp (f1, f2) -> let str1 = string_of_formula f1 in - (match f1 with - Imp (_, _) -> "(" ^ str1 ^ ")" - | _ -> str1) ^ " ⇒ " ^ string_of_formula f2 -;; -(* match (f1, f2) with - | (Var v1, Var v2) -> (string_of_formula f1) ^ " -> " ^ (string_of_formula f2) - | (Var v1, False) | (False, Var v1) -> (string_of_formula f1) ^ " -> " ^ (string_of_formula f2) - | (False, False) -> (string_of_formula f1) ^ " -> " ^ (string_of_formula f2) - | (f1, f2) -> "(" ^ (string_of_formula f1) ^ " -> " ^ (string_of_formula f2) ^ ")" *) - -let pp_print_formula fmtr f = - Format.pp_print_string fmtr (string_of_formula f) - -type theorem = { assump : formula list; concl : formula } - -let assumptions thm = thm.assump -let consequence thm = thm.concl - -let pp_print_theorem fmtr thm = - let open Format in - pp_open_hvbox fmtr 2; - begin match assumptions thm with - | [] -> () - | f :: fs -> - pp_print_formula fmtr f; - fs |> List.iter (fun f -> - pp_print_string fmtr ","; - pp_print_space fmtr (); - pp_print_formula fmtr f); - pp_print_space fmtr () - end; - pp_open_hbox fmtr (); - pp_print_string fmtr "⊢"; - pp_print_space fmtr (); - pp_print_formula fmtr (consequence thm); - pp_close_box fmtr (); - pp_close_box fmtr () - -let by_assumption f = - { assump=[f]; concl=f } - -let imp_i f thm = - { assump=(List.filter ((<>) f) thm.assump); concl=(Imp (f, thm.concl)) } - -let imp_e th1 th2 = - match th1.concl with - | False | Var _ -> failwith "th1 conclusion is not implication" - | Imp (phi, psi) -> if phi <> th2.concl then failwith "th1 conclusion's premise is not th2 premise conclusion" else - { assump = th1.assump @ th2.assump; concl = psi} - -let bot_e f thm = - match thm with - | {assump=ass; concl=False} -> {assump=ass; concl=f} - | _ -> failwith "thm conclusion is not False" diff --git a/Semestr 3/pf/lista5/proof/_build/logic.ml.depends b/Semestr 3/pf/lista5/proof/_build/logic.ml.depends deleted file mode 100644 index 5169b43..0000000 --- a/Semestr 3/pf/lista5/proof/_build/logic.ml.depends +++ /dev/null @@ -1 +0,0 @@ -logic.ml: Format List diff --git a/Semestr 3/pf/lista5/proof/_build/logic.mli b/Semestr 3/pf/lista5/proof/_build/logic.mli deleted file mode 100644 index afbdc7d..0000000 --- a/Semestr 3/pf/lista5/proof/_build/logic.mli +++ /dev/null @@ -1,44 +0,0 @@ -(** reprezentacja formuł *) -type formula = False | Var of string | Imp of formula * formula - -val pp_print_formula : Format.formatter -> formula -> unit - -(** reprezentacja twierdzeń *) -type theorem - -(** założenia twierdzenia *) -val assumptions : theorem -> formula list -(** teza twierdzeni *) -val consequence : theorem -> formula - -val pp_print_theorem : Format.formatter -> theorem -> unit - -(** by_assumption f konstuuje następujący dowód - - -------(Ax) - {f} ⊢ f *) -val by_assumption : formula -> theorem - -(** imp_i f thm konstuuje następujący dowód - - thm - Γ ⊢ φ - ---------------(→I) - Γ \ {f} ⊢ f → φ *) -val imp_i : formula -> theorem -> theorem - -(** imp_e thm1 thm2 konstuuje następujący dowód - - thm1 thm2 - Γ ⊢ φ → ψ Δ ⊢ φ - ------------------(→E) - Γ ∪ Δ ⊢ ψ *) -val imp_e : theorem -> theorem -> theorem - -(** bot_e f thm konstruuje następujący dowód - - thm - Γ ⊢ ⊥ - -----(⊥E) - Γ ⊢ f *) -val bot_e : formula -> theorem -> theorem diff --git a/Semestr 3/pf/lista5/proof/_build/logic.mli.depends b/Semestr 3/pf/lista5/proof/_build/logic.mli.depends deleted file mode 100644 index 3c54482..0000000 --- a/Semestr 3/pf/lista5/proof/_build/logic.mli.depends +++ /dev/null @@ -1 +0,0 @@ -logic.mli: Format diff --git a/Semestr 3/pf/lista5/proof/_build/logic.mllib b/Semestr 3/pf/lista5/proof/_build/logic.mllib deleted file mode 100644 index 00433f8..0000000 --- a/Semestr 3/pf/lista5/proof/_build/logic.mllib +++ /dev/null @@ -1,2 +0,0 @@ -Logic -Proof diff --git a/Semestr 3/pf/lista5/proof/_build/ocamlc.where b/Semestr 3/pf/lista5/proof/_build/ocamlc.where deleted file mode 100644 index 49511f0..0000000 --- a/Semestr 3/pf/lista5/proof/_build/ocamlc.where +++ /dev/null @@ -1 +0,0 @@ -/home/fmalinka/.opam/4.11.1/lib/ocaml diff --git a/Semestr 3/pf/lista5/proof/_build/proof.cmi b/Semestr 3/pf/lista5/proof/_build/proof.cmi Binary files differdeleted file mode 100644 index 47417e3..0000000 --- a/Semestr 3/pf/lista5/proof/_build/proof.cmi +++ /dev/null diff --git a/Semestr 3/pf/lista5/proof/_build/proof.cmo b/Semestr 3/pf/lista5/proof/_build/proof.cmo Binary files differdeleted file mode 100644 index 674156d..0000000 --- a/Semestr 3/pf/lista5/proof/_build/proof.cmo +++ /dev/null diff --git a/Semestr 3/pf/lista5/proof/_build/proof.ml b/Semestr 3/pf/lista5/proof/_build/proof.ml deleted file mode 100644 index 83ee71a..0000000 --- a/Semestr 3/pf/lista5/proof/_build/proof.ml +++ /dev/null @@ -1,109 +0,0 @@ -open Logic - -type context = (string * formula) list -type goalDesc = context * formula - -type proof = - | Assumption of theorem - | ImpInsert of theorem * proof - | ImpErase of theorem * proof * proof - | Contradiction of theorem * proof - | Whole of goalDesc - -type goal (* = TODO: tu wpisz swoją definicję *) - -let qed pf = - (* TODO: zaimplementuj *) - failwith "not implemented" - -let numGoals pf = - (* TODO: zaimplementuj *) - failwith "not implemented" - -let goals pf = - (* TODO: zaimplementuj *) - failwith "not implemented" - -let proof g f = - (* TODO: zaimplementuj *) - failwith "not implemented" - -let goal pf = - (* TODO: zaimplementuj *) - failwith "not implemented" - -let focus n pf = - (* TODO: zaimplementuj *) - failwith "not implemented" - -let unfocus gl = - (* TODO: zaimplementuj *) - failwith "not implemented" - -let next gl = - (* TODO: zaimplementuj *) - failwith "not implemented" - -let prev gl = - (* TODO: zaimplementuj *) - failwith "not implemented" - -let intro name gl = - (* TODO: zaimplementuj *) - failwith "not implemented" - -let apply f gl = - (* TODO: zaimplementuj *) - failwith "not implemented" - -let apply_thm thm gl = - (* TODO: zaimplementuj *) - failwith "not implemented" - -let apply_assm name gl = - (* TODO: zaimplementuj *) - failwith "not implemented" - -let pp_print_proof fmtr pf = - let ngoals = numGoals pf - and goals = goals pf - in if ngoals = 0 - then Format.pp_print_string fmtr "No more subgoals" - else begin - Format.pp_open_vbox fmtr (-100); - Format.pp_open_hbox fmtr (); - Format.pp_print_string fmtr "There are"; - Format.pp_print_space fmtr (); - Format.pp_print_int fmtr ngoals; - Format.pp_print_space fmtr (); - Format.pp_print_string fmtr "subgoals:"; - Format.pp_close_box fmtr (); - Format.pp_print_cut fmtr (); - goals |> List.iteri (fun n (_, f) -> - Format.pp_print_cut fmtr (); - Format.pp_open_hbox fmtr (); - Format.pp_print_int fmtr (n + 1); - Format.pp_print_string fmtr ":"; - Format.pp_print_space fmtr (); - pp_print_formula fmtr f; - Format.pp_close_box fmtr ()); - Format.pp_close_box fmtr () - end - -let pp_print_goal fmtr gl = - let (g, f) = goal gl - in - Format.pp_open_vbox fmtr (-100); - g |> List.iter (fun (name, f) -> - Format.pp_print_cut fmtr (); - Format.pp_open_hbox fmtr (); - Format.pp_print_string fmtr name; - Format.pp_print_string fmtr ":"; - Format.pp_print_space fmtr (); - pp_print_formula fmtr f; - Format.pp_close_box fmtr ()); - Format.pp_print_cut fmtr (); - Format.pp_print_string fmtr (String.make 40 '='); - Format.pp_print_cut fmtr (); - pp_print_formula fmtr f; - Format.pp_close_box fmtr () diff --git a/Semestr 3/pf/lista5/proof/_build/proof.ml.depends b/Semestr 3/pf/lista5/proof/_build/proof.ml.depends deleted file mode 100644 index 85d6816..0000000 --- a/Semestr 3/pf/lista5/proof/_build/proof.ml.depends +++ /dev/null @@ -1 +0,0 @@ -proof.ml: Format List Logic String diff --git a/Semestr 3/pf/lista5/proof/_build/proof.mli b/Semestr 3/pf/lista5/proof/_build/proof.mli deleted file mode 100644 index ad16a08..0000000 --- a/Semestr 3/pf/lista5/proof/_build/proof.mli +++ /dev/null @@ -1,86 +0,0 @@ -open Logic - -type context = (string * formula) list -type goalDesc = context * formula - -type proof -type goal - -(** Zamienia ukończony dowód na twierdzenie *) -val qed : proof -> theorem - -(** Zwraca liczbę pozostałych w dowodze celów (0 <-> dowód jest gotowy i można go zakończyć) *) -val numGoals : proof -> int - -(** Zwraca listę celów w danym dowodzie *) -val goals : proof -> goalDesc list - - -(** Tworzy pusty dowód podanego twierdzenia *) -val proof : context -> formula -> proof - -(** Zwraca (assm, phi), gdzie assm oraz phi to odpowiednio dostępne - założenia oraz formuła do udowodnienia w aktywnym podcelu *) -val goal : goal -> goalDesc - -(** Ustawia aktywny cel w danym dowodzie *) -val focus : int -> proof -> goal - -(** Zapomina informację o celu *) -val unfocus : goal -> proof - -(** Zmienia (cyklicznie) aktywny cel na następny/poprzedni *) -val next : goal -> goal -val prev : goal -> goal - -(** Wywołanie intro name pf odpowiada regule wprowadzania implikacji. - To znaczy aktywna dziura wypełniana jest regułą: - - (nowy aktywny cel) - (name,ψ) :: Γ ⊢ φ - -----------------(→I) - Γ ⊢ ψ → φ - - Jeśli aktywny cel nie jest implikacją, wywołanie kończy się błędem *) -val intro : string -> goal -> goal - -(** Wywołanie apply ψ₀ pf odpowiada jednocześnie eliminacji implikacji - i eliminacji fałszu. Tzn. jeśli do udowodnienia jest φ, a ψ₀ jest - postaci ψ₁ → ... → ψn → φ to aktywna dziura wypełniana jest regułami - - (nowy aktywny cel) (nowy cel) - Γ ⊢ ψ₀ Γ ⊢ ψ₁ - ----------------------(→E) (nowy cel) - ... Γ ⊢ ψn - ----------------------------(→E) - Γ ⊢ φ - - Natomiast jeśli ψ₀ jest postaci ψ₁ → ... → ψn → ⊥ to aktywna dziura - wypełniana jest regułami - - (nowy aktywny cel) (nowy cel) - Γ ⊢ ψ₀ Γ ⊢ ψ₁ - ----------------------(→E) (nowy cel) - ... Γ ⊢ ψn - ----------------------------(→E) - Γ ⊢ ⊥ - -----(⊥E) - Γ ⊢ φ *) -val apply : formula -> goal -> goal - -(** Wywołanie `apply_thm thm pf` działa podobnie do - `apply (Logic.consequence thm) pf`, tyle że aktywna dziura od razu - jest wypełniana dowodem thm, a otrzymane drzewo nie jest - sfokusowane na żadnym z celów. -*) - -val apply_thm : theorem -> goal -> proof - -(** Wywołanie `apply_assm name pf` działa tak jak - `apply (Logic.by_assumption f) pf`, gdzie f jest założeniem o - nazwie name -*) -val apply_assm : string -> goal -> proof - -val pp_print_proof : Format.formatter -> proof -> unit -val pp_print_goal : Format.formatter -> goal -> unit diff --git a/Semestr 3/pf/lista5/proof/_build/proof.mli.depends b/Semestr 3/pf/lista5/proof/_build/proof.mli.depends deleted file mode 100644 index e405b4e..0000000 --- a/Semestr 3/pf/lista5/proof/_build/proof.mli.depends +++ /dev/null @@ -1 +0,0 @@ -proof.mli: Format Logic diff --git a/Semestr 3/pf/lista5/proof/_tags b/Semestr 3/pf/lista5/proof/_tags deleted file mode 100644 index e69de29..0000000 --- a/Semestr 3/pf/lista5/proof/_tags +++ /dev/null diff --git a/Semestr 3/pf/lista5/proof/logic.cma b/Semestr 3/pf/lista5/proof/logic.cma Binary files differdeleted file mode 100644 index 2040e52..0000000 --- a/Semestr 3/pf/lista5/proof/logic.cma +++ /dev/null diff --git a/Semestr 3/pf/lista5/proof/logic.cmi b/Semestr 3/pf/lista5/proof/logic.cmi Binary files differdeleted file mode 100644 index d9d951f..0000000 --- a/Semestr 3/pf/lista5/proof/logic.cmi +++ /dev/null diff --git a/Semestr 3/pf/lista5/proof/logic.ml b/Semestr 3/pf/lista5/proof/logic.ml deleted file mode 100644 index 234123e..0000000 --- a/Semestr 3/pf/lista5/proof/logic.ml +++ /dev/null @@ -1,142 +0,0 @@ -(* type formula = False | Var of string | Imp of formula * formula - - let rec string_of_formula = function - | False -> "F" - | Var s -> s - | Imp (f1, f2) -> "(" ^ (string_of_formula f1) ^ " -> " ^ (string_of_formula f2) ^ ")" - (* match (f1, f2) with - | (Var v1, Var v2) -> (string_of_formula f1) ^ " -> " ^ (string_of_formula f2) - | (Var v1, False) | (False, Var v1) -> (string_of_formula f1) ^ " -> " ^ (string_of_formula f2) - | (False, False) -> (string_of_formula f1) ^ " -> " ^ (string_of_formula f2) - | (f1, f2) -> "(" ^ (string_of_formula f1) ^ " -> " ^ (string_of_formula f2) ^ ")" *) - - let pp_print_formula fmtr f = - Format.pp_print_string fmtr (string_of_formula f) - - type verdict = { assump : formula list; concl : formula } - - type theorem = - | Assumption of verdict - | ImpInsert of verdict * theorem - | ImpErase of verdict * theorem * theorem - | Contradiction of verdict * theorem - - let get_verdict thm = match thm with - | Assumption f -> f - | ImpInsert (v, _) | ImpErase (v, _, _) | Contradiction (v, _) -> v - - let assumptions thm = (get_verdict thm).assump - let consequence thm = (get_verdict thm).concl - - let pp_print_theorem fmtr thm = - let open Format in - pp_open_hvbox fmtr 2; - begin match assumptions thm with - | [] -> () - | f :: fs -> - pp_print_formula fmtr f; - fs |> List.iter (fun f -> - pp_print_string fmtr ","; - pp_print_space fmtr (); - pp_print_formula fmtr f); - pp_print_space fmtr () - end; - pp_open_hbox fmtr (); - pp_print_string fmtr "⊢"; - pp_print_space fmtr (); - pp_print_formula fmtr (consequence thm); - pp_close_box fmtr (); - pp_close_box fmtr () - - let by_assumption f = - Assumption { assump=[f]; concl=f } - - let imp_i f thm = - let premise = get_verdict thm - in ImpInsert ({assump=(List.filter ((<>) f) premise.assump); concl=(Imp (f, premise.concl))}, thm) - - let imp_e th1 th2 = - let premise1 = get_verdict th1 in - let premise2 = get_verdict th2 in - match premise1.concl with - | False | Var _ -> failwith "th1 conclusion is not implication" - | Imp (phi, psi) -> if phi <> premise2.concl then failwith "th1 conclusion's premise is not th2 premise conclusion" else - ImpErase ({assump=(premise1.assump @ premise2.assump); concl=(psi)}, th1, th2) - - let bot_e f thm = - match get_verdict thm with - | {assump=ass; concl=False}-> (Contradiction ({assump=ass; concl=f}, thm)) - | _ -> failwith "thm conclusion is not False" - - - let taut = (imp_i (Var "p") (by_assumption (Var "p"))) - let taut2 = (imp_i (Var "p") (imp_i (Var "q") (by_assumption (Var "p")))) - - let imppqr = Imp (Var "p", Imp (Var "q", Var "r")) - let imppq = Imp (Var "p", Var "q") - let imppr = Imp (Var "p", Var "r") - let taut3 = (imp_i (imppqr) (imp_i imppq (by_assumption imppr))) *) - - - -type formula = False | Var of string | Imp of formula * formula - -let rec string_of_formula f = - match f with - False -> "⊥" - | Var str -> str - | Imp (f1, f2) -> let str1 = string_of_formula f1 in - (match f1 with - Imp (_, _) -> "(" ^ str1 ^ ")" - | _ -> str1) ^ " ⇒ " ^ string_of_formula f2 -;; -(* match (f1, f2) with - | (Var v1, Var v2) -> (string_of_formula f1) ^ " -> " ^ (string_of_formula f2) - | (Var v1, False) | (False, Var v1) -> (string_of_formula f1) ^ " -> " ^ (string_of_formula f2) - | (False, False) -> (string_of_formula f1) ^ " -> " ^ (string_of_formula f2) - | (f1, f2) -> "(" ^ (string_of_formula f1) ^ " -> " ^ (string_of_formula f2) ^ ")" *) - -let pp_print_formula fmtr f = - Format.pp_print_string fmtr (string_of_formula f) - -type theorem = { assump : formula list; concl : formula } - -let assumptions thm = thm.assump -let consequence thm = thm.concl - -let pp_print_theorem fmtr thm = - let open Format in - pp_open_hvbox fmtr 2; - begin match assumptions thm with - | [] -> () - | f :: fs -> - pp_print_formula fmtr f; - fs |> List.iter (fun f -> - pp_print_string fmtr ","; - pp_print_space fmtr (); - pp_print_formula fmtr f); - pp_print_space fmtr () - end; - pp_open_hbox fmtr (); - pp_print_string fmtr "⊢"; - pp_print_space fmtr (); - pp_print_formula fmtr (consequence thm); - pp_close_box fmtr (); - pp_close_box fmtr () - -let by_assumption f = - { assump=[f]; concl=f } - -let imp_i f thm = - { assump=(List.filter ((<>) f) thm.assump); concl=(Imp (f, thm.concl)) } - -let imp_e th1 th2 = - match th1.concl with - | False | Var _ -> failwith "th1 conclusion is not implication" - | Imp (phi, psi) -> if phi <> th2.concl then failwith "th1 conclusion's premise is not th2 premise conclusion" else - { assump = th1.assump @ th2.assump; concl = psi} - -let bot_e f thm = - match thm with - | {assump=ass; concl=False} -> {assump=ass; concl=f} - | _ -> failwith "thm conclusion is not False" diff --git a/Semestr 3/pf/lista5/proof/logic.mli b/Semestr 3/pf/lista5/proof/logic.mli deleted file mode 100644 index afbdc7d..0000000 --- a/Semestr 3/pf/lista5/proof/logic.mli +++ /dev/null @@ -1,44 +0,0 @@ -(** reprezentacja formuł *) -type formula = False | Var of string | Imp of formula * formula - -val pp_print_formula : Format.formatter -> formula -> unit - -(** reprezentacja twierdzeń *) -type theorem - -(** założenia twierdzenia *) -val assumptions : theorem -> formula list -(** teza twierdzeni *) -val consequence : theorem -> formula - -val pp_print_theorem : Format.formatter -> theorem -> unit - -(** by_assumption f konstuuje następujący dowód - - -------(Ax) - {f} ⊢ f *) -val by_assumption : formula -> theorem - -(** imp_i f thm konstuuje następujący dowód - - thm - Γ ⊢ φ - ---------------(→I) - Γ \ {f} ⊢ f → φ *) -val imp_i : formula -> theorem -> theorem - -(** imp_e thm1 thm2 konstuuje następujący dowód - - thm1 thm2 - Γ ⊢ φ → ψ Δ ⊢ φ - ------------------(→E) - Γ ∪ Δ ⊢ ψ *) -val imp_e : theorem -> theorem -> theorem - -(** bot_e f thm konstruuje następujący dowód - - thm - Γ ⊢ ⊥ - -----(⊥E) - Γ ⊢ f *) -val bot_e : formula -> theorem -> theorem diff --git a/Semestr 3/pf/lista5/proof/logic.mllib b/Semestr 3/pf/lista5/proof/logic.mllib deleted file mode 100644 index 00433f8..0000000 --- a/Semestr 3/pf/lista5/proof/logic.mllib +++ /dev/null @@ -1,2 +0,0 @@ -Logic -Proof diff --git a/Semestr 3/pf/lista5/proof/proof.cmi b/Semestr 3/pf/lista5/proof/proof.cmi Binary files differdeleted file mode 100644 index 47417e3..0000000 --- a/Semestr 3/pf/lista5/proof/proof.cmi +++ /dev/null diff --git a/Semestr 3/pf/lista5/proof/proof.ml b/Semestr 3/pf/lista5/proof/proof.ml deleted file mode 100644 index 3cde679..0000000 --- a/Semestr 3/pf/lista5/proof/proof.ml +++ /dev/null @@ -1,116 +0,0 @@ -open Logic - -type context = (string * formula) list -type goalDesc = context * formula - -type proof = - | Whole of goalDesc - | Leaf of theorem - | ImpInsert of theorem * proof - | ImpErase of theorem * proof * proof - | Contradiction of theorem * proof - -type goal = Goal of (goalDesc list) * (goalDesc list) * proof - -let rec numGoals pf = - match pf with - | Whole _ -> 1 - | Leaf _ -> 0 - | ImpInsert (_, pf) | Contradiction (_, pf) -> numGoals pf - | ImpErase (_, pf1, pf2) -> (numGoals pf1) + (numGoals pf2) - -let qed pf = - if (numGoals pf) <> 0 then failwith "proof not finished" else - match pf with - | Whole _ -> failwith "proof not finished" - | Leaf thm | ImpInsert (thm, _) | ImpErase (thm, _, _) | Contradiction (thm, _) -> thm - -let rec goals pf = - match pf with - | Whole gd -> [gd] - | Leaf _ -> [] - | ImpInsert (_, pf) | Contradiction (_, pf) -> goals pf - | ImpErase (_, pf1, pf2) -> (goals pf1) @ (goals pf2) - -let proof g f = - Whole (g, f) - -let goal (Goal (bef, aft, pf)) = - if aft == [] then failwith "Goal is empty" else (List.hd aft) - -let focus n pf = - let add_goal (Goal (bef, aft, pf)) gl = - Goal (bef, gl::aft, pf) - in let goal = List.fold_left add_goal (Goal ([], [], pf)) (goals pf) in - - let unfocus gl = - (* TODO: zaimplementuj *) - failwith "not implemented" - -let next gl = - (* TODO: zaimplementuj *) - failwith "not implemented" - -let prev gl = - (* TODO: zaimplementuj *) - failwith "not implemented" - -let intro name gl = - (* TODO: zaimplementuj *) - failwith "not implemented" - -let apply f gl = - (* TODO: zaimplementuj *) - failwith "not implemented" - -let apply_thm thm gl = - (* TODO: zaimplementuj *) - failwith "not implemented" - -let apply_assm name gl = - (* TODO: zaimplementuj *) - failwith "not implemented" - -let pp_print_proof fmtr pf = - let ngoals = numGoals pf - and goals = goals pf - in if ngoals = 0 - then Format.pp_print_string fmtr "No more subgoals" - else begin - Format.pp_open_vbox fmtr (-100); - Format.pp_open_hbox fmtr (); - Format.pp_print_string fmtr "There are"; - Format.pp_print_space fmtr (); - Format.pp_print_int fmtr ngoals; - Format.pp_print_space fmtr (); - Format.pp_print_string fmtr "subgoals:"; - Format.pp_close_box fmtr (); - Format.pp_print_cut fmtr (); - goals |> List.iteri (fun n (_, f) -> - Format.pp_print_cut fmtr (); - Format.pp_open_hbox fmtr (); - Format.pp_print_int fmtr (n + 1); - Format.pp_print_string fmtr ":"; - Format.pp_print_space fmtr (); - pp_print_formula fmtr f; - Format.pp_close_box fmtr ()); - Format.pp_close_box fmtr () - end - -let pp_print_goal fmtr gl = - let (g, f) = goal gl - in - Format.pp_open_vbox fmtr (-100); - g |> List.iter (fun (name, f) -> - Format.pp_print_cut fmtr (); - Format.pp_open_hbox fmtr (); - Format.pp_print_string fmtr name; - Format.pp_print_string fmtr ":"; - Format.pp_print_space fmtr (); - pp_print_formula fmtr f; - Format.pp_close_box fmtr ()); - Format.pp_print_cut fmtr (); - Format.pp_print_string fmtr (String.make 40 '='); - Format.pp_print_cut fmtr (); - pp_print_formula fmtr f; - Format.pp_close_box fmtr () diff --git a/Semestr 3/pf/lista5/proof/proof.mli b/Semestr 3/pf/lista5/proof/proof.mli deleted file mode 100644 index 2c939fd..0000000 --- a/Semestr 3/pf/lista5/proof/proof.mli +++ /dev/null @@ -1,85 +0,0 @@ -open Logic - -type context = (string * formula) list -type goalDesc = context * formula - -type proof -type goal - -(** Zamienia ukończony dowód na twierdzenie *) -val qed : proof -> theorem - -(** Zwraca liczbę pozostałych w dowodze celów (0 <-> dowód jest gotowy i można go zakończyć) *) -val numGoals : proof -> int - -(** Zwraca listę celów w danym dowodzie *) -val goals : proof -> goalDesc list - -(** Tworzy pusty dowód podanego twierdzenia *) -val proof : context -> formula -> proof - -(** Zwraca (assm, phi), gdzie assm oraz phi to odpowiednio dostępne - założenia oraz formuła do udowodnienia w aktywnym podcelu *) -val goal : goal -> goalDesc - -(** Ustawia aktywny cel w danym dowodzie *) -val focus : int -> proof -> goal - -(** Zapomina informację o celu *) -val unfocus : goal -> proof - -(** Zmienia (cyklicznie) aktywny cel na następny/poprzedni *) -val next : goal -> goal -val prev : goal -> goal - -(** Wywołanie intro name pf odpowiada regule wprowadzania implikacji. - To znaczy aktywna dziura wypełniana jest regułą: - - (nowy aktywny cel) - (name,ψ) :: Γ ⊢ φ - -----------------(→I) - Γ ⊢ ψ → φ - - Jeśli aktywny cel nie jest implikacją, wywołanie kończy się błędem *) -val intro : string -> goal -> goal - -(** Wywołanie apply ψ₀ pf odpowiada jednocześnie eliminacji implikacji - i eliminacji fałszu. Tzn. jeśli do udowodnienia jest φ, a ψ₀ jest - postaci ψ₁ → ... → ψn → φ to aktywna dziura wypełniana jest regułami - - (nowy aktywny cel) (nowy cel) - Γ ⊢ ψ₀ Γ ⊢ ψ₁ - ----------------------(→E) (nowy cel) - ... Γ ⊢ ψn - ----------------------------(→E) - Γ ⊢ φ - - Natomiast jeśli ψ₀ jest postaci ψ₁ → ... → ψn → ⊥ to aktywna dziura - wypełniana jest regułami - - (nowy aktywny cel) (nowy cel) - Γ ⊢ ψ₀ Γ ⊢ ψ₁ - ----------------------(→E) (nowy cel) - ... Γ ⊢ ψn - ----------------------------(→E) - Γ ⊢ ⊥ - -----(⊥E) - Γ ⊢ φ *) -val apply : formula -> goal -> goal - -(** Wywołanie `apply_thm thm pf` działa podobnie do - `apply (Logic.consequence thm) pf`, tyle że aktywna dziura od razu - jest wypełniana dowodem thm, a otrzymane drzewo nie jest - sfokusowane na żadnym z celów. -*) - -val apply_thm : theorem -> goal -> proof - -(** Wywołanie `apply_assm name pf` działa tak jak - `apply (Logic.by_assumption f) pf`, gdzie f jest założeniem o - nazwie name -*) -val apply_assm : string -> goal -> proof - -val pp_print_proof : Format.formatter -> proof -> unit -val pp_print_goal : Format.formatter -> goal -> unit |