[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Karolis Petrauskas <k.petrauskas@xxxxxxxxx>*Date*: Thu, 28 Dec 2023 00:57:33 +0200

Hello,

I'm trying to use TLA*, a generalization of TLA formalized in Isabelle/HOL (https://www.isa-afp.org/entries/TLA.html). The main confusion, I believe, is how to work with the lifted expressions.

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

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

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

You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAFteovKyRWofbZ%3DDroh57HC8jDYbw_OSFJKL9EStQ-HOJ4Nseg%40mail.gmail.com.

**Follow-Ups**:**Re: [tlaplus] Trying to understand lifting in Isabelle/HOL TLA****From:*Stephan Merz

- Prev by Date:
**[tlaplus] Where does assert go in Euclid Algorithm of Chapter 4.5** - Next by Date:
**Re: [tlaplus] Trying to understand lifting in Isabelle/HOL TLA*** - Previous by thread:
**[tlaplus] Re: Where does assert go in Euclid Algorithm of Chapter 4.5** - Next by thread:
**Re: [tlaplus] Trying to understand lifting in Isabelle/HOL TLA*** - Index(es):