From VST.floyd Require Import proofauto VSU.
From LAProof.C Require Import densemat spec_alloc spec_densemat floatlib matrix_model.
From vcfloat Require Import FPStdCompCert FPStdLib.
Require Import VSTlib.spec_math VSTlib.spec_malloc.
Require Import Coq.Classes.RelationClasses.

From mathcomp Require ssreflect ssrbool ssrfun eqtype ssrnat seq choice.
From mathcomp Require fintype finfun bigop finset fingroup perm order.
From mathcomp Require div ssralg countalg finalg zmodp matrix.
From mathcomp.zify Require Import ssrZ zify.
Import fintype matrix mv_mathcomp dotprod_model.

Require Import LAProof.C.densemat_lemmas.

Unset Implicit Arguments.

Open Scope logic.

Local Definition upto_row_col {T} [m n] (A: 'M[T]_(m,n)) (i j: nat) : 'M[option T]_(m,n) :=
 \matrix_(i',j')
  if Nat.ltb i' i then Some (A i' j')
  else if Nat.ltb i i' then None
  else if Nat.ltb j' j then Some (A i' j')
  else None.

Local Ltac case_ltb := match goal with |- context [Nat.ltb ?a ?b] ⇒
    destruct (Nat.ltb_spec a b); try lia
 end.

Lemma body_densematn_mult: semax_body Vprog Gprog f_densematn_mult densematn_mult_spec.

Lemma body_densemat_mult: semax_body Vprog Gprog f_densemat_mult densemat_mult_spec.

Lemma body_densematn_dotprod: semax_body Vprog Gprog f_densematn_dotprod densematn_dotprod_spec.

Lemma body_densemat_dotprod: semax_body Vprog Gprog f_densemat_dotprod densemat_dotprod_spec.