(** * Programming and proving with lists *)
Inductive natlist : Set :=
  | nil : natlist
  | cons : nat -> natlist -> natlist.

(** appending two lists by recursion over the first input list *)
Fixpoint append (l m : natlist) {struct l} : natlist :=
  match l with
  | nil => m
  | cons x xs => cons x (append xs m)
  end.

(** one of the following lemma's has a simple proof, without induction
   which? why? *)

Lemma append_nil_r : forall l, append l nil = l.
Proof.
induction l.
- simpl. auto.
- simpl. rewrite IHl. auto.
Qed.

Lemma append_nil_l : forall l, append nil l = l.
Proof.
simpl.
auto.
Qed.

(** in the following lemma: think about what variable to do induction over *)
Lemma append_assoc : forall l k m ,
  append l (append k m) = append (append l k) m.
Proof.
induction l.
- intros k m. simpl. auto.
- intros k m. simpl. rewrite IHl. auto.
Qed.

Fixpoint length (l : natlist) : nat :=
match l with
 | nil => 0
 | cons a k => S(length k)
end.

Lemma append_length : forall l m,
  length (append l m) = length l + length m.
Proof.
Admitted.

(** Exercise 1: define a function [list_sum : natlist -> nat] that sums up 
    all elements in a list *)
Fixpoint list_sum (l: natlist) {struct l} : nat :=
  match l with
  | nil => 0
  | cons x xs => plus x (list_sum xs)
  end.

(** Exercise 2: define a function [list_map :(nat->nat) -> natlist -> natlist]
    that applies a function [f] to all elements in a list *)
Fixpoint list_map (f : nat -> nat)(l: natlist) {struct l} : natlist :=
  match l with
  | nil => nil
  | cons x xs => cons (f x) (list_map f xs)
  end.

(** reversing a list, using append *)
Fixpoint reverse (l : natlist) : natlist :=
match l with
 | nil => nil
 | cons a k => append (reverse k) (cons a nil)
end.

Lemma reverse_append : forall l m,
  reverse (append l m) = append (reverse m) (reverse l).
Proof.
intro l.
induction l.
- simpl. intro m.
  rewrite append_nil_r. auto.
- intro m. simpl.
  rewrite IHl.
  rewrite append_assoc.
  auto.
Qed.
      
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 #<br># 
   [Lemma help : forall n: nat, S n = n + 1.] #<br>#
   and then [apply help] #<br># 
   The shortest solution is to invoke [lia], which adds all kinds
   of automation regarding a.o. arithmetic#<br>#
   It is actually _not_done_ to Import such a file inside a proof: 
  do it at the beginning of your file
*)
Require Import Lia.
lia.
Qed.

(** Alternative 2: reverse the lemma [append_length] and prove it first*)
Lemma append_length' : forall l m,
  length (append l m) = length m + length l.
Proof.
induction l.
- simpl. induction m.
  + simpl; reflexivity.
  + simpl. rewrite IHm; auto.
- intro m. simpl. rewrite IHl. induction m.
  + simpl. auto.
  +  simpl. rewrite IHm. auto.
Qed.

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.

Lemma reverse_double : forall l, reverse (reverse l) = l.
Proof.
intro l.
induction l.
- simpl. reflexivity.
- simpl.
  rewrite reverse_append.
  simpl.
  rewrite IHl.
  auto.
Qed.

(** Pretty printing of lists in the standard library *)
Require Import List.

Check list.
Print list.
(** the [list] type is defined parametrically over the carrier type [A]*)
Check cons.
Check nil.

Definition example_list := cons 1 (cons 2 (cons 3 (cons 4 nil))).

Print example_list.
(** Rocq prints the list back in its own sugared notation*)

(** And there is notation for [append] *)
Definition example_list' := example_list ++ example_list.

(** Here is how you compute with the Rocq functions *)
Eval compute in example_list'.