diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-01-23 11:48:54 +0100 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-01-23 11:48:54 +0100 |
| commit | 9cb635bb49c1846da7f9c00cc475b0fac9a2fa42 (patch) | |
| tree | a78b7bc2987a76334da921abcf4165bca727b914 /CheckInsert.agda | |
| parent | 808b8da4b14b087c0dcace71fff3854a17cebe42 (diff) | |
| download | bidiragda-9cb635bb49c1846da7f9c00cc475b0fac9a2fa42.tar.gz | |
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.
Diffstat (limited to 'CheckInsert.agda')
| -rw-r--r-- | CheckInsert.agda | 12 |
1 files changed, 3 insertions, 9 deletions
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 |