## Stream: Coq users

### Topic: Tactic for destructing specific pattern match in Goal

#### David Sillman (Sep 30 2023 at 17:20):

Hi,

I'm a beginner getting started with Coq implementing a simple boolean logic lambda calculus. I'm trying to prove, by induction on boolean terms, (TmTrue, TmFalse, TmNot, TmIf), that one step of evaluation `eval1` in this lambda calculus reduces the term size, with recursive pattern-matching definitions below:

``````Inductive term : Type :=
| TmTrue  : term
| TmFalse : term
| TmNot   : term -> term
| TmIf    : term -> term -> term -> term.

Notation T := TmTrue.
Notation F := TmFalse.
Notation "~ A" := (TmNot A).
Notation "F ? G : H" := (TmIf (F) (G) (H)) (at level 100, G at level 99).

Fixpoint term_size (t: term) : nat :=
match t with
| T               => 1
| F               => 1
| ~ t'            => 1 + (term_size t')
| t' ? t'' : t''' => 1 + (term_size t') + (term_size t'') + (term_size t''')
end.

Fixpoint eval1 (t: term) : term :=
match t with
| ~ T             => F
| ~ F             => T
| ~ t'            => ~ eval1 t'
| T ? t' : t''    => t'
| F ? t' : t''    => t''
| t' ? t'' : t''' => (eval1 t') ? t'' : t'''
| _               => t
end.
``````

I've gotten through 3/4 steps of induction, proving the result for terms in the form `T`, `F` and `~ t`, but then I get stuck on the TmIf case (`t ? t' : t''`):

``````Theorem eval1_dec_size : forall (t: term),
term_size (eval1 t) <= term_size t.
Proof.
intros.
induction t; try reflexivity.
- assert
(term_size_not_eval_le :
term_size (eval1 (~ t)) <= term_size (~ (eval1 t))).
intros.
destruct t ;
try reflexivity ;
simpl ; intuition.
rewrite term_size_not_eval_le. simpl.
rewrite <- Nat.le_pred_le_succ. simpl.
apply IHt.
- simpl.
``````

Which gives me this specific sub-pattern match in the Goal:

``````1 goal
t1, t2, t3 : term
IHt1 : term_size (eval1 t1) <= term_size t1
IHt2 : term_size (eval1 t2) <= term_size t2
IHt3 : term_size (eval1 t3) <= term_size t3
______________________________________(1/1)
term_size match t1 with
| T => t2
| F => t3
| _ => eval1 t1 ? t2 : t3
end <= S (term_size t1 + term_size t2 + term_size t3)
``````

How can I "destruct" on this specific pattern match - I can easily prove the result in each of those cases using my IHts. I'm only aware of being able to destruct on a specific term, e.g. `t1`, which makes me go through _all_ cases of the term, rather than just the sub-pattern-match in the above goal. How can I destruct on that specific matching expression?

there is no built-in `destruct`-like tactic that allows you to get only some custom subgoals from an inductive type. It sounds like what you are looking for are the "views" described for example here
@David Sillman I don't understand what you mean by "just the sub-pattern-match in the above goal": pattern matching always covers all cases in Coq. Anyway, I was able to prove your theorem by destructing `t1` at that point. The code is on Gist if you want to see it (in a pedantic style, of course could be simplified): <https://gist.github.com/jp-diegidio/dc49397df0500f9b7931bb4be95a3fc8>