Basic math exercises

[lemmy]

Unfinished, random math exercises collected from Specifying Systems, LearnTLA, and elsewhere.

---- MODULE F ----
EXTENDS Naturals, FiniteSets, Sequences

(* 1. Set of all permutations of {"T","L","A"} including repetitions. *)
PermsWithReps(S) ==
    [ 1..Cardinality(S) -> S ]
    
ASSUME 
    PermsWithReps({"T","L","A"}) =
        {<<"T", "T", "T">>, <<"T", "T", "L">>, <<"T", "T", "A">>, 
            <<"T", "L", "T">>, <<"T", "L", "L">>, <<"T", "L", "A">>, 
            <<"T", "A", "T">>, <<"T", "A", "L">>, <<"T", "A", "A">>, 
            <<"L", "T", "T">>, <<"L", "T", "L">>, <<"L", "T", "A">>, 
            <<"L", "L", "T">>, <<"L", "L", "L">>, <<"L", "L", "A">>, 
            <<"L", "A", "T">>, <<"L", "A", "L">>, <<"L", "A", "A">>, 
            <<"A", "T", "T">>, <<"A", "T", "L">>, <<"A", "T", "A">>, 
            <<"A", "L", "T">>, <<"A", "L", "L">>, <<"A", "L", "A">>, 
            <<"A", "A", "T">>, <<"A", "A", "L">>, <<"A", "A", "A">>}

(* 2. All combinations of a two-digit lock. *)
TwoDigitLock ==
    [1..2 -> 0..9]

ASSUME
    /\ (0..9) \X (0..9) = TwoDigitLock
    /\ {<<n,m>> : n,m \in 10..19} \notin SUBSET TwoDigitLock

(* 3. All combinations of a three-digit lock. *)
ThreeDigitLock ==
    [1..3 -> 0..9]

ASSUME
    /\ (0..9) \X (0..9) \X (0..9) = ThreeDigitLock
    /\ {<<n,m,o>> : n,m,o \in 10..19} \notin SUBSET ThreeDigitLock

(* 4. All pairs (including repetitions) of the natural numbers. *)
PairsOfNaturals ==
    [1..2 -> Nat]

ASSUME
    {<<n,m>> : n,m \in 0..100} \subseteq PairsOfNaturals

(* 5. All triples... *)
TriplesOfNaturals ==
    [1..3 -> Nat]

ASSUME
    {<<n,m,o>> : n,m,o \in 0..25} \subseteq TriplesOfNaturals

(* 6. Set of all pairs and triples... *)
PairsAndTriplesOfNaturals ==
    [1..2 -> Nat] \cup [1..3 -> Nat]

ASSUME
    /\ {<<n,m>> : n,m \in 0..100} \subseteq PairsAndTriplesOfNaturals
    /\ {<<n,m,o>> : n,m,o \in 0..25} \subseteq PairsAndTriplesOfNaturals

(* 7. What is the Cardinality of 3. ? *)
Cardinality3 ==
    Cardinality(ThreeDigitLock)

ASSUME Cardinality3 = 1000

(* 8. What is the Cardinality of 6. (PairsAndTriplesOfNaturals) ? *)

--------------------------------------------------------------

(* 9. The range/image/co-domain of a function. *)
Range(f) == { f[x]: x \in DOMAIN f }

ASSUME Range([a |-> 1, b |-> 2, c |-> 3]) = 1..3

(* 10. The permutations of a set _without_ repetition. *)
Perms(S) ==
    { f \in [S -> S] :
        Range(f) = S }

ASSUME Perms({1,2,3}) =
             {<<1, 2, 3>>, <<1, 3, 2>>,
              <<2, 1, 3>>, <<2, 3, 1>>,
              <<3, 1, 2>>, <<3, 2, 1>>}

Perms2(S) ==
    \* If for all w in S there exists a v in S for which f[v]=w,
    \* there can be no repetitions as a consequence. The predicate
    \* demands for all elements of S to be in the range of f.
    { f \in [S -> S] :
        \A w \in S :
            \E v \in S : f[v]=w }

ASSUME Perms2({1,2,3}) =
             {<<1, 2, 3>>, <<1, 3, 2>>,
              <<2, 1, 3>>, <<2, 3, 1>>,
              <<3, 1, 2>>, <<3, 2, 1>>}

Perms3(S) ==
    { f \in [S -> S] :
        \A i,j \in DOMAIN f :
            i # j => f[i] # f[j] }

ASSUME Perms3({1,2,3}) =
             {<<1, 2, 3>>, <<1, 3, 2>>,
              <<2, 1, 3>>, <<2, 3, 1>>,
              <<3, 1, 2>>, <<3, 2, 1>>}

(* 11. Reverse a sequence (a function with domain 1..N). *)
Reverse(seq) ==
    [ i \in 1..Len(seq) |-> seq[Len(seq)+1 - i] ]

ASSUME Reverse(<<1, 2, 3>>) = <<3, 2, 1>>
ASSUME Reverse(<<>>) = <<>>

(* 12. An (infix) operator to quickly define a function mapping an x to a y.  *)
x :> y ==
    [ e \in {x} |-> y ]

ASSUME "x" :> 42 = [ x |-> 42 ]

(* 13. Merge two functions f and g *)
f ++ g ==
  [x \in (DOMAIN f) \cup (DOMAIN g) |-> IF x \in DOMAIN f THEN f[x] ELSE g[x]]

ASSUME <<1,2,3>> ++ [i \in 1..6 |-> i] = <<1, 2, 3, 4, 5, 6>>

(* 14. Advanced!!! Inverse of a function f (swap the domain and range). *)
Inverse(f) ==
   CHOOSE g \in [ Range(f) -> DOMAIN f] : \A s \in DOMAIN f: g[f[s]]=s

ASSUME Inverse(("a" :> 0) ++ ("b" :> 1) ++ ("c" :> 2)) =
              ((0 :> "a") ++ (1 :> "b") ++ (2 :> "c"))
====

-------------------------- MODULE SyntaxExcercises --------------------------
(* The idea is that learners get the spec with the operator _definitions_ replaced 
    with TRUE. A learner can then check their definitions with TLC. *)
EXTENDS Integers, Sequences, TLC

(***************************************************************************)
(* The set of the fibonacci numbers: 1,1,2,3,5,8,13,...                    *)
(***************************************************************************)
MyNat == 1..21 \* perhaps, introduce model definitions right away?
fib[n \in MyNat] == IF n <= 2 THEN 1 ELSE fib[n-1] + fib[n-2]

ASSUME fib[12] = 144

RECURSIVE fibRecurse(_)
fibRecurse(n) == IF n <= 2 THEN 1 ELSE fibRecurse(n - 1) + fibRecurse(n - 2)

ASSUME fibRecurse(12) = 144

(***************************************************************************)
(* The set of fibonacci numbers in the range [10,20).                      *)
(***************************************************************************)
FibSet == { fib[n] : n \in 10..19 }

ASSUME FibSet = {55, 89, 144, 233, 377, 610, 987, 1597, 2584, 4181}

FibSetRecurse == { fibRecurse(n) : n \in 10..19 }

ASSUME FibSetRecurse = {55, 89, 144, 233, 377, 610, 987, 1597, 2584, 4181}

(***************************************************************************)
(* The sequence of fibonacci numbers in the range [10,20).                 *)
(***************************************************************************)
FibSeq == [ e \in 1..10 |-> fib[e+9] ]

ASSUME FibSeq = <<55, 89, 144, 233, 377, 610, 987, 1597, 2584, 4181>>

(***************************************************************************)
(* The range of a function func.                                           *)
(***************************************************************************)
Range(func) == { func[e] : e \in DOMAIN func }

(* Change the 5., 10, 15. element of a function f to "abc", "def" and "ghi" *)
(* TCommit video Minute 12:30 *)
Replace(func, pos, value) == [func EXCEPT ![pos] = value ]

ASSUME [ i \in 1..3 |-> i^2 ] = Replace(Replace(Replace([i \in 1..3 |-> 0], 1, 1), 2, 4), 3, 9)

(***************************************************************************)
(* Excercise page 235/70                                                   *)
(* The sequence obtained by removing the i-th element of seq.              *)
(***************************************************************************)
Remove(seq, i) == [ j \in (1..Len(seq) - 1) |-> (IF j < i THEN seq[j] ELSE seq[j+1]) ]

(***************************************************************************)
(* Excercise page 341/91                                                   *)
(* Recursive definition of the Len(seq) _operator_ with Tail.              *)
(***************************************************************************)
RECURSIVE RecLen(_)
RecLen(seq) == IF seq = <<>> THEN 0
               ELSE 1 + RecLen(Tail(seq))

(***************************************************************************)
(* An alternative variant which treats seq as the function it is and       *)
(* returns the maximum of its DOMAIN which corresponds to the number of    *)
(* elements in seq.                                                        *)
(***************************************************************************)
DomLen(seq) == CHOOSE m \in (DOMAIN seq): (DOMAIN seq) = 1..m

(***************************************************************************)
(* Write an operator that returns the cardinality of a given set.          *)
(***************************************************************************)
RECURSIVE Card(_)
Card(S) == IF S = {} THEN 0 ELSE 1 + Card(S \ {CHOOSE e \in S : TRUE})

ASSUME Card({}) = 0 /\ Card({1,1,2,2,3,3}) = 3

(***************************************************************************)
(* Write an operator that takes a tuple/sequence and, if the tuple is      *)
(* length two, returns the reversed tuple, and otherwise raises an error.  *)
(***************************************************************************)
ReverseOfTwo(seq) == IF Len(seq) = 2 THEN <<seq[2], seq[1]>>
                                     ELSE Assert(FALSE, "")

ASSUME <<4,5>> = ReverseOfTwo(<<5,4>>)

(***************************************************************************)
(* Write an operator that takes a sequence seq and, if the sequence is of  *)
(* uneven length, returns the reversed sequence, otherwise return seq.     *)
(***************************************************************************)
Uneven(n) == n % 2 = 1
Reverse(seq) == [ i \in 1..Len(seq) |-> seq[Len(seq) - (i-1)] ]
ReverseUneven(seq) == IF Uneven(Len(seq)) THEN Reverse(seq)
                                     ELSE seq

ASSUME <<1,2,3,4,5>> = ReverseUneven(<<5,4,3,2,1>>)
ASSUME <<1,2,3,4>> = ReverseUneven(<<1,2,3,4>>)

(* Sum of elements in seq *)

(***************************************************************************)
(* Remove those elements from sequence seq for which Filter(_) holds.      *)
(***************************************************************************)
RECURSIVE Subseq(_,_)
Subseq(Filter(_), seq) == IF seq = <<>>
                          THEN <<>>
                          ELSE IF Filter(Head(seq))
                               THEN <<Head(seq)>> \o Subseq(Filter, Tail(seq))
                               ELSE Subseq(Filter, Tail(seq))

Even(n) == ~Uneven(n)

ASSUME Subseq(Even, <<1,2,1,3,3,6,8,8,23,42>>) = <<2,6,8,8,42>>

SelectSeq2(Test(_), s) ==
  LET S[i \in 0..Len(s)] ==
        IF i = 0 THEN << >> \* As a basis set the s[0] = <<>>
                 ELSE IF Test(s[i]) THEN S[i-1] \o <<s[i]>> \* copy previous value and concat with s[i]
                                    ELSE S[i-1] \* just copy the previous value
  IN S[Len(s)] \* The maximum (last function position) contains the collected sequence


ASSUME Subseq(Even, <<1,2,1,3,3,6,8,8,23,42>>) = SelectSeq2(Even, <<1,2,1,3,3,6,8,8,23,42>>)

(***************************************************************************)
(* Given DOMAIN Tuple is the set of numbers Tuple is defined over, write   *)
(* an operator that gives a set of the values of the Tuple, ie the range.  *)
(***************************************************************************)




(***************************************************************************)
(* Write an operator that takes two sets S1 and S2 and determines if the   *)
(* double of every element in S1 is an element of S2.                      *)
(***************************************************************************)




(***************************************************************************)
(* Given a sequence of sets, write an operator that determines if a given  *)
(* element is found in any of the sequence’s sets.                         *)
(* IE Op("a", <<{"b", "c"}, {"a", "c"}>>) = TRUE.                            *)
(***************************************************************************)


(* Given the (built-in) set Nat (Naturals), create a subset of S whose largest element is 42. *)
(* Hint: Override Nat with 1..1000 on the Advanced Options page of the Model editor. By default *)
(* Nat is represented as a UserValue in TLC. A UserValue is _not_ enumerable, whereas a 1..1000 *)
(* is represented as a (finite) IntervalValue which subsequently can be enumerated. *)
Subset42 == { i \in Nat: i < 43 }

\*ASSUME Subset42 = 1..42


(* The inverse of a function *)
Inverse(f) == 
   CHOOSE g \in [ Range(f) -> DOMAIN f] : \A s \in DOMAIN f: g[f[s]]=s

ASSUME Inverse("a" :> 0 @@ "b" :> 1 @@ "c" :> 2) = (0 :> "a" @@ 1 :> "b" @@ 2 :> "c")

(* Merge two functions f and g *)
Merge(f, g) == 
  [x \in (DOMAIN f) \cup (DOMAIN g) |-> IF x \in DOMAIN f THEN f[x] ELSE g[x]]

ASSUME Merge(<<1,2,3>>, [i \in 1..6 |-> i]) = <<1, 2, 3, 4, 5, 6>>

(* The permutations of a set *)
Perms(S) == 
    {f \in [S -> S] : \A w \in S : \E v \in S : f[v]=w}

ASSUME Perms({1,2,3}) = {<<1, 2, 3>>, <<1, 3, 2>>, <<2, 1, 3>>, <<2, 3, 1>>, <<3, 1, 2>>, <<3, 2, 1>>}
=============================================================================

Graphs

1. With the definitions from the Graphs module, under what conditions
   is <<p>> an element of Path(G)?

2. Find the following values, and use TLC to check your answers.
   (See the file PrintValues.tla in the folder AsynchronousMemory.)

   [i \in Nat |-> i^2][42]

   LET f == [i \in Nat |-> i^2] 
   IN  [f EXCEPT ![42] = 24][42]

   LET f == [i \in Nat |-> i^2] 
   IN  [f EXCEPT ![42] = @ - 24, ![24] = 42][42]
   
   LET f[i \in Nat] == IF i = 0 THEN 0 ELSE f[i-1] + i
   IN  f[42]

   [i \in {"a", "bc", "d"} |-> IF i = "a" THEN 17
                                          ELSE 42].a
   
   [i \in {"a", "bc", "d"} |-> IF i = "a" THEN 17
                                          ELSE 42].bc
   
   [a |-> 17, bc |-> 42, d |-> 42]["a"]

   [a |-> 17, bc |-> 42, d |-> 42]["bc"]

   DOMAIN [a |-> 17, bc |-> 42, d |-> 42]

   LET f(a) == [i \in Nat |-> a^i]
       g    == [j \in Nat |-> f(j)]
   IN  g[2][3]

   LET f(a) == [i \in Nat |-> a^i]
       g    == [j \in Nat |-> f(j)]
   IN  g[2][3]

   [i \in Nat, j \in 1..10 |-> i*j][3,4]

2. Define an operator AF such that, if r is a record, then:
   if r has a "count" field, then AF(r) is r with the count
   field incremented by 1, otherwise, AF(r) is obtained from
   r by adding a "count" field with value 0.

3. Define an operator Reverse, so if s is any sequence, then
   Reverse(s) is sequence s in reverse order. (Hint: you
   don't have to use recursion.) Test it with
   TLC. (Don't forget to check that it works on the empty
   sequence, << >> .)

4. Define a function Sum whose domain is Seq(Nat) such
   that Sum(s) is the sum of the elements of s. (Let
   Sum(<< >>) equal 0.)

5. Determine which of the following formulas are tautologies.

   (F => G) /\ (G => F) <=> (F <=> G)
   (~F /\ ~G) <=> (~F) \/ (~G)
   F => (F => G)
   (F => G) <=> (~G => ~F)
   (F => (G => H)) => ((F => G) => H) 
   (F <=> (G <=> H)) => ((F <=> G) <=> H) 
   (\A x : F /\ G) <=> (\A x : F)  /\ (\A x : G) 
   (\E x : F /\ G) <=> (\E x : F)  /\ (\E x : G) 
   (\A x : F \/ G) <=> (\A x : F)  \/ (\A x : G) 
   (\E x : F \/ G) <=> (\E x : F)  \/ (\E x : G) 

2. Which of the following formulas are valid for all sets S, T, and U?

   (S \subseteq T) <=> (S \cup T = T)
   (S \subseteq T) <=> \A x \in S : x \in T
   (S = T) <=> (S \subseteq T) /\ (T \subseteq S)
   (S \subseteq T) <=> (S \ T = {})
   (S \ T) \cup (T \ S) = (S \cup T) \ (S \cap T)
   (S \ (T \cap U)) = (S \ T) \cup (S \ U)

2. Determine which of the following formulas are temporal
   tautologies. For each one that isn't, give a counterexample.

   (a) <>[]<>F <=> []<>F
   (b) []<>[]F <=> []<>F
   (c) ~[](F \/ G) => <>~F /\ <>~G
   (d) []([]F => G) => ([]F => []G)
   (e) [](F => []G) => ([]F => []G)
   (f) [][A /\ B]_v <=> [][A]_v /\ [][B]_v
   (g) []<><<A /\ B>>_v <=> []<><<A>>_v  /\ []<><<B>>_v 
   (h) [][A => B]_v <=> [][<<A>>_v => B]_v 
   (i) WF_v(A) /\ WF_v(B) => WF_v(A \/ B)
   (j) SF_v(A) /\ SF_v(B) => SF_v(A \/ B)
   (k) ENABLED (A /\ B) => (ENABLED A) /\ (ENABLED B)

1. (a) Use TLC to print all Pythagorean triples <<i,j,k>> with
   i^2 + j^2 = k^2 for natural numbers i,j,k \leq N.
   Start with N=20. (Don't be clever and use the formula for
   generating Pythagorean triples; have TLC to it in a straightforward
   fashion.)

   (b) Next, get TLC to print only essentially Pythagorean triples--that
   is, Pythagorean triples <<i, j, k>> such that i \leq j and i,j, and k
   have no common factor. Try it with N = 50, 100, ... . Why does TLC
   take longer to generate each example as N increases?

https://github.com/tlaplus/Examples/blob/master/specifications/SpecifyingSystems/SimpleMath/README
https://github.com/tlaplus/Examples/blob/master/specifications/SpecifyingSystems/AdvancedExamples/README
https://github.com/tlaplus/Examples/blob/master/specifications/SpecifyingSystems/TLC/README
https://github.com/tlaplus/Examples/blob/master/specifications/SpecifyingSystems/HourClock/README
https://github.com/tlaplus/Examples/blob/master/specifications/SpecifyingSystems/Liveness/README
https://github.com/tlaplus/Examples/blob/master/specifications/SpecifyingSystems/FIFO/README
https://github.com/tlaplus/Examples/blob/master/specifications/SpecifyingSystems/CachingMemory/README
https://github.com/tlaplus/Examples/blob/master/specifications/SpecifyingSystems/RealTime/README

[Alexander-N]

Another option would be to put small exercises like this into Jupyter notebooks, here is an example for the ones from Learn TLA+.

[lemmy]

This issue is primarily about the content and less about the front-end (IDE). That said, why do you think that a Jupyter notebook is a good first-user front-end? My concern is that users would have to learn a new front-end once they move from constant- to state-level TLA+. If this is about a web-experience, the VSCode extension runs on Gitpod and VS/Github codespaces.

[Alexander-N]

Not having to install anything is one point, but I also like the experience of being able to easily check the output of the expression and then seeing the solution. It's true it's yet another tool which a beginner does not necessarily need to know, but for me notebooks are the most convenient way to try out things, I also like that I can document the code with markdown in the same file. It's a matter of preference and familiarity I guess.

About the exercises itself I think they have a good progression from easy to more difficult.