internlm/Lean-Github huggingface dataset:
Theorem: localDiamondTruth
Proof state before:
case mp.notPsi_imp_rho
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
w_nPsi : evaluate M w (~ψ)
⊢ ∃ Fδ ∈ H (∗β), evaluate M w (Con (Yset Fδ ψ))
Tactic:
simp [H, conEval, Yset]
Proof state after:
case mp.notPsi_imp_rho
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
w_nPsi : evaluate M w (~ψ)
⊢ ¬evaluate M w ψ ∨
    ∃ a b,
      (∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (a, b) ∈ l) ∧
        ∀ (f : Formula), f ∈ a ∨ f = (~⌈⌈b⌉⌉ψ) → evaluate M w f
Theorem: localDiamondTruth
Proof state before:
case mp.notPsi_imp_rho
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
w_nPsi : evaluate M w (~ψ)
⊢ ¬evaluate M w ψ ∨
    ∃ a b,
      (∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (a, b) ∈ l) ∧
        ∀ (f : Formula), f ∈ a ∨ f = (~⌈⌈b⌉⌉ψ) → evaluate M w f
Tactic:
left
Proof state after:
case mp.notPsi_imp_rho.h
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
w_nPsi : evaluate M w (~ψ)
⊢ ¬evaluate M w ψ
Theorem: localDiamondTruth
Proof state before:
case mp.notPsi_imp_rho.h
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
w_nPsi : evaluate M w (~ψ)
⊢ ¬evaluate M w ψ
Tactic:
simp at w_nPsi
Proof state after:
case mp.notPsi_imp_rho.h
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
w_nPsi : ¬evaluate M w ψ
⊢ ¬evaluate M w ψ
Theorem: localDiamondTruth
Proof state before:
case mp.notPsi_imp_rho.h
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
w_nPsi : ¬evaluate M w ψ
⊢ ¬evaluate M w ψ
Tactic:
exact w_nPsi
Proof state after:
no goals
Theorem: localDiamondTruth
Proof state before:
case mpr
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
Tactic:
apply right_to_left_claim
Proof state after:
no goals
Theorem: relateSeq_toChain'
Proof state before:
W : Type
M : KripkeModel W
δ : List Program
v w : W
⊢ relateSeq M δ v w → δ ≠ [] → ∃ l, l.length + 1 = δ.length ∧ List.Chain' (pairRel M) (((?'⊤) :: δ).zip (v :: l ++ [w]))
Tactic:
induction δ generalizing v w
Proof state after:
case nil
W : Type
M : KripkeModel W
v w : W
⊢ relateSeq M [] v w → [] ≠ [] → ∃ l, l.length + 1 = [].length ∧ List.Chain' (pairRel M) ([?'⊤].zip (v :: l ++ [w]))

case cons
W : Type
M : KripkeModel W
head✝ : Program
tail✝ : List Program
tail_ih✝ :
  ∀ {v w : W},
    relateSeq M tail✝ v w →
      tail✝ ≠ [] → ∃ l, l.length + 1 = tail✝.length ∧ List.Chain' (pairRel M) (((?'⊤) :: tail✝).zip (v :: l ++ [w]))
v w : W
⊢ relateSeq M (head✝ :: tail✝) v w →
    head✝ :: tail✝ ≠ [] →
      ∃ l,
        l.length + 1 = (head✝ :: tail✝).length ∧ List.Chain' (pairRel M) (((?'⊤) :: head✝ :: tail✝).zip (v :: l ++ [w]))
Theorem: relateSeq_toChain'
Proof state before:
W : Type
M : KripkeModel W
v w : W
⊢ relateSeq M [] v w → [] ≠ [] → ∃ l, l.length + 1 = [].length ∧ List.Chain' (pairRel M) ([?'⊤].zip (v :: l ++ [w]))
Tactic:
case nil =>
  simp [relateSeq]
Proof state after:
no goals
Theorem: relateSeq_toChain'
Proof state before:
W : Type
M : KripkeModel W
v w : W
⊢ relateSeq M [] v w → [] ≠ [] → ∃ l, l.length + 1 = [].length ∧ List.Chain' (pairRel M) ([?'⊤].zip (v :: l ++ [w]))
Tactic:
simp [relateSeq]
Proof state after:
no goals
Theorem: relateSeq_toChain'
Proof state before:
W : Type
M : KripkeModel W
e : Program
δ : List Program
IH :
  ∀ {v w : W},
    relateSeq M δ v w →
      δ ≠ [] → ∃ l, l.length + 1 = δ.length ∧ List.Chain' (pairRel M) (((?'⊤) :: δ).zip (v :: l ++ [w]))
v w : W
⊢ relateSeq M (e :: δ) v w →
    e :: δ ≠ [] → ∃ l, l.length + 1 = (e :: δ).length ∧ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: l ++ [w]))
Tactic:
cases em (δ = [])
Proof state after:
case inl
W : Type
M : KripkeModel W
e : Program
δ : List Program
IH :
  ∀ {v w : W},
    relateSeq M δ v w →
      δ ≠ [] → ∃ l, l.length + 1 = δ.length ∧ List.Chain' (pairRel M) (((?'⊤) :: δ).zip (v :: l ++ [w]))
v w : W
h✝ : δ = []
⊢ relateSeq M (e :: δ) v w →
    e :: δ ≠ [] → ∃ l, l.length + 1 = (e :: δ).length ∧ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: l ++ [w]))

case inr
W : Type
M : KripkeModel W
e : Program
δ : List Program
IH :
  ∀ {v w : W},
    relateSeq M δ v w →
      δ ≠ [] → ∃ l, l.length + 1 = δ.length ∧ List.Chain' (pairRel M) (((?'⊤) :: δ).zip (v :: l ++ [w]))
v w : W
h✝ : ¬δ = []
⊢ relateSeq M (e :: δ) v w →
    e :: δ ≠ [] → ∃ l, l.length + 1 = (e :: δ).length ∧ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: l ++ [w]))
Theorem: relateSeq_toChain'
Proof state before:
W : Type
M : KripkeModel W
e : Program
δ : List Program
IH :
  ∀ {v w : W},
    relateSeq M δ v w →
      δ ≠ [] → ∃ l, l.length + 1 = δ.length ∧ List.Chain' (pairRel M) (((?'⊤) :: δ).zip (v :: l ++ [w]))
v w : W
δ_eq_empty : δ = []
⊢ relateSeq M (e :: δ) v w →
    e :: δ ≠ [] → ∃ l, l.length + 1 = (e :: δ).length ∧ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: l ++ [w]))
Tactic:
case inl δ_eq_empty =>
  subst δ_eq_empty
  intro _
  simp_all [pairRel]
Proof state after:
no goals
Theorem: relateSeq_toChain'
Proof state before:
W : Type
M : KripkeModel W
e : Program
δ : List Program
IH :
  ∀ {v w : W},
    relateSeq M δ v w →
      δ ≠ [] → ∃ l, l.length + 1 = δ.length ∧ List.Chain' (pairRel M) (((?'⊤) :: δ).zip (v :: l ++ [w]))
v w : W
δ_eq_empty : δ = []
⊢ relateSeq M (e :: δ) v w →
    e :: δ ≠ [] → ∃ l, l.length + 1 = (e :: δ).length ∧ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: l ++ [w]))
Tactic:
subst δ_eq_empty
Proof state after:
W : Type
M : KripkeModel W
e : Program
v w : W
IH :
  ∀ {v w : W},
    relateSeq M [] v w → [] ≠ [] → ∃ l, l.length + 1 = [].length ∧ List.Chain' (pairRel M) ([?'⊤].zip (v :: l ++ [w]))
⊢ relateSeq M [e] v w →
    [e] ≠ [] → ∃ l, l.length + 1 = [e].length ∧ List.Chain' (pairRel M) ([?'⊤, e].zip (v :: l ++ [w]))
Theorem: relateSeq_toChain'
Proof state before:
W : Type
M : KripkeModel W
e : Program
v w : W
IH :
  ∀ {v w : W},
    relateSeq M [] v w → [] ≠ [] → ∃ l, l.length + 1 = [].length ∧ List.Chain' (pairRel M) ([?'⊤].zip (v :: l ++ [w]))
⊢ relateSeq M [e] v w →
    [e] ≠ [] → ∃ l, l.length + 1 = [e].length ∧ List.Chain' (pairRel M) ([?'⊤, e].zip (v :: l ++ [w]))
Tactic:
intro _
Proof state after:
W : Type
M : KripkeModel W
e : Program
v w : W
IH :
  ∀ {v w : W},
    relateSeq M [] v w → [] ≠ [] → ∃ l, l.length + 1 = [].length ∧ List.Chain' (pairRel M) ([?'⊤].zip (v :: l ++ [w]))
a✝ : relateSeq M [e] v w
⊢ [e] ≠ [] → ∃ l, l.length + 1 = [e].length ∧ List.Chain' (pairRel M) ([?'⊤, e].zip (v :: l ++ [w]))
Theorem: relateSeq_toChain'
Proof state before:
W : Type
M : KripkeModel W
e : Program
v w : W
IH :
  ∀ {v w : W},
    relateSeq M [] v w → [] ≠ [] → ∃ l, l.length + 1 = [].length ∧ List.Chain' (pairRel M) ([?'⊤].zip (v :: l ++ [w]))
a✝ : relateSeq M [e] v w
⊢ [e] ≠ [] → ∃ l, l.length + 1 = [e].length ∧ List.Chain' (pairRel M) ([?'⊤, e].zip (v :: l ++ [w]))
Tactic:
simp_all [pairRel]
Proof state after:
no goals
Theorem: relateSeq_toChain'
Proof state before:
W : Type
M : KripkeModel W
e : Program
δ : List Program
IH :
  ∀ {v w : W},
    relateSeq M δ v w →
      δ ≠ [] → ∃ l, l.length + 1 = δ.length ∧ List.Chain' (pairRel M) (((?'⊤) :: δ).zip (v :: l ++ [w]))
v w : W
δ_notEmpty : ¬δ = []
⊢ relateSeq M (e :: δ) v w →
    e :: δ ≠ [] → ∃ l, l.length + 1 = (e :: δ).length ∧ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: l ++ [w]))
Tactic:
simp only [relateSeq]
Proof state after:
W : Type
M : KripkeModel W
e : Program
δ : List Program
IH :
  ∀ {v w : W},
    relateSeq M δ v w →
      δ ≠ [] → ∃ l, l.length + 1 = δ.length ∧ List.Chain' (pairRel M) (((?'⊤) :: δ).zip (v :: l ++ [w]))
v w : W
δ_notEmpty : ¬δ = []
⊢ (∃ u, relate M e v u ∧ relateSeq M δ u w) →
    e :: δ ≠ [] → ∃ l, l.length + 1 = (e :: δ).length ∧ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: l ++ [w]))
Theorem: relateSeq_toChain'
Proof state before:
W : Type
M : KripkeModel W
e : Program
δ : List Program
IH :
  ∀ {v w : W},
    relateSeq M δ v w →
      δ ≠ [] → ∃ l, l.length + 1 = δ.length ∧ List.Chain' (pairRel M) (((?'⊤) :: δ).zip (v :: l ++ [w]))
v w : W
δ_notEmpty : ¬δ = []
⊢ (∃ u, relate M e v u ∧ relateSeq M δ u w) →
    e :: δ ≠ [] → ∃ l, l.length + 1 = (e :: δ).length ∧ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: l ++ [w]))
Tactic:
rintro ⟨u, v_d_u, u_δ_w⟩ _
Proof state after:
case intro.intro
W : Type
M : KripkeModel W
e : Program
δ : List Program
IH :
  ∀ {v w : W},
    relateSeq M δ v w →
      δ ≠ [] → ∃ l, l.length + 1 = δ.length ∧ List.Chain' (pairRel M) (((?'⊤) :: δ).zip (v :: l ++ [w]))
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
a✝ : e :: δ ≠ []
⊢ ∃ l, l.length + 1 = (e :: δ).length ∧ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: l ++ [w]))
Theorem: relateSeq_toChain'
Proof state before:
case intro.intro
W : Type
M : KripkeModel W
e : Program
δ : List Program
IH :
  ∀ {v w : W},
    relateSeq M δ v w →
      δ ≠ [] → ∃ l, l.length + 1 = δ.length ∧ List.Chain' (pairRel M) (((?'⊤) :: δ).zip (v :: l ++ [w]))
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
a✝ : e :: δ ≠ []
⊢ ∃ l, l.length + 1 = (e :: δ).length ∧ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: l ++ [w]))
Tactic:
specialize IH u_δ_w δ_notEmpty
Proof state after:
case intro.intro
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
a✝ : e :: δ ≠ []
IH : ∃ l, l.length + 1 = δ.length ∧ List.Chain' (pairRel M) (((?'⊤) :: δ).zip (u :: l ++ [w]))
⊢ ∃ l, l.length + 1 = (e :: δ).length ∧ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: l ++ [w]))
Theorem: relateSeq_toChain'
Proof state before:
case intro.intro
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
a✝ : e :: δ ≠ []
IH : ∃ l, l.length + 1 = δ.length ∧ List.Chain' (pairRel M) (((?'⊤) :: δ).zip (u :: l ++ [w]))
⊢ ∃ l, l.length + 1 = (e :: δ).length ∧ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: l ++ [w]))
Tactic:
rcases IH with ⟨l, l_def, lchain⟩
Proof state after:
case intro.intro.intro.intro
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
a✝ : e :: δ ≠ []
l : List W
l_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel M) (((?'⊤) :: δ).zip (u :: l ++ [w]))
⊢ ∃ l, l.length + 1 = (e :: δ).length ∧ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: l ++ [w]))
Theorem: relateSeq_toChain'
Proof state before:
case intro.intro.intro.intro
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
a✝ : e :: δ ≠ []
l : List W
l_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel M) (((?'⊤) :: δ).zip (u :: l ++ [w]))
⊢ ∃ l, l.length + 1 = (e :: δ).length ∧ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: l ++ [w]))
Tactic:
use (u :: l)
Proof state after:
case h
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
a✝ : e :: δ ≠ []
l : List W
l_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel M) (((?'⊤) :: δ).zip (u :: l ++ [w]))
⊢ (u :: l).length + 1 = (e :: δ).length ∧ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: u :: l ++ [w]))
Theorem: relateSeq_toChain'
Proof state before:
case h
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
a✝ : e :: δ ≠ []
l : List W
l_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel M) (((?'⊤) :: δ).zip (u :: l ++ [w]))
⊢ (u :: l).length + 1 = (e :: δ).length ∧ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: u :: l ++ [w]))
Tactic:
constructor
Proof state after:
case h.left
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
a✝ : e :: δ ≠ []
l : List W
l_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel M) (((?'⊤) :: δ).zip (u :: l ++ [w]))
⊢ (u :: l).length + 1 = (e :: δ).length

case h.right
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
a✝ : e :: δ ≠ []
l : List W
l_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel M) (((?'⊤) :: δ).zip (u :: l ++ [w]))
⊢ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: u :: l ++ [w]))
Theorem: relateSeq_toChain'
Proof state before:
case h.left
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
a✝ : e :: δ ≠ []
l : List W
l_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel M) (((?'⊤) :: δ).zip (u :: l ++ [w]))
⊢ (u :: l).length + 1 = (e :: δ).length
Tactic:
simp_all
Proof state after:
no goals
Theorem: relateSeq_toChain'
Proof state before:
case h.right
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
a✝ : e :: δ ≠ []
l : List W
l_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel M) (((?'⊤) :: δ).zip (u :: l ++ [w]))
⊢ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: u :: l ++ [w]))
Tactic:
simp_all [pairRel]
Proof state after:
case h.right
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
l : List W
l_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: δ.zip (l ++ [w]))
⊢ List.Chain' (pairRel M) ((e, u) :: δ.zip (l ++ [w]))
Theorem: relateSeq_toChain'
Proof state before:
case h.right
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
l : List W
l_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: δ.zip (l ++ [w]))
⊢ List.Chain' (pairRel M) ((e, u) :: δ.zip (l ++ [w]))
Tactic:
apply List.Chain'.cons'
Proof state after:
case h.right.a
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
l : List W
l_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: δ.zip (l ++ [w]))
⊢ List.Chain' (pairRel M) (δ.zip (l ++ [w]))

case h.right.a
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
l : List W
l_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: δ.zip (l ++ [w]))
⊢ ∀ y ∈ (δ.zip (l ++ [w])).head?, pairRel M (e, u) y
Theorem: relateSeq_toChain'
Proof state before:
case h.right.a
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
l : List W
l_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: δ.zip (l ++ [w]))
⊢ List.Chain' (pairRel M) (δ.zip (l ++ [w]))
Tactic:
have := List.Chain'.tail lchain
Proof state after:
case h.right.a
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
l : List W
l_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: δ.zip (l ++ [w]))
this : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: δ.zip (l ++ [w])).tail
⊢ List.Chain' (pairRel M) (δ.zip (l ++ [w]))
Theorem: relateSeq_toChain'
Proof state before:
case h.right.a
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
l : List W
l_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: δ.zip (l ++ [w]))
this : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: δ.zip (l ++ [w])).tail
⊢ List.Chain' (pairRel M) (δ.zip (l ++ [w]))
Tactic:
simp_all
Proof state after:
no goals
Theorem: relateSeq_toChain'
Proof state before:
case h.right.a
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
l : List W
l_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: δ.zip (l ++ [w]))
⊢ ∀ y ∈ (δ.zip (l ++ [w])).head?, pairRel M (e, u) y
Tactic:
cases l <;> cases δ
Proof state after:
case h.right.a.nil.nil
W : Type
M : KripkeModel W
e : Program
v w u : W
v_d_u : relate M e v u
δ_notEmpty : ¬[] = []
u_δ_w : relateSeq M [] u w
l_def : [].length + 1 = [].length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: [].zip ([] ++ [w]))
⊢ ∀ y ∈ ([].zip ([] ++ [w])).head?, pairRel M (e, u) y

case h.right.a.nil.cons
W : Type
M : KripkeModel W
e : Program
v w u : W
v_d_u : relate M e v u
head✝ : Program
tail✝ : List Program
δ_notEmpty : ¬head✝ :: tail✝ = []
u_δ_w : relateSeq M (head✝ :: tail✝) u w
l_def : [].length + 1 = (head✝ :: tail✝).length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: (head✝ :: tail✝).zip ([] ++ [w]))
⊢ ∀ y ∈ ((head✝ :: tail✝).zip ([] ++ [w])).head?, pairRel M (e, u) y

case h.right.a.cons.nil
W : Type
M : KripkeModel W
e : Program
v w u : W
v_d_u : relate M e v u
head✝ : W
tail✝ : List W
δ_notEmpty : ¬[] = []
u_δ_w : relateSeq M [] u w
l_def : (head✝ :: tail✝).length + 1 = [].length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: [].zip (head✝ :: tail✝ ++ [w]))
⊢ ∀ y ∈ ([].zip (head✝ :: tail✝ ++ [w])).head?, pairRel M (e, u) y

case h.right.a.cons.cons
W : Type
M : KripkeModel W
e : Program
v w u : W
v_d_u : relate M e v u
head✝¹ : W
tail✝¹ : List W
head✝ : Program
tail✝ : List Program
δ_notEmpty : ¬head✝ :: tail✝ = []
u_δ_w : relateSeq M (head✝ :: tail✝) u w
l_def : (head✝¹ :: tail✝¹).length + 1 = (head✝ :: tail✝).length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: (head✝ :: tail✝).zip (head✝¹ :: tail✝¹ ++ [w]))
⊢ ∀ y ∈ ((head✝ :: tail✝).zip (head✝¹ :: tail✝¹ ++ [w])).head?, pairRel M (e, u) y
Theorem: relateSeq_toChain'
Proof state before:
case h.right.a.nil.nil
W : Type
M : KripkeModel W
e : Program
v w u : W
v_d_u : relate M e v u
δ_notEmpty : ¬[] = []
u_δ_w : relateSeq M [] u w
l_def : [].length + 1 = [].length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: [].zip ([] ++ [w]))
⊢ ∀ y ∈ ([].zip ([] ++ [w])).head?, pairRel M (e, u) y

case h.right.a.nil.cons
W : Type
M : KripkeModel W
e : Program
v w u : W
v_d_u : relate M e v u
head✝ : Program
tail✝ : List Program
δ_notEmpty : ¬head✝ :: tail✝ = []
u_δ_w : relateSeq M (head✝ :: tail✝) u w
l_def : [].length + 1 = (head✝ :: tail✝).length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: (head✝ :: tail✝).zip ([] ++ [w]))
⊢ ∀ y ∈ ((head✝ :: tail✝).zip ([] ++ [w])).head?, pairRel M (e, u) y

case h.right.a.cons.nil
W : Type
M : KripkeModel W
e : Program
v w u : W
v_d_u : relate M e v u
head✝ : W
tail✝ : List W
δ_notEmpty : ¬[] = []
u_δ_w : relateSeq M [] u w
l_def : (head✝ :: tail✝).length + 1 = [].length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: [].zip (head✝ :: tail✝ ++ [w]))
⊢ ∀ y ∈ ([].zip (head✝ :: tail✝ ++ [w])).head?, pairRel M (e, u) y

case h.right.a.cons.cons
W : Type
M : KripkeModel W
e : Program
v w u : W
v_d_u : relate M e v u
head✝¹ : W
tail✝¹ : List W
head✝ : Program
tail✝ : List Program
δ_notEmpty : ¬head✝ :: tail✝ = []
u_δ_w : relateSeq M (head✝ :: tail✝) u w
l_def : (head✝¹ :: tail✝¹).length + 1 = (head✝ :: tail✝).length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: (head✝ :: tail✝).zip (head✝¹ :: tail✝¹ ++ [w]))
⊢ ∀ y ∈ ((head✝ :: tail✝).zip (head✝¹ :: tail✝¹ ++ [w])).head?, pairRel M (e, u) y
Tactic:
all_goals simp_all [pairRel]
Proof state after:
no goals
Theorem: relateSeq_toChain'
Proof state before:
case h.right.a.cons.cons
W : Type
M : KripkeModel W
e : Program
v w u : W
v_d_u : relate M e v u
head✝¹ : W
tail✝¹ : List W
head✝ : Program
tail✝ : List Program
δ_notEmpty : ¬head✝ :: tail✝ = []
u_δ_w : relateSeq M (head✝ :: tail✝) u w
l_def : (head✝¹ :: tail✝¹).length + 1 = (head✝ :: tail✝).length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: (head✝ :: tail✝).zip (head✝¹ :: tail✝¹ ++ [w]))
⊢ ∀ y ∈ ((head✝ :: tail✝).zip (head✝¹ :: tail✝¹ ++ [w])).head?, pairRel M (e, u) y
Tactic:
simp_all [pairRel]
Proof state after:
no goals