You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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-pwithout modifying the proof. For that, it's enough to change the theory to
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
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 withbut 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 toFollowing 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 linebut
lambdapi export -o lp
only exports the initial theory.The text was updated successfully, but these errors were encountered: