From 588af2bbc0f165a5e3e39f4d70dc37eb4b5da741 Mon Sep 17 00:00:00 2001 From: Valery Isaev Date: Sun, 8 Mar 2020 21:22:37 +0300 Subject: [PATCH] Replace transport with rewrite0 and rewriteF --- .../main/java/org/arend/lib/StdExtension.java | 10 +- .../org/arend/lib/tactic/RewriteTactic.java | 102 ++++++++++++------ src/Algebra/Monoid/GCD.ard | 2 +- src/Algebra/Ring/Localization.ard | 2 +- src/Equiv.ard | 11 +- src/Equiv/HalfAdjoint.ard | 5 +- src/HLevel.ard | 2 +- src/Homotopy/Localization/Separated.ard | 2 +- src/Homotopy/Loop.ard | 2 +- src/Homotopy/Pointed.ard | 3 +- src/Homotopy/Truncation.ard | 4 +- 11 files changed, 96 insertions(+), 49 deletions(-) diff --git a/meta/src/main/java/org/arend/lib/StdExtension.java b/meta/src/main/java/org/arend/lib/StdExtension.java index ea2e0fca..99698c5a 100644 --- a/meta/src/main/java/org/arend/lib/StdExtension.java +++ b/meta/src/main/java/org/arend/lib/StdExtension.java @@ -45,9 +45,11 @@ public void load(@NotNull DefinitionProvider provider) { @Override public void declareDefinitions(DefinitionContributor contributor) { MetaDefinition meta = new RewriteTactic(this); - contributor.declare(ModulePath.fromString("Paths.Meta"), LongName.fromString("rewrite"), Precedence.DEFAULT, new DeferredMetaDefinition(ExpressionTypechecker.Stage.AFTER_LEVELS, meta)); - contributor.declare(ModulePath.fromString("Paths.Meta"), LongName.fromString("rewrite1"), Precedence.DEFAULT, new DeferredMetaDefinition(ExpressionTypechecker.Stage.BEFORE_SOLVER, meta)); - contributor.declare(ModulePath.fromString("Paths.Meta"), LongName.fromString("rewrite2"), Precedence.DEFAULT, new DeferredMetaDefinition(ExpressionTypechecker.Stage.BEFORE_LEVELS, meta)); - contributor.declare(ModulePath.fromString("Paths.Meta"), LongName.fromString("rewrite3"), Precedence.DEFAULT, new DeferredMetaDefinition(ExpressionTypechecker.Stage.AFTER_LEVELS, meta)); + contributor.declare(ModulePath.fromString("Paths.Meta"), new LongName("rewrite"), Precedence.DEFAULT, new RewriteTactic(this, RewriteTactic.Mode.IMMEDIATE_BACKWARDS)); + contributor.declare(ModulePath.fromString("Paths.Meta"), new LongName("rewriteF"), Precedence.DEFAULT, new RewriteTactic(this, RewriteTactic.Mode.IMMEDIATE_FORWARD)); + contributor.declare(ModulePath.fromString("Paths.Meta"), new LongName("rewrite0"), Precedence.DEFAULT, new RewriteTactic(this, RewriteTactic.Mode.IMMEDIATE_BACKWARDS)); + contributor.declare(ModulePath.fromString("Paths.Meta"), new LongName("rewrite1"), Precedence.DEFAULT, new DeferredMetaDefinition(ExpressionTypechecker.Stage.BEFORE_SOLVER, meta)); + contributor.declare(ModulePath.fromString("Paths.Meta"), new LongName("rewrite2"), Precedence.DEFAULT, new DeferredMetaDefinition(ExpressionTypechecker.Stage.BEFORE_LEVELS, meta)); + contributor.declare(ModulePath.fromString("Paths.Meta"), new LongName("rewrite3"), Precedence.DEFAULT, new DeferredMetaDefinition(ExpressionTypechecker.Stage.AFTER_LEVELS, meta)); } } diff --git a/meta/src/main/java/org/arend/lib/tactic/RewriteTactic.java b/meta/src/main/java/org/arend/lib/tactic/RewriteTactic.java index cb70e21e..24daeda6 100644 --- a/meta/src/main/java/org/arend/lib/tactic/RewriteTactic.java +++ b/meta/src/main/java/org/arend/lib/tactic/RewriteTactic.java @@ -2,9 +2,9 @@ import org.arend.ext.concrete.ConcreteFactory; import org.arend.ext.concrete.expr.*; -import org.arend.ext.core.definition.CoreFunctionDefinition; import org.arend.ext.core.expr.CoreExpression; import org.arend.ext.core.expr.CoreFunCallExpression; +import org.arend.ext.core.expr.CoreInferenceReferenceExpression; import org.arend.ext.core.ops.CMP; import org.arend.ext.error.ErrorReporter; import org.arend.ext.error.TypeMismatchError; @@ -22,9 +22,17 @@ public class RewriteTactic extends BaseMetaDefinition { private final StdExtension ext; + private final Mode mode; - public RewriteTactic(StdExtension ext) { + public enum Mode { IMMEDIATE_FORWARD, IMMEDIATE_BACKWARDS, DEFERRED_BACKWARDS } + + public RewriteTactic(StdExtension ext, Mode mode) { this.ext = ext; + this.mode = mode; + } + + public RewriteTactic(StdExtension ext) { + this(ext, Mode.DEFERRED_BACKWARDS); } @Override @@ -43,9 +51,9 @@ private void getNumber(ConcreteExpression expression, Set result, Error @Override public CheckedExpression invoke(@NotNull ExpressionTypechecker typechecker, @NotNull ContextData contextData) { List args = contextData.getArguments(); - int argNum = 0; + int currentArg = 0; Set occurrences; - if (!args.get(0).isExplicit()) { + if (!args.isEmpty() && !args.get(0).isExplicit()) { occurrences = new HashSet<>(); if (args.get(0) instanceof ConcreteTupleExpression) { for (ConcreteExpression expr : ((ConcreteTupleExpression) args.get(0)).getFields()) { @@ -54,12 +62,18 @@ public CheckedExpression invoke(@NotNull ExpressionTypechecker typechecker, @Not } else { getNumber(args.get(0).getExpression(), occurrences, typechecker.getErrorReporter()); } - argNum++; + currentArg++; } else { occurrences = null; } - ConcreteExpression arg0 = args.get(argNum).getExpression(); + CoreExpression expectedType = contextData.getExpectedType() == null ? null : contextData.getExpectedType().getUnderlyingExpression(); + boolean isForward = mode == Mode.IMMEDIATE_FORWARD || expectedType == null || args.size() > currentArg + 2; + if ((isForward || mode == Mode.IMMEDIATE_BACKWARDS) && !checkContextData(contextData, typechecker.getErrorReporter())) { + return null; + } + + ConcreteExpression arg0 = args.get(currentArg++).getExpression(); CheckedExpression path = typechecker.typecheck(arg0); if (path == null) { return null; @@ -70,35 +84,63 @@ public CheckedExpression invoke(@NotNull ExpressionTypechecker typechecker, @Not return null; } - CoreExpression right = eq.getDefCallArguments().get(2); - CoreExpression type = contextData.getExpectedType(); ConcreteReferenceExpression refExpr = contextData.getReferenceExpression(); ConcreteFactory factory = ext.factory.withData(refExpr.getData()); + ConcreteExpression transport = factory.ref(ext.transport.getRef(), refExpr.getPLevel(), refExpr.getHLevel()); + + if (!isForward && mode == Mode.IMMEDIATE_BACKWARDS && expectedType instanceof CoreInferenceReferenceExpression) { + CoreExpression right = eq.getDefCallArguments().get(2).getUnderlyingExpression(); + if (right instanceof CoreInferenceReferenceExpression && ((CoreInferenceReferenceExpression) right).getVariable() == ((CoreInferenceReferenceExpression) expectedType).getVariable()) { + ArendRef ref = factory.local("T"); + return typechecker.typecheck(transport + .app(factory.lam(Collections.singletonList(factory.param(ref)), factory.ref(ref))) + .app(factory.core("transport (\\lam T => T) {!} _", path)) + .app(args.get(currentArg).getExpression())); + } + isForward = true; + } + + CheckedExpression lastArg; + CoreExpression value; + CoreExpression type; + if (isForward) { + lastArg = typechecker.typecheck(args.get(currentArg++).getExpression()); + if (lastArg == null) { + return null; + } + value = eq.getDefCallArguments().get(1); + type = lastArg.getType(); + } else { + lastArg = null; + value = eq.getDefCallArguments().get(2); + type = expectedType; + } + ArendRef ref = factory.local("x"); - return typechecker.typecheck( - factory.ref(ext.transport.getRef(), refExpr.getPLevel(), refExpr.getHLevel()) - .app(factory.lam(Collections.singletonList(factory.param(ref)), factory.meta("transport (\\lam x => {!}) _ _", new MetaDefinition() { - @Override - public CheckedExpression invoke(@NotNull ExpressionTypechecker typechecker, @NotNull ContextData contextData) { - CheckedExpression var = typechecker.typecheck(factory.ref(ref)); - assert var != null; - final int[] num = { 0 }; - CoreExpression absExpr = type.recreate(expression -> { - if (typechecker.compare(expression, right, CMP.EQ, refExpr)) { - num[0]++; - return occurrences == null || occurrences.contains(num[0]) ? var.getExpression() : null; - } else { - return null; - } - }); - if (absExpr == null) { - typechecker.getErrorReporter().report(new TypecheckingError("Cannot substitute expression", contextData.getReferenceExpression())); + return typechecker.typecheck(transport + .app(factory.lam(Collections.singletonList(factory.param(ref)), factory.meta("transport (\\lam x => {!}) _ _", new MetaDefinition() { + @Override + public CheckedExpression invoke(@NotNull ExpressionTypechecker typechecker, @NotNull ContextData contextData) { + CheckedExpression var = typechecker.typecheck(factory.ref(ref)); + assert var != null; + final int[] num = { 0 }; + CoreExpression absExpr = type.recreate(expression -> { + if (typechecker.compare(expression, value, CMP.EQ, refExpr)) { + num[0]++; + return occurrences == null || occurrences.contains(num[0]) ? var.getExpression() : null; + } else { return null; } - return typechecker.check(absExpr, refExpr); + }); + if (absExpr == null) { + typechecker.getErrorReporter().report(new TypecheckingError("Cannot substitute expression", contextData.getReferenceExpression())); + return null; } - }))) - .app(factory.core("transport _ {!} _", path)) - .app(args.get(argNum + 1).getExpression())); + return typechecker.check(absExpr, refExpr); + } + }))) + .app(factory.core("transport _ {!} _", path)) + .app(lastArg == null ? args.get(currentArg++).getExpression() : factory.core("transport _ _ {!}", lastArg)) + .app(args.subList(currentArg, args.size()))); } } diff --git a/src/Algebra/Monoid/GCD.ard b/src/Algebra/Monoid/GCD.ard index 60a84257..6008a0a4 100644 --- a/src/Algebra/Monoid/GCD.ard +++ b/src/Algebra/Monoid/GCD.ard @@ -198,6 +198,6 @@ (GCD.gcd|val2 {gcdC a (gcd a b * c)}) \lemma gcd_*_div {M : GCDMonoid} (a b c : M) (a|bc : LDiv a (b * c)) (a_b : GCD a b ide) : LDiv a c => - div-from~ (rewrite (pmap (`* in~ c) (gcd_~ a_b) *> ide-left (in~ c)) + div-from~ (rewrite1 (pmap (`* in~ c) (gcd_~ a_b) *> ide-left (in~ c)) (gcd_*_div~ (in~ a) (in~ b) (in~ c) (div-to~ a|bc))) } diff --git a/src/Algebra/Ring/Localization.ard b/src/Algebra/Ring/Localization.ard index f7c50661..f3053dd4 100644 --- a/src/Algebra/Ring/Localization.ard +++ b/src/Algebra/Ring/Localization.ard @@ -301,7 +301,7 @@ | in~ (r,(s,p)) => \let | j => path (~-equiv {SType S} (r,(s,p)) (r * ide, (ide * s, contains_* ide s contains_ide p)) (inv (*-assoc _ _ _))) | d r' => pmap (\lam (t : RingHom R Q) => func {t} r') q - | m1 => transport (\lam t => Inv {Q} t (g.func (in~ (ide, (s, p))))) (d s) (MonoidHom.presInv g (elem-inv S s p)) + | m1 => rewrite (d s) (MonoidHom.presInv g (elem-inv S s p)) | m2 => MonoidHom.presInv h (elem-inv S s p) \in g.func (in~ (r,(s,p))) ==< pmap g.func j >== g.func (in~ (r * ide, (ide * s, contains_* ide s contains_ide p))) ==< g.func-* (in~ (r, (ide, contains_ide))) (in~ (ide, (s, p))) >== diff --git a/src/Equiv.ard b/src/Equiv.ard index 7ec26326..fdff3a98 100644 --- a/src/Equiv.ard +++ b/src/Equiv.ard @@ -2,8 +2,9 @@ \import Equiv.Path \import Function \import HLevel -\import Paths \import Logic +\import Paths +\import Paths.Meta -- # Definition of equivalences @@ -18,7 +19,7 @@ idpe) \lemma isContr (e : Equiv) : Contr (Section e.f) - => transport (\lam X => Contr X) (inv (=Fiber e.f)) (Equiv=>contrFibers (-o_Equiv e) id) + => rewrite (inv (=Fiber e.f)) (Equiv=>contrFibers (-o_Equiv e) id) \lemma levelProp (r : Retraction) : isProp (Section r.f) => \lam s => isContr=>isProp (isContr (\new Equiv { | Section => s | Retraction => r })) s @@ -33,7 +34,7 @@ idpe) \lemma isContr (e : Equiv) : Contr (Retraction e.f) - => transport (\lam X => Contr X) (inv (=Fiber e.f)) (Equiv=>contrFibers (o-_Equiv e) id) + => rewrite (inv (=Fiber e.f)) (Equiv=>contrFibers (o-_Equiv e) id) \lemma levelProp (s : Section) : isProp (Retraction s.f) => \lam r => isContr=>isProp (isContr (\new Equiv { | Section => s | Retraction => r })) r @@ -50,10 +51,10 @@ \func equals {A B : \Type} {e e' : Equiv {A} {B}} (p : e.f = e'.f) : e = e' => path (\lam i => \new Equiv { | Section => pathOver (isContr=>isProp (Section.isContr e') - (transport (\lam f => Section f) p (\new Section e.f e.ret e.ret_f)) + (rewrite0 p (\new Section e.f e.ret e.ret_f)) (\new Section e'.f e'.ret e'.ret_f)) @ i | Retraction => pathOver (isContr=>isProp (Retraction.isContr e') - (transport (\lam f => Retraction f) p (\new Retraction e.f e.sec e.f_sec)) + (rewrite0 p (\new Retraction e.f e.sec e.f_sec)) (\new Retraction e'.f e'.sec e'.f_sec)) @ i }) diff --git a/src/Equiv/HalfAdjoint.ard b/src/Equiv/HalfAdjoint.ard index a699ad07..d0417dc7 100644 --- a/src/Equiv/HalfAdjoint.ard +++ b/src/Equiv/HalfAdjoint.ard @@ -3,6 +3,7 @@ \import Equiv.Univalence \import HLevel \import Paths +\import Paths.Meta \record HAEquiv (f_ret_f=f_sec_f : \Pi (x : A) -> pmap f (ret_f x) = f_sec (f x)) \extends QEquiv \where { @@ -26,7 +27,7 @@ | T1'-isContr (r : Retraction f) (x : A) : Contr (T1' r x) => isProp=>HLevel_-2+1 (Fib f (f x)) (isContr=>isProp (Equiv=>contrFibers e (f x))) _ _ | T1-isContr (r : Retraction f) (x : A) : Contr (T1 r x) => - transport (\lam A => Contr A) (T1'=T1 r x) (T1'-isContr r x) + rewrite (T1'=T1 r x) (T1'-isContr r x) | T2 => \Sigma (r : Retraction f) (\Pi (x : A) -> T1 r x) | T2-isContr : Contr T2 => HLevels_-2-sigma (\lam r => \Pi (x : A) -> T1 r x) {0} (Retraction.isContr e) @@ -38,5 +39,5 @@ | f_ret_f=f_sec_f x => (t.2 x).2 }) (\lam (r : HAEquiv f) => (\new Retraction f r.sec r.f_sec, \lam x => (r.ret_f x, r.f_ret_f=f_sec_f x))) (\lam t2 => idp) (\lam (hae : HAEquiv f) => idp {HAEquiv f hae.ret hae.ret_f hae.f_sec hae.f_ret_f=f_sec_f})) - \in isContr=>isProp (transport (\lam A => Contr A) E T2-isContr) e e' + \in isContr=>isProp (rewrite E T2-isContr) e e' } diff --git a/src/HLevel.ard b/src/HLevel.ard index 8aaecdb0..a9bc7972 100644 --- a/src/HLevel.ard +++ b/src/HLevel.ard @@ -41,7 +41,7 @@ \use \level levelProp (A : \Type) (c1 c2 : Contr A) : c1 = c2 => path (\lam i => \new Contr A { | center => c1.contraction c2.center @ i - | contraction => pathOver (path (\lam i a' => isProp=>isSet A (isContr=>isProp c1) c2.center a' (transport (\lam a => \Pi (a' : A) -> a = a') (c1.contraction c2.center) c1.contraction a') (c2.contraction a') @ i)) @ i + | contraction => pathOver (path (\lam i a' => isProp=>isSet A (isContr=>isProp c1) c2.center a' (rewrite (c1.contraction c2.center) c1.contraction a') (c2.contraction a') @ i)) @ i }) } diff --git a/src/Homotopy/Localization/Separated.ard b/src/Homotopy/Localization/Separated.ard index a29729ee..b5d9f586 100644 --- a/src/Homotopy/Localization/Separated.ard +++ b/src/Homotopy/Localization/Separated.ard @@ -50,7 +50,7 @@ } \in (\new Local { | local => B-local }, \new Localization { | local-univ C => Extension.contr-equiv f.f (\lam g b => \case f.isSurj b \with { - | inP (a',q) => rewrite q (coe (\lam i => Contr (\Sigma (c : C) (\Pi (a : f.A) -> inv (Equiv-to-= (local-univ {(p a a').2} (\new Local (g a = c) (local {C} (g a) c)))) @ i))) + | inP (a',q) => rewrite1 q (coe (\lam i => Contr (\Sigma (c : C) (\Pi (a : f.A) -> inv (Equiv-to-= (local-univ {(p a a').2} (\new Local (g a = c) (local {C} (g a) c)))) @ i))) (coe (\lam i => Contr (\Sigma (c : C) (inv (QEquiv-to-= (pi-contr-right a' (\lam x _ => g x = c))) @ i))) (lsigma (g a')) right) right) }) }) } diff --git a/src/Homotopy/Loop.ard b/src/Homotopy/Loop.ard index 1de988d5..2cc2bf61 100644 --- a/src/Homotopy/Loop.ard +++ b/src/Homotopy/Loop.ard @@ -18,7 +18,7 @@ (n : Nat) (p : \Pi (x0 : X) -> (x0 = x0) ofHLevel_-1+ n) : X ofHLevel_-1+ suc n - => \lam x x' => hLevel-inh n (\lam q => rewrite q (p x)) + => \lam x x' => hLevel-inh n (\lam q => rewrite1 q (p x)) \lemma loop-level-iter {X : \Type} (n : Nat) diff --git a/src/Homotopy/Pointed.ard b/src/Homotopy/Pointed.ard index 5646e2a3..535731b3 100644 --- a/src/Homotopy/Pointed.ard +++ b/src/Homotopy/Pointed.ard @@ -1,6 +1,7 @@ \import Homotopy.Space \import Logic \import Paths +\import Paths.Meta \class Pointed \extends InhSpace | base : E @@ -15,7 +16,7 @@ \where { \func ext {A B : Pointed} {f g : A ->* B} (p : \Pi (x : A) -> f.1 x = g.1 x) (q : p base *> g.2 = f.2) : f = g => \let | p' => path (\lam i x => p x @ i) - | q' => Jl (\lam _ p'' => transport (\lam (m : A -> B) => m base = base) p'' f.2 = inv (pmap (\lam (h : A -> B) => h base) p'') *> f.2) + | q' => Jl (\lam _ p'' => rewriteF p'' f.2 = inv (pmap (\lam (h : A -> B) => h base) p'') *> f.2) (inv (idp_*> _)) p' *> rotatePathLeft (inv q) \in path (\lam i => (p' @ i, pathOver q' @ i)) } diff --git a/src/Homotopy/Truncation.ard b/src/Homotopy/Truncation.ard index 01ce2e27..29212062 100644 --- a/src/Homotopy/Truncation.ard +++ b/src/Homotopy/Truncation.ard @@ -14,7 +14,7 @@ | isTruncated : A ofHLevel_-1+ n \where { \func ext {n : Nat} (t t' : Truncated_-1+ n) (p : t.A = t'.A) : t = t' => - path (\lam i => \new Truncated_-1+ n (p @ i) (pathOver (ofHLevel_-1+.levelProp t'.A n (transport (`ofHLevel_-1+ n) p t.isTruncated) t'.isTruncated) @ i)) + path (\lam i => \new Truncated_-1+ n (p @ i) (pathOver (ofHLevel_-1+.levelProp t'.A n (rewrite0 p t.isTruncated) t'.isTruncated) @ i)) \func equiv {n : Nat} (t t' : Truncated_-1+ n) : QEquiv {t = t'} {t.A = t'.A} => pathEquiv (\lam (t t' : Truncated_-1+ n) => t.A = t'.A) (\lam {t} {t'} => \new Retraction { @@ -63,7 +63,7 @@ | inT a => g a | hubT r => rewrite (path (spokeT r north)) (elim P g (r north)) | spokeT r x i => - \let | f y => transport (\lam x => P x) (path (spokeT r y)) (elim P g (r y)) + \let | f y => rewrite (path (spokeT r y)) (elim P g (r y)) | p0 => f north | c : Contr (Sphere.pointed n ->* Pointed.make p0) => rewrite (inv (SphereLoopEquiv n (Pointed.make p0)))