使用 "rewrite [hypothesis with implication]"

Question

正在学习 CIS 500 软件基础课程CIS 500 Software Foundations course. Currently on 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.

Answer 1

你的假设IHl1是：

IHl1 : forall (Y : Type) (l2 : list Y),
       length l1 = length l2 -> split (combine l1 l2) = (l1, l2)

所以为了重写它，你需要实例化Y类型和l2列表。接下来，您需要提供等式 length l1 = length l2 来重写 split (combine l1 l2) = (l1,l2)。整个解决方案是：

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. 
  simpl. intros. destruct l2. 
  reflexivity. 
  inversion H.
  intros.  destruct l2. 
  inversion H.
  simpl. inversion H. rewrite (IHl1 Y l2 H1). reflexivity.
Qed.

请注意，要重写 IHl1，我们需要实例化通用量词（为其变量传递足够的值）并为蕴涵提供左侧。用 Coq 的话来说：rewrite (IHl1 Y l2 H1) 正在传递类型 Y 来实例化 IHl1 中的 forall (Y : Type)。 l2.

也是如此

使用 "rewrite [hypothesis with implication]"

Using "rewrite [hypothesis with implication]"

coq

coq-tactic