reals - order, got rid of lossy unification, and aplied solver

Author: marcinjangrzybowski

Cubical/Data/Rationals/Fast/Properties.agda

@@ -455,12 +455,38 @@ maxAbsorbLMin = SetQuotient.elimProp2 (λ _ _ → isSetℚ _ _)
         ≡⟨ sym (ℤ.·DistR+ (ℕ₊₁→ℤ b) (c ℤ.· ℕ₊₁→ℤ f) (e ℤ.· ℕ₊₁→ℤ d)) ⟩
       ℕ₊₁→ℤ b ℤ.· (c ℤ.· ℕ₊₁→ℤ f ℤ.+ e ℤ.· ℕ₊₁→ℤ d) ∎
 
+_impl+_ : ℚ → ℚ → ℚ
+_impl+_ = OnCommonDenomSym.go +Rec
 
 _+_ : ℚ → ℚ → ℚ
-_+_ = OnCommonDenomSym.go +Rec
+[ a ] + [ a₁ ] = [ a ] impl+ [ a₁ ]
+[ a ] + eq/ a₁ b r i = [ a ] impl+ (eq/ a₁ b r i)
+[ a ] + _//_.squash/ x₁ x₂ p q i i₁ =
+  isSetℚ ([ a ] + x₁) ([ a ] + x₂) (λ i₁ → [ a ] + p i₁) (λ i₁ → [ a ] + q i₁)  i i₁
+eq/ a b r i + [ a₁ ] = (eq/ a b r i) impl+ [ a₁ ]
+eq/ a b r i + eq/ a₁ b₁ r₁ i₁ =
+ isSet→isSet' isSetℚ
+   (λ i₁ → [ a ] impl+ eq/ a₁ b₁ r₁ i₁) (λ i₁ → [ b ] impl+ eq/ a₁ b₁ r₁ i₁)
+   (λ i → eq/ a b r i impl+ [ a₁ ]) (λ i → eq/ a b r i impl+ [ b₁ ]) i i₁
+eq/ a b r i + _//_.squash/ x₁ x₂ p q i₁ i₂ =
+  isGroupoid→isGroupoid' (isSet→isGroupoid isSetℚ)
+    (λ i₁ i₂ → isSetℚ ([ a ] + x₁) ([ a ] + x₂) (λ i₃ → [ a ] + p i₃) (λ i₃ → [ a ] + q i₃) i₁ i₂)
+    (λ i₁ i₂ → isSetℚ ([ b ] + x₁) ([ b ] + x₂) (λ i₃ → [ b ] + p i₃) (λ i₃ → [ b ] + q i₃) i₁ i₂)
+    (λ i i₂ → eq/ a b r i + p i₂) (λ i i₂ → eq/ a b r i + q i₂)
+    (λ i i₁ → eq/ a b r i + x₁) (λ i i₁ → eq/ a b r i + x₂)
+    i i₁ i₂
+_//_.squash/ x x₁ p q i i₁ + z =
+  isSetℚ (x + z) (x₁ + z) (cong (_+ z) p) (cong (_+ z) q) i i₁
+
++-impl : ∀ x y → x + y ≡ x impl+ y
++-impl = SetQuotient.ElimProp2.go w
+ where
+ w : SetQuotient.ElimProp2 (λ z z₁ → z + z₁ ≡ (z impl+ z₁))
+ w .SetQuotient.ElimProp2.isPropB _ _ = isSetℚ _ _
+ w .SetQuotient.ElimProp2.f _ _ = refl
 
 +Comm : ∀ x y → x + y ≡ y + x
-+Comm = OnCommonDenomSym.go-comm +Rec
++Comm x y = +-impl x y ∙∙ OnCommonDenomSym.go-comm +Rec x y ∙∙ sym (+-impl y x)
 
 +IdL : ∀ x → 0 + x ≡ x
 +IdL = SetQuotient.elimProp (λ _ → isSetℚ _ _)
@@ -479,11 +505,39 @@ _+_ = OnCommonDenomSym.go +Rec
 ·Rec .OnCommonDenomSym.g-sym (a , _) (c , _) = ℤ.·Comm a c
 ·Rec .OnCommonDenomSym.g-eql (a , b) (c , d) (e , _) p = lem₁ a (ℕ₊₁→ℤ d) c (ℕ₊₁→ℤ b) e p
 
+_impl·_ : ℚ → ℚ → ℚ
+_impl·_ = OnCommonDenomSym.go ·Rec
+
 _·_ : ℚ → ℚ → ℚ
-_·_ = OnCommonDenomSym.go ·Rec
+[ a ] · [ a₁ ] = [ a ] impl· [ a₁ ]
+[ a ] · eq/ a₁ b r i = [ a ] impl· (eq/ a₁ b r i)
+[ a ] · _//_.squash/ x₁ x₂ p q i i₁ =
+  isSetℚ ([ a ] · x₁) ([ a ] · x₂) (λ i₁ → [ a ] · p i₁) (λ i₁ → [ a ] · q i₁)  i i₁
+eq/ a b r i · [ a₁ ] = (eq/ a b r i) impl· [ a₁ ]
+eq/ a b r i · eq/ a₁ b₁ r₁ i₁ =
+ isSet→isSet' isSetℚ
+   (λ i₁ → [ a ] impl· eq/ a₁ b₁ r₁ i₁) (λ i₁ → [ b ] impl· eq/ a₁ b₁ r₁ i₁)
+   (λ i → eq/ a b r i impl· [ a₁ ]) (λ i → eq/ a b r i impl· [ b₁ ]) i i₁
+eq/ a b r i · _//_.squash/ x₁ x₂ p q i₁ i₂ =
+  isGroupoid→isGroupoid' (isSet→isGroupoid isSetℚ)
+    (λ i₁ i₂ → isSetℚ ([ a ] · x₁) ([ a ] · x₂) (λ i₃ → [ a ] · p i₃) (λ i₃ → [ a ] · q i₃) i₁ i₂)
+    (λ i₁ i₂ → isSetℚ ([ b ] · x₁) ([ b ] · x₂) (λ i₃ → [ b ] · p i₃) (λ i₃ → [ b ] · q i₃) i₁ i₂)
+    (λ i i₂ → eq/ a b r i · p i₂) (λ i i₂ → eq/ a b r i · q i₂)
+    (λ i i₁ → eq/ a b r i · x₁) (λ i i₁ → eq/ a b r i · x₂)
+    i i₁ i₂
+_//_.squash/ x x₁ p q i i₁ · z =
+  isSetℚ (x · z) (x₁ · z) (cong (_· z) p) (cong (_· z) q) i i₁
+
+·-impl : ∀ x y → x · y ≡ x impl· y
+·-impl = SetQuotient.ElimProp2.go w
+ where
+ w : SetQuotient.ElimProp2 (λ z z₁ → z · z₁ ≡ (z impl· z₁))
+ w .SetQuotient.ElimProp2.isPropB _ _ = isSetℚ _ _
+ w .SetQuotient.ElimProp2.f _ _ = refl
 
 ·Comm : ∀ x y → x · y ≡ y · x
-·Comm = OnCommonDenomSym.go-comm ·Rec
+·Comm x y = ·-impl x y ∙∙ OnCommonDenomSym.go-comm ·Rec x y ∙∙ sym (·-impl y x)
+
 
 ·IdL : ∀ x → 1 · x ≡ x
 ·IdL = SetQuotient.elimProp (λ _ → isSetℚ _ _) λ (_ , _) → eq/ _ _ ℤ!
@@ -633,3 +687,25 @@ x+x≡2x x = cong₂ _+_
     (sym (·IdL x))
     (sym (·IdL x))
     ∙ sym (·DistR+ 1 1 x)
+
+
+eqElim : (lrhs : ℚ → ℚ × ℚ) →
+  (∀ {k m} → fst (lrhs ([ (k , 1+ m) ]))
+        ≡  snd (lrhs ([ (k , 1+ m) ])))
+    → ∀ (ε : ℚ) → fst (lrhs ε) ≡ snd (lrhs ε)
+eqElim lrhs p = SetQuotient.ElimProp.go w
+  where
+
+  w : SetQuotient.ElimProp (λ z → fst (lrhs z) ≡ snd (lrhs z))
+  w .SetQuotient.ElimProp.isPropB _ = isSetℚ _ _
+  w .SetQuotient.ElimProp.f (n , (1+ n₁)) = p {n} {n₁}
+
+eqElim₂ : (lrhs : ℚ → ℚ → ℚ × ℚ) →
+  (∀ {k m k' m'} → fst (lrhs [ (k , 1+ m) ] [ (k' , 1+ m') ])
+        ≡  snd (lrhs [ (k , 1+ m) ] [ (k' , 1+ m') ]))
+    → ∀ (x y : ℚ) → fst (lrhs x y) ≡ (snd (lrhs x y))
+eqElim₂ lrhs p = SetQuotient.ElimProp2.go w
+  where
+  w : SetQuotient.ElimProp2 (λ z z' → fst (lrhs z z') ≡ snd (lrhs z z'))
+  w .SetQuotient.ElimProp2.isPropB _ _ = isSetℚ _ _
+  w .SetQuotient.ElimProp2.f (n , (1+ n₁)) (m , (1+ m₁)) = p {n} {n₁} {m} {m₁}

Cubical/HITs/CauchyReals/Order.agda

@@ -91,7 +91,7 @@ opaque
 
 
 
- +ᵣ-impl : ∀ x y → x +ᵣ y ≡ NonExpanding₂.go sumR x y 
+ +ᵣ-impl : ∀ x y → x +ᵣ y ≡ NonExpanding₂.go sumR x y
  +ᵣ-impl _ _ = refl
 
  rat-+ᵣ-lim : ∀ r x y → rat r +ᵣ lim x y ≡ lim (λ ε → rat r +ᵣ x ε)
@@ -184,9 +184,9 @@ opaque
  maxᵣ : ℝ → ℝ → ℝ
  maxᵣ = NonExpanding₂.go maxR
 
- maxᵣ-impl : ∀ x y → maxᵣ x y ≡ NonExpanding₂.go maxR x y 
+ maxᵣ-impl : ∀ x y → maxᵣ x y ≡ NonExpanding₂.go maxR x y
  maxᵣ-impl _ _ = refl
- 
+
  minᵣ-rat : ∀ a b → minᵣ (rat a) (rat b) ≡ rat (ℚ.min a b)
  minᵣ-rat _ _ = refl
 
@@ -336,24 +336,21 @@ opaque
        x' = x ℚ.+ fst (/3₊ (y-x))
        y' = x' ℚ.+ fst (/3₊ (y-x))
    in ∣ (x' , y') ,
-           ≤ℚ→≤ᵣ x x' (
-              subst (ℚ._≤ x') (ℚ.+IdR x)
-                    (ℚ.≤-o+ 0 (fst (/3₊ (y-x))) x
-                     (ℚ.0≤ℚ₊ (/3₊ (y-x)))) )
-         , subst (ℚ._< y') (ℚ.+IdR x')
-                    (ℚ.<-o+ 0 (fst (/3₊ (y-x))) x'
-                     (ℚ.0<ℚ₊ (/3₊ (y-x))))
-         , ≤ℚ→≤ᵣ y' y
-             (subst2 {x = y' ℚ.+ 0} {y = y'} (ℚ._≤_) (ℚ.+IdR y')
-                ({!!}
-                  ∙∙
-                   cong {x = ℚ.[ 1 / 3 ] ℚ.+ ℚ.[ 1 / 3 ] ℚ.+ ℚ.[ 1 / 3 ]}
-                     {1} (λ a → x ℚ.+ a ℚ.· (y ℚ.- x))
-                    ℚ.decℚ?
-                   ∙∙ (cong (x ℚ.+_) (ℚ.·IdL (y ℚ.- x))
-                       ∙ ℚ!))
-               ((ℚ.≤-o+ 0 (fst (/3₊ (y-x))) y'
-                     (ℚ.0≤ℚ₊ (/3₊ (y-x))))))  ∣₁
+       (let p : ∀ x y → ((x ℚ.+ ((y ℚ.- x) ℚ.· [ 1 / 3 ]))
+                   ℚ.+ ((y ℚ.- x) ℚ.· [ 1 / 3 ])) ℚ.+ ((y ℚ.- x) ℚ.· [ 1 / 3 ]) ≡ y
+            p = ℚ.eqElim₂ _ (ℚ.eqℚ ℤ!)
+        in (≤ℚ→≤ᵣ x x' (
+                 subst (ℚ._≤ x') (ℚ.+IdR x)
+                       (ℚ.≤-o+ 0 (fst (/3₊ (y-x))) x
+                        (ℚ.0≤ℚ₊ (/3₊ (y-x)))) )
+            , subst (ℚ._< y') (ℚ.+IdR x')
+                       (ℚ.<-o+ 0 (fst (/3₊ (y-x))) x'
+                        (ℚ.0<ℚ₊ (/3₊ (y-x))))
+            , ≤ℚ→≤ᵣ y' y
+                (subst2 {x = y' ℚ.+ 0} {y = y'} (ℚ._≤_) (ℚ.+IdR y')
+                    (p x y)
+                  ((ℚ.≤-o+ 0 (fst (/3₊ (y-x))) y'
+                        (ℚ.0≤ℚ₊ (/3₊ (y-x))))))))  ∣₁
 
  <ᵣ→<ℚ : ∀ q r → rat q <ᵣ rat r → q ℚ.< r
  <ᵣ→<ℚ = ElimProp2.go w
@@ -465,7 +462,7 @@ opaque
 
  -ᵣ-impl : ∀ x → -ᵣ x ≡ fst (fromLipschitz (1 , _) ((rat ∘ ℚ.-_ ) , ℚ-isLip)) x
  -ᵣ-impl x = refl
- 
+
  -ᵣ-lip : Lipschitz-ℝ→ℝ 1 -ᵣ_
  -ᵣ-lip = snd -ᵣR
 
@@ -578,7 +575,7 @@ opaque
 
  absᵣ : ℝ → ℝ
  absᵣ = fst absᵣL
- 
+
  absᵣ0 : absᵣ 0 ≡ 0
  absᵣ0 = refl
 
@@ -675,7 +672,7 @@ opaque
  w .Elimℝ-Prop2Sym.rat-ratA r q = (cong -ᵣ_ (+ᵣ-rat _ _) ∙ -ᵣ-rat _) ∙ cong rat (ℚ.-Distr r q) ∙
    sym (+ᵣ-rat _ _) ∙
     cong₂ _+ᵣ_ (sym (-ᵣ-rat _)) (sym (-ᵣ-rat _))
- w .Elimℝ-Prop2Sym.rat-limA r x y x₁ =   
+ w .Elimℝ-Prop2Sym.rat-limA r x y x₁ =
    cong (-ᵣ_) (rat-+ᵣ-lim _ _ _)
     ∙  -ᵣ-lim' _ _
     ∙  (congLim _ _ _ _  λ q → x₁ q ∙ cong (_-ᵣ x q) (-ᵣ-rat r))
@@ -704,9 +701,32 @@ opaque
  minusComm-absᵣ : ∀ x y → absᵣ (x +ᵣ (-ᵣ y)) ≡ absᵣ (y +ᵣ (-ᵣ x))
  minusComm-absᵣ x y = -absᵣ _ ∙ cong absᵣ (-[x-y]≡y-x x y)
 
-
+opaque
+ unfolding _<ᵣ_
  denseℚinℝ : ∀ u v → u <ᵣ v → ∃[ q ∈ ℚ ] ((u <ᵣ rat q) × (rat q <ᵣ v))
- denseℚinℝ u v = {!!}
+ denseℚinℝ u v =
+  PT.map λ ((p , q) , u≤p , p<q , q≤v) →
+  let
+    m = (p ℚ.+ q) ℚ.· [ 1 / 2 ]
+    p<m = subst2 ℚ._<_ (
+      p ℚ.· [ 1 / 2 ] ℚ.+ p ℚ.· [ 1 / 2 ] ≡⟨ sym $ ℚ.·DistL+ p [ 1 / 2 ] [ 1 / 2 ] ⟩
+      p ℚ.· [ 4 / 4 ]                      ≡⟨ cong (p ℚ.·_) (ℚ.[n/n]≡[m/m] 3 0) ⟩
+      p ℚ.· [ 1 / 1 ]                      ≡⟨ ℚ.·IdR p ⟩
+      p                                    ∎)
+      (sym (ℚ.·DistR+ p q [ 1 / 2 ]))
+      (ℚ.<-o+ (p ℚ.· [ 1 / 2 ]) (q ℚ.· [ 1 / 2 ]) (p ℚ.· [ 1 / 2 ])
+        (ℚ.<-·o p q [ 1 / 2 ] (ℚ.0<pos 0 2) p<q))
+    m<q = subst2 ℚ._<_
+      (sym (ℚ.·DistR+ p q [ 1 / 2 ]))
+      (
+      q ℚ.· [ 1 / 2 ] ℚ.+ q ℚ.· [ 1 / 2 ] ≡⟨ sym $ ℚ.·DistL+ q [ 1 / 2 ] [ 1 / 2 ] ⟩
+      q ℚ.· [ 4 / 4 ]                      ≡⟨ cong (q ℚ.·_) (ℚ.[n/n]≡[m/m] 3 0) ⟩
+      q ℚ.· [ 1 / 1 ]                      ≡⟨ ℚ.·IdR q ⟩
+      q                                    ∎)
+      (ℚ.<-+o (p ℚ.· [ 1 / 2 ]) (q ℚ.· [ 1 / 2 ]) (q ℚ.· [ 1 / 2 ])
+        ((ℚ.<-·o p q [ 1 / 2 ] (ℚ.0<pos 0 2) p<q)))
+  in
+    m , ∣ (p , m) , u≤p , p<m , ≤ᵣ-refl _ ∣₁ , ∣ (m , q) , ≤ᵣ-refl _ , m<q , q≤v ∣₁
 
 
 
@@ -717,7 +737,7 @@ opaque
  w : Elimℝ-Prop (λ z → 0 ≤ᵣ absᵣ z)
  w .Elimℝ-Prop.ratA q = isTrans≤≡ᵣ _ _ _ (≤ℚ→≤ᵣ 0 (ℚ.abs' q)
    (subst (0 ℚ.≤_) (ℚ.abs'≡abs q) (ℚ.0≤abs q))) (sym (absᵣ-rat' _))
- w .Elimℝ-Prop.limA x p x₁ = 
+ w .Elimℝ-Prop.limA x p x₁ =
   let
 
       zz : _ ≡ _
@@ -726,12 +746,12 @@ opaque
                λ q → sym (≤ᵣ→≡ (x₁ q)) ∙ maxᵣ-impl _ _
               )
 
-      
+
   in ≡→≤ᵣ ((cong₂ maxᵣ refl (absᵣ-lim' _ _) ∙ maxᵣ-impl _ _)
        ∙ (snd (NonExpanding₂.β-rat-lim' {ℚ.max} maxR 0 (λ q → (absᵣ (x q)))
           λ _ _ → absᵣ-nonExpanding  _ _ _ (p _ _))
          ∙ zz) ∙ sym (absᵣ-lim' _ _))
-  
+
 
  w .Elimℝ-Prop.isPropA _ = isProp≤ᵣ _ _
 

Cubical/Tactics/CommRingSolver/FastRationalsReflection.agda

@@ -92,6 +92,23 @@ private
         variableList (t ∷ ts)
           = varg (con (quote _∷vec_) (t v∷ (variableList ts) ∷ []))
 
+  normaliserCallAsTerm : Term → Arg Term → Term → Term
+  normaliserCallAsTerm R varList lhs =
+    def
+       (quote normaliseRing)
+       (R v∷ lhs v∷ varList ∷ [])
+
+
+  normaliserCallWithVars : ℕ → Vars → Term → Term → Term
+  normaliserCallWithVars n vars R lhs =
+      normaliserCallAsTerm R (variableList vars) lhs
+      where
+        variableList : Vars → Arg Term
+        variableList [] = varg (con (quote emptyVec) [])
+        variableList (t ∷ ts)
+          = varg (con (quote _∷vec_) (t v∷ (variableList ts) ∷ []))
+
+
 module pr (R : CommRing ℓ) {n : ℕ} where
   open CommRingStr (snd R)
 
@@ -221,6 +238,16 @@ module CommRingReflection (cring : Term) (names : RingNames) where
             ass n = indexOf n vars
         in (fst r1 ass , fst r2 ass , vars ))
 
+  toAlgebraExpressionLHS : Term → TC (Term × Vars)
+  toAlgebraExpressionLHS lhs = do
+      (e , vars) ← buildExpression lhs
+
+      returnTC (
+        let ass : VarAss
+            ass n = indexOf n vars
+        in (e ass , vars ))
+
+
 private
   checkIsRing : Term → TC Term
   checkIsRing ring = checkType ring (def (quote CommRing) (unknown v∷ []))
@@ -244,6 +271,32 @@ private
       let solution = solverCallWithVars (length vars) vars commRing lhs' rhs'
       unify hole solution
 
+  normalise!-macro : Term → TC Unit
+  normalise!-macro hole =
+      withReduceDefs
+          (false , ((quote ℚ._+_) ∷ (quote (ℚ.-_)) ∷ (quote ℚ._·_) ∷ []))
+    do
+      commRing ← checkIsRing (def (quote ℚCommRing) [])
+      goal ← inferType hole >>= normalise
+      names ← findRingNames commRing
+
+      -- wait-for-type goal
+      just (lhs , rhs) ← get-boundary goal
+        where
+          nothing
+            → typeError(strErr "The CommRingSolver failed to parse the goal "
+                               ∷ termErr goal ∷ [])
+
+      (lhs' , vars) ← CommRingReflection.toAlgebraExpressionLHS commRing names lhs
+
+      let solution = normaliserCallWithVars (length vars) vars commRing lhs'
+
+      unify hole solution
+
 macro
   ℚ! : Term → TC _
   ℚ! = solve!-macro
+
+
+  ℚ↓ : Term → TC _
+  ℚ↓ = normalise!-macro