处理假设 [英] Handling let in hypothesis
本文介绍了处理假设的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！
问题描述
作为Coq的一项练习，我试图证明以下函数返回一对等长列表。
As an exercise in Coq, I'm trying to prove that the following function returns a pair of lists of equal length.
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 语句里面，我不知道该如何处理：
After the last step I get a hypothesis with a let statement inside, which I do not know how to handle:
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
推荐答案
您要进行销毁（拆分AB tx）。这将把它分解成两部分，分别绑定到 ta 和 tb
You want to do destruct (split A B tx). This will break it up, binding the two pieces to ta and tb
这篇关于处理假设的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
查看全文
