blob: 0b85ee02da2fc6ec590045e5f18bb295f73db1cb (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
|
+++
title = "Subset Types and Variations"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3b3c"]
forwardlinks = []
zettelid = "3b3d"
+++
`refine` can be used to define functions that take in and return subset
types, by allowing you to replace placeholders with underscores, which
can be proven afterwards. Together with powerful proof automation, this
can be a nice way to define these dependent functions in a more similar
way that they would be defined in Haskell or ML.
However, `Program` is a term in Galina which can be used to prove these
without `refine`, however, `refine` gives more control over how the
proof is done.
The `sumbool` type is the type that can return a proof of either type in
it's constructor.
`if then else` is actually overloaded in Coq and can work for any
two-constructor `Inductive` type. This means it can be used with
`sumbool` as well. When extracting `sumbool` to OCaml code, it uses
`Left` and `Right` by default, however, it is better to use `true` and
`false` in `bool` instead, which are built into OCaml. This can easily
be done by telling Coq how it should extract the `sumbool` type.
`sumor` is another type, which can either return a value of type A, or a
proof of type B, which is written as the following: `A + {B}`.
|
