{-# OPTIONS --cubical-compatible --safe #-}
open import Equality
module Nat.Solver
{reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where
open Derived-definitions-and-properties eq
import Equality.Propositional as EP
open import Equality.Instances-related
open import Prelude
open import Bijection eq using (_↔_)
open import Function-universe eq
open import Data.Nat.Solver
open import Data.Vec as Vec
open import Data.Vec.N-ary
open import Function.Bundles using (Equivalence)
import Relation.Binary.Reflection
import Relation.Binary.PropositionalEquality as P
open +-*-Solver public using (_:=_; _:+_; _:*_; _:^_)
open +-*-Solver.Polynomial public using (con)
open +-*-Solver hiding (solve)
open Relation.Binary.Reflection (P.setoid _) var ⟦_⟧ ⟦_⟧↓ correct
using (close)
private
≡↔≡ : ∀ {a} {A : Type a} {x y : A} → x ≡ y ↔ x P.≡ y
≡↔≡ = proj₁ (all-equality-types-isomorphic eq EP.equality-with-J)
≡→≡ : ∀ {a} {A : Type a} {x y : A} → x ≡ y → x P.≡ y
≡→≡ = _↔_.to ≡↔≡
≡←≡ : ∀ {a} {A : Type a} {x y : A} → x P.≡ y → x ≡ y
≡←≡ = _↔_.from ≡↔≡
solve :
∀ n (f : N-ary n (Polynomial n)
(Polynomial n × Polynomial n)) →
Eqʰ n _≡_ (curryⁿ ⟦ proj₁ (close n f) ⟧↓)
(curryⁿ ⟦ proj₂ (close n f) ⟧↓) →
Eq n _≡_ (curryⁿ ⟦ proj₁ (close n f) ⟧)
(curryⁿ ⟦ proj₂ (close n f) ⟧)
solve n f =
Eqʰ n _≡_ (curryⁿ ⟦ proj₁ (close n f) ⟧↓)
(curryⁿ ⟦ proj₂ (close n f) ⟧↓) ↝⟨ Eqʰ-to-Eq n _≡_ ⟩
Eq n _≡_ (curryⁿ ⟦ proj₁ (close n f) ⟧↓)
(curryⁿ ⟦ proj₂ (close n f) ⟧↓) ↔⟨⟩
∀ⁿ n (curryⁿ λ xs → (curryⁿ ⟦ proj₁ (close n f) ⟧↓ $ⁿ xs) ≡
(curryⁿ ⟦ proj₂ (close n f) ⟧↓ $ⁿ xs)) ↝⟨ Equivalence.to (uncurry-∀ⁿ n) ⟩
(∀ (xs : Vec _ n) →
(curryⁿ λ xs → (curryⁿ ⟦ proj₁ (close n f) ⟧↓ $ⁿ xs) ≡
(curryⁿ ⟦ proj₂ (close n f) ⟧↓ $ⁿ xs)) $ⁿ xs) ↝⟨ (∀-cong _ λ xs → ≡⇒↝ _ $ ≡←≡ $ left-inverse _ xs) ⟩
(∀ (xs : Vec _ n) →
(curryⁿ ⟦ proj₁ (close n f) ⟧↓ $ⁿ xs) ≡
(curryⁿ ⟦ proj₂ (close n f) ⟧↓ $ⁿ xs)) ↝⟨ (∀-cong _ λ _ → ≡→≡) ⟩
(∀ (xs : Vec _ n) →
(curryⁿ ⟦ proj₁ (close n f) ⟧↓ $ⁿ xs) P.≡
(curryⁿ ⟦ proj₂ (close n f) ⟧↓ $ⁿ xs)) ↝⟨ (∀-cong _ λ xs → ≡⇒↝ _ $ sym $ ≡←≡ $ left-inverse _ xs) ⟩
(∀ (xs : Vec _ n) →
(curryⁿ λ xs → (curryⁿ ⟦ proj₁ (close n f) ⟧↓ $ⁿ xs) P.≡
(curryⁿ ⟦ proj₂ (close n f) ⟧↓ $ⁿ xs)) $ⁿ xs) ↝⟨ Equivalence.from (uncurry-∀ⁿ n) ⟩
∀ⁿ n (curryⁿ λ xs → (curryⁿ ⟦ proj₁ (close n f) ⟧↓ $ⁿ xs) P.≡
(curryⁿ ⟦ proj₂ (close n f) ⟧↓ $ⁿ xs)) ↔⟨⟩
Eq n P._≡_ (curryⁿ ⟦ proj₁ (close n f) ⟧↓)
(curryⁿ ⟦ proj₂ (close n f) ⟧↓) ↝⟨ Eq-to-Eqʰ n P._≡_ ⟩
Eqʰ n P._≡_ (curryⁿ ⟦ proj₁ (close n f) ⟧↓)
(curryⁿ ⟦ proj₂ (close n f) ⟧↓) ↝⟨ +-*-Solver.solve n f ⟩
Eq n P._≡_ (curryⁿ ⟦ proj₁ (close n f) ⟧)
(curryⁿ ⟦ proj₂ (close n f) ⟧) ↔⟨⟩
∀ⁿ n (curryⁿ λ xs → (curryⁿ ⟦ proj₁ (close n f) ⟧ $ⁿ xs) P.≡
(curryⁿ ⟦ proj₂ (close n f) ⟧ $ⁿ xs)) ↝⟨ Equivalence.to (uncurry-∀ⁿ n) ⟩
(∀ (xs : Vec _ n) →
(curryⁿ λ xs → (curryⁿ ⟦ proj₁ (close n f) ⟧ $ⁿ xs) P.≡
(curryⁿ ⟦ proj₂ (close n f) ⟧ $ⁿ xs)) $ⁿ xs) ↝⟨ (∀-cong _ λ xs → ≡⇒↝ _ $ ≡←≡ $ left-inverse _ xs) ⟩
(∀ (xs : Vec _ n) →
(curryⁿ ⟦ proj₁ (close n f) ⟧ $ⁿ xs) P.≡
(curryⁿ ⟦ proj₂ (close n f) ⟧ $ⁿ xs)) ↝⟨ (∀-cong _ λ _ → ≡←≡) ⟩
(∀ (xs : Vec _ n) →
(curryⁿ ⟦ proj₁ (close n f) ⟧ $ⁿ xs) ≡
(curryⁿ ⟦ proj₂ (close n f) ⟧ $ⁿ xs)) ↝⟨ (∀-cong _ λ xs → ≡⇒↝ _ $ sym $ ≡←≡ $ left-inverse _ xs) ⟩
(∀ (xs : Vec _ n) →
(curryⁿ λ xs → (curryⁿ ⟦ proj₁ (close n f) ⟧ $ⁿ xs) ≡
(curryⁿ ⟦ proj₂ (close n f) ⟧ $ⁿ xs)) $ⁿ xs) ↝⟨ Equivalence.from (uncurry-∀ⁿ n) ⟩
∀ⁿ n (curryⁿ λ xs → (curryⁿ ⟦ proj₁ (close n f) ⟧ $ⁿ xs) ≡
(curryⁿ ⟦ proj₂ (close n f) ⟧ $ⁿ xs)) ↔⟨⟩
Eq n _≡_ (curryⁿ ⟦ proj₁ (close n f) ⟧)
(curryⁿ ⟦ proj₂ (close n f) ⟧) □