lesson2.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 Import mini_ssreflect.

(* ignore these directives *)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Add Printing Coercion is_true.
Notation "x '= true'" := (is_true x) (x at level 100, at level 0, only printing).
Remove Printing If bool.

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

<div class="slide vfill">
<p>
<h2>
 Programs, Specifications and Proofs
</h2>

<p>
<h3>
 In this lecture, first steps on:
</h3>

<p>
<ul class="doclist">
  <li> writing programs & specifications
<ul class="doclist">
    <li> functions

    </li>
  <li> simple data

  </li>
  <li> containers

  </li>
  <li> symbolic computations

  </li>
  <li> higher order functions and mathematical notations

  </li>
  </ul>
  
  </li>
<li> writing proofs
<ul class="doclist">
  <li> proofs by computation

  </li>
<li> proofs by case split

</li>
<li> proofs by rewriting

</li>
</ul>

</li>
</ul>
<h3>
 Extra material:
</h3>

<p>
<ul class="doclist">
  <li> <a href="cheat_sheet.html">Coq cheat sheet</a> (during ex session)

  </li>
<li> <a href="https://math-comp.github.io/mcb/">Mathematical Components</a>
  chapters one and two (at home)

</li>
</ul>
<h3>
 Disclaimer:
</h3>

<p>
<ul class="doclist">
  <li> I'm a computer scientist, I speak weird ;-)

  </li>
<li> don't be afraid, raise your hand and I'll do my best to explain my lingo.

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

<div class="slide">
<h2>
 Functions
</h2>

<p>
Functions are written using the <tt>fun .. => ..</tt> syntax. Down below we write
the function:
<p>
$$ n \mapsto 1 + n $$
<p>
The command <tt>Check</tt> verifies that a term is well typed.
The precise meaning will be given tomorrow morning, for now think about
it as a well formed element of some set.
<p>
<div>
</div>
<div><textarea id='coq-ta-2'>
Check (fun n : nat => 1 + n).
</textarea></div>
<div><p>
</div>
<p>
Coq answers by annotating the term with its type (the <tt>-></tt> denotes the function
space):
<p>
$$ \mathbb{N} \to \mathbb{N} $$
<p>
Function application is written by writing the function
on the left of the argument (eg, not as in the mathematical
practice).
<p>
<div>
</div>
<div><textarea id='coq-ta-3'>
Check 2.
Check (fun n : nat => 1 + n) 2.
</textarea></div>
<div><p>
</div>
<p>
Terms (hence functions) can be given a name using
the <tt>Definition</tt> command. The command offers some
syntactic sugar for binding the function arguments.
<p>
<div>
</div>
<div><textarea id='coq-ta-4'>
Definition f : nat -> nat := (fun n : nat => 1 + n).
(* Definition f (n : nat) : nat := 1 + n. *)
</textarea></div>
<div><p>
</div>
<p>
Named terms can be printed.
<p>
<div>
</div>
<div><textarea id='coq-ta-5'>
Print f.
</textarea></div>
<div><p>
</div>
<p>
Coq is able to compute with terms, in particular
one can obtain the normal form via the <tt>Eval lazy in</tt>
command.
<p>
<div>
</div>
<div><textarea id='coq-ta-6'>
Eval lazy in f 2.
</textarea></div>
<div><p>
</div>
<p>
Notice that <quote>computation</quote> is made of many steps.
In particular <tt>f</tt> has to be unfolded (delta step)
and then the variable substituted for the argument
(beta).
<p>
<div>
</div>
<div><textarea id='coq-ta-7'>
Eval lazy delta[f] in f 2.
Eval lazy delta[f] beta in f 2.
</textarea></div>
<div><p>
</div>
<p>
Nothing but functions (and their types) are built-in in Coq.
All the rest is defined, even <tt>1</tt>, <tt>2</tt> and <tt>+</tt> are not primitive.
<p>
<p><br/><p>
<p>
<div class="note">(notes)<div class="note-text">
<p>
This slide corresponds to
section 1.1 of
<a href="https://math-comp.github.io/mcb/">the Mathematical Components book</a>
</div></div>
<p>
</div>
<hr/>

<div class="slide">
<h2>
 Data types
</h2>

<p>
Data types can be declared using the <tt>Inductive</tt> command.
<p>
Many of them are already available in the Coq library called
<tt>Prelude</tt> that is automatically loaded. We hence just print
them.
<p>
<tt>Inductive bool := true | false.</tt>
<p>
<div>
</div>
<div><textarea id='coq-ta-8'>
Print bool.
</textarea></div>
<div><p>
</div>
<p>
This command declares a new type <tt>bool</tt> and declares
how the terms of this type are built.
Only <tt>true</tt> and <tt>false</tt> are *canonical* inhabitants of
<tt>bool</tt> and they are called *constructors*.
<p>
Remark: a data type declaration prescribes the shape of values, not
which operations are available nor their properties.
We are going to use programs (functions) to describe the operations
on a data type.
<p>
Coq provides one very primitive operation that works on data types.
This operation lets you take a decision based on the canonical shape
of the data. It is written <tt>match x with true => ... | false => .. end</tt>.
<p>
<div>
</div>
<div><textarea id='coq-ta-9'>
Definition twoVtree (b : bool) : nat :=
  match b with
  | true => 2
  | false => 3
  end.

Eval lazy in twoVtree true.
Eval lazy delta in twoVtree true.
Eval lazy delta beta in twoVtree true.
Eval lazy delta beta iota in twoVtree true.
</textarea></div>
<div><p>
</div>
<p>
We define a few boolean operators that will come in handy
later on.
<p>
<div>
</div>
<div><textarea id='coq-ta-10'>
Definition andb (b1 : bool) (b2 : bool) : bool :=
  match b1 with true => b2   | false => false end.

Definition orb (b1 :bool) (b2 : bool) : bool :=
  match b1 with true => true | false => b2    end.

Infix "&&" := andb.
Infix "||" := orb.

Check true && false || false.
</textarea></div>
<div><p>
</div>
<p>
The <tt>Infix</tt> command lets one declare infix notations.
Precendence and associativity is already declared in the
prelude of Coq, here we just associate the constants
<tt>andb</tt> and <tt>orb</tt> to these notataions.
<p>
Natural numbers are defined similarly to booleans:
<p>
<tt>Inductive nat := O | S (n : nat).</tt>
<p>
Remark that the declaration is recursive.
<p>
<div>
</div>
<div><textarea id='coq-ta-11'>
Print nat.
</textarea></div>
<div><p>
</div>
<p>
Remark:
<p>
Coq provides a special notation for literals, eg <tt>3</tt>,
that is just sugar for <tt>S (S (S O))</tt>.
<p>
<div>
</div>
<div><textarea id='coq-ta-12'>
Check 3.
</textarea></div>
<div><p>
</div>
<p>
Now let's define a simple operation on natural numbers.
<p>
As for booleans, Coq provides a primitie operation to
make decisions based on the canonical values.
<p>
<div>
</div>
<div><textarea id='coq-ta-13'>
Definition pred (n : nat) : nat :=
  match n with 0 => 0 | S p => p end.

Eval lazy in pred 7.
</textarea></div>
<div><p>
</div>
<p>
Remark that <tt>p</tt> is a binder. When the <tt>match..with..end</tt>
is evaluated, and <tt>n</tt> put in normal form, then if it
is <tt>S t</tt> the variable <tt>p</tt> takes <tt>t</tt> and the second
is taken.
<p>
Since the data type of natural number is recursive Coq provides
another primitive operation called <tt>Fixpoint</tt>.
<p>
<div>
</div>
<div><textarea id='coq-ta-14'>
Fixpoint addn (n : nat) (m : nat) : nat :=
  match n with
  | 0 => m
  | S p => S (addn p m)
  end.
Infix "+" := addn.
Eval lazy in 3 + 2.
</textarea></div>
<div><p>
</div>
<p>
Let's now write the equality test for natural numbers
<p>
<div>
</div>
<div><textarea id='coq-ta-15'>
Fixpoint eqn (n : nat) (m : nat) : bool :=
  match n, m with
  | 0, 0 => true
  | S p, S q => eqn p q
  | _, _ => false
  end.
Infix "==" := eqn : bool_scope.
Eval lazy in 3 == 4.
</textarea></div>
<div><p>
</div>
<p>
Other examples are subtraction and order
<p>
<div>
</div>
<div><textarea id='coq-ta-16'>
Fixpoint subn (m : nat) (n : nat) : nat :=
  match m, n with
  | S p, S q => subn p q
  | _ , _ => m
  end.

Infix "-" := subn.

Eval lazy in 3 - 2.
Eval lazy in 2 - 3. (* truncated *)

Definition leq m n := m - n == 0.

Infix "<=" := leq.

Eval lazy in 4 <= 5.
</textarea></div>
<div><p>
</div>
<p>
<p><br/><p>
<p>
<div class="note">(notes)<div class="note-text">
<p>
This slide corresponds to
section 1.2 of
<a href="https://math-comp.github.io/mcb/">the Mathematical Components book</a>
</div></div>
<p>
</div>
<p>
</div>
<hr/>

<div class="slide">
<h2>
 Containers
</h2>

<p>
Containers let one aggregate data, for example to form a
pair or a list.  The interesting characteristic of containers
is that they are polymorphic: the same container can be used
to hold terms of many types.
<p>
<pre class="inline-coq" data-lang="coq">
Inductive list (A : Type) := nil | cons (hd : A) (tl : list A).<p>
</pre>
<div>
</div>
<div><textarea id='coq-ta-17'>
Check cons 1 nil.
Check [:: 3; 4; 5 ].
</textarea></div>
<div><p>
</div>
<p>
The notation <tt>[:: .. ; .. ]</tt> can be used to form list
by separating the elements with <tt>;</tt>. When there are no elements
what is left is <tt>[::]</tt> that is the empty list.
<p>
And of course we can use list with other data types
<p>
<div>
</div>
<div><textarea id='coq-ta-18'>
Check [:: 3; 4; 5 ].
Check [:: true; false; true ].
</textarea></div>
<div><p>
</div>
<p>
Let's now define the <tt>size</tt> function.
<p>
<div>
</div>
<div><textarea id='coq-ta-19'>
Fixpoint size A (s : list A) : nat :=
  match s with
  | cons _ tl => S (size tl)
  | nil => 0
  end.

Eval lazy in size [:: 1; 8; 34].
Eval lazy in size [:: true; false; false].

</textarea></div>
<div><p>
</div>
<p>
Given that the contents of containers are of an
arbitrary type many common operations are parametrized
by functions that are specific to the type of the
contents.
<p>
<pre class="inline-coq" data-lang="coq">
Fixpoint map A B (f : A -> B) (s : list A) : list B :=
  match s with cons e tl => cons (f e) map f tl | nil => nil end.<p>
</pre>
<div>
</div>
<div><textarea id='coq-ta-20'>
Definition l := [:: 1; 2; 3].
Check  map (fun x => S x) l.
Eval lazy in map (fun x => S x) l.
</textarea></div>
<div><p>
</div>
<p>
The <a href="http://math-comp.github.io/math-comp/htmldoc/mathcomp.ssreflect.seq.html">seq</a>
library of Mathematical Components contains many combinators. Their syntax
is documented in the header of the file.
<p>
<p><br/><p>
<p>
<div class="note">(notes)<div class="note-text">
<p>
This slide corresponds to
section 1.3 of
<a href="https://math-comp.github.io/mcb/">the Mathematical Components book</a>
</div></div>
<p>
</div>
<hr/>

<div class="slide">
<h2>
 Symbols
</h2>

<p>
The section mecanism is used to describe a context under
which definitions are made. Coq lets us not only define
terms, but also compute with them in that context.
<p>
We use this mecanism to talk about symbolic computation.
<p>
<div>
</div>
<div><textarea id='coq-ta-21'>
Section symbols.
Variables x : nat.

Eval lazy in pred (S x).
Eval lazy in pred x .
</textarea></div>
<div><p>
</div>
<p>
Computation can take place in presence of variables
as long as constructors can be consumed. When no
more constructors are available computation is
stuck.
<p>
Let's not look at a very common higher order
function.
<p>
<div>
</div>
<div><textarea id='coq-ta-22'>

Fixpoint foldr A T (f : T -> A -> A) (a : A) (s : list T) :=
  match s with
  | cons x xs => f x (foldr f a xs)
  | nil => a
  end.
</textarea></div>
<div><p>
</div>
<p>
The best way to understand what <tt>foldr</tt> does 
is to postulate a variable <tt>f</tt> and compute. 
<p>
<div>
</div>
<div><textarea id='coq-ta-23'>

Variable f : nat -> nat -> nat.

Eval lazy in foldr f    3 [:: 1; 2 ].

</textarea></div>
<div><p>
</div>
<p>
If we plug <tt>addn</tt> in place of <tt>f</tt> we
obtain a term that evaluates to a number.
<p>
<div>
</div>
<div><textarea id='coq-ta-24'>

Eval lazy in foldr addn 3 [:: 1; 2 ].

End symbols.

</textarea></div>
<div><p>
</div>
<p>
<div class="note">(notes)<div class="note-text">
<p>
This slide corresponds to
sections 1.4 and 1.5 of
<a href="https://math-comp.github.io/mcb/">the Mathematical Components book</a>
</div></div>
<p>
</div>
<hr/>

<div class="slide">
<h2>
 Higher order functions and mathematical notations
</h2>

<p>
Let's try to write this formula in Coq
<p>
$$ \sum_{i=1}^n (i * 2 - 1) = n ^ 2 $$
<p>
We need a bit of infrastructure
<p>
<div>
</div>
<div><textarea id='coq-ta-25'>
Fixpoint iota (m : nat) (n : nat) : list nat :=
  match n with
  | 0 => nil
  | S u => cons m (iota (S m) u)
  end.

Eval lazy in iota 0 5.

</textarea></div>
<div><p>
</div>
<p>
Combining <tt>iota</tt> and <tt>foldr</tt> we can get pretty
close to the LaTeX source for the formula above.
<p>
<div>
</div>
<div><textarea id='coq-ta-26'>

Notation "\sum_ ( m <= i < n ) F" :=
  (foldr (fun i a => F + a) 0 (iota m (n-m)))
  (at level 41, m, n, i at level 50, F at level 41).

Check \sum_(1 <= x < 5) (x * 2 - 1).
Eval lazy in \sum_(1 <= x < 5) (x * 2 - 1).
</textarea></div>
<div><p>
</div>
<p>
<p><br/><p>
<p>
<div class="note">(notes)<div class="note-text">
<p>
This slide corresponds to
section 1.6 of
<a href="https://math-comp.github.io/mcb/">the Mathematical Components book</a>
</div></div>
<p>
</div>
<hr/>

<div class="slide">
<h2>
 Formal statements
</h2>

<p>
Most of the statements that we consider in Mathematical
Components are equalities.
<p>
It is not surprising one can equate two numbers.
<p>
<div>
</div>
<div><textarea id='coq-ta-27'>
Lemma addnA (m n k : nat) : m + (n + k) = m + n + k.
Abort.
</textarea></div>
<div><p>
</div>
<p>
Remark: to save space, variables of the same type can be
writte <tt>(a b c : type)</tt> instead of <tt>(a : type) (b : type) ...</tt>.
<p>
We have defined many boolean tests that can
play the role of predicates.
<p>
<div>
</div>
<div><textarea id='coq-ta-28'>
Check 0 <= 4. (* not a statement *)
Check (0 <= 4) = true. (* a statement we can prove *)
</textarea></div>
<div><p>
</div>
<p>
More statements using equality and predicates in bool
<p>
<div>
</div>
<div><textarea id='coq-ta-29'>
Lemma eqn_leq (m n : nat) : (m == n) = (m <= n) && (n <= m).
Abort.

Lemma leq0n (n : nat) : 0 <= n.
Abort.
</textarea></div>
<div><p>
</div>
<p>
Remark: in the first statement <tt>=</tt> really means
<quote>if and only if</quote>.
<p>
Remark: Coq adds <tt>= true</tt> automatically when we state a lemma.
<p>
<div>
</div>
<div><textarea id='coq-ta-30'>
Check is_true.
</textarea></div>
<div><p>
</div>
<p>
<p><br/><p>
<p>
<div class="note">(notes)<div class="note-text">
This slide corresponds to
section 2.1 of
<a href="https://math-comp.github.io/mcb/">the Mathematical Components book</a>
</div></div>
<p>
<p><br/><p>
</div>
<hr/>

<div class="slide">
<h2>
 Proofs by computation
</h2>

<p>
Our statements are made of programs. Hence they compute!
<p>
The <tt>by[]</tt> proof command solves trivial goals (mostly) by
computation.
<p>
<pre class="inline-coq" data-lang="coq">
Fixpoint addn n m :=
  match n with 0 => m | S p => S (addn p m) end.<p>
</pre><pre class="inline-coq" data-lang="coq">
Fixpoint subn m n : nat :=
  match m, n with
  | S p, S q => subn p q
  | _ , _ => m
  end.<p>
</pre><pre class="inline-coq" data-lang="coq">
Fixpoint eqn (n : nat) (m : nat) : bool :=
  match n, m with
  | 0, 0 => true
  | S p, S q => eqn p q
  | _, _ => false
  end.<p>
</pre><pre class="inline-coq" data-lang="coq">
Definition leq m n := m - n == 0.<p>
</pre>
<div>
</div>
<div><textarea id='coq-ta-31'>
Lemma addSn m n : S m + n = S (m + n).
Proof. by []. Qed.

Lemma leq0n n : 0 <= n.
Proof. by []. Qed.

Lemma ltn0 n : S n <= 0 = false.
Proof. by []. Qed.

Lemma ltnS m n : (S m <= S n) = (m <= n).
Proof. by []. Qed.
</textarea></div>
<div><p>
</div>
<p>
Let's look around.
<p>
<tt>Locate</tt> looks for a symbol to find the name behing id.
<p>
<div>
</div>
<div><textarea id='coq-ta-32'>

Locate "~~".
Print negb.

Lemma negbK (b : bool) : ~~ (~~ b) = b.
Proof. Fail by []. Abort.
</textarea></div>
<div><p>
</div>
<p>
It is not always the case the computation solves all our
problems. In particular here there are no constructors to
consume, hence computation is stuck.
<p>
To prove <tt>negbK</tt> we need a case split.
<p>
<p><br/><p>
<p>
<div class="note">(notes)<div class="note-text">
This slide corresponds to
section 2.2.1 of
<a href="https://math-comp.github.io/mcb/">the Mathematical Components book</a>
</div></div>
<p>
<p><br/><p>
</div>
<hr/>

<div class="slide">
<h2>
 Proofs by case analysis
</h2>

<p>
The proof of <tt>negbK</tt> requires a case analysis: given that
<tt>b</tt> is of type bool, it can only be <tt>true</tt> or <tt>false</tt>.
<p>
The <tt>case: term</tt> command performs this proof step.
<p>
<div>
</div>
<div><textarea id='coq-ta-33'>
Lemma negbK (b : bool) : ~~ (~~ b) = b.
Proof.
case: b.
  by [].
by [].
Qed.

Lemma andbC (b1 b2 : bool) : b1 && b2 = b2 && b1.
Proof.
by case: b1; case: b2.
Qed.

Lemma orbN b : b || ~~ b.
Proof.
by case: b.
Qed.

</textarea></div>
<div><p>
</div>
<p>
The constructors of <tt>bool</tt> have no arguments, but for
example the second constructor of <tt>nat</tt> has one.
<p>
In this case one has to complement the command by supplying
names for these arguments.
<p>
<div>
</div>
<div><textarea id='coq-ta-34'>
Lemma leqn0 (n : nat) : (n <= 0) = (n == 0).
Proof.
case: n => [| p].
  by [].
by [].
Qed.
</textarea></div>
<div><p>
</div>
<p>
Sometimes case analysis is not enough.
<p>
<pre class="inline-coq" data-lang="coq">
Fixpoint muln (m n : nat) : nat :=
  match m with 0 => 0 | S p => n + muln p n end.<p>
</pre>
<div>
</div>
<div><textarea id='coq-ta-35'>
Lemma muln_eq0 (m n : nat) :
  (m * n == 0) = (m == 0) || (n == 0).
Proof.
case: m => [|p].
  by [].
case: n => [|k]; last first. (* rotates the goals *)
  by [].
Abort.
</textarea></div>
<div><p>
</div>
<p>
We don't know how to prove this yet.
But maybe someone proved it already...
<p>
<div>
</div>
<div><textarea id='coq-ta-36'>
Search _ (_ * 0) in MC.
</textarea></div>
<div><p>
</div>
<p>
The <tt>Search</tt> command is quite primitive but also
your best friend.
<p>
It takes a head pattern, the whildcard <tt>_</tt>
in the examples above, followed by term or patterns.
<p>
You must always use <tt>in MC</tt> in order to limit the search space
to the set of lemmas relevant to these lectures.
<p>
<div class="note">(notes)<div class="note-text">
This slide corresponds to
sections 2.2.2 and 2.5 of
<a href="https://math-comp.github.io/mcb/">the Mathematical Components book</a>
</div></div>
<p>
<p><br/><p>
</div>
<hr/>

<div class="slide">
<h2>
 Proofs by rewriting
</h2>

<p>
The <tt>rewrite</tt> tactic uses an equation. If offers many
more flags than the ones we will see (hint: check the
Coq user manual, SSReflect chapter).
<p>
<div>
</div>
<div><textarea id='coq-ta-37'>
Lemma muln_eq0 (m n : nat) :
  (m * n == 0) = (m == 0) || (n == 0).
Proof.
case: m => [ // |p].
case: n => [ |k //].
rewrite muln0.
by [].
Qed.
</textarea></div>
<div><p>
</div>
<p>
Let's now look at another example to learn more
about <tt>rewrite</tt>.
<p>
<div>
</div>
<div><textarea id='coq-ta-38'>
Lemma leq_mul2l (m n1 n2 : nat) :
  (m * n1 <= m * n2) = (m == 0) || (n1 <= n2).
Proof.
rewrite /leq.
(* Search _ (_ * (_ - _)) in MC. *)
rewrite -mulnBr.
rewrite muln_eq0.
by [].
Qed.
</textarea></div>
<div><p>
</div>
<p>
<div class="note">(notes)<div class="note-text">
This slide corresponds to
section 2.2.3 of
<a href="https://math-comp.github.io/mcb/">the Mathematical Components book</a>
</div></div>
<p>
<p><br/><p>
</div>
<p>
<div class="slide">
<h2>
 Lesson 1: sum up
</h2>

<p>
<h3>
 Programs and specifications
</h3>

<p>
<ul class="doclist">
  <li> <tt>fun .. => ..</tt>

  </li>
<li> <tt>Check</tt>

</li>
<li> <tt>Definition</tt>

</li>
<li> <tt>Print</tt>

</li>
<li> <tt>Eval lazy</tt>

</li>
<li> <tt>Indcutive</tt> declarations <tt>bool</tt>, <tt>nat</tt>, <tt>seq</tt>.

</li>
<li> <tt>match .. with .. end</tt> and <tt>if .. is .. then .. else ..</tt>

</li>
<li> <tt>Fixpoint</tt>

</li>
<li> <tt>andb</tt> <tt>orb</tt> <tt>eqn</tt> <tt>leq</tt> <tt>addn</tt> <tt>subn</tt> <tt>size</tt> <tt>foldr</tt>

</li>
</ul>
<h3>
 Proofs
</h3>

<p>
<ul class="doclist">
  <li> <tt>expr = true</tt> or <tt>expr = expr</tt> is a specification

  </li>
<li> <tt>by []</tt> trivial proofs (including computation)

</li>
<li> <tt>case: m => [//|p]</tt> case split

</li>
<li> <tt>rewrite t1 /t2</tt> rewrite

</li>
</ul>
</div>
<p>
</div>
<div><textarea id='coq-ta-39'>
</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',  'coq-ta-35',  'coq-ta-36', 
                  'coq-ta-37',  'coq-ta-38',  'coq-ta-39'];
</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>