Skip to content

Instantly share code, notes, and snippets.

Created July 21, 2022 14:32
Show Gist options
  • Save gabrielhdt/25d4492421267d4dc041b4bafe7d8377 to your computer and use it in GitHub Desktop.
Save gabrielhdt/25d4492421267d4dc041b4bafe7d8377 to your computer and use it in GitHub Desktop.
Proof search using unification hints
constant symbol Set: TYPE;
injective symbol El : Set → TYPE;
notation El prefix 1;
constant symbol o : Set;
injective symbol Prf : El o → TYPE;
notation Prf prefix 1;
constant symbol &-> : Set → Set → Set;
notation &-> infix right 7;
rule El $a &-> $b ↪ El $a → El $b;
constant symbol &=> : El (o &-> o &-> o);
notation &=> infix right 7;
rule Prf $a &=> $b ↪ Prf $a → Prf $b;
constant symbol all (dom: Set): El ((dom &-> o) &-> o);
rule Prf all $dom (λ x, $p.[x]) ↪ Π z: El $dom, Prf $p.[z];
/// The type of inhabited types
constant symbol I : TYPE;
/// `inhabit S x` states that encoded type `S` is inhabited by `x`.
constant symbol inhabit (S: Set) (_: El S): I;
/// `# witness` returns the type shown inhabited by `witness`.
symbol # : I → Set;
notation # prefix 2;
rule # inhabit $e _ ↪ $e;
injective symbol W : Set → TYPE;
constant symbol w (e: Set): W e;
/// `Inhabitedp e` asserts whether [e] is an inhabited type code.
constant symbol Inhabitedp [i: I] (_: W # i): TYPE;
package_name = struct
root_path = struct
/// # Unification rules as a proof search engine.
require open struct.encoding;
/// ## _ad-hoc_ polymorphism
/// Unification rules can be used to find instances of some structure.
/// In the following, we define the encoded types of *magmas*, provide
/// instances of these magmas and show that we can define an overloaded
/// operator `<>` on magmas. Magmas are defined as *fully bundled* structures,
/// that is, the type of magmas is not parametrised by the carrier.
/// We define the encoded type of _magmas_. A magma is a carrier with a binary
/// (stable) operator. We also define the constructor `mkMagma`.
constant symbol magma : Set;
constant symbol mkMagma (sort: Set) (_: El sort &-> sort &-> sort): El magma;
/// `sort m` returns the carrier of the magma `m`.
symbol sort (_: El magma): Set;
rule sort (mkMagma $s _) ↪ $s;
/// `x <> y` is the binary operation on elements of a magma `m` such that
/// `x` and `y` are in the carrier of `m`.
symbol <> [m: El magma]: El (sort m &-> sort m &-> sort m);
notation <> infix left 4;
rule @<> (mkMagma _ $op) ↪ $op;
/// Define the encoded natural numbers
constant symbol nat: Set;
constant symbol zero: El nat;
constant symbol succ : El (nat &-> nat);
/// Define a binary operation
symbol + : El (nat &-> nat &-> nat);
rule + (succ $n) $m ↪ succ (+ $n $m);
rule + zero $m ↪ $m;
/// Define the magma `(N, +)`
symbol mNat+ ≔ mkMagma nat +;
/// and the unification rule that gives a canonical solution.
unif_rule sort $m ≡ nat ↪ [$m ≡ mNat+];
type zero <> zero;
assert ⊢ ((succ zero) <> zero) ≡ succ zero;
/// In the first assertion above, the unification problem
/// `sort ?m ≡ nat` is generated by the application of `<>` to `zero`.
/// The unification rule allows to instantiate `?m` with the magma `mNat+`.
/// The second assertion shows that `<>` can be computationally _ad-hoc_
/// polymorphic: the implementation of `<>` for natural numbers is selected.
/// Define a second magma: the reals with a product, to see how _ad-hoc_
/// polymorphism works.
constant symbol reals: Set;
constant symbol zR : El reals;
symbol * : El (reals &-> reals &-> reals);
/// Define the magma `(R, *)` and the unification rule
symbol mReals* ≔ mkMagma reals *;
unif_rule sort $m ≡ reals ↪ [$m ≡ mReals*];
/// Now we have overloading at type level (and computational level as seen
/// before)
type zR <> zR;
/// ## Inhabitation
/// Unification rules can also be used to provide canonical inhabitants.
/// The term `Inhabitedp (w e)` type checks whenever the unification problem
/// `# ?x ≡ nat` has a solution where `# (inhabit s e) = s`. Therefore,
/// in order to type check `Inhabited (w e)` without manual intervention,
/// it is enough to declared the unification hint `# $x ≡ s ↪ $x ≡ inhabit s e`,
/// where `e` is indeed an element of `El s`.
unif_rule # $x ≡ nat ↪ [ $x ≡ inhabit nat zero ];
symbol inhabited_nat : Inhabitedp (w nat);
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment