Hello,
In TLAPS, it is clear how to decompose a proof based on the connectives. But it is unclear to me how to approach the same in TLA*. I took the following as a trivial example:
lemma
fixes a and b
assumes a1: "⊢ a"
and a2: "⊢ b"
shows "⊢ a ∧ b"
using a1 a2 by auto
This lemma is proved by auto, but there is no direct rule for that. To understand what's happening here, I tried to decompose the proof into atomic steps:
lemma
fixes a and b
assumes a1: "⊢ a"
and a2: "⊢ b"
shows "⊢ a ∧ b"
proof
fix w
show "w ⊨ a ∧ b"
proof -
have "a w" using a1 by rule
moreover have "b w" using a2 by rule
ultimately have "a w ∧ b w" by rule
hence "(∧) (a w) (b w)" by simp
hence "(lift2 (∧) a b) w" using unl_lift2 by simp
hence "w ⊨ lift2 (∧) a b" by simp
thus "w ⊨ a ∧ b" by simp
qed
qed
Is this reasoning the one (approximately) the auto tactic should be used internally?
I don't know if those steps are atomic. I tried to use rule tactics only but failed to find the actual rules. Maybe it's because a lot is done by macro rewriting. My knowledge here is limited.
Maybe you know of good pointers (apart from the theory document) on how to prove things in this theory? I manage to prove simple invariants with the help of the sledgehammer, but I feel quite lost, only having random events of success.
Karolis