Match Case Analysis and Propagation (redux)

Using Coq
1

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.

Thanks for reading!

2

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
3

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.

4

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!