github-repos/tla-plus
1
0
Fork 0
mirror of https://github.com/pingcap/tla-plus.git synced 2024-12-27 13:00:31 +08:00
Code Issues Packages Projects Releases Wiki Activity

Fix silly error in Coq proof.

Browse Source
This commit is contained in:
foreverbell 2018-01-21 20:45:05 +08:00
parent 5aee4f13c6
commit 7bf22a8151
No known key found for this signature in database
GPG Key ID: 92D5B279E66E4E51
1 changed files with 4 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
TwoPC/Coq/TwoPC.v
View File

@ -142,7 +142,7 @@ Inductive StateMultiStep : State -> State -> Prop :=
StateMultiStep state state StateMultiStep state state
| StateMultiStep1 : | StateMultiStep1 :
forall state state1 state2, forall state state1 state2,
StateMultiStep state1 state2 -> StateStep state1 state2 ->
StateMultiStep state state1 -> StateMultiStep state state1 ->
StateMultiStep state state2. StateMultiStep state state2.
@ -275,7 +275,9 @@ Lemma Safety' :
Invariant state -> Invariant state ->
Invariant state'. Invariant state'.
Proof. Proof.
induction 1; crush. induction 1; intros.
+ auto.
+ eapply StateStepKeepsInvariant; eauto.
Qed. Qed.
Theorem Safety : Theorem Safety :