crypto-agda/flipbased-running.agda at master · demtech/crypto-agda · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
open import Function
open import Data.Nat.NP
open import Data.Fin using (Fin)
open import Relation.Binary.NP
import Relation.Binary.PropositionalEquality as ≡
open ≡ using (_≗_; _≡_)

open import Data.Bits
open import Data.Bits.Count
import flipbased
import flipbased-counting

module flipbased-running
   (↺ : ∀ {a} → ℕ → Set a → Set a)
   (toss : ↺ 1 Bit)
   (return↺ : ∀ {n a} {A : Set a} → A → ↺ n A)
   (map↺ : ∀ {n a b} {A : Set a} {B : Set b} → (A → B) → ↺ n A → ↺ n B)
   (join↺ : ∀ {n₁ n₂ a} {A : Set a} → ↺ n₁ (↺ n₂ A) → ↺ (n₁ + n₂) A)
   (run↺ : ∀ {n a} {A : Set a} → ↺ n A → Bits n → A)
 where

open flipbased ↺ toss return↺ map↺ join↺

count↺ᶠ : ∀ {c} → EXP c → Fin (suc (2^ c))
count↺ᶠ f = #⟨ run↺ f ⟩ᶠ

count↺ : ∀ {c} → EXP c → ℕ
count↺ f = #⟨ run↺ f ⟩

open flipbased-counting ↺ toss return↺ map↺ join↺ count↺

infix 4 _≗↺_ _≗⅁?_

_≗↺_ : ∀ {c a} {A : Set a} (f g : ↺ c A) → Set a
f ≗↺ g = run↺ f ≗ run↺ g

_≗⅁?_ : ∀ {c} (g₀ g₁ : ⅁? c) → Set
g₀ ≗⅁? g₁ = ∀ b → g₀ b ≗↺ g₁ b

Reversible-≗⅁? : ∀ {c} (g : ⅁? c) → Set
Reversible-≗⅁? g = g ≗⅁? g ∘ not

≗⇒≈↺ : ∀ {c} {f g : EXP c} → f ≗↺ g → f ≈↺ g
≗⇒≈↺ {f = f} {g} = ≗-cong-# (run↺ f) (run↺ g)

≗⇒≋↺ : ∀ {c} {f g : EXP c} → f ≗↺ g → f ≋↺ g
≗⇒≋↺ eq rewrite ≗⇒≈↺ eq = ≡.refl


difference-lemma↺ : ∀ {n}(A B F : EXP n)
  → #⟨ |not| (run↺ F) |∧| run↺ A ⟩ ≡ #⟨ |not| (run↺ F) |∧| run↺ B ⟩
  → dist #⟨ run↺ A ⟩ #⟨ run↺ B ⟩ ≤ #⟨ run↺ F ⟩
difference-lemma↺ A B F = difference-lemma (run↺ A) (run↺ B) (run↺ F)


module ≗↺ {n} {a} {A : Set a} where
  setoid : Setoid _ _
  setoid = record { Carrier = C; _≈_ = ℛ; isEquivalence = isEquivalence }
      where
        C : Set _
        C = ↺ n A

        ℛ : C → C → Set _
        ℛ = _≗↺_

        refl : Reflexive ℛ
        refl _ = ≡.refl

        sym : Symmetric ℛ
        sym p x = ≡.sym (p x)

        trans : Transitive ℛ
        trans p q x = ≡.trans (p x) (q x)

        isEquivalence : IsEquivalence ℛ
        isEquivalence = record { refl = refl; sym = sym; trans = trans }

  module Reasoning = Setoid-Reasoning setoid
  open Setoid setoid public

module ≗⅁? {n} where
  setoid : Setoid _ _
  setoid = record { Carrier = C; _≈_ = ℛ; isEquivalence = isEquivalence }
      where
        C : Set _
        C = ⅁? n

        ℛ : C → C → Set _
        ℛ = _≗⅁?_

        refl : Reflexive ℛ
        refl _ _ = ≡.refl

        sym : Symmetric ℛ
        sym p b R = ≡.sym (p b R)

        trans : Transitive ℛ
        trans p q b R = ≡.trans (p b R) (q b R)

        isEquivalence : IsEquivalence ℛ
        isEquivalence = record { refl = refl; sym = sym; trans = trans }

  module Reasoning = Setoid-Reasoning setoid
  open Setoid setoid public

≋↺-cong-≗↺ : ∀ {c c'} {f g : EXP c} {f' g' : EXP c'} → f ≗↺ g → f' ≗↺ g' → f ≋↺ f' → g ≋↺ g'
≋↺-cong-≗↺ f≗g f'≗g' f≈f' rewrite ≗⇒≈↺ f≗g | ≗⇒≈↺ f'≗g' = f≈f'

≈↺-cong-≗↺ : ∀ {n} {f g f' g' : EXP n} → f ≗↺ g → f' ≗↺ g' → f ≈↺ f' → g ≈↺ g'
≈↺-cong-≗↺ f≗g f'≗g' f≈f' rewrite ≗⇒≈↺ f≗g | ≗⇒≈↺ f'≗g' = f≈f'

Reversible-≗⅁?⇒Reversible⅁? : ∀ {c} (g : ⅁? c) → Reversible-≗⅁? g → Reversible⅁? g
Reversible-≗⅁?⇒Reversible⅁? g g≈g∘not = ≗⇒≈↺ ∘ g≈g∘not