Menu ▾ ▴

#366 Apply case analysis to arbitrary expression

unplanned
open
nobody
None
5
2022-11-09
2022-03-16
Guillaume Verdier
No

Currently, the case analysis tactic only works on identifiers (which type is a datatype).
Some users would like to be able to apply this tactic on any arbitrary expression which type is a datatype.
For now, it is possible to do it in two steps: first use the abstract expression tactic to abstract the expression, then apply the case analysis tactic on the abstracted expression. However, it would be preferable to be able to do it in a single step.

Discussion

  • Laurent Voisin

    Laurent Voisin - 2022-03-16

    When implementing this feature, we should take care with the well-definedness of the expression. As we will extract it outside of its context, we will need to generate some subgoal to demonstrate that this extraction does not create an ill-defined expression (the WD of a single identifier is always true).

     

  • Laurent Voisin

    Laurent Voisin - 2022-11-09
    • Description has changed:

    Diff:

    --- old
+++ new
@@ -1,3 +1,3 @@
 Currently, the case analysis tactic only works on identifiers (which type is a datatype).
 Some users would like to be able to apply this tactic on any arbitrary expression which type is a datatype.
-For now, it is possible to do it in two steps: first use the abstract expression tactic to abstract the expression, then apply the case analysis tactic on the abstracted expression. However, it would by preferable to be able to do it in a single step.
+For now, it is possible to do it in two steps: first use the abstract expression tactic to abstract the expression, then apply the case analysis tactic on the abstracted expression. However, it would be preferable to be able to do it in a single step.
     

  • Laurent Voisin

    Laurent Voisin - 2022-11-09

    This would be implemented in the DT distinct case reasoner / tactic. There is no need to create a new level, because this cannot happen currently. We should also take care to not generate a WD subgoal when it is not needed (e.g., bare identifier).

     

Log in to post a comment.

MongoDB Logo MongoDB