why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2018-01-05T15:19:50+01:00https://gitlab.inria.fr/why3/why3/-/issues/13Compute inside an hypothesis2018-01-05T15:19:50+01:00DAILLER SylvainCompute inside an hypothesisAdd a transformation having the same behavior as compute_in_goal for an hypothesis.Add a transformation having the same behavior as compute_in_goal for an hypothesis.https://gitlab.inria.fr/why3/why3/-/issues/14Add simpl2018-01-05T15:19:32+01:00DAILLER SylvainAdd simplAdd a transformation that does less reductions/rewriting than compute_in_goal. It should be similar to the Coq tactics simpl or red.Add a transformation that does less reductions/rewriting than compute_in_goal. It should be similar to the Coq tactics simpl or red.https://gitlab.inria.fr/why3/why3/-/issues/15destruct_alg improvement2017-11-15T16:25:17+01:00DAILLER Sylvaindestruct_alg improvementCurrently, "destruct_alg x" does not work on some cases: it should introduce the new destructed part at the right position in the task. When destructed components are used before their definition, the transformation fails.
Also, rewriti...Currently, "destruct_alg x" does not work on some cases: it should introduce the new destructed part at the right position in the task. When destructed components are used before their definition, the transformation fails.
Also, rewriting after applying this transformation should not be necessary. Add a boolean (or a new transformation name) so that subst is done right after destruct_alg.https://gitlab.inria.fr/why3/why3/-/issues/16subst should remove declarations2018-05-16T16:14:22+02:00DAILLER 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.https://gitlab.inria.fr/why3/why3/-/issues/17Error in transformation remove2019-05-10T16:06:32+02:00DAILLER SylvainError in transformation removeThe error returned by remove should be improved. Instead of "ident not yet declared", it should print something like "cannot remove x since it appears in H".The error returned by remove should be improved. Instead of "ident not yet declared", it should print something like "cannot remove x since it appears in H".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.https://gitlab.inria.fr/why3/why3/-/issues/19Apply with x2017-11-16T12:40:35+01:00DAILLER SylvainApply with xIt should be possible to give hint terms to apply (or rewrite). For example:
"apply h with x,y"
For example, it should allow to directly apply a lemma on transitivity:
"H : forall x y z, x < y -> y < z -> x < z
Goal: 0 < 2"
"apply H...It should be possible to give hint terms to apply (or rewrite). For example:
"apply h with x,y"
For example, it should allow to directly apply a lemma on transitivity:
"H : forall x y z, x < y -> y < z -> x < z
Goal: 0 < 2"
"apply H with 1" generates two new goals "0 < 1" and "1 < 2"2017-11-15https://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/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/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/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/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/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/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/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/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/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/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/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/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 Claude