The Coq mailing list

[Ramkumar Ramachandra <artagnon AT gmail.com>]

Hi,

I have this code:

Definition augmentReg (reg : registration) (t : serverState) : option block :=

let bals := clientBalances t in

match reg with

| mkRegistration _ n (directTransfer k amt) =>

(match M.find n bals with

| Some bal => (match M.find k bals with

| Some bal2 => Some ((mkRegistration 1 n (balance (bal - amt)))

:: (mkRegistration 1 k (balance (bal2 + amt))) :: nil)

| _ => None

end)

| _ => None

end)

| _ => None

end.

Definition augmentReg_zServerState : forall r, augmentReg r zServerState = None.

Proof.

intros.

unfold augmentReg.

simpl.

Admitted.

And my hypotheses/goals window looks like:

• r: registration

• 1/1match r with | {| body := body |} => match body with | directTransfer _ _ => None | statusUpdate => None | commitment => None | balance _ => None | candidacy _ => None | electionVote _ => None | elected _ => None | resign _ => None | encSchedule _ => None | encScheduleVote _ => None | scheduleVerdict _ => None | encChallenge _ => None | encChallengeVote _ => None | challengeVerdict _ => None | decryption _ _ => None end end = None

What tactic can I use to collapse all the cases?

Thanks.

Ram