The coercion
app enables to program Coq coercions in Elpi.
This app is experimental.
The coercion
predicate lives in the database coercion.db
% [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.
This example maps True : Prop
to true : bool
, which is a function you
cannot express in type theory, hence in the standard Coercion system.
From elpi.apps Require Import coercion.
From Coq Require Import Bool.
Elpi Accumulate coercion.db lp:{{
coercion _ {{ True }} {{ Prop }} {{ bool }} {{ true }}.
coercion _ {{ False }} {{ Prop }} {{ bool }} {{ false }}.
}}.
Check True && False.
This coercion enriches x : T
to a {x : T | P x}
by using
my_solver
to prove P x
.
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 [],
].
}}.
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.