diff --git a/.vscode/settings.json b/.vscode/settings.json index 8427b3d80..dc57bf116 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -27,7 +27,6 @@ "src/coq_elpi_vernacular_syntax.ml": true, "**/Makefile.coq": true, "**/Makefile.coq.conf": true, - "**/.merlin": true }, "restructuredtext.confPath": "${workspaceFolder}/alectryon/recipes/sphinx", "ocaml.server.args": [ diff --git a/Makefile b/Makefile index 8adfefa18..8c91fd0ab 100644 --- a/Makefile +++ b/Makefile @@ -21,7 +21,7 @@ export ELPIDIR DEPS=$(ELPIDIR)/elpi.cmxa $(ELPIDIR)/elpi.cma -APPS=$(addprefix apps/, derive eltac NES locker coercion) +APPS=$(addprefix apps/, derive eltac NES locker coercion tc) ifeq "$(COQ_ELPI_ALREADY_INSTALLED)" "" DOCDEP=build diff --git a/_CoqProject b/_CoqProject index 1e0d91b72..37e5a23c2 100644 --- a/_CoqProject +++ b/_CoqProject @@ -18,6 +18,12 @@ -R apps/eltac/tests elpi.apps.eltac.tests -R apps/eltac/examples elpi.apps.eltac.examples -R apps/coercion/theories elpi.apps.coercion +-R apps/coercion/theories elpi.apps.coercion +-R apps/coercion/tests elpi.apps.tc.coercion +-R apps/coercion/elpi elpi.apps.coercion +-R apps/tc/theories elpi.apps.tc +-R apps/tc/tests elpi.apps.tc.tests +-R apps/tc/elpi elpi.apps.tc theories/elpi.v theories/wip/memoization.v diff --git a/apps/tc/Makefile b/apps/tc/Makefile new file mode 100644 index 000000000..9b84ee407 --- /dev/null +++ b/apps/tc/Makefile @@ -0,0 +1,40 @@ +# detection of coq +ifeq "$(COQBIN)" "" +COQBIN := $(shell which coqc >/dev/null 2>&1 && dirname `which coqc`) +endif +ifeq "$(COQBIN)" "" +$(error Coq not found, make sure it is installed in your PATH or set COQBIN) +else +$(info Using coq found in $(COQBIN), from COQBIN or PATH) +endif +export COQBIN := $(COQBIN)/ + +all: build test + +build: Makefile.coq + @$(MAKE) --no-print-directory -f Makefile.coq + +test: Makefile.test.coq + @$(MAKE) --no-print-directory -f Makefile.test.coq + +theories/%.vo: force + @$(MAKE) --no-print-directory -f Makefile.coq $@ +tests/%.vo: force build Makefile.test.coq + @$(MAKE) --no-print-directory -f Makefile.test.coq $@ +examples/%.vo: force build Makefile.test.coq + @$(MAKE) --no-print-directory -f Makefile.test.coq $@ + +Makefile.coq Makefile.coq.conf: _CoqProject + @$(COQBIN)/coq_makefile -f _CoqProject -o Makefile.coq + @$(MAKE) --no-print-directory -f Makefile.coq .merlin +Makefile.test.coq Makefile.test.coq.conf: _CoqProject.test + @$(COQBIN)/coq_makefile -f _CoqProject.test -o Makefile.test.coq + +clean: Makefile.coq Makefile.test.coq + @$(MAKE) -f Makefile.coq $@ + @$(MAKE) -f Makefile.test.coq $@ + +.PHONY: force all build test + +install: + @$(MAKE) -f Makefile.coq $@ diff --git a/apps/tc/Makefile.coq.local b/apps/tc/Makefile.coq.local new file mode 100644 index 000000000..eabb28219 --- /dev/null +++ b/apps/tc/Makefile.coq.local @@ -0,0 +1,19 @@ +CAMLPKGS+= -package coq-elpi.elpi +OCAMLPATH:=../../src/:$(OCAMLPATH) +export OCAMLPATH + +# detection of elpi +ifeq "$(ELPIDIR)" "" +ELPIDIR=$(shell ocamlfind query elpi 2>/dev/null) +endif +ifeq "$(ELPIDIR)" "" +$(error Elpi not found, make sure it is installed in your PATH or set ELPIDIR) +endif +export ELPIDIR + +merlin-hook:: + echo "S $(abspath $(ELPIDIR))" >> .merlin + echo "B $(abspath $(ELPIDIR))" >> .merlin + if [ "$(ELPIDIR)" != "elpi/findlib/elpi" ]; then\ + echo "PKG elpi" >> .merlin;\ + fi \ No newline at end of file diff --git a/apps/tc/_CoqProject b/apps/tc/_CoqProject new file mode 100644 index 000000000..1e009a732 --- /dev/null +++ b/apps/tc/_CoqProject @@ -0,0 +1,16 @@ +# Hack to see Coq-Elpi even if it is not installed yet +-Q ../../theories elpi +-I ../../src +-docroot elpi.apps + +-R theories elpi.apps +-R elpi elpi.apps.tc + +src/coq_elpi_tc_hook.mlg +src/coq_elpi_class_tactics_hacked.ml +src/elpi_tc_plugin.mlpack + +-I src/ +src/META.coq-elpi-tc + +theories/tc.v diff --git a/apps/tc/_CoqProject.test b/apps/tc/_CoqProject.test new file mode 100644 index 000000000..5eab1487e --- /dev/null +++ b/apps/tc/_CoqProject.test @@ -0,0 +1,48 @@ +# Hack to see Coq-Elpi even if it is not installed yet +-Q ../../theories elpi +-I ../../src + +-Q elpi elpi.apps.tc +-R theories elpi.apps +-R tests elpi.apps.tc.tests +-I src + +tests/premisesSort/sortCode.v +tests/premisesSort/sort1.v +# tests/premisesSort/sort2.v +# tests/premisesSort/sort3.v +# tests/premisesSort/sort4.v +tests/included_proof.v +# tests/goalDispatch.v + +# Import order of instances +tests/importOrder/sameOrderCommand.v +tests/importOrder/f1.v +tests/importOrder/f2a.v +tests/importOrder/f2b.v +# tests/importOrder/f3a.v +# tests/importOrder/f3b.v +# tests/importOrder/f3c.v +# tests/importOrder/f3d.v +# tests/importOrder/f3e.v +# tests/importOrder/f3f.v +# tests/importOrder/f3g.v + +tests/nobacktrack.v +tests/removeEta.v +tests/patternFragment.v +tests/contextDeepHierarchy.v +tests/mode_no_repetion.v +# tests/test_commands_API.v +tests/section_in_out.v +tests/eqSimplDef.v +tests/eqSimpl.v + +tests/injTest.v +# Test with light version of base.v of stdpp +tests/stdppInj.v +tests/stdppInjClassic.v +tests/test.v + +# Test with base.v of stdpp +# tests/bigTest.v diff --git a/apps/tc/elpi/alias.elpi b/apps/tc/elpi/alias.elpi new file mode 100644 index 000000000..211d22b72 --- /dev/null +++ b/apps/tc/elpi/alias.elpi @@ -0,0 +1,15 @@ +pred alias i:term, o:term. + +pred replace-with-alias.aux i:list term, o:list term, o:bool. +replace-with-alias.aux [] [] ff. +replace-with-alias.aux [X | Xs] [Y | Ys] B :- + replace-with-alias X Y B', + replace-with-alias.aux Xs Ys B'', + or B' B'' B. + +pred replace-with-alias i:term, o:term, o:bool. +replace-with-alias A Sol tt :- alias A Sol', + replace-with-alias Sol' Sol _. +replace-with-alias (app ToReplace) (app Sol) A :- + replace-with-alias.aux ToReplace Sol A. +replace-with-alias A A ff. \ No newline at end of file diff --git a/apps/tc/elpi/base.elpi b/apps/tc/elpi/base.elpi new file mode 100644 index 000000000..5ccacd310 --- /dev/null +++ b/apps/tc/elpi/base.elpi @@ -0,0 +1,67 @@ +% [count L X R] counts the occurrences of X in L +pred count i:list A, i:A, o:int. +count [] _ 0. +count [A | TL] A R :- count TL A X, R is (X + 1). +count [_ | TL] A R :- count TL A R. + +pred expected-found i:A, i:A. +expected-found Expected Found :- + Expected = Found; + halt "Assertion error" + "\nExpected :" Expected + "\nFound :" Found. + +pred last-no-error i:list A, o:A. +last-no-error A B :- + (std.last [] _ :- !, fail) => std.last A B. + +% [find L F R] returns the first R in L such that (F R) is valid +pred find i:list A, i:(A -> prop), o:A. +find [] _ _ :- std.fatal-error "find element not found". +find [R | _] F R :- F R. +find [_ | L] F R :- find L F R. + +pred find-opt i:list A, i:(A -> prop), o:(option A). +find-opt [] _ none. +find-opt [R | _] F (some R) :- F R. +find-opt [_ | L] F R :- find-opt L F R. + +pred for-loop i:int, i:int, i:(int -> prop). +for-loop A A _. +for-loop A B _ :- A > B, std.fatal-error "first param should be smaller then the sencond one". +for-loop A B F :- F A, for-loop {calc (A + 1)} B F. + +pred list-init i:int, i:(int -> A -> prop), o:list A. +list-init N _ _ :- N < 0, std.fatal-error "list-init negative length". +list-init 0 _ [] :- !. +list-init N F [A | TL] :- + F N A, N1 is N - 1, list-init N1 F TL. + +pred for-loop0 i:int, i:(int -> prop). +for-loop0 B F :- for-loop 0 B F. + +pred args->str-list i:list argument, o: list string. +args->str-list L Res :- + std.map L (x\r\ str r = x) Res. + +pred or i:bool, i:bool, o:bool. +or ff ff ff :- !. +or _ _ tt. + +pred neg i:bool, o:bool. +neg tt ff. +neg ff tt. + +pred fail->bool i:prop, o:bool. +fail->bool P ff :- P, !. +fail->bool _ tt. + +pred sep. +sep :- coq.say "---------------------------------". + +pred do i:list prop. +do []. +do [P|PS] :- P, do PS. + +pred do-once i:prop. +do-once A :- A, !. \ No newline at end of file diff --git a/apps/tc/elpi/compiler.elpi b/apps/tc/elpi/compiler.elpi new file mode 100644 index 000000000..5302000a2 --- /dev/null +++ b/apps/tc/elpi/compiler.elpi @@ -0,0 +1,220 @@ +% returns the classes on which the current gref depends +pred get-sub-classes i:gref, o:list gref. +get-sub-classes GR Res :- + coq.env.dependencies GR _ DepSet, + coq.gref.set.elements DepSet DepList, + std.filter DepList coq.TC.class? Res. + +pred unify-fo i:list name, i:list term, i:list (term -> term), o:term, i:list term, o:term. +unify-fo [Name | Names] [Ty | Tys] [Fun | Funs] (fun Name Ty Fun) [X|Xs] R :- + var R, !, + unify-fo Names Tys Funs (Fun X) Xs R. +unify-fo _ _ _ F L R :- var R, !, coq.mk-app F L R. +unify-fo _ _ _ F L (app R) :- + std.appendR H L R, + if (H = [X]) (F = X) (F = app H). +unify-fo _ _ _ F [] F. + +pred remove-ho-unification i:prop, i:bool, i:int, i:term, i:term, i:list prop, i:list term, i:list name, i:list term, i:list (term -> term), i:list term, i:list prop, o:prop. +:name "remove-ho-unification:start" +remove-ho-unification IsHead IsPositive 0 Ty AppInst Premises [] _ _ _ _ Fixes Clause :- !, + copy Ty Ty1, + copy AppInst AppInst1, + if (IsPositive = tt) + (make-tc IsHead Ty1 AppInst1 {std.append Fixes Premises} Clause) + (make-tc IsHead Ty1 AppInst1 Premises Clause1, std.append Fixes [Clause1] L, Clause = do L). +remove-ho-unification IsHead IsPositive 0 Ty AppInst Premises [(app [X | Y] as G) | TL] Names Types Funs [Gen | GensTL] Fixes P2 :- !, + std.length Y Arity, + std.split-at Arity Types SubTypes TypesTL, + std.split-at Arity Names SubNames NamesTL, + std.split-at Arity Funs SubFuns FunsTL, + P1 = (unify-fo SubNames SubTypes SubFuns X Y Gen), + copy G Gen => + remove-ho-unification IsHead IsPositive 0 Ty AppInst Premises TL NamesTL TypesTL FunsTL GensTL [P1 | Fixes] P2. + +remove-ho-unification IsHead tt N Ty AppInst Premises LT NameL TypeL FunL GenL Fixes (pi ty f name gen\ Clause ty f name gen) :- + N > 0, + N1 is N - 1, + pi name ty f gen\ remove-ho-unification IsHead tt N1 Ty AppInst Premises LT + [name | NameL] [ty | TypeL] [f | FunL] + [gen | GenL] Fixes (Clause ty f name gen). + +remove-ho-unification IsHead ff N Ty AppInst Premises LT NameL TypeL FunL GenL Fixes (sigma ty f name gen\ Clause ty f name gen) :- + N > 0, + N1 is N - 1, + pi name ty f gen\ remove-ho-unification IsHead ff N1 Ty AppInst Premises LT + [name | NameL] [ty | TypeL] [f | FunL] + [gen | GenL] Fixes (Clause ty f name gen). + +pred pattern-fragment? i:term. +pattern-fragment? (app [HD|TL]) :- + not (HD = global _), distinct_names [HD | TL]. + +pred get-pattern-fragment i:term, o:list term. +get-pattern-fragment T1 TL :- !, + (pi L G GL\ fold-map (app L as G) GL G [G | GL] :- distinct_names L) => + % (pi G GL\ fold-map (app _ as G) GL G GL) => + (pi G GL\ fold-map (prod _ _ _ as G) GL G GL) => + fold-map T1 [] _ TL. + +/* +compile-aux [Ty Inst Premises PiAccRev UnivL IsPositive Clause No-Premises] +Ty : the type of the instance +Inst : the instance term on the form (global InstGref) +Premises : list of constraints/premises of an instances found from its type +PiAccRev : the list of pi variables accumulated from the (prod _ _ Bo) of the + type of Inst. The will be used on the solution of the clause + coq.mk-app Inst {std.rev PiAccRev} Sol +UnivL : the list of universes of types inside Ty that are replaced with + a fresh variable to simplify unification +IsPositive : bring the information about the positivity of the current sub-term + e.g. if T = A -> (B -> C) -> D, then: + D is positive in T, (B -> C) is negative, A is positive in T + C is positivie in (B -> C), B is negative in (B -> C) + IsPositive is used to know how to accumulate sigma Xi\ and pi x\ in the + current clause +IsHead : a prop [true|false] to know if we are compiling the head of the + instance or one hypothesis of its premises +Clause : the solution to be returned +No-Premises : a boolean saying if the returned clause as no premises that is an + instance with no hypothesis +*/ +pred compile-aux i:term, i:term, i:list prop, i:list term, i:list univ, i:bool, i:prop, o:prop, o:bool. +:name "compiler-aux:start" +compile-aux Ty I [] [] [X | XS] IsPositive IsHead (pi x\ C x) IsLeaf :- !, + pi x\ copy (sort (typ X)) (sort (typ x)) => copy Ty (Ty1 x), + compile-aux (Ty1 x) I [] [] XS IsPositive IsHead (C x) IsLeaf. +compile-aux (prod N T F) I RevPremises ListVar [] IsPositive IsHead Clause ff :- !, + (if (IsPositive = tt) (Clause = pi x\ C x) (Clause = (pi x\ decl x N T => C x))), + pi p\ sigma NewPremise TC L\ + if (get-TC-of-inst-type T TC, coq.TC.class? TC /*, not (occurs p (F p))*/) + (compile-aux T p [] [] [] {neg IsPositive} false NewPremise _, + if (classes TC deterministic) + (L = [do-once NewPremise | RevPremises]) + (L = [NewPremise | RevPremises])) (L = RevPremises), + compile-aux (F p) I L [p | ListVar] [] IsPositive IsHead (C p) _. +:if "simple-compiler" +compile-aux Ty I RevPremises ListVar [] _ IsHead Clause tt :- !, + std.rev RevPremises RevRHS, + coq.mk-app I {std.rev ListVar} AppInst, + make-tc IsHead Ty AppInst RevRHS Clause. +compile-aux Ty I RevPremises ListVar [] IsPositive IsHead Clause tt :- !, + std.rev RevPremises Premises, + coq.mk-app I {std.rev ListVar} AppInst, + std.append {get-pattern-fragment Ty} {get-pattern-fragment AppInst} Term-to-be-fixed, + std.fold Term-to-be-fixed 0 (e\acc\r\ sigma L X\ e = app X, std.length X L, r is acc + L - 1) Len, + remove-ho-unification IsHead IsPositive Len Ty AppInst Premises Term-to-be-fixed [] [] [] [] [] Clause. + +% build a list of Clauses of type tc to be temporarly added to the +% database, used in theorems having assumptions. +pred compile-ctx i:goal-ctx, o:list prop. +compile-ctx [] []. +compile-ctx [X | Xs] [Clause | ResTl] :- + (decl Var _ Ty = X; def Var _ Ty _ = X), + is-instance-term Ty, + compile-ty Ty Var _ _ Clause, + compile-ctx Xs ResTl. +compile-ctx [_ | Tl] L :- compile-ctx Tl L. + +pred compile-ty i:term, i:term, o:bool, o:gref, o:prop. +compile-ty Ty Inst IsLeaf TC-of-Inst Clause:- + if (get-TC-of-inst-type Ty TC-of-Inst)( + @redflags! coq.redflags.beta => coq.reduction.lazy.norm Ty Ty1, + coq.univ.variable.set.elements {coq.univ.variable.of-term Ty1} L, + std.map L (x\r\ coq.univ.variable r x) L1, + compile-aux Ty1 Inst [] [] L1 tt true Clause IsLeaf) + % (coq.warning "" "" "Adding polymorphic Instance" Inst). + true. + +pred compile i:gref, o:bool, o:gref, o:prop. +compile InstGR IsLeaf TC-of-Inst Clause:- + coq.env.typeof InstGR Ty, + compile-ty Ty (global InstGR) IsLeaf TC-of-Inst Clause. + +% if an instance depends on multiple TC then a warning is raised. +pred warn-multiple-deps i:gref, i:list gref. +warn-multiple-deps Inst Dep :- + if (fail, {std.length Dep} > 1) ( + coq.warning "add-inst-with-multiple-deps" "TC-warning" + "Adding" Inst "which dependes on mulitple class dependencies:" Dep) + true. + +pred has-context-deps i:gref. +has-context-deps GR :- + coq.env.section SectionVars, + coq.env.dependencies GR _ Deps, + std.exists SectionVars (x\ coq.gref.set.mem (const x) Deps). + +% [add-inst->db IgnoreClassDepL Inst] add the Inst to +% the database except those depending on at least one +% inside IgnoreClassDepL +pred is-local. +is-local :- std.mem {attributes} (attribute "local" _). + +pred make-inst-graft i:gref, i:bool, o:grafting. +make-inst-graft Inst _NoPremises (after Grafting) :- + RawGrafting is int_to_string {get-inst-prio Inst}, + % if (NoPremises = tt) (Grafting = RawGrafting) (Grafting is RawGrafting ^ "_complex"). + Grafting = RawGrafting. + +pred add-inst->db i:list gref, i:bool, i:gref. +:name "add-inst->db:start" +add-inst->db IgnoreClassDepL ForceAdd Inst :- + coq.env.current-section-path SectionPath, + get-sub-classes Inst Dep, + warn-multiple-deps Inst Dep, + if ((ForceAdd = tt; not (instance _ Inst _)), + not (std.exists Dep (std.mem IgnoreClassDepL)), not (banned Inst)) + ( + compile Inst IsLeaf TC-of-Inst Clause, + % TODO: a clause is flexible if an instance is polimorphic (pglobal) + not (var Clause), + make-inst-graft Inst IsLeaf Graft, + get-full-path Inst ClauseName, + if (is-local) (Visibility = [@local!]) + (if (has-context-deps Inst) + (@local! => add-tc-db _ Graft (instance SectionPath Inst TC-of-Inst)) + (@global! => add-tc-db _ Graft (instance [] Inst TC-of-Inst)), Visibility = [@global!]), + Visibility => add-tc-db ClauseName Graft Clause + ) + true; @global! => add-tc-db _ _ (banned Inst), + coq.warning "Not-added" "TC_solver" "Warning : Cannot compile " Inst "since it is pglobal". + +pred add-tc i:list gref, i:list gref, i:gref. +add-tc IgnoreDepClassGR IgnoreInstsGR GR:- + % add-modes GR, + get-inst-by-tc-name GR InstL, + std.filter InstL (x\ not (std.mem IgnoreInstsGR x)) InstLF, + std.forall InstLF (add-inst->db IgnoreDepClassGR ff). + +pred add-tc-or-inst-gr i:list string, i:list string, i:list gref. +add-tc-or-inst-gr IgnoreDepClass IgnoreInsts Names :- + std.map IgnoreDepClass coq.locate IgnoreDepClassGR, + std.map IgnoreInsts coq.locate IgnoreInstsGR, + std.forall Names (GR\ + if2 (coq.TC.class? GR)(add-tc IgnoreDepClassGR IgnoreInstsGR GR) + (is-instance-gr GR)(add-inst->db IgnoreDepClassGR ff GR) + (coq.warning "not-inst-nor-tc" "TC-warning" GR "is neither a TC nor a instance") + ). + +% [add-tc-or-inst IgnoreDepClass ClassName] look +% for all the instances of ClassName and call the pred +% add-inst->db +pred add-tc-or-inst i:list string, i:list string, i:list string. +add-tc-or-inst IgnoreDepClass IgnoreInsts Names :- + std.map Names coq.locate L, + add-tc-or-inst-gr IgnoreDepClass IgnoreInsts L. + +% takes a Path and a GR and returns if +% the GR is located in Path +pred is-in-path i:string, i:gref. +is-in-path Path GR :- + std.mem {coq.gref->path GR} Path. + +% Look for the instances of ClassName +% that are located in Path. +pred add-path i:string, i:string. +add-path ClassName Path :- + coq.locate ClassName GR, + std.filter {get-inst-by-tc-name GR} (is-in-path Path) InstInPath, + std.forall InstInPath (add-inst->db [] ff). \ No newline at end of file diff --git a/apps/tc/elpi/create_tc_predicate.elpi b/apps/tc/elpi/create_tc_predicate.elpi new file mode 100644 index 000000000..5a70d4115 --- /dev/null +++ b/apps/tc/elpi/create_tc_predicate.elpi @@ -0,0 +1,50 @@ +pred bool->mode-term i:bool, o:pair argument_mode string. +% TODO: here every mode is declared to O;term. +% If you want to make it work as intended, +% replace the output of tt with "i:term" +:name "bool->mode-term" +bool->mode-term tt (pr in "term"). +bool->mode-term ff (pr out "term"). + +pred modes->string i:list bool, o:list (pair argument_mode string). +modes->string L S :- + std.map L bool->mode-term S. + +pred make-tc-modes i:int, o:list (pair argument_mode string). +make-tc-modes NB_args ModesStr :- + list-init NB_args (x\r\ r = ff) ModesBool, + modes->string ModesBool ModesStr. + +pred add-tc-pred i:search-mode, i:gref, i:int. +add-tc-pred SearchMode Gr NbArgs :- + if (not (coq.TC.class? Gr)) + (halt Gr "is not a typeclass") true, + not (classes Gr _), !, + if ( + coq.option.get ["AddModes"] (coq.option.bool tt), + coq.hints.modes Gr "typeclass_instances" ModesProv, + not (ModesProv = [])) + ( + coq.hints.modes Gr "typeclass_instances" ModesProv, + std.assert! (ModesProv = [HintModes]) "At the moment we only allow TC with one Hint Mode", + std.map {std.append HintModes [mode-output]} (x\r\ if (x = mode-output) (r = ff) (r = tt)) ModesBool, + modes->string ModesBool Modes + ) + (make-tc-modes NbArgs Modes), + gref->string-no-path Gr GrStr, + coq.elpi.add-predicate "tc.db" _ GrStr Modes, + add-tc-db _ _ (tc-mode Gr Modes), + @global! => coq.elpi.accumulate _ "tc.db" (clause _ _ (classes Gr SearchMode)). +add-tc-pred _ _ _. + +pred add-class-gr i:search-mode, i:gref. +add-class-gr SearchMode TC_Gr :- + coq.env.typeof TC_Gr TC_Ty, + coq.count-prods TC_Ty N', + N is N' + 1, % Plus one for the solution + add-tc-pred SearchMode TC_Gr N. + +pred add-class-str i:search-mode, i:string. +add-class-str SearchMode TC_Name :- + coq.locate TC_Name TC_Gr, + add-class-gr SearchMode TC_Gr. \ No newline at end of file diff --git a/apps/tc/elpi/modes.elpi b/apps/tc/elpi/modes.elpi new file mode 100644 index 000000000..56058aa89 --- /dev/null +++ b/apps/tc/elpi/modes.elpi @@ -0,0 +1,42 @@ +% pred make-modes-cl i:gref, i:list term, i:term, i:list (list hint-mode), i:list (list term), o:prop. +% make-modes-cl T V (prod _ _ X) HintModes L (pi x\ C x):- +% std.map HintModes (x\r\ [r|_] = x) FST, +% std.map HintModes (x\r\ [_|r] = x) LAST, +% pi x\ sigma NewL\ +% std.map2 L FST (l\m\r\ if (m = mode-input) (r = [x | l]) (r = l)) NewL, +% make-modes-cl T [x | V] (X x) LAST NewL (C x). +% make-modes-cl T V _ _ L Clause :- +% Ty = {coq.mk-app (global T) {std.rev V}}, +% Clause = (pi s\ tc T Ty s :- std.forall L (x\ std.exists x var), !, coq.error "Invalid mode for" Ty). + +% takes the type of a class and build a list +% of hint mode where the last element is mandatory +pred make-last-hint-mode-input i:term, o:list hint-mode. +make-last-hint-mode-input (prod _ _ (x\ (prod _ _ _) as T)) [mode-output | L] :- + pi x\ make-last-hint-mode-input (T x) L. +make-last-hint-mode-input (prod _ _ _) [mode-input]. +make-last-hint-mode-input (sort _) []. + +% build a list of the seme langht as the the passed one +% where all the elements are [] +pred build-empty-list i:list B, o:list (list A). +build-empty-list [] []. +build-empty-list [_ | TL] [[] | L] :- + build-empty-list TL L. + +% add the hint modes of a Class to the database. +% note that if the Class has not specified hint mode +% then we assume the hint mode to be - - - ... ! +pred add-modes i:gref. +:if "add-modes" +add-modes GR :- + % the hint mode is added only if not exists + if (not (classes GR _)) ( + coq.env.typeof GR Ty, + coq.hints.modes GR "typeclass_instances" ModesProv, + if (ModesProv = []) (Modes = [{make-last-hint-mode-input Ty}]) (Modes = ModesProv), + % make-modes-cl GR [] Ty Modes {build-empty-list Modes} Cl, + % add-tc-db _ (after "firstHook") Cl, + add-tc-db _ _ (classes GR classic) + ) true. +add-modes _. \ No newline at end of file diff --git a/apps/tc/elpi/parser_addInstances.elpi b/apps/tc/elpi/parser_addInstances.elpi new file mode 100644 index 000000000..359e87a27 --- /dev/null +++ b/apps/tc/elpi/parser_addInstances.elpi @@ -0,0 +1,31 @@ +kind enum type. +type path string -> string -> enum. +type addInstPrio int -> string -> enum. +type tcOrInst list string -> enum. +type ignoreInstances, ignoreClasses string -> list string -> enum. + +pred parse i:list argument, o:enum. +parse [str ClassName, str "path", str Path] (path ClassName Path). +parse [str ClassName, str "ignoreInstances" | InstNames] (ignoreInstances ClassName Res) :- + args->str-list InstNames Res. +parse [str ClassName, str "ignoreClasses" | ClassNames] (ignoreClasses ClassName Res) :- + args->str-list ClassNames Res. +parse ClassNames (tcOrInst Res) :- args->str-list ClassNames Res. +parse [int N, str Instance] (addInstPrio N Instance). + +pred run-command i:enum. +:if "debug" +run-command A :- coq.say A, fail. +run-command (ignoreClasses ClassName IgnoreClasses) :- + add-tc-or-inst IgnoreClasses [] [ClassName]. +run-command (tcOrInst InstNames) :- + add-tc-or-inst [] [] InstNames. +run-command (path ClassName Path):- + add-path ClassName Path. +run-command (ignoreInstances ClassName InstNames):- + add-tc-or-inst [] InstNames [ClassName]. +run-command (addInstPrio Prio InstanceName) :- + coq.locate InstanceName InstGr, + compile InstGr _ _ C, + S is int_to_string Prio, + add-tc-db _ (before S) C. \ No newline at end of file diff --git a/apps/tc/elpi/rewrite_forward.elpi b/apps/tc/elpi/rewrite_forward.elpi new file mode 100644 index 000000000..4bf0341c1 --- /dev/null +++ b/apps/tc/elpi/rewrite_forward.elpi @@ -0,0 +1,73 @@ +pred forward i:term, o:term, o:list (pair (list term) term). + +% Auxiliary function for rewrite-forward +pred rewrite-forward->list i:term, i:name, i:prop, o:list prop. +rewrite-forward->list P N (forward _ Lemma RewL) L :- + coq.mk-app Lemma [P] LemmaApp, + % coq.typecheck LemmaApp T ok, + % coq.say T, + std.map RewL (x\r\ sigma ProjL Ty Pr\ + pr ProjL Ty = x, + make-proj-app ProjL LemmaApp Pr, + r = decl Pr N Ty) L. + +% Takes a decl from the context and returns the list of its atomic +% representations by looking in the forward clauses +pred rewrite-forward i:prop, o:list prop. +rewrite-forward (decl P N Ty) L :- + std.findall (forward Ty _ _) FwdL, + std.map FwdL (rewrite-forward->list P N) RewFdw, + std.flatten RewFdw L. +rewrite-forward _ []. + +% Takes a list of projections ([proj1|proj2]*) and a term T +% and returns the coq's term (projX (projY (... (projZ T)))) +% Note that app [Proj, _, _, Rest] has two holes for the types +% of the left and right side of Rest +pred make-proj-app i:list term, i:term, o:term. +make-proj-app [Proj | Projs] T (app [Proj, L, R, Rest]) :- + make-proj-app Projs T Rest, + % TODO: here we do a naive typecheck to get the types L and R of Rest, + % it can be done in a faster way + coq.typecheck Rest {{and lp:L lp:R}} ok. +make-proj-app [] T T. + +% Takes a conjunction C of terms and []. It returns a list of pair: +% The paths to the conjunct c in C and the path to reach it in C +pred rec-split-and i:term, i:(list term), o:list (pair (list term) term). +rec-split-and {{lp:A /\ lp:B}} DL L :- + LEFT = [{{proj1}} | DL], + RIGHT = [{{proj2}} | DL], + rec-split-and A LEFT AL, + rec-split-and B RIGHT BL, + std.append AL BL L. +rec-split-and A P [pr P A]. + +% It takes a rewriting-lemma and abstract it into elpi in a forward +% clause of type forward. The base case wants a ∀(x : T).f x, since +% we want to keep trace of the type T of x. +pred compile-rewrite i:term, i:term, i:list term, o:prop. +compile-rewrite (prod _ Ty ((x\ app _) as Bo)) Lemma L (pi x\ forward Ty LemmaApp (TL x)) :- + pi x\ + coq.mk-app Lemma {std.rev L} LemmaApp, + rec-split-and (Bo x) [] (TL x). +compile-rewrite (prod _ _ Bo) Lemma L (pi x\ C x) :- + pi x\ compile-rewrite (Bo x) Lemma [x | L] (C x). + +% Takes a string (the name of a rewriting-lemma), +% compiles and adds it as a forward clause in tc.db +pred add-lemma->forward i:string. +add-lemma->forward Lemma :- + coq.locate Lemma Gr, + coq.env.typeof Gr Type, + compile-rewrite Type (global Gr) [] Cl, + coq.elpi.accumulate _ "tc.db" (clause Lemma _ Cl). + +% TODO: @FissoreD @gares should make a set in output? +pred rewrite-dep i:list prop, o:list prop. +rewrite-dep [] []. +rewrite-dep [A | B] L :- + rewrite-forward A NewA, not (NewA = []), + std.append NewA B ToTreat, + rewrite-dep ToTreat L. +rewrite-dep [A | TL] [A | L] :- rewrite-dep TL L. \ No newline at end of file diff --git a/apps/tc/elpi/solver.elpi b/apps/tc/elpi/solver.elpi new file mode 100644 index 000000000..64f7f9bf0 --- /dev/null +++ b/apps/tc/elpi/solver.elpi @@ -0,0 +1,105 @@ +msolve L N :- !, + coq.ltac.all (coq.ltac.open solve) {std.rev L} N. + +pred my-refine i:term, i:goal, o:(list sealed-goal). +% :if "time-refine" +my-refine T G GL :- !, std.time( + coq.reduction.eta-contract T T-eta-red, + % T-eta-red = T, + refine T-eta-red G GL) FF, + if (coq.option.get ["TimeRefine"] (coq.option.bool tt)) (coq.say "Refine Time" FF) true. +% my-refine T G GL :- refine T G GL. + +pred tc-search-time i:term, o:term. +tc-search-time Ty X :- !, + std.time (tc Ty X) Time, + if (coq.option.get ["TimeTC"] (coq.option.bool tt)) (coq.say "TC search" Time) true. + +pred build-context-clauses i:list prop, o:list prop. +% Add the section's definition to the given context +% and atomize context hypothesis if needed +build-context-clauses Ctx Clauses :- + std.map {coq.env.section} (x\r\ sigma F\ coq.env.typeof (const x) F, r = (decl (global (const x)) _ F)) SectionCtx, + std.append Ctx SectionCtx CtxAndSection, + compile-ctx {rewrite-dep CtxAndSection} Clauses. + +pred tc i:term, o:term. +tc Ty Sol :- + Ty = app [global TC | TL'], + std.append TL' [Sol] TL, + % replace-with-alias T T' A, !, + % A = tt, tc Gref T' Sol. + coq.elpi.predicate {gref->string-no-path TC} TL Q, Q. + +pred solve1 i:goal, o:(list sealed-goal). +% solve1 (goal C _ (prod N Ty F) S _ as _G) _L GL :- !, +% @pi-decl N Ty x\ +% declare-evar [decl x N Ty|C] (Raw x) (F x) (Sol x), +% solve1 (goal [decl x N Ty|C] (Raw x) (F x) (Sol x) []) _L GL, +% if (Sol x = app [HD, x]) (S = HD) (S = fun N Ty Sol). +% solve1 (goal C _ (prod N Ty F) XX _ as G) _L GL :- !, +% % intros_if_needed Prod C [] +% (@pi-decl N Ty x\ +% declare-evar [decl x N Ty|C] (Raw x) (F x) (Sol x), +% solve1 (goal [decl x N Ty|C] (Raw x) (F x) (Sol x) []) _L _, +% coq.safe-dest-app (Sol x) Hd (Args x)), +% if (pi x\ last-no-error (Args x) x, std.drop-last 1 (Args x) NewArgs) +% (coq.mk-app Hd NewArgs Out, refine Out G GL) ( +% % coq.say "Not eta" (Sol x) x (fun N Ty Sol), +% XX = (fun N Ty Sol)). +% solve1 (goal C _ (prod N _ _ as P) _ A as G) _L GL :- !, +% declare-evar C T P S', +% G' = (goal C T P S' A), +% refine (fun N _ _) G' GL1, +% coq.ltac.all (coq.ltac.open solve) GL1 _, +% refine S' G GL. +solve1 (goal C _ (prod N Ty F) _ _ as G) GL :- !, + (@pi-decl N Ty x\ + declare-evar [decl x N Ty|C] (Raw x) (F x) (Sol x), + solve1 (goal [decl x N Ty|C] (Raw x) (F x) (Sol x) []) _), + if (pi x\ + % also check the head does not contain x + coq.safe-dest-app (Sol x) Hd (Args x), + last-no-error (Args x) x, + std.drop-last 1 (Args x) NewArgs) + (coq.mk-app Hd NewArgs Out, refine Out G GL1) (refine (fun N _ _) G GL1), + coq.ltac.all (coq.ltac.open solve) GL1 GL. +% solve1 (goal _ _ (prod N _ _) _ _ as G) GL :- !, +% refine (fun N _ _) G GL1, +% coq.ltac.all (coq.ltac.open solve) GL1 GL. +solve1 (goal Ctx _ Ty Sol _ as G) GL :- + var Sol, + build-context-clauses Ctx Clauses, + % @redflags! coq.redflags.beta => coq.reduction.lazy.norm Ty Ty1, + Clauses => if (tc-search-time Ty Proof) + ( + % @no-tc! => coq.elaborate-skeleton X _ X' ok, + % coq.say "Solution " X "end" X' "caio", + % std.assert! (ground_term X') "solution not complete", + % (pi F\ (copy (fun _ _ x\ (app [F, x])) F :- !)) => copy X X', + my-refine Proof G GL; + coq.say "illtyped solution:" {coq.term->string Proof} + ) + (GL = [seal G]). + +% In order to have more or less verbosity, +% we use the solve1 predicate to make TC resolution. +% The solve predicate is used to have different Debug behaviors. +:if "solve-print-goal" +solve (goal Ctx _ Ty _ _) _ :- + coq.say "Ctx" Ctx "Ty" Ty, fail. +:if "solve-print-type" +solve (goal _ _ Ty _ _) _ :- + coq.say "Ty" Ty, fail. +:if "solve-trace-time" +solve A B :- !, + std.spy-do! [std.time (solve1 A B) Time, coq.say Time]. +:if "solve-trace" +solve A B :- !, + std.spy-do! [solve1 A B]. +:if "solve-time" +solve A B :- !, + std.time (solve1 A B) Time, coq.say "Time Solve" Time. +solve A B :- solve1 A B. + +main _. \ No newline at end of file diff --git a/apps/tc/elpi/tc_aux.elpi b/apps/tc/elpi/tc_aux.elpi new file mode 100644 index 000000000..b4d3ffac8 --- /dev/null +++ b/apps/tc/elpi/tc_aux.elpi @@ -0,0 +1,135 @@ +% Contains the list of classes that +% cannot be compiled + +% returns the TC from the type of an instance +pred get-TC-of-inst-type i:term, o:gref. +get-TC-of-inst-type (prod _ _ A) GR:- + pi x\ get-TC-of-inst-type (A x) GR. +get-TC-of-inst-type (app [global TC | _]) TC. +get-TC-of-inst-type (global TC) TC. + +pred remove-eta i:term, o:term. +remove-eta A B :- !, + (pi F\ copy (fun _ _ x\ (app [F, x])) F) => copy A B. + +pred drop-last i:list A, i:list A, o:list A. +drop-last [X | XS] [Y | YS] L :- + same_term X Y, !, drop-last XS YS L. +drop-last L [] L' :- std.rev L L'. + +pred remove-eta2.aux i:term, i:list term, o:term. +remove-eta2.aux (app [Hd | L]) V R :- !, std.do! [ + copy Hd Hd', + std.map L copy L', + drop-last {std.rev L'} V F, + coq.mk-app Hd' F R]. + +remove-eta2.aux (fun _ _ Bo) L R :- + pi x\ remove-eta2.aux (Bo x) [x | L] R. + +pred remove-eta2 i:term, o:term. +remove-eta2 A B :- !, + (pi A B\ copy A B :- remove-eta2.aux A [] B) => copy A B. + +pred instances-of-current-section o:list gref. +:name "MySectionEndHook" +instances-of-current-section InstsFiltered :- + coq.env.current-section-path SectionPath, + std.findall (instance SectionPath _ _) Insts, + coq.env.section SectionVars, + std.map-filter Insts (x\r\ sigma X\ instance _ r _ = x, const X = r, not(std.mem SectionVars X)) InstsFiltered. + +pred is-instance-gr i:gref. +is-instance-gr GR :- + coq.env.typeof GR Ty, + is-instance-term Ty. + +pred is-instance-term i:term. +is-instance-term T :- + get-TC-of-inst-type T TC, + coq.TC.class? TC. + +% adds a clause to the tc.db DB at the passed grafting +pred add-tc-db o:id, o:grafting, i:prop. +add-tc-db ClauseName Graft PR :- + coq.elpi.accumulate _ "tc.db" + (clause ClauseName Graft PR); coq.error "cannot add " PR " to tc.db". + +% takes a tc-instance and return the gref of the inst +pred inst->gref i:tc-instance, o:gref. +inst->gref (tc-instance Res _) Res. + +% returns all the instances of the passed ClassName +pred get-inst-by-tc-name i:gref, o:list gref. +get-inst-by-tc-name TC GRL:- + coq.TC.db-for TC Inst, + std.map Inst inst->gref GRL', + std.rev GRL' GRL. + +pred app-has-class i:term. +app-has-class T :- + get-TC-of-inst-type T Hd, + coq.TC.class? Hd. + +% input (∀ a, b, c ... => app [A, B, ..., Last]) +% returns Last +pred get-last i:term, o:term. +get-last (prod _ _ Bo) R :- + pi x\ get-last (Bo x) R. +get-last (app L) R :- + std.last L R. + +% TC preds are on the form tc-[PATH_TO_TC].tc-[TC-Name] +pred gref->string-no-path i:gref, o:string. +gref->string-no-path Gr S :- + if (coq.option.get ["TC_NameFullPath"] (coq.option.bool tt)) + (coq.gref->path Gr [Hd | Tl], + std.fold Tl Hd (x\acc\r\ r is acc ^ "." ^ x) Path', + Path is Path' ^ ".tc-") + (Path = ""), + S is "tc-" ^ Path ^ {coq.gref->id Gr}. + +pred no-backtrack i:list prop, o:list prop. +no-backtrack [] []. +no-backtrack [do X | XS] [std.do! [(std.do! X') | XS']] :- !, + no-backtrack X X', no-backtrack XS XS'. +no-backtrack [X | XS] [std.do! [X | XS']] :- !, no-backtrack XS XS'. + +pred make-tc i:prop, i:term, i:term, i:list prop, o:prop. +make-tc _IsHead Ty Inst Hyp Clause :- + app [global TC | TL] = Ty, + gref->string-no-path TC TC_Str, + std.append TL [Inst] Args, + coq.elpi.predicate TC_Str Args Q, + % if (classes TC deterministic, IsHead) (std.append [!] Hyp Hyp') (Hyp' = Hyp), + if2 (Hyp = []) (Clause = Q) + (Hyp = [Hd]) (Clause = (Q :- Hd)) + (Clause = (Q :- Hyp)). + + +pred get-inst-prio-coq i:term, i:list term, o:int. +get-inst-prio-coq (prod _ _ A) L Prio :- + pi x\ get-inst-prio-coq (A x) [x | L] Prio. +get-inst-prio-coq (app _ as App) L Prio :- + std.fold L 0 (T\acc\r\ if (not(occurs T App)) (r is acc + 1) (r = acc)) Prio. +get-inst-prio-coq A _ _ :- coq.error "Invalid case for" A. + +% returns the priority of an instance from the gref of an instance +pred get-inst-prio i:gref, o:int. +get-inst-prio InstGr Prio :- + coq.env.typeof InstGr InstTy, + get-TC-of-inst-type InstTy TC, + find-opt {coq.TC.db-for TC} + (x\ tc-instance InstGr Prio' = x) (some _), !, + if (Prio' = 0) (get-inst-prio-coq InstTy [] Prio) (Prio = Prio'). +get-inst-prio _ 0. + +% TODO: @FissoreD improve this method complexity +pred get-full-path i:gref, o:string. +% :if "get-full-path" +get-full-path Gr Res' :- + coq.gref->string Gr Path, + coq.env.current-section-path SectionPath, + std.fold SectionPath "" (e\acc\r\ r is acc ^ "." ^ e) Res, + Res' is Res ^ Path. +% get-full-path _ _. \ No newline at end of file diff --git a/apps/tc/src/META.coq-elpi-tc b/apps/tc/src/META.coq-elpi-tc new file mode 100644 index 000000000..5c3045ab8 --- /dev/null +++ b/apps/tc/src/META.coq-elpi-tc @@ -0,0 +1,10 @@ + +package "plugin" ( + directory = "." + requires = "coq-core.plugins.ltac coq-elpi.elpi" + archive(byte) = "elpi_tc_plugin.cma" + archive(native) = "elpi_tc_plugin.cmxa" + plugin(byte) = "elpi_tc_plugin.cma" + plugin(native) = "elpi_tc_plugin.cmxs" +) +directory = "." diff --git a/apps/tc/src/coq_elpi_tc_hook.mlg b/apps/tc/src/coq_elpi_tc_hook.mlg new file mode 100644 index 000000000..09ec0faae --- /dev/null +++ b/apps/tc/src/coq_elpi_tc_hook.mlg @@ -0,0 +1,31 @@ +DECLARE PLUGIN "coq-elpi-tc.plugin" + +{ +open Stdarg +open Elpi_plugin +open Coq_elpi_arg_syntax +open Coq_elpi_class_tactics_hacked + +} + +VERNAC COMMAND EXTEND ElpiTypeclasses CLASSIFIED AS SIDEFF + +| #[ atts = any_attribute ] [ "Elpi" "Override" "TC" qualified_name(p) "All" ] -> { + let () = ignore_unknown_attributes atts in + takeover false [] (snd p) } +| #[ atts = any_attribute ] [ "Elpi" "Override" "TC" qualified_name(p) "None" ] -> { + let () = ignore_unknown_attributes atts in + takeover true [] (snd p) } + + +| #[ atts = any_attribute ] [ "Elpi" "Override" "TC" qualified_name(p) "Only" ne_reference_list(cs) ] -> { + let () = ignore_unknown_attributes atts in + takeover false cs (snd p) } +| #[ atts = any_attribute ] [ "Elpi" "Override" "TC" "+" reference_list(cs) ] -> { + let () = ignore_unknown_attributes atts in + takeover_add cs } +| #[ atts = any_attribute ] [ "Elpi" "Override" "TC" "-" reference_list(cs) ] -> { + let () = ignore_unknown_attributes atts in + takeover_rm cs } + +END \ No newline at end of file diff --git a/apps/tc/src/elpi_tc_plugin.mlpack b/apps/tc/src/elpi_tc_plugin.mlpack new file mode 100644 index 000000000..8aed0b167 --- /dev/null +++ b/apps/tc/src/elpi_tc_plugin.mlpack @@ -0,0 +1,2 @@ +Coq_elpi_class_tactics_hacked +Coq_elpi_tc_hook \ No newline at end of file diff --git a/apps/tc/tests/add_alias.v b/apps/tc/tests/add_alias.v new file mode 100644 index 000000000..e22549d70 --- /dev/null +++ b/apps/tc/tests/add_alias.v @@ -0,0 +1,30 @@ +From elpi.apps Require Import tc. +Elpi Override TC TC_solver All. +Elpi Debug "use-alias". + +Class foo (A : Type) := f : Type. + +Global Instance fooNat : foo nat := {f := nat}. +Global Instance fooBool : foo bool := {f := bool}. + +Elpi AddClasses foo. +Elpi AddInstances foo. + +Definition nat' := nat. + + +Goal foo nat. apply _. Qed. +Goal foo bool. apply _. Qed. +Goal foo nat'. Fail apply _. Abort. + +Module A. + Elpi Accumulate TC_solver lp:{{ + alias {{nat'}} {{nat}}. + }}. + Goal foo nat'. apply _. Qed. +End A. + +Definition nat'' := nat'. + +Elpi AddAlias (nat'') (nat'). +Goal foo nat''. apply _. Qed. diff --git a/apps/tc/tests/bigTest.v b/apps/tc/tests/bigTest.v new file mode 100644 index 000000000..df761c1cb --- /dev/null +++ b/apps/tc/tests/bigTest.v @@ -0,0 +1,1787 @@ +(** This file collects type class interfaces, notations, and general theorems +that are used throughout the whole development. Most importantly it contains +abstract interfaces for ordered structures, sets, and various other data +structures. *) + +(* We want to ensure that [le] and [lt] refer to operations on [nat]. +These two functions being defined both in [Coq.Bool] and in [Coq.Peano], +we must export [Coq.Peano] later than any export of [Coq.Bool]. *) +(* We also want to ensure that notations from [Coq.Utf8] take precedence +over the ones of [Coq.Peano] (see Coq PR#12950), so we import [Utf8] last. *) +From Coq Require Export Morphisms RelationClasses List Bool Setoid Peano Utf8. +From Coq Require Import Permutation. +Export ListNotations. +From Coq.Program Require Export Basics Syntax. +From elpi.apps Require Import tc. + +Set assert_same_generated_TC. +Global Set Warnings "+elpi". + + +(** This notation is necessary to prevent [length] from being printed +as [strings.length] if strings.v is imported and later base.v. See +also strings.v and +https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/144 and +https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/129. *) +Notation length := Datatypes.length. + +(** * Enable implicit generalization. *) +(** This option enables implicit generalization in arguments of the form + [`{...}] (i.e., anonymous arguments). Unfortunately, it also enables + implicit generalization in [Instance]. We think that the fact that both + behaviors are coupled together is a [bug in + Coq](https://github.com/coq/coq/issues/6030). *) +Global Generalizable All Variables. + +Elpi Override TC TC_solver All. + +(** * Tweak program *) +(** 1. Since we only use Program to solve logical side-conditions, they should +always be made Opaque, otherwise we end up with performance problems due to +Coq blindly unfolding them. + +Note that in most cases we use [Next Obligation. (* ... *) Qed.], for which +this option does not matter. However, sometimes we write things like +[Solve Obligations with naive_solver (* ... *)], and then the obligations +should surely be opaque. *) +Global Unset Transparent Obligations. + +(** 2. Do not let Program automatically simplify obligations. The default +obligation tactic is [Tactics.program_simpl], which, among other things, +introduces all variables and gives them fresh names. As such, it becomes +impossible to refer to hypotheses in a robust way. *) +Obligation Tactic := idtac. + +(** 3. Hide obligations and unsealing lemmas from the results of the [Search] +commands. *) +Add Search Blacklist "_obligation_". +Add Search Blacklist "_unseal". + +(** * Sealing off definitions *) +Section seal. + Local Set Primitive Projections. + Record seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }. +MySectionEnd. +Global Arguments unseal {_ _} _ : assert. +Global Arguments seal_eq {_ _} _ : assert. + +(** * Solving type class instances *) +(** The tactic [tc_solve] is used to solve type class goals by invoking type +class search. It is similar to [apply _], but it is more robust since it does +not affect unrelated goals/evars due to https://github.com/coq/coq/issues/6583. + +The tactic [tc_solve] is particularly useful when building custom tactics that +need tight control over when type class search is invoked. In Iris, many of the +proof mode tactics make use of [notypeclasses refine] and use [tc_solve] to +manually invoke type class search. + +Note that [typeclasses eauto] is multi-success. That means, whenever subsequent +tactics fail, it will backtrack to [typeclasses eauto] to try the next type +class instance. This is almost always undesired and can lead to poor performance +and horrible error messages. Hence, we wrap it in a [once]. *) +Ltac tc_solve := + solve [once (typeclasses eauto)]. + +(** * Non-backtracking type classes *) +(** The type class [TCNoBackTrack P] can be used to establish [P] without ever +backtracking on the instance of [P] that has been found. Backtracking may +normally happen when [P] contains evars that could be instanciated in different +ways depending on which instance is picked, and type class search somewhere else +depends on this evar. + +The proper way of handling this would be by setting Coq's option +`Typeclasses Unique Instances`. However, this option seems to be broken, see Coq +issue #6714. + +See https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/112 for a rationale +of this type class. *) +Class TCNoBackTrack (P : Prop) := TCNoBackTrack_intro { tc_no_backtrack : P }. +Global Hint Extern 0 (TCNoBackTrack _) => + notypeclasses refine (TCNoBackTrack_intro _ _); tc_solve : typeclass_instances. + +(* A conditional at the type class level. Note that [TCIf P Q R] is not the same +as [TCOr (TCAnd P Q) R]: the latter will backtrack to [R] if it fails to +establish [Q], i.e. does not have the behavior of a conditional. Furthermore, +note that [TCOr (TCAnd P Q) (TCAnd (TCNot P) R)] would not work; we generally +would not be able to prove the negation of [P]. *) +Inductive TCIf (P Q R : Prop) : Prop := + | TCIf_true : P → Q → TCIf P Q R + | TCIf_false : R → TCIf P Q R. +Existing Class TCIf. + +Global Hint Extern 0 (TCIf _ _ _) => + first [notypeclasses refine (TCIf_true _ _ _ _ _); [tc_solve|] + |notypeclasses refine (TCIf_false _ _ _ _)] : typeclass_instances. + +(** * Typeclass opaque definitions *) +(** The constant [tc_opaque] is used to make definitions opaque for just type +class search. Note that [simpl] is set up to always unfold [tc_opaque]. *) +Definition tc_opaque {A} (x : A) : A := x. +Typeclasses Opaque tc_opaque. +Global Arguments tc_opaque {_} _ /. + +(** Below we define type class versions of the common logical operators. It is +important to note that we duplicate the definitions, and do not declare the +existing logical operators as type classes. That is, we do not say: + + Existing Class or. + Existing Class and. + +If we could define the existing logical operators as classes, there is no way +of disambiguating whether a premise of a lemma should be solved by type class +resolution or not. + +These classes are useful for two purposes: writing complicated type class +premises in a more concise way, and for efficiency. For example, using the [Or] +class, instead of defining two instances [P → Q1 → R] and [P → Q2 → R] we could +have one instance [P → Or Q1 Q2 → R]. When we declare the instance that way, we +avoid the need to derive [P] twice. *) +Inductive TCOr (P1 P2 : Prop) : Prop := + | TCOr_l : P1 → TCOr P1 P2 + | TCOr_r : P2 → TCOr P1 P2. +Existing Class TCOr. +Global Existing Instance TCOr_l | 9. +Global Existing Instance TCOr_r | 10. +Global Hint Mode TCOr ! ! : typeclass_instances. + +Inductive TCAnd (P1 P2 : Prop) : Prop := TCAnd_intro : P1 → P2 → TCAnd P1 P2. +Existing Class TCAnd. +Global Existing Instance TCAnd_intro. +Global Hint Mode TCAnd ! ! : typeclass_instances. + +Inductive TCTrue : Prop := TCTrue_intro : TCTrue. +Existing Class TCTrue. +Global Existing Instance TCTrue_intro. + +(** The class [TCFalse] is not stricly necessary as one could also use +[False]. However, users might expect that TCFalse exists and if it +does not, it can cause hard to diagnose bugs due to automatic +generalization. *) +Inductive TCFalse : Prop :=. +Existing Class TCFalse. + +(** The class [TCUnless] can be used to check that search for [P] +fails. This is useful as a guard for certain instances together with +classes like [TCFastDone] (see [tactics.v]) to prevent infinite loops +(e.g. when saturating the context). *) +Notation TCUnless P := (TCIf P TCFalse TCTrue). + +Inductive TCForall {A} (P : A → Prop) : list A → Prop := + | TCForall_nil : TCForall P [] + | TCForall_cons x xs : P x → TCForall P xs → TCForall P (x :: xs). +Existing Class TCForall. +Global Existing Instance TCForall_nil. +Global Existing Instance TCForall_cons. +Global Hint Mode TCForall ! ! ! : typeclass_instances. + +(** The class [TCForall2 P l k] is commonly used to transform an input list [l] +into an output list [k], or the converse. Therefore there are two modes, either +[l] input and [k] output, or [k] input and [l] input. *) +Inductive TCForall2 {A B} (P : A → B → Prop) : list A → list B → Prop := + | TCForall2_nil : TCForall2 P [] [] + | TCForall2_cons x y xs ys : + P x y → TCForall2 P xs ys → TCForall2 P (x :: xs) (y :: ys). +Existing Class TCForall2. +Global Existing Instance TCForall2_nil. +Global Existing Instance TCForall2_cons. +Global Hint Mode TCForall2 ! ! ! ! - : typeclass_instances. +Global Hint Mode TCForall2 ! ! ! - ! : typeclass_instances. + +Inductive TCExists {A} (P : A → Prop) : list A → Prop := + | TCExists_cons_hd x l : P x → TCExists P (x :: l) + | TCExists_cons_tl x l: TCExists P l → TCExists P (x :: l). +Existing Class TCExists. +Global Existing Instance TCExists_cons_hd | 10. +Global Existing Instance TCExists_cons_tl | 20. +Global Hint Mode TCExists ! ! ! : typeclass_instances. + +Inductive TCElemOf {A} (x : A) : list A → Prop := + | TCElemOf_here xs : TCElemOf x (x :: xs) + | TCElemOf_further y xs : TCElemOf x xs → TCElemOf x (y :: xs). +Existing Class TCElemOf. +Global Existing Instance TCElemOf_here. +Global Existing Instance TCElemOf_further. +Global Hint Mode TCElemOf ! ! ! : typeclass_instances. + +(** We declare both arguments [x] and [y] of [TCEq x y] as outputs, which means +[TCEq] can also be used to unify evars. This is harmless: since the only +instance of [TCEq] is [TCEq_refl] below, it can never cause loops. See +https://gitlab.mpi-sws.org/iris/iris/merge_requests/391 for a use case. *) +Inductive TCEq {A} (x : A) : A → Prop := TCEq_refl : TCEq x x. +Existing Class TCEq. +Global Existing Instance TCEq_refl. +Global Hint Mode TCEq ! - - : typeclass_instances. + +Lemma TCEq_eq {A} (x1 x2 : A) : TCEq x1 x2 ↔ x1 = x2. +Proof. split; destruct 1; reflexivity. Qed. + +Inductive TCDiag {A} (C : A → Prop) : A → A → Prop := + | TCDiag_diag x : C x → TCDiag C x x. +Existing Class TCDiag. +Global Existing Instance TCDiag_diag. +Global Hint Mode TCDiag ! ! ! - : typeclass_instances. +Global Hint Mode TCDiag ! ! - ! : typeclass_instances. + +(** Given a proposition [P] that is a type class, [tc_to_bool P] will return +[true] iff there is an instance of [P]. It is often useful in Ltac programming, +where one can do [lazymatch tc_to_bool P with true => .. | false => .. end]. *) +Definition tc_to_bool (P : Prop) + {p : bool} `{TCIf P (TCEq p true) (TCEq p false)} : bool := p. + +(** Throughout this development we use [stdpp_scope] for all general purpose +notations that do not belong to a more specific scope. *) +Declare Scope stdpp_scope. +Delimit Scope stdpp_scope with stdpp. +Global Open Scope stdpp_scope. + +(** Change [True] and [False] into notations in order to enable overloading. +We will use this to give [True] and [False] a different interpretation for +embedded logics. *) +Notation "'True'" := True (format "True") : type_scope. +Notation "'False'" := False (format "False") : type_scope. + +(** Change [forall] into a notation in order to enable overloading. *) +Notation "'forall' x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity, + only parsing) : type_scope. + + +(** * Equality *) +(** Introduce some Haskell style like notations. *) +Notation "(=)" := eq (only parsing) : stdpp_scope. +Notation "( x =.)" := (eq x) (only parsing) : stdpp_scope. +Notation "(.= x )" := (λ y, eq y x) (only parsing) : stdpp_scope. +Notation "(≠)" := (λ x y, x ≠ y) (only parsing) : stdpp_scope. +Notation "( x ≠.)" := (λ y, x ≠ y) (only parsing) : stdpp_scope. +Notation "(.≠ x )" := (λ y, y ≠ x) (only parsing) : stdpp_scope. + +Infix "=@{ A }" := (@eq A) + (at level 70, only parsing, no associativity) : stdpp_scope. +Notation "(=@{ A } )" := (@eq A) (only parsing) : stdpp_scope. +Notation "(≠@{ A } )" := (λ X Y, ¬X =@{A} Y) (only parsing) : stdpp_scope. +Notation "X ≠@{ A } Y":= (¬X =@{ A } Y) + (at level 70, only parsing, no associativity) : stdpp_scope. + +Global Hint Extern 0 (_ = _) => reflexivity : core. +Global Hint Extern 100 (_ ≠ _) => discriminate : core. + +Global Instance: ∀ A, PreOrder (=@{A}). +Proof. split; repeat intro; congruence. Qed. + +(** ** Setoid equality *) +(** We define an operational type class for setoid equality, i.e., the +"canonical" equivalence for a type. The typeclass is tied to the \equiv +symbol. This is based on (Spitters/van der Weegen, 2011). *) +Class Equiv A := equiv: relation A. +(* No Hint Mode set because of Coq bug #14441. +Global Hint Mode Equiv ! : typeclass_instances. *) + +(** We instruct setoid rewriting to infer [equiv] as a relation on +type [A] when needed. This allows setoid_rewrite to solve constraints +of shape [Proper (eq ==> ?R) f] using [Proper (eq ==> (equiv (A:=A))) f] +when an equivalence relation is available on type [A]. We put this instance +at level 150 so it does not take precedence over Coq's stdlib instances, +favoring inference of [eq] (all Coq functions are automatically morphisms +for [eq]). We have [eq] (at 100) < [≡] (at 150) < [⊑] (at 200). *) +Elpi AddClasses Equiv. +Global Instance equiv_rewrite_relation `{Equiv A} : + RewriteRelation (@equiv A _) | 150 := {}. + +Infix "≡" := equiv (at level 70, no associativity) : stdpp_scope. +Infix "≡@{ A }" := (@equiv A _) + (at level 70, only parsing, no associativity) : stdpp_scope. + +Notation "(≡)" := equiv (only parsing) : stdpp_scope. +Notation "( X ≡.)" := (equiv X) (only parsing) : stdpp_scope. +Notation "(.≡ X )" := (λ Y, Y ≡ X) (only parsing) : stdpp_scope. +Notation "(≢)" := (λ X Y, ¬X ≡ Y) (only parsing) : stdpp_scope. +Notation "X ≢ Y":= (¬X ≡ Y) (at level 70, no associativity) : stdpp_scope. +Notation "( X ≢.)" := (λ Y, X ≢ Y) (only parsing) : stdpp_scope. +Notation "(.≢ X )" := (λ Y, Y ≢ X) (only parsing) : stdpp_scope. + +Notation "(≡@{ A } )" := (@equiv A _) (only parsing) : stdpp_scope. +Notation "(≢@{ A } )" := (λ X Y, ¬X ≡@{A} Y) (only parsing) : stdpp_scope. +Notation "X ≢@{ A } Y":= (¬X ≡@{ A } Y) + (at level 70, only parsing, no associativity) : stdpp_scope. + +(** The type class [LeibnizEquiv] collects setoid equalities that coincide +with Leibniz equality. We provide the tactic [fold_leibniz] to transform such +setoid equalities into Leibniz equalities, and [unfold_leibniz] for the +reverse. *) +Class LeibnizEquiv A `{Equiv A} := + leibniz_equiv (x y : A) : x ≡ y → x = y. +Global Hint Mode LeibnizEquiv ! - : typeclass_instances. + +Elpi AddClasses LeibnizEquiv Reflexive. + +Lemma leibniz_equiv_iff `{LeibnizEquiv A, !Reflexive (≡@{A})} (x y : A) : + x ≡ y ↔ x = y. +Proof. split; [apply leibniz_equiv|]. intros ->; reflexivity. Qed. + +Ltac fold_leibniz := repeat + match goal with + | H : context [ _ ≡@{?A} _ ] |- _ => + setoid_rewrite (leibniz_equiv_iff (A:=A)) in H + | |- context [ _ ≡@{?A} _ ] => + setoid_rewrite (leibniz_equiv_iff (A:=A)) + end. +Ltac unfold_leibniz := repeat + match goal with + | H : context [ _ =@{?A} _ ] |- _ => + setoid_rewrite <-(leibniz_equiv_iff (A:=A)) in H + | |- context [ _ =@{?A} _ ] => + setoid_rewrite <-(leibniz_equiv_iff (A:=A)) + end. + +Definition equivL {A} : Equiv A := (=). + +(** A [Params f n] instance forces the setoid rewriting mechanism not to +rewrite in the first [n] arguments of the function [f]. We will declare such +instances for all operational type classes in this development. *) +Global Instance: Params (@equiv) 2 := {}. + +(** The following instance forces [setoid_replace] to use setoid equality +(for types that have an [Equiv] instance) rather than the standard Leibniz +equality. *) +Global Instance equiv_default_relation `{Equiv A} : + DefaultRelation (≡@{A}) | 3 := {}. +Global Hint Extern 0 (_ ≡ _) => reflexivity : core. +Global Hint Extern 0 (_ ≡ _) => symmetry; assumption : core. + + +(** * Type classes *) +(** ** Decidable propositions *) +(** This type class by (Spitters/van der Weegen, 2011) collects decidable +propositions. *) +Class Decision (P : Prop) := decide : {P} + {¬P}. +Global Hint Mode Decision ! : typeclass_instances. +Global Arguments decide _ {_} : simpl never, assert. + +(** Although [RelDecision R] is just [∀ x y, Decision (R x y)], we make this +an explicit class instead of a notation for two reasons: + +- It allows us to control [Hint Mode] more precisely. In particular, if it were + defined as a notation, the above [Hint Mode] for [Decision] would not prevent + diverging instance search when looking for [RelDecision (@eq ?A)], which would + result in it looking for [Decision (@eq ?A x y)], i.e. an instance where the + head position of [Decision] is not en evar. +- We use it to avoid inefficient computation due to eager evaluation of + propositions by [vm_compute]. This inefficiency arises for example if + [(x = y) := (f x = f y)]. Since [decide (x = y)] evaluates to + [decide (f x = f y)], this would then lead to evaluation of [f x] and [f y]. + Using the [RelDecision], the [f] is hidden under a lambda, which prevents + unnecessary evaluation. *) +Class RelDecision {A B} (R : A → B → Prop) := + decide_rel x y :> Decision (R x y). +Global Hint Mode RelDecision ! ! ! : typeclass_instances. +Global Arguments decide_rel {_ _} _ {_} _ _ : simpl never, assert. +Notation EqDecision A := (RelDecision (=@{A})). + +(** ** Inhabited types *) +(** This type class collects types that are inhabited. *) +Class Inhabited (A : Type) : Type := populate { inhabitant : A }. +Global Hint Mode Inhabited ! : typeclass_instances. +Global Arguments populate {_} _ : assert. + +(** ** Proof irrelevant types *) +(** This type class collects types that are proof irrelevant. That means, all +elements of the type are equal. We use this notion only used for propositions, +but by universe polymorphism we can generalize it. *) +Class ProofIrrel (A : Type) : Prop := proof_irrel (x y : A) : x = y. +Global Hint Mode ProofIrrel ! : typeclass_instances. + +(** ** Common properties *) +(** These operational type classes allow us to refer to common mathematical +properties in a generic way. For example, for injectivity of [(k ++.)] it +allows us to write [inj (k ++.)] instead of [app_inv_head k]. *) +Class Inj {A B} (R : relation A) (S : relation B) (f : A → B) : Prop := + inj x y : S (f x) (f y) → R x y. + + + +Class Inj2 {A B C} (R1 : relation A) (R2 : relation B) + (S : relation C) (f : A → B → C) : Prop := + inj2 x1 x2 y1 y2 : S (f x1 x2) (f y1 y2) → R1 x1 y1 ∧ R2 x2 y2. +Class Cancel {A B} (S : relation B) (f : A → B) (g : B → A) : Prop := + cancel : ∀ x, S (f (g x)) x. +Class Surj {A B} (R : relation B) (f : A → B) := + surj y : ∃ x, R (f x) y. +Class IdemP {A} (R : relation A) (f : A → A → A) : Prop := + idemp x : R (f x x) x. +Class Comm {A B} (R : relation A) (f : B → B → A) : Prop := + comm x y : R (f x y) (f y x). + +Class LeftId {A} (R : relation A) (i : A) (f : A → A → A) : Prop := + left_id x : R (f i x) x. +Class RightId {A} (R : relation A) (i : A) (f : A → A → A) : Prop := + right_id x : R (f x i) x. +Class Assoc {A} (R : relation A) (f : A → A → A) : Prop := + assoc x y z : R (f x (f y z)) (f (f x y) z). +Class LeftAbsorb {A} (R : relation A) (i : A) (f : A → A → A) : Prop := + left_absorb x : R (f i x) i. +Class RightAbsorb {A} (R : relation A) (i : A) (f : A → A → A) : Prop := + right_absorb x : R (f x i) i. +Class AntiSymm {A} (R S : relation A) : Prop := + anti_symm x y : S x y → S y x → R x y. +Class Total {A} (R : relation A) := total x y : R x y ∨ R y x. +Class Trichotomy {A} (R : relation A) := + trichotomy x y : R x y ∨ x = y ∨ R y x. +Class TrichotomyT {A} (R : relation A) := + trichotomyT x y : {R x y} + {x = y} + {R y x}. + +Notation Involutive R f := (Cancel R f f). +Lemma involutive {A} {R : relation A} (f : A → A) `{Involutive R f} x : + R (f (f x)) x. +Proof. auto. Qed. + +Global Arguments irreflexivity {_} _ {_} _ _ : assert. +Global Arguments inj {_ _ _ _} _ {_} _ _ _ : assert. +Global Arguments inj2 {_ _ _ _ _ _} _ {_} _ _ _ _ _: assert. +Global Arguments cancel {_ _ _} _ _ {_} _ : assert. +Global Arguments surj {_ _ _} _ {_} _ : assert. +Global Arguments idemp {_ _} _ {_} _ : assert. +Global Arguments comm {_ _ _} _ {_} _ _ : assert. +Global Arguments left_id {_ _} _ _ {_} _ : assert. +Global Arguments right_id {_ _} _ _ {_} _ : assert. +Global Arguments assoc {_ _} _ {_} _ _ _ : assert. +Global Arguments left_absorb {_ _} _ _ {_} _ : assert. +Global Arguments right_absorb {_ _} _ _ {_} _ : assert. +Global Arguments anti_symm {_ _} _ {_} _ _ _ _ : assert. +Global Arguments total {_} _ {_} _ _ : assert. +Global Arguments trichotomy {_} _ {_} _ _ : assert. +Global Arguments trichotomyT {_} _ {_} _ _ : assert. + +Lemma not_symmetry `{R : relation A, !Symmetric R} x y : ¬R x y → ¬R y x. +Proof. intuition. Qed. +Lemma symmetry_iff `(R : relation A) `{!Symmetric R} x y : R x y ↔ R y x. +Proof. intuition. Qed. +Elpi AddClasses Inj2. +Lemma not_inj `{Inj A B R R' f} x y : ¬R x y → ¬R' (f x) (f y). +Proof. intuition. Qed. +Lemma not_inj2_1 `{Inj2 A B C R R' R'' f} x1 x2 y1 y2 : + ¬R x1 x2 → ¬R'' (f x1 y1) (f x2 y2). +Proof. intros HR HR''. destruct (inj2 f x1 y1 x2 y2); auto. Qed. +Lemma not_inj2_2 `{Inj2 A B C R R' R'' f} x1 x2 y1 y2 : + ¬R' y1 y2 → ¬R'' (f x1 y1) (f x2 y2). +Proof. intros HR' HR''. destruct (inj2 f x1 y1 x2 y2); auto. Qed. + +Lemma inj_iff {A B} {R : relation A} {S : relation B} (f : A → B) + `{!Inj R S f} `{!Proper (R ==> S) f} x y : S (f x) (f y) ↔ R x y. +Proof. firstorder. Qed. +Global Instance inj2_inj_1 `{Inj2 A B C R1 R2 R3 f} y : Inj R1 R3 (λ x, f x y). +Proof. repeat intro; edestruct (inj2 f); eauto. Qed. +Global Instance inj2_inj_2 `{Inj2 A B C R1 R2 R3 f} x : Inj R2 R3 (f x). +Proof. repeat intro; edestruct (inj2 f); eauto. Qed. + +Elpi AddAllClasses. +Elpi AddClasses RelDecision Cancel. +Elpi AddAllInstances. +Elpi Override TC - ProperProxy. +(* TODO: Here coq use external *) +Lemma cancel_inj `{Cancel A B R1 f g, !Equivalence R1, !Proper (R2 ==> R1) f} : + Inj R1 R2 g. +Proof. + Unset Typeclasses Debug. + (* + 2: looking for (ProperProxy eq y) without backtracking +2.1: (*external*) (class_apply @eq_proper_proxy || + class_apply @reflexive_proper_proxy) on +(ProperProxy eq y), 0 subgoal(s) +2.1: after (*external*) (class_apply @eq_proper_proxy || + class_apply @reflexive_proper_proxy) finished, 0 goals are shelved and unsolved ( ) + *) + intros x y E. rewrite <-(cancel f g x), <-(cancel f g y), E. reflexivity. +Qed. +Lemma cancel_surj `{Cancel A B R1 f g} : Surj R1 f. +Proof. intros y. exists (g y). auto. Qed. + +(** The following lemmas are specific versions of the projections of the above +type classes for Leibniz equality. These lemmas allow us to enforce Coq not to +use the setoid rewriting mechanism. *) +Lemma idemp_L {A} f `{!@IdemP A (=) f} x : f x x = x. +Proof. auto. Qed. +Lemma comm_L {A B} f `{!@Comm A B (=) f} x y : f x y = f y x. +Proof. auto. Qed. +Lemma left_id_L {A} i f `{!@LeftId A (=) i f} x : f i x = x. +Proof. auto. Qed. +Lemma right_id_L {A} i f `{!@RightId A (=) i f} x : f x i = x. +Proof. auto. Qed. +Lemma assoc_L {A} f `{!@Assoc A (=) f} x y z : f x (f y z) = f (f x y) z. +Proof. auto. Qed. +Lemma left_absorb_L {A} i f `{!@LeftAbsorb A (=) i f} x : f i x = i. +Proof. auto. Qed. +Lemma right_absorb_L {A} i f `{!@RightAbsorb A (=) i f} x : f x i = i. +Proof. auto. Qed. + +(** ** Generic orders *) +(** The classes [PreOrder], [PartialOrder], and [TotalOrder] use an arbitrary +relation [R] instead of [⊆] to support multiple orders on the same type. *) +Definition strict {A} (R : relation A) : relation A := λ X Y, R X Y ∧ ¬R Y X. +Global Instance: Params (@strict) 2 := {}. + +Class PartialOrder {A} (R : relation A) : Prop := { + partial_order_pre :> PreOrder R; + partial_order_anti_symm :> AntiSymm (=) R +}. + +Global Hint Mode PartialOrder ! ! : typeclass_instances. + +Class TotalOrder {A} (R : relation A) : Prop := { + total_order_partial :> PartialOrder R; + total_order_trichotomy :> Trichotomy (strict R) +}. +Global Hint Mode TotalOrder ! ! : typeclass_instances. + +(** * Logic *) +Global Instance prop_inhabited : Inhabited Prop := populate True. + +Notation "(∧)" := and (only parsing) : stdpp_scope. +Notation "( A ∧.)" := (and A) (only parsing) : stdpp_scope. +Notation "(.∧ B )" := (λ A, A ∧ B) (only parsing) : stdpp_scope. + +Notation "(∨)" := or (only parsing) : stdpp_scope. +Notation "( A ∨.)" := (or A) (only parsing) : stdpp_scope. +Notation "(.∨ B )" := (λ A, A ∨ B) (only parsing) : stdpp_scope. + +Notation "(↔)" := iff (only parsing) : stdpp_scope. +Notation "( A ↔.)" := (iff A) (only parsing) : stdpp_scope. +Notation "(.↔ B )" := (λ A, A ↔ B) (only parsing) : stdpp_scope. + +Global Hint Extern 0 (_ ↔ _) => reflexivity : core. +Global Hint Extern 0 (_ ↔ _) => symmetry; assumption : core. + +Lemma or_l P Q : ¬Q → P ∨ Q ↔ P. +Proof. tauto. Qed. +Lemma or_r P Q : ¬P → P ∨ Q ↔ Q. +Proof. tauto. Qed. +Lemma and_wlog_l (P Q : Prop) : (Q → P) → Q → (P ∧ Q). +Proof. tauto. Qed. +Lemma and_wlog_r (P Q : Prop) : P → (P → Q) → (P ∧ Q). +Proof. tauto. Qed. +Lemma impl_transitive (P Q R : Prop) : (P → Q) → (Q → R) → (P → R). +Proof. tauto. Qed. +Lemma forall_proper {A} (P Q : A → Prop) : + (∀ x, P x ↔ Q x) → (∀ x, P x) ↔ (∀ x, Q x). +Proof. firstorder. Qed. +Lemma exist_proper {A} (P Q : A → Prop) : + (∀ x, P x ↔ Q x) → (∃ x, P x) ↔ (∃ x, Q x). +Proof. firstorder. Qed. + +Global Instance eq_comm {A} : Comm (↔) (=@{A}). +Proof. red; intuition. Qed. +Global Instance flip_eq_comm {A} : Comm (↔) (λ x y, y =@{A} x). +Proof. red; intuition. Qed. +Global Instance iff_comm : Comm (↔) (↔). +Proof. red; intuition. Qed. +Global Instance and_comm : Comm (↔) (∧). +Proof. red; intuition. Qed. +Global Instance and_assoc : Assoc (↔) (∧). +Proof. red; intuition. Qed. +Global Instance and_idemp : IdemP (↔) (∧). +Proof. red; intuition. Qed. +Global Instance or_comm : Comm (↔) (∨). +Proof. red; intuition. Qed. +Global Instance or_assoc : Assoc (↔) (∨). +Proof. red; intuition. Qed. +Global Instance or_idemp : IdemP (↔) (∨). +Proof. red; intuition. Qed. +Global Instance True_and : LeftId (↔) True (∧). +Proof. red; intuition. Qed. +Global Instance and_True : RightId (↔) True (∧). +Proof. red; intuition. Qed. +Global Instance False_and : LeftAbsorb (↔) False (∧). +Proof. red; intuition. Qed. +Global Instance and_False : RightAbsorb (↔) False (∧). +Proof. red; intuition. Qed. +Global Instance False_or : LeftId (↔) False (∨). +Proof. red; intuition. Qed. +Global Instance or_False : RightId (↔) False (∨). +Proof. red; intuition. Qed. +Global Instance True_or : LeftAbsorb (↔) True (∨). +Proof. red; intuition. Qed. +Global Instance or_True : RightAbsorb (↔) True (∨). +Proof. red; intuition. Qed. +Global Instance True_impl : LeftId (↔) True impl. +Proof. unfold impl. red; intuition. Qed. +Global Instance impl_True : RightAbsorb (↔) True impl. +Proof. unfold impl. red; intuition. Qed. + + +(** * Common data types *) +(** ** Functions *) +Notation "(→)" := (λ A B, A → B) (only parsing) : stdpp_scope. +Notation "( A →.)" := (λ B, A → B) (only parsing) : stdpp_scope. +Notation "(.→ B )" := (λ A, A → B) (only parsing) : stdpp_scope. + +Notation "t $ r" := (t r) + (at level 65, right associativity, only parsing) : stdpp_scope. +Notation "($)" := (λ f x, f x) (only parsing) : stdpp_scope. +Notation "(.$ x )" := (λ f, f x) (only parsing) : stdpp_scope. + +Infix "∘" := compose : stdpp_scope. +Notation "(∘)" := compose (only parsing) : stdpp_scope. +Notation "( f ∘.)" := (compose f) (only parsing) : stdpp_scope. +Notation "(.∘ f )" := (λ g, compose g f) (only parsing) : stdpp_scope. + +Elpi AddAllClasses. + +Global Instance impl_inhabited {A} `{Inhabited B} : Inhabited (A → B) := + populate (λ _, inhabitant). + +(** Ensure that [simpl] unfolds [id], [compose], and [flip] when fully +applied. *) +Global Arguments id _ _ / : assert. +Global Arguments compose _ _ _ _ _ _ / : assert. +Global Arguments flip _ _ _ _ _ _ / : assert. +Global Arguments const _ _ _ _ / : assert. +Typeclasses Transparent id compose flip const. + +Definition fun_map {A A' B B'} (f: A' → A) (g: B → B') (h : A → B) : A' → B' := + g ∘ h ∘ f. + +Global Instance const_proper `{R1 : relation A, R2 : relation B} (x : B) : + Reflexive R2 → Proper (R1 ==> R2) (λ _, x). +Proof. intros ? y1 y2; reflexivity. Qed. + +Global Instance id_inj {A} : Inj (=) (=) (@id A). +Proof. intros ??; auto. Qed. +Global Instance compose_inj {A B C} R1 R2 R3 (f : A → B) (g : B → C) : + Inj R1 R2 f → Inj R2 R3 g → Inj R1 R3 (g ∘ f). +Proof. red; intuition. Qed. +Elpi AddClasses Surj. +Global Instance id_surj {A} : Surj (=) (@id A). +Proof. intros y; exists y; reflexivity. Qed. +Global Instance compose_surj {A B C} R (f : A → B) (g : B → C) : + Surj (=) f → Surj R g → Surj R (g ∘ f). +Proof. + intros ?? x. unfold compose. destruct (surj g x) as [y ?]. + destruct (surj f y) as [z ?]. exists z. congruence. +Qed. + +Global Instance id_comm {A B} (x : B) : Comm (=) (λ _ _ : A, x). +Proof. intros ?; reflexivity. Qed. +Global Instance id_assoc {A} (x : A) : Assoc (=) (λ _ _ : A, x). +Proof. intros ???; reflexivity. Qed. +Global Instance const1_assoc {A} : Assoc (=) (λ x _ : A, x). +Proof. intros ???; reflexivity. Qed. +Global Instance const2_assoc {A} : Assoc (=) (λ _ x : A, x). +Proof. intros ???; reflexivity. Qed. +Global Instance const1_idemp {A} : IdemP (=) (λ x _ : A, x). +Proof. intros ?; reflexivity. Qed. +Global Instance const2_idemp {A} : IdemP (=) (λ _ x : A, x). +Proof. intros ?; reflexivity. Qed. + +(** ** Lists *) +Global Instance list_inhabited {A} : Inhabited (list A) := populate []. + +Definition zip_with {A B C} (f : A → B → C) : list A → list B → list C := + fix go l1 l2 := + match l1, l2 with x1 :: l1, x2 :: l2 => f x1 x2 :: go l1 l2 | _ , _ => [] end. +Notation zip := (zip_with pair). + +(** ** Booleans *) +(** The following coercion allows us to use Booleans as propositions. *) +Coercion Is_true : bool >-> Sortclass. +Global Hint Unfold Is_true : core. +Global Hint Immediate Is_true_eq_left : core. +Global Hint Resolve orb_prop_intro andb_prop_intro : core. +Notation "(&&)" := andb (only parsing). +Notation "(||)" := orb (only parsing). +Infix "&&*" := (zip_with (&&)) (at level 40). +Infix "||*" := (zip_with (||)) (at level 50). + +Global Instance bool_inhabated : Inhabited bool := populate true. + +Definition bool_le (β1 β2 : bool) : Prop := negb β1 || β2. +Infix "=.>" := bool_le (at level 70). +Infix "=.>*" := (Forall2 bool_le) (at level 70). +Global Instance: PartialOrder bool_le. +Proof. repeat split; repeat intros [|]; compute; tauto. Qed. + +Lemma andb_True b1 b2 : b1 && b2 ↔ b1 ∧ b2. +Proof. destruct b1, b2; simpl; tauto. Qed. +Lemma orb_True b1 b2 : b1 || b2 ↔ b1 ∨ b2. +Proof. destruct b1, b2; simpl; tauto. Qed. +Lemma negb_True b : negb b ↔ ¬b. +Proof. destruct b; simpl; tauto. Qed. +Lemma Is_true_true (b : bool) : b ↔ b = true. +Proof. now destruct b. Qed. +Lemma Is_true_true_1 (b : bool) : b → b = true. +Proof. apply Is_true_true. Qed. +Lemma Is_true_true_2 (b : bool) : b = true → b. +Proof. apply Is_true_true. Qed. +Lemma Is_true_false (b : bool) : ¬ b ↔ b = false. +Proof. now destruct b; simpl. Qed. +Lemma Is_true_false_1 (b : bool) : ¬b → b = false. +Proof. apply Is_true_false. Qed. +Lemma Is_true_false_2 (b : bool) : b = false → ¬b. +Proof. apply Is_true_false. Qed. + +(** ** Unit *) +Global Instance unit_equiv : Equiv unit := λ _ _, True. +Elpi AddInstances Equiv. +Global Instance unit_equivalence : Equivalence (≡@{unit}). +Proof. repeat split. Qed. +Global Instance unit_leibniz : LeibnizEquiv unit. +Proof. intros [] []; reflexivity. Qed. +Global Instance unit_inhabited: Inhabited unit := populate (). + +(** ** Empty *) +Global Instance Empty_set_equiv : Equiv Empty_set := λ _ _, True. +Elpi AddInstances Equiv. +Global Instance Empty_set_equivalence : Equivalence (≡@{Empty_set}). +Proof. repeat split. Qed. +Global Instance Empty_set_leibniz : LeibnizEquiv Empty_set. +Proof. intros [] []; reflexivity. Qed. + +(** ** Products *) +Notation "( x ,.)" := (pair x) (only parsing) : stdpp_scope. +Notation "(., y )" := (λ x, (x,y)) (only parsing) : stdpp_scope. + +Notation "p .1" := (fst p) (at level 2, left associativity, format "p .1"). +Notation "p .2" := (snd p) (at level 2, left associativity, format "p .2"). + +Global Instance: Params (@pair) 2 := {}. +Global Instance: Params (@fst) 2 := {}. +Global Instance: Params (@snd) 2 := {}. + +Global Instance: Params (@curry) 3 := {}. +Global Instance: Params (@uncurry) 3 := {}. + +Definition uncurry3 {A B C D} (f : A → B → C → D) (p : A * B * C) : D := + let '(a,b,c) := p in f a b c. +Global Instance: Params (@uncurry3) 4 := {}. +Definition uncurry4 {A B C D E} (f : A → B → C → D → E) (p : A * B * C * D) : E := + let '(a,b,c,d) := p in f a b c d. +Global Instance: Params (@uncurry4) 5 := {}. + +Definition curry3 {A B C D} (f : A * B * C → D) (a : A) (b : B) (c : C) : D := + f (a, b, c). +Global Instance: Params (@curry3) 4 := {}. +Definition curry4 {A B C D E} (f : A * B * C * D → E) + (a : A) (b : B) (c : C) (d : D) : E := f (a, b, c, d). +Global Instance: Params (@curry4) 5 := {}. + +Definition prod_map {A A' B B'} (f: A → A') (g: B → B') (p : A * B) : A' * B' := + (f (p.1), g (p.2)). +Global Arguments prod_map {_ _ _ _} _ _ !_ / : assert. + +Definition prod_zip {A A' A'' B B' B''} (f : A → A' → A'') (g : B → B' → B'') + (p : A * B) (q : A' * B') : A'' * B'' := (f (p.1) (q.1), g (p.2) (q.2)). +Global Arguments prod_zip {_ _ _ _ _ _} _ _ !_ !_ / : assert. + +Global Instance prod_inhabited {A B} (iA : Inhabited A) + (iB : Inhabited B) : Inhabited (A * B) := + match iA, iB with populate x, populate y => populate (x,y) end. + +(** Note that we need eta for products for the [uncurry_curry] lemmas to hold +in non-applied form ([uncurry (curry f) = f]). *) +Lemma curry_uncurry {A B C} (f : A → B → C) : curry (uncurry f) = f. +Proof. reflexivity. Qed. +Lemma uncurry_curry {A B C} (f : A * B → C) p : uncurry (curry f) p = f p. +Proof. destruct p; reflexivity. Qed. +Lemma curry3_uncurry3 {A B C D} (f : A → B → C → D) : curry3 (uncurry3 f) = f. +Proof. reflexivity. Qed. +Lemma uncurry3_curry3 {A B C D} (f : A * B * C → D) p : + uncurry3 (curry3 f) p = f p. +Proof. destruct p as [[??] ?]; reflexivity. Qed. +Lemma curry4_uncurry4 {A B C D E} (f : A → B → C → D → E) : + curry4 (uncurry4 f) = f. +Proof. reflexivity. Qed. +Lemma uncurry4_curry4 {A B C D E} (f : A * B * C * D → E) p : + uncurry4 (curry4 f) p = f p. +Proof. destruct p as [[[??] ?] ?]; reflexivity. Qed. + +Global Instance pair_inj {A B} : Inj2 (=) (=) (=) (@pair A B). +Proof. injection 1; auto. Qed. +Global Instance prod_map_inj {A A' B B'} (f : A → A') (g : B → B') : + Inj (=) (=) f → Inj (=) (=) g → Inj (=) (=) (prod_map f g). +Proof. + intros ?? [??] [??] ?; simpl in *; f_equal; + [apply (inj f)|apply (inj g)]; congruence. +Qed. + +Definition prod_relation {A B} (R1 : relation A) (R2 : relation B) : + relation (A * B) := λ x y, R1 (x.1) (y.1) ∧ R2 (x.2) (y.2). + +Section prod_relation. + Context `{RA : relation A, RB : relation B}. + + Global Instance prod_relation_refl : + Reflexive RA → Reflexive RB → Reflexive (prod_relation RA RB). + Proof. firstorder eauto. Qed. + Global Instance prod_relation_sym : + Symmetric RA → Symmetric RB → Symmetric (prod_relation RA RB). + Proof. firstorder eauto. Qed. + Global Instance prod_relation_trans : + Transitive RA → Transitive RB → Transitive (prod_relation RA RB). + Proof. firstorder eauto. Qed. + Elpi AddInstances Transitive Reflexive Symmetric. + Global Instance prod_relation_equiv : + Equivalence RA → Equivalence RB → Equivalence (prod_relation RA RB). + Proof. split; apply _. Qed. + + Global Instance pair_proper' : Proper (RA ==> RB ==> prod_relation RA RB) pair. + Proof. firstorder eauto. Qed. + Global Instance pair_inj' : Inj2 RA RB (prod_relation RA RB) pair. + Proof. inversion_clear 1; eauto. Qed. + Global Instance fst_proper' : Proper (prod_relation RA RB ==> RA) fst. + Proof. firstorder eauto. Qed. + Global Instance snd_proper' : Proper (prod_relation RA RB ==> RB) snd. + Proof. firstorder eauto. Qed. + + Global Instance curry_proper' `{RC : relation C} : + Proper ((prod_relation RA RB ==> RC) ==> RA ==> RB ==> RC) curry. + Proof. firstorder eauto. Qed. + Global Instance uncurry_proper' `{RC : relation C} : + Proper ((RA ==> RB ==> RC) ==> prod_relation RA RB ==> RC) uncurry. + Proof. intros f1 f2 Hf [x1 y1] [x2 y2] []; apply Hf; assumption. Qed. + + Global Instance curry3_proper' `{RC : relation C, RD : relation D} : + Proper ((prod_relation (prod_relation RA RB) RC ==> RD) ==> + RA ==> RB ==> RC ==> RD) curry3. + Proof. firstorder eauto. Qed. + Global Instance uncurry3_proper' `{RC : relation C, RD : relation D} : + Proper ((RA ==> RB ==> RC ==> RD) ==> + prod_relation (prod_relation RA RB) RC ==> RD) uncurry3. + Proof. intros f1 f2 Hf [[??] ?] [[??] ?] [[??] ?]; apply Hf; assumption. Qed. + + Global Instance curry4_proper' `{RC : relation C, RD : relation D, RE : relation E} : + Proper ((prod_relation (prod_relation (prod_relation RA RB) RC) RD ==> RE) ==> + RA ==> RB ==> RC ==> RD ==> RE) curry4. + Proof. firstorder eauto. Qed. + Global Instance uncurry4_proper' `{RC : relation C, RD : relation D, RE : relation E} : + Proper ((RA ==> RB ==> RC ==> RD ==> RE) ==> + prod_relation (prod_relation (prod_relation RA RB) RC) RD ==> RE) uncurry4. + Proof. + intros f1 f2 Hf [[[??] ?] ?] [[[??] ?] ?] [[[??] ?] ?]; apply Hf; assumption. + Qed. +MySectionEnd. + +Global Instance prod_equiv `{Equiv A,Equiv B} : Equiv (A * B) := + prod_relation (≡) (≡). + +Elpi AddClasses Equivalence. + +(** Below we make [prod_equiv] type class opaque, so we first lift all +instances *) +Section prod_setoid. + Context `{Equiv A, Equiv B}. + Elpi Accumulate TC_solver lp:{{ + shorten tc-Coq.Classes.RelationClasses.{tc-Equivalence}. + :after "lastHook" + tc-Equivalence A RA R :- + RA = {{@equiv _ (@prod_equiv _ _ _ _)}}, + RA' = {{@prod_relation _ _ _ _}}, + coq.unify-eq RA RA' ok, + % coq.say A RA, + tc-Equivalence A RA' R. + }}. + (* Elpi Typecheck TC_solver. *) + + Elpi AddInstances Equiv Equivalence. + + Elpi Accumulate TC_solver lp:{{ + :after "firstHook" + solve1 (goal C _ (prod N Ty F) _ _ as G) GL :- !, + (@pi-decl N Ty x\ + declare-evar [decl x N Ty|C] (Raw x) (F x) (Sol x), + solve1 (goal [decl x N Ty|C] (Raw x) (F x) (Sol x) []) _, + coq.safe-dest-app (Sol x) Hd (Args x)), + if (pi x\ last-no-error (Args x) x, std.drop-last 1 (Args x) NewArgs) + (coq.mk-app Hd NewArgs Out, refine Out G GL1) (refine (fun N _ _) G GL1), + coq.ltac.all (coq.ltac.open solve) GL1 GL. + }}. + Elpi Typecheck TC_solver. + + Global Instance prod_equivalence@{i} (C D: Type@{i}) `{Equiv C, Equiv D}: + @Equivalence C (≡@{C}) → @Equivalence D (≡@{D}) → @Equivalence (C * D) (≡@{C * D}) := _. + + Elpi Accumulate TC_solver lp:{{ + + pred remove_equiv_prod_equiv i:term, o:term. + remove_equiv_prod_equiv T1 T3 :- + T1 = {{@equiv _ (@prod_equiv _ _ _ _)}}, !, + T2 = {{@prod_relation lp:F lp:G lp:A lp:B}}, + coq.unify-eq T1 T2 ok, + remove_equiv_prod_equiv A X, + remove_equiv_prod_equiv B Y, + {{@prod_relation lp:F lp:G lp:X lp:Y}} = T3. + remove_equiv_prod_equiv (app L1) (app L2) :- !, + std.map L1 remove_equiv_prod_equiv L2. + remove_equiv_prod_equiv A A. + + shorten tc-Coq.Classes.Morphisms.{tc-Proper}. + + :after "lastHook" + tc-Proper A B C R :- + B = {{ @respectful _ _ _ _ }}, + remove_equiv_prod_equiv B B1, + tc-Proper A B1 C R. + + tc-Proper A {{@respectful lp:K1 lp:K2 lp:B1 (@respectful lp:K3 lp:K4 lp:B2 lp:B3)}} C S :- + C1 = {{ @equiv _ _ }}, + C2 = {{ @equiv _ _ }}, + C3 = {{ @prod_relation _ _ _ _ }}, + coq.unify-eq B1 C1 ok, + coq.unify-eq B2 C2 ok, + coq.unify-eq B3 C3 ok, + tc-Proper A {{@respectful lp:K1 lp:K2 lp:C1 (@respectful lp:K3 lp:K4 lp:C2 lp:C3)}} C S. + + }}. + Elpi Typecheck TC_solver. + Elpi AddInstances Proper. + + Global Instance pair_proper : Proper ((≡) ==> (≡) ==> (≡@{A*B})) pair := _. + + Elpi Accumulate TC_solver lp:{{ + shorten tc-elpi.apps.tc.tests.bigTest.{tc-Inj2}. + % shorten tc-bigTest.{tc-Inj2}. + :after "lastHook" + tc-Inj2 A B C RA RB RC F S :- + RC = app [global {coq.locate "equiv"} | _], + remove_equiv_prod_equiv RC RC', + tc-Inj2 A B C RA RB RC' F S. + }}. + Elpi Typecheck TC_solver. + + Elpi AddInstances Inj2. + Global Instance pair_equiv_inj : Inj2 (≡) (≡) (≡@{A*B}) pair := _. + Global Instance fst_proper : Proper ((≡@{A*B}) ==> (≡)) fst := _. + Global Instance snd_proper : Proper ((≡@{A*B}) ==> (≡)) snd := _. + + Global Instance curry_proper `{Equiv C} : + Proper (((≡@{A*B}) ==> (≡@{C})) ==> (≡) ==> (≡) ==> (≡)) curry := _. + + Global Instance uncurry_proper `{Equiv C} : + Proper (((≡) ==> (≡) ==> (≡)) ==> (≡@{A*B}) ==> (≡@{C})) uncurry := _. + + Global Instance curry3_proper `{Equiv C, Equiv D} : + Proper (((≡@{A*B*C}) ==> (≡@{D})) ==> + (≡) ==> (≡) ==> (≡) ==> (≡)) curry3 := _. + Global Instance uncurry3_proper `{Equiv C, Equiv D} : + Proper (((≡) ==> (≡) ==> (≡) ==> (≡)) ==> + (≡@{A*B*C}) ==> (≡@{D})) uncurry3 := _. + + Global Instance curry4_proper `{Equiv C, Equiv D, Equiv E} : + Proper (((≡@{A*B*C*D}) ==> (≡@{E})) ==> + (≡) ==> (≡) ==> (≡) ==> (≡) ==> (≡)) curry4 := _. + Global Instance uncurry4_proper `{Equiv C, Equiv D, Equiv E} : + Proper (((≡) ==> (≡) ==> (≡) ==> (≡) ==> (≡)) ==> + (≡@{A*B*C*D}) ==> (≡@{E})) uncurry4 := _. +MySectionEnd. + +Global Typeclasses Opaque prod_equiv. + +Global Instance prod_leibniz {A : Type} {B : Type} `{LeibnizEquiv A, LeibnizEquiv B} : + LeibnizEquiv (A * B). +Proof. +intros [??] [??] [??]; f_equal; apply leibniz_equiv; auto. + (* Set Printing All. + Set Printing Universes. + Show Proof. *) +Qed. + +(** ** Sums *) +Definition sum_map {A A' B B'} (f: A → A') (g: B → B') (xy : A + B) : A' + B' := + match xy with inl x => inl (f x) | inr y => inr (g y) end. +Global Arguments sum_map {_ _ _ _} _ _ !_ / : assert. + +Global Instance sum_inhabited_l {A B} (iA : Inhabited A) : Inhabited (A + B) := + match iA with populate x => populate (inl x) end. +Global Instance sum_inhabited_r {A B} (iB : Inhabited B) : Inhabited (A + B) := + match iB with populate y => populate (inr y) end. + +Global Instance inl_inj {A B} : Inj (=) (=) (@inl A B). +Proof. injection 1; auto. Qed. +Global Instance inr_inj {A B} : Inj (=) (=) (@inr A B). +Proof. injection 1; auto. Qed. + +(* TODO: here last term is flexible ? *) +Global Instance sum_map_inj {A A' B B'} (f : A → A') (g : B → B') : + Inj (=) (=) f → Inj (=) (=) g → Inj (=) (=) (sum_map f g). +Proof. intros ?? [?|?] [?|?] [=]; f_equal; apply (inj _); auto. Qed. + +Inductive sum_relation {A B} + (RA : relation A) (RB : relation B) : relation (A + B) := + | inl_related x1 x2 : RA x1 x2 → sum_relation RA RB (inl x1) (inl x2) + | inr_related y1 y2 : RB y1 y2 → sum_relation RA RB (inr y1) (inr y2). + +Section sum_relation. + Context `{RA : relation A, RB : relation B}. + Global Instance sum_relation_refl : + Reflexive RA → Reflexive RB → Reflexive (sum_relation RA RB). + Proof. intros ?? [?|?]; constructor; reflexivity. Qed. + Global Instance sum_relation_sym : + Symmetric RA → Symmetric RB → Symmetric (sum_relation RA RB). + Proof. destruct 3; constructor; eauto. Qed. + Global Instance sum_relation_trans : + Transitive RA → Transitive RB → Transitive (sum_relation RA RB). + Proof. destruct 3; inversion_clear 1; constructor; eauto. Qed. + + Elpi AddInstances Transitive Reflexive Symmetric. + Global Instance sum_relation_equiv : + Equivalence RA → Equivalence RB → Equivalence (sum_relation RA RB). + Proof. split; apply _. Qed. + Global Instance inl_proper' : Proper (RA ==> sum_relation RA RB) inl. + Proof. constructor; auto. Qed. + Global Instance inr_proper' : Proper (RB ==> sum_relation RA RB) inr. + Proof. constructor; auto. Qed. + Global Instance inl_inj' : Inj RA (sum_relation RA RB) inl. + Proof. inversion_clear 1; auto. Qed. + Global Instance inr_inj' : Inj RB (sum_relation RA RB) inr. + Proof. inversion_clear 1; auto. Qed. +MySectionEnd. + +Elpi AddInstances Proper. + +Global Instance sum_equiv `{Equiv A, Equiv B} : Equiv (A + B) := sum_relation (≡) (≡). + +Elpi Accumulate TC_solver lp:{{ + pred remove_equiv_sum_equiv i:term, o:term. + remove_equiv_sum_equiv T1 T3 :- + T1 = {{@equiv _ (@sum_equiv _ _ _ _)}}, !, + T2 = {{@sum_relation lp:F lp:G lp:A lp:B}}, + coq.unify-eq T1 T2 ok, + remove_equiv_sum_equiv A X, + remove_equiv_sum_equiv B Y, + {{@sum_relation lp:F lp:G lp:X lp:Y}} = T3. + remove_equiv_sum_equiv (app L1) (app L2) :- !, + std.map L1 remove_equiv_sum_equiv L2. + remove_equiv_sum_equiv A A. + + shorten tc-Coq.Classes.Morphisms.{tc-Proper}. + :after "lastHook" + tc-Proper A B C R :- + B = {{ @respectful _ _ _ _ }}, + remove_equiv_sum_equiv B B1, + tc-Proper A B1 C R. +}}. +Elpi Typecheck TC_solver. + +Elpi AddInstances Equiv. + +Global Instance inl_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@inl A B) := _. +Global Instance inr_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@inr A B) := _. + +Elpi AddInstances Inj. + +(* Elpi added here *) +Elpi Accumulate TC_solver lp:{{ + shorten tc-elpi.apps.tc.tests.bigTest.{tc-Inj}. + % shorten tc-bigTest.{tc-Inj}. + :after "lastHook" + tc-Inj A B R1 R2 S C :- + R2 = {{@equiv (sum _ _) sum_equiv}}, + R2' = {{sum_relation _ _}}, + coq.unify-eq R2 R2' ok, + tc-Inj A B R1 R2' S C. +}}. +Elpi Typecheck TC_solver. + +Global Instance inl_equiv_inj `{Equiv A, Equiv B} : Inj (≡) (≡) (@inl A B) := _. +Global Instance inr_equiv_inj `{Equiv A, Equiv B} : Inj (≡) (≡) (@inr A B) := _. +Typeclasses Opaque sum_equiv. + +(** ** Option *) +Global Instance option_inhabited {A} : Inhabited (option A) := populate None. + +(** ** Sigma types *) +Global Arguments existT {_ _} _ _ : assert. +Global Arguments projT1 {_ _} _ : assert. +Global Arguments projT2 {_ _} _ : assert. + +Global Arguments exist {_} _ _ _ : assert. +Global Arguments proj1_sig {_ _} _ : assert. +Global Arguments proj2_sig {_ _} _ : assert. +Notation "x ↾ p" := (exist _ x p) (at level 20) : stdpp_scope. +Notation "` x" := (proj1_sig x) (at level 10, format "` x") : stdpp_scope. + +Elpi AddClasses ProofIrrel. + +Lemma proj1_sig_inj {A} (P : A → Prop) x (Px : P x) y (Py : P y) : + x↾Px = y↾Py → x = y. +Proof. injection 1; trivial. Qed. + +Section sig_map. + Context `{P : A → Prop} `{Q : B → Prop} (f : A → B) (Hf : ∀ x, P x → Q (f x)). + Definition sig_map (x : sig P) : sig Q := f (`x) ↾ Hf _ (proj2_sig x). + Global Instance sig_map_inj: + (∀ x, ProofIrrel (P x)) → Inj (=) (=) f → Inj (=) (=) sig_map. + Proof. + intros ?? [x Hx] [y Hy]. injection 1. intros Hxy. + apply (inj f) in Hxy; subst. + rewrite (proof_irrel _ Hy). auto. + Qed. +MySectionEnd. +Global Arguments sig_map _ _ _ _ _ _ !_ / : assert. + +Definition proj1_ex {P : Prop} {Q : P → Prop} (p : ∃ x, Q x) : P := + let '(ex_intro _ x _) := p in x. +Definition proj2_ex {P : Prop} {Q : P → Prop} (p : ∃ x, Q x) : Q (proj1_ex p) := + let '(ex_intro _ x H) := p in H. + +(** * Operations on sets *) +(** We define operational type classes for the traditional operations and +relations on sets: the empty set [∅], the union [(∪)], +intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset +[(⊆)] and element of [(∈)] relation, and disjointess [(##)]. *) +Class Empty A := empty: A. +Global Hint Mode Empty ! : typeclass_instances. +Notation "∅" := empty (format "∅") : stdpp_scope. + +Elpi AddClasses Empty. + +Global Instance empty_inhabited `(Empty A) : Inhabited A := populate ∅. + +Class Union A := union: A → A → A. +Global Hint Mode Union ! : typeclass_instances. +Global Instance: Params (@union) 2 := {}. +Infix "∪" := union (at level 50, left associativity) : stdpp_scope. +Notation "(∪)" := union (only parsing) : stdpp_scope. +Notation "( x ∪.)" := (union x) (only parsing) : stdpp_scope. +Notation "(.∪ x )" := (λ y, union y x) (only parsing) : stdpp_scope. +Infix "∪*" := (zip_with (∪)) (at level 50, left associativity) : stdpp_scope. +Notation "(∪*)" := (zip_with (∪)) (only parsing) : stdpp_scope. + +Elpi AddClasses Union. +Definition union_list `{Empty A} `{Union A} : list A → A := fold_right (∪) ∅. +Global Arguments union_list _ _ _ !_ / : assert. +Notation "⋃ l" := (union_list l) (at level 20, format "⋃ l") : stdpp_scope. + +Class Intersection A := intersection: A → A → A. +Global Hint Mode Intersection ! : typeclass_instances. +Global Instance: Params (@intersection) 2 := {}. +Infix "∩" := intersection (at level 40) : stdpp_scope. +Notation "(∩)" := intersection (only parsing) : stdpp_scope. +Notation "( x ∩.)" := (intersection x) (only parsing) : stdpp_scope. +Notation "(.∩ x )" := (λ y, intersection y x) (only parsing) : stdpp_scope. + +Class Difference A := difference: A → A → A. +Global Hint Mode Difference ! : typeclass_instances. +Global Instance: Params (@difference) 2 := {}. +Infix "∖" := difference (at level 40, left associativity) : stdpp_scope. +Notation "(∖)" := difference (only parsing) : stdpp_scope. +Notation "( x ∖.)" := (difference x) (only parsing) : stdpp_scope. +Notation "(.∖ x )" := (λ y, difference y x) (only parsing) : stdpp_scope. +Infix "∖*" := (zip_with (∖)) (at level 40, left associativity) : stdpp_scope. +Notation "(∖*)" := (zip_with (∖)) (only parsing) : stdpp_scope. + +Class Singleton A B := singleton: A → B. +Global Hint Mode Singleton - ! : typeclass_instances. +Global Instance: Params (@singleton) 3 := {}. +Notation "{[ x ]}" := (singleton x) (at level 1) : stdpp_scope. +Notation "{[ x ; y ; .. ; z ]}" := + (union .. (union (singleton x) (singleton y)) .. (singleton z)) + (at level 1) : stdpp_scope. + +Class SubsetEq A := subseteq: relation A. +Global Hint Mode SubsetEq ! : typeclass_instances. +Global Instance: Params (@subseteq) 2 := {}. +Infix "⊆" := subseteq (at level 70) : stdpp_scope. +Notation "(⊆)" := subseteq (only parsing) : stdpp_scope. +Notation "( X ⊆.)" := (subseteq X) (only parsing) : stdpp_scope. +Notation "(.⊆ X )" := (λ Y, Y ⊆ X) (only parsing) : stdpp_scope. +Notation "X ⊈ Y" := (¬X ⊆ Y) (at level 70) : stdpp_scope. +Notation "(⊈)" := (λ X Y, X ⊈ Y) (only parsing) : stdpp_scope. +Notation "( X ⊈.)" := (λ Y, X ⊈ Y) (only parsing) : stdpp_scope. +Notation "(.⊈ X )" := (λ Y, Y ⊈ X) (only parsing) : stdpp_scope. + +Infix "⊆@{ A }" := (@subseteq A _) (at level 70, only parsing) : stdpp_scope. +Notation "(⊆@{ A } )" := (@subseteq A _) (only parsing) : stdpp_scope. + +Infix "⊆*" := (Forall2 (⊆)) (at level 70) : stdpp_scope. +Notation "(⊆*)" := (Forall2 (⊆)) (only parsing) : stdpp_scope. + +Global Hint Extern 0 (_ ⊆ _) => reflexivity : core. +Global Hint Extern 0 (_ ⊆* _) => reflexivity : core. + +Infix "⊂" := (strict (⊆)) (at level 70) : stdpp_scope. +Notation "(⊂)" := (strict (⊆)) (only parsing) : stdpp_scope. +Notation "( X ⊂.)" := (strict (⊆) X) (only parsing) : stdpp_scope. +Notation "(.⊂ X )" := (λ Y, Y ⊂ X) (only parsing) : stdpp_scope. +Notation "X ⊄ Y" := (¬X ⊂ Y) (at level 70) : stdpp_scope. +Notation "(⊄)" := (λ X Y, X ⊄ Y) (only parsing) : stdpp_scope. +Notation "( X ⊄.)" := (λ Y, X ⊄ Y) (only parsing) : stdpp_scope. +Notation "(.⊄ X )" := (λ Y, Y ⊄ X) (only parsing) : stdpp_scope. + +Infix "⊂@{ A }" := (strict (⊆@{A})) (at level 70, only parsing) : stdpp_scope. +Notation "(⊂@{ A } )" := (strict (⊆@{A})) (only parsing) : stdpp_scope. + +Notation "X ⊆ Y ⊆ Z" := (X ⊆ Y ∧ Y ⊆ Z) (at level 70, Y at next level) : stdpp_scope. +Notation "X ⊆ Y ⊂ Z" := (X ⊆ Y ∧ Y ⊂ Z) (at level 70, Y at next level) : stdpp_scope. +Notation "X ⊂ Y ⊆ Z" := (X ⊂ Y ∧ Y ⊆ Z) (at level 70, Y at next level) : stdpp_scope. +Notation "X ⊂ Y ⊂ Z" := (X ⊂ Y ∧ Y ⊂ Z) (at level 70, Y at next level) : stdpp_scope. + +(** We define type classes for multisets: disjoint union [⊎] and the multiset +singleton [{[+ _ +]}]. Multiset literals [{[+ x1; ..; xn +]}] are defined in +terms of iterated disjoint union [{[+ x1 +]} ⊎ .. ⊎ {[+ xn +]}], and are thus +different from set literals [{[ x1; ..; xn ]}], which use [∪]. + +Note that in principle we could reuse the set singleton [{[ _ ]}] for multisets, +and define [{[+ x1; ..; xn +]}] as [{[ x1 ]} ⊎ .. ⊎ {[ xn ]}]. However, this +would risk accidentally using [{[ x1; ..; xn ]}] for multisets (leading to +unexpected results) and lead to ambigious pretty printing for [{[+ x +]}]. *) +Class DisjUnion A := disj_union: A → A → A. +Global Hint Mode DisjUnion ! : typeclass_instances. +Global Instance: Params (@disj_union) 2 := {}. +Infix "⊎" := disj_union (at level 50, left associativity) : stdpp_scope. +Notation "(⊎)" := disj_union (only parsing) : stdpp_scope. +Notation "( x ⊎.)" := (disj_union x) (only parsing) : stdpp_scope. +Notation "(.⊎ x )" := (λ y, disj_union y x) (only parsing) : stdpp_scope. + +Class SingletonMS A B := singletonMS: A → B. +Global Hint Mode SingletonMS - ! : typeclass_instances. +Global Instance: Params (@singletonMS) 3 := {}. +Notation "{[+ x +]}" := (singletonMS x) + (at level 1, format "{[+ x +]}") : stdpp_scope. +Notation "{[+ x ; y ; .. ; z +]}" := + (disj_union .. (disj_union (singletonMS x) (singletonMS y)) .. (singletonMS z)) + (at level 1, format "{[+ x ; y ; .. ; z +]}") : stdpp_scope. + +Elpi AddClasses Singleton DisjUnion. +Elpi AddAllClasses. +Definition option_to_set `{Singleton A C, Empty C} (mx : option A) : C := + match mx with None => ∅ | Some x => {[ x ]} end. +Fixpoint list_to_set `{Singleton A C, Empty C, Union C} (l : list A) : C := + match l with [] => ∅ | x :: l => {[ x ]} ∪ list_to_set l end. +Elpi AddClasses SingletonMS. +Fixpoint list_to_set_disj `{SingletonMS A C, Empty C, DisjUnion C} (l : list A) : C := + match l with [] => ∅ | x :: l => {[+ x +]} ⊎ list_to_set_disj l end. + +Class ScalarMul N A := scalar_mul : N → A → A. +Global Hint Mode ScalarMul - ! : typeclass_instances. +(** The [N] arguments is typically [nat] or [Z], so we do not want to rewrite +in that. Hence, the value of [Params] is 3. *) +Global Instance: Params (@scalar_mul) 3 := {}. +(** The notation [*:] and level is taken from ssreflect, see +https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/ssrnotations.v *) +Infix "*:" := scalar_mul (at level 40, left associativity) : stdpp_scope. +Notation "(*:)" := scalar_mul (only parsing) : stdpp_scope. +Notation "( x *:.)" := (scalar_mul x) (only parsing) : stdpp_scope. +Notation "(.*: x )" := (λ y, scalar_mul y x) (only parsing) : stdpp_scope. + +(** The class [Lexico A] is used for the lexicographic order on [A]. This order +is used to create finite maps, finite sets, etc, and is typically different from +the order [(⊆)]. *) +Class Lexico A := lexico: relation A. +Global Hint Mode Lexico ! : typeclass_instances. + +Class ElemOf A B := elem_of: A → B → Prop. +Global Hint Mode ElemOf - ! : typeclass_instances. +Global Instance: Params (@elem_of) 3 := {}. +Infix "∈" := elem_of (at level 70) : stdpp_scope. +Notation "(∈)" := elem_of (only parsing) : stdpp_scope. +Notation "( x ∈.)" := (elem_of x) (only parsing) : stdpp_scope. +Notation "(.∈ X )" := (λ x, elem_of x X) (only parsing) : stdpp_scope. +Notation "x ∉ X" := (¬x ∈ X) (at level 80) : stdpp_scope. +Notation "(∉)" := (λ x X, x ∉ X) (only parsing) : stdpp_scope. +Notation "( x ∉.)" := (λ X, x ∉ X) (only parsing) : stdpp_scope. +Notation "(.∉ X )" := (λ x, x ∉ X) (only parsing) : stdpp_scope. + +Infix "∈@{ B }" := (@elem_of _ B _) (at level 70, only parsing) : stdpp_scope. +Notation "(∈@{ B } )" := (@elem_of _ B _) (only parsing) : stdpp_scope. + +Notation "x ∉@{ B } X" := (¬x ∈@{B} X) (at level 80, only parsing) : stdpp_scope. +Notation "(∉@{ B } )" := (λ x X, x ∉@{B} X) (only parsing) : stdpp_scope. + +Class Disjoint A := disjoint : A → A → Prop. +Global Hint Mode Disjoint ! : typeclass_instances. +Global Instance: Params (@disjoint) 2 := {}. +Infix "##" := disjoint (at level 70) : stdpp_scope. +Notation "(##)" := disjoint (only parsing) : stdpp_scope. +Notation "( X ##.)" := (disjoint X) (only parsing) : stdpp_scope. +Notation "(.## X )" := (λ Y, Y ## X) (only parsing) : stdpp_scope. + +Infix "##@{ A }" := (@disjoint A _) (at level 70, only parsing) : stdpp_scope. +Notation "(##@{ A } )" := (@disjoint A _) (only parsing) : stdpp_scope. + +Infix "##*" := (Forall2 (##)) (at level 70) : stdpp_scope. +Notation "(##*)" := (Forall2 (##)) (only parsing) : stdpp_scope. + +Global Hint Extern 0 (_ ## _) => symmetry; eassumption : core. +Global Hint Extern 0 (_ ##* _) => symmetry; eassumption : core. + +Class Filter A B := filter: ∀ (P : A → Prop) `{∀ x, Decision (P x)}, B → B. +Global Hint Mode Filter - ! : typeclass_instances. + +Class UpClose A B := up_close : A → B. +Global Hint Mode UpClose - ! : typeclass_instances. +Notation "↑ x" := (up_close x) (at level 20, format "↑ x"). + +(** * Monadic operations *) +(** We define operational type classes for the monadic operations bind, join +and fmap. We use these type classes merely for convenient overloading of +notations and do not formalize any theory on monads (we do not even define a +class with the monad laws). *) +Class MRet (M : Type → Type) := mret: ∀ {A}, A → M A. +Global Arguments mret {_ _ _} _ : assert. +Global Instance: Params (@mret) 3 := {}. +Global Hint Mode MRet ! : typeclass_instances. + +Class MBind (M : Type → Type) := mbind : ∀ {A B}, (A → M B) → M A → M B. +Global Arguments mbind {_ _ _ _} _ !_ / : assert. +Global Instance: Params (@mbind) 4 := {}. +Global Hint Mode MBind ! : typeclass_instances. + +Class MJoin (M : Type → Type) := mjoin: ∀ {A}, M (M A) → M A. +Global Arguments mjoin {_ _ _} !_ / : assert. +Global Instance: Params (@mjoin) 3 := {}. +Global Hint Mode MJoin ! : typeclass_instances. + +Class FMap (M : Type → Type) := fmap : ∀ {A B}, (A → B) → M A → M B. +Global Arguments fmap {_ _ _ _} _ !_ / : assert. +Global Instance: Params (@fmap) 4 := {}. +Global Hint Mode FMap ! : typeclass_instances. + +Class OMap (M : Type → Type) := omap: ∀ {A B}, (A → option B) → M A → M B. +Global Arguments omap {_ _ _ _} _ !_ / : assert. +Global Instance: Params (@omap) 4 := {}. +Global Hint Mode OMap ! : typeclass_instances. + +Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : stdpp_scope. +Notation "( m ≫=.)" := (λ f, mbind f m) (only parsing) : stdpp_scope. +Notation "(.≫= f )" := (mbind f) (only parsing) : stdpp_scope. +Notation "(≫=)" := (λ m f, mbind f m) (only parsing) : stdpp_scope. + +Notation "x ← y ; z" := (y ≫= (λ x : _, z)) + (at level 20, y at level 100, z at level 200, only parsing) : stdpp_scope. + +Notation "' x ← y ; z" := (y ≫= (λ x : _, z)) + (at level 20, x pattern, y at level 100, z at level 200, only parsing) : stdpp_scope. + +Infix "<$>" := fmap (at level 61, left associativity) : stdpp_scope. + +Notation "x ;; z" := (x ≫= λ _, z) + (at level 100, z at level 200, only parsing, right associativity): stdpp_scope. + +Notation "ps .*1" := (fmap (M:=list) fst ps) + (at level 2, left associativity, format "ps .*1"). +Notation "ps .*2" := (fmap (M:=list) snd ps) + (at level 2, left associativity, format "ps .*2"). + +Class MGuard (M : Type → Type) := + mguard: ∀ P {dec : Decision P} {A}, (P → M A) → M A. +Global Arguments mguard _ _ _ !_ _ _ / : assert. +Global Hint Mode MGuard ! : typeclass_instances. +Notation "'guard' P ; z" := (mguard P (λ _, z)) + (at level 20, z at level 200, only parsing, right associativity) : stdpp_scope. +Notation "'guard' P 'as' H ; z" := (mguard P (λ H, z)) + (at level 20, z at level 200, only parsing, right associativity) : stdpp_scope. + +(** * Operations on maps *) +(** In this section we define operational type classes for the operations +on maps. In the file [fin_maps] we will axiomatize finite maps. +The function look up [m !! k] should yield the element at key [k] in [m]. *) +Class Lookup (K A M : Type) := lookup: K → M → option A. +Global Hint Mode Lookup - - ! : typeclass_instances. +Global Instance: Params (@lookup) 4 := {}. +Notation "m !! i" := (lookup i m) (at level 20) : stdpp_scope. +Notation "(!!)" := lookup (only parsing) : stdpp_scope. +Notation "( m !!.)" := (λ i, m !! i) (only parsing) : stdpp_scope. +Notation "(.!! i )" := (lookup i) (only parsing) : stdpp_scope. +Global Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch, assert. + +(** The function [lookup_total] should be the total over-approximation +of the partial [lookup] function. *) +Class LookupTotal (K A M : Type) := lookup_total : K → M → A. +Global Hint Mode LookupTotal - - ! : typeclass_instances. +Global Instance: Params (@lookup_total) 4 := {}. +Notation "m !!! i" := (lookup_total i m) (at level 20) : stdpp_scope. +Notation "(!!!)" := lookup_total (only parsing) : stdpp_scope. +Notation "( m !!!.)" := (λ i, m !!! i) (only parsing) : stdpp_scope. +Notation "(.!!! i )" := (lookup_total i) (only parsing) : stdpp_scope. +Global Arguments lookup_total _ _ _ _ !_ !_ / : simpl nomatch, assert. + +(** The singleton map *) +Class SingletonM K A M := singletonM: K → A → M. +Global Hint Mode SingletonM - - ! : typeclass_instances. +Global Instance: Params (@singletonM) 5 := {}. +Notation "{[ k := a ]}" := (singletonM k a) (at level 1) : stdpp_scope. + +(** The function insert [<[k:=a]>m] should update the element at key [k] with +value [a] in [m]. *) +Class Insert (K A M : Type) := insert: K → A → M → M. +Global Hint Mode Insert - - ! : typeclass_instances. +Global Instance: Params (@insert) 5 := {}. +Notation "<[ k := a ]>" := (insert k a) + (at level 5, right associativity, format "<[ k := a ]>") : stdpp_scope. +Global Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch, assert. + +(** Notation for more elements (up to 13) *) +(* Defining a generic notation does not seem possible with Coq's + recursive notation system, so we define individual notations + for some cases relevant in practice. *) +(* The "format" makes sure that linebreaks are placed after the separating semicola [;] when printing. *) +(* TODO : we are using parantheses in the "de-sugaring" of the notation instead of [$] because Coq 8.12 + and earlier have trouble with using the notation for printing otherwise. + Once support for Coq 8.12 is dropped, this can be replaced with [$]. *) +Notation "{[ k1 := a1 ; k2 := a2 ]}" := + (<[ k1 := a1 ]>{[ k2 := a2 ]}) + (at level 1, format + "{[ '[hv' '[' k1 := a1 ; ']' '/' '[' k2 := a2 ']' ']' ]}") : stdpp_scope. +Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ]}" := + (<[ k1 := a1 ]> ( <[ k2 := a2 ]>{[ k3 := a3 ]})) + (at level 1, format + "{[ '[hv' '[' k1 := a1 ; ']' '/' '[' k2 := a2 ; ']' '/' '[' k3 := a3 ']' ']' ]}") : stdpp_scope. +Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ]}" := + (<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]>{[ k4 := a4 ]}))) + (at level 1, format + "{[ '[hv' '[' k1 := a1 ; ']' '/' '[' k2 := a2 ; ']' '/' '[' k3 := a3 ; ']' '/' '[' k4 := a4 ']' ']' ]}") : stdpp_scope. +Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ]}" := + (<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]>{[ k5 := a5 ]})))) + (at level 1, format + "{[ '[hv' '[' k1 := a1 ; ']' '/' '[' k2 := a2 ; ']' '/' '[' k3 := a3 ; ']' '/' '[' k4 := a4 ; ']' '/' '[' k5 := a5 ']' ']' ]}") : stdpp_scope. +Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ]}" := + (<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]> ( + <[ k5 := a5 ]>{[ k6 := a6 ]}))))) + (at level 1, format + "{[ '[hv' '[' k1 := a1 ; ']' '/' '[' k2 := a2 ; ']' '/' '[' k3 := a3 ; ']' '/' '[' k4 := a4 ; ']' '/' '[' k5 := a5 ; ']' '/' '[' k6 := a6 ']' ']' ]}") : stdpp_scope. +Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ]}" := + (<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]> ( + <[ k5 := a5 ]> ( <[ k6 := a6 ]>{[ k7 := a7 ]})))))) + (at level 1, format + "{[ '[hv' '[' k1 := a1 ; ']' '/' '[' k2 := a2 ; ']' '/' '[' k3 := a3 ; ']' '/' '[' k4 := a4 ; ']' '/' '[' k5 := a5 ; ']' '/' '[' k6 := a6 ; ']' '/' '[' k7 := a7 ']' ']' ]}") : stdpp_scope. +Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ]}" := + (<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]> ( + <[ k5 := a5 ]> ( <[ k6 := a6 ]> ( <[ k7 := a7 ]>{[ k8 := a8 ]}))))))) + (at level 1, format + "{[ '[hv' '[' k1 := a1 ; ']' '/' '[' k2 := a2 ; ']' '/' '[' k3 := a3 ; ']' '/' '[' k4 := a4 ; ']' '/' '[' k5 := a5 ; ']' '/' '[' k6 := a6 ; ']' '/' '[' k7 := a7 ; ']' '/' '[' k8 := a8 ']' ']' ]}") : stdpp_scope. +Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ; k9 := a9 ]}" := + (<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]> ( + <[ k5 := a5 ]> ( <[ k6 := a6 ]> ( <[ k7 := a7 ]> ( <[ k8 := a8 ]>{[ k9 := a9 ]})))))))) + (at level 1, format + "{[ '[hv' '[' k1 := a1 ; ']' '/' '[' k2 := a2 ; ']' '/' '[' k3 := a3 ; ']' '/' '[' k4 := a4 ; ']' '/' '[' k5 := a5 ; ']' '/' '[' k6 := a6 ; ']' '/' '[' k7 := a7 ; ']' '/' '[' k8 := a8 ; ']' '/' '[' k9 := a9 ']' ']' ]}") : stdpp_scope. +Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ; k9 := a9 ; k10 := a10 ]}" := + (<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]> ( + <[ k5 := a5 ]> ( <[ k6 := a6 ]> ( <[ k7 := a7 ]> ( <[ k8 := a8 ]> ( + <[ k9 := a9 ]>{[ k10 := a10 ]}))))))))) + (at level 1, format + "{[ '[hv' '[' k1 := a1 ; ']' '/' '[' k2 := a2 ; ']' '/' '[' k3 := a3 ; ']' '/' '[' k4 := a4 ; ']' '/' '[' k5 := a5 ; ']' '/' '[' k6 := a6 ; ']' '/' '[' k7 := a7 ; ']' '/' '[' k8 := a8 ; ']' '/' '[' k9 := a9 ; ']' '/' '[' k10 := a10 ']' ']' ]}") : stdpp_scope. +Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ; k9 := a9 ; k10 := a10 ; k11 := a11 ]}" := + (<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]> ( + <[ k5 := a5 ]> ( <[ k6 := a6 ]> ( <[ k7 := a7 ]> ( <[ k8 := a8 ]> ( + <[ k9 := a9 ]> ( <[ k10 := a10 ]>{[ k11 := a11 ]})))))))))) + (at level 1, format + "{[ '[hv' '[' k1 := a1 ; ']' '/' '[' k2 := a2 ; ']' '/' '[' k3 := a3 ; ']' '/' '[' k4 := a4 ; ']' '/' '[' k5 := a5 ; ']' '/' '[' k6 := a6 ; ']' '/' '[' k7 := a7 ; ']' '/' '[' k8 := a8 ; ']' '/' '[' k9 := a9 ; ']' '/' '[' k10 := a10 ; ']' '/' '[' k11 := a11 ']' ']' ]}") : stdpp_scope. +Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ; k9 := a9 ; k10 := a10 ; k11 := a11 ; k12 := a12 ]}" := + (<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]> ( + <[ k5 := a5 ]> ( <[ k6 := a6 ]> ( <[ k7 := a7 ]> ( <[ k8 := a8 ]> ( + <[ k9 := a9 ]> ( <[ k10 := a10 ]> ( <[ k11 := a11 ]>{[ k12 := a12 ]}))))))))))) + (at level 1, format + "{[ '[hv' '[' k1 := a1 ; ']' '/' '[' k2 := a2 ; ']' '/' '[' k3 := a3 ; ']' '/' '[' k4 := a4 ; ']' '/' '[' k5 := a5 ; ']' '/' '[' k6 := a6 ; ']' '/' '[' k7 := a7 ; ']' '/' '[' k8 := a8 ; ']' '/' '[' k9 := a9 ; ']' '/' '[' k10 := a10 ; ']' '/' '[' k11 := a11 ; ']' '/' '[' k12 := a12 ']' ']' ]}") : stdpp_scope. +Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ; k9 := a9 ; k10 := a10 ; k11 := a11 ; k12 := a12 ; k13 := a13 ]}" := + (<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]> ( + <[ k5 := a5 ]> ( <[ k6 := a6 ]> ( <[ k7 := a7 ]> ( <[ k8 := a8 ]> ( + <[ k9 := a9 ]> ( <[ k10 := a10 ]> ( <[ k11 := a11 ]> ( <[ k12 := a12 ]>{[ k13 := a13 ]})))))))))))) + (at level 1, format + "{[ '[hv' '[' k1 := a1 ; ']' '/' '[' k2 := a2 ; ']' '/' '[' k3 := a3 ; ']' '/' '[' k4 := a4 ; ']' '/' '[' k5 := a5 ; ']' '/' '[' k6 := a6 ; ']' '/' '[' k7 := a7 ; ']' '/' '[' k8 := a8 ; ']' '/' '[' k9 := a9 ; ']' '/' '[' k10 := a10 ; ']' '/' '[' k11 := a11 ; ']' '/' '[' k12 := a12 ; ']' '/' '[' k13 := a13 ']' ']' ]}") : stdpp_scope. + +(** The function delete [delete k m] should delete the value at key [k] in +[m]. If the key [k] is not a member of [m], the original map should be +returned. *) +Class Delete (K M : Type) := delete: K → M → M. +Global Hint Mode Delete - ! : typeclass_instances. +Global Instance: Params (@delete) 4 := {}. +Global Arguments delete _ _ _ !_ !_ / : simpl nomatch, assert. + +(** The function [alter f k m] should update the value at key [k] using the +function [f], which is called with the original value. *) +Class Alter (K A M : Type) := alter: (A → A) → K → M → M. +Global Hint Mode Alter - - ! : typeclass_instances. +Global Instance: Params (@alter) 4 := {}. +Global Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch, assert. + +(** The function [partial_alter f k m] should update the value at key [k] using the +function [f], which is called with the original value at key [k] or [None] +if [k] is not a member of [m]. The value at [k] should be deleted if [f] +yields [None]. *) +Class PartialAlter (K A M : Type) := + partial_alter: (option A → option A) → K → M → M. +Global Hint Mode PartialAlter - - ! : typeclass_instances. +Global Instance: Params (@partial_alter) 4 := {}. +Global Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch, assert. + +(** The function [dom m] should yield the domain of [m]. That is a finite +set of type [D] that contains the keys that are a member of [m]. +[D] is an output of the typeclass, i.e., there can be only one instance per map +type [M]. *) +Class Dom (M D : Type) := dom: M → D. +Global Hint Mode Dom ! - : typeclass_instances. +Global Instance: Params (@dom) 3 := {}. +Global Arguments dom : clear implicits. +Global Arguments dom {_ _ _} !_ / : simpl nomatch, assert. + +(** The function [merge f m1 m2] should merge the maps [m1] and [m2] by +constructing a new map whose value at key [k] is [f (m1 !! k) (m2 !! k)].*) +Class Merge (M : Type → Type) := + merge: ∀ {A B C}, (option A → option B → option C) → M A → M B → M C. +Global Hint Mode Merge ! : typeclass_instances. +Global Instance: Params (@merge) 4 := {}. +Global Arguments merge _ _ _ _ _ _ !_ !_ / : simpl nomatch, assert. + +(** The function [union_with f m1 m2] is supposed to yield the union of [m1] +and [m2] using the function [f] to combine values of members that are in +both [m1] and [m2]. *) +Class UnionWith (A M : Type) := + union_with: (A → A → option A) → M → M → M. +Global Hint Mode UnionWith - ! : typeclass_instances. +Global Instance: Params (@union_with) 3 := {}. +Global Arguments union_with {_ _ _} _ !_ !_ / : simpl nomatch, assert. + +(** Similarly for intersection and difference. *) +Class IntersectionWith (A M : Type) := + intersection_with: (A → A → option A) → M → M → M. +Global Hint Mode IntersectionWith - ! : typeclass_instances. +Global Instance: Params (@intersection_with) 3 := {}. +Global Arguments intersection_with {_ _ _} _ !_ !_ / : simpl nomatch, assert. + +Class DifferenceWith (A M : Type) := + difference_with: (A → A → option A) → M → M → M. +Global Hint Mode DifferenceWith - ! : typeclass_instances. +Global Instance: Params (@difference_with) 3 := {}. +Global Arguments difference_with {_ _ _} _ !_ !_ / : simpl nomatch, assert. + +Elpi AddClasses IntersectionWith DifferenceWith. +Definition intersection_with_list `{IntersectionWith A M} + (f : A → A → option A) : M → list M → M := fold_right (intersection_with f). +Global Arguments intersection_with_list _ _ _ _ _ !_ / : assert. + +(** * Notations for lattices. *) +(** SqSubsetEq registers the "canonical" partial order for a type, and is used +for the \sqsubseteq symbol. *) +Class SqSubsetEq A := sqsubseteq: relation A. +Global Hint Mode SqSubsetEq ! : typeclass_instances. +Global Instance: Params (@sqsubseteq) 2 := {}. +Infix "⊑" := sqsubseteq (at level 70) : stdpp_scope. +Notation "(⊑)" := sqsubseteq (only parsing) : stdpp_scope. +Notation "( x ⊑.)" := (sqsubseteq x) (only parsing) : stdpp_scope. +Notation "(.⊑ y )" := (λ x, sqsubseteq x y) (only parsing) : stdpp_scope. + +Infix "⊑@{ A }" := (@sqsubseteq A _) (at level 70, only parsing) : stdpp_scope. +Notation "(⊑@{ A } )" := (@sqsubseteq A _) (only parsing) : stdpp_scope. + +(** [sqsubseteq] does not take precedence over the stdlib's instances (like [eq], +[impl], [iff]) or std++'s [equiv]. +We have [eq] (at 100) < [≡] (at 150) < [⊑] (at 200). *) +Elpi AddClasses SqSubsetEq. +Global Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑@{A}) | 200 := {}. + +Global Hint Extern 0 (_ ⊑ _) => reflexivity : core. + +Class Meet A := meet: A → A → A. +Global Hint Mode Meet ! : typeclass_instances. +Global Instance: Params (@meet) 2 := {}. +Infix "⊓" := meet (at level 40) : stdpp_scope. +Notation "(⊓)" := meet (only parsing) : stdpp_scope. +Notation "( x ⊓.)" := (meet x) (only parsing) : stdpp_scope. +Notation "(.⊓ y )" := (λ x, meet x y) (only parsing) : stdpp_scope. + +Class Join A := join: A → A → A. +Global Hint Mode Join ! : typeclass_instances. +Global Instance: Params (@join) 2 := {}. +Infix "⊔" := join (at level 50) : stdpp_scope. +Notation "(⊔)" := join (only parsing) : stdpp_scope. +Notation "( x ⊔.)" := (join x) (only parsing) : stdpp_scope. +Notation "(.⊔ y )" := (λ x, join x y) (only parsing) : stdpp_scope. + +Class Top A := top : A. +Global Hint Mode Top ! : typeclass_instances. +Notation "⊤" := top (format "⊤") : stdpp_scope. + +Class Bottom A := bottom : A. +Global Hint Mode Bottom ! : typeclass_instances. +Notation "⊥" := bottom (format "⊥") : stdpp_scope. + + +(** * Axiomatization of sets *) +(** The classes [SemiSet A C], [Set_ A C], and [TopSet A C] axiomatize sets of +type [C] with elements of type [A]. The first class, [SemiSet] does not include +intersection and difference. It is useful for the case of lists, where decidable +equality is needed to implement intersection and difference, but not union. + +Note that we cannot use the name [Set] since that is a reserved keyword. Hence +we use [Set_]. *) +Elpi AddClasses ElemOf Difference Intersection. + +Class SemiSet A C `{ElemOf A C, + Empty C, Singleton A C, Union C} : Prop := { + not_elem_of_empty (x : A) : x ∉@{C} ∅; (* We prove + [elem_of_empty : x ∈@{C} ∅ ↔ False] in [sets.v], which is more convenient for + rewriting. *) + elem_of_singleton (x y : A) : x ∈@{C} {[ y ]} ↔ x = y; + elem_of_union (X Y : C) (x : A) : x ∈ X ∪ Y ↔ x ∈ X ∨ x ∈ Y +}. +Global Hint Mode SemiSet - ! - - - - : typeclass_instances. + +Elpi AddClasses SemiSet. +Class Set_ A C `{ElemOf A C, Empty C, Singleton A C, + Union C, Intersection C, Difference C} : Prop := { + set_semi_set :> SemiSet A C; + elem_of_intersection (X Y : C) (x : A) : x ∈ X ∩ Y ↔ x ∈ X ∧ x ∈ Y; + elem_of_difference (X Y : C) (x : A) : x ∈ X ∖ Y ↔ x ∈ X ∧ x ∉ Y +}. +Global Hint Mode Set_ - ! - - - - - - : typeclass_instances. + +Elpi AddClasses Top Set_. +Class TopSet A C `{ElemOf A C, Empty C, Top C, Singleton A C, + Union C, Intersection C, Difference C} : Prop := { + top_set_set :> Set_ A C; + elem_of_top' (x : A) : x ∈@{C} ⊤; (* We prove [elem_of_top : x ∈@{C} ⊤ ↔ True] + in [sets.v], which is more convenient for rewriting. *) +}. +Global Hint Mode TopSet - ! - - - - - - - : typeclass_instances. + +(** We axiomative a finite set as a set whose elements can be +enumerated as a list. These elements, given by the [elements] function, may be +in any order and should not contain duplicates. *) +Class Elements A C := elements: C → list A. +Global Hint Mode Elements - ! : typeclass_instances. +Global Instance: Params (@elements) 3 := {}. + +(** We redefine the standard library's [In] and [NoDup] using type classes. *) +Inductive elem_of_list {A} : ElemOf A (list A) := + | elem_of_list_here (x : A) l : x ∈ x :: l + | elem_of_list_further (x y : A) l : x ∈ l → x ∈ y :: l. +Global Existing Instance elem_of_list. + +Elpi AddInstances ElemOf. + +Lemma elem_of_list_In {A} (l : list A) x : x ∈ l ↔ In x l. +Proof. + split. + - induction 1; simpl; auto. + - induction l; destruct 1; subst; constructor; auto. +Qed. +Inductive NoDup {A} : list A → Prop := + | NoDup_nil_2 : NoDup [] + | NoDup_cons_2 x l : x ∉ l → NoDup l → NoDup (x :: l). +Elpi Override TC - Proper. + +(* Elpi Print TC_solver. *) +Lemma NoDup_ListNoDup {A} (l : list A) : NoDup l ↔ List.NoDup l. +Proof. + split. + - induction 1; constructor; rewrite <-?elem_of_list_In; auto. + - induction 1; constructor; rewrite ?elem_of_list_In; auto. +Qed. + +Elpi AddAllClasses. + +(** Decidability of equality of the carrier set is admissible, but we add it +anyway so as to avoid cycles in type class search. *) +Class FinSet A C `{ElemOf A C, Empty C, Singleton A C, Union C, + Intersection C, Difference C, Elements A C, EqDecision A} : Prop := { + fin_set_set :> Set_ A C; + elem_of_elements (X : C) x : x ∈ elements X ↔ x ∈ X; + NoDup_elements (X : C) : NoDup (elements X) +}. +Global Hint Mode FinSet - ! - - - - - - - - : typeclass_instances. + +Class Size C := size: C → nat. +Global Hint Mode Size ! : typeclass_instances. +Global Arguments size {_ _} !_ / : simpl nomatch, assert. +Global Instance: Params (@size) 2 := {}. + +(** The class [MonadSet M] axiomatizes a type constructor [M] that can be +used to construct a set [M A] with elements of type [A]. The advantage +of this class, compared to [Set_], is that it also axiomatizes the +the monadic operations. The disadvantage is that not many inhabitants are +possible: we will only provide as inhabitants [propset] and [listset], which are +represented respectively using Boolean functions and lists with duplicates. + +More interesting implementations typically need +decidable equality, or a total order on the elements, which do not fit +in a type constructor of type [Type → Type]. *) +Elpi AddClasses MJoin FMap MRet MBind. + +Class MonadSet M `{∀ A, ElemOf A (M A), + ∀ A, Empty (M A), ∀ A, Singleton A (M A), ∀ A, Union (M A), + !MBind M, !MRet M, !FMap M, !MJoin M} : Prop := { + monad_set_semi_set A :> SemiSet A (M A); + elem_of_bind {A B} (f : A → M B) (X : M A) (x : B) : + x ∈ X ≫= f ↔ ∃ y, x ∈ f y ∧ y ∈ X; + elem_of_ret {A} (x y : A) : x ∈@{M A} mret y ↔ x = y; + elem_of_fmap {A B} (f : A → B) (X : M A) (x : B) : + x ∈ f <$> X ↔ ∃ y, x = f y ∧ y ∈ X; + elem_of_join {A} (X : M (M A)) (x : A) : + x ∈ mjoin X ↔ ∃ Y : M A, x ∈ Y ∧ Y ∈ X +}. + +(** The [Infinite A] class axiomatizes types [A] with infinitely many elements. +It contains a function [fresh : list A → A] that given a list [xs] gives an +element [fresh xs ∉ xs]. + +We do not directly make [fresh] a field of the [Infinite] class, but use a +separate operational type class [Fresh] for it. That way we can overload [fresh] +to pick fresh elements from other data structure like sets. See the file +[fin_sets], where we define [fresh : C → A] for any finite set implementation +[FinSet C A]. + +Note: we require [fresh] to respect permutations, which is needed to define the +aforementioned [fresh] function on finite sets that respects set equality. + +Instead of instantiating [Infinite] directly, consider using [max_infinite] or +[inj_infinite] from the [infinite] module. *) +Class Fresh A C := fresh: C → A. +Global Hint Mode Fresh - ! : typeclass_instances. +Global Instance: Params (@fresh) 3 := {}. +Global Arguments fresh : simpl never. + +Elpi AddClasses Fresh. +Class Infinite A := { + infinite_fresh :> Fresh A (list A); + infinite_is_fresh (xs : list A) : fresh xs ∉ xs; + infinite_fresh_Permutation :> Proper (@Permutation A ==> (=)) fresh; +}. +Global Hint Mode Infinite ! : typeclass_instances. +Global Arguments infinite_fresh : simpl never. + +(** * Miscellaneous *) +Class Half A := half: A → A. +Global Hint Mode Half ! : typeclass_instances. +Notation "½" := half (format "½") : stdpp_scope. +Notation "½*" := (fmap (M:=list) half) : stdpp_scope. + +(* + Ad hoc rule for the Inj on the form + Inj ?R1 ?R3 (fun ?x => ...). + We suppose in this case to work with the + compose of two function + (usefull case here: https://github.com/FissoreD/myStdpp/blob/main/stdpp/numbers.v#L1068) +*) + +Elpi Accumulate tc.db lp:{{ + shorten tc-elpi.apps.tc.tests.bigTest.{tc-Inj, tc-Inj2}. + % shorten tc-bigTest.{tc-Inj, tc-Inj2}. + :after "lastHook" + tc-Inj A B R1 R3 F S :- + F = (fun _ _ _), !, + G = {{ compose _ _ }}, + coq.unify-eq G F ok, + tc-Inj A B R1 R3 G S. + + :after "lastHook" + tc-Inj A B R1 R3 {{S}} S :- + tc-Inj A B R1 R3 {{PeanoNat.Nat.succ}} S. + + :after "lastHook" + tc-Inj T1 T2 R1 R3 (app L) S :- + std.last L Last, + coq.typecheck Last Ty ok, + std.drop-last 1 L Firsts, + if (Firsts = [F]) true (F = app Firsts), + S = {{@inj2_inj_2 _ _ _ _ _ _ lp:F lp:S1 lp:Last}}, + tc-Inj2 Ty T1 T2 _ R1 R3 F S1. + + % :after "lastHook" + % tc {{ Inj _ _ lp:{{app L}} }} S :- + % L = [_,_,_ |_], + % std.last L Last, + % std.drop-last 1 L Firsts, + % App = app [app Firsts, Last], + % tc {{Inj _ _ lp:App}} S. +}}. +Elpi Typecheck TC_solver. + +Elpi AddInstances Inj Comm Inj2. \ No newline at end of file diff --git a/apps/tc/tests/compile_add_pred.v b/apps/tc/tests/compile_add_pred.v new file mode 100644 index 000000000..1f10a1a7e --- /dev/null +++ b/apps/tc/tests/compile_add_pred.v @@ -0,0 +1,127 @@ +From elpi Require Import elpi. + +Elpi Db tc.db lp:{{ + pred classes i:gref. + + pred bool->mode-term i:bool, o:string. + bool->mode-term tt "i:term". + bool->mode-term ff "o:term". + + pred modes->string i:list bool, o:string. + modes->string L S :- + std.map L bool->mode-term L', + std.string.concat "," L' S. + + pred list-init i:int, i:(int -> A -> prop), o:list A. + list-init N _ _ :- N < 0, std.fatal-error "list-init negative length". + list-init 0 _ [] :- !. + list-init N F [A | TL] :- + F N A, N1 is N - 1, list-init N1 F TL. + + pred fail->bool i:prop, o:bool. + fail->bool P ff :- P, !. + fail->bool _ tt. + + pred make-tc-modes i:int, o:string. + make-tc-modes NB_args ModesStr :- + list-init NB_args (x\r\ fail->bool (x = 1) r) ModesBool, + modes->string ModesBool ModesStr. + + pred gref->string-no-path i:gref, o:string. + gref->string-no-path Gr S :- + coq.gref->id Gr S', + S is "tc-" ^ S'. + + pred add-tc-pred i:gref, i:int. + add-tc-pred Gr NbArgs :- + not (classes Gr), + make-tc-modes NbArgs Modes, + gref->string-no-path Gr GrStr, + D is "pred " ^ GrStr ^ " " ^ Modes ^ ".", + coq.elpi.add-predicate "tc.db" D, + coq.elpi.accumulate _ "tc.db" (clause _ _ (classes Gr)). + add-tc-pred _ _. + + pred make-tc i:term, i:term, i:list prop, o:prop. + make-tc Ty Inst Hyp Clause :- + app [global TC | TL] = Ty, + gref->string-no-path TC TC_Str, + std.append TL [Inst] Args, + std.length Args ArgsLen, + add-tc-pred TC ArgsLen, + coq.elpi.predicate TC_Str Args Q, + Clause = (Q :- Hyp). + + pred app-has-class i:term, o:gref. + app-has-class (prod _ _ T) C :- pi x\ app-has-class (T x) C. + app-has-class (app [global T|_]) T :- coq.TC.class? T. + + pred compile i:term, i:term, i:list prop, i:list term, o:prop. + compile (prod _ T F) I ListRHS ListVar (pi x\ C x) :- !, + pi p cond\ sigma Clause L\ + if (app-has-class T _) (compile T p [] [] Clause, L = [Clause | ListRHS]) (L = ListRHS), + compile (F p) I L [p | ListVar] (C p). + compile Ty I Premises ListVar Clause :- !, + std.rev Premises PremisesRev, + coq.mk-app I {std.rev ListVar} AppInst, + make-tc Ty AppInst PremisesRev Clause. +}}. + +Elpi Command addClass. +Elpi Accumulate Db tc.db. +Elpi Accumulate lp:{{ + main [str TC_Name] :- + coq.locate TC_Name TC_Gr, + coq.env.typeof TC_Gr TC_Ty, + coq.count-prods TC_Ty N', + N is N' + 1, % Plus one for the solution + add-tc-pred TC_Gr N. +}}. +Elpi Typecheck. + +Elpi Command compile. +Elpi Accumulate Db tc.db. +Elpi Accumulate lp:{{ + main [str InstName] :- + coq.locate InstName InstGr, + coq.env.typeof InstGr InstTy, + compile InstTy (global InstGr) [] [] Cl, + coq.say Cl, + coq.elpi.accumulate _ "tc.db" (clause _ _ Cl). +}}. +Elpi Typecheck. + +Elpi Tactic solver. +Elpi Accumulate Db tc.db. +Elpi Accumulate lp:{{ + msolve L N :- !, + coq.ltac.all (coq.ltac.open solve) {std.rev L} N. + + solve (goal _ _ Ty Sol _ as G) GL :- + var Sol, + Ty = app [global TC | TL'], + std.append TL' [X] TL, + if (coq.elpi.predicate {gref->string-no-path TC} TL Q, Q) + ( + refine X G GL; + coq.say "illtyped solution:" {coq.term->string X} + ) + (GL = [seal G]). +}}. +Elpi Typecheck. + +Class EqSimpl (T : Type) := {eqb : T -> T -> bool}. + +Global Instance EqU : EqSimpl unit := { eqb A B := true }. +Global Instance EqP {A B: Type} `(EqSimpl A, EqSimpl B) : EqSimpl (A * B) := { eqb A B := true }. + +Elpi addClass EqSimpl. +Elpi compile EqU. +Elpi compile EqP. + +Elpi Override TC solver All. + +Check (_ : EqSimpl unit). +Check (_ : EqSimpl (unit * unit)). + + diff --git a/apps/tc/tests/contextDeepHierarchy.v b/apps/tc/tests/contextDeepHierarchy.v new file mode 100644 index 000000000..daa154696 --- /dev/null +++ b/apps/tc/tests/contextDeepHierarchy.v @@ -0,0 +1,38 @@ +From elpi.apps Require Import tc. +Unset Typeclass Resolution For Conversion. +Unset TC_NameFullPath. +(* Elpi Debug "simple-compiler". *) +Elpi Override TC TC_solver All. + + +Class X (A: Type). +Class Y (A: Type). +Class Z (A: Type). +Elpi AddClasses X Y Z. + +Local Instance Inst1@{i} {A: Type@{i}} : X A -> Y A. Qed. +Local Instance Inst2@{i} (A : Type@{i}): (forall A : Type@{i}, X A -> Y A) -> Z A. Qed. + +Elpi AddAllInstances. + +(* Elpi Print TC_solver "TC_solver.html" ".*: [0-9]+.*". *) + +(*Print Universes.*) + +Set Printing Universes. Set Printing All. + +(* TODO: here Elpi Trace Fails... *) +(* Elpi Trace Browser. *) + +Goal forall A, Z A. + intros. + apply _. + + (* Elpi Override TC TC_solver None. *) + (*refine (fun (A : Type) => Inst2 A (@Inst1)).*) + (* apply _. *) + Show Proof. +Qed. + +(* Good : (fun A : Type => Inst2 A (@Inst1)) *) +(* Not Good : (fun A : Type => Inst2 A (fun (H : ?elpi_evar) (H0 : ?elpi_evar0@{y:=H}) => Inst1 H0)) *) \ No newline at end of file diff --git a/apps/tc/tests/cyclicTC_jarl.v b/apps/tc/tests/cyclicTC_jarl.v new file mode 100644 index 000000000..c6a1b41f0 --- /dev/null +++ b/apps/tc/tests/cyclicTC_jarl.v @@ -0,0 +1,69 @@ +From elpi.apps Require Import tc. +Elpi Debug "simple-compiler". +Unset TC_NameFullPath. + +Elpi Override TC TC_solver All. + +Class A (T1 : Type). +Class B (T1 : Type). + +Global Instance instA' (T1 : Type) (T2 : Type) : A bool. Qed. +Global Instance instA (T1 : Type) `(B T1) : A T1. Qed. + +Global Instance instB (T1 : Type) `(A T1) : B T1. Qed. +Global Instance instB' : B nat . Qed. + +Elpi Accumulate tc.db lp:{{ + pred explored_gref o:gref. + + pred should_fail i:list gref, i:gref, i:gref. + should_fail [] _ _. + should_fail [Current | Tl] Current BlackElt :- !, + if (std.mem Tl BlackElt) fail true. + should_fail [_ | Tl] Current BlackElt :- !, + should_fail Tl Current BlackElt. + + pred already_explored i:gref, i:gref. + already_explored Current BlackElt :- + std.findall (explored_gref _) As, + std.map As (x\r\ x = explored_gref r) As', + should_fail As' Current BlackElt. + + pred get_other i:gref, o:gref. + + pred under_extra i:gref, i:list prop, o:list prop. + under_extra A B C :- std.map B (x\r\ (explored_gref A => x) = r) C1, + C = [sigma x\ get_other A x, already_explored A x | C1]. + + :after "firstHook" + make-tc IsHead Ty Inst Hyp Clause :- !, + app [global TC | TL] = Ty, + gref->string-no-path TC TC_Str, + std.append TL [Inst] Args, + coq.elpi.predicate TC_Str Args Q, + if (not IsHead) (Hyp = Hyp') (under_extra TC Hyp Hyp'), + Clause = (Q :- Hyp'). +}}. +Elpi Typecheck TC_solver. + +Elpi AddAllClasses. +Elpi AddAllInstances. + +Elpi Command AddRecursivelyDependantTC. +Elpi Accumulate Db tc.db. +Elpi Accumulate lp:{{ + main [trm (global A), trm (global B)] :- + coq.elpi.accumulate _ "tc.db" + (clause _ _ (get_other A B)), + coq.elpi.accumulate _ "tc.db" + (clause _ _ (get_other B A)). + main L :- coq.say L. +}}. +Elpi Typecheck. + +Elpi AddRecursivelyDependantTC (A) (B). + +Elpi Bound Steps 10000. +Check (_ : B bool). +Check (_ : A nat). + diff --git a/apps/tc/tests/eqSimpl.v b/apps/tc/tests/eqSimpl.v new file mode 100644 index 000000000..07948357e --- /dev/null +++ b/apps/tc/tests/eqSimpl.v @@ -0,0 +1,19 @@ + +From elpi.apps Require Import tc. +From elpi.apps Require Import eqSimplDef. + +Elpi Debug "simple-compiler". + +Set AddModes. + +Elpi Override TC TC_solver Only Eqb. +Elpi AddClasses Eqb. +Elpi AddInstances Eqb. +Elpi Override TC TC_solver All. +Fail Check (fun n m : _ => eqb n m). + +Elpi Trace Browser. +Goal (tt, (tt, true)) == (tt, (tt, true)) = true. + easy. +Qed. + diff --git a/apps/tc/tests/eqSimplDef.v b/apps/tc/tests/eqSimplDef.v new file mode 100644 index 000000000..c2e1854d8 --- /dev/null +++ b/apps/tc/tests/eqSimplDef.v @@ -0,0 +1,20 @@ +Require Import Bool Arith List. + +Class Eqb A : Type := eqb : A -> A -> bool. +Global Hint Mode Eqb + : typeclass_instances. + +Notation " x == y " := (eqb x y) (no associativity, at level 70). + +Global Instance eqU : Eqb unit := { eqb x y := true }. +Global Instance eqB : Eqb bool := { eqb x y := if x then y else negb y }. +Global Instance eqP {A B} `{Eqb A} `{Eqb B} : Eqb (A * B) := { + eqb x y := (fst x == fst y) && (snd x == snd y) }. +(* Global Instance eqN : Eqb nat := { + eqb := fix add (a: nat) b := match a, b with + | 0, 0 => true + | S a, S b => add a b + | _, _ => false + end }. + + +Check (forall n, n + n == 2 * n = true). *) \ No newline at end of file diff --git a/apps/tc/tests/importOrder/f1.v b/apps/tc/tests/importOrder/f1.v new file mode 100644 index 000000000..a2b17d269 --- /dev/null +++ b/apps/tc/tests/importOrder/f1.v @@ -0,0 +1,7 @@ +From elpi.apps.tc.tests.importOrder Require Export sameOrderCommand. + +Class A (T : Set) := f : T -> T. + +Elpi AddClasses A. + +Elpi SameOrderImport. \ No newline at end of file diff --git a/apps/tc/tests/importOrder/f2a.v b/apps/tc/tests/importOrder/f2a.v new file mode 100644 index 000000000..0fcf326c3 --- /dev/null +++ b/apps/tc/tests/importOrder/f2a.v @@ -0,0 +1,11 @@ +From elpi.apps.tc.tests.importOrder Require Export f1. +From elpi.apps.tc.tests.importOrder Require Export sameOrderCommand. + + +Global Instance f2aa : A nat := {f x := x}. +Global Instance f2ab : A nat := {f x := x}. +Global Instance f2ac : A nat := {f x := x}. +Global Instance f2ad : A nat := {f x := x}. + +Elpi AddInstances A. +(* Elpi SameOrderImport. *) \ No newline at end of file diff --git a/apps/tc/tests/importOrder/f2b.v b/apps/tc/tests/importOrder/f2b.v new file mode 100644 index 000000000..2f87a80aa --- /dev/null +++ b/apps/tc/tests/importOrder/f2b.v @@ -0,0 +1,9 @@ +From elpi.apps.tc.tests.importOrder Require Export f1. + +Global Instance f2ba : A nat := {f x := x}. +Global Instance f2bb : A nat := {f x := x}. +Global Instance f2bc : A nat := {f x := x}. +Global Instance f2bd : A nat := {f x := x}. + +Elpi AddInstances A. +(* Elpi SameOrderImport. *) diff --git a/apps/tc/tests/importOrder/f3a.v b/apps/tc/tests/importOrder/f3a.v new file mode 100644 index 000000000..c32eac7c1 --- /dev/null +++ b/apps/tc/tests/importOrder/f3a.v @@ -0,0 +1,7 @@ +From elpi.apps.tc.tests.importOrder Require Import f2a. +From elpi.apps.tc.tests.importOrder Require Import f2b. +(* Elpi AddAllInstances. *) +Print HintDb typeclass_instances. + +Elpi Print TC_solver "tests/f3a". +Elpi SameOrderImport. diff --git a/apps/tc/tests/importOrder/f3b.v b/apps/tc/tests/importOrder/f3b.v new file mode 100644 index 000000000..dce7ecc47 --- /dev/null +++ b/apps/tc/tests/importOrder/f3b.v @@ -0,0 +1,7 @@ +From elpi.apps.tc.tests.importOrder Require Import f2b. +From elpi.apps.tc.tests.importOrder Require Import f2a. +(* Elpi AddAllInstances. *) +Print HintDb typeclass_instances. + +Elpi Print TC_solver "tests/f3b". +Elpi SameOrderImport. \ No newline at end of file diff --git a/apps/tc/tests/importOrder/f3c.v b/apps/tc/tests/importOrder/f3c.v new file mode 100644 index 000000000..1027dcd20 --- /dev/null +++ b/apps/tc/tests/importOrder/f3c.v @@ -0,0 +1,39 @@ +From elpi.apps.tc.tests.importOrder Require Export f1. + +Global Instance f3a : A nat := {f x := x}. +Global Instance f3b : A nat := {f x := x}. +Global Instance f3c : A nat := {f x := x}. +Elpi AddAllInstances. +Elpi SameOrderImport. + +Section S1. + Global Instance f3d : A nat := {f x := x}. + Global Instance f3e : A nat := {f x := x}. + Global Instance f3f : A nat := {f x := x}. + Elpi AddAllInstances. + Elpi SameOrderImport. +MySectionEnd. +Elpi SameOrderImport. + +Section S2. + Context (T : Set). + Global Instance f3g : A T := {f x := x}. + Elpi AddAllInstances. + Elpi SameOrderImport. +MySectionEnd. +Elpi SameOrderImport. + +Section S3. + Context (T : Set). + Global Instance f3g2 : A (T: Set) := {f x := x}. + + Global Instance f3h T1 T2 `(A T1, A T2) : A (T1 * T2) := {f x := x}. + + Global Instance f3g3 : A (T: Set) := {f x := x}. + Global Instance f3g4 : A (T: Set) | 10 := {f x := x}. + + Elpi AddAllInstances. + Elpi SameOrderImport. +MySectionEnd. + +Elpi SameOrderImport. \ No newline at end of file diff --git a/apps/tc/tests/importOrder/f3d.v b/apps/tc/tests/importOrder/f3d.v new file mode 100644 index 000000000..4b1a9bdcb --- /dev/null +++ b/apps/tc/tests/importOrder/f3d.v @@ -0,0 +1,31 @@ +From elpi.apps.tc.tests.importOrder Require Export f1. +From elpi.apps.tc.tests.importOrder Require Import f2b. +Elpi SameOrderImport. + +Global Instance f3a' T1 T2 `(A T1, A T2) : A (T1 * T2) := {f x := x}. +Elpi AddInstances A. + +Elpi SameOrderImport. +Module M4'. + (* From elpi.apps.tc.tests.importOrder Require Import f2a. *) + Elpi SameOrderImport. + + Global Instance f3a : A nat := {f x := x}. + Elpi AddInstances f3a. + + Section S1. + Global Instance f3b : A nat := {f x := x}. + Elpi AddInstances f3b. + Section S1'. + Global Instance f3c : A nat := {f x := x}. + Elpi AddInstances f3c. + MySectionEnd. + MySectionEnd. + + Elpi SameOrderImport. + + Section S2. + Global Instance f3h T1 T2 `(A T1, A T2) : A (T1 * T2) := {f x := x}. + Elpi AddInstances f3h. + MySectionEnd. +End M4'. \ No newline at end of file diff --git a/apps/tc/tests/importOrder/f3e.v b/apps/tc/tests/importOrder/f3e.v new file mode 100644 index 000000000..fbffe2a68 --- /dev/null +++ b/apps/tc/tests/importOrder/f3e.v @@ -0,0 +1,25 @@ +From elpi.apps.tc.tests.importOrder Require Export f1. +From elpi.apps.tc.tests.importOrder Require Import f2b. + +Global Instance f3a' T1 T2 `(A T1, A T2) : A (T1 * T2) := {f x := x}. +Elpi AddAllInstances. +Elpi SameOrderImport. +Module M4'. + From elpi.apps.tc.tests.importOrder Require Import f2a. + + Global Instance f3a : A nat := {f x := x}. + + Section S1. + Global Instance f3b : A nat := {f x := x}. + Section S1'. + Global Instance f3c : A nat := {f x := x}. + MySectionEnd. + MySectionEnd. + + Section S2. + Global Instance f3h T1 T2 `(A T1, A T2) : A (T1 * T2) := {f x := x}. + MySectionEnd. +End M4'. + +Elpi AddAllInstances. +Elpi SameOrderImport. \ No newline at end of file diff --git a/apps/tc/tests/importOrder/f3f.v b/apps/tc/tests/importOrder/f3f.v new file mode 100644 index 000000000..d183876c1 --- /dev/null +++ b/apps/tc/tests/importOrder/f3f.v @@ -0,0 +1,17 @@ +From elpi.apps.tc.tests.importOrder Require Import f1. + +Section S1. + Context (T : Set). + Global Instance f3a : A T := {f x := x}. + Elpi AddInstances f3a. + Elpi SameOrderImport. + + Section S2. + Context (T1 : Set). + Global Instance f3b : A T1 := {f x := x}. + Elpi AddInstances f3b. + MySectionEnd. + + Elpi SameOrderImport. +MySectionEnd. +Elpi SameOrderImport. \ No newline at end of file diff --git a/apps/tc/tests/importOrder/f3g.v b/apps/tc/tests/importOrder/f3g.v new file mode 100644 index 000000000..1650e3416 --- /dev/null +++ b/apps/tc/tests/importOrder/f3g.v @@ -0,0 +1,11 @@ +From elpi.apps.tc.tests.importOrder Require Export f1. + +Module M8. + Class Classe (A: Type) (B: Type). + Elpi AddClasses Classe. + + Global Instance I (a b c d: Type): Classe a a -> Classe b c. Admitted. + + Elpi AddAllInstances. + Elpi SameOrderImport. +End M8. diff --git a/apps/tc/tests/importOrder/f4.v b/apps/tc/tests/importOrder/f4.v new file mode 100644 index 000000000..62681ca25 --- /dev/null +++ b/apps/tc/tests/importOrder/f4.v @@ -0,0 +1 @@ +From elpi.apps.tc.tests.importOrder Require Import f3f. \ No newline at end of file diff --git a/apps/tc/tests/importOrder/sameOrderCommand.v b/apps/tc/tests/importOrder/sameOrderCommand.v new file mode 100644 index 000000000..1e7980554 --- /dev/null +++ b/apps/tc/tests/importOrder/sameOrderCommand.v @@ -0,0 +1,14 @@ +From elpi Require Export tc. + +Elpi Command SameOrderImport. +Elpi Accumulate Db tc.db. +Elpi Accumulate lp:{{ + main _ :- + std.findall (instance _ _ _) RulesInst, + coq.TC.db DB_tc-inst, + std.map RulesInst (x\inst\ instance _Path inst _TC = x) RulesElpi, + std.map DB_tc-inst (x\inst\ tc-instance inst _ = x) RulesCoq, + if (RulesElpi = RulesCoq) true ( + coq.error "Error in import order\n" + "Expected :" RulesCoq "\nFound :" RulesElpi). +}}. \ No newline at end of file diff --git a/apps/tc/tests/included_proof.v b/apps/tc/tests/included_proof.v new file mode 100644 index 000000000..f78f0d54f --- /dev/null +++ b/apps/tc/tests/included_proof.v @@ -0,0 +1,31 @@ +From elpi.apps Require Import tc. + +Class EqDec (A : Type) := + { eqb : A -> A -> bool ; + eqb_leibniz : forall x y, eqb x y = true -> x = y }. + +Generalizable Variables A. + +Class Ord `(E : EqDec A) := { le : A -> A -> bool }. + +Class C (A : Set). + +Global Instance cInst `{e: EqDec nat} : Ord e -> C nat. Admitted. + +Elpi AddAllClasses. + +(* + We want to be sure that cInst when compiled has only one hypothesis: (Ord e). + We don't want the hypothesis {e : EqDec nat} since it will be verified by (Ord e) +*) +(* TODO: it should not fail *) +Fail Elpi Query TC_solver lp:{{ + compile {{:gref cInst}} _ _ CL, + CL = (pi a\ pi b\ (_ :- (Hyp a b))), + coq.say Hyp, + pi a b\ + expected-found (do _) (Hyp a b). +}}. + + + diff --git a/apps/tc/tests/injTest.v b/apps/tc/tests/injTest.v new file mode 100644 index 000000000..3c9263ad0 --- /dev/null +++ b/apps/tc/tests/injTest.v @@ -0,0 +1,124 @@ +From elpi.apps Require Import tc. +From Coq Require Import Morphisms RelationClasses List Bool Setoid Peano Utf8. + +Generalizable All Variables. + +Class Inj {A B} (R : relation A) (S : relation B) (f : A -> B) := + inj x y : S (f x) (f y) -> R x y. + +Class Inj2 {A B C} (R1 : relation A) (R2 : relation B) + (S : relation C) (f : A → B → C) : Prop := + inj2 x1 x2 y1 y2 : S (f x1 x2) (f y1 y2) → R1 x1 y1 ∧ R2 x2 y2. + +Elpi Override TC TC_solver Only Inj Inj2. + +Definition gInj x := x + 1. +Definition fInj x := x * 3. + +Axiom eq1 : relation nat. +Axiom eq2 : relation nat. +Axiom eq3 : relation nat. + +Local Instance isInjg : Inj eq3 eq1 gInj. Admitted. + +Local Instance isInjf : Inj eq1 eq3 fInj. Admitted. + +Local Instance isInjf_old : Inj eq1 eq2 fInj. Admitted. +Local Instance isInjg_old : Inj eq2 eq3 gInj. Admitted. + +Local Instance isInjf_eq : Inj eq eq fInj. Admitted. +Local Instance isInjg_eq : Inj eq eq gInj. Admitted. + +Local Instance id_inj {A} : Inj eq eq (@id A). Admitted. +Local Instance inl_inj {A B} : Inj eq eq (@inl A B). Admitted. +Local Instance inr_inj {A B} : Inj eq eq (@inr A B). Admitted. + +Definition compose {T1 T2 T3: Type} (g: T2 -> T3) (f : T1 -> T2) (x: T1) := g(f x). +Local Instance compose_inj {A B C} R1 R2 R3 (f : A -> B) (g : B -> C) : + Inj R1 R2 f -> Inj R2 R3 g -> Inj R1 R3 (compose g f). +Admitted. + +Elpi AddAllClasses. + +Elpi AddInstances Inj. + +Goal exists A B, Inj A B (compose gInj fInj). Admitted. + + +Goal forall (T1 T2 : Type) (f: T1 -> T2), + let r := Inj eq eq f in + let x := true in + (if x then r else r) -> Inj eq eq f. + intros ? ? f r x H. + unfold x, r in H. + apply _. +Qed. + +Goal forall (T1 T2 : Type) (f: T1 -> T2), + let r := Inj eq eq f in + let b := true in + let cond := (match b with + | true => r + | false => f = f end) in + cond -> Inj eq eq f. + intros. + unfold cond in H. + simpl in H. + unfold r in H. + apply _. +Qed. + +Local Instance inj2_inj_1 `{Inj2 A B C R1 R2 R3 ff} y : Inj R1 R3 (λ x, ff x y). +Admitted. + +Global Instance inj2_inj_2 `{Inj2 A B C R1 R2 R3 ff} x : Inj R2 R3 (ff x). +Admitted. + +Elpi AddClasses Inj2. +Elpi AddInstances Inj. + +Goal Inj2 eq eq eq Nat.mul -> Inj eq eq (Nat.mul 0). + intros. + apply _. +Qed. + +Goal Inj2 eq eq eq Nat.add -> Inj eq eq (fun x => Nat.add x 0). +intros. +apply _. +Qed. + +Definition p (T : Type) := @pair T T. + +Goal Inj eq eq (compose fInj gInj). +Proof. +apply _. +Qed. + +Elpi Print TC_solver. +Set Warnings "+elpi". + + +Elpi Accumulate tc.db lp:{{ + shorten tc-elpi.apps.tc.tests.injTest.{tc-Inj}. + % shorten tc-injTest.{tc-Inj}. + tc-Inj T1 T2 R1 R3 F S :- + F = (fun _ _ _), + G = {{ compose _ _ }}, + coq.unify-eq G F ok, + tc-Inj T1 T2 R1 R3 G S. +}}. + +Elpi Typecheck TC_solver. + +Goal Inj eq eq (compose fInj gInj). apply _. Qed. +Goal Inj eq eq (fun x => fInj (gInj x)). apply _. Qed. + +Goal forall (A: Type) (x: A -> A), + let y := Inj eq eq x in + let z := y in z -> + Inj eq eq (compose x x). +Proof. + intros T x y z H. + unfold z, y in H. + apply _. +Qed. \ No newline at end of file diff --git a/apps/tc/tests/mode_no_repetion.v b/apps/tc/tests/mode_no_repetion.v new file mode 100644 index 000000000..d6ffcf07c --- /dev/null +++ b/apps/tc/tests/mode_no_repetion.v @@ -0,0 +1,46 @@ +From elpi.apps Require Import tc. +From elpi.apps.tc.tests Require Import eqSimplDef. +From elpi.apps.tc Extra Dependency "base.elpi" as base. +From elpi.apps.tc Extra Dependency "tc_aux.elpi" as tc_aux. + +Elpi Debug "simple-compiler". + +Set AddModes. +Elpi AddClasses Eqb. +Elpi AddInstances Eqb. + +(* + Tests if the modes of TC are added exactly one time + to the DB +*) + +Elpi Command len_test. +Elpi Accumulate Db tc.db. +Elpi Accumulate File base. +Elpi Accumulate File tc_aux. +Elpi Accumulate lp:{{ + pred only-one-tc i:gref. + only-one-tc Gr :- + not (app-has-class {coq.env.typeof Gr}). + only-one-tc (indt _). + only-one-tc (const _ as GR) :- + std.findall (classes GR _) Cl, + std.assert! ({std.length Cl} = 1) + "Unexpected number of instances". + only-one-tc Gr :- coq.error "Should not be here" Gr. + + main [str "all_only_one"] :- !, + std.forall {coq.TC.db-tc} only-one-tc. + + main [str E] :- + coq.locate E GR, + only-one-tc GR. +}}. +Elpi Typecheck. + +Elpi len_test Eqb. + +Elpi AddAllClasses. +Elpi AddAllInstances. + +Elpi len_test "all_only_one". \ No newline at end of file diff --git a/apps/tc/tests/nobacktrack.v b/apps/tc/tests/nobacktrack.v new file mode 100644 index 000000000..e0c2db6dd --- /dev/null +++ b/apps/tc/tests/nobacktrack.v @@ -0,0 +1,44 @@ +From elpi.apps Require Import tc. + +Elpi Debug "simple-compiler". +Unset TC_NameFullPath. + +Module A. + + Class C (n : nat) := {}. + Local Instance c_1 : C 1 | 10 := {}. + Local Instance c_2 : C 2 | 1 := {}. + + Class D (n : nat) := {}. + Local Instance d_1 : D 1 := {}. + + Class E (n : nat) := {}. + Local Instance foo {n} : C n -> D n -> E n := {}. + + #[deterministic] Elpi AddClasses C. + Elpi AddClasses D E. + Elpi AddAllInstances. + Elpi Override TC TC_solver All. + + Goal exists n, E n. + eexists. + Fail apply _. + Abort. + +End A. + +Module B. + + Class A (T : Set) := f : T -> T. + #[deterministic] Elpi AddClasses A. + + Global Instance A1 : A bool := {f x := x}. + Global Instance A2 `(A bool) : A (bool * bool) := + {f x := x}. + Global Instance A3 `(A nat) : A (bool * bool) := + {f x := x}. + Elpi AddAllInstances. + + Goal A (bool * bool). apply _. Qed. + +End B. \ No newline at end of file diff --git a/apps/tc/tests/nobacktrack2.v b/apps/tc/tests/nobacktrack2.v new file mode 100644 index 000000000..b47de0d59 --- /dev/null +++ b/apps/tc/tests/nobacktrack2.v @@ -0,0 +1,39 @@ +From Coq Require Import Setoid. + +Module B. + Class Persistent (A: Prop). + Class Separable (A: Prop). + Local Instance persistent_separable P: + Persistent P -> Separable P | 10. + Admitted. + Local Instance and_persistent P Q : + Persistent P -> Persistent Q -> Persistent (P /\ Q) | 0. + Admitted. + Local Instance and_separable P1 P2 : + Separable P1 -> Separable P2 -> Separable (P1 /\ P2) | 0. + Admitted. + + Goal forall (P Q : Prop), Persistent (P /\ Q) <-> Persistent (Q /\ P). + intros. + split. + intros. + apply and_persistent. + . + rewrite and_comm. + destruct Persistent. + + Goal forall (P Q: Prop), Persistent P -> Persistent Q -> Separable (P /\ Q). + apply _. + Qed. + Goal forall (P Q R: Prop), Persistent (P) -> Persistent (R /\ Q) -> Separable (P /\ Q /\ R). + intros. + apply _. + Qed. + + From elpi.apps Require Import tc. + Elpi AddAllInstances. + Elpi Override TC TC_solver All. + Goal forall (P Q R: Prop), Persistent P -> Persistent (Q /\ R) -> Separable (P /\ Q /\ R). + apply _. + Qed. +End B. \ No newline at end of file diff --git a/apps/tc/tests/patternFragment.v b/apps/tc/tests/patternFragment.v new file mode 100644 index 000000000..648e460e5 --- /dev/null +++ b/apps/tc/tests/patternFragment.v @@ -0,0 +1,74 @@ +From elpi.apps Require Import tc. +Elpi Override TC TC_solver All. +Unset TC_NameFullPath. +Set DebugTC. + +Class Y (A: Type). +Class Z (A: Type). +Class Ex (P : Type -> Type) (A: Type). +Elpi AddClasses Y Z Ex. + +Module M4. +Local Instance Inst1: Y (bool * bool). Qed. +Local Instance Inst2 A F: (forall (a b c : Type), Y (F a b) -> Y (F b c)) -> Z A. Qed. +#[local] Elpi AddInstances Inst1 Inst2. +Goal Z bool. + apply _. + Show Proof. + Unshelve. apply nat. + Show Proof. Qed. +End M4. + +Module M5. +Local Instance Inst1: Y (bool * bool). Qed. +Local Instance Inst2 A F (R: Type -> Type -> Type): forall x, + (forall (a : Type), Y (F a)) -> Ex (R x) A. Qed. +#[local] Elpi AddInstances Inst1 Inst2. +Goal forall (A:Type) x (R: Type -> Type -> Type ->Type), Ex (R x x) A. apply _. Qed. +End M5. + +Module M1. +Local Instance Inst1: Y (bool * bool). Qed. +Local Instance Inst2 A F: (forall (a : Type), Y (F a)) -> Z A. Qed. +#[local] Elpi AddInstances Inst1 Inst2. + +(* Elpi Accumulate TC_solver lp:{{ + tc {{:gref Z}} {{Z lp:A}} {{Inst2 lp:A lp:{{fun _ _ F}} lp:S }} :- + pi a\ + tc {{:gref Y}} (app [global {{:gref Y}}, F a]) (Sol a), + (Sol a = {{ lp:S lp:a }} ; (S = fun _ _ Sol)). +}}. *) +Goal forall (A:Type), Z A. apply _. Qed. +End M1. + +Module M2. +Local Instance Inst1: Y (bool * bool). Qed. +Local Instance Inst2 A F: (forall (a: Type), Y (F a)) -> Z A. Qed. +#[local] Elpi AddInstances Inst1 Inst2. +Elpi Print TC_solver. +Goal Z bool. apply _. Qed. +End M2. + +Module M3. +Local Instance Inst1: Y (bool * bool). Qed. +Local Instance Inst2 A F: (forall (a b c d: Type), Y (F b c d)) -> Z A. Qed. +Elpi AddInstances Inst1 Inst2. +Goal Z bool. apply _. Qed. +End M3. + +Module M6. +Local Instance Inst1: Y (bool * bool). Qed. +Local Instance Inst2 A F: (forall (a b c d e f g: Type), Y (F a b c d) -> Y (F e f g a)) -> Z A. Qed. +Elpi AddInstances Inst1 Inst2. +Goal Z bool. apply _. Unshelve. apply nat. Qed. +End M6. + +Module M1b. +Local Instance Inst2 A F: (forall (a : Type), Y (F a)) -> Ex F A. Qed. +Elpi AddInstances Inst2. +Goal forall (A:Type) (f : Type -> Type), (forall x, Y (f x)) -> exists f, Ex f A. intros. eexists. apply _. + Unshelve. + apply A. +Qed. +End M1b. + diff --git a/apps/tc/tests/patternFragmentBug.v b/apps/tc/tests/patternFragmentBug.v new file mode 100644 index 000000000..8570fd7fc --- /dev/null +++ b/apps/tc/tests/patternFragmentBug.v @@ -0,0 +1,57 @@ +From elpi.apps Require Import tc. + +Class X (A: Type). +Class Y (A: Type). +Class Z (A: Type). + +Local Instance Inst1 A: Y (A * A). Qed. +Local Instance Inst2 A F: (forall (a: Type), Y (F a)) -> Z A. Qed. + +Elpi Accumulate TC_solver lp:{{ + :after "firstHook" + solve1 (goal Ctx _ Ty Sol _ as G) _L GL :- !, + var Sol, + % Add's the section's definition to the current context + % in order to add its TC if present + std.map {coq.env.section} (x\r\ sigma F\ coq.env.typeof (const x) F, r = (decl (global (const x)) _ F)) SectionCtx, + ctx->clause {std.append Ctx SectionCtx} Clauses, + % get-last Ty InstFun, + Ty = app [global TC | _], + coq.say Ty, + % coq.say "Clauses" Clauses, + Clauses => if (tc-search-time TC Ty X) + ( + coq.say {coq.term->string X}, + % @no-tc! => coq.elaborate-skeleton X _ X' ok, + % coq.say "Solution " X "end" X' "caio", + % std.assert! (ground_term X') "solution not complete", + my-refine X G GL; + coq.say "illtyped solution:" {coq.term->string X} + ) + (GL = [seal G]). +}}. + +Elpi Accumulate TC_solver lp:{{ + % tc _ A _ :- fail. + + tc _ {{Z lp:A}} {{Inst2 lp:A lp:F lp:S}} :- + F = fun _ {{Type}} F', + S = fun _ {{Type}} S', + pi a\ tc {{:gref Y}} {{Y lp:{{F' a}}}} (S' a). +}}. +Elpi Typecheck TC_solver. + +Elpi Override TC TC_solver All. +Elpi AddAllInstances. +Unset Typeclass Resolution For Conversion. + +Goal Z bool. +intros. +(* TODO: here Elpi Trace Fails... *) +Elpi Trace Browser. + + (* Elpi Override TC TC_solver Only Z. *) + (* Elpi Override TC - Z. *) + apply _. + Show Proof. +Qed. \ No newline at end of file diff --git a/apps/tc/tests/premisesSort/sort1.v b/apps/tc/tests/premisesSort/sort1.v new file mode 100644 index 000000000..3678f25c3 --- /dev/null +++ b/apps/tc/tests/premisesSort/sort1.v @@ -0,0 +1,17 @@ +From elpi.apps.tc.tests.premisesSort Require Import sortCode. + +Class A (S : Type). +Class B (S : Type). +Class C (S : Type). + +Global Instance A1 : A nat. Admitted. +Global Instance A2 : A bool. Admitted. + +Global Instance B1 : B nat. Admitted. + +Global Instance C1 {T : Type} `{A T, B T} : C bool. Admitted. + +(* Simpl example where we do backtrack *) +Goal C bool. + apply _. +Qed. \ No newline at end of file diff --git a/apps/tc/tests/premisesSort/sort2.v b/apps/tc/tests/premisesSort/sort2.v new file mode 100644 index 000000000..8423ac724 --- /dev/null +++ b/apps/tc/tests/premisesSort/sort2.v @@ -0,0 +1,32 @@ +From elpi.apps.tc.tests.premisesSort Require Import sortCode. +Elpi Debug "simple-compiler". +Set AddModes. + +Class A (S : Type). +Class B (S : Type). +Class C (S : Type). + +Global Hint Mode A + : typeclass_instances. + +Global Instance A1 : A nat. Admitted. + +Global Instance B1 : B nat. Admitted. + +(* + Here since the output of T is input in A, we want to reorder + the goals such that the proof of be is computed first. + Question do we want to raise an error or try to rearrange + subgoals in C1. We can try to make an analysis in the compiling + phase to raise the error. +*) +Global Instance C1 {T : Type} `{e : A T, B T} : C bool. Admitted. + +Elpi AddAllClasses. +Elpi AddAllInstances. + +Elpi Override TC TC_solver All. + +Elpi Print TC_solver. +Goal C bool. + apply _. +Qed. \ No newline at end of file diff --git a/apps/tc/tests/premisesSort/sort3.v b/apps/tc/tests/premisesSort/sort3.v new file mode 100644 index 000000000..8ccec6882 --- /dev/null +++ b/apps/tc/tests/premisesSort/sort3.v @@ -0,0 +1,28 @@ +From elpi.apps.tc.tests.premisesSort Require Import sortCode. +Elpi Debug "simple-compiler". + +Class A (S : Type) (T : Type). +Class B (S : Type) (T : Type). +Class C (S : Type). + +Global Hint Mode A + - : typeclass_instances. +Global Hint Mode B + - : typeclass_instances. +Elpi AddAllClasses. + +Global Instance A1 : A nat nat. Admitted. +Global Instance B1 : B nat nat. Admitted. + +Global Instance C1 {S T : Type} `{B S T, A T S} : C T. Admitted. + +Elpi AddAllInstances. +Elpi Override TC TC_solver All. +Goal C nat. + apply _. +Qed. + +(* Following has a cyclic dependecy, therefore error *) +(* Global Instance C2 {S T : Type} `{A T S, B S T} : C bool. Admitted. *) +(* Elpi AddInstances C2. *) + +(* Global Instance C3 {S T : Type} `{B T S} : C S. Admitted. *) +(* Elpi AddInstances C3. *) \ No newline at end of file diff --git a/apps/tc/tests/premisesSort/sort4.v b/apps/tc/tests/premisesSort/sort4.v new file mode 100644 index 000000000..e1ed85709 --- /dev/null +++ b/apps/tc/tests/premisesSort/sort4.v @@ -0,0 +1,59 @@ +From elpi.apps.tc.tests.premisesSort Require Import sortCode. +Elpi Debug "simple-compiler". +Set AddModes. + +Class A (S : Type) (T : Type). +Class C (S : Type) (T : Type). +Class B (S : Type) (T : Type) `(A S T, C S T) := f : forall (x : S), x = x. + +Global Hint Mode A + + : typeclass_instances. +Global Hint Mode C + + : typeclass_instances. + +Global Instance A1 : A nat nat. Admitted. +Global Instance C1 : C nat nat. Admitted. +Global Instance B1 (S : Type) (T : Type) (a : A S T) (c : C S T) : B S T a c. Admitted. + +Elpi AddAllClasses. +Elpi AddAllInstances. +Elpi Override TC TC_solver All. + +Elpi Accumulate tc.db lp:{{ + pred get-inout-sealed-goal i:argument_mode, i:sealed-goal, o:list term. + get-inout-sealed-goal AMode (seal (goal _ _ (app [global GR | L]) Sol _)) Res :- + tc-mode GR Modes, std.append L [Sol] L', + std.map2-filter L' Modes (t\m\r\ pr AMode _ = m, var t, r = t) Res. + get-inout-sealed-goal out (seal (goal _ _ _ Sol _)) [Sol]. + get-inout-sealed-goal _ _ []. + + pred sort-goals i:list sealed-goal, o:list int. + sort-goals L NL :- + std.map-i L (i\x\r\ r = pr x i) LookupList, + std.map L (x\r\ sigma M\ get-inout-sealed-goal in x M, r = pr x M) InputModes, + std.map L (x\r\ sigma Output Deps\ + get-inout-sealed-goal out x Output, + std.map-filter InputModes (x\r\ + sigma Fst Snd\ pr Fst Snd = x, + std.exists Output (v\ std.exists Snd (v1\ occurs_var v v1)), r = Fst) Deps, % O(N^2) + sigma Output2Nb Deps2Nb\ + std.lookup! LookupList x Output2Nb, + std.map Deps (std.lookup! LookupList) Deps2Nb, + r = pr Output2Nb Deps2Nb) Graph, + coq.toposort Graph NL. + + pred sort-sealed-goals i:list sealed-goal, o:list sealed-goal. + sort-sealed-goals SGL SortedSGL :- + sort-goals SGL SGLIndexes, + std.map SGLIndexes (x\r\ std.nth x SGL r) SortedSGL. + + :after "firstHook" msolve L N :- !, + sort-sealed-goals L LSort, + coq.say LSort, + coq.ltac.all (coq.ltac.open solve) LSort N. + + :after "firstHook" msolve A _ :- coq.say A, sep, fail. +}}. +Elpi Typecheck TC_solver. + +Goal 3 = 3. + Fail apply f. +Abort. \ No newline at end of file diff --git a/apps/tc/tests/premisesSort/sortCode.v b/apps/tc/tests/premisesSort/sortCode.v new file mode 100644 index 000000000..99b25a308 --- /dev/null +++ b/apps/tc/tests/premisesSort/sortCode.v @@ -0,0 +1,90 @@ + +From elpi Require Import tc. + +Elpi Accumulate tc.db lp:{{ + pred get-pattern-fragment i:term, o:list term. + + pred get-inout i:argument_mode, i:term, o:list term. + % TODO: the second arg may not be an (app L) + get-inout AMode (app [global GR | L]) Res :- + std.drop-last 1 {tc-mode GR} Modes, + std.map2-filter L Modes (t\m\r\ pr AMode _ = m, r = t) Res. + get-inout _ _ []. + + pred input-must-have-predecessor i:term, i:term, i:list term, i:list term. + input-must-have-predecessor _ _ [] _ :- !. + input-must-have-predecessor Instance Premise [Mode | Modes] Premises :- + std.exists Premises (p\ sigma MOut\ + get-inout out p MOut, std.mem MOut Mode), + input-must-have-predecessor Instance Premise Modes Premises. + input-must-have-predecessor Instance Premise [Mode | _] _ :- + coq.error "Input mode" Mode "of" + Premise "cannot be inferred from the other premises of the instance" + Instance. + + + % CurrentType is the type of the current instance to get its input variables, + % These variables should not create edges in the graph + pred sort-hypothesis i:term, i:term, i:list term, o:list int. + sort-hypothesis Instance (app [_ | InputCurrentType]) L NL :- + std.map-i L (i\x\r\ r = pr x i) LookupList, + std.map L (premise\r\ sigma M M'\ get-inout in premise M, + std.filter M (x\ not (std.mem InputCurrentType x)) M', + input-must-have-predecessor Instance premise M' L, + r = pr premise M') InputModes, + % foreach goal, we associate those goals having a dependency on it, + % in particular a goal G2 depends on G1 if a variable V is in + % output mode for G1 and in input mode for G2 (the dependency graph will + % and edge going from G1 to G2 : G1 -> G2) + std.map L (x\r\ sigma Output Deps\ % O(N^3 * check of occurs) + % the list of variable in input of the current goal G + get-inout out x Output, + % for each output modes of all goals, we keep those having an output + % which exists in the input variable of G + std.map-filter InputModes (x\r\ + sigma Fst Snd\ pr Fst Snd = x, + std.exists Output (v\ std.exists Snd (v1\ occurs v v1)), r = Fst) Deps, % O(N^2) + sigma Output2Nb Deps2Nb\ + std.lookup! LookupList x Output2Nb, + std.map Deps (std.lookup! LookupList) Deps2Nb, + r = pr Output2Nb Deps2Nb) Graph, + coq.toposort Graph NL. + + pred sort-and-compile-premises i:term, i:term, i:list term, i:list term, i:prop, o:list prop. + sort-and-compile-premises Instance CurrentType Types Vars IsPositive Premises :- + sort-hypothesis Instance CurrentType Types TypesSortedIndexes, % O (n^3) + % std.map-i Types (i\e\r\ r = i) TypesSortedIndexes, + std.map TypesSortedIndexes (x\r\ std.nth x Vars r) SortedVars, % O (n^2) + std.map TypesSortedIndexes (x\r\ std.nth x Types r) SortedTypes, % O (n^2) + std.map2-filter SortedTypes SortedVars (t\v\r\ + compile-aux1 t v [] [] [] (not IsPositive) false r _) Premises. + + pred compile-aux1 i:term, i:term, i:list term, i:list univ, i:list term, i:prop, i:prop, o:prop, o:bool. + :name "compiler-aux:start" + compile-aux1 Ty I [] [X | XS] [] IsPositive IsHead (pi x\ C x) IsLeaf :- !, + pi x\ copy (sort (typ X)) (sort (typ x)) => copy Ty (Ty1 x), + compile-aux1 (Ty1 x) I [] XS [] IsPositive IsHead (C x) IsLeaf. + compile-aux1 (prod N T F) I ListVar [] Types IsPositive IsHead Clause ff :- !, + (if IsPositive (Clause = pi x\ C x) (Clause = (pi x\ decl x N T => C x))), + pi p\ sigma Type\ + if (app-has-class T, not (occurs p (F p))) (Type = T) (Type = app []), + compile-aux1 (F p) I [p | ListVar] [] [Type | Types] IsPositive IsHead (C p) _. + :if "simple-compiler" + % TODO: here we don't do pattern fragment unification + compile-aux1 Ty I ListVar [] Types IsPositive IsHead Clause tt :- !, + sort-and-compile-premises I Ty Types ListVar IsPositive Premises, + coq.mk-app I {std.rev ListVar} AppInst, + make-tc IsHead Ty AppInst Premises Clause. + compile-aux1 Ty I ListVar [] Types IsPositive IsHead Clause tt :- !, + sort-and-compile-premises I Ty Types ListVar IsPositive Premises, + coq.mk-app I {std.rev ListVar} AppInst, + std.append {get-pattern-fragment Ty} {get-pattern-fragment AppInst} Term-to-be-fixed, + std.fold Term-to-be-fixed 0 (e\acc\r\ sigma L X\ e = app X, std.length X L, r is acc + L - 1) Len, + if (IsPositive) (IsPositiveBool = tt) (IsPositiveBool = ff), + remove-ho-unification IsHead IsPositiveBool Len Ty AppInst Premises Term-to-be-fixed [] [] [] [] [] Clause. + + :after "firstHook" + compile-aux Ty Inst _Premises _VarAcc UnivL IsPositive IsHead Clause NoPremises :- !, + compile-aux1 Ty Inst [] UnivL [] (IsPositive = tt, true; false) IsHead Clause NoPremises. +}}. +Elpi Typecheck TC_solver. \ No newline at end of file diff --git a/apps/tc/tests/removeEta.v b/apps/tc/tests/removeEta.v new file mode 100644 index 000000000..0fdd631ef --- /dev/null +++ b/apps/tc/tests/removeEta.v @@ -0,0 +1,37 @@ +From elpi Require Import tc. + +Elpi Query TC_solver lp:{{ + remove-eta2 {{fun x => 3 x}} {{3}} +}}. + +Elpi Query TC_solver lp:{{ + remove-eta2 {{fun x => 3 x x}} {{fun x => 3 x x}} +}}. + +Elpi Query TC_solver lp:{{ + remove-eta2 {{fun x => 3}} {{fun x => 3}} +}}. + +Elpi Query TC_solver lp:{{ + remove-eta2 {{fun x => 3 (fun y => 4 y) x}} {{3 4}} +}}. + +Elpi Query TC_solver lp:{{ + remove-eta2 {{fun x => 3 (fun y => x y)}} {{3}} +}}. + +Elpi Query TC_solver lp:{{ + remove-eta2 {{fun x y => 3 x y}} {{3}} +}}. + +Elpi Query TC_solver lp:{{ + remove-eta2 {{fun x y => 3 y x}} {{fun x y => 3 y x}} +}}. + +Elpi Query TC_solver lp:{{ + remove-eta2 {{fun x y => 3 _ y}} {{fun x => 3 _}} +}}. + +Elpi Query TC_solver lp:{{ + remove-eta2 {{fun x y => 3 _ _}} {{fun x y => 3 _ _}} +}}. \ No newline at end of file diff --git a/apps/tc/tests/section_in_out.v b/apps/tc/tests/section_in_out.v new file mode 100644 index 000000000..e643d2d09 --- /dev/null +++ b/apps/tc/tests/section_in_out.v @@ -0,0 +1,60 @@ +From elpi.apps Require Import tc. +From elpi.apps.tc Extra Dependency "base.elpi" as base. + +Elpi Command len_test. +Elpi Accumulate Db tc.db. +Elpi Accumulate File base. +Elpi Accumulate lp:{{ + % contains the number of instances that are not + % imported from other files + pred origial_tc o:int. + main [int Len] :- + std.findall (instance _ _ _) Insts, + std.map Insts (x\r\ instance _ r _ = x) R, + WantedLength is {origial_tc} + Len, + std.assert! ({std.length R} = WantedLength) + "Unexpected number of instances", + std.forall R (x\ sigma L\ + std.assert! (count R x L, L = 1) "Duplicates in instances"). +}}. +(* Elpi Typecheck. *) + +Elpi Query TC_solver lp:{{ + std.findall (instance _ _ _) Rules, + std.length Rules Len, + coq.elpi.accumulate _ "tc.db" (clause _ _ (origial_tc Len)). +}}. + +Class Eqb A:= eqb: A -> A -> bool. +Global Instance eqA : Eqb unit := { eqb x y := true }. + +Elpi AddAllClasses. +Elpi AddInstances Eqb. + +Elpi len_test 1. + +Section A. + Context (A : Type). + Global Instance eqB : Eqb bool := { eqb x y := if x then y else negb y }. + Elpi AddInstances Eqb. + Elpi len_test 2. + + Global Instance eqC : Eqb A := {eqb _ _ := true}. + Elpi AddInstances Eqb. + Elpi len_test 3. + + Section B. + Context (B : Type). + Global Instance eqD : Eqb B := {eqb _ _ := true}. + Elpi AddInstances Eqb. + Elpi len_test 4. + MySectionEnd. + + Elpi len_test 4. + +MySectionEnd. + +Elpi len_test 4. + + + diff --git a/apps/tc/tests/sortUvarTyp.v b/apps/tc/tests/sortUvarTyp.v new file mode 100644 index 000000000..3152d695f --- /dev/null +++ b/apps/tc/tests/sortUvarTyp.v @@ -0,0 +1,10 @@ +From elpi.apps Require Import tc. +From Coq Require Export Morphisms. + +Global Instance pairSort: Params (@pair) 2 := {}. + +Definition fst1 T := @fst T T . + +Global Instance fstSort: Params (@fst1) 2 := {}. +Elpi AddInstances pairSort fstSort. +(* Elpi Print TC_solver. *) diff --git a/apps/tc/tests/stdppInj.v b/apps/tc/tests/stdppInj.v new file mode 100644 index 000000000..aea5e0134 --- /dev/null +++ b/apps/tc/tests/stdppInj.v @@ -0,0 +1,280 @@ +From Coq Require Export Morphisms RelationClasses List Bool Setoid Peano Utf8. +From Coq Require Import Permutation. +Export ListNotations. +From Coq.Program Require Export Basics Syntax. +From elpi.apps Require Export tc. +Elpi Debug "simple-compiler". + +(* TODO: @FissoreD this flag not works *) +(* Unset TC_NameFullPath. *) + +Notation length := Datatypes.length. +Global Generalizable All Variables. +Global Unset Transparent Obligations. + +(* Set Warnings "+elpi". *) + +Definition tc_opaque {A} (x : A) : A := x. +(* Typeclasses Opaque tc_opaque. *) + +Global Arguments tc_opaque {_} _ /. +Declare Scope stdpp_scope. +Delimit Scope stdpp_scope with stdpp. +Global Open Scope stdpp_scope. +Notation "(=)" := eq (only parsing) : stdpp_scope. +Notation "( x =.)" := (eq x) (only parsing) : stdpp_scope. +Notation "(.= x )" := (λ y, eq y x) (only parsing) : stdpp_scope. +Notation "(≠)" := (λ x y, x ≠ y) (only parsing) : stdpp_scope. +Notation "( x ≠.)" := (λ y, x ≠ y) (only parsing) : stdpp_scope. +Notation "(.≠ x )" := (λ y, y ≠ x) (only parsing) : stdpp_scope. +Infix "=@{ A }" := (@eq A) + (at level 70, only parsing, no associativity) : stdpp_scope. +Notation "(=@{ A } )" := (@eq A) (only parsing) : stdpp_scope. +Notation "(≠@{ A } )" := (λ X Y, ¬X =@{A} Y) (only parsing) : stdpp_scope. +Notation "X ≠@{ A } Y":= (¬X =@{ A } Y) + (at level 70, only parsing, no associativity) : stdpp_scope. + +Global Hint Extern 0 (_ = _) => reflexivity : core. +Global Hint Extern 100 (_ ≠ _) => discriminate : core. + +Global Instance: ∀ A, PreOrder (=@{A}). +Proof. split; repeat intro; congruence. Qed. +Class Equiv A := equiv: relation A. +Global Instance equiv_rewrite_relation `{Equiv A} : + RewriteRelation (@equiv A _) | 150 := {}. + +Infix "≡" := equiv (at level 70, no associativity) : stdpp_scope. +Infix "≡@{ A }" := (@equiv A _) + (at level 70, only parsing, no associativity) : stdpp_scope. + +Notation "(≡)" := equiv (only parsing) : stdpp_scope. +Notation "( X ≡.)" := (equiv X) (only parsing) : stdpp_scope. +Notation "(.≡ X )" := (λ Y, Y ≡ X) (only parsing) : stdpp_scope. +Notation "(≢)" := (λ X Y, ¬X ≡ Y) (only parsing) : stdpp_scope. +Notation "X ≢ Y":= (¬X ≡ Y) (at level 70, no associativity) : stdpp_scope. +Notation "( X ≢.)" := (λ Y, X ≢ Y) (only parsing) : stdpp_scope. +Notation "(.≢ X )" := (λ Y, Y ≢ X) (only parsing) : stdpp_scope. + +Notation "(≡@{ A } )" := (@equiv A _) (only parsing) : stdpp_scope. +Notation "(≢@{ A } )" := (λ X Y, ¬X ≡@{A} Y) (only parsing) : stdpp_scope. +Notation "X ≢@{ A } Y":= (¬X ≡@{ A } Y) + (at level 70, only parsing, no associativity) : stdpp_scope. +Class LeibnizEquiv A `{Equiv A} := + leibniz_equiv (x y : A) : x ≡ y → x = y. +Global Hint Mode LeibnizEquiv ! - : typeclass_instances. + +Global Instance: Params (@equiv) 2 := {}. +Global Instance equiv_default_relation `{Equiv A} : + DefaultRelation (≡@{A}) | 3 := {}. +Global Hint Extern 0 (_ ≡ _) => reflexivity : core. +Global Hint Extern 0 (_ ≡ _) => symmetry; assumption : core. + + +Class Inj {A B} (R : relation A) (S : relation B) (f : A → B) : Prop := + inj x y : S (f x) (f y) → R x y. + +Class Inj2 {A B C} (R1 : relation A) (R2 : relation B) + (S : relation C) (f : A → B → C) : Prop := + inj2 x1 x2 y1 y2 : S (f x1 x2) (f y1 y2) → R1 x1 y1 ∧ R2 x2 y2. + +Global Arguments irreflexivity {_} _ {_} _ _ : assert. +Global Arguments inj {_ _ _ _} _ {_} _ _ _ : assert. +Global Arguments inj2 {_ _ _ _ _ _} _ {_} _ _ _ _ _: assert. + +Global Instance inj2_inj_1 `{Inj2 A B C R1 R2 R3 f} y : Inj R1 R3 (λ x, f x y). +Proof. repeat intro; edestruct (inj2 f); eauto. Qed. +Global Instance inj2_inj_2 `{Inj2 A B C R1 R2 R3 f} x : Inj R2 R3 (f x). +Proof. repeat intro; edestruct (inj2 f); eauto. Qed. + +Notation "(∧)" := and (only parsing) : stdpp_scope. +Notation "( A ∧.)" := (and A) (only parsing) : stdpp_scope. +Notation "(.∧ B )" := (λ A, A ∧ B) (only parsing) : stdpp_scope. + +Notation "(∨)" := or (only parsing) : stdpp_scope. +Notation "( A ∨.)" := (or A) (only parsing) : stdpp_scope. +Notation "(.∨ B )" := (λ A, A ∨ B) (only parsing) : stdpp_scope. + +Notation "(↔)" := iff (only parsing) : stdpp_scope. +Notation "( A ↔.)" := (iff A) (only parsing) : stdpp_scope. +Notation "(.↔ B )" := (λ A, A ↔ B) (only parsing) : stdpp_scope. + +Global Hint Extern 0 (_ ↔ _) => reflexivity : core. +Global Hint Extern 0 (_ ↔ _) => symmetry; assumption : core. + +Notation "(→)" := (λ A B, A → B) (only parsing) : stdpp_scope. +Notation "( A →.)" := (λ B, A → B) (only parsing) : stdpp_scope. +Notation "(.→ B )" := (λ A, A → B) (only parsing) : stdpp_scope. + +Notation "t $ r" := (t r) + (at level 65, right associativity, only parsing) : stdpp_scope. +Notation "($)" := (λ f x, f x) (only parsing) : stdpp_scope. +Notation "(.$ x )" := (λ f, f x) (only parsing) : stdpp_scope. + +Infix "∘" := compose : stdpp_scope. +Notation "(∘)" := compose (only parsing) : stdpp_scope. +Notation "( f ∘.)" := (compose f) (only parsing) : stdpp_scope. +Notation "(.∘ f )" := (λ g, compose g f) (only parsing) : stdpp_scope. +(** Ensure that [simpl] unfolds [id], [compose], and [flip] when fully +applied. *) +Global Arguments id _ _ / : assert. +Global Arguments compose _ _ _ _ _ _ / : assert. +Global Arguments flip _ _ _ _ _ _ / : assert. +Global Arguments const _ _ _ _ / : assert. + +Definition fun_map {A A' B B'} (f: A' → A) (g: B → B') (h : A → B) : A' → B' := + g ∘ h ∘ f. + +Global Instance id_inj {A} : Inj (=) (=) (@id A). +Proof. intros ??; auto. Qed. +Global Instance compose_inj {A B C} R1 R2 R3 (f : A → B) (g : B → C) : + Inj R1 R2 f → Inj R2 R3 g → Inj R1 R3 (g ∘ f). +Proof. red; intuition. Qed. + +(** ** Products *) +Notation "( x ,.)" := (pair x) (only parsing) : stdpp_scope. +Notation "(., y )" := (λ x, (x,y)) (only parsing) : stdpp_scope. + +Notation "p .1" := (fst p) (at level 2, left associativity, format "p .1"). +Notation "p .2" := (snd p) (at level 2, left associativity, format "p .2"). + +Definition prod_map {A A' B B'} (f: A → A') (g: B → B') (p : A * B) : A' * B' := + (f (p.1), g (p.2)). +Global Arguments prod_map {_ _ _ _} _ _ !_ / : assert. + +Global Instance pair_inj {A B} : Inj2 (=) (=) (=) (@pair A B). +Proof. injection 1; auto. Qed. +Global Instance prod_map_inj {A A' B B'} (f : A → A') (g : B → B') : + Inj (=) (=) f → Inj (=) (=) g → Inj (=) (=) (prod_map f g). +Proof. + intros ?? [??] [??] ?; simpl in *; f_equal; + [apply (inj f)|apply (inj g)]; congruence. +Qed. + +Definition prod_relation {A B} (R1 : relation A) (R2 : relation B) : + relation (A * B) := λ x y, R1 (x.1) (y.1) ∧ R2 (x.2) (y.2). + +Section prod_relation. + Context `{RA : relation A, RB : relation B}. + Global Instance pair_inj' : Inj2 RA RB (prod_relation RA RB) pair. + Proof. inversion_clear 1; eauto. Qed. +MySectionEnd. + +Global Instance prod_equiv `{Equiv A,Equiv B} : Equiv (A * B) := + prod_relation (≡) (≡). +Elpi AddAllClasses. + +Section prod_setoid. + Context `{Equiv A, Equiv B}. + + Elpi Accumulate TC_solver lp:{{ + shorten tc-elpi.apps.tc.tests.stdppInj.{tc-Inj2}. + % shorten tc-stdppInj.{tc-Inj2}. + tc-Inj2 A B C RA RB RC F S :- + RC = app [global {coq.locate "equiv"} | _], + Res = {{prod_relation _ _}}, + coq.unify-eq RC Res ok, + tc-Inj2 A B C RA RB Res F S. + }}. + Elpi Typecheck TC_solver. + + Elpi AddInstances Inj2. + Global Instance pair_equiv_inj : Inj2 (≡) (≡) (≡@{A*B}) pair := _. +MySectionEnd. + +(* Typeclasses Opaque prod_equiv. *) + +(** ** Sums *) +Definition sum_map {A A' B B'} (f: A → A') (g: B → B') (xy : A + B) : A' + B' := + match xy with inl x => inl (f x) | inr y => inr (g y) end. +Global Arguments sum_map {_ _ _ _} _ _ !_ / : assert. + +Global Instance inl_inj {A B} : Inj (=) (=) (@inl A B). +Proof. injection 1; auto. Qed. +Global Instance inr_inj {A B} : Inj (=) (=) (@inr A B). +Proof. injection 1; auto. Qed. + +Global Instance sum_map_inj {A A' B B'} (f : A → A') (g : B → B') : + Inj (=) (=) f → Inj (=) (=) g → Inj (=) (=) (sum_map f g). +Proof. intros ?? [?|?] [?|?] [=]; f_equal; apply (inj _); auto. Qed. + +Inductive sum_relation {A B} + (RA : relation A) (RB : relation B) : relation (A + B) := + | inl_related x1 x2 : RA x1 x2 → sum_relation RA RB (inl x1) (inl x2) + | inr_related y1 y2 : RB y1 y2 → sum_relation RA RB (inr y1) (inr y2). + +Section sum_relation. + Context `{RA : relation A, RB : relation B}. + Global Instance inl_inj' : Inj RA (sum_relation RA RB) inl. + Proof. inversion_clear 1; auto. Qed. + Global Instance inr_inj' : Inj RB (sum_relation RA RB) inr. + Proof. inversion_clear 1; auto. Qed. +MySectionEnd. + +Global Instance sum_equiv `{Equiv A, Equiv B} : Equiv (A + B) := sum_relation (≡) (≡). + +(* Elpi added here *) +Elpi Accumulate TC_solver lp:{{ + shorten tc-elpi.apps.tc.tests.stdppInj.{tc-Inj}. + % shorten tc-stdppInj.{tc-Inj}. + tc-Inj A B RA {{@equiv (sum _ _) (@sum_equiv _ _ _ _)}} S C :- + tc-Inj A B RA {{sum_relation _ _}} S C. +}}. +Elpi Typecheck TC_solver. + +Global Instance inl_equiv_inj `{Equiv A, Equiv B} : Inj (≡) (≡) (@inl A B) := _. +Global Instance inr_equiv_inj `{Equiv A, Equiv B} : Inj (≡) (≡) (@inr A B) := _. + +Notation "` x" := (proj1_sig x) (at level 10, format "` x") : stdpp_scope. + +(* Elpi AddInstances Inj ignoreInstances compose_inj. *) +Elpi Override TC TC_solver Only Inj. + +Elpi AddAllInstances compose_inj. + +Elpi Accumulate TC_solver lp:{{ + shorten tc-elpi.apps.tc.tests.stdppInj.{tc-Inj}. + tc-Inj A B RA RB F X :- + F = fun _ _ _, + G = {{@compose _ _ _ _ _}}, + coq.unify-eq G F ok, + tc-Inj A B RA RB G X. +}}. +Elpi Typecheck TC_solver. + +Definition f := Nat.add 0. +Global Instance h: Inj eq eq f. + unfold f. simpl. easy. +Qed. + +(* Set Warnings "+elpi". *) + + +Elpi Accumulate tc.db lp:{{ + shorten tc-elpi.apps.tc.tests.stdppInj.{tc-Inj}. + :after "lastHook" + tc-Inj A B RA RB F S :- + F = (fun _ _ _), !, + G = {{ compose _ _ }}, + coq.unify-eq G F ok, + tc-Inj A B RA RB G S. +}}. +Elpi Typecheck TC_solver. + +Elpi AddInstances 1000 h. +Elpi AddInstances 1000 compose_inj. + +Goal Inj eq eq (compose (@id nat) id). +apply _. +Qed. + +Goal Inj eq eq (compose (compose (@id nat) id) id). +apply _. +Qed. + +Goal Inj eq eq (fun (x:nat) => id (id x)). +apply _. +Qed. + +Goal Inj eq eq (fun (x: nat) => (compose id id) (id x)). +apply (compose_inj eq eq); apply _. +Qed. \ No newline at end of file diff --git a/apps/tc/tests/stdppInjClassic.v b/apps/tc/tests/stdppInjClassic.v new file mode 100644 index 000000000..cbf7c1c36 --- /dev/null +++ b/apps/tc/tests/stdppInjClassic.v @@ -0,0 +1,218 @@ +From Coq Require Export Morphisms RelationClasses List Bool Setoid Peano Utf8. +From Coq Require Import Permutation. +Export ListNotations. +From Coq.Program Require Export Basics Syntax. + +Notation length := Datatypes.length. +Global Generalizable All Variables. +Global Unset Transparent Obligations. + +Definition tc_opaque {A} (x : A) : A := x. +(* Typeclasses Opaque tc_opaque. *) + +Global Arguments tc_opaque {_} _ /. +Declare Scope stdpp_scope. +Delimit Scope stdpp_scope with stdpp. +Global Open Scope stdpp_scope. +Notation "(=)" := eq (only parsing) : stdpp_scope. +Notation "( x =.)" := (eq x) (only parsing) : stdpp_scope. +Notation "(.= x )" := (λ y, eq y x) (only parsing) : stdpp_scope. +Notation "(≠)" := (λ x y, x ≠ y) (only parsing) : stdpp_scope. +Notation "( x ≠.)" := (λ y, x ≠ y) (only parsing) : stdpp_scope. +Notation "(.≠ x )" := (λ y, y ≠ x) (only parsing) : stdpp_scope. +Infix "=@{ A }" := (@eq A) + (at level 70, only parsing, no associativity) : stdpp_scope. +Notation "(=@{ A } )" := (@eq A) (only parsing) : stdpp_scope. +Notation "(≠@{ A } )" := (λ X Y, ¬X =@{A} Y) (only parsing) : stdpp_scope. +Notation "X ≠@{ A } Y":= (¬X =@{ A } Y) + (at level 70, only parsing, no associativity) : stdpp_scope. + +Global Hint Extern 0 (_ = _) => reflexivity : core. +Global Hint Extern 100 (_ ≠ _) => discriminate : core. + +Global Instance: ∀ A, PreOrder (=@{A}). +Proof. split; repeat intro; congruence. Qed. +Class Equiv A := equiv: relation A. +Global Instance equiv_rewrite_relation `{Equiv A} : + RewriteRelation (@equiv A _) | 150 := {}. + +Infix "≡" := equiv (at level 70, no associativity) : stdpp_scope. +Infix "≡@{ A }" := (@equiv A _) + (at level 70, only parsing, no associativity) : stdpp_scope. + +Notation "(≡)" := equiv (only parsing) : stdpp_scope. +Notation "( X ≡.)" := (equiv X) (only parsing) : stdpp_scope. +Notation "(.≡ X )" := (λ Y, Y ≡ X) (only parsing) : stdpp_scope. +Notation "(≢)" := (λ X Y, ¬X ≡ Y) (only parsing) : stdpp_scope. +Notation "X ≢ Y":= (¬X ≡ Y) (at level 70, no associativity) : stdpp_scope. +Notation "( X ≢.)" := (λ Y, X ≢ Y) (only parsing) : stdpp_scope. +Notation "(.≢ X )" := (λ Y, Y ≢ X) (only parsing) : stdpp_scope. + +Notation "(≡@{ A } )" := (@equiv A _) (only parsing) : stdpp_scope. +Notation "(≢@{ A } )" := (λ X Y, ¬X ≡@{A} Y) (only parsing) : stdpp_scope. +Notation "X ≢@{ A } Y":= (¬X ≡@{ A } Y) + (at level 70, only parsing, no associativity) : stdpp_scope. +Class LeibnizEquiv A `{Equiv A} := + leibniz_equiv (x y : A) : x ≡ y → x = y. +Global Hint Mode LeibnizEquiv ! - : typeclass_instances. + +Global Instance: Params (@equiv) 2 := {}. +Global Instance equiv_default_relation `{Equiv A} : + DefaultRelation (≡@{A}) | 3 := {}. +Global Hint Extern 0 (_ ≡ _) => reflexivity : core. +Global Hint Extern 0 (_ ≡ _) => symmetry; assumption : core. + + +Class Inj {A B} (R : relation A) (S : relation B) (f : A → B) : Prop := + inj x y : S (f x) (f y) → R x y. + +Class Inj2 {A B C} (R1 : relation A) (R2 : relation B) + (S : relation C) (f : A → B → C) : Prop := + inj2 x1 x2 y1 y2 : S (f x1 x2) (f y1 y2) → R1 x1 y1 ∧ R2 x2 y2. + +Global Arguments irreflexivity {_} _ {_} _ _ : assert. +Global Arguments inj {_ _ _ _} _ {_} _ _ _ : assert. +Global Arguments inj2 {_ _ _ _ _ _} _ {_} _ _ _ _ _: assert. + +Global Instance inj2_inj_1 `{Inj2 A B C R1 R2 R3 f} y : Inj R1 R3 (λ x, f x y). +Proof. repeat intro; edestruct (inj2 f); eauto. Qed. +Global Instance inj2_inj_2 `{Inj2 A B C R1 R2 R3 f} x : Inj R2 R3 (f x). +Proof. repeat intro; edestruct (inj2 f); eauto. Qed. + +Notation "(∧)" := and (only parsing) : stdpp_scope. +Notation "( A ∧.)" := (and A) (only parsing) : stdpp_scope. +Notation "(.∧ B )" := (λ A, A ∧ B) (only parsing) : stdpp_scope. + +Notation "(∨)" := or (only parsing) : stdpp_scope. +Notation "( A ∨.)" := (or A) (only parsing) : stdpp_scope. +Notation "(.∨ B )" := (λ A, A ∨ B) (only parsing) : stdpp_scope. + +Notation "(↔)" := iff (only parsing) : stdpp_scope. +Notation "( A ↔.)" := (iff A) (only parsing) : stdpp_scope. +Notation "(.↔ B )" := (λ A, A ↔ B) (only parsing) : stdpp_scope. + +Global Hint Extern 0 (_ ↔ _) => reflexivity : core. +Global Hint Extern 0 (_ ↔ _) => symmetry; assumption : core. + +Notation "(→)" := (λ A B, A → B) (only parsing) : stdpp_scope. +Notation "( A →.)" := (λ B, A → B) (only parsing) : stdpp_scope. +Notation "(.→ B )" := (λ A, A → B) (only parsing) : stdpp_scope. + +Notation "t $ r" := (t r) + (at level 65, right associativity, only parsing) : stdpp_scope. +Notation "($)" := (λ f x, f x) (only parsing) : stdpp_scope. +Notation "(.$ x )" := (λ f, f x) (only parsing) : stdpp_scope. + +Infix "∘" := compose : stdpp_scope. +Notation "(∘)" := compose (only parsing) : stdpp_scope. +Notation "( f ∘.)" := (compose f) (only parsing) : stdpp_scope. +Notation "(.∘ f )" := (λ g, compose g f) (only parsing) : stdpp_scope. +(** Ensure that [simpl] unfolds [id], [compose], and [flip] when fully +applied. *) +Global Arguments id _ _ / : assert. +Global Arguments compose _ _ _ _ _ _ / : assert. +Global Arguments flip _ _ _ _ _ _ / : assert. +Global Arguments const _ _ _ _ / : assert. + +Definition fun_map {A A' B B'} (f: A' → A) (g: B → B') (h : A → B) : A' → B' := + g ∘ h ∘ f. + +Global Instance id_inj {A} : Inj (=) (=) (@id A). +Proof. intros ??; auto. Qed. +Global Instance compose_inj {A B C} R1 R2 R3 (f : A → B) (g : B → C) : + Inj R1 R2 f → Inj R2 R3 g → Inj R1 R3 (g ∘ f). +Proof. red; intuition. Qed. + +(** ** Products *) +Notation "( x ,.)" := (pair x) (only parsing) : stdpp_scope. +Notation "(., y )" := (λ x, (x,y)) (only parsing) : stdpp_scope. + +Notation "p .1" := (fst p) (at level 2, left associativity, format "p .1"). +Notation "p .2" := (snd p) (at level 2, left associativity, format "p .2"). + +Definition prod_map {A A' B B'} (f: A → A') (g: B → B') (p : A * B) : A' * B' := + (f (p.1), g (p.2)). +Global Arguments prod_map {_ _ _ _} _ _ !_ / : assert. + +Global Instance pair_inj {A B} : Inj2 (=) (=) (=) (@pair A B). +Proof. injection 1; auto. Qed. +Global Instance prod_map_inj {A A' B B'} (f : A → A') (g : B → B') : + Inj (=) (=) f → Inj (=) (=) g → Inj (=) (=) (prod_map f g). +Proof. + intros ?? [??] [??] ?; simpl in *; f_equal; + [apply (inj f)|apply (inj g)]; congruence. +Qed. + +Definition prod_relation {A B} (R1 : relation A) (R2 : relation B) : + relation (A * B) := λ x y, R1 (x.1) (y.1) ∧ R2 (x.2) (y.2). + +Section prod_relation. + Context `{RA : relation A, RB : relation B}. + Global Instance pair_inj' : Inj2 RA RB (prod_relation RA RB) pair. + Proof. inversion_clear 1; eauto. Qed. +End prod_relation. + +Global Instance prod_equiv `{Equiv A,Equiv B} : Equiv (A * B) := + prod_relation (≡) (≡). + +Section prod_setoid. + Context `{Equiv A, Equiv B}. + Global Instance pair_equiv_inj : Inj2 (≡) (≡) (≡@{A*B}) pair := _. +End prod_setoid. + +(* Typeclasses Opaque prod_equiv. *) + +(** ** Sums *) +Definition sum_map {A A' B B'} (f: A → A') (g: B → B') (xy : A + B) : A' + B' := + match xy with inl x => inl (f x) | inr y => inr (g y) end. +Global Arguments sum_map {_ _ _ _} _ _ !_ / : assert. + +Global Instance inl_inj {A B} : Inj (=) (=) (@inl A B). +Proof. injection 1; auto. Qed. +Global Instance inr_inj {A B} : Inj (=) (=) (@inr A B). +Proof. injection 1; auto. Qed. + +Global Instance sum_map_inj {A A' B B'} (f : A → A') (g : B → B') : + Inj (=) (=) f → Inj (=) (=) g → Inj (=) (=) (sum_map f g). +Proof. intros ?? [?|?] [?|?] [=]; f_equal; apply (inj _); auto. Qed. + +Inductive sum_relation {A B} + (RA : relation A) (RB : relation B) : relation (A + B) := + | inl_related x1 x2 : RA x1 x2 → sum_relation RA RB (inl x1) (inl x2) + | inr_related y1 y2 : RB y1 y2 → sum_relation RA RB (inr y1) (inr y2). + +Section sum_relation. + Context `{RA : relation A, RB : relation B}. + Global Instance inl_inj' : Inj RA (sum_relation RA RB) inl. + Proof. inversion_clear 1; auto. Qed. + Global Instance inr_inj' : Inj RB (sum_relation RA RB) inr. + Proof. inversion_clear 1; auto. Qed. +End sum_relation. + +Global Instance sum_equiv `{Equiv A, Equiv B} : Equiv (A + B) := sum_relation (≡) (≡). + +Global Instance inl_equiv_inj `{Equiv A, Equiv B} : Inj (≡) (≡) (@inl A B) := _. +Global Instance inr_equiv_inj `{Equiv A, Equiv B} : Inj (≡) (≡) (@inr A B) := _. + +Notation "` x" := (proj1_sig x) (at level 10, format "` x") : stdpp_scope. + +Definition f := Nat.add 0. +Global Instance h: Inj eq eq f. + unfold f. simpl. easy. +Qed. + +Goal Inj eq eq (compose (@id nat) id). +apply _. +Qed. + +Goal Inj eq eq (compose (compose (@id nat) id) id). +apply _. +Qed. + +(* Goal Inj eq eq (fun (x:nat) => id (id x)). +apply _. +Qed. *) + +Goal Inj eq eq (fun (x: nat) => (compose id id) (id x)). +apply (compose_inj eq eq); apply _. +Qed. \ No newline at end of file diff --git a/apps/tc/tests/test.v b/apps/tc/tests/test.v new file mode 100644 index 000000000..e15c7603f --- /dev/null +++ b/apps/tc/tests/test.v @@ -0,0 +1,20 @@ +From elpi.apps.tc.tests Require Import stdppInj. +Elpi TC_solver. Set TimeRefine. Set TimeTC. Set Debug "elpitime". +Elpi Accumulate TC_solver lp:{{ + :after "firstHook" + tc-Inj A B RA RB {{@compose lp:A lp:A lp:A lp:FL lp:FL}} Sol :- !, + tc-Inj A B RA RB FL Sol1, + coq.typecheck A TA ok, + coq.typecheck RA TRA ok, + coq.typecheck FL TFL ok, + coq.typecheck Sol1 TSol1 ok, + Sol = {{ + let a : lp:TA := lp:A in + let sol : lp:TSol1 := lp:Sol1 in + let ra : lp:TRA := lp:RA in + let fl : lp:TFL := lp:FL in + @compose_inj a a a ra ra ra fl fl sol sol}}. +}}. +Elpi Typecheck TC_solver. + +Goal Inj eq eq((compose (compose (compose f f )(compose f f ))(compose (compose f f )(compose f f )))). Time apply _. Qed. diff --git a/apps/tc/tests/test_commands_API.v b/apps/tc/tests/test_commands_API.v new file mode 100644 index 000000000..705508457 --- /dev/null +++ b/apps/tc/tests/test_commands_API.v @@ -0,0 +1,58 @@ +From elpi.apps Require Import tc. +From elpi.apps.tc.tests Require Import eqSimplDef. + +Elpi Command len_test. +Elpi Accumulate Db tc.db. +Elpi Accumulate lp:{{ + pred count i:gref, i:int. + count GR Len :- + if (const _ = GR) + (std.findall (instance _ _ GR) Cl, + std.assert! ({std.length Cl} = Len) + "Unexpected number of instances") + true. + + main [str E, int Len] :- + coq.locate E GR, + count GR Len. +}}. +Elpi Typecheck. + +Elpi AddClasses Eqb. + +Module test1. + Elpi AddInstances Eqb ignoreInstances eqP. + Elpi len_test Eqb 2. +End test1. +Reset test1. + +Module test2. + Elpi len_test Eqb 0. +End test2. +Reset test2. + +Module test3. + Elpi AddInstances Eqb. + Elpi len_test Eqb 3. +End test3. +Reset test3. + + +(* About RewriteRelation. + +About RelationClasses.RewriteRelation. + + +Elpi Query TC_solver lp:{{ + coq.gref->id {{:gref RelationClasses.RewriteRelation}} L. +}}. *) + +Module test4. + Elpi AddAllClasses. + Elpi AddAllInstances eqU. + + Elpi Query TC_solver lp:{{ + EqP = {{:gref eqU}}, + std.assert! (not (instance _ EqP _)) "EqP should not be in the DB". + }}. +End test4. \ No newline at end of file diff --git a/apps/tc/tests/test_tc.v b/apps/tc/tests/test_tc.v new file mode 100644 index 000000000..da488ee9a --- /dev/null +++ b/apps/tc/tests/test_tc.v @@ -0,0 +1,12 @@ +From elpi.apps Require Import tc. + +Elpi Override TC TC_solver All. + +Class a (N: nat). +Instance b : a 3. Qed. +Instance c : a 4. Qed. + +Elpi AddAllClasses. +Elpi AddAllInstances. + +Goal a 4. apply _. Qed. diff --git a/apps/tc/tests/univConstraint.v b/apps/tc/tests/univConstraint.v new file mode 100644 index 000000000..393e5ba39 --- /dev/null +++ b/apps/tc/tests/univConstraint.v @@ -0,0 +1,81 @@ +From Coq Require Export List. +From elpi.apps Require Export compiler. +Global Generalizable All Variables. + +Elpi Override TC TC_solver All. + +Class ElemOf A B := elem_of: A -> B -> Prop. +Class Elements A C := elements: C -> list A. + +Elpi AddClasses ElemOf. + +Inductive elem_of_list {A} : ElemOf A (list A) := + | elem_of_list_here (x : A) l : elem_of x (x :: l) + | elem_of_list_further (x y : A) l : elem_of x l -> elem_of x (y :: l). +Global Existing Instance elem_of_list. + +Elpi AddInstances ElemOf. + +Inductive NoDup {A} : list A -> Prop := + | NoDup_nil_2 : NoDup nil + | NoDup_cons_2 x l : not (elem_of x l) -> NoDup l -> NoDup (x :: l). + +Module A. + Class FinSet A C `{ElemOf A C,Elements A C} : Prop := { + NoDup_elements (X : C) : @NoDup A (elements X) + }. + + Fail Class FinSet1 A C `{ElemOf A C,Elements A C} : Prop := { + NoDup_elements (X : C) : NoDup (elements X) + }. +End A. + +Module B. + + Elpi Accumulate TC_solver lp:{{ + :after "firstHook" + msolve L N :- !, + coq.ltac.all (coq.ltac.open solve) L N. + + pred sep. + sep :- coq.say "----------------". + + :after "firstHook" + solve1 (goal Ctx _ Ty Sol _ as G) _L GL :- + not (Ty = prod _ _ _), var Sol, + ctx->clause Ctx Clauses, Ty = app [global TC | _], + @redflags! coq.redflags.beta => coq.reduction.lazy.norm Ty Ty1, + Clauses => if (tc-search-time TC Ty1 X) + ( + (copy A A :- var A => copy X X_), + coq.say "X" X "X_" X_, + my-refine X G GL; + coq.say "illtyped solution:" {coq.term->string X} + ) + (GL = [seal G]). + }}. + Elpi Typecheck TC_solver. + + (* Class IgnoreClass. +Elpi Override TC TC_solver Only IgnoreClass. +Set Typeclasses Debug. *) +(* Elpi Trace Browser. *) + Class FinSet2 A C `{ElemOf A C, Elements A C} : Prop := { + elem_of_elements2 (X : C) x : iff (elem_of x (elements X)) (elem_of x X); + NoDup_elements2 (X : C) : @NoDup A (elements X) + }. + +(* +1: looking for (ElemOf ?A (list ?A0)) with backtracking +1.1: simple apply @elem_of_list on (ElemOf ?A (list ?A0)), 0 subgoal(s) + +2: looking for (Elements ?A C) with backtracking +2.1: exact H0 on (Elements ?A C), 0 subgoal(s) + +3: looking for (ElemOf A C) without backtracking +3.1: exact H on (ElemOf A C), 0 subgoal(s) +-------------------------------------------------------------------------- +1: looking for (Elements A C) without backtracking +1.1: exact H0 on (Elements A C), 0 subgoal(s) +*) +End B. \ No newline at end of file diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v new file mode 100644 index 000000000..157eb4f91 --- /dev/null +++ b/apps/tc/theories/tc.v @@ -0,0 +1,212 @@ +Declare ML Module "coq-elpi-tc.plugin". +From elpi Require Import elpi. + +From elpi.apps.tc Extra Dependency "base.elpi" as base. +From elpi.apps.tc Extra Dependency "compiler.elpi" as compiler. +From elpi.apps.tc Extra Dependency "parser_addInstances.elpi" as parser_addInstances. +From elpi.apps.tc Extra Dependency "modes.elpi" as modes. +From elpi.apps.tc Extra Dependency "alias.elpi" as alias. +From elpi.apps.tc Extra Dependency "solver.elpi" as solver. +From elpi.apps.tc Extra Dependency "rewrite_forward.elpi" as rforward. +From elpi.apps.tc Extra Dependency "tc_aux.elpi" as tc_aux. +From elpi.apps.tc Extra Dependency "create_tc_predicate.elpi" as create_tc_predicate. + +(* Set Warnings "+elpi". *) + +Elpi Db tc.db lp:{{ + % the type of search for a typeclass + % deterministic :- no backtrack after having found a solution/fail + % classic :- the classic search, if a path is failing, we backtrack + kind search-mode type. + type deterministic search-mode. + type classic search-mode. + + % contains the instances added to the DB + % associated to the list of sections they belong to + % :index (1) + pred instance o:list string, o:gref, o:gref. + + % contains the typeclasses added to the DB + :index (3) + pred classes o:gref, o:search-mode. + + % pred on which we graft instances in the database + pred hook o:string. + :name "firstHook" hook "firstHook". + :name "lastHook" hook "lastHook". + + % the set of instances that we are not yet able to compile, + % in majority they use polimorphic TC + :index (3) + pred banned o:gref. + + % [tc-signature TC Modes], returns for each Typeclass TC + % its Modes + :index (3) + pred tc-mode i:gref, o:list (pair argument_mode string). +}}. + +Elpi Command print_instances. +Elpi Accumulate Db tc.db. +Elpi Accumulate lp:{{ + main [str TC] :- + std.assert! (coq.locate TC TC_Gr) "The entered TC not exists", + std.findall (instance _ _ TC_Gr) Rules, + coq.say "Instances list for" TC_Gr "is:" Rules. + main [] :- + std.findall (instance _ _ _) Rules, + coq.say "Instances list is:" Rules. +}}. +(* Elpi Typecheck. *) + +Elpi Command MySectionEnd. +Elpi Accumulate Db tc.db. +Elpi Accumulate File tc_aux. +Elpi Accumulate File base. +Elpi Accumulate File modes. +Elpi Accumulate File compiler. +Elpi Accumulate lp:{{ + main _ :- + instances-of-current-section InstsFiltered, + coq.env.end-section, + std.forall {std.rev InstsFiltered} (add-inst->db [] tt). +}}. +(* Elpi Typecheck. *) + +Elpi Command AddAllInstances. +Elpi Accumulate Db tc.db. +Elpi Accumulate File tc_aux. +Elpi Accumulate File base. +Elpi Accumulate File modes. +Elpi Accumulate File compiler. +Elpi Accumulate lp:{{ + main L :- + std.time ( + args->str-list L L1, + std.forall {coq.TC.db-tc} (x\ add-tc-or-inst-gr [] L1 [x])) T, + if (coq.option.get ["TimeAddInstances"] (coq.option.bool tt)) + (coq.say "Add instance Time" T) true. +}}. +(* Elpi Typecheck. *) + +Elpi Command AddInstances. +Elpi Accumulate Db tc.db. +Elpi Accumulate File base. +Elpi Accumulate File tc_aux. +Elpi Accumulate File modes. +Elpi Accumulate File compiler. +Elpi Accumulate File parser_addInstances. +Elpi Accumulate lp:{{ + % The main of the Command + main Arguments :- + std.time (parse Arguments Res, run-command Res) T, + if (coq.option.get ["TimeAddInstances"] (coq.option.bool tt)) + (coq.say "Add instance all Time" T) true. +}}. +(* Elpi Typecheck. *) +Elpi Query lp:{{ + coq.option.add ["TimeAddInstances"] (coq.option.bool ff) ff. +}}. +(* Elpi Typecheck. *) + +Elpi Command AddHooks. +Elpi Accumulate Db tc.db. +Elpi Accumulate File base. +Elpi Accumulate File tc_aux. +Elpi Accumulate lp:{{ + main [int N] :- + % IterNb is (N + 1) * 2, + % for-loop0 IterNb (x\ sigma HookNameProv HookName Div Mod\ + % Div is x div 2, Mod is x mod 2, + % HookNameProv is int_to_string Div, + % if (Mod = 0) (HookName = HookNameProv) (HookName is HookNameProv ^ "_complex"), + % @global! => add-tc-db HookName (after "firstHook") hook + % ). + IterNb is N + 1, + for-loop0 IterNb (x\ sigma HookName\ + HookName is int_to_string x, + @global! => add-tc-db HookName (before "lastHook") (hook HookName) + ). +}}. +(* Elpi Typecheck. *) + +Elpi AddHooks 1000. + +Elpi Command AddForwardRewriting. +Elpi Accumulate Db tc.db. +Elpi Accumulate File base. +Elpi Accumulate File tc_aux. +Elpi Accumulate File rforward. +Elpi Accumulate lp:{{ + main L :- + std.forall {args->str-list L} add-lemma->forward. +}}. +(* Elpi Typecheck. *) + +Elpi Command AddAlias. +Elpi Accumulate Db tc.db. +Elpi Accumulate File base. +Elpi Accumulate File tc_aux. +Elpi Accumulate File alias. +Elpi Accumulate lp:{{ + main [trm New, trm Old] :- + add-tc-db _ _ (alias New Old). +}}. +(* Elpi Typecheck. *) + +Elpi Tactic TC_solver. +Elpi Accumulate Db tc.db. +Elpi Accumulate File rforward. +Elpi Accumulate File base. +Elpi Accumulate File tc_aux. +Elpi Accumulate File modes. +Elpi Accumulate File alias. +Elpi Accumulate File compiler. +Elpi Accumulate File create_tc_predicate. +Elpi Accumulate File solver. +Elpi Query lp:{{ + coq.option.add ["UseRemoveEta"] (coq.option.bool tt) ff, + coq.option.add ["TimeTC"] (coq.option.bool ff) ff, + coq.option.add ["TC_NameFullPath"] (coq.option.bool tt) ff, + coq.option.add ["TimeRefine"] (coq.option.bool ff) ff, + coq.option.add ["DebugTC"] (coq.option.bool ff) ff, + coq.option.add ["AddModes"] (coq.option.bool ff) ff. +}}. +Elpi Typecheck. + +Elpi Command AddClasses. +Elpi Accumulate File base. +Elpi Accumulate File tc_aux. +Elpi Accumulate Db tc.db. +Elpi Accumulate File create_tc_predicate. +Elpi Accumulate lp:{{ + main L :- + std.mem {attributes} (attribute "deterministic" _), + std.forall {args->str-list L} (add-class-str deterministic). + main L :- std.forall {args->str-list L} (add-class-str classic). + main _ :- halt "This commands accepts: [classic|deterministic]? TC-names*". +}}. +(* Elpi Typecheck. *) + +(* + Adds all classes in the db. Note that in this case the search mode is set + to classic by default +*) +Elpi Command AddAllClasses. +Elpi Accumulate File base. +Elpi Accumulate File tc_aux. +Elpi Accumulate Db tc.db. +Elpi Accumulate File create_tc_predicate. +Elpi Accumulate lp:{{ + main _ :- + coq.TC.db-tc TC, + std.forall TC (add-class-gr classic). +}}. +Elpi Typecheck. + +Elpi Export AddInstances. +Elpi Export AddAllInstances. +Elpi Export MySectionEnd. + +Elpi AddAllClasses. +Elpi AddAllInstances. diff --git a/elpi-builtin.elpi b/elpi-builtin.elpi index 86a22a137..4c6705dd6 100644 --- a/elpi-builtin.elpi +++ b/elpi-builtin.elpi @@ -1187,8 +1187,8 @@ type unix.process out_stream -> in_stream -> in_stream -> unix.process. % Environment can be left unspecified, defaults to the current process % environment. % This API only works reliably since OCaml 4.12. -external pred unix.process.open i:string, i:list string, i:list string, - o:unix.process, o:diagnostic. +external pred unix.process.open i:string, i:list string, i:list string, + o:unix.process, o:diagnostic. % [unix.process.close P Diagnostic] OCaml's Unix.close_process_full external pred unix.process.close i:unix.process, o:diagnostic.