Replace transport with rewrite0 and rewriteF

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));
   }
 }

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<Integer> result, Error
   @Override
   public CheckedExpression invoke(@NotNull ExpressionTypechecker typechecker, @NotNull ContextData contextData) {
     List<? extends ConcreteArgument> args = contextData.getArguments();
-    int argNum = 0;
+    int currentArg = 0;
     Set<Integer> 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())));
   }
 }

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)))
   }

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))) >==

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
       })
 

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'
   }

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
       })
   }
 

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)
             }) })
   }

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)

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))
   }

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)))