The Coq mailing list

[Mathijs Kwik <mathijs AT bluescreen303.nl>]

Hi Cedric,

Cedric Auger 
<sedrikov AT gmail.com>
 writes:

> 2014-06-08 17:56 GMT+02:00 Mathijs Kwik 
> <mathijs AT bluescreen303.nl>:
>
>> Theorem app_length_cons : forall (X : Type) (l1 l2 : list X)
>>                                   (x : X) (n : nat),
>>      length (l1 ++ (x :: l2)) = n ->
>>      S (length (l1 ++ l2)) = n.
>> Proof.
>>   intros X l1 l2 x n. generalize dependent l2. generalize dependent n.
>>   induction l1 as [|v1 l1'].
>>   Case "l1 = []". intros n l2 h. apply h.
>>   Case "l1 = v1 :: l1'".
>>     intros n l2. simpl. intro h.
>>     destruct n as [|n'].
>>     SCase "n = 0". inversion h.
>>     SCase "n = S n'".
>>       apply f_equal.
>>       apply IHl1'.
>>       inversion h.
>>       reflexivity.
>> Qed.
>> (** [] *)
>>
>
> In this case, I am not sure, it is really useful to have 'n'.
> The form you define in app_length_cons' is the one, I would rather tend to
> use.
> In fact to prove app_length_cons, I would start with:
> "intros X l1 l2 x _ []." which would end in having
> "S (length (l1 ++ l2)) = length (l1 ++ (x :: l2))" as goal.
> Then a "induction l1 as [|v1 l1']; simpl in *." would lead to two subgoals
> easily provable
> (no need for inversion, 'n' would be removed, and 'l2' does not need to be
> generalized).

This is a nice solution indeed. It uses patterns in intros, which I have
not been introduced to, but it's not hard to grasp and indeed cleans up
my proof.

>
> I now understand, that in fact, you meant that "(forall n, x = n -> y = n)"
> is equivalent to "(x = y)".
> Well, in this case you are right, and I find simpler the form where there
> is no implication.

Yes, I still need to grasp the terminology a bit better to formulate
questions :)

>
>
>>
>> Theorem app_length_cons' : forall (X : Type) (l1 l2 : list X) (x : X),
>>      length (l1 ++ (x :: l2)) = S (length (l1 ++ l2)).
>> Proof.
>>   symmetry.
>>   apply app_length_cons with x.
>>   reflexivity.
>> Qed.
>>
>> (** **** Exercise: 4 stars, optional (app_length_twice) *)
>> (** Prove this by induction on [l], without using app_length. *)
>>
>> Theorem app_length_twice : forall (X:Type) (n:nat) (l:list X),
>>      length l = n ->
>>      length (l ++ l) = n + n.
>> Proof.
>>   intros X n l. generalize dependent n.
>>   induction l as [|x xs].
>>   Case "l = []".
>>     intros n h.
>>     inversion h.
>>     reflexivity.
>>   Case "l = x :: xs".
>>     intros n h.
>>     destruct n as [|n'].
>>     SCase "n = 0". inversion h.
>>     SCase "n = S n'".
>>       rewrite app_length_cons'.
>>       rewrite <- plus_n_Sm.
>>       simpl.
>>       apply f_equal.
>>       apply f_equal.
>>       apply IHxs.
>>       inversion h.
>>       reflexivity.
>> Qed.
>> (** [] *)
>>
>
> Here again, I would first deal with 'n':
>
> "intros X _ l []." should produce
> "length (l++l) = (length l) + (length l)" and remove 'n'.
> Then "induction l as [|x xs]; simpl in *." should produce two goals.
> The first one is "O = O" and is trivially solved.
> The second one is
> "IHl:length(xs++xs)=(length xs) + (length xs) ⊢
> S(length(xs++x::xs)=S((length xs)+S(length xs))".
>
> From here, you can take advantage of the "forall n, x=n->y=n" form of
> app_length_cons by simply using:
> "f_equal; apply app_length_cons" which will change your goal in
> "IHl:length(xs++xs)=(length xs) + (length xs) ⊢ S (length(xs++xs))=(length
> xs)+S(length xs)".

I get stuck after f_equal. It seems app_length_cons is stated
backwards. Our goal is the app_length_cons implication, not
app_length_cons goal itself. So I'm looking for some inverse apply,
"unapply" or "apply <-".

Theorem app_length_twice : forall (X:Type) (n:nat) (l:list X),
     length l = n ->
     length (l ++ l) = n + n.
Proof.
  intros X _ l [].
  induction l as [|x xs].
  Case "l = []". reflexivity.
  Case "l = x :: xs".
    simpl.
    f_equal.


> Then "rewrite IHl; generalize (length xs); clear." would reduce your goal
> to "forall n, S(n + n) = n + S n" which is easily solvable.

Yes, I can see how the remaining steps will go. I just miss the crucial step.

>
> Or you can rewrite directly with your app_length_cons' for a very similar
> proof.
>
> The two ways are very similar. It is more or less your own style which will
> decide the form you will use in this case.

This was indeed what my question was about mainly. It seems that using
intros patterns will turn the implication form into the other.

Thanks for you help!
Mathijs