The Coq mailing list

[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?

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.
(** [] *)

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.
(** [] *)