# Match Case Analysis and Propagation (redux)

Hi, all! This question is similar to one I posted last month during my first week of learning Coq, but I think I can ask it properly this time. I’ll have a brief description of my general question first and then a concrete MWE after.

### The Question

I frequently want to destructure `match` expressions based upon what I know them to be equal to. For instance, consider the following hypothesis:

``````H : match f x with
| Foo _ => Some n
| _ => None
end = Some m
``````

I would expect to be able to break this into the following hypothesis:

``````H : ((exists z, f x = Foo z) /\ Some n = Some m) \/ ((exists z, f x = z) /\ None = Some n)
``````

My reasoning is based on the operational semantics of `match`. `f x` is going to match one of these two patterns. Each pattern is a case: the match subject has to match the pattern and the result has to propagate through the equality to the right-hand side. The above is the barest form of hypothesis one might get as a result; ideally, junk like `(exists z, f x = z)` would be discarded and `discriminate` would be applied appropriately.

Is there a tactic that can understand what a `match` expression does? Is there a flaw in my reasoning that would prevent such a tactic from existing? So far, my strategy has been to destruct on `x` and let `f` simplify, but that hasn’t been scaling to my use case in which `x` has fourteen different constructors and the behavior of `f` is rather involved. Surely, there must be a better approach… yes?

### The Example

Here’s the MWE for the question I wrote above. Let’s imagine we’re proving soundness of an extremely simple reduction system. First, I’ll give a simple AST. I distinguish values from expressions here because it is relevant in my real use case.

``````Require Import Bool.

Inductive type :=
| TBool
| TUnit
.

Inductive expr :=
| EValue : value -> expr
| EAnd : expr -> expr -> expr

with value :=
| VBool : bool -> value
| VUnit : value
.
``````

Here’s the definition of small-step evaluation I’m using:

``````Fixpoint step (e : expr) : option expr :=
match e with
| EValue _ => None
| EAnd (EValue (VBool b1)) (EValue (VBool b2)) =>
Some (EValue (VBool (b1 && b2)))
| EAnd (EValue _) (EValue _) => None
| EAnd (EValue v1) e2 =>
option_map (fun e2' => EAnd (EValue v1) e2') (step e2)
| EAnd e1 e2 =>
option_map (fun e1' => EAnd e1' e2) (step e1)
end
.
``````

And here’s a type inference function:

``````Fixpoint infer_type (e : expr) : option type :=
match e with
| EValue (VBool _) => Some TBool
| EValue VUnit => Some TUnit
| EAnd e1 e2 =>
match infer_type e1, infer_type e2 with
| Some TBool, Some TBool => Some TBool
| _, _ => None
end
end
.
``````

I’d like to prove the soundness of this type system, which I state as follows:

``````Lemma progress :
forall (e : expr) (t : type), infer_type e = Some t ->
(exists (v : value), e = EValue v) \/
(exists (e' : expr), step e = Some e' /\ infer_type e' = Some t).
``````

The proof proceeds by induction on `e` with the `EValue` (base) case being typically boring. In the `EAnd` (inductive) case, I simplify the lemma’s precondition to learn a bit about my situation. Here’s the proof I have so far:

``````Proof.
induction e.
- intros t H. left. exists v. reflexivity.
- intros t H. right. simpl.
``````

And here is my proof state:

``````1 goal
e1, e2 : expr
IHe1 : forall t : type,
infer_type e1 = Some t ->
(exists v : value, e1 = EValue v) \/
(exists e' : expr, step e1 = Some e' /\ infer_type e' = Some t)
IHe2 : forall t : type,
infer_type e2 = Some t ->
(exists v : value, e2 = EValue v) \/
(exists e' : expr, step e2 = Some e' /\ infer_type e' = Some t)
t : type
H : match infer_type e1 with
| Some TBool => match infer_type e2 with
| Some TBool => Some TBool
| _ => None
end
| _ => None
end = Some t
______________________________________(1/1)
exists e' : expr, step (EAnd e1 e2) = Some e' /\ infer_type e' = Some t
``````

It seems obvious to me that I should be able to learn the following from `H` based upon the semantics of `match`:

• `infer_type e1 = Some TBool`
• `infer_type e2 = Some TBool`
• `Some TBool = Some t`

Is there a Coq tactic that will analyze the `match` expression and produce cases from it so that I can boil it down to the above?

The only two strategies I’ve found so far are

1. Case analyze on a proof of decidability of equality of the subject (e.g. `destruct (type_eq_dec (infer_type e1) TBool as [H'|H']`), which is pretty verbose and doesn’t help much with the antimatch case; or
2. Case analyze on parts of the subject (e.g. `e1`) until the `match` dissolves away on its own.

Given how tedious and clunky these feel, I assume they must be bad form.

Sure. Just destruct the values of `infer_type e1` and `infer_type e2`, remembering their origin using `eqn:` (plus some cleanup of pointless goals using `easy`):

``````destruct (infer_type e1) as [[|]|] eqn:T1 ; try easy.
destruct (infer_type e2) as [[|]|] eqn:T2 ; try easy.
``````

You will end up with a single goal with the following hypotheses:

``````T1: infer_type e1 = Some TBool
T2: infer_type e2 = Some TBool
H: Some TBool = Some t
``````

As @silene said you shoud destruct on `f x` instead, and keep the equality with `eqn:h`.
you can have a look at this attempt to automate it: coq-tactical/src/SimplMatch.v at master · tchajed/coq-tactical · GitHub .

If you happen to often mimick the case analysis of a function (eg to prove properties of this function) you may want to have a look at the Equation plugin and its `funelim` tactic. This may take a while to master (you need to define the functions in a different syntax) but it is quite nice to automate this kind of reasoning.

Thank you both for the help and the patience! When @silene answered this question a month ago, I failed to absorb the relevance of destructing on an expression (instead focusing on the pattern matching notation and the `eqn` option at the time). This makes a lot more sense now that I’m revisiting it.

Sorry for needing to be told twice!