proposition: Lemma mint_eval_eq_bterm_int_fapp : forall k i fi val (v : vector (bterm k) i), let arg_eval := Vmap2 (@mat_matrixInt_prod (S k)) (args fi) (Vmap (@mi_of_term k) v) in mi_eval_aux fi (Vmap (fun t : bterm k => mint_eval val (mi_of_term t)) v) =v mint_eval val (mkMatrixInt (add_vectors (Vcons (AMatrixBasedInt.const fi) (Vmap (@AMatrixBasedInt.const A matrix dim (S k)) arg_eval))) (combine_matrices (Vmap (@args A matrix dim (S k)) arg_eval))).
proof: Proof. induction i; intros. VOtac. simpl. unfold mi_eval_aux, add_vectors. simpl. autorewrite with arith. sym. apply mint_eval_const. VSntac v. simpl mi_eval_aux. rewrite mi_eval_cons, IHi. simpl. trans (@mint_eval val (S k) (@mkMatrixInt A matrix dim (S k) (@M.mat_vec_prod dim dim (@Vhead (matrix dim dim) i (@args A matrix dim (S i) fi)) (@AMatrixBasedInt.const A matrix dim (S k) (@Vhead (mint (S k)) i (@Vmap (ABterm.bterm sig k) (mint (S k)) (@mi_of_term k) (S i) v))) [+] @add_vectors dim (S i) (@Vcons (vector A dim) (@AMatrixBasedInt.const A matrix dim (S i) fi) i (@Vmap (mint (S k)) (vector A dim) (@AMatrixBasedInt.const A matrix dim (S k)) i (@Vmap2 (matrix dim dim) (mint (S k)) (mint (S k)) (@mat_matrixInt_prod (S k)) i (@Vtail (matrix dim dim) i (@args A matrix dim (S i) fi)) (@Vtail (mint (S k)) i (@Vmap (ABterm.bterm sig k) (mint (S k)) (@mi_of_term k) (S i) v)))))) (@combine_matrices (S i) (S k) (@Vcons (vector (matrix dim dim) (S k)) (@Vmap (matrix dim dim) (matrix dim dim) (@mat_mult dim dim dim (@Vhead (matrix dim dim) i (@args A matrix dim (S i) fi))) (S k) (@args A matrix dim (S k) (@Vhead (mint (S k)) i (@Vmap (ABterm.bterm sig k) (mint (S k)) (@mi_of_term k) (S i) v)))) i (@Vmap (mint (S k)) (vector (matrix dim dim) (S k)) (@args A matrix dim (S k)) i (@Vmap2 (matrix dim dim) (mint (S k)) (mint (S k)) (@mat_matrixInt_prod (S k)) i (@Vtail (matrix dim dim) i (@args A matrix dim (S i) fi)) (@Vtail (mint (S k)) i (@Vmap (ABterm.bterm sig k) (mint (S k)) (@mi_of_term k) (S i) v)))))))). 2:{ apply mint_eval_mor. split. rewrite add_vectors_perm, (add_vectors_cons (i := S i) (mat_vec_prod (Vhead (args fi)) (AMatrixBasedInt.const (Vhead (Vmap (mi_of_term (k:=k)) v))))). refl. refl. } rewrite mint_eval_cons. apply vector_plus_mor. 2:{ rewrite Vmap_tail. refl. } rewrite H. simpl. fold (mat_matrixInt_prod (Vhead (args fi)) (mi_of_term (Vhead v))). sym. apply mint_eval_mult_factor. Qed.
imports: CoLoR(Matrix AMonAlg VecUtil OrdSemiRing ATrs LogicUtil RelUtil NatUtil AWFMInterpretation) Coq(PeanoNat Setoid Morphisms)