# Semantics verification of an LTL fragment logic

I am a beginner to Isabelle and I went over the proof documentation. I am trying to implement a fragment logic of LTL over finite intervals and finite traces called MLTL, the syntax and semantics can be found here in Section 2.

I used the formal proof for LTL on the archive as a basis (find it here). The MLTL fragment is more simple, as a trace is finite. I used the following code in Isabelle to implement it:

theory MLTL
imports Main
begin

datatype (formula_mltl: 'a ) mltl =
True_mltl                               ("true")
| False_mltl                              ("false")
| Prop_mltl 'a                            ("prop'(_')")
| Not_mltl "'a mltl"                      ("not _" [85] 85)
| And_mltl "'a mltl" "'a mltl"            ("_ and _" [82,82] 81)
| Or_mltl "'a mltl" "'a mltl"             ("_ or _" [81,81] 80)
| Implies_mltl "'a mltl" "'a mltl"        ("_ implies _" [81,81] 80 )
| Future_mltl  "nat" "nat" "'a mltl"                     ("F [_  , _] _ " [88] 87 )
| Global_mltl  "nat" "nat"  "'a mltl"                   ("G [_ , _ ] _" [88] 87 )
| Until_mltl "'a mltl"   "nat" "nat"   "'a mltl"         ("_ U [_ ,_ ] _" [84,84] 83 )
(*Need to define suffix*)

primrec semantics_mltl :: "['a set list, 'a mltl] ⇒ bool" ("_ ⊨  _" [81,81] 80 )
where
"π ⊨ true = True"
| "π ⊨ false = False"
| "π ⊨ prop(q) = (q ∈ hd π )"
| "π ⊨ not φ = (¬(π ⊨ φ))"
| "π ⊨ φ and ψ = (π ⊨ φ ∧ π ⊨ ψ)"
| "π ⊨ (φ or ψ) = ((π ⊨ φ) ∨ (π ⊨ ψ))"
| "π ⊨ (φ implies ψ) = ((π⊨ φ) ⟶ (π⊨ ψ))"
| "π ⊨ (F [lb,ub] φ) = (∃j::nat∈{lb..<ub+1}.  ( drop j π) ⊨ φ )"
| "π ⊨ (G[lb,ub] φ) = (∀j::nat∈{lb..<ub+1}.  ( drop j π) ⊨ φ ) "
| "π ⊨ (φ U[lb,ub] ψ) = (∃j∈{lb..<ub+1}. ( ((drop j π) ⊨ ψ) ∧ (∀k<j. (drop k π) ⊨ φ)))"

lemma l1:
"([set [p,q],set [r,s],set [s,t]]) ⊨ (G[1,2] (prop(s)))"
unfolding MLTL.semantics_mltl.simps


Towards the end in lemma l1, I try to verify that the semantics is implemented correctly. So I check for the satisfaction of MLTL formula G[1,2] prop(s), for a trace, [{p,q},{r,s},{s,t}]. The first and second elements of the list are sets that contain s, so I know that the lemma holds true. Question: How do I prove the lemma using Isabelle?

Simp rules for recursive definitions are supposed to be transparent, so you shouldn't need to invoke them for some simple applications. Tools like auto and simp take them into account.

Actually, trying apply auto to see what happens is not a bad choice. We get the following goal:

 ⋀j. Suc 0 ≤ j ⟹ j < 3 ⟹ s ∈ hd (drop j [{p, q}, {r, s}, {s, t}])


This is essentially trivial, the only missing step should be to realize that you can perform cases/induction on j to complete the task.

I came up with a horrible proof by cases at first,

apply auto
apply (case_tac "j=1")
apply simp
apply (case_tac "j=2")
apply simp


... but you are not supposed to this! For at least three reasons:

1. It does obviously not scale up;
2. It unnecessarily uses apply commands when an Isar proof would be better; and
3. It is using a variable name j that was invented by auto, which tomorrow could be called ja or something worse.

I couldn't manage to complete a nice proof by hand (I mostly use Isabelle/ZF, not HOL), but by using Sledgehammer I was able to complete it:

lemma l1:
"([set [p,q],set [r,s],set [s,t]]) ⊨ (G[1,2] (prop(s)))"
proof auto
show "Suc 0 ≤ j ⟹ j < 3 ⟹ s ∈ hd (drop j [{p, q}, {r, s}, {s, t}])" for j
proof (induct j)
case 0
then
show ?case by simp
next
case (Suc j)
then
show ?case ― ‹Hit "Apply" on Sledgehammer tab here!›
qed
qed


But now knowing that drop_Cons' was useful here, I tried using that and run Sledgehammer again at the beginning:

lemma l1:
"([set [p,q],set [r,s],set [s,t]]) ⊨ (G[1,2] (prop(s)))"
using drop_Cons'
by (smt (verit) One_nat_def atLeastLessThan_iff drop_Suc_Cons
insertCI le_less_Suc_eq length_Cons less_Suc_eq
list.sel(1) list.set(2) list.size(3) list.size(4)


Admittedly, it is not very neat but that came almost without any thinking.

I'm sure there is a shorter way, I leave to the HOL experts to edit my answer!

EDIT: Actually, using auto as an initial method is also not very advisable (the goal stated in show could change slightly and we would have an error at that point), so one could make explicit that we're proving an auxiliary fact (now written a bit more simply) and then instruct auto to solve the goal by using that:

lemma l1:
"([set [p,q],set [r,s],set [s,t]]) ⊨ (G[1,2] (prop(s)))"
proof -
have "1 ≤ j ∧ j < 3 ⟹ s ∈ hd (drop j [{p, q}, {r, s}, {s, t}])" for j
proof (induct j)
case 0
then
show ?case by simp
next
case (Suc j)
then
show ?case by (simp add: drop_Cons')
qed
then
show ?thesis by auto
qed

• Thanks, this works pretty well. After reading this, I tried sledgehammer after proof auto, and that works as well. Jun 9, 2022 at 19:37
• Today I recalled that another suggestion in Gerwin's Style Guide for Isabelle/HOL was that using auto as the first step proof is not a very good idea... I'll edit accordingly Jun 10, 2022 at 11:44