Email Gateway (Aug 22 2022 at 14:28): Email Gateway (Aug 22 2022 at 14:28):From: Mark Wassell <mpwassell@gmail.com>
Hello,
I have a simple inductive predicate:
inductive Q' :: "nat ⇒ bool" where
Q'0: "Q' 0" |
Q'n: "List.list_all (λk. Q' k) [0..<n] ⟹ Q' n"
The monotonicity proof for this fails. I take the goal from the error
window and prove it:
lemma xx [mono]: "mono (λp x. x = 0 ∨ (∃n. x = n ∧ list_all p [0..<n]))"
unfolding pred_list_def mono_def
proof((rule allI)+,rule impI)
fix x and y::"nat⇒bool"
assume "x≤y"
show "(λxa. xa = 0 ∨ (∃n. xa = n ∧ Ball (set [0..<n]) x))
≤ (λx. x = 0 ∨ (∃n. x = n ∧ Ball (set [0..<n]) y))" using ‹x ≤
y› by blast
qed
However the monotonicity proof for the predicate still doesn't work. It has
been added to the 'mono' list and if I include the line 'monos xx' after
the inductive predicate definition, there is still no proof.
The inductive predicate
inductive Q :: "nat ⇒ bool" where
Q0: "Q 0" |
Qn: "(∀k∈set[0..<n]. Q k) ⟹ Q n"
is ok. I believe that Q' and Q and equivalent.
Cheers
Mark
Email Gateway (Aug 22 2022 at 14:29):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Mark,
The monotonicity prover of the inductive package requires a specific format for
monotonicity rules. In particular, there is no point in proven the monotonicity statement
yourself and adding it.
In general, you need a separate monotonicity preservation statement for every higher-order
combinator that is apply to the inductively defined constant. For your definition of Q'
with List.list_all, you have to prove and declare the corresponding monotonicity rule. In
the other definition, you use bounded universal quantification, for which there is already
a monotonicity rule in place.
You can infer the format by looking at the goal state of the failed proof attempt. For
list_all, the right rule is this:
(!!x. P x --> Q x) ==> list_all P xs --> list_all Q xs
Monotonicity must be expressed using HOL implication and Pure quantification.
Another remark: I recommend to use universal quantification instead of list_all, because
list_all is used almost exclusively for code generation, i.e., proof automation will be
less good. In particular, the proof method induction works much better with universal
quantifiers than any other higher-order combinator.
Best,
Andreas
Last updated: Apr 27 2024 at 04:17 UTC