Exporting refined signatures

[gabrielhdt]

Since we have coercions available, I'd like to see what the theory looks like after the coercions have been inserted. Here follows a practical use case.

Use case: inserting explicit introduction of implication

Assume one has an encoding of (a fragment of) first order logic with the elimination of the implication to the product, like this

constant symbol I: TYPE;
constant symbol Prop: TYPE;
symbol Prf (_: Prop): TYPE;

symbol imp (_: Prop) (_: Prop): Prop;

rule Prf (imp $x $y) ↪ Prf $x → Prf $y;

symbol p-imp-p (p: Prop): Prf (imp p p) ≔ λ x : (Prf p), x;

There are various reasons one would like to avoid that rewrite rule and use the explicit elimination of implication with the constant constant symbol imp-i (p: Prop) (q: Prop): (Prf p → Prf q) → Prf (imp p q);. Therefore one may replace the previous theory with

constant symbol I: TYPE;
constant symbol Prop: TYPE;
symbol Prf (_: Prop): TYPE;

symbol imp (_: Prop) (_: Prop): Prop;

symbol imp-i (p: Prop) (q: Prop): (Prf p → Prf q) → Prf (imp p q);

but in that case the proof of p-imp-p doesn't type check anymore.

With coercions, we can recover well-typedness of p-imp-p without modifying the proof. For that, it's enough to change the theory to

constant symbol I: TYPE;
constant symbol Prop: TYPE;
symbol Prf (_: Prop): TYPE;

symbol imp (_: Prop) (_: Prop): Prop;

coerce_rule coerce (Π(a:$A),$B.[a]) (Π(a:$A),$C.[a]) (λ(a:$A),$e.[a])
          ↪ λ(a:$A), (coerce $B.[a] $C.[a] $e.[a]);
constant symbol imp-i (p: Prop) (q: Prop): (Prf p → Prf q) → Prf (imp p q);
coerce_rule coerce (Prf $p → Prf $p) (Prf (imp $p $p)) (λ x: Prf $p, x)
          ↪ imp-i $p $p (λ x: Prf $p, x);

Following that, one may be interested to see the new proof. It can be seen calling lambdapi with option --debug i where one can spot the line

Coerced [λ p x, x : Π p: Prop, Prf p → Prf p <: λ a, imp-i a a (λ x, x) : Π p: Prop, Prf (imp p p)]

but lambdapi export -o lp only exports the initial theory.

[fblanqui]

-o lp calls Pretty, which works on p_terms. We should rename this mode raw_lp, and a add a new mode lp working on terms.