Merge branch 'complex'

meta/src/main/java/org/arend/lib/error/LinearSolverError.java

@@ -16,26 +16,38 @@
 
 public class LinearSolverError extends TypecheckingError {
   private final ExpressionPrettifier prettifier;
+  private final Equation<CoreExpression> equation;
   private final List<? extends Equation<CoreExpression>> equations;
 
-  public LinearSolverError(ExpressionPrettifier prettifier, boolean isContradiction, List<? extends Equation<CoreExpression>> equations, @Nullable ConcreteSourceNode cause) {
-    super(isContradiction ? "Cannot infer a contradiction" : "Cannot solve the equation", cause);
+  public LinearSolverError(ExpressionPrettifier prettifier, Equation<CoreExpression> equation, List<? extends Equation<CoreExpression>> equations, @Nullable ConcreteSourceNode cause) {
+    super(equation == null ? "Cannot infer a contradiction" : "Cannot solve the equation", cause);
+    this.equation = equation;
     this.prettifier = prettifier;
     this.equations = equations;
   }
 
+  private Doc getEquationDoc(Equation<CoreExpression> equation, PrettyPrinterConfig ppConfig) {
+    String op = switch (equation.operation) {
+      case LESS -> "<";
+      case LESS_OR_EQUALS -> "<=";
+      case EQUALS -> "=";
+    };
+    return hang(termDoc(equation.lhsTerm, prettifier, ppConfig), hang(text(op), termDoc(equation.rhsTerm, prettifier, ppConfig)));
+  }
+
   @Override
   public Doc getBodyDoc(PrettyPrinterConfig ppConfig) {
-    if (equations.isEmpty()) return nullDoc();
+    if (equations.isEmpty() && equation == null) return nullDoc();
     List<Doc> docs = new ArrayList<>(equations.size());
     for (Equation<CoreExpression> equation : equations) {
-      String op = switch (equation.operation) {
-        case LESS -> "<";
-        case LESS_OR_EQUALS -> "<=";
-        case EQUALS -> "=";
-      };
-      docs.add(hang(termDoc(equation.lhsTerm, prettifier, ppConfig), hang(text(op), termDoc(equation.rhsTerm, prettifier, ppConfig))));
+      docs.add(getEquationDoc(equation, ppConfig));
     }
-    return hang(text("Assumptions:"), vList(docs));
+    Doc result = hang(text("Assumptions:"), vList(docs));
+    return equation == null ? result : vList(hang(text("Equation:"), getEquationDoc(equation, ppConfig)), result);
+  }
+
+  @Override
+  public boolean hasExpressions() {
+    return !(equations.isEmpty() && equation == null);
   }
 }

meta/src/main/java/org/arend/lib/meta/linear/LinearSolver.java

@@ -48,10 +48,14 @@ public LinearSolver(ExpressionTypechecker typechecker, ConcreteSourceNode marker
     factory = ext.factory.withData(marker);
   }
 
+  private CoreClassDefinition getInstanceClass() {
+    return ext.equationMeta.LinearlyOrderedSemiring;
+  }
+
   private CoreExpression findInstance(CoreExpression type, boolean reportError) {
-    TypedExpression instance = typechecker.findInstance(ext.equationMeta.LinearlyOrderedSemiring, type, null, marker);
+    TypedExpression instance = type == null ? null : typechecker.findInstance(getInstanceClass(), type, null, marker);
     if (instance == null) {
-      if (reportError) errorReporter.report(new InstanceInferenceError(typechecker.getExpressionPrettifier(), ext.equationMeta.LinearlyOrderedSemiring.getRef(), type, marker));
+      if (reportError) errorReporter.report(new InstanceInferenceError(typechecker.getExpressionPrettifier(), getInstanceClass().getRef(), type, marker));
       return null;
     }
     return instance.getExpression();
@@ -97,13 +101,13 @@ private Hypothesis<CoreExpression> typeToEquation(CoreExpression type, CoreBindi
       if (field == ext.equationMeta.less || field == ext.equationMeta.lessOrEquals) {
         CoreExpression arg = fieldCall.getArgument();
         CoreExpression argType = arg.computeType().normalize(NormalizationMode.WHNF);
-        if (argType instanceof CoreClassCallExpression classCall && classCall.getDefinition().isSubClassOf(ext.equationMeta.LinearlyOrderedSemiring)) {
+        if (argType instanceof CoreClassCallExpression classCall && classCall.getDefinition().isSubClassOf(getInstanceClass())) {
           return new Hypothesis<>(expr, arg, field == ext.equationMeta.less ? Equation.Operation.LESS : Equation.Operation.LESS_OR_EQUALS, relationData.leftExpr, relationData.rightExpr, BigInteger.ONE);
         } else {
           if (reportError) errorReporter.report(new TypeError(typechecker.getExpressionPrettifier(), "", argType, marker) {
             @Override
             public LineDoc getShortHeaderDoc(PrettyPrinterConfig ppConfig) {
-              return DocFactory.hList(DocFactory.text("The type of the equation should be "), DocFactory.refDoc(ext.equationMeta.LinearlyOrderedSemiring.getRef()));
+              return DocFactory.hList(DocFactory.text("The type of the equation should be "), DocFactory.refDoc(getInstanceClass().getRef()));
             }
           });
           return null;
@@ -118,14 +122,21 @@ public LineDoc getShortHeaderDoc(PrettyPrinterConfig ppConfig) {
     }
 
     if (relationData.defCall.getDefinition() == ext.equationMeta.addGroupLess) {
-      return new Hypothesis<>(expr, relationData.defCall.getDefCallArguments().get(0), Equation.Operation.LESS, relationData.leftExpr, relationData.rightExpr, BigInteger.ONE);
+      CoreExpression instance = relationData.defCall.getDefCallArguments().get(0);
+      TypedExpression typedInstance = instance.computeTyped();
+      CoreExpression instanceType = typedInstance.getType().normalize(NormalizationMode.WHNF);
+      if (!(instanceType instanceof CoreClassCallExpression classCall && classCall.getDefinition().isSubClassOf(getInstanceClass()))) {
+        instance = findInstance(instanceType instanceof CoreClassCallExpression classCall ? Utils.getClassifyingExpression(classCall, typedInstance) : null, reportError);
+        if (instance == null) return null;
+      }
+      return new Hypothesis<>(expr, instance, Equation.Operation.LESS, relationData.leftExpr, relationData.rightExpr, BigInteger.ONE);
     }
 
     var pair = instanceCache.computeIfAbsent(relationData.defCall.getDefinition(), def -> {
       DefImplInstanceSearchParameters parameters = new DefImplInstanceSearchParameters(def) {
         @Override
         protected List<CoreClassField> getRelationFields(CoreClassDefinition classDef) {
-          return classDef.isSubClassOf(ext.equationMeta.LinearlyOrderedSemiring) ? Arrays.asList(ext.equationMeta.less, ext.equationMeta.lessOrEquals) : Collections.emptyList();
+          return classDef.isSubClassOf(getInstanceClass()) ? Arrays.asList(ext.equationMeta.less, ext.equationMeta.lessOrEquals) : Collections.emptyList();
         }
       };
       TypedExpression instance = typechecker.findInstance(parameters, null, null, marker);
@@ -583,7 +594,7 @@ public TypedExpression solve(CoreExpression expectedType, ConcreteExpression hin
       }
     }
 
-    errorReporter.report(new LinearSolverError(typechecker.getExpressionPrettifier(), resultEquation == null, rules, marker));
+    errorReporter.report(new LinearSolverError(typechecker.getExpressionPrettifier(), resultEquation, rules, marker));
     return null;
   }
 }

meta/src/main/java/org/arend/lib/util/Utils.java

@@ -481,4 +481,9 @@ public static ArendRef getReference(ConcreteExpression expr, ErrorReporter error
     errorReporter.report(new TypecheckingError("Expected a reference", expr));
     return null;
   }
+
+  public static CoreExpression getClassifyingExpression(CoreClassCallExpression classCall, TypedExpression thisExpr) {
+    CoreClassField field = classCall.getDefinition().getClassifyingField();
+    return field == null ? null : classCall.getImplementation(field, thisExpr);
+  }
 }

src/Algebra/Field.ard

@@ -130,6 +130,9 @@
 
   \lemma decideZeroOrInv (x : E) : (x = 0) `Or` Inv x
     => aux zro/=ide x (eitherZeroOrInv x)
+
+  \lemma finv-diff {x : E} (xi : x /= 0) (x+1i : x + 1 /= 0) : finv x - finv (x + 1) = finv (x * (x + 1))
+    => equation {usingOnly (finv-right xi, finv-right x+1i, finv-right $ nonZero_* xi x+1i)}
 } \where {
   \private \lemma aux {R : CRing} (p : zro /= {R} ide) (x : R) (q : (x = 0) || Inv x) : (x = 0) `Or` Inv x
     \level Or.levelProp (\lam x=0 (j : Inv x) => p $ inv zro_*-left *> pmap (`* _) (inv x=0) *> j.inv-right)

src/Algebra/Field/Algebraic.ard

@@ -6,6 +6,7 @@
 \import Algebra.Monoid
 \import Algebra.Monoid.Category
 \import Algebra.Monoid.PermSet
+\import Algebra.Ordered
 \import Algebra.Pointed
 \import Algebra.Pointed.Category
 \import Algebra.Ring
@@ -132,7 +133,7 @@
                         {d : Nat} (pd : \Pi (j : Fin pl.len) -> permSet-length (pl j) < d) (a : Array R n) (pl/=0 : pl.len /= 0) {p : MPoly (Fin n) R} (pp : p = BigSum \lam j => msMonomial (pc j) (pl j))
         : ∃ (m : Nat) (degree<= (change-vars p d a) m) (Inv (polyCoef (change-vars p d a) m)) \elim pp
         | idp =>
-          \let | pow>0 {n} : 0 < pow d n => NatSemiring.pow>0 $ zero<=_ <∘r pd (transport Fin (suc_pred pl/=0) 0)
+          \let | pow>0 {n} : 0 < pow d n => NatSemiring.pow>0 $ zero<=_ <-transitive-right pd (transport Fin (suc_pred pl/=0) 0)
                | (m,rd,ri) => poly-degrees {_} {\lam j => change-vars (msMonomial 1 (pl j)) d a} pc
                     (\lam j => permSet-univ {_} {AbMonoid.toCMonoid NatSemiring} (later \lam i => pow d i) (pl j))
                     (\lam j => rewrite (change-vars_monomial {_} {_} {pl j}) $ permSet-univ_monic {_} {\lam j => padd pzero (a j) + pow (padd 1 0) (pow d j)} {\lam j => pow d j}

src/Algebra/Group.ard

@@ -212,6 +212,12 @@
   \lemma BigSum_negative {l : Array E} : negative (BigSum l) = BigSum (map negative l) \elim l
     | nil => negative_zro
     | a :: l => negative_+ *> +-comm *> pmap (_ +) BigSum_negative
+
+  \lemma sum-cancel-left {x y z : E} : x + z - (x + y) = z - y
+    => pmap (_ +) negative_+ *> pmap2 (+) +-comm +-comm *> +-assoc *> pmap (z +) (inv +-assoc *> pmap (`- y) negative-right *> zro-left)
+
+  \lemma diff-cancel-left {x y z : E} : x - z - (x - y) = y - z
+    => sum-cancel-left *> +-comm *> pmap (`- z) negative-isInv
 } \where {
     \use \coerce fromCGroup (G : CGroup) => \new AbGroup G.E G.ide (G.*) G.ide-left G.ide-right G.*-assoc G.inverse G.inverse-left G.*-comm
     \use \coerce toCGroup (G : AbGroup) => \new CGroup G.E G.zro (G.+) G.zro-left G.zro-right G.+-assoc G.negative G.negative-left G.+-comm