Propositional logic and examples

Logic symbols have been used in previous examples, mainly symbols such as \ a, \ e, = >.

\E

E is the initial letter of "exists", which means existence. When writing down \ e x \ in S: P (x) means that there is at least one X in s, making p true. The return value of an expression starting with \ e is Boolean.

\E x \in {1,2} : x > 0  by true
\E x \in {} : x > 0  by false

\E means that there is an element that meets the condition, ~ \ e means that there is no element that meets the condition

\A

The initial letter of "All" of A. when you write \ a x \ in S: P (x) means that P is true for All elements in S. When there is an element that makes p FALSE, the expression returns FALSE.

\A x \in {} : FALSE  = TRUE  

~\A is the opposite of \ a.

=>And < = >

P = > Q means that if P is true, then q is also true. Note: when p is false, Q can also be true. In TLC, P = > q is equivalent to ~ P / Q.

P < = > Q means that both P and Q are true or false. Equivalent to (~ P /\ ~Q) / (P /\ Q)

be careful:=> And <=> As a logical connector, and/\and\/With the same priority, the indentation rules are the same.

example

1. Given a number set S and a number N, define an expression to return whether N elements can be found in S so that the sum of these N elements is 0.

\* The topic can be divided into: 1. From S A subset was found in 2. The length of the subset is N，3，Find the sum of the elements of the subset. 4. There is a subset, and the sum of the elements is equal to 0
\* Found a subset with length N Collection of
Op2(S,n) == { e \in SUBSET S : Cardinality(e) = n }
\* Find the sum of set elements
RECURSIVE Sum(_)
Sum(S) == IF S = {} THEN 0
          ELSE LET x == CHOOSE x \in S : TRUE
                         IN  x + Sum(S \ {x})
\* Expression definition
Sum2Zero(S,N) == \E e \in Op2(S,N) : Sum(e)=0

2. Given an expression Op(,) And a set S, defining an expression that returns whether the expression is exchangeable for all elements in the set S. For example, iscommutative (add (,), {1,2}) = true because Add(1,2) and Add(2,1) are equal.

IsCommutative(Op(_,_), S) == \A x \in S, y \in S : Op(x,y) = Op(y,x)

3. Given a set, returns the maximum number in the set

Max(S) == CHOOSE x \in S : \A y \in S : y <= x 
\* Note that the judgment here must be<= ，Can't be<. Because there is no number bigger than itself.

4. Given a set s, if the element P in the set is a prime number, p-2 is a prime number, or p+2 is a prime number, then p is a twin prime number. Find the largest twin prime in S.

\* 1,Find whether a number is a prime number
IsPrime(x) == x > 1 /\ ~\E d \in 2..(x-1) : x % d = 0
\* 2,Find whether a number is a twin prime number
IsTwinPrime(a) == /\ IsPrime(a) /\ (IsPrime(a-2) \/ IsPrime(a+2))
\* 3,Find the set of twin prime numbers
GetTwinPrime(S) == { a \in S : IsTwinPrime(a)}
\* 4,Find the maximum twin prime
LargestTwinPrime(S) == CHOOSE x \in GetTwinPrime(S): \A y \in GetTwinPrime(S) : x >=y 

5. Returns the largest pair of twin prime numbers in the above set. If a twin prime number is missing, the pair is invalid. For example: {3,5,13} the maximum twin prime pair is < < 3,5 > >, because the twin prime number 11 of 13 is not in the set.

\* 1,The set of pairs of twin prime numbers from the set of twin prime numbers, if a,a+2 If they are all in the collection, they are retained a. 
GetPairTwinPrime(S) == { a \in GetTwinPrime(S): a+2 \in GetTwinPrime(S)}
\* 2,Find the maximum value from the set of twin prime pairs x,that<<x,x+2>>That's what you want
LargestPariTwinPrime(S) == LET x == CHOOSE x \in GetPairTwinPrime(S) : 
						     \A y \in GetPairTwinPrime(S) : x >=y
                           	IN <<x,x+2>>

6. Given the positive integer tuple stockprices, which is used to represent the change of stock value in a day, write an operator to determine the maximum profit that can be obtained, assuming that you can only buy and sell first and buy and sell at most once.

\* You can only buy and sell once. You only need to find the largest difference between the two numbers,
\* You can only buy first and then. You need to subtract the number in front from the number in the back
\* 1,Converts a tuple to a tuple pair, with the first element preceding the second element
\* for example<<1,2,3>> Translate into <<1,2>>,<<1,3>>,<<2,3>>Equivalent to{1} \X {2,3} \union {2} \X {3} 
RECURSIVE newSxS(_)
newSxS(S) == IF Len(S) > 1 
                THEN LET newset== <<{Head(S)},{S[t]:t \in 2..Len(S)}>>
                       IN newset[1] \X newset[2] \union  newSxS(Tail(S))
                      
             ELSE {}
\* Select from a binary set<<x,y>>The one with the largest difference is enough             
MaxProfit(stockprices) == LET sxs == newSxS(stockprices)
                             IN LET res == CHOOSE <<x,y>> \in sxs: 
                                         \A <<a,b>> \in sxs : y-x >= b-a 
                                IN IF res[2]-res[1] > 0 THEN res[2]-res[1]
                                   ELSE 0  \* If there is no profit, do not operate. If you have to buy and sell once, return res[2]-res[1]that will do