(* Exercise coq_list_06 *)

(* Those are the definitions from the previous exercise: *)

Inductive natlist : Set :=
  | nil : natlist
  | cons : nat -> natlist -> natlist.

Fixpoint append (l m : natlist) {struct l} : natlist :=
  match l with
  | nil => m
  | cons x xs => cons x (append xs m)
  end.

Fixpoint length (l : natlist) : nat :=
match l with
  nil => 0
 | cons a k => S(length k)
end.
 (* copy your definition from the previous exercise here *)

Fixpoint reverse (l : natlist) : natlist :=
match l with
 nil => nil
 | cons a k => append (reverse k) (cons a nil)
end.

 (* copy your definition from the previous exercise here *)

(* Now let us prove that reverse does not change the length
   of a list *)

(* For this we may need a result proven in one of the previous
   exercises and some results about natural numbers (remember
   the exercises concerning natural numbers?) *)
Axiom append_length : forall l m,
  length (append l m) = length l + length m.
Require Import Arith.

Lemma reverse_length : forall l,
  length l = length (reverse l).
Proof.
induction l.
- simpl;auto.
- simpl.
  rewrite IHl.
  simpl.
  rewrite append_length.
  simpl.
  auto.
(* Alternative 1: First prove a separate 
   Lemma help : forall n: nat, S n = n + 1.
   and then " apply help" 
   The shortest solution is to invoke Lia
*)
Require Import Lia.
lia.
Qed.

(* Alternative 2: reverse the lemma about append_length ! *)
Axiom append_length' : forall l m,
  length (append l m) = length m + length l.

Lemma reverse_length' : forall l,
  length l = length (reverse l).
Proof.
induction l.
- simpl;auto.
- simpl.
  rewrite IHl.
  simpl.
  rewrite append_length'.
  simpl.
  auto.
Qed.