5
$\begingroup$

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?

$\endgroup$

1 Answer 1

2
$\begingroup$

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!›
      by (simp add: drop_Cons')
  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)
      nat_1_add_1 semantics_mltl.simps(3) semantics_mltl.simps(9)) 

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
$\endgroup$
2
  • $\begingroup$ Thanks, this works pretty well. After reading this, I tried sledgehammer after proof auto, and that works as well. $\endgroup$
    – Gokul
    Jun 9, 2022 at 19:37
  • $\begingroup$ 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 $\endgroup$ Jun 10, 2022 at 11:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.