potan

Хеш-функция

hash: Data -> CheckSum
hashProp1: (x:Data) -> (y:Data) -> (hash x = hash y) -> (x = y)
hashProp2: (rev: CheckSum -> Data) -> (p: (d: Data -> rev (hash d) = d)) -> Void

Симметричное шифрование

encode: Key -> Data -> Encrypted
decode: Key -> Encrypted -> Data
cryptProp1: (k: Key) -> (d: Encrypted) -> (encode k (decode k d)) = d
cryptProp2: (k: Key) -> (d: Data) -> (decode k (encode k d)) = d
cryptProt3: ((d:Data, e:Encrypt) -> (k: Key ** (encode k d = e))) -> Void
cryptProp4: (((d1:Data, e1:Encrypt) -> (d2:Data, e2:Encrypt) -> Either (k: Key -> encode k d1 = e1 -> encode k d2 = e2) (k: Key -> encode k d1 = e1 -> encode k d2 = e2 -> Void)

zelych

  Inductive last (a: A): list A -> Prop :=
  | last_one: last a (a :: nil)
  | last_many: forall (l: list A) (x: A), last a l -> last a (x :: l).

  Lemma last_nil: forall (a: A), last a nil -> False.