From 0a5bb4e9d223f74858d8d9022f1169852899e81a Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Sat, 5 Jan 2013 10:41:37 +0100 Subject: shrink base case of lemma-/notin-lookupM-assoc --- Bidir.agda | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) (limited to 'Bidir.agda') diff --git a/Bidir.agda b/Bidir.agda index bed902a..fd33bbc 100644 --- a/Bidir.agda +++ b/Bidir.agda @@ -57,12 +57,7 @@ lemma-lookupM-assoc i is x xs h p | just h' = apply-checkInsertProof i x h' r } lemma-∉-lookupM-assoc : {m n : ℕ} → (i : Fin n) → (is : Vec (Fin n) m) → (xs : Vec Carrier m) → (h : FinMapMaybe n Carrier) → assoc is xs ≡ just h → (i ∉ toList is) → lookupM i h ≡ nothing -lemma-∉-lookupM-assoc i [] [] h ph i∉is = begin - lookupM i h - ≡⟨ cong (lookupM i) (sym (just-injective ph)) ⟩ - lookupM i empty - ≡⟨ lemma-lookupM-empty i ⟩ - nothing ∎ +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 { -- cgit v1.2.3