diff options
| -rw-r--r-- | CHANGES | 1 | ||||
| -rw-r--r-- | pygments/lexers/_mapping.py | 4 | ||||
| -rw-r--r-- | pygments/lexers/functional.py | 144 | ||||
| -rw-r--r-- | pygments/lexers/hdl.py | 4 | ||||
| -rwxr-xr-x | scripts/find_error.py | 3 | ||||
| -rw-r--r-- | tests/examplefiles/coq_RelationClasses | 447 |
6 files changed, 598 insertions, 5 deletions
@@ -33,6 +33,7 @@ Version 1.5 * Urbiscript (PR#17) * OpenEdge ABL (PR#27) * SystemVerilog (PR#35) + * Coq (#734) - In the LaTeX formatter, escape special &, < and > chars (#648). diff --git a/pygments/lexers/_mapping.py b/pygments/lexers/_mapping.py index fb4e0703..180037f7 100644 --- a/pygments/lexers/_mapping.py +++ b/pygments/lexers/_mapping.py @@ -56,6 +56,7 @@ LEXERS = { 'ColdfusionHtmlLexer': ('pygments.lexers.templates', 'Coldfusion HTML', ('cfm',), ('*.cfm', '*.cfml', '*.cfc'), ('application/x-coldfusion',)), 'ColdfusionLexer': ('pygments.lexers.templates', 'cfstatement', ('cfs',), (), ()), 'CommonLispLexer': ('pygments.lexers.functional', 'Common Lisp', ('common-lisp', 'cl'), ('*.cl', '*.lisp', '*.lsp', '*.el'), ('text/x-common-lisp',)), + 'CoqLexer': ('pygments.lexers.functional', 'Coq', ('coq',), ('*.v',), ('text/x-coq',)), 'CppLexer': ('pygments.lexers.compiled', 'C++', ('cpp', 'c++'), ('*.cpp', '*.hpp', '*.c++', '*.h++', '*.cc', '*.hh', '*.cxx', '*.hxx'), ('text/x-c++hdr', 'text/x-c++src')), 'CppObjdumpLexer': ('pygments.lexers.asm', 'cpp-objdump', ('cpp-objdump', 'c++-objdumb', 'cxx-objdump'), ('*.cpp-objdump', '*.c++-objdump', '*.cxx-objdump'), ('text/x-cpp-objdump',)), 'CssDjangoLexer': ('pygments.lexers.templates', 'CSS+Django/Jinja', ('css+django', 'css+jinja'), (), ('text/css+django', 'text/css+jinja')), @@ -170,12 +171,9 @@ LEXERS = { 'OpenEdgeLexer': ('pygments.lexers.other', 'OpenEdge ABL', ('openedge', 'abl', 'progress'), ('*.p', '*.cls'), ('text/x-openedge', 'application/x-openedge')), 'PerlLexer': ('pygments.lexers.agile', 'Perl', ('perl', 'pl'), ('*.pl', '*.pm'), ('text/x-perl', 'application/x-perl')), 'PhpLexer': ('pygments.lexers.web', 'PHP', ('php', 'php3', 'php4', 'php5'), ('*.php', '*.php[345]'), ('text/x-php',)), - 'PlPgsqlLexer': ('pygments.lexers.postgres', 'PL/pgSQL', ('plpgsql',), (), ('text/x-plpgsql',)), 'PlPgsqlLexer': ('pygments.lexers.sql', 'PL/pgSQL', ('plpgsql',), (), ('text/x-plpgsql',)), 'PostScriptLexer': ('pygments.lexers.other', 'PostScript', ('postscript',), ('*.ps', '*.eps'), ('application/postscript',)), - 'PostgresConsoleLexer': ('pygments.lexers.postgres', 'PostgreSQL console (psql)', ('psql', 'postgresql-console', 'postgres-console'), (), ('text/x-postgresql-psql',)), 'PostgresConsoleLexer': ('pygments.lexers.sql', 'PostgreSQL console (psql)', ('psql', 'postgresql-console', 'postgres-console'), (), ('text/x-postgresql-psql',)), - 'PostgresLexer': ('pygments.lexers.postgres', 'PostgreSQL SQL dialect', ('postgresql', 'postgres'), (), ('text/x-postgresql',)), 'PostgresLexer': ('pygments.lexers.sql', 'PostgreSQL SQL dialect', ('postgresql', 'postgres'), (), ('text/x-postgresql',)), 'PovrayLexer': ('pygments.lexers.other', 'POVRay', ('pov',), ('*.pov', '*.inc'), ('text/x-povray',)), 'PrologLexer': ('pygments.lexers.compiled', 'Prolog', ('prolog',), ('*.prolog', '*.pro', '*.pl'), ('text/x-prolog',)), diff --git a/pygments/lexers/functional.py b/pygments/lexers/functional.py index e3b099df..0b3e1f36 100644 --- a/pygments/lexers/functional.py +++ b/pygments/lexers/functional.py @@ -14,11 +14,10 @@ import re from pygments.lexer import Lexer, RegexLexer, bygroups, include, do_insertions from pygments.token import Text, Comment, Operator, Keyword, Name, \ String, Number, Punctuation, Literal, Generic, Error -import pygments.formatters __all__ = ['SchemeLexer', 'CommonLispLexer', 'HaskellLexer', 'LiterateHaskellLexer', 'SMLLexer', 'OcamlLexer', 'ErlangLexer', - 'ErlangShellLexer', 'OpaLexer'] + 'ErlangShellLexer', 'OpaLexer', 'CoqLexer'] class SchemeLexer(RegexLexer): @@ -1399,3 +1398,144 @@ class OpaLexer(RegexLexer): (r'[^\-]+|-', Comment), ], } + + +class CoqLexer(RegexLexer): + """ + For the `Coq <http://coq.inria.fr/>`_ theorem prover. + + *New in Pygments 1.5.* + """ + + name = 'Coq' + aliases = ['coq'] + filenames = ['*.v'] + mimetypes = ['text/x-coq'] + + keywords1 = [ + # Vernacular commands + 'Section', 'Module', 'End', 'Require', 'Import', 'Export', 'Variable', + 'Variables', 'Parameter', 'Parameters', 'Axiom', 'Hypothesis', + 'Hypotheses', 'Notation', 'Local', 'Tactic', 'Reserved', 'Scope', + 'Open', 'Close', 'Bind', 'Delimit', 'Definition', 'Let', 'Ltac', + 'Fixpoint', 'CoFixpoint', 'Morphism', 'Relation', 'Implicit', + 'Arguments', 'Set', 'Unset', 'Contextual', 'Strict', 'Prenex', + 'Implicits', 'Inductive', 'CoInductive', 'Record', 'Structure', + 'Canonical', 'Coercion', 'Theorem', 'Lemma', 'Corollary', + 'Proposition', 'Fact', 'Remark', 'Example', 'Proof', 'Goal', 'Save', + 'Qed', 'Defined', 'Hint', 'Resolve', 'Rewrite', 'View', 'Search', + 'Show', 'Print', 'Printing', 'All', 'Graph', 'Projections', 'inside', + 'outside', + ] + keywords2 = [ + # Gallina + 'forall', 'exists', 'exists2', 'fun', 'fix', 'cofix', 'struct', + 'match', 'end', 'in', 'return', 'let', 'if', 'is', 'then', 'else', + 'for', 'of', 'nosimpl', 'with', 'as', + ] + keywords3 = [ + # Sorts + 'Type', 'Prop', + ] + keywords4 = [ + # Tactics + 'pose', 'set', 'move', 'case', 'elim', 'apply', 'clear', 'hnf', 'intro', + 'intros', 'generalize', 'rename', 'pattern', 'after', 'destruct', + 'induction', 'using', 'refine', 'inversion', 'injection', 'rewrite', + 'congr', 'unlock', 'compute', 'ring', 'field', 'replace', 'fold', + 'unfold', 'change', 'cutrewrite', 'simpl', 'have', 'suff', 'wlog', + 'suffices', 'without', 'loss', 'nat_norm', 'assert', 'cut', 'trivial', + 'revert', 'bool_congr', 'nat_congr', 'symmetry', 'transitivity', 'auto', + 'split', 'left', 'right', 'autorewrite', + ] + keywords5 = [ + # Terminators + 'by', 'done', 'exact', 'reflexivity', 'tauto', 'romega', 'omega', + 'assumption', 'solve', 'contradiction', 'discriminate', + ] + keywords6 = [ + # Control + 'do', 'last', 'first', 'try', 'idtac', 'repeat', + ] + # 'as', 'assert', 'begin', 'class', 'constraint', 'do', 'done', + # 'downto', 'else', 'end', 'exception', 'external', 'false', + # 'for', 'fun', 'function', 'functor', 'if', 'in', 'include', + # 'inherit', 'initializer', 'lazy', 'let', 'match', 'method', + # 'module', 'mutable', 'new', 'object', 'of', 'open', 'private', + # 'raise', 'rec', 'sig', 'struct', 'then', 'to', 'true', 'try', + # 'type', 'val', 'virtual', 'when', 'while', 'with' + keyopts = [ + '!=', '#', '&', '&&', r'\(', r'\)', r'\*', r'\+', ',', '-', + r'-\.', '->', r'\.', r'\.\.', ':', '::', ':=', ':>', ';', ';;', '<', + '<-', '=', '>', '>]', '>}', r'\?', r'\?\?', r'\[', r'\[<', r'\[>', + r'\[\|', ']', '_', '`', '{', '{<', r'\|', r'\|]', '}', '~', '=>', + r'/\\', r'\\/', + u'Π', u'λ', + ] + operators = r'[!$%&*+\./:<=>?@^|~-]' + word_operators = ['and', 'asr', 'land', 'lor', 'lsl', 'lxor', 'mod', 'or'] + prefix_syms = r'[!?~]' + infix_syms = r'[=<>@^|&+\*/$%-]' + primitives = ['unit', 'int', 'float', 'bool', 'string', 'char', 'list', + 'array'] + + tokens = { + 'root': [ + (r'\s+', Text), + (r'false|true|\(\)|\[\]', Name.Builtin.Pseudo), + (r'\(\*', Comment, 'comment'), + (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'\b(%s)\b' % '|'.join(keywords5), Keyword.Pseudo), + (r'\b(%s)\b' % '|'.join(keywords6), Keyword.Reserved), + (r'\b([A-Z][A-Za-z0-9_\']*)(?=\s*\.)', + Name.Namespace, 'dotted'), + (r'\b([A-Z][A-Za-z0-9_\']*)', Name.Class), + (r'(%s)' % '|'.join(keyopts), Operator), + (r'(%s|%s)?%s' % (infix_syms, prefix_syms, operators), Operator), + (r'\b(%s)\b' % '|'.join(word_operators), Operator.Word), + (r'\b(%s)\b' % '|'.join(primitives), Keyword.Type), + + (r"[^\W\d][\w']*", Name), + + (r'\d[\d_]*', Number.Integer), + (r'0[xX][\da-fA-F][\da-fA-F_]*', Number.Hex), + (r'0[oO][0-7][0-7_]*', Number.Oct), + (r'0[bB][01][01_]*', Number.Binary), + (r'-?\d[\d_]*(.[\d_]*)?([eE][+\-]?\d[\d_]*)', Number.Float), + + (r"'(?:(\\[\\\"'ntbr ])|(\\[0-9]{3})|(\\x[0-9a-fA-F]{2}))'", + String.Char), + (r"'.'", String.Char), + (r"'", Keyword), # a stray quote is another syntax element + + (r'"', String.Double, 'string'), + + (r'[~?][a-z][\w\']*:', Name.Variable), + ], + 'comment': [ + (r'[^(*)]+', Comment), + (r'\(\*', Comment, '#push'), + (r'\*\)', Comment, '#pop'), + (r'[(*)]', Comment), + ], + 'string': [ + (r'[^"]+', String.Double), + (r'""', String.Double), + (r'"', String.Double, '#pop'), + ], + 'dotted': [ + (r'\s+', Text), + (r'\.', Punctuation), + (r'[A-Z][A-Za-z0-9_\']*(?=\s*\.)', Name.Namespace), + (r'[A-Z][A-Za-z0-9_\']*', Name.Class, '#pop'), + (r'[a-z][a-z0-9_\']*', Name, '#pop'), + (r'', Text, '#pop') + ], + } + + def analyse_text(text): + if text.startswith('(*'): + return True diff --git a/pygments/lexers/hdl.py b/pygments/lexers/hdl.py index 989b0f25..d7180374 100644 --- a/pygments/lexers/hdl.py +++ b/pygments/lexers/hdl.py @@ -264,3 +264,7 @@ class SystemVerilogLexer(RegexLexer): if value.isupper(): token = Name.Constant yield index, token, value + + def analyse_text(text): + if text.startswith('//') or text.startswith('/*'): + return 0.5 diff --git a/scripts/find_error.py b/scripts/find_error.py index 1b793790..fcd36199 100755 --- a/scripts/find_error.py +++ b/scripts/find_error.py @@ -101,6 +101,9 @@ def main(fn, lexer=None, options={}): if lx.__class__.__bases__ == (RegexLexer,): lx.__class__.__bases__ = (DebuggingRegexLexer,) debug_lexer = True + elif lx.__class__.__bases__ == (DebuggingRegexLexer,): + # already debugged before + debug_lexer = True lno = 1 text = file(fn, 'U').read() text = text.strip('\n') + '\n' diff --git a/tests/examplefiles/coq_RelationClasses b/tests/examplefiles/coq_RelationClasses new file mode 100644 index 00000000..94c51bf1 --- /dev/null +++ b/tests/examplefiles/coq_RelationClasses @@ -0,0 +1,447 @@ +(* -*- coding: utf-8 -*- *) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** * Typeclass-based relations, tactics and standard instances + + This is the basic theory needed to formalize morphisms and setoids. + + Author: Matthieu Sozeau + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) + +(* $Id: RelationClasses.v 14641 2011-11-06 11:59:10Z herbelin $ *) + +Require Export Coq.Classes.Init. +Require Import Coq.Program.Basics. +Require Import Coq.Program.Tactics. +Require Import Coq.Relations.Relation_Definitions. + +(** We allow to unfold the [relation] definition while doing morphism search. *) + +Notation inverse R := (flip (R:relation _) : relation _). + +Definition complement {A} (R : relation A) : relation A := fun x y => R x y -> False. + +(** Opaque for proof-search. *) +Typeclasses Opaque complement. + +(** These are convertible. *) + +Lemma complement_inverse : forall A (R : relation A), complement (inverse R) = inverse (complement R). +Proof. reflexivity. Qed. + +(** We rebind relations in separate classes to be able to overload each proof. *) + +Set Implicit Arguments. +Unset Strict Implicit. + +Class Reflexive {A} (R : relation A) := + reflexivity : forall x, R x x. + +Class Irreflexive {A} (R : relation A) := + irreflexivity : Reflexive (complement R). + +Hint Extern 1 (Reflexive (complement _)) => class_apply @irreflexivity : typeclass_instances. + +Class Symmetric {A} (R : relation A) := + symmetry : forall x y, R x y -> R y x. + +Class Asymmetric {A} (R : relation A) := + asymmetry : forall x y, R x y -> R y x -> False. + +Class Transitive {A} (R : relation A) := + transitivity : forall x y z, R x y -> R y z -> R x z. + +Hint Resolve @irreflexivity : ord. + +Unset Implicit Arguments. + +(** A HintDb for relations. *) + +Ltac solve_relation := + match goal with + | [ |- ?R ?x ?x ] => reflexivity + | [ H : ?R ?x ?y |- ?R ?y ?x ] => symmetry ; exact H + end. + +Hint Extern 4 => solve_relation : relations. + +(** We can already dualize all these properties. *) + +Generalizable Variables A B C D R S T U l eqA eqB eqC eqD. + +Lemma flip_Reflexive `{Reflexive A R} : Reflexive (flip R). +Proof. tauto. Qed. + +Hint Extern 3 (Reflexive (flip _)) => apply flip_Reflexive : typeclass_instances. + +Program Definition flip_Irreflexive `(Irreflexive A R) : Irreflexive (flip R) := + irreflexivity (R:=R). + +Program Definition flip_Symmetric `(Symmetric A R) : Symmetric (flip R) := + fun x y H => symmetry (R:=R) H. + +Program Definition flip_Asymmetric `(Asymmetric A R) : Asymmetric (flip R) := + fun x y H H' => asymmetry (R:=R) H H'. + +Program Definition flip_Transitive `(Transitive A R) : Transitive (flip R) := + fun x y z H H' => transitivity (R:=R) H' H. + +Hint Extern 3 (Irreflexive (flip _)) => class_apply flip_Irreflexive : typeclass_instances. +Hint Extern 3 (Symmetric (flip _)) => class_apply flip_Symmetric : typeclass_instances. +Hint Extern 3 (Asymmetric (flip _)) => class_apply flip_Asymmetric : typeclass_instances. +Hint Extern 3 (Transitive (flip _)) => class_apply flip_Transitive : typeclass_instances. + +Definition Reflexive_complement_Irreflexive `(Reflexive A (R : relation A)) + : Irreflexive (complement R). +Proof. firstorder. Qed. + +Definition complement_Symmetric `(Symmetric A (R : relation A)) : Symmetric (complement R). +Proof. firstorder. Qed. + +Hint Extern 3 (Symmetric (complement _)) => class_apply complement_Symmetric : typeclass_instances. +Hint Extern 3 (Irreflexive (complement _)) => class_apply Reflexive_complement_Irreflexive : typeclass_instances. + +(** * Standard instances. *) + +Ltac reduce_hyp H := + match type of H with + | context [ _ <-> _ ] => fail 1 + | _ => red in H ; try reduce_hyp H + end. + +Ltac reduce_goal := + match goal with + | [ |- _ <-> _ ] => fail 1 + | _ => red ; intros ; try reduce_goal + end. + +Tactic Notation "reduce" "in" hyp(Hid) := reduce_hyp Hid. + +Ltac reduce := reduce_goal. + +Tactic Notation "apply" "*" constr(t) := + first [ refine t | refine (t _) | refine (t _ _) | refine (t _ _ _) | refine (t _ _ _ _) | + refine (t _ _ _ _ _) | refine (t _ _ _ _ _ _) | refine (t _ _ _ _ _ _ _) ]. + +Ltac simpl_relation := + unfold flip, impl, arrow ; try reduce ; program_simpl ; + try ( solve [ intuition ]). + +Local Obligation Tactic := simpl_relation. + +(** Logical implication. *) + +Program Instance impl_Reflexive : Reflexive impl. +Program Instance impl_Transitive : Transitive impl. + +(** Logical equivalence. *) + +Program Instance iff_Reflexive : Reflexive iff. +Program Instance iff_Symmetric : Symmetric iff. +Program Instance iff_Transitive : Transitive iff. + +(** Leibniz equality. *) + +Instance eq_Reflexive {A} : Reflexive (@eq A) := @eq_refl A. +Instance eq_Symmetric {A} : Symmetric (@eq A) := @eq_sym A. +Instance eq_Transitive {A} : Transitive (@eq A) := @eq_trans A. + +(** Various combinations of reflexivity, symmetry and transitivity. *) + +(** A [PreOrder] is both Reflexive and Transitive. *) + +Class PreOrder {A} (R : relation A) : Prop := { + PreOrder_Reflexive :> Reflexive R ; + PreOrder_Transitive :> Transitive R }. + +(** A partial equivalence relation is Symmetric and Transitive. *) + +Class PER {A} (R : relation A) : Prop := { + PER_Symmetric :> Symmetric R ; + PER_Transitive :> Transitive R }. + +(** Equivalence relations. *) + +Class Equivalence {A} (R : relation A) : Prop := { + Equivalence_Reflexive :> Reflexive R ; + Equivalence_Symmetric :> Symmetric R ; + Equivalence_Transitive :> Transitive R }. + +(** An Equivalence is a PER plus reflexivity. *) + +Instance Equivalence_PER `(Equivalence A R) : PER R | 10 := + { PER_Symmetric := Equivalence_Symmetric ; + PER_Transitive := Equivalence_Transitive }. + +(** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *) + +Class Antisymmetric A eqA `{equ : Equivalence A eqA} (R : relation A) := + antisymmetry : forall {x y}, R x y -> R y x -> eqA x y. + +Program Definition flip_antiSymmetric `(Antisymmetric A eqA R) : + Antisymmetric A eqA (flip R). +Proof. firstorder. Qed. + +(** Leibinz equality [eq] is an equivalence relation. + The instance has low priority as it is always applicable + if only the type is constrained. *) + +Program Instance eq_equivalence : Equivalence (@eq A) | 10. + +(** Logical equivalence [iff] is an equivalence relation. *) + +Program Instance iff_equivalence : Equivalence iff. + +(** We now develop a generalization of results on relations for arbitrary predicates. + The resulting theory can be applied to homogeneous binary relations but also to + arbitrary n-ary predicates. *) + +Local Open Scope list_scope. + +(* Notation " [ ] " := nil : list_scope. *) +(* Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) (at level 1) : list_scope. *) + +(** A compact representation of non-dependent arities, with the codomain singled-out. *) + +Fixpoint arrows (l : list Type) (r : Type) : Type := + match l with + | nil => r + | A :: l' => A -> arrows l' r + end. + +(** We can define abbreviations for operation and relation types based on [arrows]. *) + +Definition unary_operation A := arrows (A::nil) A. +Definition binary_operation A := arrows (A::A::nil) A. +Definition ternary_operation A := arrows (A::A::A::nil) A. + +(** We define n-ary [predicate]s as functions into [Prop]. *) + +Notation predicate l := (arrows l Prop). + +(** Unary predicates, or sets. *) + +Definition unary_predicate A := predicate (A::nil). + +(** Homogeneous binary relations, equivalent to [relation A]. *) + +Definition binary_relation A := predicate (A::A::nil). + +(** We can close a predicate by universal or existential quantification. *) + +Fixpoint predicate_all (l : list Type) : predicate l -> Prop := + match l with + | nil => fun f => f + | A :: tl => fun f => forall x : A, predicate_all tl (f x) + end. + +Fixpoint predicate_exists (l : list Type) : predicate l -> Prop := + match l with + | nil => fun f => f + | A :: tl => fun f => exists x : A, predicate_exists tl (f x) + end. + +(** Pointwise extension of a binary operation on [T] to a binary operation + on functions whose codomain is [T]. + For an operator on [Prop] this lifts the operator to a binary operation. *) + +Fixpoint pointwise_extension {T : Type} (op : binary_operation T) + (l : list Type) : binary_operation (arrows l T) := + match l with + | nil => fun R R' => op R R' + | A :: tl => fun R R' => + fun x => pointwise_extension op tl (R x) (R' x) + end. + +(** Pointwise lifting, equivalent to doing [pointwise_extension] and closing using [predicate_all]. *) + +Fixpoint pointwise_lifting (op : binary_relation Prop) (l : list Type) : binary_relation (predicate l) := + match l with + | nil => fun R R' => op R R' + | A :: tl => fun R R' => + forall x, pointwise_lifting op tl (R x) (R' x) + end. + +(** The n-ary equivalence relation, defined by lifting the 0-ary [iff] relation. *) + +Definition predicate_equivalence {l : list Type} : binary_relation (predicate l) := + pointwise_lifting iff l. + +(** The n-ary implication relation, defined by lifting the 0-ary [impl] relation. *) + +Definition predicate_implication {l : list Type} := + pointwise_lifting impl l. + +(** Notations for pointwise equivalence and implication of predicates. *) + +Infix "<∙>" := predicate_equivalence (at level 95, no associativity) : predicate_scope. +Infix "-∙>" := predicate_implication (at level 70, right associativity) : predicate_scope. + +Open Local Scope predicate_scope. + +(** The pointwise liftings of conjunction and disjunctions. + Note that these are [binary_operation]s, building new relations out of old ones. *) + +Definition predicate_intersection := pointwise_extension and. +Definition predicate_union := pointwise_extension or. + +Infix "/∙\" := predicate_intersection (at level 80, right associativity) : predicate_scope. +Infix "\∙/" := predicate_union (at level 85, right associativity) : predicate_scope. + +(** The always [True] and always [False] predicates. *) + +Fixpoint true_predicate {l : list Type} : predicate l := + match l with + | nil => True + | A :: tl => fun _ => @true_predicate tl + end. + +Fixpoint false_predicate {l : list Type} : predicate l := + match l with + | nil => False + | A :: tl => fun _ => @false_predicate tl + end. + +Notation "∙⊤∙" := true_predicate : predicate_scope. +Notation "∙⊥∙" := false_predicate : predicate_scope. + +(** Predicate equivalence is an equivalence, and predicate implication defines a preorder. *) + +Program Instance predicate_equivalence_equivalence : Equivalence (@predicate_equivalence l). + Next Obligation. + induction l ; firstorder. + Qed. + Next Obligation. + induction l ; firstorder. + Qed. + Next Obligation. + fold pointwise_lifting. + induction l. firstorder. + intros. simpl in *. pose (IHl (x x0) (y x0) (z x0)). + firstorder. + Qed. + +Program Instance predicate_implication_preorder : + PreOrder (@predicate_implication l). + Next Obligation. + induction l ; firstorder. + Qed. + Next Obligation. + induction l. firstorder. + unfold predicate_implication in *. simpl in *. + intro. pose (IHl (x x0) (y x0) (z x0)). firstorder. + Qed. + +(** We define the various operations which define the algebra on binary relations, + from the general ones. *) + +Definition relation_equivalence {A : Type} : relation (relation A) := + @predicate_equivalence (_::_::nil). + +Class subrelation {A:Type} (R R' : relation A) : Prop := + is_subrelation : @predicate_implication (A::A::nil) R R'. + +Implicit Arguments subrelation [[A]]. + +Definition relation_conjunction {A} (R : relation A) (R' : relation A) : relation A := + @predicate_intersection (A::A::nil) R R'. + +Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relation A := + @predicate_union (A::A::nil) R R'. + +(** Relation equivalence is an equivalence, and subrelation defines a partial order. *) + +Set Automatic Introduction. + +Instance relation_equivalence_equivalence (A : Type) : + Equivalence (@relation_equivalence A). +Proof. exact (@predicate_equivalence_equivalence (A::A::nil)). Qed. + +Instance relation_implication_preorder A : PreOrder (@subrelation A). +Proof. exact (@predicate_implication_preorder (A::A::nil)). Qed. + +(** *** Partial Order. + A partial order is a preorder which is additionally antisymmetric. + We give an equivalent definition, up-to an equivalence relation + on the carrier. *) + +Class PartialOrder {A} eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} := + partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (inverse R)). + +(** The equivalence proof is sufficient for proving that [R] must be a morphism + for equivalence (see Morphisms). + It is also sufficient to show that [R] is antisymmetric w.r.t. [eqA] *) + +Instance partial_order_antisym `(PartialOrder A eqA R) : ! Antisymmetric A eqA R. +Proof with auto. + reduce_goal. + pose proof partial_order_equivalence as poe. do 3 red in poe. + apply <- poe. firstorder. +Qed. + +(** The partial order defined by subrelation and relation equivalence. *) + +Program Instance subrelation_partial_order : + ! PartialOrder (relation A) relation_equivalence subrelation. + + Next Obligation. + Proof. + unfold relation_equivalence in *. firstorder. + Qed. + +Typeclasses Opaque arrows predicate_implication predicate_equivalence + relation_equivalence pointwise_lifting. + +(** Rewrite relation on a given support: declares a relation as a rewrite + relation for use by the generalized rewriting tactic. + It helps choosing if a rewrite should be handled + by the generalized or the regular rewriting tactic using leibniz equality. + Users can declare an [RewriteRelation A RA] anywhere to declare default + relations. This is also done automatically by the [Declare Relation A RA] + commands. *) + +Class RewriteRelation {A : Type} (RA : relation A). + +Instance: RewriteRelation impl. +Instance: RewriteRelation iff. +Instance: RewriteRelation (@relation_equivalence A). + +(** Any [Equivalence] declared in the context is automatically considered + a rewrite relation. *) + +Instance equivalence_rewrite_relation `(Equivalence A eqA) : RewriteRelation eqA. + +(** Strict Order *) + +Class StrictOrder {A : Type} (R : relation A) := { + StrictOrder_Irreflexive :> Irreflexive R ; + StrictOrder_Transitive :> Transitive R +}. + +Instance StrictOrder_Asymmetric `(StrictOrder A R) : Asymmetric R. +Proof. firstorder. Qed. + +(** Inversing a [StrictOrder] gives another [StrictOrder] *) + +Lemma StrictOrder_inverse `(StrictOrder A R) : StrictOrder (inverse R). +Proof. firstorder. Qed. + +(** Same for [PartialOrder]. *) + +Lemma PreOrder_inverse `(PreOrder A R) : PreOrder (inverse R). +Proof. firstorder. Qed. + +Hint Extern 3 (StrictOrder (inverse _)) => class_apply StrictOrder_inverse : typeclass_instances. +Hint Extern 3 (PreOrder (inverse _)) => class_apply PreOrder_inverse : typeclass_instances. + +Lemma PartialOrder_inverse `(PartialOrder A eqA R) : PartialOrder eqA (inverse R). +Proof. firstorder. Qed. + +Hint Extern 3 (PartialOrder (inverse _)) => class_apply PartialOrder_inverse : typeclass_instances. |