lesson6.html

<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml">

<head>
    <meta http-equiv="content-type" content="text/html;charset=utf-8" />

    <link rel="stylesheet" href="jscoq/node_modules/bootstrap/dist/css/bootstrap.min.css" />

    <title>Machine-Checked Mathematics</title>
    <link rel="stylesheet" href="local.css" />

    <script src='https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.5/MathJax.js?config=TeX-MML-AM_CHTML'
        async></script>
    <script src="Blob.js" type="text/javascript"></script>
    <script src="FileSaver.js" type="text/javascript"></script>

</head>

<body>
    <div id="ide-wrapper" class="toggled">
        <div id="code-wrapper">
            <div id="document">
                <p>
                Use ALT-(up-arrow) and ALT-(down-arrow) to process this document inside your browser, line-by-line. 
		Use ALT-(right-arrow) to go to the cursor. 
                You can
                <span class="save-button" onClick="save_coq_snippets()">save your edits</span>
                inside your browser and
                <span class="save-button" onClick="load_coq_snippets()">load them back</span>.
                <!-- (edits are also saved when you close the window) -->
                Finally, you can
                <span class="save-button" onClick="download_coq_snippets()">download</span>
                your working copy of the file, e.g., for sending it to teachers.
                <hl />
                </p>
<div><textarea id='coq-ta-1'>
From mathcomp Require mini_ssreflect.

Reserved Notation "x == y" (at level 70, no associativity).

(* Set Implicit Arguments. *)
(* Unset Strict Implicit. *)
(* Unset Printing Implicit Defensive. *)
</textarea></div>
<div><p>
<hr/>

<div class="slide vfill">
<p>
<h2>
 Type-inference Based Automation
</h2>

<p>
Today:
<p>
<ul class="doclist">
  <li> Automating the synthesis of statements

  </li>
<li> Automating proofs by enhanced unification

</li>
<li> Mathematical structures in dependent type theory

</li>
</ul>
</div>
<hr/>

<div class="slide vfill">
<p>
<h2>
 Redundant annotations: polymorphism
</h2>

<p>
Remember, from Lesson 2, the definition of the (polymorphic) type of lists, of which we make an isomorphic copy here:
<p>
<div>
</div>
<div><textarea id='coq-ta-2'>
Module ImplicitsForLists.

Inductive list (A : Type) : Type :=
    nil : list A | cons : A -> list A -> list A.

About nil.
About cons.
</textarea></div>
<div><p>
</div>
<p>
Except that our copy is not (yet) configured: it 
behaves <quote>as on a black board</quote>.
In fact, a well-typed term of type <tt>list A</tt> features many copies of the polymorphic parameter <tt>A</tt>:
<p>
<div>
</div>
<div><textarea id='coq-ta-3'>
Check cons nat 3 (cons nat 2 (nil nat)).
</textarea></div>
<div><p>
</div>
<p>
Yet the proof assistant is able to infer the value of this parameter, from the type of elements stored in the list:
<p>
<div>
</div>
<div><textarea id='coq-ta-4'>
Check cons _ 3 (cons _ 2 (nil _)).
</textarea></div>
<div><p>
</div>
<p>
Therefore, we can configure the definition, so that we do not even have
to mention the holes:
<div>
</div>
<div><textarea id='coq-ta-5'>
Arguments cons {A}.
Arguments nil {A}.

Fail Check cons _ 3 (cons _ 2 (nil _)).
Check cons 3 (cons 2 nil).

End ImplicitsForLists.

</textarea></div>
<div><p>
</div>
<p>
</div>
<hr/>

<div class="slide vfill">
<p>
<h2>
 Matching and unification
</h2>

<p>
In Lesson 3, we have seen that tactics use information from the goal, to compute relevant instances of lemmas.
<p>
This is typically the case with the <tt>apply:</tt> tactic:
<div>
</div>
<div><textarea id='coq-ta-6'>
Module Tactics.
Import mini_ssreflect.

(* do not care about these declarations, they are
   just here to have as many implicit arguments as possible. *)

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Variable (P : nat -> Prop).

Lemma apply_example1 (n m : nat)  : (forall k, P k) -> P 4.
Proof.
move=> h.
apply: h.
Qed.

</textarea></div>
<div><p>
</div>
<p>
Although it cannot guess arbitrary information, as balance has to be 
maintained between automation and efficiency:
<p>
<div>
</div>
<div><textarea id='coq-ta-7'>
Lemma apply_example2 : (forall k l , P (k * l)) -> P 6.
Proof.
move=> h.
Fail apply: h.
apply: (h 2 3).
Qed.

End Tactics.
</textarea></div>
<div><p>
</div>
<p>
</div>
<hr/>

<div class="slide vfill">
<p>
<h2>
 Coercions
</h2>

<p>
So far, the information inferred by the proof assistant was based on
constraints coming from typing rules and matching.
<p>
But the user can also add extra inference features, based on the content of the libraries.
<p>
This is what we have done in Lecture 2 and 3 when discussing how terms of type <tt>bool</tt> could be promoted to the status of statement, i.e., terms of type <tt>Prop</tt>.
<p>
<div>
</div>
<div><textarea id='coq-ta-8'>

Module Coercion.

Fail Check false : Prop.

Import mini_ssreflect.

Check false : Prop.

Set Printing Coercions.

Check false : Prop.

Print is_true.

Variables (A B : Set) (a : A).

Variable f : A -> B.

Fail Check a : B.

Coercion f : A >-> B.

Check a : B.

Unset Printing Coercions.

End Coercion.

</textarea></div>
<div><p>
<div>
<p>
Caveat: use with care, as it can obfuscate statements...
</div>
<hr/>

<div class="slide vfill">
<p>
<h2>
 Dependent pairs
</h2>

<p>
In Lesson 3, we have discussed the extension of a dependently typed lambda calculus with inductive types, so as to better represent constructions, e.g. natural numbers, booleans, etc.
<p>
Here is an important example of extension, introducing dependent pairs. Let us start with the introduction (typing) rule:
<p>
$$\frac{\Gamma \vdash T\ :\ Set \quad \Gamma \vdash P\ :\ T \rightarrow Prop}{\Gamma \vdash \Sigma x\ :\ T, p\ x : Set} $$
<p>
Using Coq's inductive types, this becomes:
<p>
<div>
</div>
<div><textarea id='coq-ta-9'>
Module InductiveDependentPairs.

Section InductiveDependentPairs.

Variables (T : Set) (P :  T -> Prop).

Inductive dep_pair : Set := MkPair (t : T) (p : P t).

Check MkPair.

</textarea></div>
<div><p>
</div>
<p>
And here are the projections of a pair onto its components:
<div>
</div>
<div><textarea id='coq-ta-10'>

Definition proj1 (p : dep_pair) : T :=
  match p with
  |MkPair x px => x
  end.

About proj1.

Definition proj2 (p : dep_pair) : P (proj1 p) :=
  match p with
  |MkPair x px => px
  end.

About proj2.

End InductiveDependentPairs.

About proj1.

About proj2.

End InductiveDependentPairs.

</textarea></div>
<div><p>
</div>
<p>
Coq provides a specific syntax to define a dependent pair and its projections in one go:
<p>
<div>
</div>
<div><textarea id='coq-ta-11'>

Section RecordDependentPair.

Variables (T : Set) (P :  T -> Prop).

Record dep_pair : Set := MkPair {proj1 : T; proj2 : P proj1}.

About MkPair.

About proj1.

About proj2.

End RecordDependentPair.

</textarea></div>
<div><p>
</div>
<p>
Dependent pairs can be used to define a sub-type, i.e., a type for a sub-collection of elements in a given type. Here is a type for strictly positive natural numbers:
<div>
</div>
<div><textarea id='coq-ta-12'>

Module PosNat.

Import mini_ssreflect.

Record pos_nat : Set := PosNat {val : nat; pos_val : 1 <= val}.
</textarea></div>
<div><p>
</div>
<p>
And here is a way to build terms of type <tt>pos_nat</tt>:
<p>
<div>
</div>
<div><textarea id='coq-ta-13'>

Lemma pos_S (x : nat) : 1 <= S x.
Proof. by []. Qed.

Definition pos_nat_S (n : nat) : pos_nat := PosNat (S n) (pos_S n).

</textarea></div>
<div><p>
</div>
<p>
Still, this is a sub-type, and not a sub-set: functions expecting
arguments in <tt>nat</tt> do not apply:
<p>
<div>
</div>
<div><textarea id='coq-ta-14'>

Fail Lemma pos_nat_add (x y : pos_nat) : 1 <= x + y.

</textarea></div>
<div><p>
</div>
<p>
But we can correct this using a coercion.
<p>
<div>
</div>
<div><textarea id='coq-ta-15'>

Coercion val : pos_nat >-> nat.

Lemma pos_add (x y : pos_nat) : 1 <= x + y.
Proof. by rewrite addn_gt0; case: x => x ->. Qed.

</textarea></div>
<div><p>
</div>
<p>
And we can use this lemma to define a new term of type <tt>pos_nat</tt>, 
from two existing ones:
<p>
<div>
</div>
<div><textarea id='coq-ta-16'>
Definition pos_nat_add (x y : pos_nat) : pos_nat := PosNat _ (pos_add x y).
</textarea></div>
<div><p>
</div>
<p>
</div>
<hr/>

<div class="slide vfill">
<p>
<h2>
 Currying
</h2>

<p>
<div>
<p>
</div>
<p>
As you may have noticed, we have been stating lemmas using chains 
of implications rather than conjunctions.
<p>
This is because a conjunction is a pair of facts, and most of the
time we will have to break this pair, in order to use each hypothesis.
<p>
<div>
</div>
<div><textarea id='coq-ta-17'>

Section Curry.

Variables A B C : Prop.
Hypothesis hAC : A -> C.

Lemma uncurry : A /\ B -> C.
Proof. move=> hAB. apply: hAC. case: hAB => hA hB. by []. Qed.

Lemma curry : A -> B -> C.
Proof. move=> hA hB. apply: hAC. by []. Qed.

End Curry.
</textarea></div>
<div><p>
</div>
<p>
</div>
<hr/>

<div class="slide vfill">
<p>
<h2>
 Uncurry
</h2>

<p>
Dependent pairs also allow to phrase statements in a curry- or uncurry-style. 
<p>
For instance, consider a predicate (a property) P on natural numbers,
which holds for any strictly positive number.
<p>
<div>
</div>
<div><textarea id='coq-ta-18'>

Section PosNatAutomation.

Variable P : nat -> Prop.

</textarea></div>
<div><p>
</div>
<p>
We can phrase this property on P in two different style:
<p>
<div>
</div>
<div><textarea id='coq-ta-19'>

Hypothesis posP1 : forall n : nat, 0 < n -> P n.

Hypothesis posP2 : forall p : pos_nat, P p.

Set Printing Coercions.

About posP2.

</textarea></div>
<div><p>
</div>
<p>
Now, let us prove a toy corollary of this property, using the two 
different variants. First using <tt>posP1</tt>:
<p>
<div>
</div>
<div><textarea id='coq-ta-20'>

Lemma Pexample1 (x : nat) : P (S x + 3).
Proof.
apply: posP1.
rewrite addn_gt0.
by [].
Qed.

</textarea></div>
<div><p>
</div>
<p>
The proof possibly requires using one step per symbol used in the
expression, provided the symbol refers to an operation preserving
strict positivity, like <tt>+</tt>.
<p>
This calls for some automation, implemented as a dedicated tactic.
</div>
<hr/>

<p>
<div class="slide vfill">
<p>
<h2>
 Augmenting unification
</h2>

<p>
Let us now see how things work with the second version of the hypothesis. In fact, it stops quite soon:
<div>
</div>
<div><textarea id='coq-ta-21'>

Lemma Pexample2 (x : nat) : P ((S x) + 3).
Proof.
Fail apply: posP2.
Abort.
</textarea></div>
<div><p>
</div>
<p>
The problem here is that unifying <tt>P ((S x) + 3</tt> with the conclusion
of <tt>posP2</tt> does not work, as it requires guessing the value of a pair
from the sole value of its first component:
<p>
<pre>
    P ((S x) + 3) ~ P (val ?)         ? : pos_nat
</pre>
<p>
which is an instance of the following problem:
<p>
<pre>
    n + m ~  val ?         ? : pos_nat
</pre>
<p>
Now if <tt>n</tt> and <tt>m</tt> are not arbitrary terms, but themselves
projections of terms in <tt>pos_nat</tt>, we have a candidate solution 
at hand:
<p>
<div>
</div>
<div><textarea id='coq-ta-22'>

Goal forall x y : pos_nat, val x + val y = val (pos_nat_add x y).
by [].
Qed.
</textarea></div>
<div><p>
</div>
<p>
We just need to inform Coq that we want this solution to be used
to solve this otherwise unsolvable problem:
<p>
<div>
</div>
<div><textarea id='coq-ta-23'>

Canonical pos_nat_add.

Lemma Pexample2' (x y : pos_nat) : P (x + y).
Proof.
apply: posP2.
Qed.

</textarea></div>
<div><p>
</div>
<p>
This worked because Coq was able to infer a solution of the form:
<pre>
   (val x) + (val y) ~ val (pos_nat_add x y)
</pre>
<p>
<div>
</div>
<div><textarea id='coq-ta-24'>

Lemma Pexample2 (x : nat) : P ((S x) + 3).
Proof.
Fail apply: posP2.
Abort.

</textarea></div>
<div><p>
</div>
<p>
Now the problem has been turned into:
<p>
<pre>
    P ((S x) + 3) ~ P (val (pos_nat_add ?1 ?2)         ?1, ?2 : pos_nat
    S x ~ val ?1
    3   ~ val ?2

</pre>
<p>
But once again, these problems do not have intrinsic solutions: we
have to inform the unification algorithm of the lemma <tt>pos_nat_S</tt>.
<p>
<div>
</div>
<div><textarea id='coq-ta-25'>

Goal forall n : nat, S n = val (pos_nat_S n).
Proof. by []. Qed.

Canonical pos_nat_S.

Lemma Pexample2'' (n : nat) : P (S n).
Proof.
apply: posP2.
Qed.

Lemma Pexample2 (x : nat) : P ((S x) + 3).
Proof.
apply: posP2.
Abort.

End PosNatAutomation.

End PosNat.

</textarea></div>
<div><p>
</div>
<p>
</div>
<hr/>

<p>
<div class="slide vfill">
<h2>
 Structures as dependent tuples
</h2>

<p>
Dependent pairs generalize to dependent tuples:
<p>
$$ \Sigma x_1\ :\ T_1 \Sigma x_2\ :\ T_2\ x_1 \dots \Sigma x_{n+1}\ :\ T_{n +1} x_1\ \dots\ x_n $$
<p>
Just like sequences \( (x_1, x_2 \dots, x_n) \) 
flatten nested pairs \( (x_1, (x_2, (\dots, x_n)) \), 
dependent tuples flatten dependent pairs.
<p>
Dependent tuples are represented by inductive types with a single constructor, and \(n\) arguments. Here is an example:
<p>
<div>
</div>
<div><textarea id='coq-ta-26'>

Module EqType.

Import mini_ssrfun mini_ssrbool.

Definition eq_axiom (T : Type) (op : T -> T -> bool) : Prop :=
   forall x y : T, reflect (x = y) (op x y) .

Record eqType : Type := 
  EqType {car : Type; eq_op : car -> car -> bool; eqP : eq_axiom _ eq_op}.

</textarea></div>
<div><p>
</div>
<p>
Dependent tuples can indeed model mathematical structures, which
bundle a carrier set (here a type) with subsets, operations, 
and prescribed properties on these data.
<p>
<div>
</div>
<div><textarea id='coq-ta-27'>

Record monoid : Set := 
  Monoid {
      mon_car : Set; 
      mon_op : mon_car -> mon_car -> mon_car;
      mon_e : mon_car;
      mon_opA : associative mon_op;
      mon_opem : left_id mon_e mon_op;
      mon_opme : right_id mon_e mon_op
    }.

</textarea></div>
<div><p>
</div>
<p>
<p><br/><p>
<p>
<div class="note">(notes)<div class="note-text">
<p>
Dependent tuples ressemble contexts, i.e., sequences of variables paired with types, with dependencies coming in order. Such a sequence is sometimes also refered to as a <i>telescope</i>, a terminology introduced by de Bruijn in
<a href="https://www.win.tue.nl/automath/archive/pdf/aut103.pdf">this</a> paper.
</div></div>
<p>
</div>
<hr/>

<p>
<div class="slide vfill">
<h2>
 Sharing notations and theory
</h2>

<p>
In Lesson 2, we defined an infix notation <tt>==</tt> for equality on type <tt>nat</tt>. 
More generally, we can make this notation available on instances of the
<tt>eqType</tt> structure, for types endowed with an effective equality test.
<p>
<div>
</div>
<div><textarea id='coq-ta-28'>

Notation "a == b" := (eq_op _ a b).

Section eqTypeTheory.

Variables (E : eqType) (x y : car E).

Check x == y.

</textarea></div>
<div><p>
</div>
<p>
Instances of a same structure share a <i>theory</i>, i.e., a corpus of results that follow from the axioms of the structure.
<p>
<div>
</div>
<div><textarea id='coq-ta-29'>

Lemma eq_op_refl : x == x.
Proof. apply/eqP. by []. Qed.

End eqTypeTheory.

</textarea></div>
<div><p>
</div>
<p>
Some of these results are about the preservation of the structure.
<p>
<div>
</div>
<div><textarea id='coq-ta-30'>
Section OptioneqType.

Variables (E : eqType).

Definition option_eq (x y : option (car E)) : bool :=
  match x, y with
  |Some u, Some v => eq_op _ u v
  |None, None => true
  |_, _ => false
  end.

Lemma option_eqP : eq_axiom _ option_eq.
Proof.
case=> [a|] [b|]; prove_reflect => //=.
- by move/eqP->.
- case=> ->. apply: eq_op_refl.
Qed.

Definition option_eqType : eqType := EqType _ option_eq option_eqP.

End OptioneqType.

Check option_eqType.

</textarea></div>
<div><p>
</div>
<p>
We can define base case instances of the structure, for instance 
using the lemmas proved in Lesson 4.
<p>
<div>
</div>
<div><textarea id='coq-ta-31'>

Fixpoint eqn m n {struct m} :=
  match m, n with
  | 0, 0 => true
  | S m', S n' => eqn m' n'
  | _, _ => false
  end.

Lemma eqnP : eq_axiom _ eqn.
Proof.
move=> n m; prove_reflect => [|<-]; last by elim n.
by elim: n m => [|n IHn] [|m] //= /IHn->.
Qed.

Definition nat_eqType : eqType := EqType _ _ eqnP.

</textarea></div>
<div><p>
</div>
<p>
But this is not enough.
<p>
<div>
</div>
<div><textarea id='coq-ta-32'>

Fail Check 2 == 3.

</textarea></div>
<div><p>
</div>
<p>
This is a similar problem to the one of inferring positivity proofs,
and it can be solved the same way.
<p>
<div>
</div>
<div><textarea id='coq-ta-33'>

Canonical nat_eqType.

Check 2 == 3.

Fail Check Some 2 == Some 3.

Canonical option_eqType.

Check Some 2 == Some 3.

Goal Some (Some 2) == Some (Some 2).
apply: eq_op_refl.
Qed.

End EqType.
</textarea></div>
<div><p>
</div>
<p>
<p><br/><p>
<p>
<div class="note">(notes)<div class="note-text">
<p>
For more about these hints for unification, and the way they can be
used to implement hierarchies of structures, you might refer to:
<a href="https://hal.inria.fr/hal-00816703v2">this</a> tutorial.
</div></div>
<p>
</div>
<hr/>

</div>
<div><textarea id='coq-ta-34'>
</textarea></div>
<script type="text/javascript">
 var coqdoc_ids = ['coq-ta-1',  'coq-ta-2',  'coq-ta-3',  'coq-ta-4', 
                  'coq-ta-5',  'coq-ta-6',  'coq-ta-7',  'coq-ta-8', 
                  'coq-ta-9',  'coq-ta-10',  'coq-ta-11',  'coq-ta-12', 
                  'coq-ta-13',  'coq-ta-14',  'coq-ta-15',  'coq-ta-16', 
                  'coq-ta-17',  'coq-ta-18',  'coq-ta-19',  'coq-ta-20', 
                  'coq-ta-21',  'coq-ta-22',  'coq-ta-23',  'coq-ta-24', 
                  'coq-ta-25',  'coq-ta-26',  'coq-ta-27',  'coq-ta-28', 
                  'coq-ta-29',  'coq-ta-30',  'coq-ta-31',  'coq-ta-32', 
                  'coq-ta-33',  'coq-ta-34'];
</script>
<hr />

<script type="text/javascript">

  function load_coq_snippets() {
    for (i = 0; i < coqdoc_ids.length; ++i) {
      document.getElementById(coqdoc_ids[i]).nextSibling.CodeMirror.setValue(
        localStorage.getItem('coq-snippet-' + coqdoc_ids[i]));
    }
  }

  function save_coq_snippets() {
    for (i = 0; i < coqdoc_ids.length; ++i) {
      localStorage.setItem('coq-snippet-' + coqdoc_ids[i], document.getElementById(coqdoc_ids[i]).nextSibling.CodeMirror.getValue());
    }
    alert("Coq snippets saved.");
  }

  function download_coq_snippets() {
    var chunks = []
    for (i = 0; i < coqdoc_ids.length; ++i) {
      chunks.push(document.getElementById(coqdoc_ids[i]).nextSibling.CodeMirror.getValue())
    }
    var data = new Blob(chunks, { type: "text/plain;charset=utf-8" });
    saveAs(data, 'source.v');
  }


  alignWithTop = true;
  current = 0;
  slides = [];
  function select_current() {
    for (var i = 0; i < slides.length; i++) {
      var s = document.getElementById('slideno' + i);
      if (i == current) {
        s.setAttribute('class', 'slideno selected');
      } else {
        s.setAttribute('class', 'slideno');
      }
    }
  }

  function mk_tooltip(label, text) {
    var t = document.createElement("div");
    t.setAttribute('class', 'slide-tooltip');
    t.innerHTML = label;

    var s = document.createElement("span");
    s.setAttribute('class', 'slide-tooltiptext slide-tooltip-left');
    s.innerHTML = text;

    t.appendChild(s);
    return t;
  }

  function find_hx(e) {
    for (var i = 0; i < e.children.length; i++) {
      var x = e.children[i];
      if (x.tagName == "H1" ||
        x.tagName == "H2" ||
        x.tagName == "H3" ||
        x.tagName == "H4") return x.textContent;
    }
    return null;
  }

  function init_slides() {
    var toolbar = document.getElementById('document');
    if (toolbar) {
      var tools = document.createElement("div");
      var tprev = document.createElement("div");
      var tnext = document.createElement("div");
      tools.setAttribute('id', 'tools');
      tprev.setAttribute('id', 'prev');
      tprev.setAttribute('onclick', 'prev_slide();');
      tnext.setAttribute('id', 'next');
      tnext.setAttribute('onclick', 'next_slide();');
      toolbar.prepend(tools);
      tools.appendChild(tprev);
      tools.appendChild(tnext);

      slides = document.getElementsByClassName('slide');
      for (var i = 0; i < slides.length; i++) {
        var s = document.createElement("div");
        s.setAttribute('id', 'slideno' + i);
        s.setAttribute('class', 'slideno');
        s.setAttribute('onclick', 'goto_slide(' + i + ');');
        var title = find_hx(slides[i]);
        if (title == null) {
          title = "goto slide " + i;
        }
        var t = mk_tooltip(i, title);
        s.appendChild(t)
        tools.appendChild(s);
      }
      select_current();
    } else {
      //retry later
      setTimeout(init_slides, 100);
    }
  }
  function on_screen(rect) {
    return (
      rect.top >= 0 &&
      rect.top <= (window.innerHeight || document.documentElement.clientHeight)
    );
  }
  function update_scrolled() {
    for (var i = slides.length - 1; i >= 0; i--) {
      var rect = slides[i].getBoundingClientRect();
      if (on_screen(rect)) {
        current = i;
        select_current();
      }
    }
  }
  function goto_slide(n) {
    current = n;
    var element = slides[current];
    console.log(element);
    element.scrollIntoView(alignWithTop);
    select_current();
  }
  function next_slide() {
    current++;
    if (current >= slides.length) { current = slides.length - 1; }
    var element = slides[current];
    console.log(element);
    element.scrollIntoView(alignWithTop);
    select_current();
  }
  function prev_slide() {
    current--;
    if (current < 0) { current = 0; }
    var element = slides[current];
    element.scrollIntoView(alignWithTop);
    select_current();
  }

  window.onload = init_slides;
  window.onbeforeunload = save_coq_snippets;
  window.onscroll = update_scrolled;
</script>

</div> <!-- /#document     -->
</div> <!-- /#code-wrapper -->
</div> <!-- /#ide-wrapper  -->

<script src="./jscoq/ui-js/jscoq-loader.js" type="text/javascript"></script>
<script type="text/javascript">
  var coq;

  loadJsCoq('./jscoq/')
    .then(loadJs("./jscoq/node_modules/codemirror/addon/runmode/runmode"))
    .then(loadJs("./jscoq/node_modules/codemirror/addon/runmode/colorize"))
    .then(function () {
      var coqInline = document.getElementsByClassName("inline-coq");
      CodeMirror.colorize(coqInline);
    })
    .then(function () {
      coq = new CoqManager(coqdoc_ids,
        { base_path: './jscoq/',
          init_pkgs: ['init'],
          all_pkgs: ['init','math-comp']
         }
      );
    });
</script>
</body>

</html>