diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2012-01-26 11:45:06 +0100 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2012-01-26 11:45:06 +0100 |
| commit | 024635440449c8249cdff9d5637fcb7e02b5d293 (patch) | |
| tree | ac6e83c2ca80c1b41bb24154274b0d4f4dc54b6c /Bidir.agda | |
| parent | 90d67cb200626cdb0eb4ead36278af8119dfe661 (diff) | |
| download | bidiragda-024635440449c8249cdff9d5637fcb7e02b5d293.tar.gz | |
complete the yes part of lemma-checkInsert-generate using inspect
Diffstat (limited to 'Bidir.agda')
| -rw-r--r-- | Bidir.agda | 11 |
1 files changed, 6 insertions, 5 deletions
@@ -74,11 +74,12 @@ lemma-insert-same (.(just a) ∷ xs) zero a refl = refl lemma-insert-same (x ∷ xs) (suc i) a p = cong (_∷_ x) (lemma-insert-same xs i a p) lemma-checkInsert-generate : {τ : Set} {n : ℕ} → (eq : EqInst τ) → (f : Fin n → τ) → (i : Fin n) → (is : List (Fin n)) → checkInsert eq i (f i) (generate f is) ≡ just (generate f (i ∷ is)) -lemma-checkInsert-generate eq f i is with lookupM i (generate f is) -lemma-checkInsert-generate eq f i is | nothing = refl -lemma-checkInsert-generate eq f i is | just x with eq (f i) x -lemma-checkInsert-generate eq f i is | just .(f i) | yes refl = cong just (lemma-insert-same (generate f is) i (f i) {!!}) -lemma-checkInsert-generate eq f i is | just x | no ¬p = {!!} +lemma-checkInsert-generate eq f i is with lookupM i (generate f is) | inspect (lookupM i) (generate f is) +lemma-checkInsert-generate eq f i is | nothing | _ = refl +lemma-checkInsert-generate eq f i is | just x | _ with eq (f i) x +lemma-checkInsert-generate eq f i is | just .(f i) | Reveal_is_.[_] p | yes refl = cong just (lemma-insert-same (generate f is) i (f i) (sym p)) +lemma-checkInsert-generate eq f i is | just x | _ | no ¬p = {!!} + lemma-1 : {τ : Set} {n : ℕ} → (eq : EqInst τ) → (f : Fin n → τ) → (is : List (Fin n)) → assoc eq is (map f is) ≡ just (generate f is) lemma-1 eq f [] = refl |