The \argument command

Generating argumentation sentences automatically

The following code defines the \argument command (along with all the supporting commands it utilizes):

Code for the \argument command 
\usepackage{cleveref}

%% 
%%  Automatic referencing of definitions
%% 

\ExplSyntaxOn

\seq_new:N \g_cflist_loaded
\seq_new:N \g_cflist_pending

\NewDocumentCommand{\cfadd} { m } {
  \seq_if_in:NnF \g_cflist_loaded { #1 } {
    \seq_if_in:NnF \g_cflist_pending { #1 } {
      \seq_gput_right:Nn \g_cflist_pending { #1 }
    }
  }
}

\NewDocumentCommand{\cfconsiderloaded} { m } {
  \seq_gput_right:Nn \g_cflist_loaded {#1}
}

\NewDocumentCommand{\cfremove} { m } {
  \seq_gremove_all:Nn \g_cflist_pending { #1 }
}

\NewDocumentCommand{\cfload} { o } {
  \seq_if_empty:NTF \g_cflist_pending {
    \IfValueTF{#1}{\ignorespaces}{\unskip}
  } {
    (cf.\ \cref{\seq_use:Nn \g_cflist_pending {,}})\IfValueTF{#1}{#1~}{\unskip}
    \seq_gconcat:NNN \g_cflist_loaded \g_cflist_loaded \g_cflist_pending
    \seq_gclear:N \g_cflist_pending
    \IfValueT{#1}{\ignorespaces}
  }
}

\NewDocumentCommand{\cfclear} {} {
  \seq_gclear:N \g_cflist_loaded
  \seq_gclear:N \g_cflist_pending
}

\NewDocumentCommand{\cfout} { o } {
  \seq_if_empty:NTF \g_cflist_pending {\unskip\IfValueT{#1}{\ignorespaces}} {
    (cf.\ \cref{\seq_use:Nn \g_cflist_pending {,}})\IfValueTF{#1}{#1~}{\unskip}
    \seq_gclear:N \g_cflist_pending
    \IfValueT{#1}{\ignorespaces}
  }
}

\NewDocumentCommand{\ifnocf} { m } {
  \seq_if_empty:NT \g_cflist_pending { #1 }
}

\ExplSyntaxOff

%% 
%%  Alternating note and observe
%% 

\ExplSyntaxOn

\bool_new:N \g_noteobserve

\NewDocumentCommand{\setnote}{}{
  \bool_gset_true:N \g_noteobserve
}

\NewDocumentCommand{\setobserve}{}{
  \bool_gset_false:N \g_noteobserve
}

\NewDocumentCommand{\nobs}{ o }{
  \IfValueT{#1}{
    \str_if_eq:noTF {note} {#1} {
      \bool_gset_true:N \g_noteobserve
    } {
      \str_if_eq:noTF {Note} {#1} {
        \bool_gset_true:N \g_noteobserve
      } {
        \bool_gset_false:N \g_noteobserve
      }
    }
  }
  \bool_if:nTF { \g_noteobserve } {
    \bool_gset_false:N \g_noteobserve
    note
  } {
    \bool_gset_true:N \g_noteobserve
    observe
  }
  \IfValueF{#1}{~}
}

\NewDocumentCommand{\Nobs}{ o }{
  \IfValueT{#1}{
    \str_if_eq:noTF {note} {#1} {
      \bool_gset_true:N \g_noteobserve
    } {
      \str_if_eq:noTF {Note} {#1} {
        \bool_gset_true:N \g_noteobserve
      } {
        \bool_gset_false:N \g_noteobserve
      }
    }
  }
  \bool_if:nTF { \g_noteobserve } {
    \bool_gset_false:N \g_noteobserve
    Note
  } {
    \bool_gset_true:N \g_noteobserve
    Observe
  }
  \IfValueF{#1}{~}
}

\ExplSyntaxOff

%% 
%%  Alternating hence and therefore
%% 

\ExplSyntaxOn

\bool_new:N \g_hencetherefore

\NewDocumentCommand{\hence}{ o }{
  \IfValueT{#1}{
    \str_if_eq:noTF {hence} {#1} {
      \bool_gset_true:N \g_hencetherefore
    } {
      \str_if_eq:noTF {Hence} {#1} {
        \bool_gset_true:N \g_hencetherefore
      } {
        \bool_gset_false:N \g_hencetherefore
      }
    }
  }
  \bool_if:nTF { \g_hencetherefore } {
    \bool_gset_false:N \g_hencetherefore
    hence
  } {
    \bool_gset_true:N \g_hencetherefore
    therefore
  }
  \IfValueF{#1}{~}
}

\NewDocumentCommand{\Hence}{ o }{
  \IfValueT{#1}{
    \str_if_eq:noTF {hence} {#1} {
      \bool_gset_true:N \g_hencetherefore
    } {
      \str_if_eq:noTF {Hence} {#1} {
        \bool_gset_true:N \g_hencetherefore
      } {
        \bool_gset_false:N \g_hencetherefore
      }
    }
  }
  \bool_if:nTF { \g_hencetherefore } {
    \bool_gset_false:N \g_hencetherefore
    Hence,~we~obtain
  } {
    \bool_gset_true:N \g_hencetherefore
    Therefore,~we~obtain
  }
  \IfValueF{#1}{~}
}

\ExplSyntaxOff

%% 
%%  Cycling through proof verbs
%% 

\ExplSyntaxOn

\seq_const_from_clist:Nn \g_prove_mru {
  establish,
  demonstrate,
  prove,
  show,
  imply,
  ensure
}

\prop_new:N \l__verbs
\prop_put:Nnn \l__verbs {show} {shows}
\prop_put:Nnn \l__verbs {imply} {implies}
\prop_put:Nnn \l__verbs {demonstrate} {demonstrates}
\prop_put:Nnn \l__verbs {prove} {proves}
\prop_put:Nnn \l__verbs {establish} {establishes}
\prop_put:Nnn \l__verbs {ensure} {ensures}
\prop_put:Nnn \l__verbs {assure} {assures}

\tl_new:N \g_wordtmp
\seq_new:N \l_mytmps

\cs_generate_variant:Nn \str_if_in:nnTF { nVTF }
\cs_generate_variant:Nn \str_if_in:nnTF { xVTF }

\NewDocumentCommand{\prove}{ o }{
  \IfValueTF{#1}{
    \seq_clear:N \l_mytmps
    \seq_map_inline:Nn \g_prove_mru {
      \str_if_eq:nnTF {##1} {ensure} {
        \str_set:Nn \l_temps {n}
      } {
        \str_set:Nx \l_temps {\str_head_ignore_spaces:n {##1}}
      }
      \str_if_in:xVTF {#1} \l_temps {
        \seq_put_right:Nn \l_mytmps {##1}
      } { }
    }
    \seq_get_right:NN \l_mytmps \g_wordtmp
  } {
    \seq_get_right:NN \g_prove_mru \g_wordtmp
  }
  \tl_use:N \g_wordtmp
  \IfValueTF{#1}{}{~}
  \seq_gput_left:NV \g_prove_mru \g_wordtmp
  \seq_gremove_duplicates:N \g_prove_mru
}

\NewDocumentCommand{\proves}{ o }{
  \IfValueTF{#1}{
    \seq_clear:N \l_mytmps
    \seq_map_inline:Nn \g_prove_mru {
      \str_if_eq:nnTF {##1} {ensure} {
        \str_set:Nn \l_temps {n}
      } {
        \str_set:Nx \l_temps {\str_head_ignore_spaces:n {##1}}
      }
      \str_if_in:xVTF {#1} \l_temps {
        \seq_put_right:Nn \l_mytmps {##1}
      } { }
    }
    \seq_get_right:NN \l_mytmps \g_wordtmp
  } {
    \seq_get_right:NN \g_prove_mru \g_wordtmp
  }
  \str_set:NV \l_tmpa_str \g_wordtmp
  \prop_get:NVN \l__verbs \l_tmpa_str \l_tmpa_tl
  \tl_use:N \l_tmpa_tl
  \IfValueTF{#1}{}{~}
  \seq_gput_left:NV \g_prove_mru \g_wordtmp
  \seq_gremove_duplicates:N \g_prove_mru
}

\ExplSyntaxOff

%% 
%%  Local labels and references
%% 

\ExplSyntaxOn

\newcommand{\llabel}[1]{\savelabel{#1}\label{\loc.#1}\ignorespaces}

\clist_new:N \l_localreflist
\clist_new:N \l_reflist

\NewDocumentCommand{\lref} { m } {
  \clist_set:No \l_localreflist {#1}
  \clist_clear:N \l_reflist
  \clist_map_inline:Nn \l_localreflist { \clist_put_right:Nn \l_reflist {\loc.##1} }
  \cref{\l_reflist}
}

\NewDocumentCommand{\Lref} { m } {
  \clist_set:No \l_localreflist {#1}
  \clist_clear:N \l_reflist
  \clist_map_inline:Nn \l_localreflist { \clist_put_right:Nn \l_reflist {\loc.##1} }
  \Cref{\l_reflist}
}

\NewDocumentCommand{\itref}{ m m }{
  \clist_set:No \l_localreflist {#2}
  \clist_clear:N \l_reflist
  \clist_map_inline:Nn \l_localreflist { \clist_put_right:Nn \l_reflist {#1.##1} }
  \cref{\l_reflist}~in~\cref{#1}
}

\ExplSyntaxOff

%% 
%%  Enumerations
%% 

\ExplSyntaxOn

\seq_new:N \l_enum_seq
\int_new:N \l_num_items

\bool_new:N \g_commaused_bool

\providecommand{\comma}{}

\cs_new:Nn \enum_it:nn {
  \int_case:nnF {\l_num_items - #1} {
    {0} {
      \renewcommand{\comma}{}
      #2\space
    }
    {1} {
      \bool_gset_false:N \g_commaused_bool
      \renewcommand{\comma}{,~\bool_gset_true:N \g_commaused_bool}
      #2
      \bool_if:NTF \g_commaused_bool {} {,~}
      and~
    }
  } {
    \bool_gset_false:N \g_commaused_bool
    \renewcommand{\comma}{,~\bool_gset_true:N \g_commaused_bool}
    #2
    \bool_if:NTF \g_commaused_bool {} {,~}
  }
}


\cs_new:Nn \enum_it_U:nn {
  \int_case:nnF {\l_num_items - #1} {
    {0} {
      \renewcommand{\comma}{}
      #2
      \space
    }
    {1} {
      \bool_gset_false:N \g_commaused_bool
      \renewcommand{\comma}{,~\bool_gset_true:N \g_commaused_bool}
      #2
      \bool_if:NTF \g_commaused_bool {} {,~}
      and~
    }
  } {
    \bool_gset_false:N \g_commaused_bool
    \renewcommand{\comma}{,~\bool_gset_true:N \g_commaused_bool}
    \int_compare:nTF {#1=1} {
      \text_titlecase_first:n {#2}
    } {
      #2
    }
    \bool_if:NTF \g_commaused_bool {} {,~}
  }
}

\cs_generate_variant:Nn \tl_if_eq:nnTF {onTF}

\cs_new:Nn \enum:nnnn {
  \seq_set_split:Nnn \l_enum_seq ; {#1}
  \seq_remove_all:Nn \l_enum_seq { }
  \seq_remove_all:Nn \l_enum_seq {#2}
  \seq_log:N \l_enum_seq
  \int_set:Nn \l_num_items {\seq_count:N \l_enum_seq}
  \int_log:N \l_num_items
  \int_case:nnF {\l_num_items} {
    { 0 } { 0 }
    { 1 } {
      \IfBooleanTF{#4} {
        \tl_set:Nn \l_text_case_exclude_arg_tl {\cref}
        \bool_set_false:N \l_text_titlecase_check_letter_bool
        \text_titlecase_first:n {\seq_use:Nn \l_enum_seq {}}
      } {
        \seq_use:Nn \l_enum_seq {}
      }
      \space
      \tl_if_eq:onTF{#3}{-}{}{
        \bool_if:NTF \l_plural_bool {
          \prove[#3]~
        } {
          \proves[#3]~
        }
      }
    }
    { 2 } {
      \IfBooleanTF{#4} {
        \tl_set:Nn \l_text_case_exclude_arg_tl {\cref}
        \bool_set_false:N \l_text_titlecase_check_letter_bool
        \text_titlecase_first:n {\seq_item:Nn \l_enum_seq {1}}
        {} ~and~
        \seq_item:Nn \l_enum_seq {2}
      } {
        \seq_use:Nn \l_enum_seq {~and~}
      }
      \space
      \tl_if_eq:onTF{#3}{-}{}{
        \prove[#3]~
      }
    }
  } {
    \IfBooleanTF{#4} {
      \tl_set:Nn \l_text_case_exclude_arg_tl {\cref}
      \seq_indexed_map_function:NN \l_enum_seq \enum_it_U:nn
    } {
      \seq_indexed_map_function:NN \l_enum_seq \enum_it:nn
    }
    \tl_if_eq:onTF{#3}{-}{}{
      \prove[#3]~
    }
    % \seq_use:Nnnn \l_enum_seq {~and~} {,~} {,~and~}
    % \unskip
  }
}

\cs_generate_variant:Nn \enum:nnnn {nxnn}
\cs_generate_variant:Nn \enum:nnnn {nxxn}


\NewDocumentCommand{\enum}{O{} m O{-} s}{
  \IfBooleanTF{#4}{
    \enum:nxnn {#2} {#1} {sindep} \BooleanFalse
  } {
    \enum:nxxn {#2} {#1} {#3} \BooleanFalse
  }
}

%% 
%%  Automatic argumentation sentences
%% 

\NewDocumentCommand{\dott}{}{\ifnocf{.}\space}

\bool_new:N \g_arg_start_bool
\bool_gset_true:N \g_arg_start_bool

\NewDocumentCommand{\startnewargseq}{}{\bool_gset_true:N \g_arg_start_bool \tl_set:Nn \g_label_tl {}}

\cs_generate_variant:Nn \seq_if_in:NnTF {NxTF}
\cs_generate_variant:Nn \seq_remove_all:Nn {Nx}

\int_new:N \l_random_int

\cs_generate_variant:Nn \tl_if_head_eq_catcode:nNTF {oNTF}
\cs_generate_variant:Nn \tl_if_head_eq_catcode:nNTF {VNTF}

\cs_generate_variant:Nn \tl_if_head_eq_catcode:nNTF {eNTF}
\cs_generate_variant:Nn \tl_log:n {o}
\cs_generate_variant:Nn \tl_log:n {f}
\cs_generate_variant:Nn \tl_log:n {x}
\cs_generate_variant:Nn \tl_log:n {e}

\cs_generate_variant:Nn \tl_if_in:nnTF {onTF}
\cs_generate_variant:Nn \tl_if_in:NnTF {NeTF}

\cs_generate_variant:Nn \tl_if_head_eq_meaning:nNTF {VNTF}


\seq_const_from_clist:Nn \g_arg_mru_this {
  Ahpr,
  Tapr,
  Ctapr,
  H
}

\seq_const_from_clist:Nn \g_arg_mru_nothis {
  Ia,
  Nwc,
  N,
  Itns,
  Fm,
  Itnswc,
  Mo
}


\seq_new:N \l_arg_seq
\tl_new:N \l_cons_tl
\tl_new:N \l_dummy_tl


\bool_new:N \g_debug_bool
\bool_gset_false:N \g_debug_bool

\bool_new:N \l_insidearg_bool

\bool_new:N \g_firstargletter_bool

\sys_gset_rand_seed:n {0903}

\bool_new:N \l_plural_bool
\tl_new:N \l_arg_verbs_tl


\NewDocumentCommand{\argument}{mom}{
  % \color{blue}
  \bool_set_false:N \l_plural_bool
  \tl_set:Nn \l_arg_verbs_tl {sindep}
  \keys_define:nn { benno/argument } {
    plural .value_forbidden:n = true,
    plural .code:n = {\bool_set_true:N \l_plural_bool},
    verbs .value_required:n = false,
    verbs .tl_set:N = \l_arg_verbs_tl,
  }
  \IfValueT{#2}{
    \keys_set:nn { benno/argument } {#2}
  }
  \bool_log:N \l_plural_bool
  \bool_gset_true:N \l_insidearg_bool
  \seq_set_split:Nnn \l_arg_seq ; {#1}
  \seq_remove_all:Nn \l_arg_seq { }
  \seq_log:N \l_arg_seq
  \tl_set:Nn \l_cons_tl {#3}
  \tl_trim_spaces:N \l_cons_tl
  \seq_if_in:NxTF \l_arg_seq {\lref{\g_label_tl}} {
    % The conclusion of the previous sentence ("this") is among the arguments (Type A1 argumentation sentence)
    \seq_remove_all:Nx \l_arg_seq {\lref{\g_label_tl}}
    \seq_get_left:NNTF \l_arg_seq \l_dummy_tl {
      % There are arguments other than "this"
      \tl_trim_spaces:N \l_dummy_tl
      \bool_gset_false:N \g_firstargletter_bool
      \tl_if_head_eq_catcode:nNTF \l_dummy_tl a {
        \bool_gset_true:N \g_firstargletter_bool
      } {
        \tl_if_head_eq_meaning:VNTF \l_dummy_tl {\cref} {
          \tl_set:Nx \l_tmpa_tl {\tl_tail:N \l_dummy_tl}
          \tl_set:Nx \l_tmpb_tl {\tl_head:N \l_tmpa_tl}
          \bool_gset_true:N \g_firstargletter_bool
          \tl_if_in:NeTF \l_tmpb_tl {lem\c_colon_str} {} {
            \tl_if_in:NeTF \l_tmpb_tl {thm\c_colon_str} {} {
              \tl_if_in:NeTF \l_tmpb_tl {prop\c_colon_str} {} {
                \tl_if_in:NeTF \l_tmpb_tl {cor\c_colon_str} {} {
                  \bool_gset_false:N \g_firstargletter_bool
                }
              }
            }
          }
        } {
        }
      }
      \bool_if:NTF \g_firstargletter_bool {
        \seq_set_eq:NN \l_tmpa_seq \g_arg_mru_this
        \seq_remove_all:Nn \l_tmpa_seq {H}
        \seq_get_right:NN \l_tmpa_seq \l_tmpa_tl
        % The first argument (other than "this") starts with a letter
        % In this case we can use the "S1, S2, ..., and Sn hence prove" template
        \int_case:nnF {\seq_count:N \l_arg_seq} {
          {1} {
            % There is only one argument other than "this"
            \str_case:VnF {\l_tmpa_tl} {
              {Ahpr} {
                \bool_if:NT \g_debug_bool {C1.1}
                \seq_gput_left:Nn \g_arg_mru_this {Ahpr}
                \seq_gremove_duplicates:N \g_arg_mru_this
                \enum:nxnn {#1} {\lref{\g_label_tl}} {-} {\BooleanTrue}
                \hence~
                \bool_if:NTF \l_plural_bool {
                  \prove[\l_arg_verbs_tl]~\ignorespaces #3
                } {
                  \proves[\l_arg_verbs_tl]~\ignorespaces #3
                }
              }
              {Tapr} {
                \bool_if:NT \g_debug_bool {C1.2}
                \seq_gput_left:Nn \g_arg_mru_this {Tapr}
                \seq_gremove_duplicates:N \g_arg_mru_this
                \enum[\lref{\g_label_tl}]{
                  This;
                  #1
                }[\l_arg_verbs_tl]\ignorespaces #3
              }
              {Ctapr} {
                \bool_if:NT \g_debug_bool {C1.3}
                \seq_gput_left:Nn \g_arg_mru_this {Ctapr}
                \seq_gremove_duplicates:N \g_arg_mru_this
                Combining~
                \enum[\lref{\g_label_tl}]{
                  this;
                  #1
                } \proves[\l_arg_verbs_tl]~\ignorespaces #3
              }
            } {}
          }
        } {
          % There are at least two arguments other than "this"
          % In this case, we can use the "Combining S1, S2, ..., and Sn hence proves" template
          \str_case:VnF {\l_tmpa_tl} {
            {Ahpr} {
              \bool_if:NT \g_debug_bool {C2.1}
              \seq_gput_left:Nn \g_arg_mru_this {Ahpr}
              \seq_gremove_duplicates:N \g_arg_mru_this
              \enum:nxnn {#1} {\lref{\g_label_tl}} {-} {\BooleanTrue}
              \hence~
              \prove[\l_arg_verbs_tl]~\ignorespaces #3
            }
            {Tapr} {
              \bool_if:NT \g_debug_bool {C2.2}
              \seq_gput_left:Nn \g_arg_mru_this {Tapr}
              \seq_gremove_duplicates:N \g_arg_mru_this
              \enum[\lref{\g_label_tl}]{
                This;
                #1
              }[\l_arg_verbs_tl]\ignorespaces #3
            }
            {Ctapr} {
              \int_case:nn {\int_rand:nn {0} {1}} {
                {0} {
                  \bool_if:NT \g_debug_bool {C2.3}
                  \seq_gput_left:Nn \g_arg_mru_this {Ctapr}
                  \seq_gremove_duplicates:N \g_arg_mru_this
                  Combining~
                  \enum[\lref{\g_label_tl}]{
                    this;
                    #1
                  } \proves[\l_arg_verbs_tl]~\ignorespaces #3
                }
                {1} {
                  \bool_if:NT \g_debug_bool {C2.4}
                  \seq_gput_left:Nn \g_arg_mru_this {Ctapr}
                  \seq_gremove_duplicates:N \g_arg_mru_this
                  Combining~
                  \enum:nxnn {#1} {\lref{\g_label_tl}} {-} {\BooleanFalse}
                  \hence~
                  \proves[\l_arg_verbs_tl]~\ignorespaces #3
                }
              }
            }
          } {}
        }
      } {
        \seq_set_eq:NN \l_tmpa_seq \g_arg_mru_this
        \seq_remove_all:Nn \l_tmpa_seq {H}
        \seq_remove_all:Nn \l_tmpa_seq {Ahpr}
        \seq_get_right:NN \l_tmpa_seq \l_tmpa_tl
        % The first argument (other than "this") does not start with a letter
        \int_case:nnF {\seq_count:N \l_arg_seq} {
          {1} {
            % There is only one argument other than "this"
            \str_case:VnF {\l_tmpa_tl} {
              {Tapr} {
                \bool_if:NT \g_debug_bool {C3.1}
                \seq_gput_left:Nn \g_arg_mru_this {Tapr}
                \seq_gremove_duplicates:N \g_arg_mru_this
                \enum[\lref{\g_label_tl}]{
                  This;
                  #1
                }[\l_arg_verbs_tl]\ignorespaces #3
              }
              {Ctapr} {
                \bool_if:NT \g_debug_bool {C3.2}
                \seq_gput_left:Nn \g_arg_mru_this {Ctapr}
                \seq_gremove_duplicates:N \g_arg_mru_this
                Combining~
                \enum[\lref{\g_label_tl}]{
                  this;
                  #1
                } \proves[\l_arg_verbs_tl]~\ignorespaces #3
              }
            } {}
          }
        } {
          % There are at least two arguments other than "this"
          \str_case:VnF {\l_tmpa_tl} {
            {Tapr} {
              \bool_if:NT \g_debug_bool {C4.1}
              \seq_gput_left:Nn \g_arg_mru_this {Tapr}
              \seq_gremove_duplicates:N \g_arg_mru_this
              \enum[\lref{\g_label_tl}]{
                This;
                #1
              }[\l_arg_verbs_tl]\ignorespaces #3
            }
            {Ctapr} {
              \int_case:nn {\int_rand:nn {0} {1}} {
                {0} {
                  \bool_if:NT \g_debug_bool {C4.2}
                  \seq_gput_left:Nn \g_arg_mru_this {Ctapr}
                  \seq_gremove_duplicates:N \g_arg_mru_this
                  Combining~
                  \enum[\lref{\g_label_tl}]{
                    this;
                    #1
                  } \proves[\l_arg_verbs_tl]~\ignorespaces #3
                }
                {1} {
                  \bool_if:NT \g_debug_bool {C4.3}
                  \seq_gput_left:Nn \g_arg_mru_this {Ctapr}
                  \seq_gremove_duplicates:N \g_arg_mru_this
                  Combining~
                  \enum:nxnn {#1} {\lref{\g_label_tl}} {-} {\BooleanFalse}
                  \hence~
                  \proves[\l_arg_verbs_tl]~\ignorespaces #3    
                }
              }
            }
          } {}
        }
      }
    } {
      % "This" is the only argument
      \tl_if_head_eq_catcode:oNTF \l_cons_tl a {
        % The consequence starts with a letter
        \seq_set_eq:NN \l_tmpa_seq \g_arg_mru_this
        \seq_remove_all:Nn \l_tmpa_seq {Ctapr}
        \seq_remove_all:Nn \l_tmpa_seq {Ahpr}
        \seq_get_right:NN \l_tmpa_seq \l_tmpa_tl
        \str_case:VnF {\l_tmpa_tl} {
          {H} {
            \bool_if:NT \g_debug_bool {C5.1}
            \seq_gput_left:Nn \g_arg_mru_this {H}
            \seq_gremove_duplicates:N \g_arg_mru_this
            Hence,~we~obtain~\ignorespaces #3
          }
          {Tapr} {
            \bool_if:NT \g_debug_bool {C5.2}
            \seq_gput_left:Nn \g_arg_mru_this {Tapr}
            \seq_gremove_duplicates:N \g_arg_mru_this
            This~\proves[\l_arg_verbs_tl]~\ignorespaces #3
          }
        } {}
      } {
        % The consequence does not start with a letter
        % These are cases like "This establishes item (i)". We do not want to 
        % use "Hence, we obtain item (i)" in this case.
        \bool_if:NT \g_debug_bool {C6.1}
        \seq_gput_left:Nn \g_arg_mru_this {Tapr}
        \seq_gremove_duplicates:N \g_arg_mru_this
        This~\proves[\l_arg_verbs_tl]~\ignorespaces #3
      }
    } 
  } {
    % The previous sentence is not referenced (Type A2 or Type B1 argumentation sentence)
    \int_compare:nNnTF {\seq_count:N \l_arg_seq} = {0} {
      % Special case: There are no arguments (should not actually happen)
      \bool_if:NTF \g_arg_start_bool {
        \bool_if:NT \g_debug_bool {C7.1}
        \Nobs\unskip
        #3
      } {
        \bool_if:NT \g_debug_bool {C7.2}
        \Moreover~
        #3
      }
    } {
      % There are arguments
      \bool_if:NTF \g_arg_start_bool {
        % We are at the start of a new sequence of argumentation sentences (i.e., the start
        % of the proof or after a "establishes item (x)"), Type A2 argumentation sentence
        \bool_if:NT \g_debug_bool {C8.1}
        \tl_log:N \l_arg_verbs_tl
        \Nobs~that~
        \enum{
          #1
        }[\l_arg_verbs_tl]\ignorespaces #3
      } {
        % Type B1 argumentation sentence
        \int_compare:nNnTF {\seq_count:N \l_arg_seq} = {1} {
          \seq_set_eq:NN \l_tmpa_seq \g_arg_mru_nothis
          \seq_remove_all:Nn \l_tmpa_seq {Nwc}
          \seq_remove_all:Nn \l_tmpa_seq {Itnswc}
          \seq_get_right:NN \l_tmpa_seq \l_tmpa_tl
        } {
          \seq_get_right:NN \g_arg_mru_nothis \l_tmpa_tl
        }
        \str_case:VnF {\l_tmpa_tl} {
          {Mo} {
            \bool_if:NT \g_debug_bool {C9.1}
            \seq_gput_left:Nn \g_arg_mru_nothis {Mo}
            \seq_gremove_duplicates:N \g_arg_mru_nothis
            Moreover,~\nobs~that~
            \enum{
              #1
            }[\l_arg_verbs_tl]\ignorespaces #3
          }
          {Fm} {
            \bool_if:NT \g_debug_bool {C9.2}
            \seq_gput_left:Nn \g_arg_mru_nothis {Fm}
            \seq_gremove_duplicates:N \g_arg_mru_nothis
            Furthermore,~\nobs~that~
            \enum{
              #1
            }[\l_arg_verbs_tl]\ignorespaces #3
          }
          {Ia} {
            \bool_if:NT \g_debug_bool {C9.3}
            \seq_gput_left:Nn \g_arg_mru_nothis {Ia}
            \seq_gremove_duplicates:N \g_arg_mru_nothis
            In~addition,~\nobs~that~
            \enum{
              #1
            }[\l_arg_verbs_tl]\ignorespaces #3
          }
          {N} {
            \bool_if:NT \g_debug_bool {C9.4}
            \seq_gput_left:Nn \g_arg_mru_nothis {N}
            \seq_gremove_duplicates:N \g_arg_mru_nothis
            Next,~\nobs~that~
            \enum{
              #1
            }[\l_arg_verbs_tl]\ignorespaces #3
          }
          {Itns} {
            \bool_if:NT \g_debug_bool {C9.5}
            \seq_gput_left:Nn \g_arg_mru_nothis {Itnswc}
            \seq_gput_left:Nn \g_arg_mru_nothis {Itns}
            \seq_gremove_duplicates:N \g_arg_mru_nothis
            In~the~next~step~we~\nobs~that~
            \enum{
              #1
            }[\l_arg_verbs_tl]\ignorespaces #3
          }
          {Nwc} {
            \bool_if:NT \g_debug_bool {C9.6}
            \seq_gput_left:Nn \g_arg_mru_nothis {Nwc}
            \seq_gremove_duplicates:N \g_arg_mru_nothis
            Next~we~combine~
            \enum{
              #1
            }to~obtain~\ignorespaces #3
          }
          {Itnswc} {
            \bool_if:NT \g_debug_bool {C9.7}
            \seq_gput_left:Nn \g_arg_mru_nothis {Itns}
            \seq_gput_left:Nn \g_arg_mru_nothis {Itnswc}
            \seq_gremove_duplicates:N \g_arg_mru_nothis
            In~the~next~step~we~combine~
            \enum{
              #1
            }to~obtain~\ignorespaces #3
          }
        } {}
      }
    }
  }
  \bool_gset_false:N \g_arg_start_bool
  \bool_gset_false:N \l_insidearg_bool
  \cfload[.]%~\unskip
  % \color{black}
}

\tl_new:N \g_label_tl
\tl_gset:Nn \g_label_tl { }

\NewDocumentCommand{\savelabel}{m}{
  \bool_if:NTF \l_insidearg_bool {
    \tl_gset:Nn \g_label_tl {#1}
  } {
    \tl_gset:Nn \g_label_tl { }
  }
}

\ExplSyntaxOff

%%
%%  Convenient theorem and proof environments
%%

\ExplSyntaxOn

\NewDocumentEnvironment {athm} {m m o} {
\str_if_eq:noTF {example} {#1} {
  \bool_gset_true:N \g_example_bool
} {
  \bool_gset_false:N \g_example_bool
}
\cfclear
\IfNoValueTF{#3}{
\begin{#1}\label{#2}\global\def\loc{#2}
}{
\begin{#1}[#3]\label{#2}\global\def\loc{#2}
}
}{
\end{#1}
}

\NewDocumentEnvironment {adef} {m} {
\begin{definition}\label{#1}\global\def\loc{#1}
}{
\end{definition}
}

\NewDocumentEnvironment{aproof} {} {
\bool_if:NTF \g_example_bool {
  \bool_gset_true:N \g_arg_start_bool
  \begin{proof}[Proof~for~\cref{\loc}]
} {
  \bool_gset_true:N \g_arg_start_bool
  \begin{proof}[Proof~of~\cref{\loc}]
}
\bool_gset_false:N \g_finishproof_bool
}{
\bool_if:NTF \g_finishproof_bool {}
{\finishproofthus}
\end{proof}
}

\NewDocumentCommand{\finishproofthus} {} {
  \bool_gset_true:N \g_finishproof_bool 
  \bool_if:NTF \g_example_bool {
    The~proof~for~\cref{\loc}~is~thus~complete.
  } {
    The~proof~of~\cref{\loc}~is~thus~complete.
  }
}
\NewDocumentCommand{\finishproofthis} {} {
  \bool_gset_true:N \g_finishproof_bool 
  \bool_if:NTF \g_example_bool {
    This~completes~the~proof~for~\cref{\loc}.
  } {
    This~completes~the~proof~of~\cref{\loc}.
  }
}

\ExplSyntaxOff
The \argument command is used inside proofs and takes two mandatory arguments:
  • a semicolon-separated list of premises and
  • the consequence.
It generates an argumentation sentence which states that the premises imply the consequence.

This command is intended to be used in conjunction with the athm/aproof environments, the \llabel/\lref commands, and the \cfadd command.

Examples

The following is an example document that shows how to use the \argument command:

Let us go through some examples that illustrate how this command is used in the document. The document starts with a definition that introduces some notation.

\newcommand{\BoundedSeqs}{\cfadd{def:boundedseq}\ell^\infty}

...

\begin{definition}
  \label{def:boundedseq}
  We denote by $\BoundedSeqs$ the set which satisfies
  \begin{equation}
    \BoundedSeqs
    = 
    \{(a=(a_n)_{n\in\N}\colon\N\to\R)\colon \sup\{\abs{a_n}\colon n\in\N\} < \infty\}.
  \end{equation}
\end{definition}
Definition 1. We denote by $\ell^\infty$ the set which satisfies $$ \ell^\infty = \{(a=(a_n)_{n\in\mathbb N}\colon\mathbb N\to\mathbb R)\colon \sup\{\lvert a_n\rvert\colon n\in\mathbb N\} < \infty\}.\tag{1} $$

Note how \cfadd is used in the command for the notation to ensure that the \cfload/\cfout and \argument commands can reference this definition automatically later.

\begin{athm}{lemma}{lem:monoconv}
  Let $a\in\BoundedSeqs$ 
  and assume that 
    for all 
      $n\in\N$ 
    it holds that 
      $a_{n+1}\geq a_n$ \cfload. 
  Then 
    $a$ converges
  and
  \begin{equation}
    \lim_{n\to\infty}a_n = \sup(\{a_n\colon n\in\N\})
    \ifnocf.
  \end{equation}
  \cfout[.]
\end{athm}
Lemma 2. Let $a\in\ell^\infty$ and assume that for all $n\in\mathbb N$ it holds that $a_{n+1}\geq a_n$ (cf. Definition 1). Then $a$ converges and $$ \lim_{n\to\infty}a_n = \sup(\{a_n\colon n\in\mathbb N\}).\tag{2} $$

The \cfload command after the first sentence adds the (cf. Definition 1). The \cfout command after the second sentence doesn't do anything in this case, but it is still usually a good idea to add it: If the second sentence is changed later to reference another definition, you do not have to remember to add the \cfout command.

\begin{aproof}
  Throughout this proof let
  \begin{equation}
    \llabel{sup}
    L = \sup(\{a_n\colon n\in\N\})\dott
  \end{equation}
  \argument{
    \lref{sup};
  } {
    that for all $n\in\N$ it holds that
    \begin{equation}
      \llabel{lim1}
      a_n\leq L\dott
    \end{equation}
  }
Proof of Lemma 2. Throughout this proof let $$ L = \sup(\{a_n\colon n\in\mathbb N\}).\tag{3} $$ Observe that (3) ensures that for all $n\in\mathbb N$ it holds that $$ a_n\leq L.\tag{4} $$

Using the aproof environment automatically adds the Proof of Lemma 2 heading. The labels defined with \llabel are local to the proof, so the same labels can be used in different proofs. The first instance of the \argument command generates the sentence Observe that (3) ensures ....

Note the use of \dott at the end of the sentence, where the period . is supposed to go. This is because the \argument command automatically adds the (cf. ...) at the end of the sentence, if necessary. \dott outputs a . only if no references need to be added (if you use the eqn environment, you can use a normal period . instead).

\argument{
  \lref{sup};
  the assumption that $a\in\BoundedSeqs$;
} {
  that 
  \llabel{Lfin}
  $
    L<\infty
  $\dott
}
Next, note that (3) and the assumption that $a\in\ell^\infty$ imply that $L<\infty$.

Note that, even though this sentence contains no display, we still add a local label, so we can reference the consequence in the following sentence.

\argument{
  \lref{sup};
  \lref{Lfin};
} {
  that for all $\eps\in(0,\infty)$ there exists $m\in\N$ such that 
  \begin{equation}
    \llabel{a1}
    a_m>L-\eps\dott 
  \end{equation}
}
Combining this and (3) shows that for all $\varepsilon\in(0,\infty)$ there exists $m\in\mathbb N$ such that $$a_m>L-\varepsilon.\tag{5}$$

Note that the \argument command recognizes that \lref{Lfin} references the previous sentence, so it uses this. Instead of using the Combining this and ... shows form for the argumentation sentence, the command might also generate This and ... show. The choice is made randomly among all forms that are possible for the given number and types of premises.

Issues

Starting a new sequence of argumentation sentences

At certain places inside a proof, it is desirable to start a new sequence of argumentation sentences. 
\argument{
  \lref{eq2}
} {
  \lref{it1}\dott
}
\argument{
  the assumption that $X$ is a standard normal random variable
} {
  $\Exp[\abs{Y}]<infty$
}
This establishes item (i). Moreover, note that the assumption that $X$ is a standard normal variable ensures that $\mathbb E[\lvert Y\rvert]<\infty$.
This can be achieved with the \startnewargseq command: 
\argument{
  \lref{eq2}
} {
  \lref{it1}\dott
}
\startnewargseq
\argument{
  the assumption that $X$ is a standard normal random variable
} {
  $\Exp[\abs{Y}]<infty$
}
This establishes item (i). Note that the assumption that $X$ is a standard normal variable ensures that $\mathbb E[\lvert Y\rvert]<\infty$.

Forcing plurals

In argumentation sentences like below, the command decides whether to use the plural form of the verb based on the number of premises. But this can give the wrong result if one of the premises is already plural: 
\argument{
  \lref{eq2};
} {
  that \llabel{fdiff}
  $f$ is differentiable\dott
}
\argument{
  \lref{fdiff};
  \lref{eq4};
} {
  that \llabel{gdiff}
  $g$ is differentiable\dott
}
\argument{
  \itref{lem:aux}{it:1,it:2};
} {
  that $\sup_{x\in\R}\abs{g(x)}<\infty$\dott
}
Moreover, note that (2) ensures that $f$ is differentiable. This and (4) show that $g$ is differentiable. In addition, observe that items (i) and (ii) in Lemma 3 establishes that $\sup_{x\in\mathbb R} \lvert g(x)\rvert < \infty$.
In these cases, you can use the plural key in the optional argument of the \argument command: 
\argument{
  \itref{lem:aux}{it:1,it:2};
}[plural]{
  that $\sup_{x\in\R}\abs{g(x)}<\infty$\dott
}
In addition, observe that items (i) and (ii) in Lemma 3 establish that $\sup_{x\in\mathbb R} \lvert g(x)\rvert < \infty$.

Forcing the choice of verbs

Sometimes it might be desirable to limit the choice of verbs that the command can use. This can be achieved with the verbs=value key in the optional argument of the \argument command. Here, value is a sequence of letters from s, i, n, d, e, and p, standing for show(s), imply/implies, ensure(s), demonstrate(s), establish(es), and prove(s), respectively. 
\argument{
  the fundamental theorem of calculus
}[verbs=ep]{ % Only use "establishes" or "proves"
  \lref{it1}
}

Unless otherwise noted, all LaTeX snippets on this site are released under the Zero-Clause BSD (0BSD) license. You may copy them into your documents without attribution or including any license. No warranty.