Commit bc1b7d29 authored by Quentin Garchery's avatar Quentin Garchery

Unified syntax, transformations and register. Elaboration for assumption and trivial

parent d8dc2381
open Why3
open Certd_syntax
open Certd_transformations
open Certd_verif
let split_hyp_and_trans h = checker_ctrans checker (split_hyp_and_ctrans h)
let _ =
let open Args_wrapper in
let open Trans in
wrap_and_register ~desc:"split_hyp_and"
"split_hyp_and_cert" (Tprsymbol (Ttrans_l))
(fun where -> store (split_hyp_and_trans where))
(** Certified transformations *)
let checker_ctrans = checker_ctrans checker
let assumption_trans = checker_ctrans assumption
let trivial_trans = checker_ctrans trivial
let exfalso_trans = checker_ctrans exfalso
let intros_trans = checker_ctrans intros
let intuition_trans = checker_ctrans intuition
let swap_trans where = checker_ctrans (swap where)
let revert_trans ls = checker_ctrans (revert ls)
let intro_trans where = checker_ctrans (intro where)
let left_trans where = checker_ctrans (dir Left where)
let right_trans where = checker_ctrans (dir Right where)
let split_trans where = checker_ctrans (split_logic where)
let instantiate_trans t what = checker_ctrans (inst t what)
let assert_trans t = checker_ctrans (cut t)
let case_trans t = checker_ctrans (case t)
let rewrite_trans g rev where = checker_ctrans (rewrite g rev where)
let clear_trans l = checker_ctrans (clear l)
let pose_trans name t = checker_ctrans (pose name t)
(** Register certified transformations *)
let () =
let open Args_wrapper in let open Trans in
register_transform_l "assumption_cert" (store assumption_trans)
~desc:"A certified version of coq tactic [assumption]";
register_transform_l "trivial_cert" (store trivial_trans)
~desc:"A certified version of (simplified) coq tactic [trivial]";
register_transform_l "exfalso_cert" (store exfalso_trans)
~desc:"A certified version of coq tactic [exfalso]";
register_transform_l "intros_cert" (store intros_trans)
~desc:"A certified version of coq tactic [intros]";
register_transform_l "intuition_cert" (store intuition_trans)
~desc:"A certified version of (simplified) coq tactic [intuition]";
wrap_and_register ~desc:"A certified transformation that negates \
and swaps an hypothesis from the context to the goal]"
"swap_cert" (Topt ("in", Tprsymbol (Ttrans_l)))
(fun where -> store (swap_trans where));
wrap_and_register ~desc:"A certified transformation that generalizes a variable in the goal"
"revert_cert" (Tlsymbol (Ttrans_l))
(fun ls -> store (revert_trans ls));
wrap_and_register ~desc:"A certified version of (simplified) coq tactic [intro]"
"intro_cert" (Topt ("in", Tprsymbol (Ttrans_l)))
(fun where -> store (intro_trans where));
wrap_and_register ~desc:"A certified version of coq tactic [left]"
"left_cert" (Topt ("in", Tprsymbol (Ttrans_l)))
(fun where -> store (left_trans where));
wrap_and_register ~desc:"A certified version of coq tactic [right]"
"right_cert" (Topt ("in", Tprsymbol (Ttrans_l)))
(fun where -> store (right_trans where));
wrap_and_register ~desc:"A certified version of (simplified) coq tactic [split]"
"split_cert" (Topt ("in", Tprsymbol (Ttrans_l)))
(fun where -> store (split_trans where));
wrap_and_register ~desc:"A certified version of transformation instantiate"
"instantiate_cert" (Tterm (Topt ("in", Tprsymbol Ttrans_l)))
(fun t_inst where -> store (instantiate_trans t_inst where));
wrap_and_register ~desc:"A certified version of transformation rewrite"
"rewrite_cert" (Toptbool ("<-", (Tprsymbol (Topt ("in", Tprsymbol (Ttrans_l))))))
(fun rev g where -> store (rewrite_trans g rev where));
wrap_and_register ~desc:"A certified version of transformation assert"
"assert_cert" (Tformula Ttrans_l)
(fun t -> store (assert_trans t));
wrap_and_register ~desc:"A certified version of transformation case"
"case_cert" (Tformula Ttrans_l)
(fun t -> store (case_trans t));
wrap_and_register ~desc:"A certified version of (simplified) coq tactic [clear]"
"clear_cert" (Tprlist Ttrans_l)
(fun l -> store (clear_trans l));
wrap_and_register ~desc:"A certified version of (simplified) coq tactic [pose]"
"pose_cert" (Tstring (Tformula Ttrans_l))
(fun name t -> store (pose_trans name t))
......@@ -167,4 +167,3 @@ let checker_ctrans checker (ctr : ctrans) init_t =
This diff is collapsed.
......@@ -10,8 +10,16 @@ open Certd_syntax
type 'a cert_elab =
| Task_hole of 'a (* So we can fill the holes with the remaining tasks. Corresponds to Skip *)
| Axiom_e of cterm * ident * ident
| Trivial_hyp of ident
| Trivial_goal of ident
| Cut_e of intro * 'a cert_elab * 'a cert_elab
| Split_hyp of (meta * intro * 'a cert_elab * intro * 'a cert_elab)
| Split_goal of (meta * intro * 'a cert_elab * intro * 'a cert_elab)
| Destruct_hyp of meta * intro * intro * 'a cert_elab
| Split_hyp of meta * intro * 'a cert_elab * intro * 'a cert_elab
| Weakening_hyp of cterm * 'a cert_elab * ident
| Weakening_goal of cterm * 'a cert_elab * ident
and meta = (* what is the goal and the target hypothesis at this node of the certificate *)
{ hyp : ident;
......@@ -41,6 +49,44 @@ let rec elab (cta : ctask) (r, g : certif) (fill : 'a list) : 'a cert_elab * 'a
begin match fill with
| [] -> failwith "Not enough to fill"
| first::rest -> Task_hole first, rest end
| Axiom h ->
let t, _ = find_ident h cta in
Axiom_e (t, h, g), fill
| Trivial ->
let t, pos = find_ident g cta in
begin match t, pos with
| CTfalse, false ->
Trivial_hyp g, fill
| CTtrue, true ->
Trivial_goal g, fill
| _ -> assert false
end
| Cut (a, ce1, ce2) ->
let cta1 = Mid.add g (a, true) cta in
let ce1, fill = elab cta1 ce1 fill in
let cta2 = Mid.add g (a, false) cta in
let ce2, fill = elab cta2 ce2 fill in
Cut_e ({id = g; term = a}, ce1, ce2), fill
| Split (c1, c2) ->
let t, pos = find_ident g cta in
begin match t, pos with
| CTbinop (Tor, a, b), true | CTbinop (Tand, a, b), false ->
let cta1 = Mid.add g (a, pos) cta in
let ce1, fill = elab cta1 c1 fill in
let cta2 = Mid.add g (b, pos) cta in
let ce2, fill = elab cta2 c2 fill in
let pack = ({ hyp = g;
concl = find_goal cta},
{ id = g;
term = a},
ce1,
{ id = g;
term = b},
ce2) in
if pos then Split_hyp pack, fill
else Split_goal pack, fill
| _ -> assert false
end
| Destruct (h1, h2, c) ->
let t, pos = find_ident g cta in
begin match t, pos with
......@@ -60,26 +106,13 @@ let rec elab (cta : ctask) (r, g : certif) (fill : 'a list) : 'a cert_elab * 'a
fill
| _ -> assert false
end
| Split (c1, c2) ->
let t, pos = find_ident g cta in
begin match t, pos with
| CTbinop (Tor, a, b), true ->
let cta1 = Mid.add g (a, pos) cta in
let ce1, fill = elab cta1 c1 fill in
let cta2 = Mid.add g (b, pos) cta in
let ce2, fill = elab cta2 c2 fill in
Split_hyp
({ hyp = g;
concl = find_goal cta},
{ id = g;
term = a},
ce1,
{ id = g;
term = b},
ce2),
fill
| _ -> assert false
end
| Weakening c ->
let a, pos = find_ident g cta in
let cta = Mid.remove g cta in
let c, fill = elab cta c fill in
if pos
then Weakening_goal (a, c, g), fill
else Weakening_hyp (a, c, g), fill
| _ -> assert false
......@@ -165,19 +198,51 @@ let nopt = function
let rec print_certif fmt = function
| Task_hole s ->
fprintf fmt "%s" s
| Destruct_hyp (m, i1, i2, c) ->
fprintf fmt "destruct_hyp %a %a (%s => %s => %a) %s"
| Axiom_e (t, h, g) ->
fprintf fmt "axiom (%a) %s %s"
print_term t
(str h)
(str g)
| Trivial_hyp g ->
fprintf fmt "trivial_hyp %s" (str g)
| Trivial_goal g ->
fprintf fmt "trivial_goal %s" (str g)
| Cut_e (i, ce1, ce2) ->
fprintf fmt "cut (%a) (%s => %a) (%s => %a)"
print_term i.term
(str i.id) print_certif ce1
(str i.id) print_certif ce2
| Split_hyp (m, i1, c1, i2, c2) ->
fprintf fmt "split_hyp (%a) (%a) (%s => %a) (%s => %a) %s"
print_term i1.term
print_term i2.term
(str i1.id) (str i2.id) print_certif c
(str i1.id) print_certif c1
(str i2.id) print_certif c2
(str m.hyp)
| Split_hyp (m, i1, c1, i2, c2) ->
fprintf fmt "split_hyp %a %a (%s => %a) (%s => %a) %s"
| Split_goal (m, i1, c1, i2, c2) ->
fprintf fmt "split_goal (%a) (%a) (%s => %a) (%s => %a) %s"
print_term i1.term
print_term i2.term
(str i1.id) print_certif c1
(str i2.id) print_certif c2
(str m.hyp)
| Destruct_hyp (m, i1, i2, c) ->
fprintf fmt "destruct_hyp (%a) (%a) (%s => %s => %a) %s"
print_term i1.term
print_term i2.term
(str i1.id) (str i2.id) print_certif c
(str m.hyp)
| Weakening_hyp (a, c, g) ->
fprintf fmt "weakening_hyp (%a) (%a) %s"
print_term a
print_certif c
(str g)
| Weakening_goal (a, c, g) ->
fprintf fmt "weakening_goal (%a) (%a) %s"
print_term a
print_certif c
(str g)
let ts (ct : ctask) =
Mid.bindings ct
......
predicate a
predicate b
predicate c
axiom g : a \/ c
axiom h : a /\ b
goal G : c
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="8">
<file>
<path name=".."/><path name="test.mlw"/>
<theory name="Top">
<goal name="G">
<transf name="split_hyp_and_cert" arg1="h">
<goal name="G.0">
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
predicate a
predicate b
predicate c
predicate d
predicate e
predicate f
axiom A : a
axiom B : b
predicate p (x : bool)
goal G1 : a /\ b
goal G2 : (a /\ b) /\ (a /\ a /\ a /\ b)
goal G3 : (b /\ a) /\ ( (a /\ a) /\ c)
goal G4 : a /\ (b \/ d)
goal G5 : (a \/ c) /\ (d \/ b)
goal G6 : a /\ (c \/ d)
goal G7 : (a /\ (d \/ c) ) \/ ( ((a /\ b) /\ ((b /\ (d \/ e \/ a)) \/d)) \/ (a /\ c) )
goal G8 : ((((a /\ a) /\ (a /\ a)) /\ ((a /\ a) /\ (a /\ a))) /\ (((a /\ a) /\ (a /\ a)) /\ ((a /\ a) /\ (a /\ a)))) /\ ((((a /\ a) /\ (a /\ a)) /\ ((a /\ a) /\ (a /\ a))) /\ (((a /\ a) /\ (a /\ a)) /\ ((a /\ a) /\ (a /\ a))))
goal G9 : c /\ (d \/ f) <-> (c /\ d) \/ (c /\ f)
goal G10 : c -> d
goal G11 : a /\ (d -> d)
goal G12 : (c <-> a) -> (d \/ c)
goal G13 : (c <-> d) -> c -> d
goal G14 : (d <-> c) -> c -> d
goal G15 : (a -> b -> d <-> c) -> c -> d
goal G16 : d \/ c -> c
goal G17 : (d <-> a) -> d
goal G18 : a -> d -> b -> c -> a -> d
goal G19 : forall x. (forall u. u <-> a) -> (x <-> x)
goal G20 : exists x : bool. p x -> (forall y. p y)
goal G21 : true
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="8">
<prover id="0" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
<file>
<path name=".."/><path name="tests.mlw"/>
<theory name="Top">
<goal name="G1" proved="true">
<transf name="assert" arg1="(forall x. p x)">
<goal name="G1.0" expl="asserted formula">
</goal>
<goal name="G1.1">
</goal>
</transf>
<transf name="case_cert" arg1="true">
<goal name="G1.0">
<proof prover="0" obsolete="true"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="G1.1">
<proof prover="0" obsolete="true"><result status="valid" time="0.00"/></proof>
</goal>
</transf>
<transf name="intuition_cert" proved="true" >
</transf>
<transf name="split_all_full" proved="true" >
<goal name="G1.0" proved="true">
<transf name="assumption_cert" proved="true" >
</transf>
</goal>
<goal name="G1.1" proved="true">
<transf name="assumption_cert" proved="true" >
</transf>
</goal>
</transf>
</goal>
<goal name="G2">
<transf name="intuition_cert" proved="true" >
</transf>
</goal>
<goal name="G3">
<transf name="intuition_cert" >
<goal name="G3.0">
<transf name="assert_cert" arg1="true">
<goal name="G3.0.0">
<transf name="trivial_cert" proved="true" >
</transf>
</goal>
<goal name="G3.0.1">
<transf name="exfalso_cert" >
<goal name="G3.0.1.0">
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="G4">
<transf name="case_cert" arg1="true">
<goal name="G4.0">
</goal>
<goal name="G4.1">
</goal>
</transf>
<transf name="intuition_cert" proved="true" >
</transf>
</goal>
<goal name="G5">
<transf name="intuition_cert" proved="true" >
</transf>
</goal>
<goal name="G6">
<transf name="intuition_cert" >
<goal name="G6.0">
</goal>
</transf>
</goal>
<goal name="G7">
<transf name="intuition_cert" proved="true" >
</transf>
</goal>
<goal name="G8">
<transf name="intuition_cert" proved="true" >
</transf>
</goal>
<goal name="G9">
<transf name="intuition_cert" >
<goal name="G9.0">
</goal>
<goal name="G9.1">
</goal>
<goal name="G9.2">
</goal>
</transf>
</goal>
<goal name="G10">
<transf name="intro_cert" >
<goal name="G10.0">
</goal>
</transf>
</goal>
<goal name="G11">
<transf name="intuition_cert" proved="true" >
</transf>
</goal>
<goal name="G12">
<transf name="intro_cert" >
<goal name="G12.0">
<transf name="rewrite_cert" arg1="H">
<goal name="G12.0.0">
<transf name="intuition_cert" proved="true" >
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="G13">
<transf name="intros_cert" >
<goal name="G13.0">
<transf name="rewrite_cert" arg1="H1" arg2="in" arg3="H">
<goal name="G13.0.0">
<transf name="assumption_cert" proved="true" >
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="G14">
<transf name="intros_cert" >
<goal name="G14.0">
<transf name="rewrite_cert" arg1="&lt;-" arg2="H1" arg3="in" arg4="H">
<goal name="G14.0.0">
<transf name="assumption_cert" proved="true" >
</transf>
<transf name="trivial_cert" proved="true" >
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="G15">
<transf name="intros_cert" >
<goal name="G15.0">
<transf name="rewrite" arg1="&lt;-" arg2="H1" arg3="in" arg4="H">
<goal name="G15.0.0">
</goal>
<goal name="G15.0.1" expl="rewrite premises">
</goal>
<goal name="G15.0.2" expl="rewrite premises">
</goal>
</transf>
<transf name="rewrite_cert" arg1="&lt;-" arg2="H1" arg3="in" arg4="H">
<goal name="G15.0.0">
<transf name="assumption_cert" proved="true" >
</transf>
</goal>
<goal name="G15.0.1" expl="rewrite premises">
<transf name="assumption_cert" proved="true" >
</transf>
</goal>
<goal name="G15.0.2" expl="rewrite premises">
<transf name="assumption_cert" proved="true" >
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="G16">
<transf name="intro_cert" >
<goal name="G16.0">
<transf name="split_cert" arg1="in" arg2="H">
<goal name="G16.0.0">
</goal>
<goal name="G16.0.1">
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="G17">
<transf name="intro_cert" >
<goal name="G17.0">
<transf name="split_cert" arg1="in" arg2="H">
<goal name="G17.0.0">
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="G18">
<transf name="intros_cert" >
<goal name="G18.0">
<transf name="clear_cert" arg1="H4,H2,H1,H,A,B">
<goal name="G18.0.0">
<transf name="assumption_cert" proved="true" >
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="G19">
<transf name="introduce_premises" >
<goal name="G19.0">
<transf name="revert_cert" arg1="x">
<goal name="G19.0.0">
</goal>
</transf>
<transf name="rewrite" arg1="H">
<goal name="G19.0.0">
<proof prover="0" obsolete="true"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="G20">
<transf name="case_cert" arg1="(exists x. not p x)">
<goal name="G20.0">
<transf name="intro_cert" arg1="in" arg2="H">
<goal name="G20.0.0">
<transf name="instantiate_cert" arg1="x">
<goal name="G20.0.0.0">
<transf name="intro_cert" >
<goal name="G20.0.0.0.0">
<transf name="swap_cert" arg1="in" arg2="H2">
<goal name="G20.0.0.0.0.0">
<transf name="assumption_cert" proved="true" >
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="G20.1">
<transf name="instantiate_cert" arg1="True">
<goal name="G20.1.0">
<transf name="intros_cert" >
<goal name="G20.1.0.0">
<transf name="swap_cert" >
<goal name="G20.1.0.0.0">
<transf name="swap_cert" arg1="in" arg2="H3">
<goal name="G20.1.0.0.0.0">
<transf name="instantiate_cert" arg1="y">
<goal name="G20.1.0.0.0.0.0">
<transf name="assumption_cert" proved="true" >
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="G21">
<transf name="pose_cert" arg1="hh" arg2="true">
<goal name="G21.0">
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
......@@ -71,6 +71,9 @@ let fold_product_l f acc ll =
let flatten_rev fl =
List.fold_left (fun acc l -> List.rev_append l acc) [] fl
let rev_flatten fl =
List.fold_left (fun acc l -> l @ acc) [] fl
let part cmp l =
let l = List.stable_sort cmp l in
match l with
......
......@@ -43,6 +43,8 @@ val fold_product_l : ('a -> 'b list -> 'a) -> 'a -> 'b list list -> 'a
val flatten_rev : 'a list list -> 'a list
val rev_flatten : 'a list list -> 'a list
val part : ('a -> 'a -> int) -> 'a list -> 'a list list
(** [part cmp l] returns the list of the congruence classes with
respect to [cmp]. They are returned in reverse order *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment