The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2014-06-08 17:56 GMT+02:00 Mathijs Kwik <mathijs AT bluescreen303.nl>:

Hi all,

I'm following the "Software Foundations" tutorial and I get the feeling
I'm overly-complicating things. I understand there are probably smarter
/ more advanced tactics available that have not been introduced yet at
this stage in the tutorial. That's not what I'm after.

Please see the code below. I noticed the exercises switched from the
easy (x = y) style to implications (x = n -> y = n). I see how these
work nicely with the "apply" tactic, but it also confuses me a bit. Why
is it useful to sometimes format a theorem as an implication?

(x = n -> y = n) is weaker than (x = y): there are more (x, y, n) triples
which satisfy the first predicate than (x, y, n) which satisfy the second.
For instance, (1, 2, 3) satisfy the first predicate, but not the second.

When you perform some induction, you sometimes need to generalize your goal.
By getting it a little weaker you may avoid breaking invariants for the recursion.

 

I tried to use (app_length_cons) directly in my proof, but didn't
succeed. I had to provide the (app_length_cons') helper. I'm sure there
must be a better way?

Does anyone have a better/easier solution to app_length_twice
(preferably using tactics that have been introduced so far).

Kind regards,
Mathijs







(** **** Exercise: 3 stars, optional (app_length_cons) *)
(** Prove this by induction on [l1], without using [app_length]. *)

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).

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.
 

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

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.


--
.../Sedrikov\...