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 APPEND: |- DeclAssum example_qsort_decls env ⇒ Eval env (Var "APPEND") ((LIST_TYPE a --> LIST_TYPE a --> LIST_TYPE a) $++) Definition of refinement invariant: |- ∀a b x_2 x_1 v. PAIR_TYPE a b (x_2,x_1) v ⇔ ∃v1_1 v1_2. (v = Conv "Pair" [v1_1; v1_2]) ∧ a x_2 v1_1 ∧ b x_1 v1_2 Certificate theorem for PART: |- DeclAssum example_qsort_decls env ⇒ Eval env (Var "PART") (((a --> BOOL) --> LIST_TYPE a --> LIST_TYPE a --> LIST_TYPE a --> PAIR_TYPE (LIST_TYPE a) (LIST_TYPE a)) PART) Certificate theorem for PARTITION: |- DeclAssum example_qsort_decls env ⇒ Eval env (Var "PARTITION") (((a --> BOOL) --> LIST_TYPE a --> PAIR_TYPE (LIST_TYPE a) (LIST_TYPE a)) PARTITION) Certificate theorem for QSORT: |- DeclAssum example_qsort_decls env ⇒ Eval env (Var "QSORT") (((a --> a --> BOOL) --> LIST_TYPE a --> LIST_TYPE a) QSORT) Definition of declaration list: |- example_qsort_decls = [Dtype [(["a"],"list", [("Cons",[Tvar "a"; Tapp [Tvar "a"] "list"]); ("Nil",[])])]; Dletrec [("APPEND","v3", Fun "v4" (Mat (Var "v3") [(Pcon "Nil" [],Var "v4"); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Con "Cons" [Var "v2"; App Opapp (App Opapp (Var "APPEND") (Var "v1")) (Var "v4")])]))]; Dtype [(["a"; "b"],"prod",[("Pair",[Tvar "a"; Tvar "b"])])]; Dletrec [("PART","v3", Fun "v4" (Fun "v5" (Fun "v6" (Mat (Var "v4") [(Pcon "Nil" [],Con "Pair" [Var "v5"; Var "v6"]); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], If (App Opapp (Var "v3") (Var "v2")) (App Opapp (App Opapp (App Opapp (App Opapp (Var "PART") (Var "v3")) (Var "v1")) (Con "Cons" [Var "v2"; Var "v5"])) (Var "v6")) (App Opapp (App Opapp (App Opapp (App Opapp (Var "PART") (Var "v3")) (Var "v1")) (Var "v5")) (Con "Cons" [Var "v2"; Var "v6"])))]))))]; Dlet (Pvar "PARTITION") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (App Opapp (App Opapp (Var "PART") (Var "v1")) (Var "v2")) (Con "Nil" [])) (Con "Nil" [])))); Dletrec [("QSORT","v7", Fun "v8" (Mat (Var "v8") [(Pcon "Nil" [],Con "Nil" []); (Pcon "Cons" [Pvar "v6"; Pvar "v5"], Let "v3" (App Opapp (App Opapp (Var "PARTITION") (Fun "v4" (App Opapp (App Opapp (Var "v7") (Var "v4")) (Var "v6")))) (Var "v5")) (Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], App Opapp (App Opapp (Var "APPEND") (App Opapp (App Opapp (Var "APPEND") (App Opapp (App Opapp (Var "QSORT") (Var "v7")) (Var "v2"))) (Con "Cons" [Var "v6"; Con "Nil" []]))) (App Opapp (App Opapp (Var "QSORT") (Var "v7")) (Var "v1")))]))]))]]