show a stronger lemma-checkInsert-restrict
[~helmut/bidiragda.git] / CheckInsert.agda
index 9302fc7..47af215 100644 (file)
@@ -58,16 +58,10 @@ lemma-checkInsert-wrong i x m x' d refl | .(just x') with deq x x'
 lemma-checkInsert-wrong i x m x' d refl | .(just x') | yes q = contradiction q d
 lemma-checkInsert-wrong i x m x' d refl | .(just x') | no ¬q = refl
 
-lemma-checkInsert-restrict : {n : â„•} â†’ (f : Fin n â†’ Carrier) â†’ (i : Fin n) â†’ (is : List (Fin n)) â†’ Setoid._≈_ (MaybeSetoid (vecIsSetoid (MaybeSetoid A.setoid) n)) (checkInsert i (f i) (restrict f is)) (just (restrict f (i âˆ· is)))
+lemma-checkInsert-restrict : {n : â„•} â†’ (f : Fin n â†’ Carrier) â†’ (i : Fin n) â†’ (is : List (Fin n)) â†’ checkInsert i (f i) (restrict f is) â‰¡ just (restrict f (i âˆ· is))
 lemma-checkInsert-restrict f i is with checkInsert i (f i) (restrict f is) | insertionresult i (f i) (restrict f is)
-lemma-checkInsert-restrict f i is | ._ | same x fi≈x p = MaybeEq.just (lemma-insert-same _ i (f i) (begin
-  lookupM i (restrict f is)
-    â‰¡âŸ¨ p âŸ©
-  just x
-    â‰ˆâŸ¨ MaybeEq.just (Setoid.sym A.setoid fi≈x) âŸ©
-  just (f i) âˆŽ))
-  where open EqR (MaybeSetoid A.setoid)
-lemma-checkInsert-restrict f i is | ._ | new _ = Setoid.refl (MaybeSetoid (vecIsSetoid (MaybeSetoid A.setoid) _))
+lemma-checkInsert-restrict f i is | ._ | same x fi≈x p = cong just (lemma-insert-same _ i (f i) (trans p (cong just (sym (lemma-lookupM-restrict i f is x p)))))
+lemma-checkInsert-restrict f i is | ._ | new _ = refl
 lemma-checkInsert-restrict f i is | ._ | wrong x fi≉x p = contradiction (IsPreorder.reflexive (Setoid.isPreorder A.setoid) (lemma-lookupM-restrict i f is x p)) fi≉x
 
 lemma-lookupM-checkInsert : {n : â„•} â†’ (i j : Fin n) â†’ (x y : Carrier) â†’ (h h' : FinMapMaybe n Carrier) â†’ lookupM i h â‰¡ just x â†’ checkInsert j y h â‰¡ just h' â†’ lookupM i h' â‰¡ just x