show a stronger lemma-checkInsert-restrict
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Thu, 23 Jan 2014 10:48:54 +0000 (11:48 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Thu, 23 Jan 2014 10:48:54 +0000 (11:48 +0100)
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
CheckInsert.agda
FinMap.agda

index 0b2967d..4c59791 100644 (file)
@@ -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
index 9302fc7..47af215 100644 (file)
@@ -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
index a85f119..1fc2d16 100644 (file)
@@ -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