[Prev][Next][Index]
Re: how to get LP to prove things like ~(1 <= 0) and (0 <= 2)?
When the LSL checker translates LSL into LP input, it makes the rewrite rules
for DecimalLiterals passive, which means that they don't get applied
automatically. For example, 2 will not be rewritten to succ(succ(0)).
(I'm not sure why the LSL checker makes them passive. Perhaps it's to
keep conjectures and facts more readable.)
At any rate, you probably want to make them "active" via the command
"make active DecimalLiterals". This is enough to prove ~(1 <= 0) by
rewriting. It's also a necessary first step for the proofs below.
To prove 0 <= 2, you also need to use facts named IsTO. The easiest proof
to understand is to instantiate the rule for transitivity.
instantiate x by 0, y by 1, z by 2 in IsTO.2
(It's a good thing you didn't want to prove 0 <= 9.)
The crit command is useful for finding such instantiations automatically.
To prove 0 <= 2, you can do
resume by contradiction % This turns the (negated) conjecture into
% a rewrite rule that crit can use.
crit *hyp with * % This is a common idiom in proofs.
% For this proof, crit *contrahyp with isto.4
% suffices.
Also, there may be shorter proofs using the experimental "zap" command that
I believe is still under development.
-Mark Vandevoorde
Reference(s):