To play this document inside your browser use ALT-N and ALT-P. If you get stack overflow errors, try to use Google Chrome or Chromium with the command line option --js-flags="--harmony-tailcalls".

You can save your edits inside your browser and load them back (edits are also saved when you close the window). Finally you can download the file for offline editing.


We start by loading a few libraries

Basics: data structures and logic

We open a name space to make experiments.

Type bool and its inhabitants:

Definition by pattern-matching:

What you see is what you get:

Computation:

Proof by computation, using the conversion rule:

Proof by case analysis:

Case analysis justification:

Type nat and its inhabitants:

Constructors feature notations 0 and _.+1.

Definition by pattern-matching:

Proof by computation:

Definition by recurrence:

Proof by computation:

Proof by recurrence:

Definition by recurrence:

What is the difference between (eqn k l) and (k = l) ?

Inference of implicit information

Here is a type of polymorphic lists:

As such there is a verbose duplication of parameters:

Avoid over-specification of the theorems to be applied:

We can define types which pairs a data type with a specification:

We can use unification to infer the assumptions:

Oracles

Sorry, the demo is not available in your browser.

Reflection based tactics

Correctness relies on the assumptions on op2 and z and u:

This is the way the ring tactic is implemented.

End

Sorry, the end of the demo is not available in your browser.