The Coq mailing list

[Merlin Göttlinger <megoettlinger AT gmail.com>]

Hi,

while not really being automated, I use this tactic to deal with equalities on match hypotheses:

Ltac match_hyp := match goal with

                  | [_ : match ?p with _ => _ end = _ |- _] => destruct p; simpl

                  end.

Note that you can match on match ... with ... in Ltac but not on the specific cases in the match.

If you run repeat match_hyp it should solve the original question, right?

Cheers,

Merlin

Heiko Becker <hbecker AT mpi-sws.org> schrieb am Mi., 17. Jan. 2018 um 16:02 Uhr:

Hello,

recently I had similar issues.
I tried automating similar reasoning over multiple proofs.
As it turns out, you cannot directly match on a "match ... with ..." in an ltac match-goal phrase.
So I came up with the following code that may help you:

  Definition optionLift (X Y:Type) (v:option X) (f:X -> Y) (e:Y) :=
    match v with
    |Some val => f val
    | None => e
    end.

  Lemma optionLift_eq (X Y:Type) v (f:X -> Y) (e:Y):
    match v with |Some val => f val | None => e end = optionLift X Y v f e.
  Proof.
    reflexivity.
  Qed.

  Ltac remove_matches := rewrite optionLift_eq in *.

  Ltac match_factorize_asm :=
    match goal with
    | [ H: ?t = ?u |- context [optionLift _ _ ?t _ _]]
      => rewrite H; cbn
    | [ H1: ?t = ?u, H2: context [optionLift _ _ ?t _ _] |- _ ]
      => rewrite H1 in H2; cbn in H2
    | [ H: context [optionLift _ _ ?t _ _] |- _ ]
      => destruct t eqn:?; cbn in H; try congruence
    end.

  Ltac match_factorize :=
    match_factorize_asm ||
    match goal with
    | [ |- context [optionLift _ _ ?t _ _] ]
      => destruct t eqn:?; cbn; try congruence
    end.

As I was dealing with a setting where it could be that I had previously inspected parts of the match, the tactic also checks that the term to be destructed is not already an assumption. If you need only prove your goal from below, you can drop these cases.
Additionally, you may want to change the last call in match_factorize, respectively match_factorize_asm into "auto" or "reflexivity" to automatically prove the "None = None" cases you will get.

Maybe this code helps you a bit.


Best,

Heiko

On 01/17/2018 01:28 AM, Ramkumar Ramachandra wrote:

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