diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-05-16 11:17:14 +0200 |
---|---|---|
committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-06-05 14:41:54 +0200 |
commit | 0e48f50f2c84bafc410097bd67fab66b10947bf3 (patch) | |
tree | 67d4decbfe8e6c43c9e0f4f2706ed6cb29332a77 /doc/sphinx/proof-engine | |
parent | 14352537ee96958913823ad1b8865a21f0b6ad3a (diff) |
[ssr] some fixes to the documentation markup
Diffstat (limited to 'doc/sphinx/proof-engine')
-rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 5c448e564..f842c6e31 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -2817,11 +2817,11 @@ Another useful construct is reduction, showing that a particular case is in fact general enough to prove a general property. This kind of reasoning step usually starts with: “Without loss of generality, we can suppose that …”. Formally, this corresponds to the proof of a goal -G by introducing a cut wlog_statement -> G. Hence the user shall -provide a proof for both (wlog_statement -> G) -> G and -wlog_statement -> G. However, such cuts are usually rather +``G`` by introducing a cut ``wlog_statement -> G``. Hence the user shall +provide a proof for both ``(wlog_statement -> G) -> G`` and +``wlog_statement -> G``. However, such cuts are usually rather painful to perform by -hand, because the statement wlog_statement is tedious to write by hand, +hand, because the statement ``wlog_statement`` is tedious to write by hand, and sometimes even to read. |SSR| implements this kind of reasoning step through the :tacn:`without loss` @@ -2881,9 +2881,10 @@ are unique. wlog: q1 q2 r1 r2 / q1 <= q2. by case (le_gt_dec q1 q2)=> H; last symmetry; eauto with arith. -The ``wlog suff`` variant is simpler, since it cuts wlog_statement instead -of wlog_statement -> G. It thus opens the goals wlog_statement -> G -and wlog_statement. +The ``wlog suff`` variant is simpler, since it cuts ``wlog_statement`` instead +of ``wlog_statement -> G``. It thus opens the goals +``wlog_statement -> G`` +and ``wlog_statement``. In its simplest form the ``generally have : …`` tactic is equivalent to ``wlog suff : …`` followed by last first. When the ``have`` tactic is used |