rework README for coercion

apps/coercion/README.md

@@ -1,25 +1,80 @@
 # Coercion
 
-The `coercion` predicate enables to program Coq coercions in Elpi.
+The `coercion` app enables to program Coq coercions in Elpi.
 
-## Example of `coercion`
+This app is experimental.
+
+## The coercion predicate
+
+The `coercion` predicate lives in the database `coercion.db`
+
+```elpi
+% [coercion Ctx V Inferred Expected Res] is queried to cast V to Res
+% - [Ctx] is the context
+% - [V] is the value to be coerced
+% - [Inferred] is the type of [V]
+% - [Expected] is the type [V] should be coerced to
+% - [Res] is the result (of type [Expected])
+pred coercion i:goal-ctx, i:term, i:term, i:term, o:term.
+```
+
+By addings rules for this predicate one can recover from a type error, that is
+when `Inferred` and `Expected` are not unifiable.
+
+## Simple example of coercion
+
+This example maps `True : Prop` to `true : bool`, which is a function you
+cannot express in type theory, hence in the standard Coercion system.
 
 ```coq
 From elpi.apps Require Import coercion.
+From Coq Require Import Bool.
 
-Elpi Accumulate Coercion lp:{{
+Elpi Accumulate coercion.db lp:{{
 
-coercion _ {{ true }} {{ bool }} {{ Prop }} {{ True }}.
-coercion _ {{ false }} {{ bool }} {{ Prop }} {{ False }}.
+coercion _ {{ True }} {{ Prop }} {{ bool }} {{ true }}.
+coercion _ {{ False }} {{ Prop }} {{ bool }} {{ false }}.
 
 }}.
-Elpi Typecheck Coercion.
+Elpi Typecheck coercion. (* checks the elpi program is OK *)
 
-Check true : Prop.
-Check false : Prop.
+Check True && False.
 ```
 
-## Requirements
+## Example of coercion with proof automation
+
+This coercion enriches `x : T` to a `{x : T | P x}` by using
+`my_solver` to prove `P x`.
+
+```coq
+From elpi.apps Require Import coercion.
+From Coq Require Import Arith ssreflect.
+
+Ltac my_solver := trivial with arith.
+
+Elpi Accumulate coercion.db lp:{{
+
+coercion _ X Ty {{ @sig lp:Ty lp:P }} Solution :- std.do! [
+  % we unfold letins since the solver is dumb and the `as` in the second
+  % example introduces a letin
+  (pi a b b1\ copy a b :- def a _ _ b, copy b b1) => copy X X1,
+  % we build the solution
+  Solution = {{ @exist lp:Ty lp:P lp:X1 _ }},
+  % we call the solver
+  coq.ltac.collect-goals Solution [G] [],
+  coq.ltac.open (coq.ltac.call-ltac1 "my_solver") G [],
+].
 
-Appropriate version of Coq with support for coercion hooks
-https://github.com/coq/coq/pull/17794
+}}.
+Elpi Typecheck coercion.
+
+Goal {x : nat | x > 0}.
+apply: 3.
+Qed.
+
+Definition ensure_pos n : {x : nat | x > 0} :=
+  match n with
+  | O => 1
+  | S x as y => y
+  end.
+```

apps/coercion/_CoqProject.test

@@ -7,6 +7,7 @@
 -R tests    elpi.apps.coercion.tests
 
 tests/test_coercion.v
+tests/test_coercion_open.v
 tests/test_coercion_load.v
 
 -I src

apps/coercion/src/coq_elpi_coercion_hook.mlg

@@ -51,7 +51,7 @@ let add_coercion_hook =
 }
 
 VERNAC COMMAND EXTEND ElpiCoercion CLASSIFIED AS SIDEFF
-| #[ atts = any_attribute ] [ "Elpi" "AddCoercionHook" qualified_name(p) ] -> {
+| #[ atts = any_attribute ] [ "Elpi" "CoercionFallbackTactic" qualified_name(p) ] -> {
      let () = ignore_unknown_attributes atts in
      add_coercion_hook (snd p) }
 

apps/coercion/tests/test_coercion.v

@@ -1,27 +1,27 @@
 From elpi.apps Require Import coercion.
+From Coq Require Import Bool.
 
-Elpi Accumulate Coercion lp:{{
+Elpi Accumulate coercion.db lp:{{
 
-coercion _ {{ true }} {{ bool }} {{ Prop }} {{ True }}.
-coercion _ {{ false }} {{ bool }} {{ Prop }} {{ False }}.
+coercion _ {{ True }} {{ Prop }} {{ bool }} {{ true }}.
+coercion _ {{ False }} {{ Prop }} {{ bool }} {{ false }}.
 
 }}.
-Elpi Typecheck Coercion.
+Elpi Typecheck coercion.
 
-Check true : Prop.
-Check false : Prop.
+Check True && False.
 
 Parameter ringType : Type.
 Parameter ringType_sort : ringType -> Type.
 Parameter natmul : forall (R : ringType) (n : nat), (ringType_sort R).
 
-Elpi Accumulate Coercion lp:{{
+Elpi Accumulate coercion.db lp:{{
 
 coercion _ N {{ nat }} {{ ringType_sort lp:R }} {{ natmul lp:R lp:N }} :-
   coq.typecheck R {{ ringType }} ok.
 
 }}.
-Elpi Typecheck Coercion.
+Elpi Typecheck coercion.
 
 Section TestNatMul.
 

apps/coercion/tests/test_coercion_load.v

@@ -1,3 +1,3 @@
 Require Import test_coercion.
 
-Check true : Prop.
+Check True : bool.

apps/coercion/tests/test_coercion_open.v

@@ -0,0 +1,29 @@
+From elpi.apps Require Import coercion.
+From Coq Require Import Arith ssreflect.
+
+Ltac my_solver := trivial with arith.
+
+Elpi Accumulate coercion.db lp:{{
+
+coercion _ X Ty {{ @sig lp:Ty lp:P }} Solution :- std.do! [
+  % we unfold letins since the solve is dumb
+  (pi a b b1\ copy a b :- def a _ _ b, copy b b1) => copy X X1,
+  % we build the solution
+  Solution = {{ @exist lp:Ty lp:P lp:X1 _ }},
+  % we call the solver
+  coq.ltac.collect-goals Solution [G] [],
+  coq.ltac.open (coq.ltac.call-ltac1 "my_solver") G [],
+].
+
+}}.
+Elpi Typecheck coercion.
+
+Goal {x : nat | x > 0}.
+apply: 3.
+Qed.
+
+Definition add1 n : {x : nat | x > 0} :=
+  match n with
+  | O => 1
+  | S x as y => y
+  end.

apps/coercion/theories/coercion.v

@@ -1,8 +1,7 @@
 Declare ML Module "coq-elpi-coercion.plugin".
 From elpi Require Import elpi.
 
-Elpi Tactic Coercion.
-Elpi Accumulate lp:{{
+Elpi Db coercion.db lp:{{
 
 % predicate [coercion Ctx V Inferred Expected Res] used to add new coercion, with
 % - [Ctx] is the context
@@ -13,8 +12,14 @@ Elpi Accumulate lp:{{
 % Be careful not to trigger coercion as this may loop.
 pred coercion i:goal-ctx, i:term, i:term, i:term, o:term.
 
+}}.
+
+Elpi Tactic coercion.
+Elpi Accumulate lp:{{
+
 solve (goal Ctx _ Ty Sol [trm V, trm VTy]) _ :- coercion Ctx V VTy Ty Sol.
 
 }}.
+Elpi Accumulate Db coercion.db.
 Elpi Typecheck.
-Elpi AddCoercionHook Coercion.
+Elpi CoercionFallbackTactic coercion.