Add two theorems about transitivity of Append/Tail and IsInjective.

Author: lemmy

.github/workflows/main.yml

@@ -16,6 +16,14 @@ jobs:
     - name: Get current date
       id: date
       run: echo "::set-output name=date::$(date +'%Y%m%d%H%M')"
+    - name: Get TLAPS
+      run: wget https://tla.msr-inria.inria.fr/tlaps/dist/1.4.4/tlaps-1.4.4-x86_64-linux-gnu-inst.bin
+    - name: Install TLAPS
+      run: |
+        chmod +x tlaps-1.4.4-x86_64-linux-gnu-inst.bin
+        ./tlaps-1.4.4-x86_64-linux-gnu-inst.bin -d tlaps
+    - name: Run TLAPS
+      run: tlaps/bin/tlapm --cleanfp -I tlaps/ -I modules/ modules/SequencesExtTheorems_proofs.tla
     - name: Build with Ant
       run: ant -noinput -buildfile build.xml -Dtimestamp=${{steps.date.outputs.date}}
     - name: Create Release

modules/SequencesExtTheorems.tla

@@ -0,0 +1,22 @@
+------------------------ MODULE SequencesExtTheorems ------------------------
+LOCAL INSTANCE SequencesExt
+LOCAL INSTANCE Sequences
+LOCAL INSTANCE Functions
+
+LEMMA AppendTransitivityIsInjective
+     == ASSUME NEW S, NEW seq \in Seq(S),
+               IsInjective(seq),
+               NEW elt \in S,
+               elt \notin Range(seq)
+        PROVE IsInjective(Append(seq, elt))
+
+LEMMA TailTransitivityIsInjective
+     == ASSUME NEW S, NEW seq \in Seq(S),
+               seq # <<>>,
+               IsInjective(seq)
+        PROVE IsInjective(Tail(seq))
+
+=============================================================================
+\* Modification History
+\* Last modified Thu Feb 27 11:38:41 PST 2020 by markus
+\* Created Tue Feb 25 20:49:08 PST 2020 by markus

modules/SequencesExtTheorems_proofs.tla

@@ -0,0 +1,49 @@
+--------------------- MODULE SequencesExtTheorems_proofs ---------------------
+LOCAL INSTANCE SequencesExt
+LOCAL INSTANCE Sequences
+LOCAL INSTANCE Naturals
+LOCAL INSTANCE Functions
+LOCAL INSTANCE TLAPS
+
+LEMMA AppendTransitivityIsInjective \* With TLAPS 1.4.4+ (3ed0cde)
+     == ASSUME NEW S, NEW seq \in Seq(S),
+               IsInjective(seq),
+               NEW elt \in S,
+               elt \notin Range(seq)
+        PROVE IsInjective(Append(seq, elt))
+BY DEF IsInjective, Range
+
+LEMMA TailTransitivityIsInjective \* With TLAPS 1.4.3
+     == ASSUME NEW S, NEW seq \in Seq(S),
+               seq # <<>>,
+               IsInjective(seq)
+        PROVE IsInjective(Tail(seq))
+  <1> DEFINE ts == Tail(seq)
+  <1>1. IsInjective(ts) 
+    <2> SUFFICES ASSUME NEW i \in DOMAIN ts, NEW j \in DOMAIN ts,
+                        ts[i] = ts[j]
+                 PROVE  i = j
+      BY DEF IsInjective
+    <2>1. ts[i] = seq[i + 1] /\ ts[j] = seq[j + 1] 
+      BY SMT
+    <2>2. 1..Len(ts) = 1..Len(seq)-1
+      BY SMT
+    <2>3. 1..Len(ts) \subseteq 1..Len(seq)
+      BY SMT
+    <2>4. DOMAIN ts = 1..Len(seq)-1
+      BY SMT
+    <2>5. DOMAIN seq = 1..Len(seq)
+      BY SMT
+    <2>6. \A r, s \in 1..Len(seq): (seq[r] = seq[s]) => (r = s)
+      BY Isa, <2>5 DEF IsInjective
+    <2>7. seq \in [1..Len(seq) -> Range(seq)]
+      BY Isa, <2>5 DEF Range
+    <2>8. DOMAIN ts \subseteq DOMAIN seq
+      BY Isa, <2>2, <2>3, <2>4, <2>7
+    <2>9. QED BY <2>1, <2>2, <2>3, <2>5, <2>6, <2>7, <2>8 DEF IsInjective
+  <1>2. QED BY <1>1
+
+=============================================================================
+\* Modification History
+\* Last modified Thu Feb 27 11:44:49 PST 2020 by markus
+\* Created Thu Feb 27 11:27:48 PST 2020 by markus