Proof search using unification hints

encoding.lp

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;

lambdapi.pkg

package_name = struct
root_path = struct

structs.lp

/// # 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);