[documentation]: document seq tactic

Author: strub

doc/tactics/seq.rst

@@ -0,0 +1,32 @@
+========================================================================
+Tactic: ``seq```
+========================================================================
+
+The ``seq`` tactic applies to program-logic goals by splitting the
+program(s) under consideration into two consecutive parts.
+
+Applying ``seq`` allows one to decompose such a goal into two separate
+program-logic obligations by splitting the program(s) at a chosen point.
+The first obligation establishes that the initial precondition ensures
+some intermediate assertion after execution of the first part. The second
+obligation then shows that, assuming this intermediate assertion, execution
+of the second part entails the desired postcondition.
+
+The ``seq`` tactic requires the intermediate assertion to be supplied by
+the user, it is not inferred automatically.
+
+------------------------------------------------------------------------
+Variant: ``seq {codepos} : {formula}`` (HL)
+------------------------------------------------------------------------
+
+------------------------------------------------------------------------
+Variant: ``seq {codepos} {codepos} : {formula}`` (pRHL)
+------------------------------------------------------------------------
+
+------------------------------------------------------------------------
+Variant: ``seq`` (pHL)
+------------------------------------------------------------------------
+
+------------------------------------------------------------------------
+Variant: ``seq {codepos} : {formula}`` (eHL)
+------------------------------------------------------------------------