From 48a000f3dc05a9117a9b72e250569c204a4d1371 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Thu, 16 Jan 2014 11:32:12 +0100 Subject: generalize lemma-insert-same to arbitrary Setoids The general idea is to enable bff to use arbitrary DecSetoids. * assoc needs to learn about DecSetoid * checkInsert needs to learn about DecSetoid * InsertionResult needs to learn about Setoid * Parameters to InsertionResult.same become weaker * lemma-checkInsert-restrict should work with weaker same * lemma-insert-same needs to learn about Setoid --- FinMap.agda | 24 ++++++++++++++++++------ 1 file changed, 18 insertions(+), 6 deletions(-) (limited to 'FinMap.agda') diff --git a/FinMap.agda b/FinMap.agda index 46dbd1c..a85f119 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -1,21 +1,25 @@ module FinMap where +open import Level using () renaming (zero to ℓ₀) open import Data.Nat using (ℕ ; zero ; suc) -open import Data.Maybe using (Maybe ; just ; nothing ; maybe′) +open import Data.Maybe using (Maybe ; just ; nothing ; maybe′) renaming (setoid to MaybeEq) open import Data.Fin using (Fin ; zero ; suc) open import Data.Fin.Props using (_≟_) open import Data.Vec using (Vec ; [] ; _∷_ ; _[_]≔_ ; replicate ; tabulate ; foldr) renaming (lookup to lookupVec ; map to mapV) +open import Data.Vec.Equality using () +open Data.Vec.Equality.Equality using (_∷-cong_) open import Data.Vec.Properties using (lookup∘tabulate) open import Data.List using (List ; [] ; _∷_ ; map ; zip) open import Data.Product using (_×_ ; _,_) open import Function using (id ; _∘_ ; flip ; const) open import Relation.Nullary using (yes ; no) open import Relation.Nullary.Negation using (contradiction) +open import Relation.Binary using (Setoid ; module Setoid) 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) +open import Generic using (just-injective ; vecIsSetoid) FinMapMaybe : ℕ → Set → Set FinMapMaybe n A = Vec (Maybe A) n @@ -60,10 +64,18 @@ partialize = mapV just 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 -lemma-insert-same (.(just a) ∷ xs) zero a refl = refl -lemma-insert-same (x ∷ xs) (suc i) a p = cong (_∷_ x) (lemma-insert-same xs i a p) +module Private {S : Setoid ℓ₀ ℓ₀} where + private + open Setoid S + reflMaybe = Setoid.refl (MaybeEq S) + _≈Maybe_ = Setoid._≈_ (MaybeEq S) + + lemma-insert-same : {n : ℕ} → (m : FinMapMaybe n Carrier) → (f : Fin n) → (a : Carrier) → lookupM f m ≈Maybe just a → Setoid._≈_ (vecIsSetoid (MaybeEq S) n) m (insert f a m) + lemma-insert-same [] () a p + lemma-insert-same {suc n} (x ∷ xs) zero a p = p ∷-cong Setoid.refl (vecIsSetoid (MaybeEq S) n) + lemma-insert-same (x ∷ xs) (suc i) a p = reflMaybe ∷-cong lemma-insert-same xs i a p + +open Private public lemma-lookupM-empty : {A : Set} {n : ℕ} → (i : Fin n) → lookupM {A} i empty ≡ nothing lemma-lookupM-empty zero = refl -- cgit v1.2.3 From 9cb635bb49c1846da7f9c00cc475b0fac9a2fa42 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Thu, 23 Jan 2014 11:48:54 +0100 Subject: show a stronger lemma-checkInsert-restrict We can actually get semantic equality there without requiring anything else. Indeed this was already hinted in the BX for free paper that says, that lemma-1 holds in semantic equality. --- Bidir.agda | 14 +------------- CheckInsert.agda | 12 +++--------- FinMap.agda | 16 ++++------------ 3 files changed, 8 insertions(+), 34 deletions(-) (limited to 'FinMap.agda') diff --git a/Bidir.agda b/Bidir.agda index 0b2967d..4c59791 100644 --- a/Bidir.agda +++ b/Bidir.agda @@ -31,25 +31,13 @@ open CheckInsert (decSetoid deq) import BFF open BFF.VecBFF Carrier deq using (assoc ; enumerate ; denumerate ; bff) -maybeSetoid-to-≡ : {A : Set} {x y : Setoid.Carrier (MaybeSetoid (≡-setoid A))} → Setoid._≈_ (MaybeSetoid (≡-setoid A)) x y → x ≡ y -maybeSetoid-to-≡ (just refl) = refl -maybeSetoid-to-≡ nothing = refl - -vecMaybeSetoid-to-≡ : {A : Set} {n : ℕ} {x y : Setoid.Carrier (vecIsSetoid (MaybeSetoid (≡-setoid A)) n)} → Setoid._≈_ (vecIsSetoid (MaybeSetoid (≡-setoid A)) n) x y → x ≡ y -vecMaybeSetoid-to-≡ VecEq.[]-cong = refl -vecMaybeSetoid-to-≡ (p₁ VecEq.∷-cong p₂) = cong₂ _∷_ (maybeSetoid-to-≡ p₁) (vecMaybeSetoid-to-≡ p₂) - -maybeVecMaybeSetoid-to-≡ : {A : Set} {n : ℕ} {x y : Setoid.Carrier (MaybeSetoid (vecIsSetoid (MaybeSetoid (≡-setoid A)) n))} → Setoid._≈_ (MaybeSetoid (vecIsSetoid (MaybeSetoid (≡-setoid A)) n)) x y → x ≡ y -maybeVecMaybeSetoid-to-≡ (just p) rewrite vecMaybeSetoid-to-≡ p = refl -maybeVecMaybeSetoid-to-≡ nothing = refl - lemma-1 : {m n : ℕ} → (f : Fin n → Carrier) → (is : Vec (Fin n) m) → assoc is (map f is) ≡ just (restrict f (toList is)) lemma-1 f [] = refl lemma-1 f (i ∷ is′) = begin (assoc is′ (map f is′) >>= checkInsert i (f i)) ≡⟨ cong (λ m → m >>= checkInsert i (f i)) (lemma-1 f is′) ⟩ checkInsert i (f i) (restrict f (toList is′)) - ≡⟨ maybeVecMaybeSetoid-to-≡ (lemma-checkInsert-restrict f i (toList is′)) ⟩ + ≡⟨ lemma-checkInsert-restrict f i (toList is′) ⟩ just (restrict f (toList (i ∷ is′))) ∎ lemma-lookupM-assoc : {m n : ℕ} → (i : Fin n) → (is : Vec (Fin n) m) → (x : Carrier) → (xs : Vec Carrier m) → (h : FinMapMaybe n Carrier) → assoc (i ∷ is) (x ∷ xs) ≡ just h → lookupM i h ≡ just x diff --git a/CheckInsert.agda b/CheckInsert.agda index 9302fc7..47af215 100644 --- a/CheckInsert.agda +++ b/CheckInsert.agda @@ -58,16 +58,10 @@ lemma-checkInsert-wrong i x m x' d refl | .(just x') with deq x x' lemma-checkInsert-wrong i x m x' d refl | .(just x') | yes q = contradiction q d lemma-checkInsert-wrong i x m x' d refl | .(just x') | no ¬q = refl -lemma-checkInsert-restrict : {n : ℕ} → (f : Fin n → Carrier) → (i : Fin n) → (is : List (Fin n)) → Setoid._≈_ (MaybeSetoid (vecIsSetoid (MaybeSetoid A.setoid) n)) (checkInsert i (f i) (restrict f is)) (just (restrict f (i ∷ is))) +lemma-checkInsert-restrict : {n : ℕ} → (f : Fin n → Carrier) → (i : Fin n) → (is : List (Fin n)) → checkInsert i (f i) (restrict f is) ≡ just (restrict f (i ∷ is)) lemma-checkInsert-restrict f i is with checkInsert i (f i) (restrict f is) | insertionresult i (f i) (restrict f is) -lemma-checkInsert-restrict f i is | ._ | same x fi≈x p = MaybeEq.just (lemma-insert-same _ i (f i) (begin - lookupM i (restrict f is) - ≡⟨ p ⟩ - just x - ≈⟨ MaybeEq.just (Setoid.sym A.setoid fi≈x) ⟩ - just (f i) ∎)) - where open EqR (MaybeSetoid A.setoid) -lemma-checkInsert-restrict f i is | ._ | new _ = Setoid.refl (MaybeSetoid (vecIsSetoid (MaybeSetoid A.setoid) _)) +lemma-checkInsert-restrict f i is | ._ | same x fi≈x p = cong just (lemma-insert-same _ i (f i) (trans p (cong just (sym (lemma-lookupM-restrict i f is x p))))) +lemma-checkInsert-restrict f i is | ._ | new _ = refl lemma-checkInsert-restrict f i is | ._ | wrong x fi≉x p = contradiction (IsPreorder.reflexive (Setoid.isPreorder A.setoid) (lemma-lookupM-restrict i f is x p)) fi≉x 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 diff --git a/FinMap.agda b/FinMap.agda index a85f119..1fc2d16 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -64,18 +64,10 @@ partialize = mapV just lemma-just≢nothing : {A Whatever : Set} {a : A} {ma : Maybe A} → ma ≡ just a → ma ≡ nothing → Whatever lemma-just≢nothing refl () -module Private {S : Setoid ℓ₀ ℓ₀} where - private - open Setoid S - reflMaybe = Setoid.refl (MaybeEq S) - _≈Maybe_ = Setoid._≈_ (MaybeEq S) - - lemma-insert-same : {n : ℕ} → (m : FinMapMaybe n Carrier) → (f : Fin n) → (a : Carrier) → lookupM f m ≈Maybe just a → Setoid._≈_ (vecIsSetoid (MaybeEq S) n) m (insert f a m) - lemma-insert-same [] () a p - lemma-insert-same {suc n} (x ∷ xs) zero a p = p ∷-cong Setoid.refl (vecIsSetoid (MaybeEq S) n) - lemma-insert-same (x ∷ xs) (suc i) a p = reflMaybe ∷-cong lemma-insert-same xs i a p - -open Private public +lemma-insert-same : {n : ℕ} {A : Set} → (m : FinMapMaybe n A) → (f : Fin n) → (a : A) → lookupM f m ≡ just a → m ≡ insert f a m +lemma-insert-same [] () a p +lemma-insert-same {suc n} (x ∷ xs) zero a p = cong (flip _∷_ xs) p +lemma-insert-same (x ∷ xs) (suc i) a p = cong (_∷_ x) (lemma-insert-same xs i a p) lemma-lookupM-empty : {A : Set} {n : ℕ} → (i : Fin n) → lookupM {A} i empty ≡ nothing lemma-lookupM-empty zero = refl -- cgit v1.2.3