why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2019-02-12T16:55:13Zhttps://gitlab.inria.fr/why3/why3/-/issues/263Removing Inline_trivial2019-02-12T16:55:13ZDAILLER SylvainRemoving Inline_trivialHello,
I don't understand what this transformation is used for. At first, I thought it was there for optimization but it seems that removing it from the driver makes `cvc4 1.5` fail on some files (`bench/ce/array_mono.mlw`).
Am I misun...Hello,
I don't understand what this transformation is used for. At first, I thought it was there for optimization but it seems that removing it from the driver makes `cvc4 1.5` fail on some files (`bench/ce/array_mono.mlw`).
Am I misunderstanding the use of this transformation ? I think there may be a bug in the rest of the transformations used for CVC4 if not.MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/269transformation replace should replace also under the conditions of `if`2019-02-12T12:55:05ZMARCHE Claudetransformation replace should replace also under the conditions of `if`Apparently `replace` does traverse the conditions of `if` termsApparently `replace` does traverse the conditions of `if` terms1.3.0DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/264destruct improvement with if then else2019-02-08T13:47:07ZDAILLER Sylvaindestruct improvement with if then elseThis issue to keep track of a suggestion by @bbecker to extend destruct to "if .. then .. else":
```
axiom H: if c1 then c2 else c3
```
destruct H would create two branches: one replacing `H` by `c1 `and `c2` and the other one replacin...This issue to keep track of a suggestion by @bbecker to extend destruct to "if .. then .. else":
```
axiom H: if c1 then c2 else c3
```
destruct H would create two branches: one replacing `H` by `c1 `and `c2` and the other one replacing it with `~c1` and `c3`.
Note: Similar behavior can be done for `match`.Benedikt BeckerBenedikt Beckerhttps://gitlab.inria.fr/why3/why3/-/issues/259improve destruct_alg2019-01-31T16:26:45ZMARCHE Claudeimprove destruct_algFeature wishes for improvements:
* allow user to provide the introduced names, e.g `destruct_alg t as x1,x2`
* rename it into something better, e.g. `destruct_term`.Feature wishes for improvements:
* allow user to provide the introduced names, e.g `destruct_alg t as x1,x2`
* rename it into something better, e.g. `destruct_term`.DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/235Avoid substituting to proxy symbols2018-11-16T09:02:53ZDAILLER SylvainAvoid substituting to proxy symbolsWhen using `subst_all` or `split_vc`, it is not rare to substitute variables to a proxy symbol:
```
H : r = (o [@mlw_proxy_symbol])
Goal : r + r = 5
```
With `subst_all` or `split_vc` would become:
`Goal: o + o = 5`
I think it is be...When using `subst_all` or `split_vc`, it is not rare to substitute variables to a proxy symbol:
```
H : r = (o [@mlw_proxy_symbol])
Goal : r + r = 5
```
With `subst_all` or `split_vc` would become:
`Goal: o + o = 5`
I think it is better to do the substitution from the other side.DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/210--list-transform should print all transformations2018-11-13T08:45:47ZDAILLER Sylvain--list-transform should print all transformations`--list-transform` should also print transformation with arguments.`--list-transform` should also print transformation with arguments.DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/231Add a transformation destruct*2018-11-08T10:28:04ZDAILLER SylvainAdd a transformation destruct*Add a transformation that performs destruct recursively on an hypothesis. It should handle all currently handled constructs: disjunction, conjunction, implications.
```
predicate p1
predicate p2
predicate p3
axiom H: p1 -> p2 -> p3
go...Add a transformation that performs destruct recursively on an hypothesis. It should handle all currently handled constructs: disjunction, conjunction, implications.
```
predicate p1
predicate p2
predicate p3
axiom H: p1 -> p2 -> p3
goal G: 1 = 1
```
destruct H should produce 3 new goals for p1, p2 and H : p3 |- G ?
[EDIT: To be more clear]
This should produce 3 new subgoals which are the following:
```
predicate p1
predicate p2
predicate p3
goal G : p1
```
```
predicate p1
predicate p2
predicate p3
goal G : p2
```
```
predicate p1
predicate p2
predicate p3
axiom H : p3
goal G : 1 = 1
```
Sorry for the misleading notations.DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/233Improve apply2018-11-07T10:08:46ZDAILLER SylvainImprove applyIn some cases, we would like apply to perform matching on hypothesis too. Coq can do that in:
```
Goal forall P Q, (forall x y, P x y -> Q) -> P 3 4 -> Q.
intros P Q H H1.
apply H with (1:=H1).
```
We could imagine:
`apply H with_hyp ...In some cases, we would like apply to perform matching on hypothesis too. Coq can do that in:
```
Goal forall P Q, (forall x y, P x y -> Q) -> P 3 4 -> Q.
intros P Q H H1.
apply H with (1:=H1).
```
We could imagine:
`apply H with_hyp H1`
To be investigated.MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/226Restricting behavior of rewrite_list2018-11-07T09:37:53ZDAILLER SylvainRestricting behavior of rewrite_listHello,
Currently `rewrite_list` uses the argument `with_terms` but I think it is difficult for the user to understand what these with_terms corresponds to with this transformation. This list of terms is supposed to be used by `apply/rew...Hello,
Currently `rewrite_list` uses the argument `with_terms` but I think it is difficult for the user to understand what these with_terms corresponds to with this transformation. This list of terms is supposed to be used by `apply/rewrite` after matching. For example,
```
module Rewrite
use int.Int
function f int : int
predicate p int
axiom A: forall a. f (a+1) = f 42
axiom B: forall a. f a = f (43 + 1)
goal g : 5 = f 42
end
```
`rewrite <- A with 43 (* To instantiate a *)`
`rewrite <- B with 43 (* To instantiate a *)`
To me, it makes less sense to try to do the same when rewriting several hypothesis at once:
`rewrite_list <- A,B with 43`
Also, I am not sure that it works when trying to instantiate with a different value for A and B. Should we remove this feature ?Raphaël Rieu-HelftRaphaël Rieu-Helfthttps://gitlab.inria.fr/why3/why3/-/issues/185transformation ``apply`` should consider ``let`` as a premise2018-10-29T14:27:58ZMARCHE Claudetransformation ``apply`` should consider ``let`` as a premiseIn the following example, I can do ``apply A`` but not ``apply B``. It would be nicer if ``apply`` considers the ``let`` as a premise of the property to apply
```
function f int : int
predicate p int int
axiom A: forall x y. x = f y -> p...In the following example, I can do ``apply A`` but not ``apply B``. It would be nicer if ``apply`` considers the ``let`` as a premise of the property to apply
```
function f int : int
predicate p int int
axiom A: forall x y. x = f y -> p x y
axiom B: forall y. let x = f y in p x y
goal g : p 17 42
```DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/195New split_vc sometimes crashes2018-10-05T09:26:19ZRaphaël Rieu-HelftNew split_vc sometimes crashesFollowing commit 22ab5177b, attempting to use split_vc on lemma `valuation_monotonous` in `examples/multiprecision/valuation.mlw` results in a failure (with the new popup!) due to an uncaught NoTerminationProof exception.Following commit 22ab5177b, attempting to use split_vc on lemma `valuation_monotonous` in `examples/multiprecision/valuation.mlw` results in a failure (with the new popup!) due to an uncaught NoTerminationProof exception.1.1.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/188Modify split_vc to not use simplify_trivial_quantification2018-10-04T13:07:54ZRaphaël Rieu-HelftModify split_vc to not use simplify_trivial_quantification1.1.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/88Improve handling of premises2018-08-29T13:46:22ZGuillaume MelquiondImprove handling of premises1. Add a meta on top of the toplevel goals (`split_theory`? IDE?) for display purpose.
2. Systematically add a transformation node that performs `split` and `intro` on a VC (can be disabled by a configuration option).
3. Modify `split_go...1. Add a meta on top of the toplevel goals (`split_theory`? IDE?) for display purpose.
2. Systematically add a transformation node that performs `split` and `intro` on a VC (can be disabled by a configuration option).
3. Modify `split_goal` so that it splits the last labeled disjunction in the context.
4. Remove the implicit `introduce_premises` used for display purpose.https://gitlab.inria.fr/why3/why3/-/issues/114Problem with infix and val predicate in transformations2018-07-18T15:19:31ZDAILLER SylvainProblem with infix and val predicate in transformationsHello,
In master, the specification of the following is not usable inside transformations with arguments (apply, rewrite, print).
```
(** equality is extensional *)
val predicate (==) (s1 s2: seq 'a)
ensures { result <-> length s...Hello,
In master, the specification of the following is not usable inside transformations with arguments (apply, rewrite, print).
```
(** equality is extensional *)
val predicate (==) (s1 s2: seq 'a)
ensures { result <-> length s1 = length s2 &&
forall i: int. 0 <= i < length s1 -> s1[i] = s2[i] }
ensures { result -> s1 = s2 }
```
This can be reproduce with the following code by searching (==) then trying to print the spec:
```
module Test
use import int.Int
use import seq.Seq
goal f: create 32 (fun x -> x) == empty -> false
end
```
I think the reason is that the spec of this is named "infix ==_spec" in pdecl.ml. This is not recognized as a valid identifier by the parser (I think because of the space and "=="). One solution would be to sanitize the new name introduced in pdecl.ml: we would get "infix_eqeq_spec" and be able to use it in transformations.
This is probably a bigger problem, the solution looks very ad hoc but I think it works.
copying @rrieuhel as you reported the bug, thanks.DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/116Array access in transformations with arguments2018-07-18T15:18:59ZDAILLER SylvainArray access in transformations with argumentsIn transformation with arguments, stuff defined with a notation cannot be reused if the notation is overloaded.
In Array63 module we have:
`function ([]) (a: array 'a) (i: int) : 'a = a.elts i`
And an example is:
```
module Test
use...In transformation with arguments, stuff defined with a notation cannot be reused if the notation is overloaded.
In Array63 module we have:
`function ([]) (a: array 'a) (i: int) : 'a = a.elts i`
And an example is:
```
module Test
use import array.Array
use import mach.array.Array63
constant d: Array.array int
constant e: Array63.array int
goal a: e[1] = 5
goal c: Array.([]) d 3 = 5
end
```
In the above, notation [] cannot be used for array d as the notation [] is used for Array63. In this example, it is not even possible to talk about Array.([]) in transformations.
The complete solution would be to accept qualified expressions in arguments of tactics: this may be difficult.
I think it's possible to disambiguate the mixfix notation as we do for infix (==^ ==^^ etc). It would require to extend the parser a little so that "[ term ]", "[ ^ term ]", "[ ^ ^ term ]" are recognized (or any similar notation).DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/128Transformation `split_vc` and term shapes2018-06-13T14:56:30ZGuillaume MelquiondTransformation `split_vc` and term shapesThe transformation `split_vc` splits the goals, simplifies trivial quantifications, and then introduces premises. Unfortunately, it means that we might end up with several proof tasks that have exactly the same shape as children of a sin...The transformation `split_vc` splits the goals, simplifies trivial quantifications, and then introduces premises. Unfortunately, it means that we might end up with several proof tasks that have exactly the same shape as children of a single node of the proof tree. As a consequence, pairing gets completely confused as soon as the code is modified.
A solution would be to change the shape algorithm so that it also hashes the premises that have been marked by `introduce_premises`. This might considerably increase the size of the shapes, but that will also make the pairing algorithm more reliable.
I mark this issue as blocking, since `split_vc` is the recommended transformation for newcomers.1.0.0Raphaël Rieu-HelftRaphaël Rieu-Helfthttps://gitlab.inria.fr/why3/why3/-/issues/126Transformation `apply` and inductive predicates2018-06-01T14:59:05ZGuillaume MelquiondTransformation `apply` and inductive predicatesThe `apply` transformation does not seem to be able to apply constructors of inductive predicate.
inductive unit = tt : unit
goal g : unit
`apply tt` gives `Transformation raised a general error: apply`The `apply` transformation does not seem to be able to apply constructors of inductive predicate.
inductive unit = tt : unit
goal g : unit
`apply tt` gives `Transformation raised a general error: apply`DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/115subst_all and split_intros_goal_wp do not substitute enough2018-05-23T11:40:23ZDAILLER Sylvainsubst_all and split_intros_goal_wp do not substitute enoughIn example verify_this_2018_rouge_et_noir_1, on the last subgoal VC_enum, after split_intros_goal_wp is applied, constant to be substituted remain in subgoal 37 like o o1 etc (as described during gt).
Applying subst_all does not work too...In example verify_this_2018_rouge_et_noir_1, on the last subgoal VC_enum, after split_intros_goal_wp is applied, constant to be substituted remain in subgoal 37 like o o1 etc (as described during gt).
Applying subst_all does not work too. subst seems to work in this case.MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/120simplify_trivial_quantification kills some goals2018-05-22T14:47:51ZRaphaël Rieu-Helftsimplify_trivial_quantification kills some goalsOn the following program, after using split_vc twice (once on the function and once on the assertion), the subgoal `not true` is generated by simplify_trivial_quantification. My understanding is that the goal `not z = y` is used to repla...On the following program, after using split_vc twice (once on the function and once on the assertion), the subgoal `not true` is generated by simplify_trivial_quantification. My understanding is that the goal `not z = y` is used to replace `z` with `y` when attempting to eliminate the quantified variable `z`, but I hope I am wrong.
```
let f (l: list int) (y:int)
= assert { match l with Cons z _ -> not z = y | Nil -> false end }
```
I'm marking this as high priority because `split_vc` is intended as a default strategy for most users.https://gitlab.inria.fr/why3/why3/-/issues/16subst should remove declarations2018-05-16T14:14:22ZDAILLER Sylvainsubst should remove declarationsApplying "subst x" should remove the definition of x. This new behavior will be added as a new name or as a boolean parameter.Applying "subst x" should remove the definition of x. This new behavior will be added as a new name or as a boolean parameter.DAILLER SylvainDAILLER Sylvain