Hello,
I'm dealing with a proof where I would like to apply an `inversion_pr`
on a task of the form:
axiom foo: exists x. A[x]
This doesn't seem to be possible so I looked for a Why3 transformation
that would transform this task into something like:
constant x.
axiom foo: A[x]
so that I could use the `inversion_pr` transformation. Once again, this
doesn't seem to exist. So I tried to write one, and I got this:
open Ident
open Term
open Decl
let rec eliminate_exists_aux pr t =
match t.t_node with
| Tquant (Texists, q) ->
let vsl, _, t' = t_open_quant q in
let intro_var subst vs =
let ls = create_lsymbol (id_clone vs.vs_name) [] (Some
vs.vs_ty) in
Mvs.add vs (fs_app ls [] vs.vs_ty) subst, create_param_decl ls
in
let subst, dl = Lists.map_fold_left intro_var Mvs.empty vsl in
let t' = t_subst subst t' in
let t = t_label_copy t t' in
dl @ eliminate_exists_aux pr t
| _ ->
[create_prop_decl Pgoal pr t]
let eliminate_exists d =
match d.d_node with
| Dprop (Paxiom, pr, t) ->
eliminate_exists_aux pr t
| _ -> [d]
let () = Trans.register_transform "eliminate_exists" (Trans.decl
eliminate_exists None)
~desc:"Destructs the axioms of the form 'exists x. A[x]'."
(I also joined the .ml file to this email.)
The `eliminate_exists_aux` function is heavily inspired by the `intros`
one in `src/transform/introduction.ml`.
The compilation goes well, and the transformation is available in the
IDE. But when I try to use it, nothing happens. I tried to use debug
messages, and the transformation seems to be applied on the right task,
but nothing changes in the IDE, except that, when I try to apply other
transformations, they are only scheduled but never applied: the IDE
seems to be blocked in an inconsistent state.
I must have missed something. Can you help me with that?
Thanks by advance,
--
Nicolas Jeannerod
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2016 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
open Ident
open Term
open Decl
let rec eliminate_exists_aux pr t =
match t.t_node with
| Tquant (Texists, q) ->
let vsl, _, t' = t_open_quant q in
let intro_var subst vs =
let ls = create_lsymbol (id_clone vs.vs_name) [] (Some vs.vs_ty) in
Mvs.add vs (fs_app ls [] vs.vs_ty) subst, create_param_decl ls
in
let subst, dl = Lists.map_fold_left intro_var Mvs.empty vsl in
let t' = t_subst subst t' in
let t = t_label_copy t t' in
dl @ eliminate_exists_aux pr t
| _ ->
[create_prop_decl Pgoal pr t]
let eliminate_exists d =
match d.d_node with
| Dprop (Paxiom, pr, t) ->
eliminate_exists_aux pr t
| _ -> [d]
let () = Trans.register_transform "eliminate_exists" (Trans.decl
eliminate_exists None)
~desc:"Destructs the axioms of the form 'exists x. A[x]'."
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/mailman/listinfo/why3-club
