ATSLIB/libats/ilist_prf

dataprop
LENGTH (ilist, int) =
  | LENGTHnil(ilist_nil, 0) of ()
  | {x:int}{xs:ilist}{n:nat}
    LENGTHcons(ilist_cons (x, xs), n+1) of LENGTH (xs, n)

length_istot

Synopsis

prfun length_istot {xs:ilist} (): [n:nat] LENGTH (xs, n)

length_isfun

Synopsis

prfun length_isfun {xs:ilist} {n1,n2:int}
  (pf1: LENGTH (xs, n1), pf2: LENGTH (xs, n2)): [n1==n2] void

length_isnat

Synopsis

prfun length_isnat
  {xs:ilist} {n:int} (pf: LENGTH (xs, n)): [n>=0] void

SNOC

Synopsis

dataprop
SNOC (ilist, int, ilist) =
  | {x:int} SNOCnil (ilist_nil, x, ilist_sing (x)) of ()
  | {x0:int} {xs1:ilist} {x:int} {xs2:ilist}
    SNOCcons (ilist_cons (x0, xs1), x, ilist_cons (x0, xs2)) of SNOC (xs1, x, xs2)

snoc_istot

Synopsis

prfun
snoc_istot{xs:ilist}{x:int} (): [xsx:ilist] SNOC (xs, x, xsx)

snoc_isfun

Synopsis

prfun
snoc_isfun{xs:ilist}{x:int}
  {xsx1,xsx2:ilist} (pf1: SNOC (xs, x, xsx1), pf2: SNOC (xs, x, xsx2)): ILISTEQ (xsx1, xsx2)

lemma_snoc_length

Synopsis

prfun
lemma_snoc_length
  {xs:ilist}{x:int}{xsx:ilist}{n:int}
  (pf1: SNOC (xs, x, xsx), pf2: LENGTH (xs, n)): LENGTH (xsx, n+1)

APPEND

Synopsis

dataprop
APPEND (ilist, ilist, ilist) =
  | {ys:ilist} APPENDnil (ilist_nil, ys, ys) of ()
  | {x:int} {xs:ilist} {ys:ilist} {zs:ilist}
    APPENDcons (ilist_cons (x, xs), ys, ilist_cons (x, zs)) of APPEND (xs, ys, zs)

append_istot

Synopsis

prfun
append_istot
  {xs,ys:ilist}(): [zs:ilist] APPEND(xs, ys, zs)

append_isfun

Synopsis

prfun
append_isfun
  {xs,ys:ilist}{zs1,zs2:ilist}
  (pf1: APPEND(xs, ys, zs1), pf2: APPEND(xs, ys, zs2)): ILISTEQ(zs1, zs2)

append_unit_left

Synopsis

prfun
append_unit_left
  {xs:ilist}(): APPEND (ilist_nil, xs, xs)

Description

This function proves that the nil sequence is a left unit for the append operation.

append_unit_right

Synopsis

prfun
append_unit_right
  {xs:ilist}(): APPEND (xs, ilist_nil, xs)

Description

This function proves that the nil sequence is a right unit for the append operation.

append_sing

Synopsis

prfun
append_sing
{x:int}{xs:ilist}
(
// argumentless
) : APPEND (ilist_sing(x), xs, ilist_cons (x, xs))

lemma_append_length

Synopsis

prfun
lemma_append_length
  {xs1,xs2:ilist}
  {xs:ilist}
  {n1,n2:int} (
  pf: APPEND (xs1, xs2, xs)
, pf1len: LENGTH (xs1, n1), pf2len: LENGTH (xs2, n2)
) : LENGTH (xs, n1+n2) // end of [lemma_append_length]

Description

Given two sequences xs1 and xs2, this function proves that the length of the concatenation of xs1 and xs2 equals the length of xs1 plus the length of xs2.

lemma_append_snoc

Synopsis

prfun
lemma_append_snoc
  {xs1:ilist}
  {x:int}
  {xs2:ilist}
  {xs1x:ilist}
  {res:ilist}
(
  pf1: APPEND(xs1, ilist_cons(x, xs2), res), pf2: SNOC (xs1, x, xs1x)
) : APPEND (xs1x, xs2, res) // end-of-prfun

lemma_append_assoc

Synopsis

prfun
lemma_append_assoc
  {xs1,xs2,xs3:ilist}
  {xs12,xs23:ilist}
  {xs12_3,xs1_23:ilist}
(
  pf12: APPEND (xs1, xs2, xs12), pf23: APPEND (xs2, xs3, xs23)
, pf12_3: APPEND (xs12, xs3, xs12_3), pf1_23: APPEND (xs1, xs23, xs1_23)
) : ILISTEQ (xs12_3, xs1_23) // end of [lemma_append_assoc]

Description

This function proves that the append operation on sequences is associative.

REVAPP

Synopsis

dataprop
REVAPP(ilist, ilist, ilist) =
  | {ys:ilist}
    REVAPPnil (ilist_nil, ys, ys) of ()
  | {x:int}{xs:ilist}{ys:ilist}{zs:ilist}
    REVAPPcons (ilist_cons (x, xs), ys, zs) of REVAPP (xs, ilist_cons (x, ys), zs)

revapp_istot

Synopsis

prfun
revapp_istot
  {xs,ys:ilist} (): [zs:ilist] REVAPP (xs, ys, zs)

revapp_isfun

Synopsis

prfun
revapp_isfun
  {xs,ys:ilist}{zs1,zs2:ilist}
  (pf1: REVAPP (xs, ys, zs1), pf2: REVAPP (xs, ys, zs2)): ILISTEQ (zs1, zs2)

lemma_revapp_length

Synopsis

prfun
lemma_revapp_length
  {xs,ys,zs:ilist}{m,n:int} (
  pf: REVAPP (xs, ys, zs), pf1len: LENGTH (xs, m), pf2len: LENGTH (ys, n)
) : LENGTH (zs, m+n) // end of [lemma_revapp_length]

NTH

Synopsis

dataprop
NTH (x0:int, ilist, int) =
  | {xs:ilist}
    NTHbas (x0, ilist_cons (x0, xs), 0)
  | {x1:int}{xs:ilist}{n:nat}
    NTHind (x0, ilist_cons (x1, xs), n+1) of NTH (x0, xs, n)

RNTH

Synopsis

dataprop
RNTH (x0:int, ilist, int) =
  | {xs:ilist}{n:nat}
    RNTHbas (x0, ilist_cons (x0, xs), n) of LENGTH (xs, n)
  | {x1:int}{xs:ilist}{n:nat}
    RNTHind (x0, ilist_cons (x1, xs), n) of RNTH (x0, xs, n)

lemma_rnth_nth

Synopsis

prfun
lemma_rnth_nth
  {x:int}{xs:ilist}
  {n:int}{i:int | i < n}
  (pf1: RNTH (x, xs, i), pf2: LENGTH (xs, n)): NTH (x, xs, n-1-i)

lemma_nth_rnth

Synopsis

prfun
lemma_nth_rnth
  {x:int}{xs:ilist}
  {n:int}{i:int | i < n}
  (pf1: NTH (x, xs, i), pf2: LENGTH (xs, n)): RNTH (x, xs, n-1-i)

lemma_nth_ilisteq

Synopsis

prfun
lemma_nth_ilisteq
  {xs1,xs2:ilist}{n:int}
(
  pf1len: LENGTH (xs1, n), pf2len: LENGTH (xs2, n)
, fpf: {x:int}{i:int | i < n} NTH (x, xs1, i) -> NTH (x, xs2, i)
) : ILISTEQ (xs1, xs2) // end of [lemma_nth_ilisteq]

lemma1_revapp_nth

Synopsis

prfun
lemma1_revapp_nth
  {xs,ys,zs:ilist}
  {n:int}{x:int}{i:int} (
  REVAPP (xs, ys, zs), LENGTH (xs, n), NTH (x, ys, i)
) : NTH (x, zs, n+i) // end of [lemma1_revapp_nth]

lemma2_revapp_nth

Synopsis

prfun
lemma2_revapp_nth
  {xs,ys,zs:ilist}
  {n:int}{x:int}{i:int} (
  REVAPP (xs, ys, zs), LENGTH (xs, n), NTH (x, xs, i)
) : NTH (x, zs, n-1-i) // end of [lemma2_revapp_nth]

lemma_reverse_nth

Synopsis

prfun
lemma_reverse_nth
  {xs,ys:ilist}
  {n:int}{x:int}{i:int}
(
  pf: REVERSE(xs, ys), pf2: LENGTH(xs, n), pf3: NTH(x, xs, i)
) : NTH (x, ys, n-1-i) // end of [lemma_reverse_nth]

lemma_reverse_symm

Synopsis

prfun
lemma_reverse_symm{xs,ys:ilist}(REVERSE(xs, ys)): REVERSE(ys, xs)

Description

This function proves that the REVERSE relation is symmetric.

INSERT

Synopsis

dataprop
INSERT (
  xi:int, ilist, int, ilist
) = // INSERT (xi, xs, i, ys): insert xi in xs at i = ys
  | {xs:ilist}
    INSERTbas (
      xi, xs, 0, ilist_cons (xi, xs)
    ) of () // end of [INSERTbas]
  | {x:int}{xs:ilist}{i:nat}{ys:ilist}
    INSERTind (
      xi, ilist_cons (x, xs), i+1, ilist_cons (x, ys)
    ) of INSERT (xi, xs, i, ys) // end of [INSERTind]

lemma_insert_length

Synopsis

prfun lemma_insert_length
  {xi:int}{xs:ilist}{i:int}{ys:ilist}{n:int}
  (pf1: INSERT (xi, xs, i, ys), pf2: LENGTH (xs, n)): LENGTH (ys, n+1)

lemma_insert_nth_at

Synopsis

prfun
lemma_insert_nth_at
  {xi:int}{xs:ilist}{i:int}{ys:ilist}
  (pf: INSERT (xi, xs, i, ys)): NTH (xi, ys, i)

lemma_insert_nth_lt

Synopsis

prfun
lemma_insert_nth_lt
  {xi:int}{xs:ilist}{i:int}{ys:ilist}{x:int}{j:int | j < i}
  (pf1: INSERT (xi, xs, i, ys), pf2: NTH (x, xs, j)): NTH (x, ys, j)

lemma_insert_nth_gte

Synopsis

prfun
lemma_insert_nth_gte
  {xi:int}{xs:ilist}{i:int}{ys:ilist}{x:int}{j:int | j >= i}
  (pf1: INSERT (xi, xs, i, ys), pf2: NTH (x, xs, j)): NTH (x, ys, j+1)

lemma_nth_insert

Synopsis

prfun
lemma_nth_insert
  {x:int}{xs:ilist}{n:int}
  (pf: NTH (x, xs, n)): [ys:ilist] INSERT (x, ys, n, xs)

UPDATE

Synopsis

dataprop
UPDATE (
  yi: int, ilist, int, ilist
) = // UPDATE
  | {x0:int}{xs:ilist}
    UPDATEbas (
      yi, ilist_cons (x0, xs), 0, ilist_cons (yi, xs)
    ) of () // end of [UPDATEbas]
  | {x:int}{xs:ilist}{i:nat}{ys:ilist}
    UPDATEind (
      yi, ilist_cons (x, xs), i+1, ilist_cons (x, ys)
    ) of UPDATE (yi, xs, i, ys) // end of [UPDATEind]

INTERCHANGE

Synopsis

absprop
INTERCHANGE
(
  xs:ilist, i:int, j:int, ys:ilist
) (* INTERCHANGE *)

PERMUTE

Synopsis

absprop
PERMUTE
(
  xs1:ilist, xs2:ilist
) (* PERMUTE *)

LTB

Synopsis

absprop LTB
  (x: int, xs: ilist) // [x] is a strict lower bound for [xs]

LTEB

Synopsis

absprop LTEB
  (x: int, xs: ilist) // [x] is a lower bound for [xs]

ISORD

Synopsis

dataprop
ISORD (ilist) =
  | ISORDnil(ilist_nil) of ()
  | {x:int} {xs:ilist}
    ISORDcons(ilist_cons(x, xs)) of (ISORD(xs), LTEB(x, xs))

SORT

Synopsis

absprop
SORT (xs:ilist, ys:ilist)

This page is created with ATS by Hongwei Xi and also maintained by Hongwei Xi.