Newbie Question: Match Case Analysis and Propagation

Using Coq
1

Hello! I’m new to Coq and to writing machine-verified proofs in general – I just started at this yesterday – and have occasionally been stymied because I know what I want to do but have no idea about the basic syntax to express it. I’m currently working on an exercise to prove a relationship between two functions and need to gather some information out of a hypothesis I have. At present, my hypothesis reads

H : match typecheck e with
| Just TBool => Just TBool
| _ => Nothing
end = Just t

Here, Just and Nothing are constructors for my own little option-like type (because I made my own to learn how such things are defined). In case it’s relevant, the definition is

Inductive maybe {A:Type} : Type :=
  | Just : A -> @maybe A
  | Nothing : @maybe A
.

I would expect to be able to learn the following from hypothesis H:

  1. That t = TBool.
  2. That typecheck e = Just TBool.

I can get the first conclusion by

destruct (typecheck e) in H.
2: inversion H.  (* eliminate "Nothing = Just t" case *)
destruct (t0) in H.
1: inversion H.  (* eliminate "Nothing = Just t" case *)
apply unjust_preserves_equal in H.

where unjust_preserves_equal is a simple lemma that states forall A : Type, forall x y : A, @Just A x = @Just A y -> x = y.. This leaves me with the hypothesis H : TBool = t, which gets me conclusion number 1 above.

This is somewhat destructive, of course, as I no longer have the structure I wanted. I presume there’s some way to “copy” H so that I could avoid losing the original match structure.

Setting that aside, I have no idea how to get conclusion number 2. maybe is a simple inductive type, so I don’t see why I shouldn’t be able to reach conclusion number 2; I just have no idea how to ask Coq to extract that conclusion from the original H’s match expression. (I tried to write a little lemma to do this, but I couldn’t find a way to make the TBool pattern a parameter to the lemma.)

Thank you!

2
  1. You can ask destruct to keep an equality around using “eqn:”.
  2. You can use “destruct ... as” to name the new variables, but also to perform further destruction, as with any intro-pattern such as “[|]”.
  3. The tactic inversion is rather heavy-handed. You can achieve the same proofs of disequality using discriminate, which happens to be part of easy.
  4. The injectivity of inductive constructors can be recovered using injection.

All in all, this means that you can do something like

destruct (typecheck e) as [[|]|] eqn:H' in H ; try easy.
injection H as H.

At this point, you should have H: TBool = t and H': typecheck e = Just TBool.

3

Thank you! This is exactly the sort of response I was hoping to get. (I clearly need to learn more about the [[|]|] syntax; I keep seeing things like it but haven’t bumped into an explanation yet I’ll go check the manual now that I have some footing.) This gives me a lot to go on; I appreciate it!

4

The first thing to understand is that [ [ | ] | ] is the composition of two intro-patterns of the form [x11 x12 x13...|x21 x22 x23...|x31 x32 x33...|...]. Such an intro-pattern is used when destructing the value of an inductive type with several constructors, and each constructor might have arguments. All the xs are used to name these arguments in the context. In your specific case, the outer pattern is just [x11| ] (i.e., the maybe type has two constructors, the first one with a single argument, and the second one with none), while the inner pattern, which takes the place of x11, is just [ | ] (i.e., two constructors again, but neither with any argument).

If you do not use the “as” part of destruct, Coq will use an intro-pattern with seemingly random names. I suggest to always use “as”, except in the very specific case where you do not care about the variable names, e.g., because you are about to call easy.

5

Wow; thanks for the supplementary explanation! This did the trick and I’ve been able to use it elsewhere as well. This is an encouraging welcome to the community. :slight_smile: