Add README

Co-authored-by: Kacper Korban <kacper.f.korban@gmail.com>
Co-authored-by: Dario Halilovic <dario.halilovic@epfl.ch>

Author: 3 people

README.md

@@ -0,0 +1,48 @@
+# StrictOrderSolver
+
+Complete solver for strict orders (transitive+irreflexive relations) for Rocq.
+
+## Usage
+
+The solver works for any relation that implements the [`Transitive`](https://rocq-prover.org/doc/V9.1.0/corelib/Corelib.Classes.RelationClasses.html#Transitive) and [`Irreflexive`](https://rocq-prover.org/doc/V9.1.0/corelib/Corelib.Classes.RelationClasses.html#Irreflexive) classes. These are implicitly implemented if you instead implement the [`StrictOrder`](https://rocq-prover.org/doc/V9.1.0/corelib/Corelib.Classes.RelationClasses.html#StrictOrder) class.
+
+To invoke the solver, use `strict_order rel`, where `rel` is your strict order relation.
+
+The solver will close the goal in two cases:
+
+1. If your goal is of the form `rel a b` and it is provable from your `rel c d` premises
+2. If your `rel c d` premises lead to a contradiction
+
+See [Tests.v](./Tests.v) for example usages and supported use-cases.
+
+```rocq
+From Ltac2 Require Import Ltac2.
+From StrictOrderSolver Require Import Solver.
+From Stdlib Require Import Classes.RelationClasses.
+
+Axiom rel : nat -> nat -> Prop.
+Instance SO : StrictOrder rel. Admitted.
+
+Goal forall a b c d e,
+   rel a e -> rel a b -> rel c d -> rel b c -> rel a d.
+Proof.
+   intros.
+   strict_order rel.
+Qed.
+```
+
+## Installation
+
+1. Pin [opam](https://opam.ocaml.org/) dependency source
+
+```sh
+opam pin add --no-action strict-order-solver.0.1.0 https://github.com/epfl-systemf/StrictOrderSolver.git
+```
+
+2. Install as a dependency (or add `strict-order-solver` to your `dune-project`/`.opam` file with the `0.1.0` version selected)
+
+```sh
+opam install strict-order-solver
+```
+
+3. Add `StrictOrderSolver` to your Rocq theories (in dune, it is the `rocq.theory (theories)` stanza)