diff options
Diffstat (limited to 'tests/lexers/coq/example.txt')
| -rw-r--r-- | tests/lexers/coq/example.txt | 5001 |
1 files changed, 5001 insertions, 0 deletions
diff --git a/tests/lexers/coq/example.txt b/tests/lexers/coq/example.txt new file mode 100644 index 00000000..45918832 --- /dev/null +++ b/tests/lexers/coq/example.txt @@ -0,0 +1,5001 @@ +---input--- +(* -*- 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. + +---tokens--- +'(*' Comment +' -' Comment +'*' Comment +'- coding: utf-8 -' Comment +'*' Comment +'- ' Comment +'*)' Comment +'\n' Text + +'(*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*)' Comment +'\n' Text + +'(*' Comment +' v ' Comment +'*' Comment +' The Coq Proof Assistant / The Coq Development Team ' Comment +'*)' Comment +'\n' Text + +'(*' Comment +' <O___,, ' Comment +'*' Comment +' INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 ' Comment +'*)' Comment +'\n' Text + +'(*' Comment +' \\VV/ ' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*)' Comment +'\n' Text + +'(*' Comment +' // ' Comment +'*' Comment +' This file is distributed under the terms of the ' Comment +'*)' Comment +'\n' Text + +'(*' Comment +' ' Comment +'*' Comment +' GNU Lesser General Public License Version 2.1 ' Comment +'*)' Comment +'\n' Text + +'(*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*' Comment +'*)' Comment +'\n\n' Text + +'(*' Comment +'*' Comment +' ' Comment +'*' Comment +' Typeclass-based relations, tactics and standard instances\n\n This is the basic theory needed to formalize morphisms and setoids.\n\n Author: Matthieu Sozeau\n Institution: LRI, CNRS UMR 8623 - University Paris Sud\n' Comment + +'*)' Comment +'\n\n' Text + +'(*' Comment +' $Id: RelationClasses.v 14641 2011-11-06 11:59:10Z herbelin $ ' Comment +'*)' Comment +'\n\n' Text + +'Require' Keyword.Namespace +' ' Text +'Export' Keyword.Namespace +' ' Text +'Coq' Name +'.' Operator +'Classes' Name +'.' Operator +'Init' Name +'.' Operator +'\n' Text + +'Require' Keyword.Namespace +' ' Text +'Import' Keyword.Namespace +' ' Text +'Coq' Name +'.' Operator +'Program' Name +'.' Operator +'Basics' Name +'.' Operator +'\n' Text + +'Require' Keyword.Namespace +' ' Text +'Import' Keyword.Namespace +' ' Text +'Coq' Name +'.' Operator +'Program' Name +'.' Operator +'Tactics' Name +'.' Operator +'\n' Text + +'Require' Keyword.Namespace +' ' Text +'Import' Keyword.Namespace +' ' Text +'Coq' Name +'.' Operator +'Relations' Name +'.' Operator +'Relation_Definitions' Name +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' We allow to unfold the [relation] definition while doing morphism search. ' Comment +'*)' Comment +'\n\n' Text + +'Notation' Keyword.Namespace +' ' Text +'inverse' Name +' ' Text +'R' Name +' ' Text +':=' Operator +' ' Text +'(' Operator +'flip' Name +' ' Text +'(' Operator +'R' Name +':' Operator +'relation' Name +' ' Text +'_' Operator +')' Operator +' ' Text +':' Operator +' ' Text +'relation' Name +' ' Text +'_' Operator +')' Operator +'.' Operator +'\n\n' Text + +'Definition' Keyword.Namespace +' ' Text +'complement' Name +' ' Text +'{' Operator +'A' Name +'}' Operator +' ' Text +'(' Operator +'R' Name +' ' Text +':' Operator +' ' Text +'relation' Name +' ' Text +'A' Name +')' Operator +' ' Text +':' Operator +' ' Text +'relation' Name +' ' Text +'A' Name +' ' Text +':=' Operator +' ' Text +'fun' Keyword +' ' Text +'x' Name +' ' Text +'y' Name +' ' Text +'=>' Operator +' ' Text +'R' Name +' ' Text +'x' Name +' ' Text +'y' Name +' ' Text +'->' Operator +' ' Text +'False' Name +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' Opaque for proof-search. ' Comment +'*)' Comment +'\n' Text + +'Typeclasses' Name +' ' Text +'Opaque' Name +' ' Text +'complement' Name +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' These are convertible. ' Comment +'*)' Comment +'\n\n' Text + +'Lemma' Keyword.Namespace +' ' Text +'complement_inverse' Name +' ' Text +':' Operator +' ' Text +'forall' Keyword +' ' Text +'A' Name +' ' Text +'(' Operator +'R' Name +' ' Text +':' Operator +' ' Text +'relation' Name +' ' Text +'A' Name +')' Operator +',' Operator +' ' Text +'complement' Name +' ' Text +'(' Operator +'inverse' Name +' ' Text +'R' Name +')' Operator +' ' Text +'=' Operator +' ' Text +'inverse' Name +' ' Text +'(' Operator +'complement' Name +' ' Text +'R' Name +')' Operator +'.' Operator +'\n' Text + +'Proof' Keyword.Namespace +'.' Operator +' ' Text +'reflexivity' Keyword.Pseudo +'.' Operator +' ' Text +'Qed' Keyword.Namespace +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' We rebind relations in separate classes to be able to overload each proof. ' Comment +'*)' Comment +'\n\n' Text + +'Set' Keyword.Namespace +' ' Text +'Implicit' Keyword.Namespace +' ' Text +'Arguments' Keyword.Namespace +'.' Operator +'\n' Text + +'Unset' Keyword.Namespace +' ' Text +'Strict' Keyword.Namespace +' ' Text +'Implicit' Keyword.Namespace +'.' Operator +'\n\n' Text + +'Class' Keyword.Namespace +' ' Text +'Reflexive' Name +' ' Text +'{' Operator +'A' Name +'}' Operator +' ' Text +'(' Operator +'R' Name +' ' Text +':' Operator +' ' Text +'relation' Name +' ' Text +'A' Name +')' Operator +' ' Text +':=' Operator +'\n ' Text +'reflexivity' Keyword.Pseudo +' ' Text +':' Operator +' ' Text +'forall' Keyword +' ' Text +'x' Name +',' Operator +' ' Text +'R' Name +' ' Text +'x' Name +' ' Text +'x' Name +'.' Operator +'\n\n' Text + +'Class' Keyword.Namespace +' ' Text +'Irreflexive' Name +' ' Text +'{' Operator +'A' Name +'}' Operator +' ' Text +'(' Operator +'R' Name +' ' Text +':' Operator +' ' Text +'relation' Name +' ' Text +'A' Name +')' Operator +' ' Text +':=' Operator +'\n ' Text +'irreflexivity' Name +' ' Text +':' Operator +' ' Text +'Reflexive' Name +' ' Text +'(' Operator +'complement' Name +' ' Text +'R' Name +')' Operator +'.' Operator +'\n\n' Text + +'Hint' Keyword.Namespace +' ' Text +'Extern' Name +' ' Text +'1' Literal.Number.Integer +' ' Text +'(' Operator +'Reflexive' Name +' ' Text +'(' Operator +'complement' Name +' ' Text +'_' Operator +')' Operator +')' Operator +' ' Text +'=>' Operator +' ' Text +'class_apply' Name +' ' Text +'@' Operator +'irreflexivity' Name +' ' Text +':' Operator +' ' Text +'typeclass_instances' Name +'.' Operator +'\n\n' Text + +'Class' Keyword.Namespace +' ' Text +'Symmetric' Name +' ' Text +'{' Operator +'A' Name +'}' Operator +' ' Text +'(' Operator +'R' Name +' ' Text +':' Operator +' ' Text +'relation' Name +' ' Text +'A' Name +')' Operator +' ' Text +':=' Operator +'\n ' Text +'symmetry' Keyword +' ' Text +':' Operator +' ' Text +'forall' Keyword +' ' Text +'x' Name +' ' Text +'y' Name +',' Operator +' ' Text +'R' Name +' ' Text +'x' Name +' ' Text +'y' Name +' ' Text +'->' Operator +' ' Text +'R' Name +' ' Text +'y' Name +' ' Text +'x' Name +'.' Operator +'\n\n' Text + +'Class' Keyword.Namespace +' ' Text +'Asymmetric' Name +' ' Text +'{' Operator +'A' Name +'}' Operator +' ' Text +'(' Operator +'R' Name +' ' Text +':' Operator +' ' Text +'relation' Name +' ' Text +'A' Name +')' Operator +' ' Text +':=' Operator +'\n ' Text +'asymmetry' Name +' ' Text +':' Operator +' ' Text +'forall' Keyword +' ' Text +'x' Name +' ' Text +'y' Name +',' Operator +' ' Text +'R' Name +' ' Text +'x' Name +' ' Text +'y' Name +' ' Text +'->' Operator +' ' Text +'R' Name +' ' Text +'y' Name +' ' Text +'x' Name +' ' Text +'->' Operator +' ' Text +'False' Name +'.' Operator +'\n\n' Text + +'Class' Keyword.Namespace +' ' Text +'Transitive' Name +' ' Text +'{' Operator +'A' Name +'}' Operator +' ' Text +'(' Operator +'R' Name +' ' Text +':' Operator +' ' Text +'relation' Name +' ' Text +'A' Name +')' Operator +' ' Text +':=' Operator +'\n ' Text +'transitivity' Keyword +' ' Text +':' Operator +' ' Text +'forall' Keyword +' ' Text +'x' Name +' ' Text +'y' Name +' ' Text +'z' Name +',' Operator +' ' Text +'R' Name +' ' Text +'x' Name +' ' Text +'y' Name +' ' Text +'->' Operator +' ' Text +'R' Name +' ' Text +'y' Name +' ' Text +'z' Name +' ' Text +'->' Operator +' ' Text +'R' Name +' ' Text +'x' Name +' ' Text +'z' Name +'.' Operator +'\n\n' Text + +'Hint' Keyword.Namespace +' ' Text +'Resolve' Keyword.Namespace +' ' Text +'@' Operator +'irreflexivity' Name +' ' Text +':' Operator +' ' Text +'ord' Name +'.' Operator +'\n\n' Text + +'Unset' Keyword.Namespace +' ' Text +'Implicit' Keyword.Namespace +' ' Text +'Arguments' Keyword.Namespace +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' A HintDb for relations. ' Comment +'*)' Comment +'\n\n' Text + +'Ltac' Keyword.Namespace +' ' Text +'solve_relation' Name +' ' Text +':=' Operator +'\n ' Text +'match' Keyword +' ' Text +'goal' Name +' ' Text +'with' Keyword +'\n ' Text +'|' Operator +' ' Text +'[' Operator +' ' Text +'|' Operator +'-' Operator +' ' Text +'?' Operator +'R' Name +' ' Text +'?' Operator +'x' Name +' ' Text +'?' Operator +'x' Name +' ' Text +']' Operator +' ' Text +'=>' Operator +' ' Text +'reflexivity' Keyword.Pseudo +'\n ' Text +'|' Operator +' ' Text +'[' Operator +' ' Text +'H' Name +' ' Text +':' Operator +' ' Text +'?' Operator +'R' Name +' ' Text +'?' Operator +'x' Name +' ' Text +'?' Operator +'y' Name +' ' Text +'|' Operator +'-' Operator +' ' Text +'?' Operator +'R' Name +' ' Text +'?' Operator +'y' Name +' ' Text +'?' Operator +'x' Name +' ' Text +']' Operator +' ' Text +'=>' Operator +' ' Text +'symmetry' Keyword +' ' Text +';' Operator +' ' Text +'exact' Keyword.Pseudo +' ' Text +'H' Name +'\n ' Text +'end' Keyword +'.' Operator +'\n\n' Text + +'Hint' Keyword.Namespace +' ' Text +'Extern' Name +' ' Text +'4' Literal.Number.Integer +' ' Text +'=>' Operator +' ' Text +'solve_relation' Name +' ' Text +':' Operator +' ' Text +'relations' Name +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' We can already dualize all these properties. ' Comment +'*)' Comment +'\n\n' Text + +'Generalizable' Name +' ' Text +'Variables' Keyword.Namespace +' ' Text +'A' Name +' ' Text +'B' Name +' ' Text +'C' Name +' ' Text +'D' Name +' ' Text +'R' Name +' ' Text +'S' Name +' ' Text +'T' Name +' ' Text +'U' Name +' ' Text +'l' Name +' ' Text +'eqA' Name +' ' Text +'eqB' Name +' ' Text +'eqC' Name +' ' Text +'eqD' Name +'.' Operator +'\n\n' Text + +'Lemma' Keyword.Namespace +' ' Text +'flip_Reflexive' Name +' ' Text +'`' Operator +'{' Operator +'Reflexive' Name +' ' Text +'A' Name +' ' Text +'R' Name +'}' Operator +' ' Text +':' Operator +' ' Text +'Reflexive' Name +' ' Text +'(' Operator +'flip' Name +' ' Text +'R' Name +')' Operator +'.' Operator +'\n' Text + +'Proof' Keyword.Namespace +'.' Operator +' ' Text +'tauto' Keyword +'.' Operator +' ' Text +'Qed' Keyword.Namespace +'.' Operator +'\n\n' Text + +'Hint' Keyword.Namespace +' ' Text +'Extern' Name +' ' Text +'3' Literal.Number.Integer +' ' Text +'(' Operator +'Reflexive' Name +' ' Text +'(' Operator +'flip' Name +' ' Text +'_' Operator +')' Operator +')' Operator +' ' Text +'=>' Operator +' ' Text +'apply' Keyword +' ' Text +'flip_Reflexive' Name +' ' Text +':' Operator +' ' Text +'typeclass_instances' Name +'.' Operator +'\n\n' Text + +'Program' Name +' ' Text +'Definition' Keyword.Namespace +' ' Text +'flip_Irreflexive' Name +' ' Text +'`' Operator +'(' Operator +'Irreflexive' Name +' ' Text +'A' Name +' ' Text +'R' Name +')' Operator +' ' Text +':' Operator +' ' Text +'Irreflexive' Name +' ' Text +'(' Operator +'flip' Name +' ' Text +'R' Name +')' Operator +' ' Text +':=' Operator +'\n ' Text +'irreflexivity' Name +' ' Text +'(' Operator +'R' Name +':=' Operator +'R' Name +')' Operator +'.' Operator +'\n\n' Text + +'Program' Name +' ' Text +'Definition' Keyword.Namespace +' ' Text +'flip_Symmetric' Name +' ' Text +'`' Operator +'(' Operator +'Symmetric' Name +' ' Text +'A' Name +' ' Text +'R' Name +')' Operator +' ' Text +':' Operator +' ' Text +'Symmetric' Name +' ' Text +'(' Operator +'flip' Name +' ' Text +'R' Name +')' Operator +' ' Text +':=' Operator +'\n ' Text +'fun' Keyword +' ' Text +'x' Name +' ' Text +'y' Name +' ' Text +'H' Name +' ' Text +'=>' Operator +' ' Text +'symmetry' Keyword +' ' Text +'(' Operator +'R' Name +':=' Operator +'R' Name +')' Operator +' ' Text +'H' Name +'.' Operator +'\n\n' Text + +'Program' Name +' ' Text +'Definition' Keyword.Namespace +' ' Text +'flip_Asymmetric' Name +' ' Text +'`' Operator +'(' Operator +'Asymmetric' Name +' ' Text +'A' Name +' ' Text +'R' Name +')' Operator +' ' Text +':' Operator +' ' Text +'Asymmetric' Name +' ' Text +'(' Operator +'flip' Name +' ' Text +'R' Name +')' Operator +' ' Text +':=' Operator +'\n ' Text +'fun' Keyword +' ' Text +'x' Name +' ' Text +'y' Name +' ' Text +'H' Name +' ' Text +"H'" Name +' ' Text +'=>' Operator +' ' Text +'asymmetry' Name +' ' Text +'(' Operator +'R' Name +':=' Operator +'R' Name +')' Operator +' ' Text +'H' Name +' ' Text +"H'" Name +'.' Operator +'\n\n' Text + +'Program' Name +' ' Text +'Definition' Keyword.Namespace +' ' Text +'flip_Transitive' Name +' ' Text +'`' Operator +'(' Operator +'Transitive' Name +' ' Text +'A' Name +' ' Text +'R' Name +')' Operator +' ' Text +':' Operator +' ' Text +'Transitive' Name +' ' Text +'(' Operator +'flip' Name +' ' Text +'R' Name +')' Operator +' ' Text +':=' Operator +'\n ' Text +'fun' Keyword +' ' Text +'x' Name +' ' Text +'y' Name +' ' Text +'z' Name +' ' Text +'H' Name +' ' Text +"H'" Name +' ' Text +'=>' Operator +' ' Text +'transitivity' Keyword +' ' Text +'(' Operator +'R' Name +':=' Operator +'R' Name +')' Operator +' ' Text +"H'" Name +' ' Text +'H' Name +'.' Operator +'\n\n' Text + +'Hint' Keyword.Namespace +' ' Text +'Extern' Name +' ' Text +'3' Literal.Number.Integer +' ' Text +'(' Operator +'Irreflexive' Name +' ' Text +'(' Operator +'flip' Name +' ' Text +'_' Operator +')' Operator +')' Operator +' ' Text +'=>' Operator +' ' Text +'class_apply' Name +' ' Text +'flip_Irreflexive' Name +' ' Text +':' Operator +' ' Text +'typeclass_instances' Name +'.' Operator +'\n' Text + +'Hint' Keyword.Namespace +' ' Text +'Extern' Name +' ' Text +'3' Literal.Number.Integer +' ' Text +'(' Operator +'Symmetric' Name +' ' Text +'(' Operator +'flip' Name +' ' Text +'_' Operator +')' Operator +')' Operator +' ' Text +'=>' Operator +' ' Text +'class_apply' Name +' ' Text +'flip_Symmetric' Name +' ' Text +':' Operator +' ' Text +'typeclass_instances' Name +'.' Operator +'\n' Text + +'Hint' Keyword.Namespace +' ' Text +'Extern' Name +' ' Text +'3' Literal.Number.Integer +' ' Text +'(' Operator +'Asymmetric' Name +' ' Text +'(' Operator +'flip' Name +' ' Text +'_' Operator +')' Operator +')' Operator +' ' Text +'=>' Operator +' ' Text +'class_apply' Name +' ' Text +'flip_Asymmetric' Name +' ' Text +':' Operator +' ' Text +'typeclass_instances' Name +'.' Operator +'\n' Text + +'Hint' Keyword.Namespace +' ' Text +'Extern' Name +' ' Text +'3' Literal.Number.Integer +' ' Text +'(' Operator +'Transitive' Name +' ' Text +'(' Operator +'flip' Name +' ' Text +'_' Operator +')' Operator +')' Operator +' ' Text +'=>' Operator +' ' Text +'class_apply' Name +' ' Text +'flip_Transitive' Name +' ' Text +':' Operator +' ' Text +'typeclass_instances' Name +'.' Operator +'\n\n' Text + +'Definition' Keyword.Namespace +' ' Text +'Reflexive_complement_Irreflexive' Name +' ' Text +'`' Operator +'(' Operator +'Reflexive' Name +' ' Text +'A' Name +' ' Text +'(' Operator +'R' Name +' ' Text +':' Operator +' ' Text +'relation' Name +' ' Text +'A' Name +')' Operator +')' Operator +'\n ' Text +':' Operator +' ' Text +'Irreflexive' Name +' ' Text +'(' Operator +'complement' Name +' ' Text +'R' Name +')' Operator +'.' Operator +'\n' Text + +'Proof' Keyword.Namespace +'.' Operator +' ' Text +'firstorder' Name +'.' Operator +' ' Text +'Qed' Keyword.Namespace +'.' Operator +'\n\n' Text + +'Definition' Keyword.Namespace +' ' Text +'complement_Symmetric' Name +' ' Text +'`' Operator +'(' Operator +'Symmetric' Name +' ' Text +'A' Name +' ' Text +'(' Operator +'R' Name +' ' Text +':' Operator +' ' Text +'relation' Name +' ' Text +'A' Name +')' Operator +')' Operator +' ' Text +':' Operator +' ' Text +'Symmetric' Name +' ' Text +'(' Operator +'complement' Name +' ' Text +'R' Name +')' Operator +'.' Operator +'\n' Text + +'Proof' Keyword.Namespace +'.' Operator +' ' Text +'firstorder' Name +'.' Operator +' ' Text +'Qed' Keyword.Namespace +'.' Operator +'\n\n' Text + +'Hint' Keyword.Namespace +' ' Text +'Extern' Name +' ' Text +'3' Literal.Number.Integer +' ' Text +'(' Operator +'Symmetric' Name +' ' Text +'(' Operator +'complement' Name +' ' Text +'_' Operator +')' Operator +')' Operator +' ' Text +'=>' Operator +' ' Text +'class_apply' Name +' ' Text +'complement_Symmetric' Name +' ' Text +':' Operator +' ' Text +'typeclass_instances' Name +'.' Operator +'\n' Text + +'Hint' Keyword.Namespace +' ' Text +'Extern' Name +' ' Text +'3' Literal.Number.Integer +' ' Text +'(' Operator +'Irreflexive' Name +' ' Text +'(' Operator +'complement' Name +' ' Text +'_' Operator +')' Operator +')' Operator +' ' Text +'=>' Operator +' ' Text +'class_apply' Name +' ' Text +'Reflexive_complement_Irreflexive' Name +' ' Text +':' Operator +' ' Text +'typeclass_instances' Name +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' ' Comment +'*' Comment +' Standard instances. ' Comment +'*)' Comment +'\n\n' Text + +'Ltac' Keyword.Namespace +' ' Text +'reduce_hyp' Name +' ' Text +'H' Name +' ' Text +':=' Operator +'\n ' Text +'match' Keyword +' ' Text +'type' Name +' ' Text +'of' Keyword +' ' Text +'H' Name +' ' Text +'with' Keyword +'\n ' Text +'|' Operator +' ' Text +'context' Name +' ' Text +'[' Operator +' ' Text +'_' Operator +' ' Text +'<->' Operator +' ' Text +'_' Operator +' ' Text +']' Operator +' ' Text +'=>' Operator +' ' Text +'fail' Name +' ' Text +'1' Literal.Number.Integer +'\n ' Text +'|' Operator +' ' Text +'_' Operator +' ' Text +'=>' Operator +' ' Text +'red' Keyword +' ' Text +'in' Keyword +' ' Text +'H' Name +' ' Text +';' Operator +' ' Text +'try' Keyword.Reserved +' ' Text +'reduce_hyp' Name +' ' Text +'H' Name +'\n ' Text +'end' Keyword +'.' Operator +'\n\n' Text + +'Ltac' Keyword.Namespace +' ' Text +'reduce_goal' Name +' ' Text +':=' Operator +'\n ' Text +'match' Keyword +' ' Text +'goal' Name +' ' Text +'with' Keyword +'\n ' Text +'|' Operator +' ' Text +'[' Operator +' ' Text +'|' Operator +'-' Operator +' ' Text +'_' Operator +' ' Text +'<->' Operator +' ' Text +'_' Operator +' ' Text +']' Operator +' ' Text +'=>' Operator +' ' Text +'fail' Name +' ' Text +'1' Literal.Number.Integer +'\n ' Text +'|' Operator +' ' Text +'_' Operator +' ' Text +'=>' Operator +' ' Text +'red' Keyword +' ' Text +';' Operator +' ' Text +'intros' Keyword +' ' Text +';' Operator +' ' Text +'try' Keyword.Reserved +' ' Text +'reduce_goal' Name +'\n ' Text +'end' Keyword +'.' Operator +'\n\n' Text + +'Tactic' Keyword.Namespace +' ' Text +'Notation' Keyword.Namespace +' ' Text +'"' Literal.String.Double +'reduce' Literal.String.Double +'"' Literal.String.Double +' ' Text +'"' Literal.String.Double +'in' Literal.String.Double +'"' Literal.String.Double +' ' Text +'hyp' Name +'(' Operator +'Hid' Name +')' Operator +' ' Text +':=' Operator +' ' Text +'reduce_hyp' Name +' ' Text +'Hid' Name +'.' Operator +'\n\n' Text + +'Ltac' Keyword.Namespace +' ' Text +'reduce' Name +' ' Text +':=' Operator +' ' Text +'reduce_goal' Name +'.' Operator +'\n\n' Text + +'Tactic' Keyword.Namespace +' ' Text +'Notation' Keyword.Namespace +' ' Text +'"' Literal.String.Double +'apply' Literal.String.Double +'"' Literal.String.Double +' ' Text +'"' Literal.String.Double +'*' Literal.String.Double +'"' Literal.String.Double +' ' Text +'constr' Name +'(' Operator +'t' Name +')' Operator +' ' Text +':=' Operator +'\n ' Text +'first' Keyword.Reserved +' ' Text +'[' Operator +' ' Text +'refine' Keyword +' ' Text +'t' Name +' ' Text +'|' Operator +' ' Text +'refine' Keyword +' ' Text +'(' Operator +'t' Name +' ' Text +'_' Operator +')' Operator +' ' Text +'|' Operator +' ' Text +'refine' Keyword +' ' Text +'(' Operator +'t' Name +' ' Text +'_' Operator +' ' Text +'_' Operator +')' Operator +' ' Text +'|' Operator +' ' Text +'refine' Keyword +' ' Text +'(' Operator +'t' Name +' ' Text +'_' Operator +' ' Text +'_' Operator +' ' Text +'_' Operator +')' Operator +' ' Text +'|' Operator +' ' Text +'refine' Keyword +' ' Text +'(' Operator +'t' Name +' ' Text +'_' Operator +' ' Text +'_' Operator +' ' Text +'_' Operator +' ' Text +'_' Operator +')' Operator +' ' Text +'|' Operator +'\n ' Text +'refine' Keyword +' ' Text +'(' Operator +'t' Name +' ' Text +'_' Operator +' ' Text +'_' Operator +' ' Text +'_' Operator +' ' Text +'_' Operator +' ' Text +'_' Operator +')' Operator +' ' Text +'|' Operator +' ' Text +'refine' Keyword +' ' Text +'(' Operator +'t' Name +' ' Text +'_' Operator +' ' Text +'_' Operator +' ' Text +'_' Operator +' ' Text +'_' Operator +' ' Text +'_' Operator +' ' Text +'_' Operator +')' Operator +' ' Text +'|' Operator +' ' Text +'refine' Keyword +' ' Text +'(' Operator +'t' Name +' ' Text +'_' Operator +' ' Text +'_' Operator +' ' Text +'_' Operator +' ' Text +'_' Operator +' ' Text +'_' Operator +' ' Text +'_' Operator +' ' Text +'_' Operator +')' Operator +' ' Text +']' Operator +'.' Operator +'\n\n' Text + +'Ltac' Keyword.Namespace +' ' Text +'simpl_relation' Name +' ' Text +':=' Operator +'\n ' Text +'unfold' Keyword +' ' Text +'flip' Name +',' Operator +' ' Text +'impl' Name +',' Operator +' ' Text +'arrow' Name +' ' Text +';' Operator +' ' Text +'try' Keyword.Reserved +' ' Text +'reduce' Name +' ' Text +';' Operator +' ' Text +'program_simpl' Name +' ' Text +';' Operator +'\n ' Text +'try' Keyword.Reserved +' ' Text +'(' Operator +' ' Text +'solve' Keyword.Pseudo +' ' Text +'[' Operator +' ' Text +'intuition' Keyword +' ' Text +']' Operator +')' Operator +'.' Operator +'\n\n' Text + +'Local' Keyword.Namespace +' ' Text +'Obligation' Name +' ' Text +'Tactic' Keyword.Namespace +' ' Text +':=' Operator +' ' Text +'simpl_relation' Name +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' Logical implication. ' Comment +'*)' Comment +'\n\n' Text + +'Program' Name +' ' Text +'Instance' Keyword.Namespace +' ' Text +'impl_Reflexive' Name +' ' Text +':' Operator +' ' Text +'Reflexive' Name +' ' Text +'impl' Name +'.' Operator +'\n' Text + +'Program' Name +' ' Text +'Instance' Keyword.Namespace +' ' Text +'impl_Transitive' Name +' ' Text +':' Operator +' ' Text +'Transitive' Name +' ' Text +'impl' Name +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' Logical equivalence. ' Comment +'*)' Comment +'\n\n' Text + +'Program' Name +' ' Text +'Instance' Keyword.Namespace +' ' Text +'iff_Reflexive' Name +' ' Text +':' Operator +' ' Text +'Reflexive' Name +' ' Text +'iff' Name +'.' Operator +'\n' Text + +'Program' Name +' ' Text +'Instance' Keyword.Namespace +' ' Text +'iff_Symmetric' Name +' ' Text +':' Operator +' ' Text +'Symmetric' Name +' ' Text +'iff' Name +'.' Operator +'\n' Text + +'Program' Name +' ' Text +'Instance' Keyword.Namespace +' ' Text +'iff_Transitive' Name +' ' Text +':' Operator +' ' Text +'Transitive' Name +' ' Text +'iff' Name +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' Leibniz equality. ' Comment +'*)' Comment +'\n\n' Text + +'Instance' Keyword.Namespace +' ' Text +'eq_Reflexive' Name +' ' Text +'{' Operator +'A' Name +'}' Operator +' ' Text +':' Operator +' ' Text +'Reflexive' Name +' ' Text +'(' Operator +'@' Operator +'eq' Name +' ' Text +'A' Name +')' Operator +' ' Text +':=' Operator +' ' Text +'@' Operator +'eq_refl' Name +' ' Text +'A' Name +'.' Operator +'\n' Text + +'Instance' Keyword.Namespace +' ' Text +'eq_Symmetric' Name +' ' Text +'{' Operator +'A' Name +'}' Operator +' ' Text +':' Operator +' ' Text +'Symmetric' Name +' ' Text +'(' Operator +'@' Operator +'eq' Name +' ' Text +'A' Name +')' Operator +' ' Text +':=' Operator +' ' Text +'@' Operator +'eq_sym' Name +' ' Text +'A' Name +'.' Operator +'\n' Text + +'Instance' Keyword.Namespace +' ' Text +'eq_Transitive' Name +' ' Text +'{' Operator +'A' Name +'}' Operator +' ' Text +':' Operator +' ' Text +'Transitive' Name +' ' Text +'(' Operator +'@' Operator +'eq' Name +' ' Text +'A' Name +')' Operator +' ' Text +':=' Operator +' ' Text +'@' Operator +'eq_trans' Name +' ' Text +'A' Name +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' Various combinations of reflexivity, symmetry and transitivity. ' Comment +'*)' Comment +'\n\n' Text + +'(*' Comment +'*' Comment +' A [PreOrder] is both Reflexive and Transitive. ' Comment +'*)' Comment +'\n\n' Text + +'Class' Keyword.Namespace +' ' Text +'PreOrder' Name +' ' Text +'{' Operator +'A' Name +'}' Operator +' ' Text +'(' Operator +'R' Name +' ' Text +':' Operator +' ' Text +'relation' Name +' ' Text +'A' Name +')' Operator +' ' Text +':' Operator +' ' Text +'Prop' Keyword.Type +' ' Text +':=' Operator +' ' Text +'{' Operator +'\n ' Text +'PreOrder_Reflexive' Name +' ' Text +':>' Operator +' ' Text +'Reflexive' Name +' ' Text +'R' Name +' ' Text +';' Operator +'\n ' Text +'PreOrder_Transitive' Name +' ' Text +':>' Operator +' ' Text +'Transitive' Name +' ' Text +'R' Name +' ' Text +'}' Operator +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' A partial equivalence relation is Symmetric and Transitive. ' Comment +'*)' Comment +'\n\n' Text + +'Class' Keyword.Namespace +' ' Text +'PER' Name +' ' Text +'{' Operator +'A' Name +'}' Operator +' ' Text +'(' Operator +'R' Name +' ' Text +':' Operator +' ' Text +'relation' Name +' ' Text +'A' Name +')' Operator +' ' Text +':' Operator +' ' Text +'Prop' Keyword.Type +' ' Text +':=' Operator +' ' Text +'{' Operator +'\n ' Text +'PER_Symmetric' Name +' ' Text +':>' Operator +' ' Text +'Symmetric' Name +' ' Text +'R' Name +' ' Text +';' Operator +'\n ' Text +'PER_Transitive' Name +' ' Text +':>' Operator +' ' Text +'Transitive' Name +' ' Text +'R' Name +' ' Text +'}' Operator +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' Equivalence relations. ' Comment +'*)' Comment +'\n\n' Text + +'Class' Keyword.Namespace +' ' Text +'Equivalence' Name +' ' Text +'{' Operator +'A' Name +'}' Operator +' ' Text +'(' Operator +'R' Name +' ' Text +':' Operator +' ' Text +'relation' Name +' ' Text +'A' Name +')' Operator +' ' Text +':' Operator +' ' Text +'Prop' Keyword.Type +' ' Text +':=' Operator +' ' Text +'{' Operator +'\n ' Text +'Equivalence_Reflexive' Name +' ' Text +':>' Operator +' ' Text +'Reflexive' Name +' ' Text +'R' Name +' ' Text +';' Operator +'\n ' Text +'Equivalence_Symmetric' Name +' ' Text +':>' Operator +' ' Text +'Symmetric' Name +' ' Text +'R' Name +' ' Text +';' Operator +'\n ' Text +'Equivalence_Transitive' Name +' ' Text +':>' Operator +' ' Text +'Transitive' Name +' ' Text +'R' Name +' ' Text +'}' Operator +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' An Equivalence is a PER plus reflexivity. ' Comment +'*)' Comment +'\n\n' Text + +'Instance' Keyword.Namespace +' ' Text +'Equivalence_PER' Name +' ' Text +'`' Operator +'(' Operator +'Equivalence' Name +' ' Text +'A' Name +' ' Text +'R' Name +')' Operator +' ' Text +':' Operator +' ' Text +'PER' Name +' ' Text +'R' Name +' ' Text +'|' Operator +' ' Text +'10' Literal.Number.Integer +' ' Text +':=' Operator +'\n ' Text +'{' Operator +' ' Text +'PER_Symmetric' Name +' ' Text +':=' Operator +' ' Text +'Equivalence_Symmetric' Name +' ' Text +';' Operator +'\n ' Text +'PER_Transitive' Name +' ' Text +':=' Operator +' ' Text +'Equivalence_Transitive' Name +' ' Text +'}' Operator +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' We can now define antisymmetry w.r.t. an equivalence relation on the carrier. ' Comment +'*)' Comment +'\n\n' Text + +'Class' Keyword.Namespace +' ' Text +'Antisymmetric' Name +' ' Text +'A' Name +' ' Text +'eqA' Name +' ' Text +'`' Operator +'{' Operator +'equ' Name +' ' Text +':' Operator +' ' Text +'Equivalence' Name +' ' Text +'A' Name +' ' Text +'eqA' Name +'}' Operator +' ' Text +'(' Operator +'R' Name +' ' Text +':' Operator +' ' Text +'relation' Name +' ' Text +'A' Name +')' Operator +' ' Text +':=' Operator +'\n ' Text +'antisymmetry' Name +' ' Text +':' Operator +' ' Text +'forall' Keyword +' ' Text +'{' Operator +'x' Name +' ' Text +'y' Name +'}' Operator +',' Operator +' ' Text +'R' Name +' ' Text +'x' Name +' ' Text +'y' Name +' ' Text +'->' Operator +' ' Text +'R' Name +' ' Text +'y' Name +' ' Text +'x' Name +' ' Text +'->' Operator +' ' Text +'eqA' Name +' ' Text +'x' Name +' ' Text +'y' Name +'.' Operator +'\n\n' Text + +'Program' Name +' ' Text +'Definition' Keyword.Namespace +' ' Text +'flip_antiSymmetric' Name +' ' Text +'`' Operator +'(' Operator +'Antisymmetric' Name +' ' Text +'A' Name +' ' Text +'eqA' Name +' ' Text +'R' Name +')' Operator +' ' Text +':' Operator +'\n ' Text +'Antisymmetric' Name +' ' Text +'A' Name +' ' Text +'eqA' Name +' ' Text +'(' Operator +'flip' Name +' ' Text +'R' Name +')' Operator +'.' Operator +'\n' Text + +'Proof' Keyword.Namespace +'.' Operator +' ' Text +'firstorder' Name +'.' Operator +' ' Text +'Qed' Keyword.Namespace +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' Leibinz equality [eq] is an equivalence relation.\n The instance has low priority as it is always applicable\n if only the type is constrained. ' Comment +'*)' Comment +'\n\n' Text + +'Program' Name +' ' Text +'Instance' Keyword.Namespace +' ' Text +'eq_equivalence' Name +' ' Text +':' Operator +' ' Text +'Equivalence' Name +' ' Text +'(' Operator +'@' Operator +'eq' Name +' ' Text +'A' Name +')' Operator +' ' Text +'|' Operator +' ' Text +'10' Literal.Number.Integer +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' Logical equivalence [iff] is an equivalence relation. ' Comment +'*)' Comment +'\n\n' Text + +'Program' Name +' ' Text +'Instance' Keyword.Namespace +' ' Text +'iff_equivalence' Name +' ' Text +':' Operator +' ' Text +'Equivalence' Name +' ' Text +'iff' Name +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' We now develop a generalization of results on relations for arbitrary predicates.\n The resulting theory can be applied to homogeneous binary relations but also to\n arbitrary n-ary predicates. ' Comment +'*)' Comment +'\n\n' Text + +'Local' Keyword.Namespace +' ' Text +'Open' Keyword.Namespace +' ' Text +'Scope' Keyword.Namespace +' ' Text +'list_scope' Name +'.' Operator +'\n\n' Text + +'(*' Comment +' Notation " [ ] " := nil : list_scope. ' Comment +'*)' Comment +'\n' Text + +'(*' Comment +' Notation " [ x ; .. ; y ] " := ' Comment +'(' Comment +'cons x .. ' Comment +'(' Comment +'cons y nil' Comment +')' Comment +' ..' Comment +')' Comment +' ' Comment +'(' Comment +'at level 1' Comment +')' Comment +' : list_scope. ' Comment +'*)' Comment +'\n\n' Text + +'(*' Comment +'*' Comment +' A compact representation of non-dependent arities, with the codomain singled-out. ' Comment +'*)' Comment +'\n\n' Text + +'Fixpoint' Keyword.Namespace +' ' Text +'arrows' Name +' ' Text +'(' Operator +'l' Name +' ' Text +':' Operator +' ' Text +'list' Name +' ' Text +'Type' Keyword.Type +')' Operator +' ' Text +'(' Operator +'r' Name +' ' Text +':' Operator +' ' Text +'Type' Keyword.Type +')' Operator +' ' Text +':' Operator +' ' Text +'Type' Keyword.Type +' ' Text +':=' Operator +'\n ' Text +'match' Keyword +' ' Text +'l' Name +' ' Text +'with' Keyword +'\n ' Text +'|' Operator +' ' Text +'nil' Name +' ' Text +'=>' Operator +' ' Text +'r' Name +'\n ' Text +'|' Operator +' ' Text +'A' Name +' ' Text +'::' Operator +' ' Text +"l'" Name +' ' Text +'=>' Operator +' ' Text +'A' Name +' ' Text +'->' Operator +' ' Text +'arrows' Name +' ' Text +"l'" Name +' ' Text +'r' Name +'\n ' Text +'end' Keyword +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' We can define abbreviations for operation and relation types based on [arrows]. ' Comment +'*)' Comment +'\n\n' Text + +'Definition' Keyword.Namespace +' ' Text +'unary_operation' Name +' ' Text +'A' Name +' ' Text +':=' Operator +' ' Text +'arrows' Name +' ' Text +'(' Operator +'A' Name +'::' Operator +'nil' Name +')' Operator +' ' Text +'A' Name +'.' Operator +'\n' Text + +'Definition' Keyword.Namespace +' ' Text +'binary_operation' Name +' ' Text +'A' Name +' ' Text +':=' Operator +' ' Text +'arrows' Name +' ' Text +'(' Operator +'A' Name +'::' Operator +'A' Name +'::' Operator +'nil' Name +')' Operator +' ' Text +'A' Name +'.' Operator +'\n' Text + +'Definition' Keyword.Namespace +' ' Text +'ternary_operation' Name +' ' Text +'A' Name +' ' Text +':=' Operator +' ' Text +'arrows' Name +' ' Text +'(' Operator +'A' Name +'::' Operator +'A' Name +'::' Operator +'A' Name +'::' Operator +'nil' Name +')' Operator +' ' Text +'A' Name +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' We define n-ary [predicate]s as functions into [Prop]. ' Comment +'*)' Comment +'\n\n' Text + +'Notation' Keyword.Namespace +' ' Text +'predicate' Name +' ' Text +'l' Name +' ' Text +':=' Operator +' ' Text +'(' Operator +'arrows' Name +' ' Text +'l' Name +' ' Text +'Prop' Keyword.Type +')' Operator +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' Unary predicates, or sets. ' Comment +'*)' Comment +'\n\n' Text + +'Definition' Keyword.Namespace +' ' Text +'unary_predicate' Name +' ' Text +'A' Name +' ' Text +':=' Operator +' ' Text +'predicate' Name +' ' Text +'(' Operator +'A' Name +'::' Operator +'nil' Name +')' Operator +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' Homogeneous binary relations, equivalent to [relation A]. ' Comment +'*)' Comment +'\n\n' Text + +'Definition' Keyword.Namespace +' ' Text +'binary_relation' Name +' ' Text +'A' Name +' ' Text +':=' Operator +' ' Text +'predicate' Name +' ' Text +'(' Operator +'A' Name +'::' Operator +'A' Name +'::' Operator +'nil' Name +')' Operator +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' We can close a predicate by universal or existential quantification. ' Comment +'*)' Comment +'\n\n' Text + +'Fixpoint' Keyword.Namespace +' ' Text +'predicate_all' Name +' ' Text +'(' Operator +'l' Name +' ' Text +':' Operator +' ' Text +'list' Name +' ' Text +'Type' Keyword.Type +')' Operator +' ' Text +':' Operator +' ' Text +'predicate' Name +' ' Text +'l' Name +' ' Text +'->' Operator +' ' Text +'Prop' Keyword.Type +' ' Text +':=' Operator +'\n ' Text +'match' Keyword +' ' Text +'l' Name +' ' Text +'with' Keyword +'\n ' Text +'|' Operator +' ' Text +'nil' Name +' ' Text +'=>' Operator +' ' Text +'fun' Keyword +' ' Text +'f' Name +' ' Text +'=>' Operator +' ' Text +'f' Name +'\n ' Text +'|' Operator +' ' Text +'A' Name +' ' Text +'::' Operator +' ' Text +'tl' Name +' ' Text +'=>' Operator +' ' Text +'fun' Keyword +' ' Text +'f' Name +' ' Text +'=>' Operator +' ' Text +'forall' Keyword +' ' Text +'x' Name +' ' Text +':' Operator +' ' Text +'A' Name +',' Operator +' ' Text +'predicate_all' Name +' ' Text +'tl' Name +' ' Text +'(' Operator +'f' Name +' ' Text +'x' Name +')' Operator +'\n ' Text +'end' Keyword +'.' Operator +'\n\n' Text + +'Fixpoint' Keyword.Namespace +' ' Text +'predicate_exists' Name +' ' Text +'(' Operator +'l' Name +' ' Text +':' Operator +' ' Text +'list' Name +' ' Text +'Type' Keyword.Type +')' Operator +' ' Text +':' Operator +' ' Text +'predicate' Name +' ' Text +'l' Name +' ' Text +'->' Operator +' ' Text +'Prop' Keyword.Type +' ' Text +':=' Operator +'\n ' Text +'match' Keyword +' ' Text +'l' Name +' ' Text +'with' Keyword +'\n ' Text +'|' Operator +' ' Text +'nil' Name +' ' Text +'=>' Operator +' ' Text +'fun' Keyword +' ' Text +'f' Name +' ' Text +'=>' Operator +' ' Text +'f' Name +'\n ' Text +'|' Operator +' ' Text +'A' Name +' ' Text +'::' Operator +' ' Text +'tl' Name +' ' Text +'=>' Operator +' ' Text +'fun' Keyword +' ' Text +'f' Name +' ' Text +'=>' Operator +' ' Text +'exists' Keyword +' ' Text +'x' Name +' ' Text +':' Operator +' ' Text +'A' Name +',' Operator +' ' Text +'predicate_exists' Name +' ' Text +'tl' Name +' ' Text +'(' Operator +'f' Name +' ' Text +'x' Name +')' Operator +'\n ' Text +'end' Keyword +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' Pointwise extension of a binary operation on [T] to a binary operation\n on functions whose codomain is [T].\n For an operator on [Prop] this lifts the operator to a binary operation. ' Comment +'*)' Comment +'\n\n' Text + +'Fixpoint' Keyword.Namespace +' ' Text +'pointwise_extension' Name +' ' Text +'{' Operator +'T' Name +' ' Text +':' Operator +' ' Text +'Type' Keyword.Type +'}' Operator +' ' Text +'(' Operator +'op' Name +' ' Text +':' Operator +' ' Text +'binary_operation' Name +' ' Text +'T' Name +')' Operator +'\n ' Text +'(' Operator +'l' Name +' ' Text +':' Operator +' ' Text +'list' Name +' ' Text +'Type' Keyword.Type +')' Operator +' ' Text +':' Operator +' ' Text +'binary_operation' Name +' ' Text +'(' Operator +'arrows' Name +' ' Text +'l' Name +' ' Text +'T' Name +')' Operator +' ' Text +':=' Operator +'\n ' Text +'match' Keyword +' ' Text +'l' Name +' ' Text +'with' Keyword +'\n ' Text +'|' Operator +' ' Text +'nil' Name +' ' Text +'=>' Operator +' ' Text +'fun' Keyword +' ' Text +'R' Name +' ' Text +"R'" Name +' ' Text +'=>' Operator +' ' Text +'op' Name +' ' Text +'R' Name +' ' Text +"R'" Name +'\n ' Text +'|' Operator +' ' Text +'A' Name +' ' Text +'::' Operator +' ' Text +'tl' Name +' ' Text +'=>' Operator +' ' Text +'fun' Keyword +' ' Text +'R' Name +' ' Text +"R'" Name +' ' Text +'=>' Operator +'\n ' Text +'fun' Keyword +' ' Text +'x' Name +' ' Text +'=>' Operator +' ' Text +'pointwise_extension' Name +' ' Text +'op' Name +' ' Text +'tl' Name +' ' Text +'(' Operator +'R' Name +' ' Text +'x' Name +')' Operator +' ' Text +'(' Operator +"R'" Name +' ' Text +'x' Name +')' Operator +'\n ' Text +'end' Keyword +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' Pointwise lifting, equivalent to doing [pointwise_extension] and closing using [predicate_all]. ' Comment +'*)' Comment +'\n\n' Text + +'Fixpoint' Keyword.Namespace +' ' Text +'pointwise_lifting' Name +' ' Text +'(' Operator +'op' Name +' ' Text +':' Operator +' ' Text +'binary_relation' Name +' ' Text +'Prop' Keyword.Type +')' Operator +' ' Text +'(' Operator +'l' Name +' ' Text +':' Operator +' ' Text +'list' Name +' ' Text +'Type' Keyword.Type +')' Operator +' ' Text +':' Operator +' ' Text +'binary_relation' Name +' ' Text +'(' Operator +'predicate' Name +' ' Text +'l' Name +')' Operator +' ' Text +':=' Operator +'\n ' Text +'match' Keyword +' ' Text +'l' Name +' ' Text +'with' Keyword +'\n ' Text +'|' Operator +' ' Text +'nil' Name +' ' Text +'=>' Operator +' ' Text +'fun' Keyword +' ' Text +'R' Name +' ' Text +"R'" Name +' ' Text +'=>' Operator +' ' Text +'op' Name +' ' Text +'R' Name +' ' Text +"R'" Name +'\n ' Text +'|' Operator +' ' Text +'A' Name +' ' Text +'::' Operator +' ' Text +'tl' Name +' ' Text +'=>' Operator +' ' Text +'fun' Keyword +' ' Text +'R' Name +' ' Text +"R'" Name +' ' Text +'=>' Operator +'\n ' Text +'forall' Keyword +' ' Text +'x' Name +',' Operator +' ' Text +'pointwise_lifting' Name +' ' Text +'op' Name +' ' Text +'tl' Name +' ' Text +'(' Operator +'R' Name +' ' Text +'x' Name +')' Operator +' ' Text +'(' Operator +"R'" Name +' ' Text +'x' Name +')' Operator +'\n ' Text +'end' Keyword +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' The n-ary equivalence relation, defined by lifting the 0-ary [iff] relation. ' Comment +'*)' Comment +'\n\n' Text + +'Definition' Keyword.Namespace +' ' Text +'predicate_equivalence' Name +' ' Text +'{' Operator +'l' Name +' ' Text +':' Operator +' ' Text +'list' Name +' ' Text +'Type' Keyword.Type +'}' Operator +' ' Text +':' Operator +' ' Text +'binary_relation' Name +' ' Text +'(' Operator +'predicate' Name +' ' Text +'l' Name +')' Operator +' ' Text +':=' Operator +'\n ' Text +'pointwise_lifting' Name +' ' Text +'iff' Name +' ' Text +'l' Name +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' The n-ary implication relation, defined by lifting the 0-ary [impl] relation. ' Comment +'*)' Comment +'\n\n' Text + +'Definition' Keyword.Namespace +' ' Text +'predicate_implication' Name +' ' Text +'{' Operator +'l' Name +' ' Text +':' Operator +' ' Text +'list' Name +' ' Text +'Type' Keyword.Type +'}' Operator +' ' Text +':=' Operator +'\n ' Text +'pointwise_lifting' Name +' ' Text +'impl' Name +' ' Text +'l' Name +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' Notations for pointwise equivalence and implication of predicates. ' Comment +'*)' Comment +'\n\n' Text + +'Infix' Name +' ' Text +'"' Literal.String.Double +'<∙>' Literal.String.Double +'"' Literal.String.Double +' ' Text +':=' Operator +' ' Text +'predicate_equivalence' Name +' ' Text +'(' Operator +'at' Name +' ' Text +'level' Name +' ' Text +'95' Literal.Number.Integer +',' Operator +' ' Text +'no' Name +' ' Text +'associativity' Name +')' Operator +' ' Text +':' Operator +' ' Text +'predicate_scope' Name +'.' Operator +'\n' Text + +'Infix' Name +' ' Text +'"' Literal.String.Double +'-∙>' Literal.String.Double +'"' Literal.String.Double +' ' Text +':=' Operator +' ' Text +'predicate_implication' Name +' ' Text +'(' Operator +'at' Name +' ' Text +'level' Name +' ' Text +'70' Literal.Number.Integer +',' Operator +' ' Text +'right' Keyword +' ' Text +'associativity' Name +')' Operator +' ' Text +':' Operator +' ' Text +'predicate_scope' Name +'.' Operator +'\n\n' Text + +'Open' Keyword.Namespace +' ' Text +'Local' Keyword.Namespace +' ' Text +'Scope' Keyword.Namespace +' ' Text +'predicate_scope' Name +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' The pointwise liftings of conjunction and disjunctions.\n Note that these are [binary_operation]s, building new relations out of old ones. ' Comment +'*)' Comment +'\n\n' Text + +'Definition' Keyword.Namespace +' ' Text +'predicate_intersection' Name +' ' Text +':=' Operator +' ' Text +'pointwise_extension' Name +' ' Text +'and' Name +'.' Operator +'\n' Text + +'Definition' Keyword.Namespace +' ' Text +'predicate_union' Name +' ' Text +':=' Operator +' ' Text +'pointwise_extension' Name +' ' Text +'or' Name +'.' Operator +'\n\n' Text + +'Infix' Name +' ' Text +'"' Literal.String.Double +'/∙\\' Literal.String.Double +'"' Literal.String.Double +' ' Text +':=' Operator +' ' Text +'predicate_intersection' Name +' ' Text +'(' Operator +'at' Name +' ' Text +'level' Name +' ' Text +'80' Literal.Number.Integer +',' Operator +' ' Text +'right' Keyword +' ' Text +'associativity' Name +')' Operator +' ' Text +':' Operator +' ' Text +'predicate_scope' Name +'.' Operator +'\n' Text + +'Infix' Name +' ' Text +'"' Literal.String.Double +'\\∙/' Literal.String.Double +'"' Literal.String.Double +' ' Text +':=' Operator +' ' Text +'predicate_union' Name +' ' Text +'(' Operator +'at' Name +' ' Text +'level' Name +' ' Text +'85' Literal.Number.Integer +',' Operator +' ' Text +'right' Keyword +' ' Text +'associativity' Name +')' Operator +' ' Text +':' Operator +' ' Text +'predicate_scope' Name +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' The always [True] and always [False] predicates. ' Comment +'*)' Comment +'\n\n' Text + +'Fixpoint' Keyword.Namespace +' ' Text +'true' Name.Builtin.Pseudo +'_' Operator +'predicate' Name +' ' Text +'{' Operator +'l' Name +' ' Text +':' Operator +' ' Text +'list' Name +' ' Text +'Type' Keyword.Type +'}' Operator +' ' Text +':' Operator +' ' Text +'predicate' Name +' ' Text +'l' Name +' ' Text +':=' Operator +'\n ' Text +'match' Keyword +' ' Text +'l' Name +' ' Text +'with' Keyword +'\n ' Text +'|' Operator +' ' Text +'nil' Name +' ' Text +'=>' Operator +' ' Text +'True' Name +'\n ' Text +'|' Operator +' ' Text +'A' Name +' ' Text +'::' Operator +' ' Text +'tl' Name +' ' Text +'=>' Operator +' ' Text +'fun' Keyword +' ' Text +'_' Operator +' ' Text +'=>' Operator +' ' Text +'@' Operator +'true' Name.Builtin.Pseudo +'_' Operator +'predicate' Name +' ' Text +'tl' Name +'\n ' Text +'end' Keyword +'.' Operator +'\n\n' Text + +'Fixpoint' Keyword.Namespace +' ' Text +'false' Name.Builtin.Pseudo +'_' Operator +'predicate' Name +' ' Text +'{' Operator +'l' Name +' ' Text +':' Operator +' ' Text +'list' Name +' ' Text +'Type' Keyword.Type +'}' Operator +' ' Text +':' Operator +' ' Text +'predicate' Name +' ' Text +'l' Name +' ' Text +':=' Operator +'\n ' Text +'match' Keyword +' ' Text +'l' Name +' ' Text +'with' Keyword +'\n ' Text +'|' Operator +' ' Text +'nil' Name +' ' Text +'=>' Operator +' ' Text +'False' Name +'\n ' Text +'|' Operator +' ' Text +'A' Name +' ' Text +'::' Operator +' ' Text +'tl' Name +' ' Text +'=>' Operator +' ' Text +'fun' Keyword +' ' Text +'_' Operator +' ' Text +'=>' Operator +' ' Text +'@' Operator +'false' Name.Builtin.Pseudo +'_' Operator +'predicate' Name +' ' Text +'tl' Name +'\n ' Text +'end' Keyword +'.' Operator +'\n\n' Text + +'Notation' Keyword.Namespace +' ' Text +'"' Literal.String.Double +'∙⊤∙' Literal.String.Double +'"' Literal.String.Double +' ' Text +':=' Operator +' ' Text +'true' Name.Builtin.Pseudo +'_' Operator +'predicate' Name +' ' Text +':' Operator +' ' Text +'predicate_scope' Name +'.' Operator +'\n' Text + +'Notation' Keyword.Namespace +' ' Text +'"' Literal.String.Double +'∙⊥∙' Literal.String.Double +'"' Literal.String.Double +' ' Text +':=' Operator +' ' Text +'false' Name.Builtin.Pseudo +'_' Operator +'predicate' Name +' ' Text +':' Operator +' ' Text +'predicate_scope' Name +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' Predicate equivalence is an equivalence, and predicate implication defines a preorder. ' Comment +'*)' Comment +'\n\n' Text + +'Program' Name +' ' Text +'Instance' Keyword.Namespace +' ' Text +'predicate_equivalence_equivalence' Name +' ' Text +':' Operator +' ' Text +'Equivalence' Name +' ' Text +'(' Operator +'@' Operator +'predicate_equivalence' Name +' ' Text +'l' Name +')' Operator +'.' Operator +'\n ' Text +'Next' Name +' ' Text +'Obligation' Name +'.' Operator +'\n ' Text +'induction' Keyword +' ' Text +'l' Name +' ' Text +';' Operator +' ' Text +'firstorder' Name +'.' Operator +'\n ' Text +'Qed' Keyword.Namespace +'.' Operator +'\n ' Text +'Next' Name +' ' Text +'Obligation' Name +'.' Operator +'\n ' Text +'induction' Keyword +' ' Text +'l' Name +' ' Text +';' Operator +' ' Text +'firstorder' Name +'.' Operator +'\n ' Text +'Qed' Keyword.Namespace +'.' Operator +'\n ' Text +'Next' Name +' ' Text +'Obligation' Name +'.' Operator +'\n ' Text +'fold' Keyword +' ' Text +'pointwise_lifting' Name +'.' Operator +'\n ' Text +'induction' Keyword +' ' Text +'l' Name +'.' Operator +' ' Text +'firstorder' Name +'.' Operator +'\n ' Text +'intros' Keyword +'.' Operator +' ' Text +'simpl' Keyword +' ' Text +'in' Keyword +' ' Text +'*' Operator +'.' Operator +' ' Text +'pose' Keyword +' ' Text +'(' Operator +'IHl' Name +' ' Text +'(' Operator +'x' Name +' ' Text +'x0' Name +')' Operator +' ' Text +'(' Operator +'y' Name +' ' Text +'x0' Name +')' Operator +' ' Text +'(' Operator +'z' Name +' ' Text +'x0' Name +')' Operator +')' Operator +'.' Operator +'\n ' Text +'firstorder' Name +'.' Operator +'\n ' Text +'Qed' Keyword.Namespace +'.' Operator +'\n\n' Text + +'Program' Name +' ' Text +'Instance' Keyword.Namespace +' ' Text +'predicate_implication_preorder' Name +' ' Text +':' Operator +'\n ' Text +'PreOrder' Name +' ' Text +'(' Operator +'@' Operator +'predicate_implication' Name +' ' Text +'l' Name +')' Operator +'.' Operator +'\n ' Text +'Next' Name +' ' Text +'Obligation' Name +'.' Operator +'\n ' Text +'induction' Keyword +' ' Text +'l' Name +' ' Text +';' Operator +' ' Text +'firstorder' Name +'.' Operator +'\n ' Text +'Qed' Keyword.Namespace +'.' Operator +'\n ' Text +'Next' Name +' ' Text +'Obligation' Name +'.' Operator +'\n ' Text +'induction' Keyword +' ' Text +'l' Name +'.' Operator +' ' Text +'firstorder' Name +'.' Operator +'\n ' Text +'unfold' Keyword +' ' Text +'predicate_implication' Name +' ' Text +'in' Keyword +' ' Text +'*' Operator +'.' Operator +' ' Text +'simpl' Keyword +' ' Text +'in' Keyword +' ' Text +'*' Operator +'.' Operator +'\n ' Text +'intro' Keyword +'.' Operator +' ' Text +'pose' Keyword +' ' Text +'(' Operator +'IHl' Name +' ' Text +'(' Operator +'x' Name +' ' Text +'x0' Name +')' Operator +' ' Text +'(' Operator +'y' Name +' ' Text +'x0' Name +')' Operator +' ' Text +'(' Operator +'z' Name +' ' Text +'x0' Name +')' Operator +')' Operator +'.' Operator +' ' Text +'firstorder' Name +'.' Operator +'\n ' Text +'Qed' Keyword.Namespace +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' We define the various operations which define the algebra on binary relations,\n from the general ones. ' Comment +'*)' Comment +'\n\n' Text + +'Definition' Keyword.Namespace +' ' Text +'relation_equivalence' Name +' ' Text +'{' Operator +'A' Name +' ' Text +':' Operator +' ' Text +'Type' Keyword.Type +'}' Operator +' ' Text +':' Operator +' ' Text +'relation' Name +' ' Text +'(' Operator +'relation' Name +' ' Text +'A' Name +')' Operator +' ' Text +':=' Operator +'\n ' Text +'@' Operator +'predicate_equivalence' Name +' ' Text +'(' Operator +'_' Operator +'::' Operator +'_' Operator +'::' Operator +'nil' Name +')' Operator +'.' Operator +'\n\n' Text + +'Class' Keyword.Namespace +' ' Text +'subrelation' Name +' ' Text +'{' Operator +'A' Name +':' Operator +'Type' Keyword.Type +'}' Operator +' ' Text +'(' Operator +'R' Name +' ' Text +"R'" Name +' ' Text +':' Operator +' ' Text +'relation' Name +' ' Text +'A' Name +')' Operator +' ' Text +':' Operator +' ' Text +'Prop' Keyword.Type +' ' Text +':=' Operator +'\n ' Text +'is_subrelation' Name +' ' Text +':' Operator +' ' Text +'@' Operator +'predicate_implication' Name +' ' Text +'(' Operator +'A' Name +'::' Operator +'A' Name +'::' Operator +'nil' Name +')' Operator +' ' Text +'R' Name +' ' Text +"R'" Name +'.' Operator +'\n\n' Text + +'Implicit' Keyword.Namespace +' ' Text +'Arguments' Keyword.Namespace +' ' Text +'subrelation' Name +' ' Text +'[' Operator +'[' Operator +'A' Name +']' Operator +']' Operator +'.' Operator +'\n\n' Text + +'Definition' Keyword.Namespace +' ' Text +'relation_conjunction' Name +' ' Text +'{' Operator +'A' Name +'}' Operator +' ' Text +'(' Operator +'R' Name +' ' Text +':' Operator +' ' Text +'relation' Name +' ' Text +'A' Name +')' Operator +' ' Text +'(' Operator +"R'" Name +' ' Text +':' Operator +' ' Text +'relation' Name +' ' Text +'A' Name +')' Operator +' ' Text +':' Operator +' ' Text +'relation' Name +' ' Text +'A' Name +' ' Text +':=' Operator +'\n ' Text +'@' Operator +'predicate_intersection' Name +' ' Text +'(' Operator +'A' Name +'::' Operator +'A' Name +'::' Operator +'nil' Name +')' Operator +' ' Text +'R' Name +' ' Text +"R'" Name +'.' Operator +'\n\n' Text + +'Definition' Keyword.Namespace +' ' Text +'relation_disjunction' Name +' ' Text +'{' Operator +'A' Name +'}' Operator +' ' Text +'(' Operator +'R' Name +' ' Text +':' Operator +' ' Text +'relation' Name +' ' Text +'A' Name +')' Operator +' ' Text +'(' Operator +"R'" Name +' ' Text +':' Operator +' ' Text +'relation' Name +' ' Text +'A' Name +')' Operator +' ' Text +':' Operator +' ' Text +'relation' Name +' ' Text +'A' Name +' ' Text +':=' Operator +'\n ' Text +'@' Operator +'predicate_union' Name +' ' Text +'(' Operator +'A' Name +'::' Operator +'A' Name +'::' Operator +'nil' Name +')' Operator +' ' Text +'R' Name +' ' Text +"R'" Name +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' Relation equivalence is an equivalence, and subrelation defines a partial order. ' Comment +'*)' Comment +'\n\n' Text + +'Set' Keyword.Namespace +' ' Text +'Automatic' Name +' ' Text +'Introduction' Name +'.' Operator +'\n\n' Text + +'Instance' Keyword.Namespace +' ' Text +'relation_equivalence_equivalence' Name +' ' Text +'(' Operator +'A' Name +' ' Text +':' Operator +' ' Text +'Type' Keyword.Type +')' Operator +' ' Text +':' Operator +'\n ' Text +'Equivalence' Name +' ' Text +'(' Operator +'@' Operator +'relation_equivalence' Name +' ' Text +'A' Name +')' Operator +'.' Operator +'\n' Text + +'Proof' Keyword.Namespace +'.' Operator +' ' Text +'exact' Keyword.Pseudo +' ' Text +'(' Operator +'@' Operator +'predicate_equivalence_equivalence' Name +' ' Text +'(' Operator +'A' Name +'::' Operator +'A' Name +'::' Operator +'nil' Name +')' Operator +')' Operator +'.' Operator +' ' Text +'Qed' Keyword.Namespace +'.' Operator +'\n\n' Text + +'Instance' Keyword.Namespace +' ' Text +'relation_implication_preorder' Name +' ' Text +'A' Name +' ' Text +':' Operator +' ' Text +'PreOrder' Name +' ' Text +'(' Operator +'@' Operator +'subrelation' Name +' ' Text +'A' Name +')' Operator +'.' Operator +'\n' Text + +'Proof' Keyword.Namespace +'.' Operator +' ' Text +'exact' Keyword.Pseudo +' ' Text +'(' Operator +'@' Operator +'predicate_implication_preorder' Name +' ' Text +'(' Operator +'A' Name +'::' Operator +'A' Name +'::' Operator +'nil' Name +')' Operator +')' Operator +'.' Operator +' ' Text +'Qed' Keyword.Namespace +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' ' Comment +'*' Comment +'*' Comment +'*' Comment +' Partial Order.\n A partial order is a preorder which is additionally antisymmetric.\n We give an equivalent definition, up-to an equivalence relation\n on the carrier. ' Comment +'*)' Comment +'\n\n' Text + +'Class' Keyword.Namespace +' ' Text +'PartialOrder' Name +' ' Text +'{' Operator +'A' Name +'}' Operator +' ' Text +'eqA' Name +' ' Text +'`' Operator +'{' Operator +'equ' Name +' ' Text +':' Operator +' ' Text +'Equivalence' Name +' ' Text +'A' Name +' ' Text +'eqA' Name +'}' Operator +' ' Text +'R' Name +' ' Text +'`' Operator +'{' Operator +'preo' Name +' ' Text +':' Operator +' ' Text +'PreOrder' Name +' ' Text +'A' Name +' ' Text +'R' Name +'}' Operator +' ' Text +':=' Operator +'\n ' Text +'partial_order_equivalence' Name +' ' Text +':' Operator +' ' Text +'relation_equivalence' Name +' ' Text +'eqA' Name +' ' Text +'(' Operator +'relation_conjunction' Name +' ' Text +'R' Name +' ' Text +'(' Operator +'inverse' Name +' ' Text +'R' Name +')' Operator +')' Operator +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' The equivalence proof is sufficient for proving that [R] must be a morphism\n for equivalence ' Comment +'(' Comment +'see Morphisms' Comment +')' Comment +'.\n It is also sufficient to show that [R] is antisymmetric w.r.t. [eqA] ' Comment +'*)' Comment +'\n\n' Text + +'Instance' Keyword.Namespace +' ' Text +'partial_order_antisym' Name +' ' Text +'`' Operator +'(' Operator +'PartialOrder' Name +' ' Text +'A' Name +' ' Text +'eqA' Name +' ' Text +'R' Name +')' Operator +' ' Text +':' Operator +' ' Text +'!' Operator +' ' Text +'Antisymmetric' Name +' ' Text +'A' Name +' ' Text +'eqA' Name +' ' Text +'R' Name +'.' Operator +'\n' Text + +'Proof' Keyword.Namespace +' ' Text +'with' Keyword +' ' Text +'auto' Keyword +'.' Operator +'\n ' Text +'reduce_goal' Name +'.' Operator +'\n ' Text +'pose' Keyword +' ' Text +'proof' Name +' ' Text +'partial_order_equivalence' Name +' ' Text +'as' Keyword +' ' Text +'poe' Name +'.' Operator +' ' Text +'do' Keyword.Reserved +' ' Text +'3' Literal.Number.Integer +' ' Text +'red' Keyword +' ' Text +'in' Keyword +' ' Text +'poe' Name +'.' Operator +'\n ' Text +'apply' Keyword +' ' Text +'<-' Operator +' ' Text +'poe' Name +'.' Operator +' ' Text +'firstorder' Name +'.' Operator +'\n' Text + +'Qed' Keyword.Namespace +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' The partial order defined by subrelation and relation equivalence. ' Comment +'*)' Comment +'\n\n' Text + +'Program' Name +' ' Text +'Instance' Keyword.Namespace +' ' Text +'subrelation_partial_order' Name +' ' Text +':' Operator +'\n ' Text +'!' Operator +' ' Text +'PartialOrder' Name +' ' Text +'(' Operator +'relation' Name +' ' Text +'A' Name +')' Operator +' ' Text +'relation_equivalence' Name +' ' Text +'subrelation' Name +'.' Operator +'\n\n ' Text +'Next' Name +' ' Text +'Obligation' Name +'.' Operator +'\n ' Text +'Proof' Keyword.Namespace +'.' Operator +'\n ' Text +'unfold' Keyword +' ' Text +'relation_equivalence' Name +' ' Text +'in' Keyword +' ' Text +'*' Operator +'.' Operator +' ' Text +'firstorder' Name +'.' Operator +'\n ' Text +'Qed' Keyword.Namespace +'.' Operator +'\n\n' Text + +'Typeclasses' Name +' ' Text +'Opaque' Name +' ' Text +'arrows' Name +' ' Text +'predicate_implication' Name +' ' Text +'predicate_equivalence' Name +'\n ' Text +'relation_equivalence' Name +' ' Text +'pointwise_lifting' Name +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' Rewrite relation on a given support: declares a relation as a rewrite\n relation for use by the generalized rewriting tactic.\n It helps choosing if a rewrite should be handled\n by the generalized or the regular rewriting tactic using leibniz equality.\n Users can declare an [RewriteRelation A RA] anywhere to declare default\n relations. This is also done automatically by the [Declare Relation A RA]\n commands. ' Comment +'*)' Comment +'\n\n' Text + +'Class' Keyword.Namespace +' ' Text +'RewriteRelation' Name +' ' Text +'{' Operator +'A' Name +' ' Text +':' Operator +' ' Text +'Type' Keyword.Type +'}' Operator +' ' Text +'(' Operator +'RA' Name +' ' Text +':' Operator +' ' Text +'relation' Name +' ' Text +'A' Name +')' Operator +'.' Operator +'\n\n' Text + +'Instance' Keyword.Namespace +':' Operator +' ' Text +'RewriteRelation' Name +' ' Text +'impl' Name +'.' Operator +'\n' Text + +'Instance' Keyword.Namespace +':' Operator +' ' Text +'RewriteRelation' Name +' ' Text +'iff' Name +'.' Operator +'\n' Text + +'Instance' Keyword.Namespace +':' Operator +' ' Text +'RewriteRelation' Name +' ' Text +'(' Operator +'@' Operator +'relation_equivalence' Name +' ' Text +'A' Name +')' Operator +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' Any [Equivalence] declared in the context is automatically considered\n a rewrite relation. ' Comment +'*)' Comment +'\n\n' Text + +'Instance' Keyword.Namespace +' ' Text +'equivalence_rewrite_relation' Name +' ' Text +'`' Operator +'(' Operator +'Equivalence' Name +' ' Text +'A' Name +' ' Text +'eqA' Name +')' Operator +' ' Text +':' Operator +' ' Text +'RewriteRelation' Name +' ' Text +'eqA' Name +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' Strict Order ' Comment +'*)' Comment +'\n\n' Text + +'Class' Keyword.Namespace +' ' Text +'StrictOrder' Name +' ' Text +'{' Operator +'A' Name +' ' Text +':' Operator +' ' Text +'Type' Keyword.Type +'}' Operator +' ' Text +'(' Operator +'R' Name +' ' Text +':' Operator +' ' Text +'relation' Name +' ' Text +'A' Name +')' Operator +' ' Text +':=' Operator +' ' Text +'{' Operator +'\n ' Text +'StrictOrder_Irreflexive' Name +' ' Text +':>' Operator +' ' Text +'Irreflexive' Name +' ' Text +'R' Name +' ' Text +';' Operator +'\n ' Text +'StrictOrder_Transitive' Name +' ' Text +':>' Operator +' ' Text +'Transitive' Name +' ' Text +'R' Name +'\n' Text + +'}' Operator +'.' Operator +'\n\n' Text + +'Instance' Keyword.Namespace +' ' Text +'StrictOrder_Asymmetric' Name +' ' Text +'`' Operator +'(' Operator +'StrictOrder' Name +' ' Text +'A' Name +' ' Text +'R' Name +')' Operator +' ' Text +':' Operator +' ' Text +'Asymmetric' Name +' ' Text +'R' Name +'.' Operator +'\n' Text + +'Proof' Keyword.Namespace +'.' Operator +' ' Text +'firstorder' Name +'.' Operator +' ' Text +'Qed' Keyword.Namespace +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' Inversing a [StrictOrder] gives another [StrictOrder] ' Comment +'*)' Comment +'\n\n' Text + +'Lemma' Keyword.Namespace +' ' Text +'StrictOrder_inverse' Name +' ' Text +'`' Operator +'(' Operator +'StrictOrder' Name +' ' Text +'A' Name +' ' Text +'R' Name +')' Operator +' ' Text +':' Operator +' ' Text +'StrictOrder' Name +' ' Text +'(' Operator +'inverse' Name +' ' Text +'R' Name +')' Operator +'.' Operator +'\n' Text + +'Proof' Keyword.Namespace +'.' Operator +' ' Text +'firstorder' Name +'.' Operator +' ' Text +'Qed' Keyword.Namespace +'.' Operator +'\n\n' Text + +'(*' Comment +'*' Comment +' Same for [PartialOrder]. ' Comment +'*)' Comment +'\n\n' Text + +'Lemma' Keyword.Namespace +' ' Text +'PreOrder_inverse' Name +' ' Text +'`' Operator +'(' Operator +'PreOrder' Name +' ' Text +'A' Name +' ' Text +'R' Name +')' Operator +' ' Text +':' Operator +' ' Text +'PreOrder' Name +' ' Text +'(' Operator +'inverse' Name +' ' Text +'R' Name +')' Operator +'.' Operator +'\n' Text + +'Proof' Keyword.Namespace +'.' Operator +' ' Text +'firstorder' Name +'.' Operator +' ' Text +'Qed' Keyword.Namespace +'.' Operator +'\n\n' Text + +'Hint' Keyword.Namespace +' ' Text +'Extern' Name +' ' Text +'3' Literal.Number.Integer +' ' Text +'(' Operator +'StrictOrder' Name +' ' Text +'(' Operator +'inverse' Name +' ' Text +'_' Operator +')' Operator +')' Operator +' ' Text +'=>' Operator +' ' Text +'class_apply' Name +' ' Text +'StrictOrder_inverse' Name +' ' Text +':' Operator +' ' Text +'typeclass_instances' Name +'.' Operator +'\n' Text + +'Hint' Keyword.Namespace +' ' Text +'Extern' Name +' ' Text +'3' Literal.Number.Integer +' ' Text +'(' Operator +'PreOrder' Name +' ' Text +'(' Operator +'inverse' Name +' ' Text +'_' Operator +')' Operator +')' Operator +' ' Text +'=>' Operator +' ' Text +'class_apply' Name +' ' Text +'PreOrder_inverse' Name +' ' Text +':' Operator +' ' Text +'typeclass_instances' Name +'.' Operator +'\n\n' Text + +'Lemma' Keyword.Namespace +' ' Text +'PartialOrder_inverse' Name +' ' Text +'`' Operator +'(' Operator +'PartialOrder' Name +' ' Text +'A' Name +' ' Text +'eqA' Name +' ' Text +'R' Name +')' Operator +' ' Text +':' Operator +' ' Text +'PartialOrder' Name +' ' Text +'eqA' Name +' ' Text +'(' Operator +'inverse' Name +' ' Text +'R' Name +')' Operator +'.' Operator +'\n' Text + +'Proof' Keyword.Namespace +'.' Operator +' ' Text +'firstorder' Name +'.' Operator +' ' Text +'Qed' Keyword.Namespace +'.' Operator +'\n\n' Text + +'Hint' Keyword.Namespace +' ' Text +'Extern' Name +' ' Text +'3' Literal.Number.Integer +' ' Text +'(' Operator +'PartialOrder' Name +' ' Text +'(' Operator +'inverse' Name +' ' Text +'_' Operator +')' Operator +')' Operator +' ' Text +'=>' Operator +' ' Text +'class_apply' Name +' ' Text +'PartialOrder_inverse' Name +' ' Text +':' Operator +' ' Text +'typeclass_instances' Name +'.' Operator +'\n' Text |