Stream: Beginner Questions

Topic: Relaxing subterms inside inequality

John Park (Aug 29 2024 at 11:11):

In a paper proof of elementary inequalities like a≥5 ⟹ b≤2 ⟹ b>0 ⟹ 1+a/b ≥ 3, one can safely "rewrite" a/b into 5/2, but to prove it in Isbaelle/HOL manually (when smt can't handle it), such relaxation of subterms involves tedious application of structural lemmas like order_trans and frac_le.

Is there any support for such common practice of relaxing subterms inside elementary inequalities, like a proof method in the form of apply (relax "a/b" into "5/2"), which applies those structural lemmas automatically?

Mathias Fleury (Aug 29 2024 at 11:31):

You are talking about this right?

lemma
  fixes a b :: real
  assumes \<open>a\<ge>5\<close> \<open>b\<le>2\<close>  \<open>b>0\<close>
  shows \<open>1+a/b \<ge> 3\<close>
proof -
  have \<open>1+a/b \<ge> 1+5/2\<close>
    using assms by (auto simp: field_simps)
  moreover have \<open>1+5/2 \<ge> (3::real)\<close>
    by auto
  ultimately show \<open>1+a/b \<ge> 3\<close> by linarith
qed

Mathias Fleury (Aug 29 2024 at 11:32):

(it would be better to use also/finally/.. instead of moreover/ultimately/linarith)

John Park (Aug 29 2024 at 11:44):

@Mathias Fleury On the contrary, the point is to avoid such manual peeling of terms, so that one can write shorter and more intuitive proofs like by (relax "a/b" into "5/2") simp.

The real inequality that I'm trying to prove right now is much more deeply nested than the example, and many of its subterms have to be relaxed, which makes such manual effort proportionally more boring.

Mathias Fleury (Aug 29 2024 at 11:52):

I was confused why you mentioned needing order_trans.

Mathias Fleury (Aug 29 2024 at 11:52):

Anyway, I am not aware of anything existing

Mathias Fleury (Aug 29 2024 at 11:53):

but I am also not convinced that it is super-hard to program in ML (at least in the simple version you presented)

John Park (Aug 29 2024 at 12:42):

Ok thanks, I'll try to make one.
Do you think if such a proof method deserves an AFP entry? It seems generally helpful to me, but the fact that it hasn't existed yet seems to suggest otherwise.

Mathias Fleury (Aug 29 2024 at 15:58):

Hard to say. I would try it for your own development. And once you are happy with it I would ask on the mailing list for feedback from other people

Mathias Fleury (Aug 29 2024 at 16:00):

@Manuel Eberl you do much more arithmetic than I do.

Manuel Eberl (Aug 29 2024 at 17:05):

Not sure how useful this would be. It sounds like an extremely specialised thing.

Manuel Eberl (Aug 29 2024 at 17:06):

The more general notion here is rewriting modulo relations other than equality (in this case ≤). I think @Simon Roßkopf has a prototype of that lying around somewhere. Not sure if it only works for congruences or also for more general things like ≤.

John Park (Aug 30 2024 at 10:49):

Manuel Eberl said:

The more general notion here is rewriting modulo relations other than equality (in this case ≤).

Thanks, this notion sounds indeed on point. I guess for inequalities it should be something like rewriting modulo closed set of relations, in this case {≥, ≤}, which are swapped at subtraction and division. Whether the relations are equivalence relations (like congruence) or not (like inequalities) shouldn't matter very much for this notion of rewriting.

Last updated: Dec 30 2024 at 16:22 UTC