Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Elpi Integration

⚠️ Work in Progress: This section is under development.

This chapter covers using Elpi for metaprogramming and automation in Ursus.

Topics to be Covered

Elpi Basics

  • What is Elpi
  • Lambda Prolog
  • Coq-Elpi integration
  • Basic syntax

Ursus Elpi Predicates

  • Contract predicates
  • Function predicates
  • Type predicates
  • Proof predicates

Custom Tactics

  • Tactic definition
  • Tactic composition
  • Tactic debugging

Code Generation

  • Template-based generation
  • AST manipulation
  • Boilerplate automation

Proof Automation

  • Proof search
  • Lemma application
  • Rewriting automation
  • Decision procedures

Elpi in Ursus

Use Cases

Code Generation

  • Contract boilerplate
  • Interface generation
  • Accessor functions

Proof Automation

  • Invariant proofs
  • Simulation proofs
  • Refinement proofs

Analysis

  • Dependency analysis
  • Type inference
  • Dead code detection

Elpi Examples

Simple Tactic

Elpi Tactic solve_simple.
Elpi Accumulate lp:{{
  solve _ _ :- coq.ltac.all (coq.ltac.open solve_simple).
}}.
Elpi Typecheck.

Code Generator

Elpi Command generate_accessors.
Elpi Accumulate lp:{{
  % Generate getter/setter for field
}}.
Elpi Typecheck.

Coming Soon

This section will include:

  • Elpi tutorial
  • Ursus predicates reference
  • Custom tactic examples
  • Code generation examples
  • Proof automation examples

Resources

  • Elpi: https://lpcic.github.io/coq-elpi/
  • Coq-Elpi Tutorial: https://lpcic.github.io/coq-elpi/tutorial_coq_elpi.html
  • Lambda Prolog: http://www.lix.polytechnique.fr/~dale/lProlog/

See Also