maybe

src/Derivative.agda

@@ -0,0 +1,55 @@
+{-# OPTIONS --guardedness #-}
+
+module Derivative where
+
+open import GeneralizedPolynomial
+  using (Polynomial; 𝟘; 𝟙; wkᵢ)
+
+open import Data.Nat
+  using (ℕ; _≟_; _≥_; suc; _≥?_; s≤s; z≤n; pred; _∸_; _+_)
+open import Data.Nat.Properties using (≤-reflexive; ≤-step; n≤1+n)
+open import Data.Unit using (⊤)
+open import Data.Empty using (⊥)
+
+
+open import Relation.Binary.PropositionalEquality
+  using (refl)
+open import Relation.Nullary using (yes; no)
+open import Relation.Nullary.Decidable
+  using (toWitness; fromWitness; True)
+
+open Polynomial
+open GeneralizedPolynomial.LeastFixpoint
+open GeneralizedPolynomial.GreatestFixpoint
+
+mutual
+
+  derivative : {n : ℕ} → (m : ℕ) → Polynomial n → Polynomial n
+  derivative {n} m       (I k)     with k ≟ m
+  ...                              | yes refl = wkᵢ 𝟙 z≤n
+  ...                              | no  k≢m  = wkᵢ 𝟘 z≤n
+  derivative {n} m       (K x)                = 𝟘
+  derivative {n} m       (μ P)                = μ (wkᵢ (derivative (suc m) P [ μ P ]) (n≤1+n _)
+                                              ⊕ᵣ   wkᵢ (derivative 0       P [ μ P ]) (n≤1+n _)
+                                              ⊗ᵣ   wkᵢ (I 0)                          (s≤s z≤n))
+  derivative {n} m       (ν P)                = ν (wkᵢ (derivative (suc m) P [ ν P ]) (n≤1+n _)
+                                              ⊕ᵣ   wkᵢ (derivative 0       P [ ν P ]) (n≤1+n _)
+                                              ⊗ᵣ   wkᵢ (I 0)                          (s≤s z≤n))
+  derivative {n} 0       (wkᵣ P)              = wkᵢ 𝟘 z≤n
+  derivative {n} (suc m) (wkᵣ P)              = wkᵣ (derivative m P)
+  derivative {n} m       (L ⊕ᵣ R)             = derivative m L ⊕ᵣ derivative m R
+  derivative {n} m       (L ⊗ᵣ R)             = (derivative m L ⊗ᵣ R) ⊕ᵣ (L ⊕ᵣ derivative m R)
+  derivative {n} m       (F [ G ])            =  derivative (suc m) F [ G ]
+                                              ⊕ᵣ derivative 0       F [ G ]
+                                              ⊗ᵣ derivative m       G
+
+infixl 10 ∂_
+infixl 10 ∂_∙_
+
+∂_ : {n : ℕ} → Polynomial n → Polynomial n
+∂ P = derivative 1 P
+
+∂_∙_ : {n : ℕ} → (m : ℕ) → {True (n ≥? m)} → Polynomial n → Polynomial n
+∂_∙_ m {m≤n} P = derivative m P
+
+

src/GeneralizedPolynomial.agda

@@ -1,19 +1,21 @@
-{-# OPTIONS --guardedness --no-positivity-check #-}
+{-# OPTIONS --guardedness --allow-unsolved-metas #-}
 
 module GeneralizedPolynomial where
 
-open import Data.Empty using (⊥-elim)
+open import Data.Empty using (⊥-elim; ⊥)
+open import Data.Unit using (⊤)
 open import Data.Sum using (_⊎_)
-open import Data.Product using (_×_; ∃-syntax; _,_)
+open import Data.Product
+  using (_×_; ∃-syntax; _,_; proj₁; proj₂)
 open import Data.Nat
   using (ℕ; suc; _<_; _≤_; _⊔_; s≤s; z≤n; _≟_; _≤?_; _<?_;
-        pred; _∸_)
+        pred; _∸_; _+_)
 open import Data.Nat.Properties
   using (≤-reflexive; ≤-trans; ≤-step; n≤1+n; ≤∧≢⇒<; ≤-pred;
-        ≮⇒≥)
+        ≮⇒≥; m≤m⊔n; m≤n⊔m; m<n⇒m≤1+n)
 open import Data.Nat.Induction using (<-rec)
 
-open import Relation.Nullary using (yes; no)
+open import Relation.Nullary using (yes; no; ¬_)
 open import Relation.Nullary.Decidable
   using (True; toWitness; fromWitness)
 open import Relation.Nullary.Negation
@@ -22,24 +24,23 @@ open import Relation.Nullary.Negation
 open import Relation.Binary.PropositionalEquality
     using (refl; ≢-sym; _≡_)
 
-private module ℕExtra where
-  n≤n⊔m : {n m : ℕ} → n ≤ n ⊔ m
-  n≤n⊔m {0}     {m}     = z≤n
-  n≤n⊔m {suc n} {0}     = ≤-reflexive refl
-  n≤n⊔m {suc n} {suc m} = s≤s n≤n⊔m
-
-  m≤n⊔m : {n m : ℕ} → m ≤ n ⊔ m
-  m≤n⊔m {0}     {m}     = ≤-reflexive refl
-  m≤n⊔m {suc n} {0}     = z≤n
-  m≤n⊔m {suc n} {suc m} = s≤s m≤n⊔m
-open ℕExtra
-
 infixl 6 _⊕ᵣ_
 infixl 7 _⊗ᵣ_
 infixl 6 _⊕_
 infixl 7 _⊗_
 infixr 8 μ_
 infixr 8 ν_
+infixr 8 wk_
+infixl 8 _[_]
+
+private module ℕextra where
+  m≤n⇒m≤1+n : ∀ {m n} → m ≤ n → m ≤ 1 + n
+  m≤n⇒m≤1+n z≤n       = z≤n
+  m≤n⇒m≤1+n (s≤s m≤n) = s≤s (m≤n⇒m≤1+n m≤n)
+
+  postulate lemma : (n m : ℕ) → (n ≤ suc m) → ¬ (n ≡ suc m) → n ≤ m
+
+open ℕextra
 
 data Polynomial : ℕ → Set₁ where
     I_   : (n : ℕ) → Polynomial (suc n)
@@ -50,99 +51,74 @@ data Polynomial : ℕ → Set₁ where
     -- Shouldn't be used explicitly by users of the lib
     _⊕ᵣ_ : {n : ℕ} → Polynomial n → Polynomial n → Polynomial n
     _⊗ᵣ_ : {n : ℕ} → Polynomial n → Polynomial n → Polynomial n
-    wk_  : {n m : ℕ} → Polynomial n → {True (n ≤? m)} → Polynomial m
+    wkᵣ_  : {n : ℕ} → Polynomial n → Polynomial (suc n)
+    _[_]  : {n : ℕ} → Polynomial (suc n) → Polynomial n → Polynomial n
 
 -- Versions that infer weakening
+wkᵢ : {n m : ℕ} → Polynomial n → (n ≤ m) → Polynomial m
+wkᵢ {0}     {0}     P n≤m = P
+wkᵢ {n}     {suc m} P n≤m with n ≟ suc m
+... | yes refl = P
+... | no n≢m   = wkᵣ (wkᵢ {n} {m} P (lemma n m n≤m n≢m))
+
+wk_ : {n m : ℕ} → Polynomial n → {True (n ≤? m)} → Polynomial m
+wk_ P {n≤m} = wkᵢ P (toWitness n≤m)
+
 _⊗_ : {n m : ℕ} → Polynomial n → Polynomial m → Polynomial (n ⊔ m)
-L ⊗ R = (wk_ L {fromWitness n≤n⊔m}) ⊗ᵣ (wk_ R {fromWitness m≤n⊔m})
+L ⊗ R = (wkᵢ L (m≤m⊔n _ _)) ⊗ᵣ (wkᵢ R (m≤n⊔m _ _))
 
 _⊕_ : {n m : ℕ} → Polynomial n → Polynomial m → Polynomial (n ⊔ m)
-L ⊕ R = (wk_ L {fromWitness n≤n⊔m}) ⊕ᵣ (wk_ R {fromWitness m≤n⊔m})
+L ⊕ R = (wkᵢ L (m≤m⊔n _ _)) ⊕ᵣ (wkᵢ R (m≤n⊔m _ _))
 
+
+𝟘 : Polynomial 0
+𝟘 = K ⊥
+
+𝟙 : Polynomial 0
+𝟙 = K ⊤
+
+infixl 3 _,⟨_⟩_
 data Context : ℕ → Set₁ where
   ∅      : Context 0
-  _,_ : {n m : ℕ} → Context n → {True (m ≤? n)} → Polynomial m → Context (suc n)
-
--- I i means to lookup the i-th position in the context from the context
--- ∅ , a , b , c , d
---     3   2   1   0
-lookup : {n : ℕ} → Context n → (m : ℕ) → {m < n} → ∃[ p ] Polynomial p × p < n
-lookup (_,_ ctx {m≤n} X) 0       {p}     = _ , X , s≤s (toWitness m≤n)
-lookup (ctx , _) (suc m) {s≤s p} with lookup ctx m {p}
-... | p , X , p<n = p , X , ≤-step p<n
-
--- ∅ , a , b , c , d (4)
--- wk to 2
--- ∅ , a , b
--- A = I 0 ⊕ I 1
--- B = I 0
--- A ⊗ B
-weaken-context : ∀ {n m : ℕ} → (m ≤ n) → Context n → Context m
-weaken-context {0}     {0} z≤z ∅ = ∅
-weaken-context {suc n} {m} m≤n ctx@(rest , _) with suc n ≟ m
-... | yes refl = ctx
-... | no  n≢m  = weaken-context (≤-pred (≤∧≢⇒< m≤n (≢-sym n≢m))) rest
+  _,⟨_⟩_ : {n m : ℕ} → Context n → (m ≤ n) → Polynomial m → Context (suc n)
+
+infixl 3 _∙_
+_∙_ : {n m : ℕ} → Context n → {True (m ≤? n)} → Polynomial m → Context (suc n)
+_∙_ ctx {m≤n} P = ctx ,⟨ toWitness m≤n ⟩ P
+
+lookup : {n : ℕ} → Context n → (m : ℕ) → (m < n) → ∃[ p ] Polynomial p × p < n
+lookup (ctx ,⟨ m≤n ⟩ X) 0       p                     = _ , X , s≤s m≤n
+lookup (ctx ,⟨ _   ⟩ _) (suc m) (s≤s p) with lookup ctx m p
+...                                     | p , X , p<n = p , X , ≤-step p<n
 
 mutual
-  eval-impl : _
-  eval-impl 0       rec (K x)           ctx = x
-  eval-impl (suc n) rec (I m)           ctx with lookup ctx m {≤-reflexive refl}
-  ... | p , X , p<n                         = rec p p<n X
-                                                  (weaken-context (≤-trans (≤-pred p<n)
-                                                                  (n≤1+n _)) ctx)
-  eval-impl n rec (wk_ {f} {m} P {f≤m}) ctx with f ≟ m
-  ... | yes refl                            = eval-impl _ rec P ctx
-  ... | no  f≢m                             = rec f (≤∧≢⇒< (toWitness f≤m) f≢m) P
-                                                           (weaken-context (toWitness f≤m) ctx)
-  eval-impl n rec (μ P)                 ctx = LeastFixpoint P ctx
-  eval-impl n rec (ν P)                 ctx = GreatestFixpoint P ctx
-  eval-impl n rec (L ⊕ᵣ R)              ctx = eval-impl _ rec L ctx ⊎ eval-impl _ rec R ctx
-  eval-impl n rec (L ⊗ᵣ R)              ctx = eval-impl _ rec L ctx × eval-impl _ rec R ctx
-
-  lemmaₙ : {n : ℕ} → True (n ≤? n)
-  lemmaₙ {n} = fromWitness (≤-reflexive refl)
-
-  data LeastFixpoint {n : ℕ} (P : Polynomial (suc n)) (ctx : Context n) : Set where
-    μ⟨_⟩ : eval P (_,_ ctx {lemmaₙ} (μ P)) → LeastFixpoint P ctx
-
-  record GreatestFixpoint {n : ℕ} (P : Polynomial (suc n)) (ctx : Context n) : Set where
+  {-# TERMINATING #-}
+  eval : {n m : ℕ} → (n ≤ m) → Polynomial n → Context m → Set
+  eval m≤n (I k)     ctx with lookup ctx k m≤n
+  ...                    | p , X , s≤s p<n = eval (≤-step p<n) X ctx
+  eval n≤m (K x)     ctx                   = x
+  eval n≤m (L ⊗ᵣ R)  ctx                   = eval n≤m L ctx × eval n≤m R ctx
+  eval n≤m (L ⊕ᵣ R)  ctx                   = eval n≤m L ctx ⊎ eval n≤m R ctx
+  eval n≤m (μ P)     ctx                   = LeastFixpoint n≤m P ctx
+  eval n≤m (ν P)     ctx                   = GreatestFixpoint n≤m P ctx
+  eval n≤m (wkᵣ P)   ctx                   = eval (≤-pred (m≤n⇒m≤1+n n≤m)) P ctx
+  eval n≤m (F [ G ]) ctx                   = eval (s≤s n≤m) F (ctx ,⟨ n≤m ⟩ G)
+
+  data LeastFixpoint {n m : ℕ}
+    (n≤m : n ≤ m) (P : Polynomial (suc n)) (ctx : Context m) : Set where
+    μ⟨_⟩ : eval (s≤s n≤m) P (ctx ,⟨ n≤m ⟩ μ P) → LeastFixpoint n≤m P ctx
+
+  record GreatestFixpoint {n m : ℕ}
+    (n≤m : n ≤ m) (P : Polynomial (suc n)) (ctx : Context m) : Set where
     coinductive
-    field rest : eval P (_,_ ctx {lemmaₙ} (ν P))
-
-
-  eval : {n : ℕ} → Polynomial n → Context n → Set
-  eval {n} = <-rec _ eval-impl n
-
-_[_/_] : {n g : ℕ} → Polynomial (suc n) → (i : ℕ) → {True (i ≤? n)} → Polynomial g → {True (g ≤? i)} → Polynomial n
-_[_/_] {n} (I m)                 i {i<n} G {g≤n}                      with i ≟ m | i <? m
-...                                        | yes i≡m  | i<?m          = wk_ G {fromWitness (≤-trans (toWitness g≤n)
-                                                                                                      (toWitness i<n))}
-_[_/_] {n} ((I suc m) )          i {i<n} G | no  i≢m  | yes i<m       = I m
-...                                        | no  i≢m  | no  i≮m       = contradiction (≤∧≢⇒< (toWitness i<n) i≢m) i≮m
-_[_/_] (μ P)                     i {i<n} G {g≤n}                      = μ (_[_/_] P (suc i) {fromWitness (s≤s (toWitness i<n))}
-                                                                                                           G {fromWitness (≤-step (toWitness g≤n))})
-_[_/_] (ν P)                     i {i<n} G {g≤n}                      = ν (_[_/_] P (suc i) {fromWitness (s≤s (toWitness i<n))}
-                                                                                                           G {fromWitness (≤-step (toWitness g≤n))})
-_[_/_] (L ⊕ᵣ R)                  i {i<n} G {g≤n}                      = (_[_/_] L i {i<n} G {g≤n}) ⊕ᵣ (_[_/_] R i {i<n} G {g≤n})
-_[_/_] (L ⊗ᵣ R)                  i {i<n} G {g≤n}                      = (_[_/_] L i {i<n} G {g≤n}) ⊗ᵣ (_[_/_] R i {i<n} G {g≤n})
-_[_/_] (wk_ {m}     {n} P {m≤n}) i {i<n} G {g≤n}                      with i <? m
-_[_/_] (wk_ {0}     {n} P {m≤n}) i {i<n} G {g≤n} | yes i<m            = wk_ P
-_[_/_] (wk_ {suc m} {n} P {m≤n}) i {i<n} G {g≤n} | yes i<m            = wk_ (_[_/_] P i {fromWitness (≤-pred i<m)}
-                                                                                        G {g≤n})
-                                                                              {fromWitness (≤-pred (toWitness m≤n))}
-...                                              | no  i≮m            = wk_ P {fromWitness (≤-trans (≮⇒≥ i≮m) (toWitness i<n ))}
-
--- g ≤ n₁        (g≤n)
--- suc suc i ≤ m (i<m)
--- suc i ≤ n     (i<n)
--- m ≤ n₁        (m<n)
+    field rest : eval (s≤s n≤m) P (ctx ,⟨ n≤m ⟩ ν P)
+
 
 ⟦_⟧ : {n m : ℕ} → {n≤m : True (n ≤? m)} → Polynomial n → Context m → Set
-⟦_⟧ {_} {_} {n≤m} F ctx = eval F (weaken-context (toWitness n≤m) ctx)
+⟦_⟧ {_} {_} {n≤m} F ctx = eval (toWitness n≤m) F ctx
 
 ⟦_⟧₁ : Polynomial 1 → Set → Set
-⟦ P ⟧₁ X = ⟦ P ⟧ (∅ , K X)
+⟦ P ⟧₁ X = ⟦ P ⟧ (∅ ∙ K X)
 
 ⟦_⟧₀ : Polynomial 0 → Set
 ⟦ P ⟧₀ = ⟦ P ⟧ ∅
-