Clear up vector reindexing
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
f7ac22257e
commit
520b2b514c
|
@ -14,7 +14,7 @@ open import Data.List.Membership.Propositional as MemProp using () renaming (_
|
||||||
open import Data.List.Relation.Unary.All using (All; []; _∷_)
|
open import Data.List.Relation.Unary.All using (All; []; _∷_)
|
||||||
open import Data.List.Relation.Unary.Any as RelAny using ()
|
open import Data.List.Relation.Unary.Any as RelAny using ()
|
||||||
open import Data.List.Relation.Unary.Any.Properties using (++⁺ʳ)
|
open import Data.List.Relation.Unary.Any.Properties using (++⁺ʳ)
|
||||||
open import Data.Fin using (Fin; suc; zero; fromℕ; inject₁; inject≤; _↑ʳ_; _↑ˡ_) renaming (_≟_ to _≟ᶠ_)
|
open import Data.Fin using (Fin; suc; zero; fromℕ; inject₁; inject≤; _↑ʳ_; _↑ˡ_) renaming (_≟_ to _≟ᶠ_; cast to castᶠ)
|
||||||
open import Data.Fin.Properties using (suc-injective)
|
open import Data.Fin.Properties using (suc-injective)
|
||||||
open import Relation.Binary.PropositionalEquality as Eq using (subst; cong; _≡_; sym; trans; refl)
|
open import Relation.Binary.PropositionalEquality as Eq using (subst; cong; _≡_; sym; trans; refl)
|
||||||
open import Relation.Nullary using (¬_)
|
open import Relation.Nullary using (¬_)
|
||||||
|
@ -121,6 +121,13 @@ module Graphs where
|
||||||
e ∈ˡ (Graph.edges g₁) →
|
e ∈ˡ (Graph.edges g₁) →
|
||||||
(↑ˡ-Edge e n) ∈ˡ (subst (λ m → List (Fin m × Fin m)) sg₂≡sg₁+n (Graph.edges g₂))
|
(↑ˡ-Edge e n) ∈ˡ (subst (λ m → List (Fin m × Fin m)) sg₂≡sg₁+n (Graph.edges g₂))
|
||||||
|
|
||||||
|
flatten-casts : ∀ {s₁ s₂ s₃ n₁ n₂ : ℕ}
|
||||||
|
(p : s₂ +ⁿ n₂ ≡ s₃) (q : s₁ +ⁿ n₁ ≡ s₂) (r : s₁ +ⁿ (n₁ +ⁿ n₂) ≡ s₃)
|
||||||
|
(idx : Fin s₁) →
|
||||||
|
castᶠ p ((castᶠ q (idx ↑ˡ n₁)) ↑ˡ n₂) ≡ castᶠ r (idx ↑ˡ (n₁ +ⁿ n₂))
|
||||||
|
flatten-casts refl refl r zero = refl
|
||||||
|
flatten-casts {(suc s₁)} {s₂} {s₃} {n₁} {n₂} refl refl r (suc idx')
|
||||||
|
rewrite flatten-casts refl refl (sym (+-assoc s₁ n₁ n₂)) idx' = refl
|
||||||
|
|
||||||
⊆-trans : ∀ {g₁ g₂ g₃ : Graph} → g₁ ⊆ g₂ → g₂ ⊆ g₃ → g₁ ⊆ g₃
|
⊆-trans : ∀ {g₁ g₂ g₃ : Graph} → g₁ ⊆ g₂ → g₂ ⊆ g₃ → g₁ ⊆ g₃
|
||||||
⊆-trans {MkGraph s₁ ns₁ es₁} {MkGraph s₂ ns₂ es₂} {MkGraph s₃ ns₃ es₃}
|
⊆-trans {MkGraph s₁ ns₁ es₁} {MkGraph s₂ ns₂ es₂} {MkGraph s₃ ns₃ es₃}
|
||||||
|
@ -139,7 +146,9 @@ module Graphs where
|
||||||
|
|
||||||
-- lookup (cast p₂ ns₃) ((Fin.cast (sym p₁) (idx ↑ˡ n₁) ↑ˡ n₂)) ≡ lookup ns₃ (Fin.cast (sym p₂) ((Fin.cast (sym p₁) (idx ↑ˡ n₁) ↑ˡ n₂))) -- by lookup-cast₂
|
-- lookup (cast p₂ ns₃) ((Fin.cast (sym p₁) (idx ↑ˡ n₁) ↑ˡ n₂)) ≡ lookup ns₃ (Fin.cast (sym p₂) ((Fin.cast (sym p₁) (idx ↑ˡ n₁) ↑ˡ n₂))) -- by lookup-cast₂
|
||||||
|
|
||||||
-- -- ??
|
-- lookup ns₃ (Fin.cast (sym p₂) ((Fin.cast (sym p₁) (idx ↑ˡ n₁) ↑ˡ n₂))) ≡ lookup ns₃ (Fin.cast (sym (+-assoc s₁ n₁ n₂)) (idx ↑ˡ (n₁ + n₂))) -- by flatten-casts
|
||||||
|
--
|
||||||
|
-- lookup ns₃ (Fin.cast (sym (+-assoc s₁ n₁ n₂)) (idx ↑ˡ (n₁ + n₂))) ≡ lookup (cast (+-assoc s₁ n₁ n₂) ns₃) (idx ↑ˡ (n₁ + n₂)) ∎
|
||||||
}
|
}
|
||||||
|
|
||||||
record Relaxable (T : Graph → Set) : Set where
|
record Relaxable (T : Graph → Set) : Set where
|
||||||
|
|
Loading…
Reference in New Issue
Block a user