All relations are part of the sterling:stdLib reasoning module. Then, for example, the full name of the relation listed below as lookup is sterling:stdLib:lookup.
Module sterling:stdLib /* Common judgments for lists */ /*Find the first item associated with the key*/ Fixed Judgment lookup : [(Key, Item)] Key Item /*Holds if no items are associated with the key*/ Fixed Judgment no_lookup : [(Key, Item)] Key /*Holds if the item is in the list*/ Fixed Judgment mem : Item [Item] /*Holds if the item is NOT in the list*/ Fixed Judgment not_mem : Item [Item] /*Splits the list into the item plus the rest of the list around it: select A Rest L*/ Fixed Judgment select : Item [Item] [Item] /*Holds if the second list contains everything in the first list Permits duplication in the subset (e.g. subset [A, A] [A] holds)*/ Fixed Judgment subset : [A] [A] /*Holds if the first list contains everything in the second list and the second list contains everything in the first list*/ Fixed Judgment permutation : [A] [A] /*Count how many times an item occurs in a list*/ Fixed Judgment count : A [A] int /*Domain of a list (first element of each pair)*/ Fixed Judgment domain : [(A, B)] [A] /*Values of a pair list (second element of each pair)*/ Fixed Judgment values : [(A, B)] [B] /*Combine two lists into a list of pairs*/ Fixed Judgment zip : [A] [B] [(A, B)] /*Drop the first N elements of a list: drop N L Rest*/ Fixed Judgment drop : int [A] [A] /*Take the first N elements of a list: take N L FirstN*/ Fixed Judgment take : int [A] [A] /*Build a range list, inclusive*/ Fixed Judgment range : int int [int] /* Rules */ =================================== [Lkp-Here] lookup (Key, Value)::Rest Key Value K != Key lookup Rest Key Value ============================= [Lkp-Later] lookup (K, V)::Rest Key Value ================ [NLkp-Nil] no_lookup [] Key K != Key no_lookup Rest Key ========================== [NLkp-Cons] no_lookup (K, V)::Rest Key =================== [Mem-Here] mem Item Item::Rest mem Item Rest ================ [Mem-Later] mem Item I::Rest =============== [NMem-Nil] not_mem Item [] I != Item not_mem Item Rest ==================== [NMem-Cons] not_mem Item I::Rest =========================== [Slct-First] select Item Rest Item::Rest select Item L1 L2 ======================= [Slct-Later] select Item I::L1 I::L2 =========== [Sbst-Nil] subset [] L mem X Supset subset Rest Supset ===================== [Sbst-Cons] subset X::Rest Supset ================= [Prm-Nil] permutation [] [] select A L2 L permutation Rest L2 ======================= [Prm-Cons] permutation (A::Rest) L ============ [Cnt-Nil] count X [] 0 count X Rest N 1 + N = N1 ================== [Cnt-ConsEq] count X X::Rest N1 X != Y count X Rest N ================= [Cnt-ConsNEq] count X Y::Rest N ============ [Dmn-Nil] domain [] [] domain Rest DRest ============================ [Dmn-Cons] domain (A, B)::Rest A::DRest ============ [Vals-Nil] values [] [] values Rest VRest ============================ [Vals-Cons] values (A, B)::Rest B::VRest ============ [Zip-Nil] zip [] [] [] zip ARest BRest Rest ================================== [Zip-Cons] zip A::ARest B::BRest (A, B)::Rest ========== [Drop-0] drop 0 L L 1 + N1 = N drop N1 L R ============= [Drop-Step] drop N X::L R =========== [Take-0] take 0 L [] 1 + N1 = N take N1 L F ================ [Take-Step] take N X::L X::F Low > High ================= [Range-End] range Low High [] Low <= High 1 + Low = PlusOne range PlusOne High Rest ======================== [Range-Step] range Low High Low::Rest
The Sterling standard library module also includes an Extensibella reasoning module with properties about its relations. These properties are all proven to hold.
lookup_unique [Key, Value] : forall L (Key : Key) (Value2 : Value) (Value1 : Value), lookup L Key Value1 -> lookup L Key Value2 -> Value1 = Value2
no_lookup [Key, Value] : forall L (Key : Key) (Value : Value), no_lookup L Key -> lookup L Key Value -> false
lookup_eq_or_not [Key, Value] : forall L (A : Key) (B : Key) (VB : Value) (VA : Value), lookup L A VA -> lookup L B VB -> A = B \/ (A = B -> false)
lookup_mem [Key, Value] : forall L (Key : Key) (Value : Value), lookup L Key Value -> mem (Key, Value) L
no_lookup_mem [Key, Value] : forall L (Key : Key) (Value : Value), no_lookup L Key -> mem (Key, Value) L -> false
no_lookup_mem_pair [Key, Value] : forall L (P : pair Key Value) K, no_lookup L K -> mem P L -> exists X Y, P = (X, Y)
lookup_select [Key, Value] : forall L (Key : Key) (Value : Value), lookup L Key Value -> exists L', select (Key, Value) L' L
no_lookup_select [Key, Value] : forall L (Key : Key) (Value : Value) R, no_lookup L Key -> select (Key, Value) R L -> false
select_lookup [Key, Value] : forall L (Key : Key) (K : Key) (Value : Value) (V : Value) R, lookup L K V -> select (Key, Value) R L -> (K = Key -> false) -> lookup R K V
no_lookup_after_select_before [Key, Value] : forall (Key : Key) (K : Key) (V : Value) Rest L, no_lookup Rest Key -> select (K, V) Rest L -> (K = Key -> false) -> no_lookup L Key
no_lookup_before_select_after [Key, Value] : forall (Key : Key) (P : pair Key Value) Rest L, no_lookup L Key -> select P Rest L -> no_lookup Rest Key
lookup_after_select_before [Key, Value] : forall (K : Key) (Key : Key) (V : Value) (Value : Value) L R, lookup R K V -> select (Key, Value) R L -> (K = Key -> false) -> lookup L K V
mem_select [Item] : forall L (X : Item), mem X L -> exists L', select X L' L
select_mem [Item] : forall L (X : Item) L', select X L' L -> mem X L
mem_after_select_before [Item] : forall L L' (Y : Item) (X : Item), select X L' L -> mem Y L' -> mem Y L
mem_before_select_after [Item] : forall L L' (Y : Item) (X : Item), select X L' L -> mem Y L -> (X = Y -> false) -> mem Y L'
select_comm [Item] : forall L Rest Rest' (Y : Item) (X : Item), select X Rest L -> select Y Rest' Rest -> exists R, select Y R L /\ select X Rest' R
mem_append_left [A] : forall L1 L2 L (A : A), mem A L1 -> L1 ++ L2 = L -> mem A L
mem_append_right [A] : forall L1 L2 L (A : A), mem A L2 -> L1 ++ L2 = L -> mem A L
mem_append [A] : forall L1 L2 L (A : A), mem A L -> L1 ++ L2 = L -> mem A L1 \/ mem A L2
not_mem [A] : forall (A : A) L, not_mem A L -> mem A L -> false
not_mem_select [A] : forall L (A : A) L', not_mem A L -> select A L' L -> false
not_mem_after_select_before [A] : forall L L' (Y : A) (X : A), select X L' L -> not_mem Y L' -> (X = Y -> false) -> not_mem Y L
not_mem_before_select_after [A] : forall L L' (Y : A) (X : A), select X L' L -> not_mem Y L -> not_mem Y L'
not_mem_append [A] : forall L1 L2 L (A : A), not_mem A L1 -> not_mem A L2 -> L1 ++ L2 = L -> not_mem A L
not_mem_append_back [A] : forall L1 L2 L (A : A), not_mem A L -> L1 ++ L2 = L -> not_mem A L1 /\ not_mem A L2
permutation_mem [Item] : forall (L : list Item) (M : list Item) I, permutation L M -> mem I L -> mem I M
perm_lemma [Item] : forall A B B' (X : Item), permutation B' A -> select X B' B -> permutation B (X::A)
permutation_symmetric [Item] : forall (M : list Item) (L : list Item), permutation L M -> permutation M L
no_lookup_permutation [Key, Value] : forall (L : list (pair Key Value)) (P : list (pair Key Value)) (Key : Key), no_lookup L Key -> permutation L P -> no_lookup P Key
count_is_integer [Item] : forall (I : Item) L N, count I L N -> is_integer N
count_geq_0 [Item] : forall (I : Item) L N, count I L N -> N >= 0
select_count [Item] : forall (I : Item) L Rest N N', count I L N -> select I Rest L -> N - 1 = N' -> count I Rest N'
count_select [Item] : forall (I : Item) L Rest N' N, count I Rest N' -> select I Rest L -> 1 + N' = N -> count I L N
select_count_neq [Item] : forall (I : Item) (J : Item) L Rest N, count I L N -> select J Rest L -> (I = J -> false) -> count I Rest N
count_select_neq [Item] : forall (I : Item) (J : Item) L Rest N, count I Rest N -> select J Rest L -> (I = J -> false) -> count I L N
count_unique [Item] : forall (I : Item) NA NB L, count I L NA -> count I L NB -> NA = NB
count_mem [Item] : forall (I : Item) N L, count I L N -> N > 0 -> mem I L
count_not_mem [Item] : forall (I : Item) L, count I L 0 -> mem I L -> false
count_greater_0 [Item] : forall (I : Item) L N, count I (I::L) N -> N > 0
subset_mem [A] : forall (Sub : list A) (Sup : list A) A, subset Sub Sup -> mem A Sub -> mem A Sup
subset_trans [A] : forall (B : list A) (C : list A) (A : list A), subset A B -> subset B C -> subset A C
subset_add_right [A] : forall Sub Sup (A : A), subset Sub Sup -> subset Sub (A::Sup)
permutation_counts [Item] : forall L P (I : Item) NL NP, permutation L P -> count I L NL -> count I P NP -> NL = NP
domain_mem [A, B] : forall L (A : A) (B : B) D, mem (A, B) L -> domain L D -> mem A D
mem_domain [A, B] : forall (L : list (pair A B)) A D, domain L D -> mem A D -> exists B, mem (A, B) L
domain_select [A, B] : forall (L : list (pair A B)) LRest A B D, domain L D -> select (A, B) LRest L -> exists DRest, select A DRest D /\ domain LRest DRest
domain_unique [A, B] : forall (L : list (pair A B)) DA DB, domain L DA -> domain L DB -> DA = DB
values_mem [A, B] : forall L (A : A) (B : B) V, mem (A, B) L -> values L V -> mem B V
values_select [A, B] : forall (L : list (pair A B)) LRest A B V, values L V -> select (A, B) LRest L -> exists VRest, select B VRest V /\ values LRest VRest
values_unique [A, B] : forall (L : list (pair A B)) VA VB, values L VA -> values L VB -> VA = VB
zip_unique [A, B] : forall (L1 : list A) (L2 : list B) LA LB, zip L1 L2 LA -> zip L1 L2 LB -> LA = LB
zip_mem_after [A, B] : forall LA LB (A : A) (B : B) Z, zip LA LB Z -> mem (A, B) Z -> mem A LA /\ mem B LB
zip_mem_before1 [A, B] : forall LA (LB : list B) (A : A) Z, zip LA LB Z -> mem A LA -> exists B, mem (A, B) Z
zip_mem_before2 [A, B] : forall (LA : list A) LB (B : B) Z, zip LA LB Z -> mem B LB -> exists A, mem (A, B) Z
drop_is_integer [A] : forall N (R : list A) (L : list A), drop N L R -> is_integer N
drop_geq_0 [A] : forall N (R : list A) (L : list A), drop N L R -> N >= 0
drop_unique [A] : forall N (RA : list A) (RB : list A) (L : list A), drop N L RA -> drop N L RB -> RA = RB
append_drop [A] : forall N (L2 : list A) (L : list A) (L1 : list A), L1 ++ L2 = L -> length L1 N -> drop N L L2
take_is_integer [A] : forall N (F : list A) (L : list A), take N L F -> is_integer N
take_geq_0 [A] : forall N (F : list A) (L : list A), take N L F -> N >= 0
take_unique [A] : forall N (RA : list A) (RB : list A) (L : list A), take N L RA -> take N L RB -> RA = RB
take_length [A] : forall N (R : list A) (L : list A), take N L R -> length R N
append_take [A] : forall N (L2 : list A) (L : list A) (L1 : list A), L1 ++ L2 = L -> length L1 N -> take N L L1
range_is : forall Low High R, is_integer Low -> range Low High R -> is_list is_integer R
is_list_int_mem : forall L (X : integer), is_list is_integer L -> mem X L -> is_integer X
range_low_lesseq : forall Low High R X, is_integer Low -> range Low High R -> mem X R -> Low <= X
range_high_lesseq : forall Low High R X, is_integer Low -> range Low High R -> mem X R -> X <= High
in_range : forall Low High R X, is_integer Low -> is_integer X -> range Low High R -> Low <= X -> X <= High -> mem X R
range_unique : forall Low High R1 R2, range Low High R1 -> range Low High R2 -> R1 = R2
range_smaller_exists : forall Low High R Low',
is_integer Low -> is_integer Low' -> range Low High R -> Low < Low' -> exists R',
range Low' High R'
range_subset : forall Low Low' High R R', is_integer Low -> is_integer Low' -> range Low High R -> range Low' High R' -> Low < Low' -> subset R' R
range_select_unique : forall Low High R X Rest Rest', is_integer Low -> range Low High R -> select X Rest R -> select X Rest' R -> Rest = Rest'
range_exists : forall Low High, is_integer Low -> is_integer High -> exists R, range Low High R