Alectryon

Lean allows you to write its own tactics and procedures using its internal API. This is known as metaprogramming.

• Monadic Interface: Most internal data structures and procedures are exposed via a monadic interface.
• The meta Keyword: Definitions that use the metaprogramming API (which access points outside the formal framework) must be annotated with the meta keyword. This informs Lean that these definitions are part of the metaprogramming layer rather than the trusted kernel.
• Safety: Even if a tactic is buggy, the resulting proof is always checked by the Lean kernel. If the tactic produces an invalid term, the kernel will reject it.

open expr tactic

private meta def contra_aux : list expr → list expr → tactic unit
| []         hs := failed
| (h₁ :: rs) hs := 
    do t₀ ← infer_type h₁,
       t  ← whnf t₀,
       (do a ← match_not t,
            h₂ ← find_same_type a hs,
            tgt ← target,
            pr ← mk_app `absurd [tgt, h₂, h₁],
            exact pr)
       <|> contra_aux rs hs

meta def contra : tactic unit := 
do ctx ← local_context,
   contra_aux ctx ctx

Instead of manually wrapping text in delimiters via JavaScript, you can configure MathJax to look for specific HTML classes using the processHtmlClass option. This is more robust but requires careful setup to ensure definitions are processed before MathJax loads.

1. Set the configuration:

   MathJax = { options: { processHtmlClass: 'mathjax_process|alectryon-io' } };

2. Customize the startup: Use MathJax.startup.pageReady to inject the necessary \( ... \) delimiters into the page before the default pageReady runs.
3. Handle loading order: Ensure this configuration is loaded before the MathJax script. In Alectryon's standalone mode, the defer option is already configured, making this reliable. In Sphinx, you must use mathjax_loading_method = "defer" or a separate JS file.

MathJax = {};
MathJax.options = { processHtmlClass: 'mathjax_process|alectryon-io' };

MathJax.startup = {
    pageReady: function () {
        // ... Custom code to add \( ... \) delimiters
        return MathJax.startup.defaultPageReady();
    }
}

Alectryon captures goals and hypotheses as Lean3 proofs progress. This allows you to document the state of a proof step-by-step.

Similar to the Coq integration, you can use the following features to reference or quote the captured proof state:

• References (:mref:): Link to specific steps or hypotheses (e.g., :mref:.s(intro H)`).
• Quotes (:mquote:): Quote specific parts of the proof state (e.g., :mquote:.s(and.intro).h#H.type`).
• Assertions (.. massert::): Assert properties about the proof state at a specific goal or step.

example (p q r : Prop) : p ∧ q ↔ q ∧ p :=
begin /- .none -/
  apply iff.intro, {
    intro H,
    apply and.intro, /- .unfold -/
    apply (and.elim_right H),
    apply (and.elim_left H),
  }, {
    intro H,
    apply and.intro,
    apply (and.elim_right H),
    apply (and.elim_left H),
  }
end

Usage in reST:

.. massert:: .s(apply iff.intro).g#2
.. mquote:: .s(apply iff.intro).g#2.ccl

Lean supports two primary styles of writing proofs:

1. Term Style

Proofs are constructed as explicit expressions in the formal language. For existential statements, you can use Unicode angle brackets ⟨ ... ⟩ (typed as \< and \>) or ASCII equivalents (| ... |) to package a witness and a proof of the property.

2. Tactic Style

Tactic-style proofs use instructions (tactics) that tell Lean how to construct the required expression. This is often more readable and allows for automation. Common tactics include:

• intros: Introduces variables into the local context.
• cases: Performs case analysis on a hypothesis.
• unfold: Expands a definition.
• existsi: Provides a witness for an existential quantifier.
• simp: Invokes the built-in simplifier to prove assertions using provided facts.
• by <tactic>: The by keyword transitions from term mode to tactic mode.

theorem even_add : ∀ m n, even m → even n → even (n + m) :=
begin
  intros m n hm hn,
  cases hm with k hk,
  cases hn with l hl,
  unfold even,
  existsi (k + l),
  simp [hk, hl, mul_add, add_sym]
end

Alectryon allows you to selectively show, hide, or link to specific parts of a proof (sentences, goals, messages, hypotheses, conclusions) using CSS-inspired paths.

Path Syntax:

• .s(*pattern*): Search for a sentence matching pattern. Use (pattern) for literal matching or {pattern} for fnmatch style.
• .msg(*str*): Match a message containing str.
• .g#id: Select goal by number (e.g., .g#1).
• .g(*str*): Select goal whose conclusion includes str.
• .h#name: Match hypothesis by name (e.g., .h#IHn).
• .h(*str*): Match hypothesis by content.
• .ccl: Match the conclusion of a goal.
• .type / .body / .name: Match hypothesis properties.

Example Paths:

• .s(Induction).h#IHm: Find sentence matching 'Induction', then find hypothesis 'IHm' in its first goal.
• .g#2.h#*: Hide all hypotheses in goal 2.

Experimental Features:

• Exclusion: Use -. prefix (e.g., -.h#IHn to hide hypothesis IHn).
• Key-Value Attributes: Append [key]=value to a path (e.g., .msg[lang]=haskell to use the Haskell lexer for message bodies).

## Example Pathing

- `.s(Goal ∀)` -> Search for sentence matching content
- `.s(Base case).ccl` -> Sentence matching 'Base case', then its first goal's conclusion
- `.s(Induction).h#IHm` -> Sentence matching 'Induction', then hypothesis 'IHm' in its first goal

Alectryon allows you to reference specific sentences, goals, and hypotheses within code fragments using a mini-language. This creates links to the corresponding parts of the proof output.

Reference Types

• By Text Search: Use :literal::mref:`search-term```. Alectryon searches for the text and automatically labels the first matching sentence.
• By Manual Label: Use :literal::mref:`label <target>`` to pick a specific label.
• By Path (Granular Access):
  • .s(sentence_name): A specific sentence.
  • .g#index: A specific goal (e.g., .g#1).
  • .h#name: A specific hypothesis.
  • .h(type_or_name): A hypothesis by its type or name.
  • .ccl: The conclusion of a goal.

Example Usage

.. coq::
   :name: setup

   Fixpoint plus_comm (n m: nat) : n + m = m + n.
   Proof.
     destruct n eqn:Heq.
     - (* Base case *) 
       rewrite <- plus_n_O; reflexivity.

# Reference the Fixpoint command
Starting at :mref:`Fixpoint plus_comm`.

# Reference a specific goal/hypothesis path
In the first case (:mref:`.s(destruct n).g#1`), we see the variable in the context (:mref:`.s(destruct n).g#1.h#n`).

:mref:`Fixpoint plus_comm"
:mref:`.s(destruct n).g#1"
:mref:`.s(destruct n).g#1.h#n"