port to math-comp 2 + vertical cell repo + flavor branch

.github/workflows/docker-action.yml

@@ -6,13 +6,9 @@ on:
   push:
     branches:
       - master
-    paths-ignore:
-      - 'documents/**'
   pull_request:
     branches:
       - '**'
-    paths-ignore:
-      - 'documents/**'
 
 jobs:
   build:
@@ -21,8 +17,7 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.16.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.16.0-coq-8.16'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.19'
       fail-fast: false
     steps:
       - uses: actions/checkout@v3

.gitignore

@@ -8,7 +8,7 @@
 Makefile.coq
 Makefile.coq.conf
 .Makefile.coq.d
-html/*.cmo
-html/*.cmi
-html/*.bytes
-html/*.js
+www/*.cmo
+www/*.cmi
+www/*.bytes
+www/*.js

README.md

@@ -6,8 +6,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 
 [![Docker CI][docker-action-shield]][docker-action-link]
 
-[docker-action-shield]: https://github.com/math-comp/trajectories/workflows/Docker%20CI/badge.svg?branch=master
-[docker-action-link]: https://github.com/math-comp/trajectories/actions?query=workflow:"Docker%20CI"
+[docker-action-shield]: https://github.com/math-comp/trajectories/actions/workflows/docker-action.yml/badge.svg?branch=master
+[docker-action-link]: https://github.com/math-comp/trajectories/actions/workflows/docker-action.yml
 
 
 
@@ -20,20 +20,20 @@ TODO
   - Reynald Affeldt (initial)
   - Yves Bertot (initial)
 - License: [CeCILL-C](LICENSE)
-- Compatible Coq versions: Coq >= 8.15, MathComp >= 1.16
+- Compatible Coq versions: Coq >= 8.17, MathComp >= 2.2.0
 - Additional dependencies:
-  - [MathComp ssreflect 1.15 or later](https://math-comp.github.io)
-  - [MathComp fingroup 1.15 or later](https://math-comp.github.io)
-  - [MathComp algebra 1.15 or later](https://math-comp.github.io)
-  - [MathComp solvable 1.15 or later](https://math-comp.github.io)
-  - [MathComp field 1.16 or later](https://math-comp.github.io)
-  - [Mathcomp real closed 1.1.3 or later](https://github.com/math-comp/real-closed/)
-  - [Algebra tactics 1.0.0](https://github.com/math-comp/algebra-tactics)
-  - [MathComp analysis](https://github.com/math-comp/analysis)
-  - [Infotheo](https://github.com/affeldt-aist/infotheo)
+  - [MathComp ssreflect 2.2.0 or later](https://math-comp.github.io)
+  - [MathComp fingroup 2.2.0 or later](https://math-comp.github.io)
+  - [MathComp algebra 2.2.0 or later](https://math-comp.github.io)
+  - [MathComp solvable 2.2.0 or later](https://math-comp.github.io)
+  - [MathComp field 2.2.0 or later](https://math-comp.github.io)
+  - [Mathcomp real closed 2.0.0 or later](https://github.com/math-comp/real-closed/)
+  - [Algebra tactics 1.2.0 or later](https://github.com/math-comp/algebra-tactics)
+  - [MathComp analysis 1.0.0 or later](https://github.com/math-comp/analysis)
+  - [Infotheo 0.7.0 of later](https://github.com/affeldt-aist/infotheo)
 - Coq namespace: `mathcomp.trajectories`
 - Related publication(s):
-  - [TODO](TODO) doi:[TODO](https://doi.org/TODO)
+  - [Safe Smooth Paths between Straight Line Obstacles](https://inria.hal.science/hal-04312815) doi:[https://doi.org/10.1007/978-3-031-61716-4_3](https://doi.org/https://doi.org/10.1007/978-3-031-61716-4_3)
 
 ## Building and installation instructions
 
@@ -70,6 +70,9 @@ references:
   https://hal.inria.fr/inria-00503017v2/document
 - Theorem of three circles in Coq (2013)
   https://arxiv.org/abs/1306.0783
+- Safe Smooth Paths between straight line obstacles
+  https://inria.hal.science/hal-04312815
+  https://link.springer.com/chapter/10.1007/978-3-031-61716-4_3
 
 ## Development information
 

_CoqProject

@@ -1,3 +1,4 @@
+theories/shortest_path.v
 theories/generic_trajectories.v
 theories/smooth_trajectories.v
 theories/convex.v
@@ -22,6 +23,16 @@ theories/encompass.v
 theories/counterclockwise.v
 theories/axiomsKnuth.v
 theories/preliminaries_hull.v
+theories/cells.v
+theories/cells_alg.v
+theories/door_crossing.v
+theories/events.v
+theories/extraction_command.v
+theories/math_comp_complements.v
+theories/no_crossing.v
+theories/opening_cells.v
+theories/points_and_edges.v
+theories/safe_cells.v
 
 -R theories trajectories
 

coq-mathcomp-trajectories.opam

@@ -17,16 +17,16 @@ TODO"""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" { (>= "8.14" & < "8.17~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "1.16.0" & < "1.17~") | (= "dev") }
-  "coq-mathcomp-fingroup" { (>= "1.16.0" & < "1.17~") | (= "dev") }
-  "coq-mathcomp-algebra" { (>= "1.16.0" & < "1.17~") | (= "dev") }
-  "coq-mathcomp-solvable" { (>= "1.16.0" & < "1.17~") | (= "dev") }
-  "coq-mathcomp-field" { (>= "1.16.0" & < "1.17~") | (= "dev") }
-  "coq-mathcomp-real-closed" { (>= "1.1.3") | (= "dev") }
-  "coq-mathcomp-algebra-tactics" { (>= "1.0.0") | (= "dev") }
-  "coq-mathcomp-analysis" { (>= "0.6.1") & (< "0.7~")}
-  "coq-infotheo" { >= "0.5.1" & < "0.6~"}
+  "coq" { (>= "8.17" & < "8.20~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "2.2.0") | (= "dev") }
+  "coq-mathcomp-fingroup" { (>= "2.2.0") | (= "dev") }
+  "coq-mathcomp-algebra" { (>= "2.2.0") | (= "dev") }
+  "coq-mathcomp-solvable" { (>= "2.2.0") | (= "dev") }
+  "coq-mathcomp-field" { (>= "2.2.0") | (= "dev") }
+  "coq-mathcomp-real-closed" { (>= "2.0.0") | (= "dev") }
+  "coq-mathcomp-algebra-tactics" { (>= "1.2.0") | (= "dev") }
+  "coq-mathcomp-analysis" { (>= "1.0.0") }
+  "coq-infotheo" { >= "0.7.0"}
 ]
 
 tags: [

documents/FHG_slides.tex

@@ -0,0 +1,192 @@
+\documentclass[compress]{beamer}
+\usepackage[latin1]{inputenc}
+\usepackage{alltt}
+\newdimen\topcrop
+\topcrop=10cm  %alternatively 8cm if the pdf inclusions are in letter format
+\newdimen\topcropBezier
+\topcropBezier=19cm %alternatively 16cm if the inclusions are in letter format
+
+\setbeamertemplate{footline}[frame number]
+\title{Smooth trajectories in straight line mazes}
+\author{Yves Bertot\\
+Joint work with Thomas Portet, Quentin Vermande}
+\date{April 2023}
+\mode<presentation>
+\begin{document}
+
+\maketitle
+\begin{frame}
+\frametitle{The game}
+\begin{itemize}
+\item Apply Type Theory-based verification to a problem understood by a
+  wide audience
+\item Find a smooth path in a maze
+\item Decompose the problem
+\begin{itemize}
+\item Find a discrete approximation of the problem
+\item Construct a piece-wise linear path
+\item smoothen the angles
+\end{itemize}
+\item Prove the correctness of the algorithm
+\begin{itemize}
+\item Safety: absence of collision
+\item work in progress
+\end{itemize}
+\end{itemize}
+\end{frame}
+\begin{frame}
+\frametitle{Example}
+\includegraphics[trim={0 0 0 \topcrop}, clip, width=\textwidth]{empty_spiral.pdf}
+\end{frame}
+\begin{frame}
+\frametitle{Cell decomposition}
+\begin{itemize}
+\item Decompose the space into simple cells
+\item Each cell is convex
+\item Each cell is free of obstacles
+\item Each cell may have safely reachable neighbors
+\end{itemize}
+\end{frame}
+\begin{frame}
+\frametitle{Vertical cell decomposition example}
+\includegraphics[trim={0 0 0 \topcrop}, clip, width=\textwidth]{cells_spiral.pdf}
+\end{frame}
+\begin{frame}
+\frametitle{Cell properties}
+\begin{itemize}
+\item Vertical edges are safe passages between two cells
+\item Moving directly from a left-edge to a right-edge is safe
+\begin{itemize}
+\item and vice-versa
+\end{itemize}
+\item Moving from a left-edge to the cell center is safe
+\begin{itemize}
+\item similarly for a right-edge
+\item moving from left-edge to left-edge is safe by going through the
+  cell center
+\end{itemize}
+\end{itemize}
+\end{frame}
+\begin{frame}
+\frametitle{Finding a path in the cell graph}
+\begin{itemize}
+\item A discrete path from cell to cell is found by breadth-first search
+\item Connected components of the graph are defined by polygons
+\item Special care for points that are already on the common edge of two cells
+\item Recent improvement: take distances into account
+\begin{itemize}
+\item Use a graph of doors instead of cells
+\item Easier to associate a distance between pairs of doors
+\item Dijkstra shortest path algorithm
+\end{itemize}
+\item In the end, a path from door to door
+\end{itemize}
+\end{frame}
+\begin{frame}
+\frametitle{Two examples of elementary safe paths}
+\includegraphics[trim={0 0 0 \topcrop}, clip, width=\textwidth]{spiral_safe2.pdf}
+\end{frame}
+\begin{frame}
+\frametitle{piecewise linear path}
+\label{broken-line}
+\includegraphics[trim={0 0 0 \topcrop}, clip, width=\textwidth]{spiral_bline.pdf}
+\end{frame}
+\begin{frame}
+\frametitle{Making corners smooth}
+\begin{itemize}
+\item Using quadratic Bezier curves
+\item Bezier curves are given by a set of control points
+   (3 for a quadratic curve)
+\item Points on the curves are obtained by computing weighted barycenters
+\begin{itemize}
+\item The curve is enclosed in the convex hull of the control points
+\end{itemize}
+\item Given control points \(a_0, a_1, \ldots, a_{n-1}, a_n\), \(a_0, a_1\)
+is tangent to the curve in \(a_0\)
+\begin{itemize}
+\item same for \(a_{n-1}, a_n\) in \(a_n\)
+\end{itemize}
+\end{itemize}
+\end{frame}
+\begin{frame}
+\frametitle{Bezier curve illustration}
+\begin{itemize}
+\item How the point for ratio \(4/9\) is computed
+\item Control points for the two subcurves are given by the new point,
+the initial starting and end points, and the solid green straight edge tip
+\end{itemize}
+\includegraphics[trim={0 6cm 0 \topcropBezier}, clip, width=\textwidth]{bezier_example2.pdf}
+\end{frame}
+\begin{frame}
+\frametitle{Using Bezier curves for smoothing}
+\begin{itemize}
+\item Add extra points in the middle of each straight line segment
+\item Uses these extra points as first and last control points for Bezier curves
+\item Use the angle point as the middle control point
+\item Check the Bezier curve for collision and repair if need be
+\end{itemize}
+\end{frame}
+\begin{frame}
+\frametitle{Collision checking, graphically}
+\includegraphics[trim={0 4cm 0 17cm}, clip, width=\textwidth]{collision.pdf}
+\end{frame}
+\begin{frame}
+\frametitle{Not passing in the top door}
+\includegraphics[trim={0 4cm 0 17cm}, clip, width=\textwidth]{collision2.pdf}
+\end{frame}
+\begin{frame}
+\frametitle{Final trajectories}
+\label{final-spiral}
+\includegraphics[trim={0 0 0 \topcrop}, clip, width=\textwidth]{smooth_spiral2.pdf}
+\end{frame}
+\begin{frame}
+\frametitle{Proof tools}
+\begin{itemize}
+\item Convex hulls (Pichardie \& B. 2001)
+\begin{itemize}
+\item Orientation predicate
+\item point below or above edge
+\end{itemize}
+\item Linear arithmetic
+\begin{itemize}
+\item Algorithms only use rational numbers
+\item Bezier curve intersections rely on algebraic numbers
+\end{itemize}
+\item Convex spaces and Bezier Curve
+\begin{itemize}
+\item Internship by Q. Vermande
+\item Using {\tt infotheo}, especially convex and conical spaces
+         (Affeldt \& Garrigue \& Saikawa 2020)
+\end{itemize}
+\end{itemize}
+\end{frame}
+\begin{frame}
+\frametitle{Vertical cell decomposition proofs}
+\begin{itemize}
+\item Use of semi-closed vertical cells
+\item Show disjoint property
+\item Show that obstacles are covered by cell tops
+\end{itemize}
+\end{frame}
+\begin{frame}
+\frametitle{Future work}
+\begin{itemize}
+\item Intend to prove only safety
+\item Produce concrete code from abstract models
+\begin{itemize}
+\item Move from exact computation to approximations
+\item Efficient implementation of graphs
+\end{itemize}
+\item Already usable in \textcolor{blue}{\href{https://stamp.gitlabpages.inria.fr/trajectories.html}{web-base demonstration}.}
+\begin{itemize}
+\item Extracted code to Ocaml, then compile to JavaScript
+\end{itemize}
+\end{itemize}
+\end{frame}
+\end{document}
+
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: t
+%%% End: 

documents/Makefile

@@ -1,4 +1,4 @@
-all : intro_slides.pdf FHG_paper.pdf
+all : intro_slides.pdf FHG_paper.pdf FHG_slides.pdf
 
 PSFILES=bezier_example.ps bezier_example2.ps cells_spiral.ps \
   collision.ps collision2.ps empty_spiral.ps polygon.ps repair2.ps \
@@ -16,5 +16,8 @@ FHG_paper.pdf : FHG_paper.tex FHG_paper.bib $(PDFFILES) illustration.png
 	pdflatex FHG_paper.tex; bibtex FHG_paper; pdflatex FHG_paper.tex \
         FHG_paper.tex
 
+FHG_slides.pdf : FHG_slides.tex $(PDFFILES)
+	PDFLATEX FHG_slides.tex; pdflatex FHG_slides.tex
+
 $(PDFFILES): %.pdf: %.ps
 	ps2pdf -sPAPERSIZE=a4 $<