why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2018-10-04T15:07:54+02:00https://gitlab.inria.fr/why3/why3/-/issues/188Modify split_vc to not use simplify_trivial_quantification2018-10-04T15:07:54+02:00Raphaël Rieu-HelftModify split_vc to not use simplify_trivial_quantification1.1.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/185transformation ``apply`` should consider ``let`` as a premise2018-10-29T15:27:58+01:00MARCHE 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
```https://gitlab.inria.fr/why3/why3/-/issues/128Transformation `split_vc` and term shapes2018-06-13T16:56:30+02:00Guillaume 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-01T16:59:05+02:00Guillaume 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`https://gitlab.inria.fr/why3/why3/-/issues/120simplify_trivial_quantification kills some goals2018-05-22T16:47:51+02:00Raphaë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/116Array access in transformations with arguments2018-07-18T17:18:59+02:00DAILLER 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).https://gitlab.inria.fr/why3/why3/-/issues/115subst_all and split_intros_goal_wp do not substitute enough2018-05-23T13:40:23+02:00DAILLER 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/114Problem with infix and val predicate in transformations2018-07-18T17:19:31+02:00DAILLER 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.https://gitlab.inria.fr/why3/why3/-/issues/101eliminate_literal, range types and Eprover driver2018-03-28T08:48:33+02:00Raphaël Rieu-Helfteliminate_literal, range types and Eprover driverOn the following example, launching Eprover fails with this error message:
"internal failure: Failure in transformation eliminate_literal
Ident int63'axiom is already declared, with a different declaration"
The SMT s...On the following example, launching Eprover fails with this error message:
"internal failure: Failure in transformation eliminate_literal
Ident int63'axiom is already declared, with a different declaration"
The SMT solvers work fine.
```
module A
use import int.Int
use import mach.int.Int63
let test (x:int63) : int63
requires { x < 100 }
= x+1
end
```MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/99Simplification of array initializer for generated Why3 code2019-06-18T09:59:37+02:00DAILLER SylvainSimplification of array initializer for generated Why3 codeFor array initializer of Why3 automatically generated code, some simplifications can sometimes be done. This ticket is about writing a transformations to simplify these array initialization.
This is relevant to new_ide only (correspondin...For array initializer of Why3 automatically generated code, some simplifications can sometimes be done. This ticket is about writing a transformations to simplify these array initialization.
This is relevant to new_ide only (corresponding draft branch is array_initializer).https://gitlab.inria.fr/why3/why3/-/issues/88Improve handling of premises2018-08-29T15:46:22+02:00Guillaume 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/79first_order_matching may instantiate matching variables using bound variables2018-02-02T11:06:21+01:00CLOCHARD Martinfirst_order_matching may instantiate matching variables using bound variablesThe routine first_order_matching within src/transform/reduction_engine.ml
does not contains any checks to prevent the unification of a matching variable
with a term containing a bound variable. As a consequence, we can prove false
in the...The routine first_order_matching within src/transform/reduction_engine.ml
does not contains any checks to prevent the unification of a matching variable
with a term containing a bound variable. As a consequence, we can prove false
in the following module (using transformation compute_specified to prove the
second goal):
```
module Soundness
use import int.Int
function f0 (x y z:int) : int = x * y + z
predicate p (f:int -> int) =
f (-1) = 0 && forall n:int. f n = f 0 + (f 1 - f 0) * n
lemma A : forall y z:int. p (fun x -> f0 x y z) <-> y = z
meta rewrite lemma A
lemma Fail : p (fun x -> f0 x x x)
lemma Absurd : false
end
```
https://gitlab.inria.fr/why3/why3/-/issues/71Incorrect ident parsing in transformations2018-02-02T10:49:53+01:00Raphaël Rieu-HelftIncorrect ident parsing in transformationsIn each of the following examples, the output of `print (+)` is `function (+) real real: real` and (in M1) `cut (0 + 0 = 0)` fails with a typing error, when (+) should be the integer addition :
```
module M1
use import real.RealInfix
...In each of the following examples, the output of `print (+)` is `function (+) real real: real` and (in M1) `cut (0 + 0 = 0)` fails with a typing error, when (+) should be the integer addition :
```
module M1
use import real.RealInfix
use import int.Int
constant x: int = 0 + 0
(* constant y: real = 0.0 + 0.0 typing error*)
goal g: True
end
module M2
use import real.RealInfix
(* constant y: real = 0.0 + 0.0 typing error*)
goal g: True
end
```
Maybe the `use import real.Real` declaration in `RealInfix` is treated as a `use export` ?https://gitlab.inria.fr/why3/why3/-/issues/34typing of transformation argument should not ignore coercion2017-11-17T10:25:39+01:00MARCHE Claudetyping of transformation argument should not ignore coercionIn a context like
```
use import int.Int
type byte = < range 0 255 >
meta coercion function byte'int
goal g : ...
```
one should be able to something like
```
cut (3 = (4:byte))
```
Instead, we get:
Parsing error: This...In a context like
```
use import int.Int
type byte = < range 0 255 >
meta coercion function byte'int
goal g : ...
```
one should be able to something like
```
cut (3 = (4:byte))
```
Instead, we get:
Parsing error: This term has type byte, but is expected to have type inthttps://gitlab.inria.fr/why3/why3/-/issues/25Do not require the user to provide the labels in replace parameters2017-11-10T12:36:56+01:00Raphaël Rieu-HelftDo not require the user to provide the labels in replace parametersThe first parameter of the "replace" transformation is only matched if the user provides all the labels of the term to be replaced. Is this necessary ?The first parameter of the "replace" transformation is only matched if the user provides all the labels of the term to be replaced. Is this necessary ?https://gitlab.inria.fr/why3/why3/-/issues/24Apply coercions in replace parameters2019-12-09T17:36:28+01:00Raphaël Rieu-HelftApply coercions in replace parametersCoercions are not applied to the parameters of the replace transformation, forcing the user to specify them (and to go look for the correct name if there are several coercions with the same name in the source).Coercions are not applied to the parameters of the replace transformation, forcing the user to specify them (and to go look for the correct name if there are several coercions with the same name in the source).https://gitlab.inria.fr/why3/why3/-/issues/23Add a revert transformation2017-12-20T14:30:45+01:00DAILLER SylvainAdd a revert transformationMake a general revert transformation.
"revert x" should transform a context:
Delta, x: t, Delta' |- G
into
Delta, x : t |- Delta' "->" G
with "->" meaning -> for hypotheses and forall quantification for symbols.
Eventually use this...Make a general revert transformation.
"revert x" should transform a context:
Delta, x: t, Delta' |- G
into
Delta, x : t |- Delta' "->" G
with "->" meaning -> for hypotheses and forall quantification for symbols.
Eventually use this revert for other transformations like induction, induction_pr etchttps://gitlab.inria.fr/why3/why3/-/issues/22induction_pr with arguments2019-03-27T15:42:06+01:00DAILLER Sylvaininduction_pr with argumentsMake a version of induction_pr with arguments.
"induction_pr H"
Same for "induction_ty_lex".Make a version of induction_pr with arguments.
"induction_pr H"
Same for "induction_ty_lex".https://gitlab.inria.fr/why3/why3/-/issues/20recursive destruct2019-04-29T13:25:34+02:00DAILLER Sylvainrecursive destructCurrently, destruct only destruct the logic connector (/\, \/, =>) at the head of a formula. It could recursively be called on the generated new hypotheses.
This should be implemented as a new name or boolean parameter.Currently, destruct only destruct the logic connector (/\, \/, =>) at the head of a formula. It could recursively be called on the generated new hypotheses.
This should be implemented as a new name or boolean parameter.https://gitlab.inria.fr/why3/why3/-/issues/18Case should add expl to its new subgoals2017-11-16T12:40:35+01:00DAILLER SylvainCase should add expl to its new subgoalsThe transformation "case" should add explanation labels to its subgoals (because these labels are visible in the proof tree). This is more clear for the user.
Transformations induction and others could also take benefits from this.The transformation "case" should add explanation labels to its subgoals (because these labels are visible in the proof tree). This is more clear for the user.
Transformations induction and others could also take benefits from this.