aboutsummaryrefslogtreecommitdiff
path: root/semestr-3/pf/lista5/proof
diff options
context:
space:
mode:
Diffstat (limited to 'semestr-3/pf/lista5/proof')
-rw-r--r--semestr-3/pf/lista5/proof/_build/logic.cmabin0 -> 5814 bytes
-rw-r--r--semestr-3/pf/lista5/proof/_build/logic.cmibin0 -> 1513 bytes
-rw-r--r--semestr-3/pf/lista5/proof/_build/logic.cmobin0 -> 2340 bytes
-rw-r--r--semestr-3/pf/lista5/proof/_build/logic.ml61
-rw-r--r--semestr-3/pf/lista5/proof/_build/logic.ml.depends1
-rw-r--r--semestr-3/pf/lista5/proof/_build/logic.mli44
-rw-r--r--semestr-3/pf/lista5/proof/_build/logic.mli.depends1
-rw-r--r--semestr-3/pf/lista5/proof/_build/logic.mllib2
-rw-r--r--semestr-3/pf/lista5/proof/_build/ocamlc.where1
-rw-r--r--semestr-3/pf/lista5/proof/_build/proof.cmibin0 -> 2358 bytes
-rw-r--r--semestr-3/pf/lista5/proof/_build/proof.cmobin0 -> 3500 bytes
-rw-r--r--semestr-3/pf/lista5/proof/_build/proof.ml109
-rw-r--r--semestr-3/pf/lista5/proof/_build/proof.ml.depends1
-rw-r--r--semestr-3/pf/lista5/proof/_build/proof.mli86
-rw-r--r--semestr-3/pf/lista5/proof/_build/proof.mli.depends1
-rw-r--r--semestr-3/pf/lista5/proof/logic.cmabin0 -> 5814 bytes
-rw-r--r--semestr-3/pf/lista5/proof/logic.cmibin0 -> 1513 bytes
-rw-r--r--semestr-3/pf/lista5/proof/logic.ml142
-rw-r--r--semestr-3/pf/lista5/proof/logic.mli44
-rw-r--r--semestr-3/pf/lista5/proof/logic.mllib2
-rw-r--r--semestr-3/pf/lista5/proof/proof.cmibin0 -> 2358 bytes
-rw-r--r--semestr-3/pf/lista5/proof/proof.ml116
-rw-r--r--semestr-3/pf/lista5/proof/proof.mli85
23 files changed, 696 insertions, 0 deletions
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
Binary files differ
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
Binary files differ
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
Binary files differ
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
Binary files differ
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
Binary files differ
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/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
Binary files differ
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
Binary files differ
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
Binary files differ
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