formal_verification_hello_world.v

Inductive List (A : Type) : Type :=
| Nil : List A
| Cons : A -> List A -> List A.


Arguments Nil {A}.
Arguments Cons {A}.


Eval compute in Cons 1 (Cons 2 Nil).

Fixpoint append {A : Type} (lsa lsb : List A) : List A :=
  match lsa with
  | Nil => lsb
  | Cons hlsa tlsa => Cons hlsa (append tlsa lsb)
  end.
          

Theorem append_nil_l {A : Type} :
  forall (u : List A), append Nil u = u.
Proof.      
  intros u.
  simpl.
  reflexivity.
Qed.

Theorem append_nil_l_prog {A : Type} :
  forall (u : List A), append Nil u = u.
Proof.      
 refine (fun u => eq_refl).
Qed.

Theorem append_nil_r {A : Type} :
  forall (u : List A), append u Nil = u.
Proof.
  induction u;
    simpl.
  + reflexivity.
  + rewrite IHu.
    reflexivity.
Qed.

Theorem append_nil_r_prog {A : Type} :
  forall (u : List A), append u Nil = u.
Proof.
  refine
    (fix Fn u {struct u} :=
       match u with
       | Nil => eq_refl
       | Cons h t => _ 
       end); simpl;
    rewrite Fn;
    exact eq_refl.
Qed.  


Theorem append_associative {A : Type} :
  forall (u v w : List A),
    append (append u v) w = append u (append v w).
Proof.
  induction u;
    simpl.
  + intros *.
    reflexivity.
  + intros *.
    rewrite IHu.
    reflexivity.
Qed.

Theorem append_associative_prog {A : Type} :
  forall (u v w : List A),
    append (append u v) w = append u (append v w).
Proof.
  refine
    (fix Fn u {struct u} :=
       match u with
       | Nil => fun v w => eq_refl
       | Cons h t => fun v w => _ 
       end); simpl;
    rewrite Fn;
    exact eq_refl.
Qed.