The proof is trivial (revisited)

The goal of this lecture note is to revisit the chapter about The proof is trivial (variations on a theme) in Week 04 in the light of OCaml’s data types.

Resources

• The OCaml code for the present lecture note (latest version: 15 Oct 2022).

The BNF of proofs

We consider the following BNF, where the notation {something}? means “zero or one occurrence of something”:

<proof>                             ::= The proof is trivial! <capitalized-adverb> <phrasal-verb-in-imperative-form> <adjective-with-a-matching-article> <noun-of-set> <in-relation-to> {<adjective>}? <noun-of-elements> {, <closing_qualifier>}?

<capitalized-adverb>                ::= Just | Simply | ...

<phrasal-verb-in-imperative-form>   ::= view the problem as | biject it to | ...

<adjective-with-a-matching-article> ::= a continuous | an open | ...

<noun-of-set>                       ::= complexity class | topological space | ...

<in-relation-to>                    ::= whose elements are | over

<adjective>                         ::= exact | skew-symmetric | ...

<noun-of-elements>                  ::= monoids | combinatorial games | ...

<closing_qualifier>                 ::= basically | symmetrically | ...

The data type for proofs

In the accompanying resource file, the BNF is implemented as an OCaml data type:

type capitalized_adverb =
  Capitalized_adverb of string;;

type phrasal_verb_in_imperative_form =
  Phrasal_verb of string;;

type article_and_adjective =
  Article_and_adjective of string;;

type noun_of_set =
  Noun_of_set of string;;

type in_relation_to =
  In_relation_to of string;;

type adjective =
  Adjective of string;;

type noun_of_elements =
  Noun_of_elements of string;;

type closing_qualifier =
  Closing_qualifier of string;;

type proof =
  Proof of capitalized_adverb * phrasal_verb_in_imperative_form * (article_and_adjective * noun_of_set) * in_relation_to * (adjective option * noun_of_elements) * closing_qualifier option;;

The resource file also contains a generator of random proofs and the following unparser:

let show_proof p =
  match p with
  | Proof (Capitalized_adverb ca,
           Phrasal_verb pviif,
           (Article_and_adjective aaa,
            Noun_of_set nos),
           In_relation_to irt,
           (oa,
            Noun_of_elements noe),
           ocq) ->
     let a = (match oa with
              | Some (Adjective a) ->
                 a ^ " "
              | None ->
                 "")
     and cq = (match ocq with
               | Some (Closing_qualifier cq) ->
                  ", " ^ cq
               | None ->
                  "")
     in "The proof is trivial!  " ^ ca ^ " " ^ pviif ^ " " ^ aaa ^ " " ^ nos ^ " " ^ irt ^ " " ^ a ^ noe ^ cq ^ ".";;

The point

The grammatical correctness of a proof corresponds to the type correctness of its OCaml representation.

Resources

• The OCaml code for the present lecture note (latest version: 15 Oct 2022).

Version

Created [15 Oct 2022]