Theorem: relateSeq_append (Pdl/Semantics.lean)

State before:
W : Type
M : KripkeModel W
l1 l2 : List Program
w v : W
⊢ relateSeq M (l1 ++ l2) w v ↔ ∃ u, relateSeq M l1 w u ∧ relateSeq M l2 u v
Tactic:
induction l1 generalizing w v
State after:
case nil
W : Type
M : KripkeModel W
l2 : List Program
w v : W
⊢ relateSeq M ([] ++ l2) w v ↔ ∃ u, relateSeq M [] w u ∧ relateSeq M l2 u v

case cons
W : Type
M : KripkeModel W
l2 : List Program
head✝ : Program
tail✝ : List Program
tail_ih✝ : ∀ (w v : W), relateSeq M (tail✝ ++ l2) w v ↔ ∃ u, relateSeq M tail✝ w u ∧ relateSeq M l2 u v
w v : W
⊢ relateSeq M (head✝ :: tail✝ ++ l2) w v ↔ ∃ u, relateSeq M (head✝ :: tail✝) w u ∧ relateSeq M l2 u v

State before:
W : Type
M : KripkeModel W
l2 : List Program
l : Program
l1 : List Program
IH : ∀ (w v : W), relateSeq M (l1 ++ l2) w v ↔ ∃ u, relateSeq M l1 w u ∧ relateSeq M l2 u v
w v : W
⊢ relateSeq M (l :: l1 ++ l2) w v ↔ ∃ u, relateSeq M (l :: l1) w u ∧ relateSeq M l2 u v
Tactic:
case cons l l1 IH =>
  simp [relateSeq]
  aesop
State after:
no goals

State before:
case nil
W : Type
M : KripkeModel W
l2 : List Program
w v : W
⊢ relateSeq M ([] ++ l2) w v ↔ ∃ u, relateSeq M [] w u ∧ relateSeq M l2 u v
Tactic:
simp [relateSeq]
State after:
no goals

State before:
W : Type
M : KripkeModel W
l2 : List Program
l : Program
l1 : List Program
IH : ∀ (w v : W), relateSeq M (l1 ++ l2) w v ↔ ∃ u, relateSeq M l1 w u ∧ relateSeq M l2 u v
w v : W
⊢ relateSeq M (l :: l1 ++ l2) w v ↔ ∃ u, relateSeq M (l :: l1) w u ∧ relateSeq M l2 u v
Tactic:
simp [relateSeq]
State after:
W : Type
M : KripkeModel W
l2 : List Program
l : Program
l1 : List Program
IH : ∀ (w v : W), relateSeq M (l1 ++ l2) w v ↔ ∃ u, relateSeq M l1 w u ∧ relateSeq M l2 u v
w v : W
⊢ (∃ u, relate M l w u ∧ relateSeq M (l1 ++ l2) u v) ↔
    ∃ u, (∃ u_1, relate M l w u_1 ∧ relateSeq M l1 u_1 u) ∧ relateSeq M l2 u v

State before:
W : Type
M : KripkeModel W
l2 : List Program
l : Program
l1 : List Program
IH : ∀ (w v : W), relateSeq M (l1 ++ l2) w v ↔ ∃ u, relateSeq M l1 w u ∧ relateSeq M l2 u v
w v : W
⊢ (∃ u, relate M l w u ∧ relateSeq M (l1 ++ l2) u v) ↔
    ∃ u, (∃ u_1, relate M l w u_1 ∧ relateSeq M l1 u_1 u) ∧ relateSeq M l2 u v
Tactic:
aesop
State after:
no goals