conv.v

From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice path.
From mathcomp Require Import div fintype tuple finfun bigop finset fingroup perm.
From mathcomp Require Import div prime binomial ssralg finalg zmodp countalg.
From mathcomp Require Import ssrint matrix.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.


Section Test.
Definition R:=nat.
Definition Image := int -> int -> R.

Section Convolution.
    Variable n : nat.
    Variable m : nat.

    Hypothesis odd_n : odd n.
    Hypothesis odd_m : odd m.

    Local Open Scope big_scope.
    
    Definition convolution (kernel: 'M[R]_(n, m)) (I:Image) : Image :=
        fun x => fun y => \sum_i \sum_j (kernel i j) * (I x y).

End Convolution.
End Test.

Definition test_image := 
    fun i : int => fun j : int => 1%N.

Local Open Scope ring_scope.
Definition test_kernel :=
    \matrix_(i < 3%N, j < 3%N)  1%N.

Example tmp : convolution test_kernel test_image 0 0 > 1%N.
Proof.
    rewrite /convolution /test_kernel /test_image => //=.