A short introduction to Higher-Order Logic Programming

%%  A quick introduction to Prolog


% Prolog is a programming language rooted in classical logic.
% Its most distinguishing features are *search* and *unification*

% A Prolog program consists of *predicates*. A predicate defines a relation between its arguments.
%
% A predicate has
% - a name (atom)
% - 0..n arguments that are Prolog terms
%
% A predicate consist of an arbitrary number of clauses. These denote /alternatives/:
% If any clause is true, the whole predicate is true.
%
% In its simplest form, a predicate relates *atoms*:

mentor(sokrates, plato).

mentor(plato, aristotle).

mentor(aristotle, alexander-the-great).

% Terms related by a predicate may also be *variables*.
% A variable starts with an upper-case letter or `_` (if the variable is unused)
%
% So far we've only seen *facts*. A fact is a clause with an empty body.
% When the body is non-empty, the clause is called a *rule*.
% A rule is a clause of the form
%
% Head :- Body.

mortal(X) :-
    human(X).

% In fact we can think of facts as special cases of rules, using the builtin 0-ary predicate `true`:

mentor(parmenides, zeno) :- true.

% is equivalent to
% mentor(parmenides, zeno).

% Interaction with a Prolog program is done via *queries*.
% A query is a Prolog term that may contain variables. Variables in a query are existentially quantified.
%
% In response to a query, Prolog answers with a logically equivalent answer:
%
% ?- mentor(sokrates, plato).
% true.
%
% ?- mentor(parmenides, X).
% X = zeno.

% It is worthwhile to examine what exactly Prolog means by a term like `X = zeno`:
% `=` is a binary predicate that holds iff both its arguments can be *unified*
%
% ?- sokrates = plato.
% false.
%
% ?- plato = X.
% X = plato.
%
% If multiple clauses unify with a goal, the alternatives are tried on *backtracking*

human(sokrates).
human(plato).
human(aristotle).

% ?- mortal(X).
% X = sokrates ;
% X = plato    ;
% X = aristotle.

% Predicates may also be recursive:

influenced(X, Y) :-
    mentor(X,Y).

influenced(X, Y) :-
    mentor(X, Z),
    influenced(Z, Y).

% Note how variables in the body of a clause are existentially quantified.

% ?- influenced(sokrates, X).
% X = plato ;
% X = aristotle ;
% X = alexander-the-great.

% A simple representation of directed graphs:
adj(a,b).
adj(b,c).
adj(c,a).
adj(c,d).

path(X, Y) :-
    adj(X, Z),
    path(Z, Y).

% Some additional examples
append([], Y, Y).
append([X | Xs], Ys, [X | Zs]) :-
    append(Xs, Ys, Zs).

member(X, [X |_]).
member(X, [_ | L]) :-
    member(X, L).

%% Logical Foundations
% ====================
%
% Prolog is based on the logic of first-order horn clauses.
%
% A clause is a disjunction of literals (atoms their negations), e.g.:
%
% a ∨ b ∨ (¬ c) ∨ (¬ b)
%
% Equivalently in set notation:
%
% { a, b, ¬ c, ¬ b }
%
% A Prolog program is a conjunction of clauses, i.e. a formula in
% Clause Normal Form (CNF).

rainy.
cold.

snowy :-
    rainy,
    cold.

% This Program can be translated into a formula in CNF:
% We interpret `:-` as an implication ←
%
% rainy ∧ cold ∧ (snowy ← (rainy ∧ cold))    % We swap ← for →
% rainy ∧ cold ∧ ((rainy ∧ cold) → snowy)    % We apply material implication
% rainy ∧ cold ∧ (¬ (rainy ∧ cold) ∨ snowy)  % De Morgan
% rainy ∧ cold ∧ (¬ rainy ∨ ¬ cold ∨ snowy)

% We get a set of clauses:
% 1. { ¬ rainy , ¬ cold , snowy }
% 2. { rainy }
% 3. { cold }

% One very important property presents itself here: All clauses of a
% Prolog program have at most one positive (non-negated) literal.
% A clause that observes that property is called a horn clause.
%
% To evaluate a query ⇔ prove that a query is satisfiable relative to
% a program, Prolog uses a resolution calculus.
%
% A resolution calculus is a proof calculus that works on formulae in CNF.
% In its most basic form it looks like this:
%
% A ∨ C    (¬ B) ∨ D    σ = mgu(A,B)
% ==================================
%       σ(C) ∨ σ(D)
%
% Horn clauses interact particulary nicely with this rule:
% When two horn clauses are resolved, the resolvent is again a horn clause.
%
% An example proof:
% We want to prove the goal
% ?- snowy.
%
% Resolution is a refutation calculus. To prove a goal, we show that
% its negation is unsatisfiable.
%
% We add the negated goal as a clause:
% { ¬ snowy }
%
% Now we do resolution:
%
% { ¬ snowy } + { ¬ rainy, ¬ cold, snowy } ⇒ { ¬ rainy, ¬ cold }
% { rainy }   + { ¬ rainy, ¬ cold }        ⇒ { ¬ cold }
% { cold }    + { ¬ cold }                 ⇒ ∅

% We have reached the empty clause, meaning our proof is done

% Another example:
%
% Goal:
% ?- mortal(X).
%
% Variables in a Query are existentially quantified.
% That means our goal corresponds to the following formula:
%
% ∃ X. mortal(X)
%
% We need to negate and translate this into CNF:
%
% ¬ ∃ X. mortal(X)
% [ V₁ / X ] ¬ mortal(X)    % where V₁ ∉ free(mortal(X))
% ¬ mortal(V₁)
%
% We get a goal clause:
%
% { ¬ mortal(V₁) }
%
% Program Clauses:
%
% 1. ∀ X. human(X) → mortal(X)
%    ⇒ [ V₂ / X ] human(X) → mortal(X)
%    ⇒ human(V₂) → mortal(V₂)
%    ⇒ (¬ human(V₂)) ∨ mortal(V₂)
%    ̂= { ¬ human(X), mortal(X) }
% 2. { human(sokrates) }
% 3. { human(plato) }
% 4. { human(aristotle) }
%
% Resolution:
%
% { ¬ mortal(V₁) } + { ¬ human(V₂), mortal(V₂) }  [ V₂ / V₁ ] ⇒ { ¬ human(V₂) }
% { ¬ human(V₂) } + { human(sokrates) }       [ sokrates / V₂ ] ⇒ ∅
%
% At this point, Prolog presents us with a satisfying substitution, namely
% X = sokrates.
%
% If we force backtracking, we get all other satisfying substitutions:
% { ¬ human(V₂) } + { human(plato) }          [ plato / V₂ ] ⇒ ∅
% { ¬ human(V₂) } + { human(aristotle) }  [ aristotle / V₂ ] ⇒ ∅
%
% If we backtrack again we are left with a set of clauses that doesn't
% allow us to derive the empty clause.
%
% { ¬ human(X) }
%
% Since nothing can be resolved, Prolog tells us that our goal is not satisfiable:
% false.

% From Prolog to λProlog
% λProlog adds some extensions to normal Prolog:
% - polymorphic typing
% - higher-order programming
% - hypothetical reasoning
%
% That makes the logic corresponding to λProlog that of higher-order hereditary harrop formulae.

%% Polymorphic Typing:
kind person type.

type sokrates person.
type plato person.
type zeno person.
type aristotle person.

pred mentor o:person o:person.
% this is roughly equivalent to
% `type mentor person -> person -> o.`
% where `o` is the type of propositions

mentor sokrates plato.
mentor plato aristotle.

pred influenced o:person o:person.
influenced X Y :-
    mentor X Y.

influenced X Y :-
    mentor X Z,
    influenced Z Y.

pred age o:person o:int.

age sokrates 70.
age plato 23.
age zeno 90.

pred older o:person o:person.
older X Y :-
  age X N,
  age Y M,
  N > M.

kind node type.
pred adj o:node o:node.
pred path o:node o:node.

path X Y :-
  adj X Z,
  path Z Y.

% Type constructors are also allowed:
kind mylist type -> type.

%% Higher-Order Programming:
%
% So far we've only seen a typed version of Prolog.
% λProlog adds another term constructor: lambda abstractions
% e.g.
%
% Id = x\ x

pred mentor-f i:(person -> person) o:person.
mentor-f F X :-
  mentor (F X) X.

pred map o:(A -> B) o:list A o:list B.
map _F nil nil.
map F (X :: L) ((F X) :: L1) :-
  map F L L1.

pred fold o:(A -> B -> B) o:list A o:B o:B.
fold _F nil B B.
fold F (X :: L) B (F X R) :-
  fold F L B R.

%% Hypothetical Reasoning
% λProlog allows scoped assumptions
%
% `rule => body` adds `rule` to the top of the program, then runs `body`.
% once `body` terminates `rule` is removed from the context

% Concrete Syntax:
kind lam type.
type lam-abs string -> lam -> lam.
type lam-app lam -> lam -> lam.
type lam-var string -> lam.

% de Bruijn:
kind db type.
type db-var int -> db.
type db-abs db -> db.
type db-app db -> db -> db.

pred depth o:int o:string.

pred lam->db o:lam i:int o:db.
lam->db (lam-app L R) D (db-app L1 R1) :-
  lam->db L D L1,
  lam->db R D R1.

lam->db (lam-abs V B) D (db-abs B1) :-
  D1 is D + 1,
  depth D V => lam->db B D1 B1.

lam->db (lam-var V) D (db-var I) :-
  depth N V,
  I is D - N - 1.

%% Scoped Quantification
% λProlog adds the term constructors `pi` and `sigma`, for universal/existential quantification.
% They are implemented as higher-order term constructors:
%
% pi x\ mentor sokrates x
%
% sigma y\ mentor y plato

pred all i:(A -> o) i:list A.
all _P nil.
all P (X :: L) :-
  P X,
  all P L.

pred some i:(A -> o) i:list A.
some P (X :: _L) :- P X.
some P (_X :: L) :- some P L.

%%% Explicit Quantification:

% All of the following are equivalent:
path X Y :- adj X Z, path Z Y.

path X Y :- sigma z\ adj X z, path z Y.

pi x\ pi y\
   (path x y :-
         sigma z\ adj x z, path z y).

%%% HOAS

kind tm, ty type.
type app tm -> tm -> tm.

% A lambda abstraction is just a function:
type abs (tm -> tm) -> tm.

type arrow ty -> ty -> ty.


% The typing rules showcase higher-order unification:
pred of i:tm o:ty.
of (app M N) T :-
  of M (arrow U T),
  of N U.

of (abs R) (arrow T U) :-
  pi x\ of x T => of (R x) U.

(* Elpi as an embedded meta-programming language for Coq *)
From elpi Require Import elpi.
Elpi Program introspection "".

(* We can query the coq environment from within elpi *)
Elpi Query lp:{{
  coq.locate "nat" GR,
  coq.locate "S" GRS
}}.

Definition x := 2.

Elpi Query lp:{{
  coq.locate "x" GR,
  coq.env.typeof GR Ty,
  GR = const C,
  coq.env.const C (some Body) TyC
}}.

(* We can also reference Coq Terms from elpi directly *)

Elpi Query lp:{{
  X = {{1}},
  N = {{nat}}
}}.

(** HOAS of Gallina Terms *)

(** `app` *)
(* type app list term -> term *)

Elpi Query lp:{{
  X = app [{{S}}, {{O}}]      
}}.

(** `fun` *)
(* type fun name -> term -> (term -> term) -> term *)

Definition foo := fun x => x + 1.

Elpi Query lp:{{
  coq.locate "foo" (const F),
  coq.env.const F (some Body) _
}}.

Elpi Query lp:{{
  fun `foo` T B = fun `bar` T B
}}.

(** `prod` *)
(* type prod name -> term -> (term -> term) -> term *)

Definition P := forall (n : nat), Prop.

Elpi Query lp:{{
  coq.locate "P" (const P),
  coq.env.const P (some Body) _    
}}.

(*
 * A loose reimplementation of the `Logic Programming` chapter of cpdt using coq-elpi.
 *)

From elpi Require Import elpi.

(* Addition as an inductive Property: *)
Inductive plusR : nat -> nat -> nat -> Prop :=
| PlusO : forall m, plusR O m m
| PlusS : forall n m r,
    plusR n m r
    -> plusR (S n) m (S r).

(* Notice how this mirrors the definition in {λ-,}Prolog: *)
Elpi Program plus "
kind nat type.
type zero nat.
type succ nat -> nat.

pred plus o:nat o:nat o:nat.
plus zero M M.
plus (succ N) M (succ R) :-
  plus N M R.
".
Elpi Typecheck.


Elpi Tactic add.
Elpi Accumulate "
pred add_p o:term o:term o:term o:term.
add_p {{O}} N N {{PlusO lp:N}}.
add_p {{S lp:N}} M {{S lp:P}} {{PlusS lp:N lp:M lp:P lp:SubProof}} :-
  add_p N M P SubProof.

solve (goal _Ctx _ {{plusR lp:N lp:M lp:P}} _ _ as G) GS :-
  add_p N M P Proof,
  refine Proof G GS.
solve _ _ :-
  coq.ltac.fail _ ""not an addition"".
".
Elpi Typecheck.

Goal exists x, plusR 4 x 7.
  eexists.
  elpi add.
Qed.

Goal exists x y, plusR x y 4.
  repeat eexists.
  elpi add.
Qed.

Require Import List.
Import ListNotations.

Section lengthR.
Variable A : Set.
Inductive lengthR : list A -> nat -> Prop :=
| lengthNil : lengthR nil O
| lengthCons : forall X Xs N,
    lengthR Xs N ->
    lengthR (cons X Xs) (S N).
End lengthR.

Print lengthR.
Elpi Tactic length.
Elpi Accumulate "
pred length i:term o:term o:term o:term.
length A {{nil}} {{O}} {{lengthNil lp:A}}.
length A {{cons lp:X lp:Xs}} {{S lp:N}} {{lengthCons lp:A lp:X lp:Xs lp:N lp:P}} :-
  length A Xs N P.

solve (goal _Ctx _ {{lengthR lp:A lp:L lp:N}} _ _ as G) GS :-
  length A L N P,
  refine P G GS.

solve _ _ :-
  coq.ltac.fail _ ""could not unify"".
".
Elpi Typecheck.

Elpi Query lp:{{
      length {{nat}} L {{3}} P
}}.

Goal exists l, lengthR nat l 4.
  eexists.
  elpi length.
  Unshelve.
  all: constructor.
Qed.

Elpi Tactic length_choose.
Elpi Accumulate "
pred choose i:term o:term.
choose {{nat}} {{O}}.
choose {{nat}} {{S lp:N}} :-
  choose {{nat}} N.
choose _T _ :-
  coq.ltac.fail _ ""Unsupported type "".

pred length-choose i:term o:term o:term o:term.
length-choose A {{nil}} {{O}} {{lengthNil lp:A}}.
length-choose A {{cons lp:X lp:Xs}} {{S lp:N}} {{lengthCons lp:A lp:X lp:Xs lp:N lp:P}} :-
  choose A X,
  length-choose A Xs N P.

solve (goal _Ctx _ {{lengthR lp:A lp:L lp:N}} _ _ as G) GS :-
  length-choose A L N P,
  refine P G GS.

solve _ _ :-
  coq.ltac.fail _ ""could not unify"".
".
Elpi Typecheck.

Goal exists l, lengthR nat l 4.
  eexists.
  elpi length_choose.
Qed.

Section appendR.
  Variable A : Set.
  Inductive appendR : list A -> list A -> list A -> Prop :=
  | appendNil : forall L,
        appendR nil L L
  | appendCons : forall X Xs Ys Zs,
      appendR Xs Ys Zs ->
      appendR (cons X Xs) Ys (cons X Zs).
End appendR.

Elpi Tactic append.
Elpi Accumulate "
pred append i:term o:term o:term o:term o:term.
append A {{nil}} L L {{appendNil lp:A lp:L}}.
append A {{cons lp:X lp:Xs}} Ys {{cons lp:X lp:Zs}} {{appendCons lp:A lp:X lp:Xs lp:Ys lp:Zs lp:P}} :-
       append A Xs Ys Zs P.

solve (goal _Ctx _ {{appendR lp:A lp:Xs lp:Ys lp:Zs}} _ _ as G) GS :-
  append A Xs Ys Zs P,
  refine P G GS.

solve _ _ :-
  coq.ltac.fail _ ""could not unify"".
".
Elpi Typecheck.

Goal forall L, appendR nat nil L L.
  intros.
  elpi append.
Qed.

Goal exists L, appendR nat [1 ; 2] L [1 ; 2 ; 3 ; 4].
  eexists.
  elpi append.
Qed.

Goal exists L X, appendR nat L [X] ([1 ; 2 ; 3 ]) /\ X = 3.
  eexists.
  eexists.
  split.
  - elpi append.
  - reflexivity.
Qed.

Elpi Tactic length_append.
Elpi Accumulate "
pred append i:term o:term o:term o:term o:term.
append A {{nil}} L L {{appendNil lp:A lp:L}}.
append A {{cons lp:X lp:Xs}} Ys {{cons lp:X lp:Zs}} {{appendCons lp:A lp:X lp:Xs lp:Ys lp:Zs lp:P}} :-
       append A Xs Ys Zs P.

pred length i:term o:term o:term o:term.
length A {{nil}} {{O}} {{lengthNil lp:A}}.
length A {{cons lp:X lp:Xs}} {{S lp:N}} {{lengthCons lp:A lp:X lp:Xs lp:N lp:P}} :-
  length A Xs N P.

solve (goal _Ctx _ {{appendR lp:A lp:Xs lp:Ys lp:Zs}} _ _ as G) GS :-
  append A Xs Ys Zs P,
  refine P G GS.

solve (goal _Ctx _ {{lengthR lp:A lp:L lp:N}} _ _ as G) GS :-
  length A L N P,
  refine P G GS.

solve _ _ :-
  coq.ltac.fail _ ""could not unify"".
".
Elpi Typecheck.

Inductive exp : Set :=
| Const : nat -> exp
| Var : exp
| Plus : exp -> exp -> exp.

Inductive eval (var : nat) : exp -> nat -> Prop :=
| EvalConst : forall n, eval var (Const n) n
| EvalVar : eval var Var var
| EvalPlus : forall e1 e2 n1 n2, eval var e1 n1
  -> eval var e2 n2
  -> eval var (Plus e1 e2) (n1 + n2).

Elpi Tactic eval.
Elpi Accumulate "
pred eval o:term o:term o:term o:term.
eval V {{Const lp:N}} N {{EvalConst lp:V lp:N}}.
eval V {{Var}} V {{EvalVar lp:V}}.
eval V {{Plus lp:E1 lp:E2}} {{lp:N1 + lp:N2}} {{EvalPlus lp:V lp:E1 lp:E2 lp:N1 lp:N2 lp:P1 lp:P2}} :-
  eval V E1 N1 P1,
  eval V E2 N2 P2.

solve (goal _Ctx _ {{eval lp:V lp:T lp:N}} _ _ as G) GS :-
  eval V T N P,
  refine P G GS.

".
Elpi Typecheck.

Elpi Query lp:{{
  eval V {{(Plus Var (Plus (Const 8) Var))}} {{(lp:V + (8 + lp:V))}} P
}}.

Example eval1 : forall var, eval var (Plus Var (Plus (Const 8) Var)) (var + (8 + var)).
intros.
elpi eval.
Qed.