Hernán Rajchert (Jan 23 2023 at 19:00): 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
Ah, I think just changing the cases to look like this :man_facepalming:
proof (cases "moneyToPay ≤ 0")
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 =.
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
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’).
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:
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.
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
Hernán Rajchert said:
lemma neg_or_positive [case_names neg_or_zero positive]: "((x ::linorder) <= 0 ⟹ P) ⟹ ( x > 0 ⟹ P) ⟹ P" tryyields 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, …
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: Dec 21 2024 at 16:20 UTC