CODEWITHSUNDEEP
coq
Shuzheng
Shuzheng

Reputation: 13830

Break "forall" hypothesis with conjunctions up into components?

I've the following hypotheses:

 H : forall m n : nat,
      f 0 n = S n /\ f (S m) 0 = f m 1 /\ f (S m) (S n) = f m (f (S m) n)

My goal is to break it up into it components. However, trying intros m n in H or destruct H doesn't work. How do I proceed?

I would like something like H0 : f 0 n = S n, H1 : f (S m) 0 = f m 1 and H2 : f (S m) (S n) = f m (f (S m) n) with m and n introduced.

Upvotes: 0

Views: 590

Answers (1)

Zimm i48
Zimm i48

Reputation: 3061

You first need to specialize the hypothesis to be able to destruct it.

If you already know to which variables you want to apply this hypothesis (let's say you have n and m already introduced in your environment), you could do the following:

specialize (H n m).
destruct H as (H0 & H1 & H2).

or shorter:

destruct (H n m) as (H0 & H1 & H2).

(which also keeps the original hypothesis H, while the first solution clears it).

Finally, if you don't know yet to what you are going to apply this hypothesis, you can use the edestruct tactic:

edestruct H as (H0 & H1 & H2).
(* And you get:
H0 : f 0 ?n = S ?n
H1 : f (S ?m) 0 = f ?m 1
H2 : f (S ?m) (S ?n) = f ?m (f (S ?m) ?n)
*)

Upvotes: 4

Related Questions