Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

bit-guessing-game: moves stuff to nplib

  • Loading branch information...
commit 9b11adeb704c2ed55a177a1cf21da6a20c39ec2c 1 parent 5b7065f
@np np authored
Showing with 2 additions and 29 deletions.
  1. +2 −29 bit-guessing-game.agda
View
31 bit-guessing-game.agda
@@ -9,7 +9,8 @@ open import Data.Bits
open import flipbased-implem using (Coins; ↺; ⅁) -- ; #⟨_⟩) renaming (count↺ to #⟨_⟩)
open import program-distance using (PrgDist; module PrgDist)
-open import Relation.Binary.PropositionalEquality
+import Relation.Binary.PropositionalEquality as
+openusing (_≡_)
module bit-guessing-game (prgDist : PrgDist) where
@@ -28,31 +29,3 @@ Oracle ca = ∃ (λ (A : GuessAdv ca) → breaks (runGuess⅁ A))
-- Any adversary cannot do better than a random guess.
GuessSec : Coins Set
GuessSec ca = (A : GuessAdv ca) ¬(breaks (runGuess⅁ A))
-
-#ᵇ : Bool
-#ᵇ b = if b then 1 else 0
-
-#ᵇ≤1 : b #ᵇ b ≤ 1
-#ᵇ≤1 true = s≤s z≤n
-#ᵇ≤1 false = z≤n
-
-#-bound : c (f : Bits c Bit) #⟨ f ⟩ ≤ 2^ c
-#-bound zero f = #ᵇ≤1 (f [])
-#-bound (suc c) f = #-bound c (f ∘ 0∷_) +-mono #-bound c (f ∘ 1∷_)
-
-#-∘vnot : c (f : Bits c Bit) #⟨ f ⟩ ≡ #⟨ f ∘ vnot ⟩
-#-∘vnot zero f = refl
-#-∘vnot (suc c) f
- rewrite #-∘vnot c (f ∘ 0∷_)
- | #-∘vnot c (f ∘ 1∷_) = ℕ°.+-comm #⟨ f ∘ 0∷_ ∘ vnot ⟩ _
-
-#-not∘ : c (f : Bits c Bit) #⟨ f ⟩ ≡ 2^ c ∸ #⟨ not ∘ f ⟩
-#-not∘ zero f with f []
-... | true = refl
-... | false = refl
-#-not∘ (suc c) f
- rewrite #-not∘ c (f ∘ 0∷_)
- | #-not∘ c (f ∘ 1∷_) = helper c #⟨ not ∘ f ∘ 0∷_ ⟩ _ (#-bound c (not ∘ f ∘ 0∷_)) (#-bound c (not ∘ f ∘ 1∷_))
- where helper : c x y x ≤ 2^ c y ≤ 2^ c (2^ c ∸ x) + (2^ c ∸ y) ≡ 2^(1 + c) ∸ (x + y)
- helper zero x y x≤ y≤ = {!!}
- helper (suc c₁) x y x≤ y≤ = {!helper c₁ x y ? ?!}
Please sign in to comment.
Something went wrong with that request. Please try again.