simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 03:05:31 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Use pose proof instead of assert in coq backend

Browse source
This commit is contained in:
Guillaume Bury 2017-08-12 09:58:13 +02:00
parent fa7da17cde
commit bd5fa2426b
1 changed files with 45 additions and 41 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

86
src/backend/coq.ml
View file

@ -43,42 +43,58 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
let pp_clause fmt c = let pp_clause fmt c =
let rec aux fmt (a, i) = let rec aux fmt (a, i) =
if i < Array.length a then if i < Array.length a then
Format.fprintf fmt "@[<h>%a ->@ @]%a" Format.fprintf fmt "%a ->@ %a"
pp_atom a.(i) aux (a, i + 1) pp_atom a.(i) aux (a, i + 1)
else else
Format.fprintf fmt "False" Format.fprintf fmt "False"
in in
Format.fprintf fmt "@[<hov 1>(%a)@]" aux (c.S.St.atoms, 0) Format.fprintf fmt "@[<hov 1>(%a)@]" aux (c.S.St.atoms, 0)
let pp_clause_intro fmt c = let clause_map c =
let rec aux fmt acc a i = let rec aux acc a i =
if i >= Array.length a then acc if i >= Array.length a then acc
else begin else begin
let name = Format.sprintf "A%d" i in let name = Format.sprintf "A%d" i in
Format.fprintf fmt "%s@ " name; aux (M.add a.(i) name acc) a (i + 1)
aux fmt (M.add a.(i) name acc) a (i + 1)
end end
in in
Format.fprintf fmt "intros @[<hov>"; aux M.empty c.S.St.atoms 0
let m = aux fmt M.empty c.S.St.atoms 0 in
Format.fprintf fmt "@].@\n";
m
let clausify fmt clause = let clausify fmt clause =
Format.fprintf fmt "(* Encoding theory clause %s into: %s *)@\n"
(name_tmp clause) (name clause);
Format.fprintf fmt "assert (%s: %a).@\ntauto. clear %s.@\n" Format.fprintf fmt "assert (%s: %a).@\ntauto. clear %s.@\n"
(name clause) pp_clause clause (name_tmp clause) (name clause) pp_clause clause (name_tmp clause)
let clause_iter m format fmt clause =
let aux atom = Format.fprintf fmt format (M.find atom m) in
Array.iter aux clause.S.St.atoms
let elim_duplicate fmt goal hyp _ = let elim_duplicate fmt goal hyp _ =
(** Printing info comment in coq *) (** Printing info comment in coq *)
Format.fprintf fmt "(* Eliminating doublons.@\n"; Format.fprintf fmt
Format.fprintf fmt " Goal : %s ; Hyp : %s *)@\n" (name goal) (name hyp); "(* Eliminating doublons. Goal : %s ; Hyp : %s *)@\n"
(** Use 'assert' to introduce the clause we want to prove *) (name goal) (name hyp);
Format.fprintf fmt "assert (%s: %a).@\n" (name goal) pp_clause goal;
(** Prove the goal: intro the atoms, then use them with the hyp *) (** Prove the goal: intro the atoms, then use them with the hyp *)
let m = pp_clause_intro fmt goal in let m = clause_map goal in
Format.fprintf fmt "exact (%s%a).@\n" Format.fprintf fmt "pose proof @[<hov>(fun %a=>@ %s%a) as %s@].@\n"
(name hyp) (fun fmt -> Array.iter (fun atom -> (clause_iter m "%s@ ") goal (name hyp)
Format.fprintf fmt " %s" (M.find atom m))) hyp.S.St.atoms (clause_iter m "@ %s") hyp (name goal)
let resolution_aux m a h1 h2 fmt () =
Format.fprintf fmt "%s%a" (name h1)
(fun fmt -> Array.iter (fun b ->
if b == a then begin
Format.fprintf fmt "@ (fun p =>@ %s%a)"
(name h2) (fun fmt -> (Array.iter (fun c ->
if c == a.S.St.neg then
Format.fprintf fmt "@ (fun np => np p)"
else
Format.fprintf fmt "@ %s" (M.find c m)))
) h2.S.St.atoms
end else
Format.fprintf fmt "@ %s" (M.find b m)
)) h1.S.St.atoms
let resolution fmt goal hyp1 hyp2 atom = let resolution fmt goal hyp1 hyp2 atom =
let a = S.St.(atom.var.pa) in let a = S.St.(atom.var.pa) in
@ -87,30 +103,18 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
else (assert (Array.memq a hyp2.S.St.atoms); hyp2, hyp1) else (assert (Array.memq a hyp2.S.St.atoms); hyp2, hyp1)
in in
(** Print some debug info *) (** Print some debug info *)
Format.fprintf fmt "(* Clausal resolution.@\n"; Format.fprintf fmt
Format.fprintf fmt " Goal : %s ; Hyps : %s, %s *)@\n" "(* Clausal resolution. Goal : %s ; Hyps : %s, %s *)@\n"
(name goal) (name h1) (name h2); (name goal) (name h1) (name h2);
(** 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 *) (** Prove the goal: intro the axioms, then perform resolution *)
let m = pp_clause_intro fmt goal in if Array.length goal.S.St.atoms = 0 then begin
Format.fprintf fmt "exact (%s%a).@\n" let m = M.empty in
(name h1) (fun fmt -> Array.iter (fun b -> Format.fprintf fmt "exact @[<hov 1>(%a)@].@\n" (resolution_aux m a h1 h2) ()
if b == a then begin end else begin
Format.fprintf fmt " (fun p => %s%a)" let m = clause_map goal in
(name h2) (fun fmt -> (Array.iter (fun c -> Format.fprintf fmt "pose proof @[<hov>(fun %a=>@ %a)@ as %s.@]@\n"
if c == a.S.St.neg then (clause_iter m "%s@ ") goal (resolution_aux m a h1 h2) () (name goal)
Format.fprintf fmt " (fun np => np p)" end
else
Format.fprintf fmt " %s" (M.find c m)))
) h2.S.St.atoms
end else
Format.fprintf fmt " %s" (M.find b m))
) h1.S.St.atoms
let prove_node t fmt node = let prove_node t fmt node =
@ -138,9 +142,9 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
let print fmt p = let print fmt p =
let h = S.H.create 4013 in let h = S.H.create 4013 in
let aux () node = let aux () node =
Format.fprintf fmt "%a@\n@\n" (prove_node h) node Format.fprintf fmt "%a" (prove_node h) node
in in
Format.fprintf fmt "(* Coq proof generated by mSAT*)@\n@\n"; Format.fprintf fmt "(* Coq proof generated by mSAT*)@\n";
S.fold aux () p S.fold aux () p
end end