Mutual recursion/induction

Stream: new members

[Logan Murphy]

I'm trying to formalize some semantics for Computation Tree Logic and I'm running into some trouble making either a mutually recursive or mutually inductive definition.

I find that if I try to make a recursive definition, I can't determine it's well-founded (at least not automatically, I'm not sure how to use using_well_founded). I assume this is because part of the definition depends on set membership which is undecidable in general.

On the other hand, if I try to make an inductive predicate I get the problem that I'm trying to index mutually inductive types in terms of one another, which Lean doesn't seem to like.

Does anyone see a way that I could work around either of these problems?

import data.fintype.basic data.set tactic data.stream.basic
open stream

namespace CTL

variables (AP : Type)

mutual inductive state_formula, path_formula
with state_formula : Type
| T             : state_formula
| atom (a : AP) : state_formula
| conj (Φ₁ Φ₂ : state_formula ) : state_formula
| neg (Φ : state_formula) : state_formula
| E (φ : path_formula) : state_formula
| A (φ : path_formula) : state_formula
with path_formula : Type
| next (Φ : state_formula) : path_formula
| until (Φ₁ Φ₂ : state_formula) : path_formula
open state_formula
open path_formula

local notation  `∼` Φ := neg Φ
local notation Φ `and` Ψ := conj Φ Ψ
local notation `O` Φ := next Φ
local notation Φ `𝒰` Ψ := until Φ Ψ

structure TS :=
(S : Type)
(H : decidable_eq S)
(Act : Type)
(TR : set (S × Act × S))
(L  : S → set AP)

def Post_of  {M : TS AP} (s : M.S) (α : M.Act) : set (M.S) := {s' | (s,α,s') ∈ M.TR}

def Post {M : TS AP} (s : M.S) : set (M.S) :=
⋃ α : M.Act, Post_of _ s α

structure path
(M : TS AP) :=
(val : stream M.S)
(H : ∀ i : ℕ, val (i + 1) ∈ Post _ (val i))

def first {M : TS AP} (π : path _ M) : M.S := π.val 0

def paths
{M : TS AP} (s : M.S) : set (path _ M) :=
(λ π, s = (first _ π))

--- recursive definition
mutual def state_sat, path_sat {M : TS AP}
with state_sat : state_formula AP → M.S → Prop
| T _ := true
| (atom a) s := a ∈ M.L s
| (Φ and Ψ) s := state_sat Φ s ∧ state_sat Ψ s
| (∼ Φ) s := ¬ (state_sat Φ s)
| (E φ) s := ∃ π : path _ M, π ∈ paths _ s → path_sat φ π --not well-founded
| (A φ) s := ∀ π : path _ M, π ∈ paths _ s → path_sat φ π --not well-founded
with path_sat : path_formula AP → path _ M → Prop
| (O Φ) π := state_sat Φ (π.val 1)
| (Φ 𝒰 Ψ) π := true

--inductive definition
mutual inductive state_sat, path_sat {M : TS AP} --indexing problem
with state_sat : M.S → state_formula AP →  Prop
| TT :
    ∀ s : M.S, state_sat s T
| atoms :
    ∀ s : M.S, ∀ a : AP, a ∈ M.L s → state_sat s (atom a)
| conj :
    ∀ s : M.S, ∀ (Φ Ψ : state_formula AP),
        state_sat s Φ ∧ state_sat s Ψ → state_sat s (Φ and Ψ)
| neg :
    ∀ s : M.S, ∀ (Φ : state_formula AP),
        ¬(state_sat s Φ)
| E (φ : path_formula AP) :
     ∀ s : M.S, ∃ π ∈ paths _ s, path_sat π φ
| A (φ : path_formula AP):
     ∀ s : M.S,
      ∀ π ∈ paths _ s, path_sat π φ
with path_sat : path _ M → path_formula AP → Prop
| next (Φ : state_formula AP):
   ∀ π : path _ M, state_sat (first _ π) (Φ) →
                   path_sat π (O Φ)
| until (Φ Ψ : state_formula AP):
   ∀ π : path _ M, ∃ j : ℕ, (state_sat (π.val j) Ψ) ∧
            (∀ k < j, state_sat (π.val k) Φ ) → path_sat π (Φ 𝒰 Ψ)
end CTL

Also, I think the inductive defintion above does what the recursive definition is supposed to do, but I'm not 100% confident in that.

[Mario Carneiro]

mutual def state_sat, path_sat {M : TS AP}
with state_sat : state_formula AP → M.S → Prop
| T := λ _, true
| (atom a) := λ s, a ∈ M.L s
| (Φ and Ψ) := λ s, state_sat Φ s ∧ state_sat Ψ s
| (∼ Φ) := λ s, ¬ (state_sat Φ s)
| (E φ) := λ s, ∃ π : path _ M, π ∈ paths _ s → path_sat φ π
| (A φ) := λ s, ∀ π : path _ M, π ∈ paths _ s → path_sat φ π
with path_sat : path_formula AP → path _ M → Prop
| (O Φ) := λ π, state_sat Φ (π.val 1)
| (Φ 𝒰 Ψ) := λ π, true

[Logan Murphy]

Oh, wow. Is there a high-level intuition for why changing the pattern-matching this way affects well-foundedness?

[Mario Carneiro]

@Logan Murphy When lean tries to invent a well founded metric for a definition, it tuples up all the arguments left of the := and uses sizeof for the resulting sigma type. So if you want to do recursion on the first argument only, allowing the second to vary arbitrarily, then you should keep it out of the pattern match

[Logan Murphy]

Right. Thank you!