started proving lemma-2
authorHelmut Grohne <helmut@subdivi.de>
Thu, 26 Jan 2012 16:12:44 +0000 (17:12 +0100)
committerHelmut Grohne <helmut@subdivi.de>
Thu, 26 Jan 2012 16:12:44 +0000 (17:12 +0100)
The step case needs two lemmata. One for the head of the resulting map and one
for the tail. The head case is shown using a

lemma-lookupM-assoc : assoc eq (i :: _) (x :: _) == just h ->
  lookupM i h == just x

Bidir.agda

index 0c41319..3123d5d 100644 (file)
@@ -9,7 +9,7 @@ open import Function using (id ; _∘_ ; flip)
 open import Relation.Nullary using (Dec ; yes ; no)
 open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Binary.Core using (_≡_ ; refl)
-open import Relation.Binary.PropositionalEquality using (cong ; inspect ; Reveal_is_)
+open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; Reveal_is_)
 open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
 
 open import FinMap
@@ -55,11 +55,34 @@ lemma-1 eq f (i âˆ· is′) = begin
     â‰¡âŸ¨ lemma-checkInsert-generate eq f i is′ âŸ©
   just (generate f (i âˆ· is′)) âˆŽ
 
-lemma-2 : {Ï„ : Set} {n : â„•} â†’ (eq : EqInst Ï„) â†’ (is : List (Fin n)) â†’ (v : List Ï„) â†’ (h : FinMapMaybe n Ï„) â†’ just h â‰¡ assoc eq is v â†’ map (flip lookup h) is â‰¡ map just v
+lemma-lookupM-assoc : {A : Set} {n : â„•} â†’ (eq : EqInst A) â†’ (i : Fin n) â†’ (is : List (Fin n)) â†’ (x : A) â†’ (xs : List A) â†’ (h : FinMapMaybe n A) â†’ assoc eq (i âˆ· is) (x âˆ· xs) â‰¡ just h â†’ lookupM i h â‰¡ just x
+lemma-lookupM-assoc eq i is x xs h    p with assoc eq is xs
+lemma-lookupM-assoc eq i is x xs h    ()   | nothing
+lemma-lookupM-assoc eq i is x xs h    p    | just h' with lookupM i h' | inspect (lookupM i) h'
+lemma-lookupM-assoc eq i is x xs .(insert i x h') refl | just h' | nothing | _ = lemma-lookupM-insert i x h'
+lemma-lookupM-assoc eq i is x xs h    p    | just h'   | just y  | _ with eq x y
+lemma-lookupM-assoc eq i is x xs h    ()   | just h'   | just y  | _ | no ¬prf
+lemma-lookupM-assoc eq i is x xs h    p    | just h'   | just .x | Reveal_is_.[_] p' | yes refl = begin
+  lookupM i h
+    â‰¡âŸ¨ cong (lookupM i) (lemma-from-just (sym p)) âŸ©
+  lookupM i h'
+    â‰¡âŸ¨ p' âŸ©
+  just x âˆŽ
+
+lemma-2 : {Ï„ : Set} {n : â„•} â†’ (eq : EqInst Ï„) â†’ (is : List (Fin n)) â†’ (v : List Ï„) â†’ (h : FinMapMaybe n Ï„) â†’ assoc eq is v â‰¡ just h â†’ map (flip lookupM h) is â‰¡ map just v
 lemma-2 eq []       []       h p = refl
 lemma-2 eq []       (x âˆ· xs) h ()
 lemma-2 eq (x âˆ· xs) []       h ()
-lemma-2 eq (i âˆ· is) (x âˆ· xs) h p = {!!}
+lemma-2 eq (i âˆ· is) (x âˆ· xs) h p = begin
+  map (flip lookupM h) (i âˆ· is)
+    â‰¡âŸ¨ refl âŸ©
+  lookup i h âˆ· map (flip lookupM h) is
+    â‰¡âŸ¨ cong (flip _∷_ (map (flip lookup h) is)) (lemma-lookupM-assoc eq i is x xs h p) âŸ©
+  just x âˆ· map (flip lookupM h) is
+    â‰¡âŸ¨ cong (_∷_ (just x)) (lemma-2 eq is xs h {!!}) âŸ©
+  just x âˆ· map just xs
+    â‰¡âŸ¨ refl âŸ©
+  map just (x âˆ· xs) âˆŽ
 
 idrange : (n : â„•) â†’ List (Fin n)
 idrange n = toList (tabulate id)