why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2018-03-28T06:48:33Zhttps://gitlab.inria.fr/why3/why3/-/issues/101eliminate_literal, range types and Eprover driver2018-03-28T06:48:33ZRaphaë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/79first_order_matching may instantiate matching variables using bound variables2018-02-02T10:06:21ZCLOCHARD 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
```
DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/71Incorrect ident parsing in transformations2018-02-02T09:49:53ZRaphaë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` ?DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/13Compute inside an hypothesis2018-01-05T14:19:50ZDAILLER 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.DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/14Add simpl2018-01-05T14:19:32ZDAILLER 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.DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/23Add a revert transformation2017-12-20T13:30:45ZDAILLER 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 etcDAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/34typing of transformation argument should not ignore coercion2017-11-17T09:25:39ZMARCHE 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 intDAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/19Apply with x2017-11-16T11:40:35ZDAILLER 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"DAILLER SylvainDAILLER Sylvain2017-11-15https://gitlab.inria.fr/why3/why3/-/issues/18Case should add expl to its new subgoals2017-11-16T11:40:35ZDAILLER 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.DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/15destruct_alg improvement2017-11-15T15:25:17ZDAILLER 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.DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/25Do not require the user to provide the labels in replace parameters2017-11-10T11:36:56ZRaphaë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 ?DAILLER SylvainDAILLER Sylvain