diff options
Diffstat (limited to 'BFFPlug.agda')
| -rw-r--r-- | BFFPlug.agda | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/BFFPlug.agda b/BFFPlug.agda index 0d69723..4992a3e 100644 --- a/BFFPlug.agda +++ b/BFFPlug.agda @@ -8,7 +8,7 @@ open import Data.Maybe using (Maybe ; just ; nothing) open import Data.Vec using (Vec) open import Data.Product using (∃ ; _,_) open import Relation.Binary using (module DecSetoid) -open import Relation.Binary.PropositionalEquality using (refl ; cong ; subst ; sym ; module ≡-Reasoning) renaming (setoid to PropEq) +open import Relation.Binary.PropositionalEquality as P using (module ≡-Reasoning) open import Relation.Nullary using (yes ; no) open import Function using (flip ; id ; _∘_) open import Function.LeftInverse using (_RightInverseOf_) @@ -32,39 +32,39 @@ bffplug G sput {i} {m} s v with sput i m ... | nothing = nothing ... | just j with Get.gl₂ G j ≟ m ... | no gl₂j≢m = nothing -bffplug G sput {i} s v | just j | yes refl with bff G j s v -... | nothing = nothing -... | just s′ = just (j , s′) +bffplug G sput {i} s v | just j | yes P.refl with bff G j s v +... | nothing = nothing +... | just s′ = just (j , s′) _SimpleRightInvOf_ : {A B : Set} → (A → B) → (B → A) → Set f SimpleRightInvOf g = ≡-to-Π f RightInverseOf ≡-to-Π g bffinv : (G : Get) → (nelteg : ℕ → Get.I G) → nelteg SimpleRightInvOf Get.gl₂ G → {i : Get.I G} → {m : ℕ} → Vec Carrier (Get.gl₁ G i) → Vec Carrier m → Maybe (Vec (Maybe Carrier) (Get.gl₁ G (nelteg m))) -bffinv G nelteg inv {m = m} s v = bff G (nelteg m) s (subst (Vec Carrier) (sym (inv m)) v) +bffinv G nelteg inv {m = m} s v = bff G (nelteg m) s (P.subst (Vec Carrier) (P.sym (inv m)) v) module InvExamples where open Examples using (reverse' ; drop' ; sieve' ; tail' ; take') reverse-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier m) - reverse-put s v = bffinv reverse' id (λ _ → refl) s v >>= sequenceV + reverse-put s v = bffinv reverse' id (λ _ → P.refl) s v >>= sequenceV drop-put : (k : ℕ) → {n m : ℕ} → Vec Carrier (k + n) → Vec Carrier m → Maybe (Vec (Maybe Carrier) (k + m)) - drop-put k = bffinv (drop' k) id (λ _ → refl) + drop-put k = bffinv (drop' k) id (λ _ → P.refl) double : ℕ → ℕ double zero = zero double (suc n) = suc (suc (double n)) sieve-inv-len : double SimpleRightInvOf ⌈_/2⌉ - sieve-inv-len zero = refl - sieve-inv-len (suc zero) = refl - sieve-inv-len (suc (suc x)) = cong (suc ∘ suc) (sieve-inv-len x) + sieve-inv-len zero = P.refl + sieve-inv-len (suc zero) = P.refl + sieve-inv-len (suc (suc x)) = P.cong (suc ∘ suc) (sieve-inv-len x) sieve-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec (Maybe Carrier) (double m)) sieve-put = bffinv sieve' double sieve-inv-len tail-put : {n m : ℕ} → Vec Carrier (suc n) → Vec Carrier m → Maybe (Vec (Maybe Carrier) (suc m)) - tail-put = bffinv tail' id (λ _ → refl) + tail-put = bffinv tail' id (λ _ → P.refl) take-put : (k : ℕ) → {n : ℕ} → Vec Carrier (k + n) → Vec Carrier k → Maybe (Vec Carrier (k + n)) take-put k = bffsameshape (take' k) |