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

- 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 - 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.

Thanks for reading!