Stare semestry, niepoukladane

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
new 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
new 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
new 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
new 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
new 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
new 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
new 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
new 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