Problem with pattern match and the simplifier. · Beginner Questions

Hi! I've managed to make a proof that I think is more verbose than it should be. The following code states the lemma and succesfully prooves the first case.

lemma reduceContractStep_preserves_assets :
  "validAndPositive_state state ⟹
   assetsInState state = assetsInReduceStepResult state (reduceContractStep env state cont)"
proof (cases cont)
  assume Case_Close: "validAndPositive_state state" "cont = Close"
  then show ?thesis
  proof (cases "accounts state")
    case Nil
    with Case_Close show ?thesis by simp
  next
    fix refundPay rest
    assume AccountNotEmpty: "accounts state = (Cons refundPay rest)"

    define accId where "accId = fst (fst refundPay)"
    define tok where "tok = snd (fst refundPay)"
    define money where "money = snd refundPay"
    then have patternMatch: "refundPay = ((accId, tok), money)"
      by (simp add: accId_def money_def tok_def)

    (* How do I improve the pattern matching of refundPay?
        I would like to define something like this:
          define accId tok money where "((accId, tok), money) ≡ refundPay"
        Or
            let "((accId, tok), money)" = refundPay
        (This fails for pattern match Clash)
        Or
          assume AccountNotEmpty: "accounts state = (Cons refundPay rest)"
    *)

    then have "money > 0" using Case_Close
      by (metis AccountNotEmpty PositiveAccounts.allAccountsPositiveState.elims(2) PositiveAccounts.validAndPositive_state.elims(2)  allAccountsPositiveMeansFirstIsPositive)

    then show ?thesis using Case_Close AccountNotEmpty patternMatch
      by auto
  next

The first thing that surprised me was that I had to manually add the validAndPositive_state state restriction in the Case_Close assumption, for some reason, the ?thesis variable does not include it.

The second thing has to do with pattern matching. In the Cons case, which I stated as the AccountNotEmpty assumption, I tried to pattern match on refundPay to prove that if the state is valid, then the money in the payment is positive, and then prove the ?thesis for the lemma. The previous code works but is too verbose, and any attempt to pattern match the refundPay constructor fails for a different reason. How can I improve this proof?

Mathias Fleury (Jan 23 2023 at 16:20):

Hernán Rajchert (Jan 23 2023 at 17:29):

lemma reduceContractStep_preserves_assets :
  "validAndPositive_state state ⟹
   assetsInState state = assetsInReduceStepResult state (reduceContractStep env state cont)"
proof (cases cont)
  assume Case_Close: "validAndPositive_state state" "cont = Close"
  then show ?thesis
  proof (cases "accounts state")
    case Nil
    with Case_Close show ?thesis by simp
  next
    fix refundPay rest
    assume AccountNotEmpty: "accounts state = (Cons refundPay rest)"

    then obtain accId tok money where patternMatch: "((accId, tok), money) = refundPay"
      by (metis Product_Type.prod.exhaust_sel)

    then have "money > 0" using Case_Close
      by (metis AccountNotEmpty PositiveAccounts.allAccountsPositiveState.elims(2) PositiveAccounts.validAndPositive_state.elims(2)  allAccountsPositiveMeansFirstIsPositive)

    then show ?thesis using Case_Close AccountNotEmpty patternMatch
      by auto
  next

Hernán Rajchert (Jan 23 2023 at 21:05):

On the initial part of the question, how can I set an assumption or premise part of the proof facts "from here on" so I don't have to reference it every time with using?

Mathias Fleury (Jan 24 2023 at 05:19):

note X = Case_Close AccountNotEmpty

Mathias Fleury (Jan 24 2023 at 05:20):

BTW, I would write the patternMatch the otherway arround patternMatch: "refundPay = ((accId, tok), money)" to make it simplifier compatible

Wolfgang Jeltsch (Jan 25 2023 at 01:13):

I think that cases doesn’t pass down facts it is fed with; so you just have to reference said facts where you actually need them within the proof by case distinction. It is different for induction. The induction method generates dedicated goals for the different cases (therefore you use ?case, not ?thesis). These dedicated goals would typically not fit facts from outside the proof by induction; therefore, induction is capable of receiving facts, which it then adapts and passes down to the different cases.

Hernán Rajchert (Jan 25 2023 at 13:33):

Thanks! This helps me understand the refinement process. I did notice that induction includes the premises while cases doesn't

Wolfgang Jeltsch (Jan 25 2023 at 15:17):

To go a bit deeper: cases introduces equality constraints as extra facts for the different cases and this way specializes the goal according to the different cases. The induction method cannot do that. The intuitive reason is that if it would link a case to the general statement via equality constraints, it would only talk about the first layer of the induction, while it has to talk about all those layers (you can apply induction steps arbitrarily often). The solution is to generate case-specific goals, accessible via ?case, and this then necessitates the generation of case-specific premises. The induction methods does both of that; for the latter you have to pass outside premises to it. With cases, on the other hand, using your outside premises in conjunction with the equality constraints that cases generates for the different cases will do the job.

Stream: Beginner Questions

Topic: Problem with pattern match and the simplifier.

Hernán Rajchert (Jan 23 2023 at 14:39):