Definition of refinement invariant:

|- (∀a x_2 x_1 v.
      LIST_TYPE a (x_2::x_1) v ⇔
      ∃v2_1 v2_2.
        (v = Conv "Cons" [v2_1; v2_2]) ∧ a x_2 v2_1 ∧
        LIST_TYPE a x_1 v2_2) ∧
   ∀a v. LIST_TYPE a [] v ⇔ (v = Conv "Nil" [])

Certificate theorem for MEM:

|- DeclAssum example_regexp_matcher_decls env ∧ EqualityType a ⇒
   Eval env (Var "MEM") ((a --> LIST_TYPE a --> BOOL) MEM)

Definition of refinement invariant:

|- (∀a x_6 v.
      REGEXP_TYPE a (Repeat x_6) v ⇔
      ∃v5_1. (v = Conv "Repeat" [v5_1]) ∧ REGEXP_TYPE a x_6 v5_1) ∧
   (∀a x_5 x_4 v.
      REGEXP_TYPE a (x_5 # x_4) v ⇔
      ∃v4_1 v4_2.
        (v = Conv "Then" [v4_1; v4_2]) ∧ REGEXP_TYPE a x_5 v4_1 ∧
        REGEXP_TYPE a x_4 v4_2) ∧
   (∀a x_3 x_2 v.
      REGEXP_TYPE a (x_3 + x_2) v ⇔
      ∃v3_1 v3_2.
        (v = Conv "Or" [v3_1; v3_2]) ∧ REGEXP_TYPE a x_3 v3_1 ∧
        REGEXP_TYPE a x_2 v3_2) ∧
   (∀a x_1 v.
      REGEXP_TYPE a (Charset x_1) v ⇔
      ∃v2_1. (v = Conv "Charset" [v2_1]) ∧ LIST_TYPE a x_1 v2_1) ∧
   ∀a v. REGEXP_TYPE a Epsilon v ⇔ (v = Conv "Epsilon" [])

Definition of refinement invariant:

|- (∀a x_1 v.
      OPTION_TYPE a (SOME x_1) v ⇔
      ∃v2_1. (v = Conv "Some" [v2_1]) ∧ a x_1 v2_1) ∧
   ∀a v. OPTION_TYPE a NONE v ⇔ (v = Conv "None" [])

Certificate theorem for match:

|- DeclAssum example_regexp_matcher_decls env ∧ EqualityType a ⇒
   Eval env (Var "match")
     ((LIST_TYPE (REGEXP_TYPE a) --> LIST_TYPE a -->
       OPTION_TYPE (LIST_TYPE (REGEXP_TYPE a)) --> BOOL) match)

Definition of declaration list:

|- example_regexp_matcher_decls =
   [Dtype
      [(["a"],"list",
        [("Cons",[Tvar "a"; Tapp [Tvar "a"] "list"]); ("Nil",[])])];
    Dletrec
      [("MEM","v3",
        Fun "v4"
          (Mat (Var "v4")
             [(Pcon "Nil" [],Val (Lit (Bool F)));
              (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
               Log Or (App Equality (Var "v3") (Var "v2"))
                 (App Opapp (App Opapp (Var "MEM") (Var "v3"))
                    (Var "v1")))]))];
    Dtype
      [(["a"],"regexp",
        [("Repeat",[Tapp [Tvar "a"] "regexp"]);
         ("Then",[Tapp [Tvar "a"] "regexp"; Tapp [Tvar "a"] "regexp"]);
         ("Or",[Tapp [Tvar "a"] "regexp"; Tapp [Tvar "a"] "regexp"]);
         ("Charset",[Tapp [Tvar "a"] "list"]); ("Epsilon",[])])];
    Dtype [(["a"],"option",[("Some",[Tvar "a"]); ("None",[])])];
    Dletrec
      [("match","v13",
        Fun "v14"
          (Fun "v15"
             (Mat (Var "v13")
                [(Pcon "Nil" [],
                  Mat (Var "v14")
                    [(Pcon "Nil" [],Val (Lit (Bool T)));
                     (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
                      Val (Lit (Bool F)))]);
                 (Pcon "Cons" [Pvar "v12"; Pvar "v11"],
                  Mat (Var "v12")
                    [(Pcon "Epsilon" [],
                      App Opapp
                        (App Opapp (App Opapp (Var "match") (Var "v11"))
                           (Var "v14")) (Var "v15"));
                     (Pcon "Charset" [Pvar "v5"],
                      Mat (Var "v14")
                        [(Pcon "Nil" [],Val (Lit (Bool F)));
                         (Pcon "Cons" [Pvar "v4"; Pvar "v3"],
                          Log And
                            (App Opapp
                               (App Opapp (Var "MEM") (Var "v4"))
                               (Var "v5"))
                            (App Opapp
                               (App Opapp
                                  (App Opapp (Var "match") (Var "v11"))
                                  (Var "v3")) (Con "None" [])))]);
                     (Pcon "Or" [Pvar "v7"; Pvar "v6"],
                      Log Or
                        (App Opapp
                           (App Opapp
                              (App Opapp (Var "match")
                                 (Con "Cons" [Var "v7"; Var "v11"]))
                              (Var "v14")) (Var "v15"))
                        (App Opapp
                           (App Opapp
                              (App Opapp (Var "match")
                                 (Con "Cons" [Var "v6"; Var "v11"]))
                              (Var "v14")) (Var "v15")));
                     (Pcon "Then" [Pvar "v9"; Pvar "v8"],
                      App Opapp
                        (App Opapp
                           (App Opapp (Var "match")
                              (Con "Cons"
                                 [Var "v9";
                                  Con "Cons" [Var "v8"; Var "v11"]]))
                           (Var "v14")) (Var "v15"));
                     (Pcon "Repeat" [Pvar "v10"],
                      If
                        (App Equality (Var "v15")
                           (Con "Some"
                              [Con "Cons"
                                 [Con "Repeat" [Var "v10"];
                                  Var "v11"]])) (Val (Lit (Bool F)))
                        (Log Or
                           (App Opapp
                              (App Opapp
                                 (App Opapp (Var "match") (Var "v11"))
                                 (Var "v14")) (Var "v15"))
                           (App Opapp
                              (App Opapp
                                 (App Opapp (Var "match")
                                    (Con "Cons"
                                       [Var "v10";
                                        Con "Cons"
                                          [Con "Repeat" [Var "v10"];
                                           Var "v11"]])) (Var "v14"))
                              (Con "Some"
                                 [Con "Cons"
                                    [Con "Repeat" [Var "v10"];
                                     Var "v11"]]))))])])))]]