diff options
Diffstat (limited to 'semestr-3/pf/lista5/proof')
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 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/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 |