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?

Thanks in advance for your patience.

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>

Last updated: Jun 22 2024 at 16:02 UTC