Fix .v files + jscoq

.gitignore

@@ -20,6 +20,5 @@
 *pdf
 **/#*#
 tex/gitrev
-coq/ch*.html
 .DS_Store
 

coq/.gitignore

@@ -0,0 +1,4 @@
+ch*.html
+index.html
+package-lock.json
+node_modules

coq/Makefile

@@ -1,10 +1,11 @@
-files=ch0.v  ch1.v  ch2.v  ch3.v  ch4.v  ch6.v  ch7.v
+files=ch0.v  ch1.v  ch2.v  ch3.v  ch4.v  ch6.v  ch7_1.v ch7_2.v ch7_3.v ch7_4.v ch7_5.v  ch8.v
 
-all: $(files:%.v=%.html)
+all: $(files:%.v=%.html) index.html
+	for f in $(files); do coqc $$f || exit 1; done
 
 ch%.html: ch%.v
 	cat jscoq_header.html > $@
-	echo "<h1>Chapter $*</h1><div><textarea id='coq'>" >> $@
+	echo "<h1>Chapter $*</h1><div><textarea id='coq-code'>" >> $@
 	cat $< >> $@
 	echo >> $@
 	echo "</textarea></div>" >> $@
@@ -13,6 +14,17 @@ ch%.html: ch%.v
 	echo "</script>" >> $@
 	cat jscoq_footer.html >> $@
 
-clean:
-	rm -f $(files:%.v=%.html)
+index.html:
+	cat index_header.html > $@
+	for file in $(files) ; do \
+		echo -n "<a href=\"" >> $@ ; \
+		echo -n $$file | sed "s/\.v/\.html/" >> $@ ; \
+		echo -n "\">" >> $@ ; \
+                echo -n "Chapter " >> $@ ; \
+                echo -n $$file | sed "s/\.v//" >> $@ ; \
+                echo "</a><br> " >> $@ ; \
+	done
+	cat index_footer.html >> $@
 
+clean:
+	rm -f $(files:%.v=%.html) index.html

coq/README.md

@@ -0,0 +1,50 @@
+# The "Mathematical Components" book code listings for jsCoq.
+
+Code snippets are intended to be viewed using jsCoq, but you also can just open
+selected `.v` file in your favorite Galina code editor. To view pages in your 
+browser locally you need install `coq`, `mathcomp`, then do `npm install` and
+`node app.js` to run node applicaion (app.js) and then open link 
+http://127.0.0.1:8010/ in your browser. A bit more detailed instructions are 
+provided below.
+
+## Installation & Run
+
+### Prerequisites
+* [Coq](https://github.com/coq/coq)
+* [The Mathematical Components library](https://github.com/math-comp/math-comp)
+* [Node.js](https://nodejs.org/en)
+
+### Installation
+* Select a directory for files, in example /home/uname/mcb/coq.
+* Put files from https://github.com/math-comp/mcb/tree/master/coq to selected
+directory.
+* Open terminal and navigate to the selected directory.
+* Type `npm install` to install dependences.
+* Type `make` to create .html files.
+
+### Run
+* Type `node app.js` to ask Node.js to serve files.
+* Navigate your browser to http://127.0.0.1:8010/ , you should see the list of
+snippets by chapters.
+
+## Editing/Contributing
+
+### Updating the code snippests
+* Edit chapter snippet file (in example, ch7.1.v).
+* Type `rm ch7.1.html && make ch7.1.html`.
+* Or alternatively type `make clean && make` to recreate all html snippet files
+in the directory (and also index.html).
+* Refresh page in your browser (if you need it).
+
+### Updating the list of snippets (index.html)
+* Add/Remove snippet file (in example, ch7.1.v).
+* Open Makefile. You will see the list of chapter files at the top of the Makefile.
+* Add/Remove file name from the list.
+* Type `rm index.html && make index.html` to generate new index.html.
+* Or alternatively type `make clean && make` to recreate all html snippet files
+in the directory and also index.html.
+
+## Homepages
+
+* Link to the [homepage of the book](https://math-comp.github.io/mcb)
+* Link to the [homepage of jsCoq](https://coq.vercel.app)

coq/app.js

@@ -0,0 +1,8 @@
+var express = require('express');
+var app = express();
+
+//setting middleware
+app.use(express.static(__dirname)); //Serves resources from current folder
+
+
+var server = app.listen(8010);

coq/ch4.v

@@ -75,6 +75,7 @@ Proof. by elim: m. Qed.
 Lemma test (G : nat -> Prop) m : G m.
 Proof.
 case: (ubnPgeq m). Show.
+Abort.
 
 Lemma edivnP m d (ed := edivn m d) :
   ((d > 0) ==> (ed.2 < d)) && (m == ed.1 * d + ed.2).

coq/ch6.v

@@ -12,7 +12,7 @@ Structure subType : Type := SubType {
   _ : forall x Px, val (@Sub x Px) = x
 }.
 End SubTypeKit.
-Implicit Arguments SubType [T P].
+Arguments SubType [T P].
 
 Notation "[ 'xsubType' 'for' v ]" :=
   (SubType _ v _ 

coq/ch7_1.v

@@ -0,0 +1,54 @@
+From mathcomp Require Import all_ssreflect.
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Module DefTupleOf.
+  Structure tuple_of n T := Tuple { tval :> seq T; _ : size tval == n }.
+  Notation "n .-tuple T" := (tuple_of n T) (at level 2).
+
+  Lemma size_tuple T n (t : n.-tuple T) : size t = n.
+  Proof. by case: t => s /= /eqP. Qed.
+
+  Example seq_on_tuple n (t : n.-tuple nat) :
+    size (rev [seq 2 * x | x <- rev t]) = size t.
+  Proof. by rewrite map_rev revK size_map. Qed.
+
+  Example just_tuple_attempt n (t : n.-tuple nat) :
+    size (rev [seq 2 * x | x <- rev t]) = size t.
+  Proof. rewrite !size_tuple. Admitted.
+
+  Notation "X (*...*)" := 
+    (let x := X in let y := _ in x) (at level 100, format "X (*...*)").
+  Notation "[LHS 'of' equation ]" := 
+    (let LHS := _ in let _infer_LHS := equation : LHS = _ in LHS) (at level 4).
+  Notation "[unify X 'with' Y ]" := 
+    (let unification := erefl _ : X = Y in True).
+
+  Fail Check forall T n (t : n.-tuple T),
+      let LHS := [LHS of size_tuple _] in
+      let RDX := size (rev t) in
+      [unify LHS with RDX].  
+
+  Variables (n : nat) (A B : Type).
+
+  Lemma rev_tupleP (t : n.-tuple A) : size (rev t) == n.
+  Proof. by rewrite size_rev size_tuple. Qed.
+
+  Canonical rev_tuple (t : n.-tuple A) := Tuple (rev_tupleP t).
+
+  Lemma map_tupleP (f : A -> B) (t : n.-tuple A) : size (map f t) == n.
+  Proof. by rewrite size_map size_tuple. Qed.
+
+  Canonical map_tuple (f : A -> B) (t : n.-tuple A) := Tuple (map_tupleP f t).
+
+  Lemma cons_tupleP (t : n.-tuple A) x : size (x :: t) == n.+1.
+  Proof. by rewrite /= size_tuple. Qed.
+
+  Canonical cons_tuple x (t : n.-tuple A) : n.+1.-tuple A :=
+    Tuple (cons_tupleP t x).
+End DefTupleOf.
+
+Example just_tuple n (t : n.-tuple nat) :
+  size (rev [seq 2 * x | x <- rev t]) = size t.
+Proof. by rewrite !size_tuple. Qed.

coq/ch7_2.v

@@ -0,0 +1,62 @@
+From mathcomp Require Import all_ssreflect.
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Module Chapter72.
+  Definition tcmp n (T : eqType) (t1 t2 : n.-tuple T) := tval t1 == tval t2.
+
+  Lemma eqtupleP n (T : eqType) : Equality.axiom (@tcmp n T).
+  Proof.
+    move => x y; apply: (iffP eqP); last first.
+      by move => ->.
+      case: x; case y => s1 p1 s2 p2 /= E.
+      rewrite E in p2 *.
+        by rewrite (eq_irrelevance p1 p2).
+  Qed.
+
+  Canonical tuple_eqTuple n T : eqType :=
+    Equality.Pack (Equality.Mixin (@eqtupleP n T)).
+
+  Check forall t : 3.-tuple nat, [:: t] == [::].
+  Check forall t : 3.-tuple bool, uniq [:: t; t].
+  Fail Check forall t : 3.-tuple (7.-tuple nat), undup_uniq [:: t; t].
+
+  Canonical tuple_subType n s := [subType for (@tval n s)].
+  Fail Definition tuple_eqMixin n T := [eqMixin of n.-tuple T by <:].
+  Canonical tuple_eqType n (T : eqType) := EqType (n.-tuple T) (@tuple_eqMixin n T).
+End Chapter72.
+
+Module Chapter721.
+  Canonical tuple_subType n T := Eval hnf in [subType for (@tval n T)].
+  Check tuple_subType.
+  Check tval.
+
+  Variables (s : seq nat) (t : 3.-tuple nat).
+  Variables size3s : size s == 3.
+  Let t1 : 3.-tuple nat := Sub s size3s.
+  Let t2 := if insub s is Some t then val (t : 3.-tuple nat) else nil.
+  Let t3 := insubd t s. (* 3.-tuple nat *)
+
+  Section SubTypeKit.
+    Variables (T : Type) (P : pred T).
+
+    Structure subType : Type := SubType {
+      sub_sort :> Type;
+      val : sub_sort -> T;
+      Sub : forall x, P x -> sub_sort;
+      (* elimination rule for sub_sort *)
+      _ : forall K (_ : forall x Px, K (@Sub x Px)) u, K u;
+      _ : forall x Px, val (@Sub x Px) = x
+    }.
+  End SubTypeKit.
+
+  Notation "[ 'subType' 'for' v ]" := (SubType _ v _
+    (fun K K_S u => let (x, Px) as u return K u := u in K_S x Px)
+    (fun x px => erefl x)).
+End Chapter721.
+
+Module Chapter722.
+  Theorem eq_irrelevance (T : eqType) (x y : T) : forall e1 e2 : x = y, e1 = e2.
+  Proof. Admitted.
+End Chapter722.

coq/ch7_3.v

@@ -0,0 +1,28 @@
+From mathcomp Require Import all_ssreflect.
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Notation count_mem x := (count [pred y | y == x]).
+
+Module finite.
+  Definition axiom (T : eqType) (e : seq T) :=
+    forall x : T, count_mem x e = 1.
+
+  Record mixin_of (T : eqType) := Mixin {
+    enum : seq T;
+    _ : @axiom T enum;                                  
+  }.
+End finite.
+
+(* Definition mytype_finMixin := Finite.Mixin mytype_enum mytype_enumP. *)
+(* Canonical mytype_finType := @Finite.Pack mytype mytype_finMixin. *)
+
+(* Lemma myenum_uniq : uniq myenum. *)
+(* Lemma mem_myenum : forall x : T, x \in myenum. *)
+(* Definition mytype_finMixin := Finite.UniqFinMixin myenum_uniq mem_myenum. *)
+
+Lemma cardT (T : finType) : #|T| = size (enum T).
+Proof. Admitted.
+Lemma forallP (T : finType) (P : pred T) : reflect (forall x, P x) [forall x, P x].
+Proof. Admitted.

coq/ch7_4.v

@@ -0,0 +1,48 @@
+From mathcomp Require Import all_ssreflect.
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Module Ordinal74.
+  Inductive ordinal (n : nat) : Type := Ordinal m of m < n.
+  Notation "''I_' n" := (ordinal n).
+
+  Coercion nat_of_ord n (i : ordinal n) := let: Ordinal m _ := i in m.
+  Canonical ordinal_subType n := [subType for (@nat_of_ord n)].
+  Definition ordinal_eqMixin n := Eval hnf in [eqMixin of (@ordinal n) by <:].
+  Canonical ordinal_eqType n :=
+    Eval hnf in EqType (ordinal n) (ordinal_eqMixin n).
+
+  Definition ord_enum n : seq (ordinal n) := pmap insub (iota 0 n).
+End Ordinal74.
+
+Lemma val_ord_enum n : map val (ord_enum n) = iota 0 n.
+Proof.
+  rewrite pmap_filter; last by exact: insubK.
+    by apply/all_filterP; apply/allP => i; rewrite mem_iota isSome_insub.
+Qed.
+
+Lemma ord_enum_uniq n : uniq (ord_enum n).
+Proof. by rewrite pmap_sub_uniq ?iota_uniq. Qed.
+
+Lemma mem_ord_enum n i : i \in (ord_enum n).
+Proof.
+    by rewrite -(mem_map (@ord_inj n)) (val_ord_enum n) mem_iota ltn_ord.
+Qed.
+
+Definition ordinal_finMixin n :=
+  Eval hnf in UniqFinMixin (ord_enum_uniq n) (@mem_ord_enum n).
+
+Canonical ordinal_finType n :=
+  Eval hnf in FinType (ordinal n) (ordinal_finMixin n).
+
+Lemma tnth_default T n (t : n.-tuple T) : 'I_n -> T.
+Proof. by rewrite -(size_tuple t); case (tval t) => [|//] []. Qed.
+
+Definition tnth T n (t : n.-tuple T) (i : 'I_n) : T :=
+  nth (tnth_default t i) t i.
+
+Definition enum_rank (T : finType) : T -> 'I_#|T|.
+Admitted.
+
+