{-# OPTIONS_HADDOCK not-home #-}
module Morley.Michelson.Optimizer.Internal.Proofs
( module Morley.Michelson.Optimizer.Internal.Proofs
) where
import Prelude hiding (EQ, GT, LT)
import Data.Constraint (Dict(..), (\\))
import Data.Type.Equality ((:~:)(..))
import Morley.Michelson.Typed (SingT(..), T(..))
import Morley.Michelson.Typed.Instr.Constraints
import Morley.Util.Peano
import Morley.Util.PeanoNatural
import Morley.Util.StubbedProof
import Morley.Util.Type
dropNDropNProof
:: forall inp out out' n m.
( out ~ Drop n inp, IsLongerOrSameLength inp n ~ 'True
, out' ~ Drop m out, IsLongerOrSameLength out m ~ 'True)
=> PeanoNatural n -> PeanoNatural m
-> Dict (Drop (AddPeano n m) inp ~ out', IsLongerOrSameLength inp (AddPeano n m) ~ 'True)
dropNDropNProof :: forall {k} (inp :: [k]) (out :: [k]) (out' :: [k]) (n :: Peano)
(m :: Peano).
(out ~ Drop n inp, IsLongerOrSameLength inp n ~ 'True,
out' ~ Drop m out, IsLongerOrSameLength out m ~ 'True) =>
PeanoNatural n
-> PeanoNatural m
-> Dict
(Drop (AddPeano n m) inp ~ out',
IsLongerOrSameLength inp (AddPeano n m) ~ 'True)
dropNDropNProof PeanoNatural n
Zero PeanoNatural m
_ = Dict (out' ~ out', 'True ~ 'True)
Dict
(Drop (AddPeano n m) inp ~ out',
IsLongerOrSameLength inp (AddPeano n m) ~ 'True)
forall (a :: Constraint). a => Dict a
Dict
dropNDropNProof (Succ PeanoNatural m
n) PeanoNatural m
m = Dict (out' ~ out', 'True ~ 'True)
Dict
(Drop ('S (AddPeano m m)) inp ~ out',
IsLongerOrSameLength inp ('S (AddPeano m m)) ~ 'True)
(Drop ('S (AddPeano m m)) inp ~ out') =>
Dict
(Drop ('S (AddPeano m m)) inp ~ out',
IsLongerOrSameLength inp ('S (AddPeano m m)) ~ 'True)
forall (a :: Constraint). a => Dict a
Dict
((Drop ('S (AddPeano m m)) inp ~ out') =>
Dict
(Drop ('S (AddPeano m m)) inp ~ out',
IsLongerOrSameLength inp ('S (AddPeano m m)) ~ 'True))
-> (Drop ('S (AddPeano m m)) inp :~: out')
-> Dict
(Drop ('S (AddPeano m m)) inp ~ out',
IsLongerOrSameLength inp ('S (AddPeano m m)) ~ 'True)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [k]) (b :: [k]). (Stubbed => a :~: b) -> a :~: b
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof @(Drop (AddPeano n m) inp) @out' case forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [k]). KList xs
forall {k} (xs :: [k]). KList xs
assumeKnown @inp of
KCons Proxy x
_ (Proxy xs
_ :: Proxy xs) -> out' :~: out'
Drop (AddPeano m m) xs :~: out'
(Drop (AddPeano m m) xs ~ out', 'True ~ 'True) =>
Drop (AddPeano m m) xs :~: out'
forall {k} (a :: k). a :~: a
Refl ((Drop (AddPeano m m) xs ~ out', 'True ~ 'True) =>
Drop (AddPeano m m) xs :~: out')
-> Dict (Drop (AddPeano m m) xs ~ out', 'True ~ 'True)
-> Drop (AddPeano m m) xs :~: out'
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (inp :: [k]) (out :: [k]) (out' :: [k]) (n :: Peano)
(m :: Peano).
(out ~ Drop n inp, IsLongerOrSameLength inp n ~ 'True,
out' ~ Drop m out, IsLongerOrSameLength out m ~ 'True) =>
PeanoNatural n
-> PeanoNatural m
-> Dict
(Drop (AddPeano n m) inp ~ out',
IsLongerOrSameLength inp (AddPeano n m) ~ 'True)
forall {k} (inp :: [k]) (out :: [k]) (out' :: [k]) (n :: Peano)
(m :: Peano).
(out ~ Drop n inp, IsLongerOrSameLength inp n ~ 'True,
out' ~ Drop m out, IsLongerOrSameLength out m ~ 'True) =>
PeanoNatural n
-> PeanoNatural m
-> Dict
(Drop (AddPeano n m) inp ~ out',
IsLongerOrSameLength inp (AddPeano n m) ~ 'True)
dropNDropNProof @xs @out @out' PeanoNatural m
n PeanoNatural m
m
((IsLongerOrSameLength inp ('S (AddPeano m m)) ~ 'True) =>
Dict
(Drop ('S (AddPeano m m)) inp ~ out',
IsLongerOrSameLength inp ('S (AddPeano m m)) ~ 'True))
-> (IsLongerOrSameLength inp ('S (AddPeano m m)) :~: 'True)
-> Dict
(Drop ('S (AddPeano m m)) inp ~ out',
IsLongerOrSameLength inp ('S (AddPeano m m)) ~ 'True)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: Bool) (b :: Bool). (Stubbed => a :~: b) -> a :~: b
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof @(IsLongerOrSameLength inp (AddPeano n m)) @'True case forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [k]). KList xs
forall {k} (xs :: [k]). KList xs
assumeKnown @inp of
KCons Proxy x
_ (Proxy xs
_ :: Proxy xs) -> 'True :~: 'True
IsLongerOrSameLength xs (AddPeano m m) :~: 'True
(Drop (AddPeano m m) xs ~ out',
IsLongerOrSameLength xs (AddPeano m m) ~ 'True) =>
IsLongerOrSameLength xs (AddPeano m m) :~: 'True
forall {k} (a :: k). a :~: a
Refl ((Drop (AddPeano m m) xs ~ out',
IsLongerOrSameLength xs (AddPeano m m) ~ 'True) =>
IsLongerOrSameLength xs (AddPeano m m) :~: 'True)
-> Dict
(Drop (AddPeano m m) xs ~ out',
IsLongerOrSameLength xs (AddPeano m m) ~ 'True)
-> IsLongerOrSameLength xs (AddPeano m m) :~: 'True
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (inp :: [k]) (out :: [k]) (out' :: [k]) (n :: Peano)
(m :: Peano).
(out ~ Drop n inp, IsLongerOrSameLength inp n ~ 'True,
out' ~ Drop m out, IsLongerOrSameLength out m ~ 'True) =>
PeanoNatural n
-> PeanoNatural m
-> Dict
(Drop (AddPeano n m) inp ~ out',
IsLongerOrSameLength inp (AddPeano n m) ~ 'True)
forall {k} (inp :: [k]) (out :: [k]) (out' :: [k]) (n :: Peano)
(m :: Peano).
(out ~ Drop n inp, IsLongerOrSameLength inp n ~ 'True,
out' ~ Drop m out, IsLongerOrSameLength out m ~ 'True) =>
PeanoNatural n
-> PeanoNatural m
-> Dict
(Drop (AddPeano n m) inp ~ out',
IsLongerOrSameLength inp (AddPeano n m) ~ 'True)
dropNDropNProof @xs @out @out' PeanoNatural m
n PeanoNatural m
m
unpairN2isUnpairProof
:: forall inp out pair s. (inp ~ pair : s, out ~ UnpairN ('S ('S 'Z)) pair ++ s
, ConstraintUnpairN (ToPeano 2) pair)
=> inp :~: PairN (ToPeano 2) out
unpairN2isUnpairProof :: forall (inp :: [T]) (out :: [T]) (pair :: T) (s :: [T]).
(inp ~ (pair : s), out ~ (UnpairN ('S ('S 'Z)) pair ++ s),
ConstraintUnpairN (ToPeano 2) pair) =>
inp :~: PairN (ToPeano 2) out
unpairN2isUnpairProof = (Stubbed =>
inp
:~: ('TPair (Head out) (Head (Tail out)) : Drop ('S ('S 'Z)) out))
-> inp
:~: ('TPair (Head out) (Head (Tail out)) : Drop ('S ('S 'Z)) out)
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof case forall {k} (x :: k). Stubbed => Sing x
forall {k} (x :: k). Sing x
forall (x :: T). Sing x
assumeSing @pair of
STPair{} -> case forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [T]). KList xs
forall {k} (xs :: [k]). KList xs
assumeKnown @out of
KCons{} -> inp :~: inp
inp
:~: ('TPair (Head out) (Head (Tail out)) : Drop ('S ('S 'Z)) out)
forall {k} (a :: k). a :~: a
Refl
where Dict (ConstraintUnpairN (ToPeano 2) pair)
_ = forall (a :: Constraint). a => Dict a
Dict @(ConstraintUnpairN (ToPeano 2) pair)
unpairNisUnpairDipUnpairNProof
:: forall inp out pair s n. (inp ~ pair : s, out ~ UnpairN ('S n) pair ++ s, ConstraintUnpairN ('S n) pair)
=> PeanoNatural n -> pair :~: RightComb (LazyTake ('S n) out)
unpairNisUnpairDipUnpairNProof :: forall (inp :: [T]) (out :: [T]) (pair :: T) (s :: [T])
(n :: Peano).
(inp ~ (pair : s), out ~ (UnpairN ('S n) pair ++ s),
ConstraintUnpairN ('S n) pair) =>
PeanoNatural n -> pair :~: RightComb (LazyTake ('S n) out)
unpairNisUnpairDipUnpairNProof PeanoNatural n
n = (Stubbed => pair :~: RightComb (Head out : LazyTake n (Tail out)))
-> pair :~: RightComb (Head out : LazyTake n (Tail out))
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof case forall {k} (x :: k). Stubbed => Sing x
forall {k} (x :: k). Sing x
forall (x :: T). Sing x
assumeSing @pair of
STPair Sing n1
_ (SingT n2
_ :: SingT r) -> case PeanoNatural n
n of
Succ PeanoNatural m
Zero -> pair :~: pair
pair :~: RightComb (Head out : LazyTake n (Tail out))
forall {k} (a :: k). a :~: a
Refl
Succ m :: PeanoNatural m
m@Succ{} -> pair :~: pair
pair :~: RightComb (Head out : LazyTake n (Tail out))
(n2
~ RightComb
(Head (UnpairN ('S ('S m)) n2 ++ s)
: Head (Tail (UnpairN ('S ('S m)) n2 ++ s))
: LazyTake m (Tail (Tail (UnpairN ('S ('S m)) n2 ++ s))))) =>
pair :~: RightComb (Head out : LazyTake n (Tail out))
forall {k} (a :: k). a :~: a
Refl ((n2
~ RightComb
(Head (UnpairN ('S ('S m)) n2 ++ s)
: Head (Tail (UnpairN ('S ('S m)) n2 ++ s))
: LazyTake m (Tail (Tail (UnpairN ('S ('S m)) n2 ++ s))))) =>
pair :~: RightComb (Head out : LazyTake n (Tail out)))
-> (n2
:~: RightComb
(Head (UnpairN ('S ('S m)) n2 ++ s)
: Head (Tail (UnpairN ('S ('S m)) n2 ++ s))
: LazyTake m (Tail (Tail (UnpairN ('S ('S m)) n2 ++ s)))))
-> pair :~: RightComb (Head out : LazyTake n (Tail out))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (inp :: [T]) (out :: [T]) (pair :: T) (s :: [T])
(n :: Peano).
(inp ~ (pair : s), out ~ (UnpairN ('S n) pair ++ s),
ConstraintUnpairN ('S n) pair) =>
PeanoNatural n -> pair :~: RightComb (LazyTake ('S n) out)
unpairNisUnpairDipUnpairNProof @(r : s) @(Tail out) PeanoNatural m
m
where Dict (inp ~ (pair : s))
_ = forall (a :: Constraint). a => Dict a
Dict @(inp ~ pair : s)
dipPairNPairIsPairNProof
:: forall inp n. ( n >= ToPeano 2 ~ 'True, IsLongerOrSameLength (Tail inp) n ~ 'True
, inp ~ Head inp : Tail inp)
=> PeanoNatural n
-> PairN ('S n) inp :~: 'TPair (Head inp) (RightComb (LazyTake n (Tail inp))) : Drop n (Tail inp)
dipPairNPairIsPairNProof :: forall (inp :: [T]) (n :: Peano).
((n >= ToPeano 2) ~ 'True,
IsLongerOrSameLength (Tail inp) n ~ 'True,
inp ~ (Head inp : Tail inp)) =>
PeanoNatural n
-> PairN ('S n) inp
:~: ('TPair (Head inp) (RightComb (LazyTake n (Tail inp)))
: Drop n (Tail inp))
dipPairNPairIsPairNProof PeanoNatural n
n = (Stubbed =>
(RightComb (Head inp : LazyTake n (Tail inp)) : Drop n (Tail inp))
:~: ('TPair (Head inp) (RightComb (LazyTake n (Tail inp)))
: Drop n (Tail inp)))
-> (RightComb (Head inp : LazyTake n (Tail inp))
: Drop n (Tail inp))
:~: ('TPair (Head inp) (RightComb (LazyTake n (Tail inp)))
: Drop n (Tail inp))
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof case (PeanoNatural n
n, forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [T]). KList xs
forall {k} (xs :: [k]). KList xs
assumeKnown @inp) of
(Succ Succ{}, KCons{}) -> (RightComb (Head inp : LazyTake n (Tail inp)) : Drop n (Tail inp))
:~: ('TPair (Head inp) (RightComb (LazyTake n (Tail inp)))
: Drop n (Tail inp))
(RightComb (Head inp : LazyTake n (Tail inp)) : Drop n (Tail inp))
:~: (RightComb (Head inp : LazyTake n (Tail inp))
: Drop n (Tail inp))
forall {k} (a :: k). a :~: a
Refl
where Dict
((n >= ToPeano 2) ~ 'True,
IsLongerOrSameLength (Tail inp) n ~ 'True)
_ = forall (a :: Constraint). a => Dict a
Dict @(n >= ToPeano 2 ~ 'True, IsLongerOrSameLength (Tail inp) n ~ 'True)
pairN2isPairProof
:: forall inp. (IsLongerOrSameLength inp ('S ('S 'Z)) ~ 'True)
=> inp :~: Head inp : Head (Tail inp) : Drop ('S ('S 'Z)) inp
pairN2isPairProof :: forall {k} (inp :: [k]).
(IsLongerOrSameLength inp ('S ('S 'Z)) ~ 'True) =>
inp :~: (Head inp : Head (Tail inp) : Drop ('S ('S 'Z)) inp)
pairN2isPairProof = (Stubbed =>
inp :~: (Head inp : Head (Tail inp) : Drop ('S ('S 'Z)) inp))
-> inp :~: (Head inp : Head (Tail inp) : Drop ('S ('S 'Z)) inp)
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof case forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [k]). KList xs
forall {k} (xs :: [k]). KList xs
assumeKnown @inp of
KCons Proxy x
_ (Proxy xs
_ :: Proxy xs) -> case forall (l :: [k]). KnownList l => KList l
forall {k} (l :: [k]). KnownList l => KList l
klist @xs of
KCons {} -> inp :~: inp
inp :~: (Head inp : Head (Tail inp) : Drop ('S ('S 'Z)) inp)
forall {k} (a :: k). a :~: a
Refl
where Dict (IsLongerOrSameLength inp ('S ('S 'Z)) ~ 'True)
_ = forall (a :: Constraint). a => Dict a
Dict @(IsLongerOrSameLength inp ('S ('S 'Z)) ~ 'True)
unconsListProof
:: forall inp n. (IsLongerOrSameLength inp ('S n) ~ 'True)
=> PeanoNatural n -> inp :~: Head inp : Tail inp
unconsListProof :: forall {a} (inp :: [a]) (n :: Peano).
(IsLongerOrSameLength inp ('S n) ~ 'True) =>
PeanoNatural n -> inp :~: (Head inp : Tail inp)
unconsListProof PeanoNatural n
_ = (Stubbed => inp :~: (Head inp : Tail inp))
-> inp :~: (Head inp : Tail inp)
forall {k} (a :: k) (b :: k). (Stubbed => a :~: b) -> a :~: b
stubProof case forall {k} (xs :: [k]). Stubbed => KList xs
forall (xs :: [a]). KList xs
forall {k} (xs :: [k]). KList xs
assumeKnown @inp of
KCons{} -> inp :~: inp
inp :~: (Head inp : Tail inp)
forall {k} (a :: k). a :~: a
Refl
where Dict (IsLongerOrSameLength inp ('S n) ~ 'True)
_ = forall (a :: Constraint). a => Dict a
Dict @(IsLongerOrSameLength inp ('S n) ~ 'True)