Search code examples
coqcoq-tactic

Using "rewrite [hypothesis with implication]"

Working through CIS 500 Software Foundations courseCIS 500 Software Foundations course. Currently on MoreCoq. I don't understand the rewrite IHl1 part. How is it working? Why does this not work when used before 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.
Solution

  • Your hypothesis IHl1 is:

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

    So in order to rewrite it, you need to instantiate the Y type and l2 list. Next, you need to provide the equality length l1 = length l2 to rewrite split (combine l1 l2) = (l1,l2). The whole solution is:

    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.

    Note that to rewrite IHl1, we need to instantiate the universal quantifiers (passing adequate values for its variables) and to provide a left hand side for the implication. In Coq words: rewrite (IHl1 Y l2 H1) is passing the type Y to instantiate the forall (Y : Type) in IHl1. The same holds for l2.