coq-contribs/lin-alg

Linear Algebra

Linear Algebra

The Linear Algebra distribution by Jasper Stein ([email protected]) extending the (required) algebra distribution by Loic Pottier, and following Chapter 1 of "Linear Algebra" by Friedberg, Insel and Spence.

Available as package coq-lin-alg via OPAM.

Share and enjoy! Jasper Stein

lin-alg's Issues

How would I construct a specific matrix?

Hi there,

As you'll soon deduce, I'm very new to coq.

I'd like to prove the validity of some very elementary calculations with matrices, like

  (0 0) + (1 1) = (1 1)
  (0 0)   (1 1)   (1 1)

but I'm having trouble figuring out how to use this library to formulate any concrete examples of matrices.

Can you give me a hint or two? I'm happy to make a PR with this sort of calculation as an "example" once I figure out how to do it :)

I have tried the following:

Definition I2 (finite1 : fin 2) (finite2 : fin 2) : Nat :=
  (* First, extract the actual indices *)
  match finite1, finite2 return nat with
    | Build_finiteT ind1 _, Build_finiteT ind2 _ =>
      (* Then, return the appropriate value *)
      match ind1, ind2 return nat with
        | O, O => (S O)
        | (S O), (S O) => (S O)
        | _, _ => O
      end
  end.

But I'm having trouble promoting this into a Map2, MAP2, and matrix. This might not even be remotely the right direction.

for what coq versions does this work?

Work for Coq 8.9?

  - coq-lin-alg → coq < 8.9~
      not available because the package is pinned to version 8.9.0

No solution found, exiting ```