Proof of Novikoff's Perceptron Convergence Theorem (Unfinished)

coq_perceptron.v

Section Perceptron.

Require Import QArith List.

Inductive Q_vector : nat -> Set :=
    | vnil  : Q_vector O
    | vcons : forall n : nat,
              Q -> Q_vector n -> Q_vector (S n).
Implicit Arguments vcons [n].
Notation "x ; v" := (vcons x v)
                    (at level 80, right associativity).

Fixpoint scala_mult {n : nat} (a : Q) (v : Q_vector n)
                    : Q_vector n :=
    match v with
    | vnil   => vnil
    | x ; v' => vcons (a * x) (scala_mult a v')
    end.
Notation "a '[*]' v" := (scala_mult a v)
                        (at level 40, no associativity).

Definition inner_prod {n : nat} (v1 v2 : Q_vector n) : Q.
Proof.
    induction n as [| n' inner_prod'].
    
        (* Case : n = 0 *)
        apply 0.
    
        (* Case : n = S n' *)
        inversion_clear v1 as [| t x1 v1'].
        inversion_clear v2 as [| t x2 v2'].
        apply (x1 * x2 + inner_prod' v1' v2').
Defined.
Notation "v1 '[.]' v2" := (inner_prod v1 v2)
                          (at level 40, left associativity).

Definition vcombine_with {n : nat}
                         (op : Q -> Q -> Q) (v1 v2 : Q_vector n)
                         : Q_vector n.
Proof.
    induction n as [| n' vcombine_with'].
    
        (* Case : n = 0 *)
        apply vnil.
    
        (* Case : n = S n' *)
        inversion_clear v1 as [| t x1 v1'].
        inversion_clear v2 as [| t x2 v2'].
        apply (op x1 x2 ; vcombine_with' v1' v2').
Defined.
Infix "[+]" := (vcombine_with Qplus)
               (at level 50, left associativity).
Infix "[-]" := (vcombine_with Qminus)
               (at level 50, left associativity).

Inductive label : Set := positive | negative.

Definition predict {n : nat} (weight testee : Q_vector n)
                   : label :=
    if Qle_bool (weight [.] testee) 0 then negative
                                      else positive.

Variable observe : forall n : nat, Q_vector n -> label.
Implicit Arguments observe [n].

Definition train {n : nat} (weight testee : Q_vector n)
                 : Q_vector n :=
    match predict weight testee, observe testee with
    | positive, positive => weight
    | positive, negative => weight [-] testee
    | negative, positive => weight [+] testee
    | negative, negative => weight
    end.

Theorem Novikoff : forall (n : nat) (samples : list (Q_vector n))
                          (init_weight : Q_vector n),
                   exists trainings : list (Q_vector n),
                   incl trainings samples /\
                   (let w := fold_left train
                                       trainings init_weight in
                    forall testee : Q_vector n,
                    In testee samples ->
                    predict w testee = observe testee).
Proof.
Admitted.

End Perceptron.