Mercurial > hg > Members > atton > agda-proofs
changeset 35:bf667ec8cba4
Set with constraint
| author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 02 Jan 2017 03:30:02 +0000 |
| parents | d9b394c245c5 |
| children | f0759cb39d37 |
| files | sandbox/SetWithConstraint.agda |
| diffstat | 1 files changed, 13 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- a/sandbox/SetWithConstraint.agda Mon Jan 02 03:17:18 2017 +0000 +++ b/sandbox/SetWithConstraint.agda Mon Jan 02 03:30:02 2017 +0000 @@ -60,3 +60,16 @@ ≡⟨ refl ⟩ suc (suc (length s)) ∎ + +insert-length-exists : (k : String) (n : ℕ )(s : MySet ℕ) {hasKey : elem k s ≡ true} {nonEmpty : s ≢ empty} + -> length (insert (k , n) s) ≡ (length s) +insert-length-exists _ _ empty {nonEmpty = n} = ⊥-elim (n refl) +insert-length-exists k n (cons x s) {hasKey = h} = begin + length (insert (k , n) (cons x s)) + ≡⟨ refl ⟩ + length (insert' (elem k (cons x s)) (k , n) (cons x s)) + ≡⟨ cong (\e -> length (insert' e (k , n) (cons x s))) h ⟩ + length (insert' true (k , n) (cons x s)) + ≡⟨ refl ⟩ + length (cons x s) + ∎