diff options
| -rw-r--r-- | CHANGES | 1 | ||||
| -rw-r--r-- | pygments/lexers/_mapping.py | 1 | ||||
| -rw-r--r-- | pygments/lexers/theorem.py | 96 | ||||
| -rw-r--r-- | tests/examplefiles/test.lean | 217 |
4 files changed, 314 insertions, 1 deletions
@@ -43,6 +43,7 @@ Version 2.0 * Isabelle (PR#386) * Jasmin (PR#349) * Kal (PR#233) + * Lean (PR#399) * LSL (PR#296) * Limbo (PR#291) * Liquid (#977) diff --git a/pygments/lexers/_mapping.py b/pygments/lexers/_mapping.py index 2728d5cb..92dc45f8 100644 --- a/pygments/lexers/_mapping.py +++ b/pygments/lexers/_mapping.py @@ -190,6 +190,7 @@ LEXERS = { 'LassoJavascriptLexer': ('pygments.lexers.templates', 'JavaScript+Lasso', ('js+lasso', 'javascript+lasso'), (), ('application/x-javascript+lasso', 'text/x-javascript+lasso', 'text/javascript+lasso')), 'LassoLexer': ('pygments.lexers.javascript', 'Lasso', ('lasso', 'lassoscript'), ('*.lasso', '*.lasso[89]'), ('text/x-lasso',)), 'LassoXmlLexer': ('pygments.lexers.templates', 'XML+Lasso', ('xml+lasso',), (), ('application/xml+lasso',)), + 'LeanLexer': ('pygments.lexers.theorem', 'Lean', ('lean',), ('*.lean',), ('text/x-lean',)), 'LighttpdConfLexer': ('pygments.lexers.configs', 'Lighttpd configuration file', ('lighty', 'lighttpd'), (), ('text/x-lighttpd-conf',)), 'LimboLexer': ('pygments.lexers.inferno', 'Limbo', ('limbo',), ('*.b',), ('text/limbo',)), 'LiquidLexer': ('pygments.lexers.templates', 'liquid', ('liquid',), ('*.liquid',), ()), diff --git a/pygments/lexers/theorem.py b/pygments/lexers/theorem.py index b7d3b627..ba942dbf 100644 --- a/pygments/lexers/theorem.py +++ b/pygments/lexers/theorem.py @@ -9,11 +9,13 @@ :license: BSD, see LICENSE for details. """ +import re + from pygments.lexer import RegexLexer, default, words from pygments.token import Text, Comment, Operator, Keyword, Name, String, \ Number, Punctuation, Generic -__all__ = ['CoqLexer', 'IsabelleLexer'] +__all__ = ['CoqLexer', 'IsabelleLexer', 'LeanLexer'] class CoqLexer(RegexLexer): @@ -370,3 +372,95 @@ class IsabelleLexer(RegexLexer): (r'`', String.Other, '#pop'), ], } + + +class LeanLexer(RegexLexer): + """ + For the `Lean <https://github.com/leanprover/lean>`_ + theorem prover. + + .. versionadded:: 2.0 + """ + 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 = ( + '!=', '#', '&', '&&', '*', '+', '-', '/', '#', '@', + '-.', '->', '.', '..', '...', '::', ':>', ';', ';;', '<', + '<-', '=', '==', '>', '_', '`', '|', '||', '~', '=>', '<=', '>=', + '/\\', '\\/', 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 = ('(', ')', ':', '{', '}', '[', ']', u'⦃', u'⦄', ':=', ',') + + primitives = ('unit', 'int', 'bool', 'string', 'char', 'list', + 'array', 'prod', 'sum', 'pair', 'real', 'nat', 'num', 'path') + + tokens = { + 'root': [ + (r'\s+', Text), + (r'\b(false|true)\b|\(\)|\[\]', Name.Builtin.Pseudo), + (r'/-', Comment, 'comment'), + (r'--.*?$', Comment.Single), + (words(keywords1, prefix=r'\b', suffix=r'\b'), Keyword.Namespace), + (words(keywords2, prefix=r'\b', suffix=r'\b'), Keyword), + (words(keywords3, prefix=r'\b', suffix=r'\b'), Keyword.Type), + (words(keywords4, prefix=r'\b', suffix=r'\b'), Keyword), + (words(operators), Name.Builtin.Pseudo), + (words(word_operators, prefix=r'\b', suffix=r'\b'), Name.Builtin.Pseudo), + (words(punctuation), Operator), + (words(primitives, prefix=r'\b', suffix=r'\b'), Keyword.Type), + (u"[A-Za-z_\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2100-\u214f]" + u"[A-Za-z_'\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2070-\u2079" + u"\u207f-\u2089\u2090-\u209c\u2100-\u214f]*", Name), + (r'\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'), + ], + } 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 |