diff options
| -rw-r--r-- | Bidir.agda | 9 | ||||
| -rw-r--r-- | FinMap.agda | 5 | ||||
| -rw-r--r-- | Generic.agda | 47 | ||||
| -rw-r--r-- | LiftGet.agda | 21 |
4 files changed, 51 insertions, 31 deletions
@@ -22,6 +22,7 @@ open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨ import FreeTheorems open FreeTheorems.VecVec using (get-type ; free-theorem) +open import Generic using (just-injective ; map-just-injective) open import FinMap import CheckInsert open CheckInsert Carrier deq @@ -128,14 +129,6 @@ lemma-<$>-just : {A B : Set} {f : A → B} {b : B} {ma : Maybe A} → f <$> ma â lemma-<$>-just {ma = just x} f<$>ma≡just-b = x , refl lemma-<$>-just {ma = nothing} () -∷-injective : {A : Set} {n : â„•} {x y : A} {xs ys : Vec A n} → (x ∷ xs) ≡ (y ∷ ys) → x ≡ y × xs ≡ ys -∷-injective refl = refl , refl - -map-just-injective : {A : Set} {n : â„•} {xs ys : Vec A n} → map Maybe.just xs ≡ map Maybe.just ys → xs ≡ ys -map-just-injective {xs = []} {ys = []} p = refl -map-just-injective {xs = x ∷ xs'} {ys = y ∷ ys'} p with ∷-injective p -map-just-injective {xs = x ∷ xs'} {ys = .x ∷ ys'} p | refl , p' = cong (_∷_ x) (map-just-injective p') - lemma-union-not-used : {m n : â„•} {A : Set} (h : FinMapMaybe n A) → (h' : FinMap n A) → (is : Vec (Fin n) m) → (toList is) in-domain-of h → map just (map (flip lookup (union h h')) is) ≡ map (flip lookupM h) is lemma-union-not-used h h' [] p = refl lemma-union-not-used h h' (i ∷ is') (Data.List.All._∷_ (x , px) p') = congâ‚‚ _∷_ (begin diff --git a/FinMap.agda b/FinMap.agda index a515a2f..46dbd1c 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -15,6 +15,8 @@ open import Relation.Binary.Core using (_≡_ ; refl ; _≢_) open import Relation.Binary.PropositionalEquality using (cong ; sym ; _≗_ ; trans ; congâ‚‚) open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) +open import Generic using (just-injective) + FinMapMaybe : â„• → Set → Set FinMapMaybe n A = Vec (Maybe A) n @@ -77,9 +79,6 @@ lemma-lookupM-insert-other zero (suc j) a (x ∷ xs) p = refl lemma-lookupM-insert-other (suc i) zero a (x ∷ xs) p = refl lemma-lookupM-insert-other (suc i) (suc j) a (x ∷ xs) p = lemma-lookupM-insert-other i j a xs (p ∘ cong suc) -just-injective : {A : Set} → {x y : A} → _≡_ {_} {Maybe A} (just x) (just y) → x ≡ y -just-injective refl = refl - lemma-lookupM-restrict : {A : Set} {n : â„•} → (i : Fin n) → (f : Fin n → A) → (is : List (Fin n)) → (a : A) → lookupM i (restrict f is) ≡ just a → f i ≡ a lemma-lookupM-restrict i f [] a p = lemma-just≢nothing p (lemma-lookupM-empty i) lemma-lookupM-restrict i f (i' ∷ is) a p with i ≟ i' diff --git a/Generic.agda b/Generic.agda new file mode 100644 index 0000000..c7cbc45 --- /dev/null +++ b/Generic.agda @@ -0,0 +1,47 @@ +module Generic where + +open import Data.List using (List ; length ; replicate) renaming ([] to []L ; _∷_ to _∷L_) +open import Data.Maybe using (Maybe ; just) +open import Data.Nat using (â„• ; zero ; suc) +open import Data.Product using (_×_ ; _,_) +open import Data.Vec using (Vec ; toList ; fromList ; map) renaming ([] to []V ; _∷_ to _∷V_) +open import Function using (_∘_) +open import Relation.Binary.Core using (_≡_ ; refl) +open import Relation.Binary.PropositionalEquality using (_≗_ ; cong ; subst ; trans) + +∷-injective : {A : Set} {n : â„•} {x y : A} {xs ys : Vec A n} → + (x ∷V xs) ≡ (y ∷V ys) → x ≡ y × xs ≡ ys +∷-injective refl = refl , refl + +just-injective : {A : Set} → {x y : A} → Maybe.just x ≡ Maybe.just y → x ≡ y +just-injective refl = refl + +length-replicate : {A : Set} {a : A} → (n : â„•) → length (replicate n a) ≡ n +length-replicate zero = refl +length-replicate (suc n) = cong suc (length-replicate n) + +map-just-injective : {A : Set} {n : â„•} {xs ys : Vec A n} → + map Maybe.just xs ≡ map Maybe.just ys → xs ≡ ys +map-just-injective {xs = []V} {ys = []V} p = refl +map-just-injective {xs = x ∷V xs′} {ys = y ∷V ys′} p with ∷-injective p +map-just-injective {xs = x ∷V xs′} {ys = .x ∷V ys′} p | refl , p′ = cong (_∷V_ x) (map-just-injective p′) + +subst-cong : {A : Set} → (T : A → Set) → {g : A → A} → {a b : A} → (f : {c : A} → T c → T (g c)) → (p : a ≡ b) → + f ∘ subst T p ≗ subst T (cong g p) ∘ f +subst-cong T f refl _ = refl + +subst-fromList : {A : Set} {x y : List A} → (p : y ≡ x) → + subst (Vec A) (cong length p) (fromList y) ≡ fromList x +subst-fromList refl = refl + +subst-subst : {A : Set} (T : A → Set) {a b c : A} → (p : a ≡ b) → (p′ : b ≡ c) → (x : T a) → + subst T p′ (subst T p x) ≡ subst T (trans p p′) x +subst-subst T refl p′ x = refl + +toList-fromList : {A : Set} → (l : List A) → toList (fromList l) ≡ l +toList-fromList []L = refl +toList-fromList (x ∷L xs) = cong (_∷L_ x) (toList-fromList xs) + +toList-subst : {A : Set} → {n m : â„•} (v : Vec A n) → (p : n ≡ m) → + toList (subst (Vec A) p v) ≡ toList v +toList-subst v refl = refl diff --git a/LiftGet.agda b/LiftGet.agda index b6d99de..31a632e 100644 --- a/LiftGet.agda +++ b/LiftGet.agda @@ -12,6 +12,7 @@ open import Relation.Binary.PropositionalEquality using (_≗_ ; sym ; cong ; re open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) import FreeTheorems +open import Generic using (length-replicate ; subst-cong ; subst-fromList ; subst-subst ; toList-fromList ; toList-subst) open FreeTheorems.ListList using (get-type ; free-theorem) open FreeTheorems.VecVec using () renaming (get-type to getV-type) @@ -39,13 +40,6 @@ length-toList : {A : Set} {n : â„•} → (v : Vec A n) → length (toList v) ≡ length-toList []V = refl length-toList (x ∷V xs) = cong suc (length-toList xs) -toList-fromList : {A : Set} → (l : List A) → toList (fromList l) ≡ l -toList-fromList [] = refl -toList-fromList (x ∷ xs) = cong (_∷_ x) (toList-fromList xs) - -toList-subst : {A : Set} → {n m : â„•} (v : Vec A n) → (p : n ≡ m) → toList (subst (Vec A) p v) ≡ toList v -toList-subst v refl = refl - getList-to-getVec-length-property : (get : get-type) → {C : Set} → {m : â„•} → (v : Vec C m) → length (get (toList v)) ≡ length (get (replicate m tt)) getList-to-getVec-length-property get {_} {m} v = begin length (get (toList v)) @@ -61,12 +55,6 @@ getList-to-getVec get = getlen , get' get' : {C : Set} {m : â„•} → Vec C m → Vec C (getlen m) get' {C} v = subst (Vec C) (getList-to-getVec-length-property get v) (fromList (get (toList v))) -subst-subst : {A : Set} (T : A → Set) {a b c : A} → (p : a ≡ b) → (p' : b ≡ c) → (x : T a)→ subst T p' (subst T p x) ≡ subst T (trans p p') x -subst-subst T refl p' x = refl - -subst-fromList : {A : Set} {x y : List A} → (p : y ≡ x) → subst (Vec A) (cong length p) (fromList y) ≡ fromList x -subst-fromList refl = refl - get-commut-1 : (get : get-type) {A : Set} → (l : List A) → fromList (get l) ≡ subst (Vec A) (sym (getList-length get l)) (projâ‚‚ (getList-to-getVec get) (fromList l)) get-commut-1 get {A} l = begin fromList (get l) @@ -100,13 +88,6 @@ get-trafo-1 get {B} l = begin vec-len : {A : Set} {n : â„•} → Vec A n → â„• vec-len {_} {n} _ = n -length-replicate : {A : Set} {a : A} → (n : â„•) → length (replicate n a) ≡ n -length-replicate 0 = refl -length-replicate (suc n) = cong suc (length-replicate n) - -subst-cong : {A : Set} → (T : A → Set) → {g : A → A} → {a b : A} → (f : {c : A} → T c → T (g c)) → (p : a ≡ b) → f ∘ subst T p ≗ subst T (cong g p) ∘ f -subst-cong T f refl _ = refl - fromList-toList : {A : Set} {n : â„•} → (v : Vec A n) → fromList (toList v) ≡ subst (Vec A) (sym (length-toList v)) v fromList-toList []V = refl fromList-toList {A} (x ∷V xs) = begin |