why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2019-12-09T16:36:28Zhttps://gitlab.inria.fr/why3/why3/-/issues/24Apply coercions in replace parameters2019-12-09T16:36:28ZRaphaĆ«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-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/22induction_pr with arguments2019-03-27T14:42:06ZDAILLER 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".DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/20recursive destruct2019-04-29T11:25:34ZDAILLER 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/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/17Error in transformation remove2019-05-10T14:06:32ZDAILLER 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".DAILLER SylvainDAILLER Sylvainhttps://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 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/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/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 Sylvain