shrink base case of lemma-/notin-lookupM-assoc
authorHelmut Grohne <helmut@subdivi.de>
Sat, 5 Jan 2013 09:41:37 +0000 (10:41 +0100)
committerHelmut Grohne <helmut@subdivi.de>
Sat, 5 Jan 2013 09:41:37 +0000 (10:41 +0100)
Bidir.agda

index bed902a..fd33bbc 100644 (file)
@@ -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 {