simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-22 01:06:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Fix Coq backend

Browse source 
Fix the end of the coq proof, so as to not introduce the empty clause as
a subgoal, and instead directly prove False
This commit is contained in:
Guillaume Bury 2017-08-09 21:09:44 +02:00
parent 04eb1ec1c5
commit 87f080ea47
1 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/backend/coq.ml
View file

@ -90,8 +90,12 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
Format.fprintf fmt "(* Clausal resolution.@\n";
Format.fprintf fmt " Goal : %s ; Hyps : %s, %s *)@\n"
(name goal) (name h1) (name h2);
(** use a cut to introduce the clause we want to prove *)
Format.fprintf fmt "assert (%s: %a).@\n" (name goal) pp_clause goal;
(** use a cut to introduce the clause we want to prove
*except* if it is the last clause, i.e the empty clause because
we already want to prove 'False',
no need to introduce it as a subgoal *)
if Array.length goal.S.St.atoms <> 0 then
Format.fprintf fmt "assert (%s: %a).@\n" (name goal) pp_clause goal;
(** Prove the goal: intro the axioms, then perform resolution *)
let m = pp_clause_intro fmt goal in
Format.fprintf fmt "exact (%s%a).@\n"