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)
+  ∎