A d∃∀duction session starts with the choice of a Lean file that contains the content of a "course". A course is essentially a structured list of Lean lemmas that are tagged as exercises, definitions and theorems. This Lean file is annotated with comments inside docstrings that starts with /- dEAduction. Statements and their annotations will be parsed by d∃∀duction to retrieve all the pertinent pieces of information.

Format description

The following rules are a mixture of rigid rules and good practice. See this page for comprehensive lists of keywords for metadata. Note that it is advised to add metadata for a better user experience, but this is not compulsory, so that designing a first draw of a course should be quite fast.

Namespaces

• The course is structured according to namespaces. Namespaces must be announced by the namespaceLean keywords starting a new line. They can be followed by an annotation giving a pretty name for the namespace, e.g.:

namespace set_theory -- Course title
/- dEAduction
PrettyName
    Set Theory
-/
namespace unions_and_intersections -- section 1
-- no docstring: pretty name is not provided in the Lean file, and d∃∀duction will compute a pretty name from the Lean name
-- essentially by removing underscores

namespace complements -- section 2
/- dEAduction
PrettyName
    Complémentaires
-/

Statements

d∃∀duction distinguishes three kinds of statements: definitions, theorems and exercises. They are all introduced by the Lean keyword lemma.

• Definitions are given in the form of an iff statement, and named using the definition namespace, i.e. they must be on a line that starts with lemma definition.. They can be given a pretty name as for namespace, e.g.:

lemma definition.intersection_deux  (A B : set X) (x : X) :  x ∈ A ∩ B ↔ ( x ∈ A ∧ x ∈ B) := 
/- dEAduction
PrettyName
    Intersection de deux ensembles
-/
begin
    iff.rfl
end

Note that the metadata must be immediately after the :=operator, before the begin / end section that may contain the proof.

• Theorems are any kind of statements which are named using the theorem namespace. Theorems may have pretty names.

• Exercises are named using the exercise namespace.

The file may contain other LEAN's lemma whose name is not in one of the three namespaces definition, theorem, exercise. They will be ignored by d∃∀duction.

Metadata

• every metadata that is to be recollected by the parser must start with a line equal to /- dEAduction, followed by the name of the field alone on its line, followed by one or several lines containing the field content. Lines contaning field contents are indented. The next unindented line is either a new field name, or a -/indicating the end of metadata parsing. A typical example is:

lemma exercise.union_distributive_inter : A ∩ (B ∪ C)  = (A ∩ B) ∪ (A ∩ C) := 
/- dEAduction
PrettyName
    Intersection d'une union
Description
    L'intersection est distributive par rapport à l'union
AvailableLogic
    $ALL -negate
AvailableProof
    $ALL -contradiction
AvailableDefinitions
    $UNTIL_NOW -union_quelconque_ensembles -intersection_quelconque_ensembles
AvailableTheorems
    double_inclusion
-/

• For every exercise, the conceiver of the course may specify a list of available logic buttons, proofs buttons, (magic buttons: not implemented yet), and statements that will appear in the corresponding windows. For this the following macros are available:

  • $ALL means all buttons (fields AvailableLogic, AvailableProofs, AvailableMagic). For instance for field AvailableLogic, the field content $ALL -and -or will result in all boutons but the and /or buttons to be displayed for the corresponding exercise.

  • $UNTIL_NOW means all statements prior to the exercise (fields AvailableDefinitions, AvailableTheorems, AvailableExercises, AvailableStatements). For instance for definitions, i.e. the field AvailableDefinitions the content $UNTIL_NOW -union_quelconque_ensembles -intersection_quelconque_ensembles would indicate that all definitions prior to the exercise will be displayed, but the one which have been declared as lemma definition.union_quelconque_ensemblesand lemma definition.intersection_quelconque_ensembles.

  • The conceiver can build its own macros, e.g. in

/- dEAduction
$SET_OPERATIONS
   union_deux_ensembles intersection_deux_ensembles
-/
Then in every other fields, `$SET_OPERATION` may be used as a shortcut for the two statements.

• List of buttons: see this page.

Settings

Deaduction comes with a config.toml file which can be found in src/deaduction/share. This file sets the 'factory' settings. Most settings can be modified by the user in the settings menu, and then the user settings are stored in ~/.deaduction/config.toml. Here is an example of an entry in Deaduction's toml file:

[logic]
# "display_unified", "display_both", "display_switch"
button_use_or_prove_mode = "display_unified"

The settings can also be set in each Lean file, or even in each exercise of a Lean file, by using the metadata keyword 'Settings', e.g.:

/- dEAduction
Settings
    logic.force_indices_for_dummy_vars --> false
    functionality.allow_induction --> false
-/

Mind the differences with the toml format: you have to indicate the section name ('logic'), and the '=' sign is replaced by '-->'. The settings are modified accordingly when the exercise is loaded, and the previous settings are restored before the next exercise. Values which are strings must be typed as double-quoted strings, e.g. --> "beginner". For the moment not all settings may be indicated in this way.

Display definitions

Say you want to define two new notions (which are not already implemented in Deaduction exercises files), evenness and divisibility. In the Lean file your definition looks like

def even (a: ℤ) := ∃ b, a = 2*b 

def divise (a b:ℤ) := ∃ c, b = a * c

The property even a will be displayed by Deaduction as a even (or, in text mode, a is even). But divise a b will be displayed as b divise which is meaninigless. This can be fixed in the Lean source file, by adding the following metadata:

/- dEAduction
Display
    divise --> (-2, " | ", -1)
-/

Integers refer to the function's arguments; negative integers start from the end, as in Python, which is useful when the function has lots of uninteresting arguments. For instance the composition of function takes 5 arguments : the three involved sets, and the two functions. Thus the rule could be

/- dEAduction
Display
    composition -->  (-2, "∘", -1)
-/

\text_is can be used as a macro which is replaced by "is" in text mode and hidden in normal mode, thus we can get a is even or a even.

Caveat

• The use of keywords (namespace, lemma exercise., etc.) inside a docstring might confuse dEAduction parser.