Stream: Beginner Questions

Topic: How can I case with integers with a custom split number?


view this post on Zulip Hernán Rajchert (Jan 23 2023 at 19:00):

Following the question I made earlier about pattern matching... on a different subgoal I'd like to split a proof into two subgoals, if moneyToPay <= 0 and if moneyToPay > 0 but when I apply cases on moneyToPay I get < 0 or >=0.

What I'm currently doing:

next
  fix payFrom payTo payTok payVal payCont
  assume Case_Pay: "validAndPositive_state state" "cont = Pay payFrom payTo payTok payVal payCont"
  then obtain moneyToPay where moneyToPaySimp: "evalValue env state payVal = moneyToPay"
    by blast
  then show ?thesis using Case_Pay
  proof (cases "moneyToPay")
    case (neg n)
    then show ?thesis using Case_Pay moneyToPaySimp
      by auto
  next
    case (nonneg n)
    then show ?thesis  using Case_Pay moneyToPaySimp nonneg
      apply (simp only: reduceContractStep.simps)
      apply (simp only: Let_def)
      (* I get stucked here because there is an if that says (if int n ≤ 0 then ... else ...) and n can be zero *)
      apply (simp only: If_def)

      sorry
  qed

This split fails because I cannot simplify an inner if that has as a condition if int n <= 0 then ... else ...

What I would like to do instead:

next
  fix payFrom payTo payTok payVal payCont
  assume Case_Pay: "validAndPositive_state state" "cont = Pay payFrom payTo payTok payVal payCont"
  then obtain moneyToPay where moneyToPaySimp: "evalValue env state payVal = moneyToPay"
    by blast
  then show ?thesis using Case_Pay
  proof (cases "moneyToPay")
    fix n
    presume "moneyToPay ≤ 0"
    then show ?thesis using Case_Pay moneyToPaySimp
      by auto
  next
    fix n
    presume "moneyToPay > 0"

    then show ?thesis  using Case_Pay moneyToPaySimp
      sorry
  qed

This has two problems, for some reason I can't use assume and I need to presume, and then I have two extra goals to prove

Failed to finish proof:
goal (2 subgoals):
 1. ⋀n. evalValue env state payVal = moneyToPay 
         validAndPositive_state state  cont = Pay payFrom payTo payTok payVal payCont  moneyToPay = int n  moneyToPay  0
 2. ⋀n. evalValue env state payVal = moneyToPay 
         validAndPositive_state state  cont = Pay payFrom payTo payTok payVal payCont  moneyToPay = - int (Suc n)  0 < moneyToPay

view this post on Zulip Hernán Rajchert (Jan 23 2023 at 19:09):

Ah, I think just changing the cases to look like this :man_facepalming:

proof (cases "moneyToPay ≤ 0")

view this post on Zulip Wolfgang Jeltsch (Jan 25 2023 at 01:28):

Yes, cases can be used in a number of ways. A complete description of the possibilities is in Subsection 6.5.2 of The Isabelle/Isar Reference Manual.

When passing a boolean expression to cases, like you did above, it makes a case distinction on the boolean in question, with a True and a False case. This is just an example of case distinction for an algebraic datatype; for example, cases with a list expression would use a case for the empty list and a case for non-empty lists.

Apparently, for int, the default rule for case distinction is the one that distinguishes between non-negative and negative numbers. However, you can always pass the rule to use to the cases method. I did this recently with the linorder_cases rule, which distinguishes between <, =, and > for values of linearly ordered types. You could, in principle, use cases moneyToPay 0 rule: linorder_cases. The advantage would be that you would get nicer case names: less, equal, and greater instead of True and False. However, you would have to handle the less-than and equals cases separately, which is probably not what you want. I don’t know of a rule that would distinguish between just and =.

view this post on Zulip Hernán Rajchert (Jan 25 2023 at 13:58):

That is awesome, I just tried the following and it worked... not sure if best practice though

lemma neg_or_positive [case_names neg_or_zero positive]:
  "(x <= 0 ⟹ P) ⟹ ( ¬ (x ≤ 0) ⟹ P) ⟹ P"
  by blast


lemma
  proof (cases "moneyToPay" rule: neg_or_positive)
    case neg_or_zero
    then show ?thesis sorry
  next
   case positive
   then show ?thesis sorry
qed

view this post on Zulip Manuel Eberl (Jan 25 2023 at 14:37):

This is perfectly fine, although I for one would replace the ¬(x ≤ 0) with x > 0. In any case, I don't really see a big advantage over just doing proof (cases "x ≥ 0"). Also, neg_or_positive is perhaps a bit misleading because x ≤ 0 does not mean ‘negative’).

view this post on Zulip Hernán Rajchert (Jan 25 2023 at 14:55):

For some reason x > 0 did not worked for me. I think I need to add a linorder restriction to x, but I'm having issues doing that.

lemma neg_or_positive [case_names neg_or_zero positive]:
  "(x <= 0 ⟹ P) ⟹ ( x > 0 ⟹ P) ⟹ P"
  try

Nitpick says:

Nitpick found a counterexample for card 'a = 1:
  Free variables:
    P = False
    x = a⇩1
Hint: Maybe you forgot a type constraint?

And this

lemma neg_or_positive [case_names neg_or_zero positive]:
  "((x ::linorder) <= 0 ⟹ P) ⟹ ( x > 0 ⟹ P) ⟹ P"
  try

yields saying Undefined type name: "linorder"⌂

I could rename neg_or_positive to bigger_than_zero :thinking:

view this post on Zulip Wolfgang Jeltsch (Jan 25 2023 at 15:02):

I think if you just use and >, the kind of the type of x is inferred to be the most general one, which is ord, the class that just declares those comparison functions, without any properties. Your rule only holds if you have a linear order.

view this post on Zulip Wolfgang Jeltsch (Jan 25 2023 at 15:05):

I would choose the name non_positive instead of neg_or_positive, to conform with the name non_negative that the default cases rule of int uses. Also the name of your rule is incorrect, as it excludes the zero case.

Furthermore, you might want to write the statement of the elimination rule using Isar’s obtains, which allows you to avoid talking about the eliminator-style encoding of disjunction and the variable P.

Here’s my version of the code:

lemma non_positive_or_positive [case_names non_positive positive]:
  fixes x :: "'a::{linorder, zero}"
  obtains "x ≤ 0" | "x > 0"
  by fastforce

lemma
  fixes i :: int
  shows "i = i"
proof (cases i rule: non_positive_or_positive)
  case non_positive
  then show ?thesis sorry
next
  case positive
  then show ?thesis sorry
qed

view this post on Zulip Manuel Eberl (Jan 26 2023 at 10:17):

Hernán Rajchert said:

lemma neg_or_positive [case_names neg_or_zero positive]:
  "((x ::linorder) <= 0 ⟹ P) ⟹ ( x > 0 ⟹ P) ⟹ P"
  try

yields saying Undefined type name: "linorder"⌂

linorder is not a type but a type class. You have to write it as (x :: 'a :: linorder). That says that x is of some fixed type 'a with the constraint that 'a of the type class linorder. Once you finish the proof, Isabelle then automatically makes this polymorphic, i.e. replaces the fixed type variable 'a with a schematic type variable ?'a that you can replace with any concrete type of type class linorder, such as int, real, …

view this post on Zulip Manuel Eberl (Jan 26 2023 at 10:18):

The typical naming scheme in Isabelle/HOL for < 0, > 0, ≥ 0, ≤ 0, by the way, is neg, pos, nonneg, nonpos.


Last updated: Mar 28 2024 at 12:29 UTC