diff options
Diffstat (limited to 'Semestr 3/pf/lista5/proof')
28 files changed, 782 insertions, 0 deletions
diff --git a/Semestr 3/pf/lista5/proof/Makefile b/Semestr 3/pf/lista5/proof/Makefile new file mode 100644 index 0000000..0f64038 --- /dev/null +++ b/Semestr 3/pf/lista5/proof/Makefile @@ -0,0 +1,22 @@ +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 new file mode 100644 index 0000000..5fda955 --- /dev/null +++ b/Semestr 3/pf/lista5/proof/README @@ -0,0 +1,30 @@ +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 new file mode 100644 index 0000000..ccd3d21 --- /dev/null +++ b/Semestr 3/pf/lista5/proof/_build/_digests @@ -0,0 +1,14 @@ +"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 new file mode 100644 index 0000000..283f2b6 --- /dev/null +++ b/Semestr 3/pf/lista5/proof/_build/_log @@ -0,0 +1,20 @@ +### 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 differnew file mode 100644 index 0000000..2040e52 --- /dev/null +++ b/Semestr 3/pf/lista5/proof/_build/logic.cma diff --git a/Semestr 3/pf/lista5/proof/_build/logic.cmi b/Semestr 3/pf/lista5/proof/_build/logic.cmi Binary files differnew file mode 100644 index 0000000..d9d951f --- /dev/null +++ b/Semestr 3/pf/lista5/proof/_build/logic.cmi diff --git a/Semestr 3/pf/lista5/proof/_build/logic.cmo b/Semestr 3/pf/lista5/proof/_build/logic.cmo Binary files differnew file mode 100644 index 0000000..7fcc4f9 --- /dev/null +++ b/Semestr 3/pf/lista5/proof/_build/logic.cmo diff --git a/Semestr 3/pf/lista5/proof/_build/logic.ml b/Semestr 3/pf/lista5/proof/_build/logic.ml new file mode 100644 index 0000000..27140d5 --- /dev/null +++ b/Semestr 3/pf/lista5/proof/_build/logic.ml @@ -0,0 +1,61 @@ +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 new file mode 100644 index 0000000..5169b43 --- /dev/null +++ b/Semestr 3/pf/lista5/proof/_build/logic.ml.depends @@ -0,0 +1 @@ +logic.ml: Format List diff --git a/Semestr 3/pf/lista5/proof/_build/logic.mli b/Semestr 3/pf/lista5/proof/_build/logic.mli new file mode 100644 index 0000000..afbdc7d --- /dev/null +++ b/Semestr 3/pf/lista5/proof/_build/logic.mli @@ -0,0 +1,44 @@ +(** 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 new file mode 100644 index 0000000..3c54482 --- /dev/null +++ b/Semestr 3/pf/lista5/proof/_build/logic.mli.depends @@ -0,0 +1 @@ +logic.mli: Format diff --git a/Semestr 3/pf/lista5/proof/_build/logic.mllib b/Semestr 3/pf/lista5/proof/_build/logic.mllib new file mode 100644 index 0000000..00433f8 --- /dev/null +++ b/Semestr 3/pf/lista5/proof/_build/logic.mllib @@ -0,0 +1,2 @@ +Logic +Proof diff --git a/Semestr 3/pf/lista5/proof/_build/ocamlc.where b/Semestr 3/pf/lista5/proof/_build/ocamlc.where new file mode 100644 index 0000000..49511f0 --- /dev/null +++ b/Semestr 3/pf/lista5/proof/_build/ocamlc.where @@ -0,0 +1 @@ +/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 differnew file mode 100644 index 0000000..47417e3 --- /dev/null +++ b/Semestr 3/pf/lista5/proof/_build/proof.cmi diff --git a/Semestr 3/pf/lista5/proof/_build/proof.cmo b/Semestr 3/pf/lista5/proof/_build/proof.cmo Binary files differnew file mode 100644 index 0000000..674156d --- /dev/null +++ b/Semestr 3/pf/lista5/proof/_build/proof.cmo diff --git a/Semestr 3/pf/lista5/proof/_build/proof.ml b/Semestr 3/pf/lista5/proof/_build/proof.ml new file mode 100644 index 0000000..83ee71a --- /dev/null +++ b/Semestr 3/pf/lista5/proof/_build/proof.ml @@ -0,0 +1,109 @@ +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 new file mode 100644 index 0000000..85d6816 --- /dev/null +++ b/Semestr 3/pf/lista5/proof/_build/proof.ml.depends @@ -0,0 +1 @@ +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 new file mode 100644 index 0000000..ad16a08 --- /dev/null +++ b/Semestr 3/pf/lista5/proof/_build/proof.mli @@ -0,0 +1,86 @@ +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 new file mode 100644 index 0000000..e405b4e --- /dev/null +++ b/Semestr 3/pf/lista5/proof/_build/proof.mli.depends @@ -0,0 +1 @@ +proof.mli: Format Logic diff --git a/Semestr 3/pf/lista5/proof/_tags b/Semestr 3/pf/lista5/proof/_tags new file mode 100644 index 0000000..e69de29 --- /dev/null +++ b/Semestr 3/pf/lista5/proof/_tags diff --git a/Semestr 3/pf/lista5/proof/logic.cma b/Semestr 3/pf/lista5/proof/logic.cma Binary files differnew file mode 100644 index 0000000..2040e52 --- /dev/null +++ b/Semestr 3/pf/lista5/proof/logic.cma diff --git a/Semestr 3/pf/lista5/proof/logic.cmi b/Semestr 3/pf/lista5/proof/logic.cmi Binary files differnew file mode 100644 index 0000000..d9d951f --- /dev/null +++ b/Semestr 3/pf/lista5/proof/logic.cmi diff --git a/Semestr 3/pf/lista5/proof/logic.ml b/Semestr 3/pf/lista5/proof/logic.ml new file mode 100644 index 0000000..234123e --- /dev/null +++ b/Semestr 3/pf/lista5/proof/logic.ml @@ -0,0 +1,142 @@ +(* 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 new file mode 100644 index 0000000..afbdc7d --- /dev/null +++ b/Semestr 3/pf/lista5/proof/logic.mli @@ -0,0 +1,44 @@ +(** 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 new file mode 100644 index 0000000..00433f8 --- /dev/null +++ b/Semestr 3/pf/lista5/proof/logic.mllib @@ -0,0 +1,2 @@ +Logic +Proof diff --git a/Semestr 3/pf/lista5/proof/proof.cmi b/Semestr 3/pf/lista5/proof/proof.cmi Binary files differnew file mode 100644 index 0000000..47417e3 --- /dev/null +++ b/Semestr 3/pf/lista5/proof/proof.cmi diff --git a/Semestr 3/pf/lista5/proof/proof.ml b/Semestr 3/pf/lista5/proof/proof.ml new file mode 100644 index 0000000..3cde679 --- /dev/null +++ b/Semestr 3/pf/lista5/proof/proof.ml @@ -0,0 +1,116 @@ +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 new file mode 100644 index 0000000..2c939fd --- /dev/null +++ b/Semestr 3/pf/lista5/proof/proof.mli @@ -0,0 +1,85 @@ +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 |