From 8c8228f563647248831d38fb098c8434bab12a78 Mon Sep 17 00:00:00 2001
From: Julin S <famubu@rawtext.club>
Date: Fri, 27 Oct 2023 14:22:33 +0530
Subject: [PATCH] [coq] [mathcomp] add few mathcomp egs

---
 coq/mathcomp/bigop-egs.v  |  5 +++++
 coq/mathcomp/general.v    | 10 ++++++++++
 coq/mathcomp/matrix-egs.v | 24 ++++++++++++++++++++++++
 3 files changed, 39 insertions(+)
 create mode 100644 coq/mathcomp/bigop-egs.v
 create mode 100644 coq/mathcomp/general.v
 create mode 100644 coq/mathcomp/matrix-egs.v

diff --git a/coq/mathcomp/bigop-egs.v b/coq/mathcomp/bigop-egs.v
new file mode 100644
index 0000000..f41689d
--- /dev/null
+++ b/coq/mathcomp/bigop-egs.v
@@ -0,0 +1,5 @@
+From mathcomp Require Import all_ssreflect all_algebra.
+
+Lemma sum_odd_3: \sum_(0 <= i < 3.*2 | odd i) i = 3^2.
+Proof.  by rewrite unlock /=. Qed.
+
diff --git a/coq/mathcomp/general.v b/coq/mathcomp/general.v
new file mode 100644
index 0000000..5846ee5
--- /dev/null
+++ b/coq/mathcomp/general.v
@@ -0,0 +1,10 @@
+From mathcomp Require Import all_ssreflect.
+
+(** * Using [exists] *)
+Goal forall w:seq nat,
+    (exists w1 w2: seq nat, w = (w1 ++ w2)%list /\ (length w)==0%nat) -> w = [::].
+Proof.
+    move=> w [w1 [w2]].
+      by case; case: w; case: w1; case: w2.
+Qed.
+
diff --git a/coq/mathcomp/matrix-egs.v b/coq/mathcomp/matrix-egs.v
new file mode 100644
index 0000000..c6e48ad
--- /dev/null
+++ b/coq/mathcomp/matrix-egs.v
@@ -0,0 +1,24 @@
+From mathcomp Require Import all_ssreflect all_algebra.
+
+Open Scope ring_scope.
+
+(* https://coq.zulipchat.com/#narrow/stream/237664-math-comp-users/topic/A.20matrix.20mul.20proof *)
+Goal
+  let mt: 'M[bool]_(2,3) :=
+    \matrix_(i<2, j<3) (if i == 0 && (j == 1) :> nat then 1 else 0) in
+  let rw := (\row_i (if i == 0 then 1 else 0)) *m mt in
+  (\sum_j (rw 0 j)) == 1.
+Proof.
+  rewrite //=.
+  by do ![rewrite !big_ord_recl !big_ord0 !mxE].
+Qed.
+
+Lemma constMxElem {V: Type} (rows cols: nat) (v: V):
+  forall (i: 'I_rows) (j: 'I_cols),
+    (((const_mx v):'M_(rows, cols)) i j) = v.
+Proof.
+  move=> i j.
+  rewrite /const_mx unlock.
+  rewrite /fun_of_matrix /=.
+  by rewrite ffunE.
+Qed.