Add lexer for lean theorem prover

2 files changed, 305 insertions, 1 deletions

diff --git a/pygments/lexers/functional.py b/pygments/lexers/functional.py
index a22c4f55..19c54f94 100644
--- a/pygments/lexers/functional.py
+++ b/pygments/lexers/functional.py
@@ -21,7 +21,7 @@ __all__ = ['RacketLexer', 'SchemeLexer', 'CommonLispLexer', 'CryptolLexer',
            'LiterateHaskellLexer', 'LiterateAgdaLexer', 'SMLLexer',
            'OcamlLexer', 'ErlangLexer', 'ErlangShellLexer', 'OpaLexer',
            'CoqLexer', 'NewLispLexer', 'NixLexer', 'ElixirLexer',
-           'ElixirConsoleLexer', 'KokaLexer', 'IdrisLexer',
+           'ElixirConsoleLexer', 'KokaLexer', 'IdrisLexer', 'LeanLexer',
            'LiterateIdrisLexer']
 
 
@@ -1686,6 +1686,93 @@ class AgdaLexer(RegexLexer):
         'escape': HaskellLexer.tokens['escape']
     }
 
+class LeanLexer(RegexLexer):
+    """
+    For the `Lean <https://github.com/leanprover/lean>`_
+    theorem prover
+    """
+    name = 'Lean'
+    aliases = ['lean']
+    filenames = ['*.lean']
+    mimetypes = ['text/x-lean']
+
+    flags = re.MULTILINE | re.UNICODE
+
+    keywords1 = ['import', 'abbreviation', 'opaque_hint', 'tactic_hint', 'definition', 'renaming',
+                 'inline', 'hiding', 'exposing', 'parameter', 'parameters', 'conjecture',
+                 'hypothesis', 'lemma', 'corollary', 'variable', 'variables', 'print', 'theorem',
+                 'axiom', 'inductive', 'structure', 'universe', 'alias', 'help',
+                 'options', 'precedence', 'postfix', 'prefix', 'calc_trans', 'calc_subst', 'calc_refl',
+                 'infix', 'infixl', 'infixr', 'notation', 'eval', 'check', 'exit', 'coercion', 'end',
+                 'private', 'using', 'namespace', 'including', 'instance', 'section', 'context',
+                 'protected', 'expose', 'export', 'set_option', 'add_rewrite', 'extends']
+
+    keywords2 = [
+        'forall', 'exists', 'fun', 'Pi', 'obtain', 'from', 'have', 'show', 'assume', 'take',
+        'let', 'if', 'else', 'then', 'by', 'in', 'with', 'begin', 'proof', 'qed', 'calc'
+    ]
+
+    keywords3 = [
+        # Sorts
+        'Type', 'Prop',
+    ]
+
+    keywords4 = [
+        # Tactics
+        'apply', 'and_then', 'or_else', 'append', 'interleave', 'par', 'fixpoint', 'repeat',
+        'at_most', 'discard', 'focus_at', 'rotate', 'try_for', 'now', 'assumption', 'eassumption',
+        'state', 'intro', 'generalize', 'exact', 'unfold', 'beta', 'trace', 'focus', 'repeat1',
+        'determ', 'destruct', 'try', 'auto', 'intros'
+    ]
+
+    operators = [
+        '!=', '#', '&', '&&', r'\*', r'\+', '-', '/', r'#', r'@',
+        r'-\.', '->', r'\.', r'\.\.', r'\.\.\.', '::', ':>', ';', ';;', '<',
+        '<-', '=', '==', '>', '_', '`', r'\|', r'\|\|', '~', '=>', '<=', '>=',
+        r'/\\', r'\\/', u'∀', u'Π', u'λ', u'↔', u'∧', u'∨', u'≠', u'≤', u'≥', u'¬', u'⁻¹', u'⬝', u'▸',
+        u'→', u'∃', u'ℕ', u'ℤ', u'≈'
+    ]
+
+    word_operators = ['and', 'or', 'not', 'iff', 'eq']
+
+    punctuation = [ r'\(', r'\)', r':', r'{', r'}', r'\[', r'\]', u'⦃', u'⦄', r':=', r',' ]
+
+    primitives = ['unit', 'int', 'bool', 'string', 'char', 'list',
+                  'array', 'prod', 'sum', 'pair', 'real', 'nat', 'num', 'path']
+
+    tokens = {
+        'root': [
+            (r'\s+', Text),
+            (r'\b(false)\b|\b(true)\b|\(\)|\[\]', Name.Builtin.Pseudo),
+            (r'/-', Comment, 'comment'),
+            (r'--.*?$', Comment.Single),
+            (r'\b(%s)\b' % '|'.join(keywords1), Keyword.Namespace),
+            (r'\b(%s)\b' % '|'.join(keywords2), Keyword),
+            (r'\b(%s)\b' % '|'.join(keywords3), Keyword.Type),
+            (r'\b(%s)\b' % '|'.join(keywords4), Keyword),
+            (r'(%s)' % '|'.join(operators[::-1]), Name.Builtin.Pseudo),
+            (r'\b(%s)\b' % '|'.join(word_operators), Name.Builtin.Pseudo),
+            (r'(%s)' % '|'.join(punctuation[::-1]), Operator),
+            (r'\b(%s)\b' % '|'.join(primitives), Keyword.Type),
+            (u"[A-Za-z_\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2100-\u214f][A-Za-z_'\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2070-\u2079\u207f-\u2089\u2090-\u209c\u2100-\u214f]*", Name),
+            (r'\d[\d]*', Number.Integer),
+            (r'"', String.Double, 'string'),
+            (r'[~?][a-z][\w\']*:', Name.Variable)
+        ],
+        'comment': [
+            # Multiline Comments
+            (r'[^/-]', Comment.Multiline),
+            (r'/-', Comment.Multiline, '#push'),
+            (r'-/', Comment.Multiline, '#pop'),
+            (r'[/-]', Comment.Multiline)
+        ],
+        'string': [
+            (r'[^\\"]+', String.Double),
+            (r'\\[n"\\]', String.Escape),
+            ('"', String.Double, '#pop'),
+        ],
+    }
+
 
 class LiterateLexer(Lexer):
     """
diff --git a/tests/examplefiles/test.lean b/tests/examplefiles/test.lean
new file mode 100644
index 00000000..a7b7e261
--- /dev/null
+++ b/tests/examplefiles/test.lean
@@ -0,0 +1,217 @@
+/-
+Theorems/Exercises from "Logical Investigations, with the Nuprl Proof Assistant"
+by Robert L. Constable and Anne Trostle
+http://www.nuprl.org/MathLibrary/LogicalInvestigations/
+-/
+import logic
+
+-- 2. The Minimal Implicational Calculus
+theorem thm1 {A B : Prop} : A → B → A :=
+assume Ha Hb, Ha
+
+theorem thm2 {A B C : Prop} : (A → B) → (A → B → C) → (A → C) :=
+assume Hab Habc Ha,
+  Habc Ha (Hab Ha)
+
+theorem thm3 {A B C : Prop} : (A → B) → (B → C) → (A → C) :=
+assume Hab Hbc Ha,
+  Hbc (Hab Ha)
+
+-- 3. False Propositions and Negation
+theorem thm4 {P Q : Prop} : ¬P → P → Q :=
+assume Hnp Hp,
+  absurd Hp Hnp
+
+theorem thm5 {P : Prop} : P → ¬¬P :=
+assume (Hp : P) (HnP : ¬P),
+  absurd Hp HnP
+
+theorem thm6 {P Q : Prop} : (P → Q) → (¬Q → ¬P) :=
+assume (Hpq : P → Q) (Hnq : ¬Q) (Hp : P),
+  have Hq : Q, from Hpq Hp,
+  show false, from absurd Hq Hnq
+
+theorem thm7 {P Q : Prop} : (P → ¬P) → (P → Q) :=
+assume Hpnp Hp,
+  absurd Hp (Hpnp Hp)
+
+theorem thm8 {P Q : Prop} : ¬(P → Q) → (P → ¬Q) :=
+assume (Hn : ¬(P → Q)) (Hp : P) (Hq : Q),
+  -- Rermak we don't even need the hypothesis Hp
+  have H : P → Q, from assume H', Hq,
+  absurd H Hn
+
+-- 4. Conjunction and Disjunction
+theorem thm9 {P : Prop} : (P ∨ ¬P) → (¬¬P → P) :=
+assume (em : P ∨ ¬P) (Hnn : ¬¬P),
+  or_elim em
+    (assume Hp, Hp)
+    (assume Hn, absurd Hn Hnn)
+
+theorem thm10 {P : Prop} : ¬¬(P ∨ ¬P) :=
+assume Hnem : ¬(P ∨ ¬P),
+  have Hnp : ¬P, from
+    assume Hp : P,
+      have Hem : P ∨ ¬P, from or_inl Hp,
+      absurd Hem Hnem,
+  have Hem : P ∨ ¬P, from or_inr Hnp,
+  absurd Hem Hnem
+
+theorem thm11 {P Q : Prop} : ¬P ∨ ¬Q → ¬(P ∧ Q) :=
+assume (H : ¬P ∨ ¬Q) (Hn : P ∧ Q),
+  or_elim H
+    (assume Hnp : ¬P, absurd (and_elim_left Hn) Hnp)
+    (assume Hnq : ¬Q, absurd (and_elim_right Hn) Hnq)
+
+theorem thm12 {P Q : Prop} : ¬(P ∨ Q) → ¬P ∧ ¬Q :=
+assume H : ¬(P ∨ Q),
+  have Hnp : ¬P, from assume Hp : P, absurd (or_inl Hp) H,
+  have Hnq : ¬Q, from assume Hq : Q, absurd (or_inr Hq) H,
+  and_intro Hnp Hnq
+
+theorem thm13 {P Q : Prop} : ¬P ∧ ¬Q → ¬(P ∨ Q) :=
+assume (H : ¬P ∧ ¬Q) (Hn : P ∨ Q),
+  or_elim Hn
+    (assume Hp : P, absurd Hp (and_elim_left H))
+    (assume Hq : Q, absurd Hq (and_elim_right H))
+
+theorem thm14 {P Q : Prop} : ¬P ∨ Q → P → Q :=
+assume (Hor : ¬P ∨ Q) (Hp : P),
+  or_elim Hor
+    (assume Hnp : ¬P, absurd Hp Hnp)
+    (assume Hq : Q, Hq)
+
+theorem thm15 {P Q : Prop} : (P → Q) → ¬¬(¬P ∨ Q) :=
+assume (Hpq : P → Q) (Hn : ¬(¬P ∨ Q)),
+  have H1 : ¬¬P ∧ ¬Q, from thm12 Hn,
+  have Hnp : ¬P, from mt Hpq (and_elim_right H1),
+  absurd Hnp (and_elim_left H1)
+
+theorem thm16 {P Q : Prop} : (P → Q) ∧ ((P ∨ ¬P) ∨ (Q ∨ ¬Q)) → ¬P ∨ Q :=
+assume H : (P → Q) ∧ ((P ∨ ¬P) ∨ (Q ∨ ¬Q)),
+  have Hpq : P → Q, from and_elim_left H,
+  or_elim (and_elim_right H)
+    (assume Hem1 : P ∨ ¬P, or_elim Hem1
+      (assume Hp : P, or_inr (Hpq Hp))
+      (assume Hnp : ¬P, or_inl Hnp))
+    (assume Hem2 : Q ∨ ¬Q, or_elim Hem2
+      (assume Hq : Q, or_inr Hq)
+      (assume Hnq : ¬Q, or_inl (mt Hpq Hnq)))
+
+-- 5. First-Order Logic: All and Exists
+section
+parameters {T : Type} {C : Prop} {P : T → Prop}
+theorem thm17a : (C → ∀x, P x) → (∀x, C → P x) :=
+assume H : C → ∀x, P x,
+  take x : T, assume Hc : C,
+  H Hc x
+
+theorem thm17b : (∀x, C → P x) → (C → ∀x, P x) :=
+assume (H : ∀x, C → P x) (Hc : C),
+  take x : T,
+  H x Hc
+
+theorem thm18a : ((∃x, P x) → C) → (∀x, P x → C) :=
+assume H : (∃x, P x) → C,
+  take x, assume Hp : P x,
+  have Hex : ∃x, P x, from exists_intro x Hp,
+  H Hex
+
+theorem thm18b : (∀x, P x → C) → (∃x, P x) → C :=
+assume (H1 : ∀x, P x → C) (H2 : ∃x, P x),
+  obtain (w : T) (Hw : P w), from H2,
+  H1 w Hw
+
+theorem thm19a : (C ∨ ¬C) → (∃x : T, true) → (C → (∃x, P x)) → (∃x, C → P x) :=
+assume (Hem : C ∨ ¬C) (Hin : ∃x : T, true) (H1 : C → ∃x, P x),
+  or_elim Hem
+    (assume Hc : C,
+      obtain (w : T) (Hw : P w), from H1 Hc,
+      have Hr : C → P w, from assume Hc, Hw,
+      exists_intro w Hr)
+    (assume Hnc : ¬C,
+      obtain (w : T) (Hw : true), from Hin,
+      have Hr : C → P w, from assume Hc, absurd Hc Hnc,
+      exists_intro w Hr)
+
+theorem thm19b : (∃x, C → P x) → C → (∃x, P x) :=
+assume (H : ∃x, C → P x) (Hc : C),
+  obtain (w : T) (Hw : C → P w), from H,
+  exists_intro w (Hw Hc)
+
+theorem thm20a : (C ∨ ¬C) → (∃x : T, true) → ((¬∀x, P x) → ∃x, ¬P x) → ((∀x, P x) → C) → (∃x, P x → C) :=
+assume Hem Hin Hnf H,
+  or_elim Hem
+    (assume Hc : C,
+      obtain (w : T) (Hw : true), from Hin,
+      exists_intro w (assume H : P w, Hc))
+    (assume Hnc : ¬C,
+      have H1 : ¬(∀x, P x), from mt H Hnc,
+      have H2 : ∃x, ¬P x, from Hnf H1,
+      obtain (w : T) (Hw : ¬P w), from H2,
+      exists_intro w (assume H : P w, absurd H Hw))
+
+theorem thm20b : (∃x, P x → C) → (∀ x, P x) → C :=
+assume Hex Hall,
+  obtain (w : T) (Hw : P w → C), from Hex,
+  Hw (Hall w)
+
+theorem thm21a : (∃x : T, true) → ((∃x, P x) ∨ C) → (∃x, P x ∨ C) :=
+assume Hin H,
+  or_elim H
+    (assume Hex : ∃x, P x,
+      obtain (w : T) (Hw : P w), from Hex,
+      exists_intro w (or_inl Hw))
+    (assume Hc  : C,
+      obtain (w : T) (Hw : true), from Hin,
+      exists_intro w (or_inr Hc))
+
+theorem thm21b : (∃x, P x ∨ C) → ((∃x, P x) ∨ C) :=
+assume H,
+  obtain (w : T) (Hw : P w ∨ C), from H,
+  or_elim Hw
+    (assume H : P w, or_inl (exists_intro w H))
+    (assume Hc : C, or_inr Hc)
+
+theorem thm22a : (∀x, P x) ∨ C → ∀x, P x ∨ C :=
+assume H, take x,
+  or_elim H
+    (assume Hl, or_inl (Hl x))
+    (assume Hr, or_inr Hr)
+
+theorem thm22b : (C ∨ ¬C) → (∀x, P x ∨ C) → ((∀x, P x) ∨ C) :=
+assume Hem H1,
+  or_elim Hem
+    (assume Hc : C,   or_inr Hc)
+    (assume Hnc : ¬C,
+      have Hx : ∀x, P x, from
+        take x,
+        have H1 : P x ∨ C, from H1 x,
+        resolve_left H1 Hnc,
+      or_inl Hx)
+
+theorem thm23a : (∃x, P x) ∧ C → (∃x, P x ∧ C) :=
+assume H,
+  have Hex : ∃x, P x, from and_elim_left H,
+  have Hc : C, from and_elim_right H,
+  obtain (w : T) (Hw : P w), from Hex,
+  exists_intro w (and_intro Hw Hc)
+
+theorem thm23b : (∃x, P x ∧ C) → (∃x, P x) ∧ C :=
+assume H,
+  obtain (w : T) (Hw : P w ∧ C), from H,
+  have Hex : ∃x, P x, from exists_intro w (and_elim_left Hw),
+  and_intro Hex (and_elim_right Hw)
+
+theorem thm24a : (∀x, P x) ∧ C → (∀x, P x ∧ C) :=
+assume H, take x,
+  and_intro (and_elim_left H x) (and_elim_right H)
+
+theorem thm24b : (∃x : T, true) → (∀x, P x ∧ C) → (∀x, P x) ∧ C :=
+assume Hin H,
+  obtain (w : T) (Hw : true), from Hin,
+  have Hc : C, from and_elim_right (H w),
+  have Hx : ∀x, P x, from take x, and_elim_left (H x),
+  and_intro Hx Hc
+
+end -- of section