module IntRNG where open import Logic.Base open import Logic.Identity open import Logic.ChainReasoning open import Data.Bool open import Data.Nat using (Nat; suc; zero) renaming ( _<_ to _<'_ ) open import Data.Integer module ChainR = Logic.ChainReasoning.Poly.Homogenous _≡_ (\x -> refl) (\x y z -> trans) open ChainR _↑_ : Int -> Int -> Int a ↑ b = (a < b) => b ! a lemmaT : {A : Set}{cond : Bool}{x y : A} -> cond ≡ true -> if cond then x else y ≡ x lemmaT refl = refl lemmaF : {A : Set}{cond : Bool}{x y : A} -> cond ≡ false -> if cond then x else y ≡ y lemmaF refl = refl dec : (b : Bool) -> (b ≡ true) \/ (b ≡ false) dec true = \/-IL refl dec false = \/-IR refl -- JK: unavoidable partiality? ↑assoc : (a : Int) -> (b : Int) -> (c : Int) -> ((a ↑ b) ↑ c) ≡ (a ↑ (b ↑ c)) ↑assoc a b c with dec (a < b) | dec (a < c) | dec (b < c) ... | \/-IL a (a ↑ b) ↑ c === b ↑ c by cong (\x -> x ↑ c) (lemmaT a a ↑ (b ↑ c) === a ↑ c by cong (\x -> a ↑ x) (lemmaT b (a ↑ b) ↑ c === b ↑ c by cong (\x -> x ↑ c) (lemmaT a a ↑ (b ↑ c) === a ↑ b by cong (\x -> a ↑ x) (lemmaF b≮c) === b by lemmaT a (a ↑ b) ↑ c === b ↑ c by cong (\x -> x ↑ c) (lemmaT a a ↑ (b ↑ c) === a ↑ b by cong (\x -> a ↑ x) (lemmaF b≮c) === b by lemmaT a (a ↑ b) ↑ c === a ↑ c by cong (\x -> x ↑ c) (lemmaF a≮b) === c by (lemmaT a a ↑ (b ↑ c) === a ↑ c by cong (\x -> a ↑ x) (lemmaT b (a ↑ b) ↑ c === a ↑ c by cong (\x -> x ↑ c) (lemmaF a≮b) === a by (lemmaF a≮c) === a ↑ (b ↑ c) by sym ( chain> a ↑ (b ↑ c) === a ↑ c by cong (\x -> a ↑ x) (lemmaT b (a ↑ b) ↑ c === a ↑ c by cong (\x -> x ↑ c) (lemmaF a≮b) === a by (lemmaF a≮c) === a ↑ (b ↑ c) by sym ( chain> a ↑ (b ↑ c) === a ↑ b by cong (\x -> a ↑ x) (lemmaF b≮c) === a by lemmaF a≮b ) 0+a≡a : {a : Int} -> pos 0 + a ≡ a 0+a≡a {pos a} = refl 0+a≡a {neg 0} = refl 0+a≡a {neg (suc n)} = refl +distr↑ : (a : Int) -> (b : Int) -> (c : Int) -> (a + (b ↑ c)) ≡ ((a + b) ↑ (a + c)) +distr↑ (pos 0) b c = chain> pos 0 + (b ↑ c) === b ↑ c by 0+a≡a === ((pos 0 + b) ↑ c) by cong (\d -> d ↑ c) (sym 0+a≡a) === ((pos 0 + b) ↑ (pos 0 + c)) by cong (\d -> (pos 0 + b) ↑ d) (sym 0+a≡a)