Stream: Coq users

Topic: Tactic for destructing specific pattern match in Goal


view this post on Zulip 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?

Thanks in advance for your patience.

view this post on Zulip Karl Palmskog (Sep 30 2023 at 17:40):

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

view this post on Zulip Julio Di Egidio (Oct 01 2023 at 06:33):

@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