From 3badfdc549d717824f72b0c1df35c52e00ce6dbf Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Wed, 9 Jan 2013 23:26:46 +0100 Subject: add new lemma-checkInsert-lookupM Suggested by Joachim Breitner. --- CheckInsert.agda | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/CheckInsert.agda b/CheckInsert.agda index 7e3f3aa..796bece 100644 --- a/CheckInsert.agda +++ b/CheckInsert.agda @@ -84,3 +84,15 @@ lemma-lookupM-checkInsert i j x y h .(insert j y h) pl refl | nothing | pl' | no lemma-lookupM-checkInsert i j x y h h' pl ph' | just z | pl' with deq y z lemma-lookupM-checkInsert i j x y h .h pl refl | just .y | pl' | yes refl = pl lemma-lookupM-checkInsert i j x y h h' pl () | just z | pl' | no ¬p + +lemma-checkInsert-lookupM : {n : ℕ} → (i j : Fin n) → i ≢ j → (x : Carrier) → (r : Maybe Carrier) → (h h' : FinMapMaybe n Carrier) → lookupM i h' ≡ r → checkInsert j x h ≡ just h' → lookupM i h ≡ r +lemma-checkInsert-lookupM i j i≢j x r h h' pl ph' with lookupM j h +lemma-checkInsert-lookupM i j i≢j x r h h' pl ph' | just y with deq x y +lemma-checkInsert-lookupM i j i≢j x r h .h pl refl | just .x | yes refl = pl +lemma-checkInsert-lookupM i j i≢j x r h h' pl () | just y | no x≢y +lemma-checkInsert-lookupM i j i≢j x r h .(insert j x h) pl refl | nothing = begin + lookupM i h + ≡⟨ lemma-lookupM-insert-other i j x h i≢j ⟩ + lookupM i (insert j x h) + ≡⟨ pl ⟩ + r ∎ -- cgit v1.2.3 From 400b30320b90620e47a16f3f1ec4ce3dad37e8b0 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Wed, 9 Jan 2013 23:46:10 +0100 Subject: rewrite lemma-\notin-lookupM-assoc It can be shortened considerably using lemma-checkInsert-lookupM. --- Bidir.agda | 23 ++++++----------------- 1 file changed, 6 insertions(+), 17 deletions(-) diff --git a/Bidir.agda b/Bidir.agda index 8fa36c9..901e2d1 100644 --- a/Bidir.agda +++ b/Bidir.agda @@ -60,23 +60,12 @@ lemma-∉-lookupM-assoc : {m n : ℕ} → (i : Fin n) → (is : Vec (Fin n) m) lemma-∉-lookupM-assoc i [] [] .empty refl i∉is = lemma-lookupM-empty i lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') h ph i∉is with assoc is' xs' | inspect (assoc is') xs' lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') h () i∉is | nothing | [ ph' ] -lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') h ph i∉is | just h' | [ ph' ] = apply-checkInsertProof i' x' h' record { - same = λ lookupM-i'-h'≡just-x' → begin - lookupM i h - ≡⟨ cong (lookupM i) (just-injective (trans (sym ph) (lemma-checkInsert-same i' x' h' lookupM-i'-h'≡just-x'))) ⟩ - lookupM i h' - ≡⟨ lemma-∉-lookupM-assoc i is' xs' h' ph' (i∉is ∘ there) ⟩ - nothing ∎ - ; new = λ lookupM-i'-h'≡nothing → begin - lookupM i h - ≡⟨ cong (lookupM i) (just-injective (trans (sym ph) (lemma-checkInsert-new i' x' h' lookupM-i'-h'≡nothing))) ⟩ - lookupM i (insert i' x' h') - ≡⟨ sym (lemma-lookupM-insert-other i i' x' h' (i∉is ∘ here)) ⟩ - lookupM i h' - ≡⟨ lemma-∉-lookupM-assoc i is' xs' h' ph' (i∉is ∘ there) ⟩ - nothing ∎ - ; wrong = λ x'' x'≢x'' lookupM-i'-h'≡just-x'' → lemma-just≢nothing (trans (sym ph) (lemma-checkInsert-wrong i' x' h' x'' x'≢x'' lookupM-i'-h'≡just-x'')) - } +lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') h ph i∉is | just h' | [ ph' ] = begin + lookupM i h + ≡⟨ sym (lemma-checkInsert-lookupM i i' (i∉is ∘ here) x' (lookupVec i h) h' h refl ph) ⟩ + lookupM i h' + ≡⟨ lemma-∉-lookupM-assoc i is' xs' h' ph' (i∉is ∘ there) ⟩ + nothing ∎ _in-domain-of_ : {n : ℕ} {A : Set} → (is : List (Fin n)) → (FinMapMaybe n A) → Set _in-domain-of_ is h = All (λ i → ∃ λ x → lookupM i h ≡ just x) is -- cgit v1.2.3 From d42ffc9d24adb2b416ff73708ae64c1d4ca50c30 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Thu, 10 Jan 2013 11:09:38 +0100 Subject: reduce a precondition of lemma-checkInsert-lookupM Now it looks a lot more like lemma-lookupM-insert-other, so rename it to lemma-lookupM-checkInsert-other. --- Bidir.agda | 2 +- CheckInsert.agda | 17 ++++++----------- 2 files changed, 7 insertions(+), 12 deletions(-) diff --git a/Bidir.agda b/Bidir.agda index 901e2d1..3dbdbdd 100644 --- a/Bidir.agda +++ b/Bidir.agda @@ -62,7 +62,7 @@ lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') h ph i∉is with assoc is' x lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') h () i∉is | nothing | [ ph' ] lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') h ph i∉is | just h' | [ ph' ] = begin lookupM i h - ≡⟨ sym (lemma-checkInsert-lookupM i i' (i∉is ∘ here) x' (lookupVec i h) h' h refl ph) ⟩ + ≡⟨ sym (lemma-lookupM-checkInsert-other i i' (i∉is ∘ here) x' h' h ph) ⟩ lookupM i h' ≡⟨ lemma-∉-lookupM-assoc i is' xs' h' ph' (i∉is ∘ there) ⟩ nothing ∎ diff --git a/CheckInsert.agda b/CheckInsert.agda index 796bece..4083720 100644 --- a/CheckInsert.agda +++ b/CheckInsert.agda @@ -85,14 +85,9 @@ lemma-lookupM-checkInsert i j x y h h' pl ph' | just z | pl' with deq y z lemma-lookupM-checkInsert i j x y h .h pl refl | just .y | pl' | yes refl = pl lemma-lookupM-checkInsert i j x y h h' pl () | just z | pl' | no ¬p -lemma-checkInsert-lookupM : {n : ℕ} → (i j : Fin n) → i ≢ j → (x : Carrier) → (r : Maybe Carrier) → (h h' : FinMapMaybe n Carrier) → lookupM i h' ≡ r → checkInsert j x h ≡ just h' → lookupM i h ≡ r -lemma-checkInsert-lookupM i j i≢j x r h h' pl ph' with lookupM j h -lemma-checkInsert-lookupM i j i≢j x r h h' pl ph' | just y with deq x y -lemma-checkInsert-lookupM i j i≢j x r h .h pl refl | just .x | yes refl = pl -lemma-checkInsert-lookupM i j i≢j x r h h' pl () | just y | no x≢y -lemma-checkInsert-lookupM i j i≢j x r h .(insert j x h) pl refl | nothing = begin - lookupM i h - ≡⟨ lemma-lookupM-insert-other i j x h i≢j ⟩ - lookupM i (insert j x h) - ≡⟨ pl ⟩ - r ∎ +lemma-lookupM-checkInsert-other : {n : ℕ} → (i j : Fin n) → i ≢ j → (x : Carrier) → (h h' : FinMapMaybe n Carrier) → checkInsert j x h ≡ just h' → lookupM i h ≡ lookupM i h' +lemma-lookupM-checkInsert-other i j i≢j x h h' ph' with lookupM j h +lemma-lookupM-checkInsert-other i j i≢j x h h' ph' | just y with deq x y +lemma-lookupM-checkInsert-other i j i≢j x h .h refl | just .x | yes refl = refl +lemma-lookupM-checkInsert-other i j i≢j x h h' () | just y | no x≢y +lemma-lookupM-checkInsert-other i j i≢j x h .(insert j x h) refl | nothing = lemma-lookupM-insert-other i j x h i≢j -- cgit v1.2.3