假设中的处理

Question

作为Coq的练习，我试图证明下面的函数返回一对长度相等的列表。

Require Import List. 

Fixpoint split (A B:Set)(x:list (A*B)) : (list A)*(list B) := 
match x with 
|nil => (nil, nil) 
|cons (a,b) x1 => let (ta, tb) := split A B x1 in (a::ta, b::tb) 
end. 

Theorem split_eq_len : forall (A B:Set)(x:list (A*B))(y:list A)(z:list B),(split A B x)=(y,z) -> length y = length z. 
Proof. 
intros A B x. 
elim x. 
simpl. 
intros y z. 
intros H. 
injection H. 
intros H1 H2. 
rewrite <- H1. 
rewrite <- H2. 
reflexivity. 
intros hx. 
elim hx. 
intros a b tx H y z. 
simpl. 
intro. 

最后一步后，我得到一个假设有let语句中，我不知道如何处理：

1 subgoals 
A : Set 
B : Set 
x : list (A * B) 
hx : A * B 
a : A 
b : B 
tx : list (A * B) 
H : forall (y : list A) (z : list B), 
    split A B tx = (y, z) -> length y = length z 
y : list A 
z : list B 
H0 : (let (ta, tb) := split A B tx in (a :: ta, b :: tb)) = (y, z) 
______________________________________(1/1) 
length y = length z 

Answer 1

你想要做destruct (split A B tx)。这将分解它，将两个部分绑定到ta和tb