完成 CIS 500 软件基础课程CIS 500 软件基础课程。目前在MoreCoq上。我不明白这rewrite IHl1
部分。它是如何工作的?为什么这在以前使用时不起作用simpl
?
Definition split_combine_statement : Prop := forall X Y (l1 : list X) (l2 : list Y),
length l1 = length l2 -> split (combine l1 l2) = (l1,l2).
Theorem split_combine : split_combine_statement.
Proof. unfold split_combine_statement. intros. generalize dependent Y. induction l1.
Case "l = []". simpl. intros. destruct l2.
SCase "l2 = []". reflexivity.
SCase "l2 = y :: l2". inversion H.
Case "l = x :: l1". intros. destruct l2.
SCase "l2 = []". inversion H.
SCase "l2 = y :: l2". simpl. rewrite IHl1.