diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2012-12-10 10:57:50 +0100 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2012-12-10 10:57:50 +0100 |
| commit | b623a3e175a96b9732446a312080fa564ae80f71 (patch) | |
| tree | c48a16953aae693ba268022d6082df6e979c5d54 /Bidir.agda | |
| parent | 68c735629c8e4390b861c94d56c5c7785b4ab179 (diff) | |
| download | bidiragda-b623a3e175a96b9732446a312080fa564ae80f71.tar.gz | |
drop unused param from lemma-map-lookupM-insert
Diffstat (limited to 'Bidir.agda')
| -rw-r--r-- | Bidir.agda | 10 |
1 files changed, 5 insertions, 5 deletions
@@ -103,13 +103,13 @@ lemma-assoc-domain (i' ∷ is') (x' ∷ xs') h ph | just h' | [ ph' ] = apply-ch ; 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-map-lookupM-insert : {m n : ℕ} → (i : Fin n) → (is : Vec (Fin n) m) → (x : Carrier) → (h : FinMapMaybe n Carrier) → i ∉ (toList is) → (toList is) in-domain-of h → map (flip lookupM (insert i x h)) is ≡ map (flip lookupM h) is -lemma-map-lookupM-insert i [] x h i∉is ph = refl -lemma-map-lookupM-insert i (i' ∷ is') x h i∉is ph = begin +lemma-map-lookupM-insert : {m n : ℕ} → (i : Fin n) → (is : Vec (Fin n) m) → (x : Carrier) → (h : FinMapMaybe n Carrier) → i ∉ (toList is) → map (flip lookupM (insert i x h)) is ≡ map (flip lookupM h) is +lemma-map-lookupM-insert i [] x h i∉is = refl +lemma-map-lookupM-insert i (i' ∷ is') x h i∉is = begin lookupM i' (insert i x h) ∷ map (flip lookupM (insert i x h)) is' ≡⟨ cong (flip _∷_ (map (flip lookupM (insert i x h)) is')) (sym (lemma-lookupM-insert-other i' i x h (i∉is ∘ here ∘ sym))) ⟩ lookupM i' h ∷ map (flip lookupM (insert i x h)) is' - ≡⟨ cong (_∷_ (lookupM i' h)) (lemma-map-lookupM-insert i is' x h (i∉is ∘ there) (Data.List.All.tail ph)) ⟩ + ≡⟨ cong (_∷_ (lookupM i' h)) (lemma-map-lookupM-insert i is' x h (i∉is ∘ there)) ⟩ lookupM i' h ∷ map (flip lookupM h) is' ∎ lemma-map-lookupM-assoc : {m n : ℕ} → (i : Fin n) → (is : Vec (Fin n) m) → (x : Carrier) → (xs : Vec Carrier m) → (h : FinMapMaybe n Carrier) → (h' : FinMapMaybe n Carrier) → assoc is xs ≡ just h' → checkInsert i x h' ≡ just h → map (flip lookupM h) is ≡ map (flip lookupM h') is @@ -123,7 +123,7 @@ lemma-map-lookupM-assoc i is x xs h h' ph' ph | no ¬p rewrite lemma-∉-lookupM map (flip lookupM h) is ≡⟨ map-cong (λ i'' → cong (lookupM i'') (just-injective (sym ph))) is ⟩ map (flip lookupM (insert i x h')) is - ≡⟨ lemma-map-lookupM-insert i is x h' ¬p (lemma-assoc-domain is xs h' ph') ⟩ + ≡⟨ lemma-map-lookupM-insert i is x h' ¬p ⟩ map (flip lookupM h') is ∎ lemma-2 : {m n : ℕ} → (is : Vec (Fin n) m) → (v : Vec Carrier m) → (h : FinMapMaybe n Carrier) → assoc is v ≡ just h → map (flip lookupM h) is ≡ map just v |