%
%  Checks the correctness of a Hilbert proof that a formula is valid,
%    *not* that a formula is a logical consequence of a set of assumptions;
%    beware of the fact that the generalization rule is applied to constants
%    rather than to variables, contrary to the traditional setting!
%    Note that the semantics of p(constant) |= formula is different to
%    the semantics of p(variable) |= formula 
%
:- ensure_loaded('../Basis/internal_operators.pl').
:- use_module('../Basis/translations.pl').
:- use_module('../Basis/utilities.pl').
:- ensure_loaded('../Basis/input_output.pl').

%
%  proof(+Deductions)
%
proof(Deductions) :- proof(Deductions, 1, [], []).

%
%  proof(+Deductions, +Line, +CheckedDeductions, +Constants)
%    Deductions and CheckDeductions are lists of pairs of the form
%    (Assumptions, Formula);
%    Line is equal to the length of CheckedDeductions + 1,
%    and the first member of Deductions is meant to generate
%    the Line'th line of the proof to be checked;
%    Constants is the list of constants to which the Generalization
%    rule has been applied in CheckedDeductions (used for proviso of
%    deduction theorem)
%    If successful, the first member of Deductions will be justified
%    as an axiom, or as an assumption, or on the basis of the deduction rule,
%    or on the basis of modus ponens, or on the basis of the generalization rule;
%    in the case of the deduction rule, where a formula of the form
%    A -> B is derived, it is necessary to check that no member of
%    Constants occurs in A
%
proof([], _, _, _).
proof([Deduction| Deductions], Line, CheckedDeductions, Constants) :-
	Deduction = (_, Formula),
	axiom(Formula, N), !,
	write_proof_line(Line, Deduction,  ['Axiom ', N]),
	NextLine is Line + 1,
	proof(Deductions, NextLine, [Deduction| CheckedDeductions], Constants).
proof([Deduction| Deductions], Line, CheckedDeductions, Constants) :-
	Deduction = (Assumptions, Formula),
	member(Formula, Assumptions),
	write_proof_line(Line, Deduction, ['Assumption']),
	NextLine is Line + 1,
	proof(Deductions, NextLine, [Deduction| CheckedDeductions], Constants).
proof([Deduction| Deductions], Line, CheckedDeductions, Constants) :-
	Deduction = (Assumptions, A imp B),
	nth1(L, CheckedDeductions, (AssumptionsSupportingB, B)),
	select(A, AssumptionsSupportingB, Assumptions),
	do_not_occur_in(Constants, A),
	LineOfB is Line - L,
	write_proof_line(Line, Deduction, ['Deduction ', LineOfB]),
	NextLine is Line + 1,
	proof(Deductions, NextLine, [Deduction| CheckedDeductions], Constants).
proof([Deduction| Deductions], Line, CheckedDeductions, Constants) :-
	Deduction = (_, B),
	nth1(L1, CheckedDeductions, (_, A imp B)),
	nth1(L2, CheckedDeductions, (_, A)), !,
	LineOfAImpliesB is Line - L1,
	LineOfA is Line - L2,
	write_proof_line(Line, Deduction,
		    ['Modus Ponens ', LineOfAImpliesB, ',', LineOfA]),
	NextLine is Line + 1,
	proof(Deductions, NextLine, [Deduction| CheckedDeductions], Constants).
proof([Deduction| Deductions], Line, CheckedDeductions, Constants) :-
	Deduction = (_, forall X: A),
	nth1(L, CheckedDeductions, (_, InstanceOfA)),
	instance(X, Constant, A, InstanceOfA), !,
	LineOfInstanceOfA is Line - L,
	write_proof_line(Line, Deduction, ['Generalization ', LineOfInstanceOfA]),
	NextLine is Line + 1,
	proof(Deductions, NextLine, [Deduction| CheckedDeductions], [Constant| Constants]).
proof([Deduction| _], Line, _, _) :-
	write_proof_line(Line, Deduction, ['cannot be justified']).

%
%  axiom(+Formula, -N)
%    Formula is by convention defined as the N'th axiom
%
axiom(A imp _ imp A, 1).
axiom((A imp B imp C) imp ((A imp B) imp A imp C), 2).
axiom((neg B imp neg A) imp A imp B, 3).
axiom(forall X: A imp B, 4) :-
	instance(X, _, A, B).
axiom(forall X: (A imp B) imp A imp forall X: B, 5) :-
	has_no_free_occurrence_in(X, A).

%
%  do_not_occur_in(+Constants, +Formula)
%
do_not_occur_in([Constant| Constants], Formula) :-
	has_no_occurrence_in(Constant, Formula),
	do_not_occur_in(Constants, Formula).
do_not_occur_in([], _).

%
%  write_proof_line(+Line, +Deduction, +Reason)
%    Deduction is the Line'th line of the proof for Justification.
%
write_proof_line(Line, Deduction, Justification) :-
	writef('%3r. ', [Line]),
	Deduction = (Assumptions, Formula),
	print_assumptions(Assumptions),
	write('|- '),
	from_internal_to_printable(Formula, PrintableFormula),
	write(PrintableFormula),
	line_position(user_output, Position),
	Spaces = 90 - Position,
	tab(Spaces),
	checklist(write, Justification),
	nl.

%
%  print_assumptions(+Assumptions)
%
print_assumptions([]) :- !.
print_assumptions(Assumptions) :-
	maplist(from_internal_to_printable, Assumptions, Printable),
	write_formula_list(Printable),
	write(' ').