diff options
| -rw-r--r-- | Bidir.agda | 11 | ||||
| -rw-r--r-- | CheckInsert.agda | 2 | ||||
| -rw-r--r-- | FinMap.agda | 6 |
3 files changed, 8 insertions, 11 deletions
@@ -163,18 +163,15 @@ map-just-injective {xs = x ∷ xs'} {ys = .x ∷ ys'} p | refl , p' = cong (_∷ 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') p with Data.List.All.head p -lemma-union-not-used h h' (i ∷ is') p | x , lookupM-i-h≡just-x = cong₂ _∷_ (begin +lemma-union-not-used h h' (i ∷ is') (All._∷_ (x , px) p') = cong₂ _∷_ (begin just (lookup i (union h h')) ≡⟨ cong just (lookup∘tabulate (λ j → maybe′ id (lookup j h') (lookupM j h)) i) ⟩ just (maybe′ id (lookup i h') (lookupM i h)) - ≡⟨ cong just (cong (maybe′ id (lookup i h')) lookupM-i-h≡just-x) ⟩ + ≡⟨ cong just (cong (maybe′ id (lookup i h')) px) ⟩ just (maybe′ id (lookup i h') (just x)) - ≡⟨ refl ⟩ - just x - ≡⟨ sym lookupM-i-h≡just-x ⟩ + ≡⟨ sym px ⟩ lookupM i h ∎) - (lemma-union-not-used h h' is' (Data.List.All.tail p)) + (lemma-union-not-used h h' is' p') theorem-2 : {getlen : ℕ → ℕ} (get : get-type getlen) → {m : ℕ} → (v : Vec Carrier (getlen m)) → (s u : Vec Carrier m) → bff get s v ≡ just u → get u ≡ v theorem-2 get v s u p with lemma-fmap-just (proj₂ (lemma-fmap-just p)) diff --git a/CheckInsert.agda b/CheckInsert.agda index 17228f2..8c1aa20 100644 --- a/CheckInsert.agda +++ b/CheckInsert.agda @@ -59,7 +59,7 @@ lemma-checkInsert-restrict f i is | ._ | insert-wrong x fi≢x p = contradiction lemma-lookupM-checkInsert : {n : ℕ} → (i j : Fin n) → (x y : Carrier) → (h h' : FinMapMaybe n Carrier) → lookupM i h ≡ just x → checkInsert j y h ≡ just h' → lookupM i h' ≡ just x lemma-lookupM-checkInsert i j x y h h' pl ph' with lookupM j h | inspect (lookupM j) h lemma-lookupM-checkInsert i j x y h .(insert j y h) pl refl | nothing | pl' with i ≟ j -lemma-lookupM-checkInsert i .i x y h .(insert i y h) pl refl | nothing | [ pl' ] | yes refl = lemma-just≢nothing (trans (sym pl) pl') +lemma-lookupM-checkInsert i .i x y h .(insert i y h) pl refl | nothing | [ pl' ] | yes refl = lemma-just≢nothing pl pl' lemma-lookupM-checkInsert 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/FinMap.agda b/FinMap.agda index 2b50920..8b4103b 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -46,8 +46,8 @@ union m1 m2 = fromFunc (λ f → maybe′ id (lookup f m2) (lookupM f m1)) restrict : {A : Set} {n : ℕ} → (Fin n → A) → List (Fin n) → FinMapMaybe n A restrict f is = fromAscList (zip is (map f is)) -lemma-just≢nothing : {A Whatever : Set} {a : A} → _≡_ {_} {Maybe A} (just a) nothing → Whatever -lemma-just≢nothing () +lemma-just≢nothing : {A Whatever : Set} {a : A} {ma : Maybe A} → ma ≡ just a → ma ≡ nothing → Whatever +lemma-just≢nothing refl () lemma-insert-same : {τ : Set} {n : ℕ} → (m : FinMapMaybe n τ) → (f : Fin n) → (a : τ) → lookupM f m ≡ just a → m ≡ insert f a m lemma-insert-same [] () a p @@ -72,7 +72,7 @@ just-injective : {A : Set} → {x y : A} → _≡_ {_} {Maybe A} (just x) (just 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 (trans (sym p) (lemma-lookupM-empty i)) +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' lemma-lookupM-restrict i f (.i ∷ is) a p | yes refl = just-injective (begin just (f i) |