Skip to content
Snippets Groups Projects
index.html 10.8 KiB
Newer Older
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml">
  <head>
    <title>jsCoq – Use Coq in Your Browser</title>
    <meta http-equiv="content-type" content="text/html;charset=utf-8" />
    <meta name="description" content="An Online IDE for the Coq Theorem Prover" />
    <!-- Move to copy with the bundle -->
    <link rel="icon" href="frontend/classic/images/favicon.png">
    <style>body { visibility: hidden; } /* FOUC avoidance */</style>
    <link rel="stylesheet" type="text/css" href="./dist/frontend/index.css">
<body class="jscoq-main">
  <div id="ide-wrapper" class="toggled">
  <div id="code-wrapper">
  <div id="document-wrapper">
    <!------------------------------->
    <!--   N A V   B A R           -->
    <!------------------------------->
    <nav class="navbar sticky-top navbar-expand-lg navbar-light bg-light">
      <div class="container-fluid">
        <a class="navbar-brand"><img src="frontend/classic/images/favicon.png"></a>
        <button class="navbar-toggler" type="button" data-bs-toggle="collapse" data-bs-target="#navbarSupportedContent" aria-controls="navbarSupportedContent" aria-expanded="false" aria-label="Toggle navigation">
          <span class="navbar-toggler-icon"></span>
        </button>
        <div class="collapse navbar-collapse" id="navbarSupportedContent">
          <ul class="navbar-nav me-auto mb-2 mb-lg-0">
            <li class="nav-item dropdown">
              <a class="nav-link dropdown-toggle" id="navbarAbout" role="button" data-bs-toggle="dropdown" aria-expanded="false">
                About
              </a>
              <ul class="dropdown-menu" aria-labelledby="navbarDropdown">
                <li><a class="dropdown-item" href="#team">jsCoq Dev Team</a></li>
                <li><hr class="dropdown-divider"></li>
                <li><a class="dropdown-item" href="https://coq.inria.fr">Coq Proof Assistant</a></li>
                <li><a class="dropdown-item" href="https://github.com/cpitclaudel/company-coq">company-coq</a></li>
              </ul>
            </li>
            <li class="nav-item dropdown">
              <a class="nav-link dropdown-toggle" id="navbarExamples" role="button" data-bs-toggle="dropdown" aria-expanded="false">
                Examples
              </a>
              <ul class="dropdown-menu" aria-labelledby="navbarDropdown">
                <li><a class="dropdown-item" href="examples/inf-primes.html">Infinitude of Primes</a></li>
                <li><a class="dropdown-item" href="examples/sqrt_2.html">Irrationality of <span class="math"><img class="symbol-sqrt" src="frontend/classic/images/sqrt.svg">2</span></a></li>
                <!-- these are only available from the full website -->
                <li><a class="dropdown-item" href="/fun/coqoban.html">🎡 Çoqoban</a></li>
                <li><hr class="dropdown-divider"></li>
                <li><a class="dropdown-item" href="/ext/sf"><img class="symbol-book" src="frontend/classic/images/book.svg">Software Foundations</a></li>
              </ul>
            </li>
          </ul>
        </div>
      </div>
Shachar Itzhaky's avatar
Shachar Itzhaky committed
      <a id="scratchpad" href="examples/scratchpad.html" title="Open scratchpad">
        <span class="newcomer scratchpad-tip">open the scratchpad<br/>to start editing</span>
      </a>
    </nav>
    <!------------------------------->
  
  <div id="document">
  <div>
    <h3>Welcome to the <span class="jscoq-name">jsCoq</span> Interactive Online System!</h3>
      <span class="jscoq-name">jsCoq</span> is an interactive,
      web-based environment for the Coq Theorem prover, and is a collaborative
      development effort. See the <a href="#team">list of contributors</a>
      below.
      <span class="jscoq-name">jsCoq</span> is open source. If you find any problem
      that you wish to report or want to add your own contribution,
      you are extremely welcome! We await your feedback at
      <a href="https://github.com/jscoq/jscoq">GitHub</a>
      and <a href="https://coq.zulipchat.com/#narrow/stream/256336-jsCoq">Zulip</a>.
    <h4>A First Example: <code>rev</code> <code></code> <code>rev = id</code></h4>
      The following is a simple proof that <code>rev</code>, the standard list
      reversal function as commonly defined in ML and other languages of the
      family, is an involution.
Shachar Itzhaky's avatar
Shachar Itzhaky committed
      Use <span class="has-kbd"><kbd>Alt</kbd>+<kbd></kbd>/<kbd></kbd></span> to step through the proof,
      and observe the proof state on the right panel.
    <textarea class="snippet">
From Coq Require Import List.
Import ListNotations.</textarea>
    <p class="interim">
      We are going to need a simpler auxiliary lemma, one that connects
      <code>rev</code>, <code>::</code> (the list constructor, also known
      as <code>cons</code>), and <code>snoc</code> (the dual of
      <code>cons</code>, a function that appends an element at the end of
      a list).
      This is because the latter two participate in the definition of
      the former, <code>rev</code>.
    <textarea class="snippet">Lemma rev_snoc_cons A :
  forall (x : A) (l : list A), rev (l ++ [x]) = x :: rev l.</textarea>
    <p class="interim">
      This proposition is proven by way of the standard induction on
      the structure of the list <code>l</code>.
    <textarea class="snippet">Proof.
  induction l.
  - reflexivity.
  - simpl. rewrite IHl. simpl. reflexivity.
Qed.</textarea>
      Now we prove the central equality with a similar induction.
    <textarea class="snippet">Theorem rev_rev A : forall (l : list A), rev (rev l) = l.
Proof.
  induction l.
  - reflexivity.
  - simpl. rewrite rev_snoc_cons. rewrite IHl.
    reflexivity.
Qed.</textarea>
      Finally, we apply functional extensionality to produce the equality
      as it was written in the title.
    <p class="interim">
      There is only one syntactic difference, which is that, in Coq, we
      need to pass an explicit value to the implicit (generic) type
      parameter <code>A</code> of <code>rev</code>.
    </p>
    <textarea class="snippet">From Coq.Program Require Import Basics.
From Coq Require Import FunctionalExtensionality.
Open Scope program_scope.
Theorem rev_invol A : rev (A:=A) ∘ rev (A:=A) = id.
Proof.
  apply functional_extensionality.
  intro x.
  unfold compose, id. rewrite rev_rev.
  reflexivity.
    <hr/> <!-- end of proof -->

    <h4>Quick start</h4>
Shachar Itzhaky's avatar
Shachar Itzhaky committed
      Use the <a href="examples/scratchpad.html">scratchpad <span class="scratchpad-small"></span></a>
      for a fresh page to write your proofs on.
      <span class="jscoq-name">jsCoq</span> provides basic UI for running
      and inspecting proofs, similar to IDEs such as <a href="https://coq.inria.fr/refman/practical-tools/coqide.html">CoqIDE</a>,
      <a href="https://proofgeneral.github.io/">Proof General</a>,
      and <a href="https://github.com/coq-community/vscoq">VSCoq</a>.
    <table class="doc-actions">
      <tr><th>Button</th><th>Key binding</th><th>Action</th></tr>
        <td><img src="frontend/classic/images/power-button-512-black.png" height="20px"></td>
Shachar Itzhaky's avatar
Shachar Itzhaky committed
        <td class="has-kbd"><kbd>F8</kbd></td>
        <td>Toggles the goal panel.</td>
      </tr>
        <td><img src="frontend/classic/images/down.png" height="15px"><img src="frontend/classic/images/up.png" height="15px"></td>
Shachar Itzhaky's avatar
Shachar Itzhaky committed
        <td class="has-kbd">
          <kbd>Alt</kbd>+<kbd></kbd>/<kbd></kbd> or<br/>
          <kbd>Alt</kbd>+<kbd>N</kbd>/<kbd>P</kbd>
        </td>
        <td>Move through the proof.</td>
      </tr>
      <tr>
        <td><img src="frontend/classic/images/to-cursor.png" height="20px"></td>
Shachar Itzhaky's avatar
Shachar Itzhaky committed
        <td class="has-kbd">
          <kbd>Alt</kbd>+<kbd>Enter</kbd> or<br/> <kbd>Ctrl</kbd>+<kbd>Enter</kbd><br/>
          (⌘ on Mac)
        </td>
        <td>Run (or go back) to the current point.</td>
      </tr>
      <tr>
Shachar Itzhaky's avatar
Shachar Itzhaky committed
        <td class="has-kbd">
          <kbd>Ctrl</kbd>+<img class="symbol-mouse" src="frontend/classic/images/pointer.svg">
        </td>
        <td>Hover executed statements to peek at the proof state after each step.</td>
    <h5>Creating your own proof scripts</h5>
      The <a href="examples/scratchpad.html">scratchpad</a> offers simple, local
      storage functionality. It also allows you to share your development with
      other users in a manner that is similar to Pastebin.
      See the <a href="https://github.com/jscoq/jscoq/tree/v8.17/docs">official docs</a>
      on GitHub for more details on using, building, embedding, and integrating
      <span class="jscoq-name">jsCoq</span> in your developments.
    </p>
      <span class="jscoq-name">jsCoq</span> comes with a variety of addon packages,
      including Coq's standard library and the
      <a href="https://math-comp.github.io">mathematical components</a>
      library.
      Feel free to experiment, and let us know if you have any suggestions
      and/or when you have done something cool with <span class="jscoq-name">jsCoq</span>.
      😎
  </p>
  </div> <!-- /#panel body -->
  <div id="team">
    <a name="team"></a>
      <p><i>The dev team</i></p>
    <ul>
      <li>
        <a href="https://www.irif.fr/~gallego/">Emilio Jesús Gallego Arias</a>
        (<a href="https://www.inria.fr">Inria</a>,
         <a href="https://u-paris.fr">Université de Paris</a>,
         <a href="https://www.irif.fr">IRIF</a>)
      </li>
      <li>
        <a href="https://www.cs.technion.ac.il/~shachari/">Shachar Itzhaky</a>
        (<a href="https://cs.technion.ac.il">Technion</a>)
      </li>
    </ul>
    <p><i>Contributors</i></p>
    <ul>
      <li>
        Benoît Pin
        (<a href="https://www.cri.ensmp.fr/">CRI</a>,
         <a href="http://www.mines-paristech.eu">MINES ParisTech</a>)
      </li>
    </ul>
  </div>
  </div> <!-- /#document -->
  </div> <!-- /#document-wrapper -->
  </div> <!-- /#code-wrapper -->
  </div> <!-- /#ide-wrapper -->

    import { JsCoq } from './jscoq.js';
    var sp = new URLSearchParams(location.search);

Shachar Itzhaky's avatar
Shachar Itzhaky committed
    if (!localStorage['scratchpad.last_filename'])
        setTimeout(() => document.body.classList.add('welcome'), 1500);
    var jscoq_ids  = ['.snippet'];
    var jscoq_opts = {
        backend:   sp.get('backend'),
        focus: false,
        editor: { mode: { 'company-coq': true } },
        all_pkgs: ['coq', 'mathcomp', 'equations', 'elpi',
                   'quickchick', 'software-foundations',
                   'hahn', 'paco', 'snu-sflib',
                   'fcsl-pcm', 'htt', 'pnp', 'stdpp', 'iris']
    JsCoq.start(jscoq_ids, jscoq_opts).then(res => {
        /* Global reference */
        window.coq = res;
  </script>
</body>