diff options
| -rw-r--r-- | Bidir.agda | 13 | ||||
| -rw-r--r-- | CheckInsert.agda | 3 | ||||
| -rw-r--r-- | LiftGet.agda | 114 |
3 files changed, 82 insertions, 48 deletions
@@ -65,11 +65,9 @@ lemma-∉-lookupM-assoc eq i [] [] h ph i∉is = begin lookupM i empty ≡⟨ lemma-lookupM-empty i ⟩ nothing ∎ -lemma-∉-lookupM-assoc eq i (i' ∷ is') (x' ∷ xs') h ph i∉is with i ≟ i' -lemma-∉-lookupM-assoc eq i (i' ∷ is') (x' ∷ xs') h ph i∉is | yes p = contradiction (here p) i∉is -lemma-∉-lookupM-assoc eq i (i' ∷ is') (x' ∷ xs') h ph i∉is | no ¬p with assoc eq is' xs' | inspect (assoc eq is') xs' -lemma-∉-lookupM-assoc eq i (i' ∷ is') (x' ∷ xs') h () i∉is | no ¬p | nothing | Reveal_is_.[_] ph' -lemma-∉-lookupM-assoc eq i (i' ∷ is') (x' ∷ xs') h ph i∉is | no ¬p | just h' | Reveal_is_.[_] ph' = apply-checkInsertProof eq i' x' h' record { +lemma-∉-lookupM-assoc eq i (i' ∷ is') (x' ∷ xs') h ph i∉is with assoc eq is' xs' | inspect (assoc eq is') xs' +lemma-∉-lookupM-assoc eq i (i' ∷ is') (x' ∷ xs') h () i∉is | nothing | Reveal_is_.[_] ph' +lemma-∉-lookupM-assoc eq i (i' ∷ is') (x' ∷ xs') h ph i∉is | just h' | Reveal_is_.[_] ph' = apply-checkInsertProof eq i' x' h' record { same = λ lookupM-i'-h'≡just-x' → begin lookupM i h ≡⟨ cong (lookupM i) (lemma-from-just (trans (sym ph) (lemma-checkInsert-same eq i' x' h' lookupM-i'-h'≡just-x'))) ⟩ @@ -80,7 +78,7 @@ lemma-∉-lookupM-assoc eq i (i' ∷ is') (x' ∷ xs') h ph i∉is | no ¬p | ju lookupM i h ≡⟨ cong (lookupM i) (lemma-from-just (trans (sym ph) (lemma-checkInsert-new eq i' x' h' lookupM-i'-h'≡nothing))) ⟩ lookupM i (insert i' x' h') - ≡⟨ sym (lemma-lookupM-insert-other i i' x' h' ¬p) ⟩ + ≡⟨ sym (lemma-lookupM-insert-other i i' x' h' (i∉is ∘ here)) ⟩ lookupM i h' ≡⟨ lemma-∉-lookupM-assoc eq i is' xs' h' ph' (i∉is ∘ there) ⟩ nothing ∎ @@ -123,8 +121,7 @@ lemma-map-lookupM-assoc eq i (i' ∷ is') x (x' ∷ xs') h h' ph' ph | yes p | ( lemma-map-lookupM-assoc eq i (i' ∷ is') x (x' ∷ xs') h h' ph' ph | yes p | (x'' , refl) | .(just x'') with eq x x'' lemma-map-lookupM-assoc eq i (i' ∷ is') x (x' ∷ xs') h .h ph' refl | yes p | (.x , refl) | .(just x) | yes refl = refl lemma-map-lookupM-assoc eq i (i' ∷ is') x (x' ∷ xs') h h' ph' () | yes p | (x'' , refl) | .(just x'') | no ¬p -lemma-map-lookupM-assoc eq i (i' ∷ is') x (x' ∷ xs') h h' ph' ph | no ¬p with lookupM i h' | lemma-∉-lookupM-assoc eq i (i' ∷ is') (x' ∷ xs') h' ph' ¬p -lemma-map-lookupM-assoc eq i (i' ∷ is') x (x' ∷ xs') h h' ph' ph | no ¬p | .nothing | refl = begin +lemma-map-lookupM-assoc eq i (i' ∷ is') x (x' ∷ xs') h h' ph' ph | no ¬p rewrite lemma-∉-lookupM-assoc eq i (i' ∷ is') (x' ∷ xs') h' ph' ¬p = begin map (flip lookupM h) (i' ∷ is') ≡⟨ map-cong (λ i'' → cong (lookupM i'') (lemma-from-just (sym ph))) (i' ∷ is') ⟩ map (flip lookupM (insert i x h')) (i' ∷ is') diff --git a/CheckInsert.agda b/CheckInsert.agda index 6c168e2..408a5b2 100644 --- a/CheckInsert.agda +++ b/CheckInsert.agda @@ -75,8 +75,7 @@ lemma-checkInsert-restrict {τ} eq f i is = apply-checkInsertProof eq i (f i) (r lemma-lookupM-checkInsert : {A : Set} {n : ℕ} → (eq : EqInst A) → (i j : Fin n) → (x y : A) → (h h' : FinMapMaybe n A) → lookupM i h ≡ just x → checkInsert eq j y h ≡ just h' → lookupM i h' ≡ just x lemma-lookupM-checkInsert eq i j x y h h' pl ph' with lookupM j h | inspect (lookupM j) h lemma-lookupM-checkInsert eq i j x y h .(insert j y h) pl refl | nothing | pl' with i ≟ j -lemma-lookupM-checkInsert eq i .i x y h .(insert i y h) pl refl | nothing | Reveal_is_.[_] pl' | yes refl with begin just x ≡⟨ sym pl ⟩ lookupM i h ≡⟨ pl' ⟩ nothing ∎ -... | () +lemma-lookupM-checkInsert eq i .i x y h .(insert i y h) pl refl | nothing | Reveal_is_.[_] pl' | yes refl = lemma-just≢nothing (begin just x ≡⟨ sym pl ⟩ lookupM i h ≡⟨ pl' ⟩ (nothing ∎)) lemma-lookupM-checkInsert eq i j x y h .(insert j y h) pl refl | nothing | pl' | no ¬p = begin lookupM i (insert j y h) ≡⟨ sym (lemma-lookupM-insert-other i j y h ¬p) ⟩ diff --git a/LiftGet.agda b/LiftGet.agda index 3c07fd7..7731f6b 100644 --- a/LiftGet.agda +++ b/LiftGet.agda @@ -8,7 +8,7 @@ open import Data.List.Properties using (length-map) open import Data.Product using (∃ ; _,_ ; proj₁ ; proj₂) open import Function using (_∘_ ; flip ; const) open import Relation.Binary.Core using (_≡_) -open import Relation.Binary.PropositionalEquality using (_≗_ ; sym ; cong ; refl) +open import Relation.Binary.PropositionalEquality using (_≗_ ; sym ; cong ; refl ; subst ; trans ; proof-irrelevance) open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) get-type : Set₁ @@ -44,15 +44,12 @@ 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) -vec-length : {A : Set} {n m : ℕ} → n ≡ m → Vec A n → Vec A m -vec-length refl v = v - toList-fromList : {A : Set} → (l : List A) → toList (fromList l) ≡ l toList-fromList [] = refl toList-fromList (x ∷ xs) = cong (_∷_ x) (toList-fromList xs) -vec-length-same : {A : Set} → (l : List A) → {n : ℕ} → (p : length l ≡ n) → toList (vec-length p (fromList l)) ≡ l -vec-length-same l refl = toList-fromList l +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 @@ -67,23 +64,40 @@ getList-to-getVec get = getlen , get' where getlen : ℕ → ℕ getlen = getList-to-getlen get get' : {C : Set} {m : ℕ} → Vec C m → Vec C (getlen m) - get' v = vec-length (getList-to-getVec-length-property get v) (fromList (get (toList v))) - -{- --- We cannot formulate the first commutation property, because the type of --- fromList (get l) depends on the concrete l, more specifically its length. -get-commut-1 : (get : get-type) → (fromList ∘ get) ≗ (proj₂ (getList-to-getVec get)) ∘ fromList -get-commut-1 get l = ? --} + 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) + ≡⟨ sym (subst-fromList (cong get (toList-fromList l))) ⟩ + subst (Vec A) (cong length (cong get (toList-fromList l))) (fromList (get (toList (fromList l)))) + ≡⟨ cong (flip (subst (Vec A)) (fromList (get (toList (fromList l))))) (proof-irrelevance (cong length (cong get (toList-fromList l))) (trans p p')) ⟩ + subst (Vec A) (trans p p') (fromList (get (toList (fromList l)))) + ≡⟨ sym (subst-subst (Vec A) p p' (fromList (get (toList (fromList l))))) ⟩ + subst (Vec A) p' (subst (Vec A) p (fromList (get (toList (fromList l))))) + ≡⟨ refl ⟩ + subst (Vec A) p' (proj₂ (getList-to-getVec get) (fromList l)) ∎ + where p : length (get (toList (fromList l))) ≡ length (get (replicate (length l) tt)) + p = getList-to-getVec-length-property get (fromList l) + p' : length (get (replicate (length l) tt)) ≡ length (get l) + p' = sym (getList-length get l) get-trafo-1 : (get : get-type) → {B : Set} → getVec-to-getList (proj₂ (getList-to-getVec get)) {B} ≗ get {B} -get-trafo-1 get l = begin +get-trafo-1 get {B} l = begin getVec-to-getList (proj₂ (getList-to-getVec get)) l ≡⟨ refl ⟩ toList (proj₂ (getList-to-getVec get) (fromList l)) ≡⟨ refl ⟩ - toList (vec-length (getList-to-getVec-length-property get (fromList l)) (fromList (get (toList (fromList l))))) - ≡⟨ vec-length-same (get (toList (fromList l))) (getList-to-getVec-length-property get (fromList l)) ⟩ + toList (subst (Vec B) (getList-to-getVec-length-property get (fromList l)) (fromList (get (toList (fromList l))))) + ≡⟨ toList-subst (fromList (get (toList (fromList l)))) (getList-to-getVec-length-property get (fromList l)) ⟩ + toList (fromList (get (toList (fromList l)))) + ≡⟨ toList-fromList (get (toList (fromList l))) ⟩ get (toList (fromList l)) ≡⟨ cong get (toList-fromList l) ⟩ get l ∎ @@ -91,47 +105,71 @@ get-trafo-1 get l = begin vec-len : {A : Set} {n : ℕ} → Vec A n → ℕ vec-len {_} {n} _ = n -vec-len-via-list : {A : Set} {n : ℕ} → (v : Vec A n) → length (toList v) ≡ vec-len v -vec-len-via-list []V = refl -vec-len-via-list (x ∷V xs) = cong suc (vec-len-via-list xs) - 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) -{- --- We cannot write the following property, because the expressions --- fromList (toList v) and v have different type. The type differs in the --- length. Somehow we would have to embed a proof that those types are in fact --- the same into the type signature of the function. -fromList-toList : {A : Set} {n : ℕ} → (v : Vec A n) → fromList (toList v) ≡ v -fromList-toList v = ? --} +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 + x ∷V fromList (toList xs) + ≡⟨ cong (_∷V_ x) (fromList-toList xs) ⟩ + x ∷V subst (Vec A) (sym (length-toList xs)) xs + ≡⟨ subst-cong (Vec A) (_∷V_ x) (sym (length-toList xs)) xs ⟩ + subst (Vec A) (cong suc (sym (length-toList xs))) (x ∷V xs) + ≡⟨ cong (λ p → subst (Vec A) p (x ∷V xs)) (proof-irrelevance (cong suc (sym (length-toList xs))) (sym (cong suc (length-toList xs)))) ⟩ + subst (Vec A) (sym (length-toList (x ∷V xs))) (x ∷V xs) ∎ get-commut-2 : (getlen : ℕ → ℕ) → (get : getV-type getlen) → {B : Set} {n : ℕ} → (toList ∘ get {B} {n}) ≗ (getVec-to-getList get) ∘ toList -get-commut-2 getlen get v = {!!} +get-commut-2 getlen get {B} v = begin + toList (get v) + ≡⟨ sym (toList-subst (get v) (cong getlen (sym (length-toList v)))) ⟩ + toList (subst (Vec B) (cong getlen (sym (length-toList v))) (get v)) + ≡⟨ cong toList (sym (subst-cong (Vec B) get (sym (length-toList v)) v)) ⟩ + toList (get (subst (Vec B) (sym (length-toList v)) v)) + ≡⟨ cong (toList ∘ get) (sym (fromList-toList v)) ⟩ + toList (get (fromList (toList v))) ∎ get-trafo-2-getlen : (getlen : ℕ → ℕ) → (get : getV-type getlen) → proj₁ (getList-to-getVec (getVec-to-getList get)) ≗ getlen get-trafo-2-getlen getlen get n = begin proj₁ (getList-to-getVec (getVec-to-getList get)) n ≡⟨ refl ⟩ length (toList (get (fromList (replicate n tt)))) - ≡⟨ vec-len-via-list (get (fromList (replicate n tt))) ⟩ + ≡⟨ length-toList (get (fromList (replicate n tt))) ⟩ vec-len (get (fromList (replicate n tt))) ≡⟨ cong getlen (length-replicate n) ⟩ getlen n ∎ getVec-getlen : {getlen₁ getlen₂ : ℕ → ℕ} → (get : getV-type getlen₁) → getlen₁ ≗ getlen₂ → getV-type getlen₂ -getVec-getlen get p {B} {n} v = vec-length (p n) (get v) +getVec-getlen get p {B} {n} v = subst (Vec B) (p n) (get v) get-trafo-2-get : (getlen : ℕ → ℕ) → (get : getV-type getlen) → {B : Set} {n : ℕ} → proj₂ (getList-to-getVec (getVec-to-getList get)) {B} {n} ≗ getVec-getlen get (sym ∘ (get-trafo-2-getlen getlen get)) -get-trafo-2-get getlen get v = begin +get-trafo-2-get getlen get {B} {n} v = begin proj₂ (getList-to-getVec (getVec-to-getList get)) v ≡⟨ refl ⟩ - vec-length (getList-to-getVec-length-property (getVec-to-getList get) v) (fromList (toList (get (fromList (toList v))))) - ≡⟨ {!!} ⟩ - vec-length (sym (get-trafo-2-getlen getlen get (vec-len v))) (vec-length (cong getlen (length-toList v)) (get (fromList (toList v)))) - ≡⟨ {!!} ⟩ - vec-length (sym (get-trafo-2-getlen getlen get (vec-len v))) (get v) + subst (Vec B) p (fromList (toList (get (fromList (toList v))))) + ≡⟨ cong (subst (Vec B) p) (fromList-toList (get (fromList (toList v)))) ⟩ + subst (Vec B) p (subst (Vec B) p' (get (fromList (toList v)))) + ≡⟨ subst-subst (Vec B) p' p (get (fromList (toList v))) ⟩ + subst (Vec B) (trans p' p) (get (fromList (toList v))) + ≡⟨ cong (subst (Vec B) (trans p' p) ∘ get) (fromList-toList v) ⟩ + subst (Vec B) (trans p' p) (get (subst (Vec B) (sym (length-toList v)) v)) + ≡⟨ cong (subst (Vec B) (trans p' p)) (subst-cong (Vec B) get (sym (length-toList v)) v) ⟩ + subst (Vec B) (trans p' p) (subst (Vec B) (cong getlen (sym (length-toList v))) (get v)) + ≡⟨ subst-subst (Vec B) (cong getlen (sym (length-toList v))) (trans p' p) (get v) ⟩ + subst (Vec B) (trans (cong getlen (sym (length-toList v))) (trans p' p)) (get v) + ≡⟨ cong (flip (subst (Vec B)) (get v)) (proof-irrelevance (trans (cong getlen (sym (length-toList v))) (trans p' p)) p'') ⟩ + subst (Vec B) p'' (get v) ≡⟨ refl ⟩ getVec-getlen get (sym ∘ (get-trafo-2-getlen getlen get)) v ∎ + where n' : ℕ + n' = length (toList (get (fromList (replicate n tt)))) + p : length (toList (get (fromList (toList v)))) ≡ n' + p = getList-to-getVec-length-property (getVec-to-getList get) v + p' : getlen (length (toList v)) ≡ length (toList (get (fromList (toList v)))) + p' = sym (length-toList (get (fromList (toList v)))) + p'' : getlen n ≡ n' + p'' = sym (get-trafo-2-getlen getlen get (vec-len v)) |