diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2012-09-14 20:41:26 +0200 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2012-09-14 20:41:26 +0200 |
| commit | dd4bbd5d31c003a054f676b859012105be81394b (patch) | |
| tree | 4367222e8836b1f4834b764acf4ae67e194539d7 | |
| parent | 566d649c300b41df3718cd717fee1bf36d4b04cd (diff) | |
| download | bidiragda-dd4bbd5d31c003a054f676b859012105be81394b.tar.gz | |
employ rewrite in lemma-map-lookupM-assoc
Thanks to Wouter Swierstra for pointing to the keyword.
| -rw-r--r-- | Bidir.agda | 3 |
1 files changed, 1 insertions, 2 deletions
@@ -130,8 +130,7 @@ lemma-map-lookupM-assoc eq i (i' ∷ is') x (x' ∷ xs') h h' ph' ph | yes p | ( lemma-map-lookupM-assoc eq i (i' ∷ is') x (x' ∷ xs') h h' ph' ph | yes p | (x'' , refl) | .(just x'') with eq x x'' lemma-map-lookupM-assoc eq i (i' ∷ is') x (x' ∷ xs') h .h ph' refl | yes p | (.x , refl) | .(just x) | yes refl = refl lemma-map-lookupM-assoc eq i (i' ∷ is') x (x' ∷ xs') h h' ph' () | yes p | (x'' , refl) | .(just x'') | no ¬p -lemma-map-lookupM-assoc eq i (i' ∷ is') x (x' ∷ xs') h h' ph' ph | no ¬p with lookupM i h' | lemma-∉-lookupM-assoc eq i (i' ∷ is') (x' ∷ xs') h' ph' ¬p -lemma-map-lookupM-assoc eq i (i' ∷ is') x (x' ∷ xs') h h' ph' ph | no ¬p | .nothing | refl = begin +lemma-map-lookupM-assoc eq i (i' ∷ is') x (x' ∷ xs') h h' ph' ph | no ¬p rewrite lemma-∉-lookupM-assoc eq i (i' ∷ is') (x' ∷ xs') h' ph' ¬p = begin map (flip lookupM h) (i' ∷ is') ≡⟨ map-cong (λ i'' → cong (lookupM i'') (lemma-from-just (sym ph))) (i' ∷ is') ⟩ map (flip lookupM (insert i x h')) (i' ∷ is') |