swap the argument order in equational reasoning (#999)

* swap the argument order in equational reasoning

* [#998]: Remove unused code, fix imports

---------

Co-authored-by: Felix Cherubini <[email protected]>

Cubical/Data/Equality.agda

@@ -9,7 +9,7 @@ defined equality types.
 module Cubical.Data.Equality where
 
 open import Cubical.Foundations.Prelude public
-  hiding ( _≡_ ; _≡⟨_⟩_ ; _∎ ; isPropIsContr)
+  hiding ( _≡_ ; step-≡ ; _∎ ; isPropIsContr)
   renaming ( refl      to reflPath
            ; transport to transportPath
            ; J         to JPath

Cubical/Foundations/Id.agda

@@ -21,7 +21,7 @@ This file contains:
 module Cubical.Foundations.Id where
 
 open import Cubical.Foundations.Prelude public
-  hiding ( _≡_ ; _≡⟨_⟩_ ; _∎ ; isPropIsContr)
+  hiding ( _≡_ ; step-≡ ; _∎ ; isPropIsContr)
   renaming ( refl      to reflPath
            ; transport to transportPath
            ; J         to JPath

Cubical/Foundations/Prelude.agda

@@ -28,7 +28,7 @@ open import Cubical.Core.Primitives public
 infixr 30 _∙_
 infixr 30 _∙₂_
 infix  3 _∎
-infixr 2 _≡⟨_⟩_ _≡⟨⟩_
+infixr 2 step-≡ _≡⟨⟩_
 infixr 2.5 _≡⟨_⟩≡⟨_⟩_
 infixl 4 _≡$_ _≡$S_
 
@@ -233,13 +233,16 @@ compPathP'-filler {B = B} {x' = x'} {p = p} {q = q} P Q j i =
 
 -- Syntax for chains of equational reasoning
 
-_≡⟨_⟩_ : (x : A) → x ≡ y → y ≡ z → x ≡ z
-_ ≡⟨ x≡y ⟩ y≡z = x≡y ∙ y≡z
+step-≡ : (x : A) → y ≡ z → x ≡ y → x ≡ z
+step-≡ _ p q = q ∙ p
+
+syntax step-≡ x y p = x ≡⟨ p ⟩ y
+
+≡⟨⟩-syntax : (x : A) → y ≡ z → x ≡ y → x ≡ z
+≡⟨⟩-syntax = step-≡
 
-≡⟨⟩-syntax : (x : A) → x ≡ y → y ≡ z → x ≡ z
-≡⟨⟩-syntax = _≡⟨_⟩_
 infixr 2 ≡⟨⟩-syntax
-syntax ≡⟨⟩-syntax x (λ i → B) y = x ≡[ i ]⟨ B ⟩ y
+syntax ≡⟨⟩-syntax x y (λ i → B) = x ≡[ i ]⟨ B ⟩ y
 
 _≡⟨⟩_ : (x : A) → x ≡ y → x ≡ y
 _ ≡⟨⟩ x≡y = x≡y

Cubical/Tactics/CommRingSolver/Examples.agda

@@ -104,16 +104,16 @@ module TestInPlaceSolving (R : CommRing ℓ) where
    testWithOneVariabl : (x : fst R) → x + 0r ≡ 0r + x
    testWithOneVariabl x = solveInPlace R (x ∷ [])
 
-   testEquationalReasoning : (x : fst R) → x + 0r ≡ 0r + x
-   testEquationalReasoning x =
-     x + 0r                       ≡⟨solveIn R withVars (x ∷ []) ⟩
-     0r + x ∎
-
    testWithTwoVariables :  (x y : fst R) → x + y ≡ y + x
    testWithTwoVariables x y =
-     x + y                      ≡⟨solveIn R withVars (x ∷ y ∷ []) ⟩
+     x + y                      ≡⟨ solveInPlace R (x ∷ y ∷ []) ⟩
      y + x ∎
 
+   testEquationalReasoning : (x : fst R) → x + 0r ≡ 0r + x
+   testEquationalReasoning x =
+     x + 0r                       ≡⟨ solveInPlace R (x ∷ []) ⟩
+     0r + x ∎
+
    {-
      So far, solving during equational reasoning has a serious
      restriction:
@@ -122,8 +122,8 @@ module TestInPlaceSolving (R : CommRing ℓ) where
      entails that in the following code, the order of 'p' and 'x' cannot be
      switched.
    -}
-   testEquationalReasoning' :  (p : (y : fst R) → 0r + y ≡ 1r) (x : fst R) → x + 0r ≡ 1r
+   testEquationalReasoning' : (p : (y : fst R) → 0r + y ≡ 1r) (x : fst R) → x + 0r ≡ 1r
    testEquationalReasoning' p x =
-     x + 0r              ≡⟨solveIn R withVars (x ∷ []) ⟩
+     x + 0r              ≡⟨ solveInPlace R (x ∷ []) ⟩
      0r + x              ≡⟨ p x ⟩
      1r ∎

Cubical/Tactics/CommRingSolver/Reflection.agda

@@ -104,29 +104,6 @@ private
   getArgs : Term → Maybe (Term × Term)
   getArgs = getLastTwoArgsOf (quote PathP)
 
-
-  firstVisibleArg : List (Arg Term) → Maybe Term
-  firstVisibleArg [] = nothing
-  firstVisibleArg (varg x ∷ l) = just x
-  firstVisibleArg (x ∷ l) = firstVisibleArg l
-
-  {-
-    If the solver needs to be applied during equational reasoning,
-    the right hand side of the equation to solve cannot be given to
-    the solver directly. The folllowing function extracts this term y
-    from a more complex expression as in:
-      x ≡⟨ solve ... ⟩ (y ≡⟨ ... ⟩ z ∎)
-  -}
-  getRhs : Term → Maybe Term
-  getRhs (def n xs) =
-    if n == (quote _∎)
-    then firstVisibleArg xs
-    else (if n == (quote _≡⟨_⟩_)
-         then firstVisibleArg xs
-         else nothing)
-  getRhs _ = nothing
-
-
   private
     solverCallAsTerm : Term → Arg Term → Term → Term → Term
     solverCallAsTerm R varList lhs rhs =
@@ -348,39 +325,12 @@ private
       let solution = solverCallByVarIndices (length varIndices) varIndices cring lhs rhs
       unify hole solution
 
-  solveEqReasoning-macro : Term → Term → Term → Term → Term → TC Unit
-  solveEqReasoning-macro lhs cring varsToSolve reasoningToTheRight hole =
-    do
-      names ← findRingNames cring
-      just varIndices ← returnTC (extractVarIndices (toListOfTerms varsToSolve))
-        where nothing → variableExtractionError varsToSolve
-
-      just rhs ← returnTC (getRhs reasoningToTheRight)
-        where
-          nothing
-            → typeError(
-                strErr "Failed to extract right hand side of equation to solve from " ∷
-                termErr reasoningToTheRight ∷ [])
-      just (lhsAST , rhsAST) ← returnTC (toAlgebraExpression cring names (just (lhs , rhs)))
-        where
-          nothing
-            → typeError(
-                strErr "Error while trying to build ASTs from " ∷
-                termErr lhs ∷ strErr " and " ∷ termErr rhs ∷ [])
-      let solverCall = solverCallByVarIndices (length varIndices) varIndices cring lhsAST rhsAST
-      unify hole (def (quote _≡⟨_⟩_) (varg lhs ∷ varg solverCall ∷ varg reasoningToTheRight ∷ []))
-
 macro
   solve : Term → Term → TC _
   solve = solve-macro
 
   solveInPlace : Term → Term → Term → TC _
   solveInPlace = solveInPlace-macro
 
-  infixr 2 _≡⟨solveIn_withVars_⟩_
-  _≡⟨solveIn_withVars_⟩_ : Term → Term → Term → Term → Term → TC Unit
-  _≡⟨solveIn_withVars_⟩_ = solveEqReasoning-macro
-
-
 fromℤ : (R : CommRing ℓ) → ℤ → fst R
 fromℤ = scalar

Cubical/Tactics/MonoidSolver/Reflection.agda

@@ -60,29 +60,6 @@ module ReflectionSolver (op unit solver : Name) where
   getArgs : Term → Maybe (Term × Term)
   getArgs = getLastTwoArgsOf (quote PathP)
 
-
-  firstVisibleArg : List (Arg Term) → Maybe Term
-  firstVisibleArg [] = nothing
-  firstVisibleArg (varg x ∷ l) = just x
-  firstVisibleArg (x ∷ l) = firstVisibleArg l
-
-  {-
-    If the solver needs to be applied during equational reasoning,
-    the right hand side of the equation to solve cannot be given to
-    the solver directly. The following function extracts this term y
-    from a more complex expression as in:
-      x ≡⟨ solve ... ⟩ (y ≡⟨ ... ⟩ z ∎)
-  -}
-  getRhs : Term → Maybe Term
-  getRhs reasoningToTheRight@(def n xs) =
-    if n == (quote _∎)
-    then firstVisibleArg xs
-    else (if n == (quote _≡⟨_⟩_)
-         then firstVisibleArg xs
-         else nothing)
-  getRhs _ = nothing
-
-
   private
     solverCallAsTerm : Term → Arg Term → Term → Term → Term
     solverCallAsTerm M varList lhs rhs =

Cubical/Tactics/NatSolver/Reflection.agda

@@ -65,29 +65,6 @@ private
   getArgs : Term → Maybe (Term × Term)
   getArgs = getLastTwoArgsOf (quote PathP)
 
-
-  firstVisibleArg : List (Arg Term) → Maybe Term
-  firstVisibleArg [] = nothing
-  firstVisibleArg (varg x ∷ l) = just x
-  firstVisibleArg (x ∷ l) = firstVisibleArg l
-
-  {-
-    If the solver needs to be applied during equational reasoning,
-    the right hand side of the equation to solve cannot be given to
-    the solver directly. The folllowing function extracts this term y
-    from a more complex expression as in:
-      x ≡⟨ solve ... ⟩ (y ≡⟨ ... ⟩ z ∎)
-  -}
-  getRhs : Term → Maybe Term
-  getRhs reasoningToTheRight@(def n xs) =
-    if n == (quote _∎)
-    then firstVisibleArg xs
-    else (if n == (quote _≡⟨_⟩_)
-         then firstVisibleArg xs
-         else nothing)
-  getRhs _ = nothing
-
-
   private
     solverCallAsTerm : Arg Term → Term → Term → Term
     solverCallAsTerm varList lhs rhs =