From 2f01bfa8f4580eb0777a66946c62dd5af6f2867c Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Sun, 22 Jan 2012 16:40:58 +0100 Subject: attempt to prove lemma-1 In order to prove lemma-1 we first show a lemma-insert-same to show that inserting the same pair twice does not change the FinMapMaye. lemma-1 still has two goals. In the first goal agda doesn't accept "is-just (f i)". Why? The second goal is to be shown as absurd. --- Bidir.agda | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/Bidir.agda b/Bidir.agda index 28534a2..736b910 100644 --- a/Bidir.agda +++ b/Bidir.agda @@ -10,6 +10,7 @@ open import Data.Product hiding (zip ; map) open import Function open import Relation.Nullary open import Relation.Binary.Core +open import Relation.Binary.PropositionalEquality module FinMap where @@ -58,9 +59,26 @@ assoc _ _ _ = nothing generate : {A : Set} {n : ℕ} → (Fin n → A) → List (Fin n) → FinMapMaybe n A generate f is = fromAscList (zip is (map f is)) +data Is-Just {A : Set} : (Maybe A) → Set where + is-just : (x : A) → Is-Just (just x) + +the : {A : Set} {t : Maybe A} → Is-Just t → A +the (is-just x) = x + +lemma-insert-same : {τ : Set} {n : ℕ} → (m : FinMapMaybe n τ) → (f : Fin n) → (a? : Is-Just (lookup f m)) → m ≡ insert f (the a?) m +lemma-insert-same [] () a? +lemma-insert-same (.(just x) ∷ xs) zero (is-just x) = refl +lemma-insert-same (x ∷ xs) (suc f′) a? = cong (_∷_ x) (lemma-insert-same xs f′ a?) + lemma-1 : {τ : Set} {n : ℕ} → (eq : (x y : τ) → Dec (x ≡ y)) → (f : Fin n → τ) → (is : List (Fin n)) → assoc eq is (map f is) ≡ just (generate f is) lemma-1 eq f [] = refl -lemma-1 eq f (i ∷ is′) = {!!} +lemma-1 eq f (i ∷ is′) with assoc eq is′ (map f is′) | generate f is′ | lemma-1 eq f is′ +lemma-1 eq f (i ∷ is′) | nothing | _ | () +lemma-1 eq f (i ∷ is′) | just m | .m | refl with lookup i m +lemma-1 eq f (i ∷ is′) | just m | .m | refl | nothing = refl +lemma-1 eq f (i ∷ is′) | just m | .m | refl | just x with eq (f i) x +lemma-1 eq f (i ∷ is′) | just m | .m | refl | just .(f i) | yes refl = cong just (lemma-insert-same m i {!!}) +lemma-1 eq f (i ∷ is′) | just m | .m | refl | just x | no ¬p = {!!} idrange : (n : ℕ) → List (Fin n) idrange n = toList (tabulate id) -- cgit v1.2.3