Theorem: LoVe.BigStepEquiv.seq_congr (LoVe/Labs/Lab6Solution.lean)

State before:
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
⊢ S₁; T₁ ~ S₂; T₂
Tactic:
intro s t
State after:
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
⊢ (S₁; T₁, s) ⟹ t ↔ (S₂; T₂, s) ⟹ t

State before:
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
⊢ (S₁; T₁, s) ⟹ t ↔ (S₂; T₂, s) ⟹ t
Tactic:
apply Iff.intro
State after:
case mp
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
⊢ (S₁; T₁, s) ⟹ t → (S₂; T₂, s) ⟹ t

case mpr
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
⊢ (S₂; T₂, s) ⟹ t → (S₁; T₁, s) ⟹ t

State before:
case mp
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
⊢ (S₁; T₁, s) ⟹ t → (S₂; T₂, s) ⟹ t

case mpr
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
⊢ (S₂; T₂, s) ⟹ t → (S₁; T₁, s) ⟹ t
Tactic:
{ intro hseq
  cases hseq with
  | seq _ _ _ u _ hS₁ hT₁ =>
    apply BigStep.seq
    { rw [BigStepEquiv] at hS
      rw [← hS]
      assumption }
    { rw [BigStepEquiv] at hT
      rw [← hT]
      assumption } }
State after:
case mpr
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
⊢ (S₂; T₂, s) ⟹ t → (S₁; T₁, s) ⟹ t

State before:
case mpr
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
⊢ (S₂; T₂, s) ⟹ t → (S₁; T₁, s) ⟹ t
Tactic:
{ intro hseq
  cases hseq with
  | seq _ _ _ u _ hS₂ hT₂ =>
    apply BigStep.seq
    { rw [BigStepEquiv] at hS
      rw [hS]
      assumption }
    { rw [BigStepEquiv] at hT
      rw [hT]
      assumption } }
State after:
no goals

State before:
case mp
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
⊢ (S₁; T₁, s) ⟹ t → (S₂; T₂, s) ⟹ t
Tactic:
intro hseq
State after:
case mp
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hseq : (S₁; T₁, s) ⟹ t
⊢ (S₂; T₂, s) ⟹ t

State before:
case mp
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hseq : (S₁; T₁, s) ⟹ t
⊢ (S₂; T₂, s) ⟹ t
Tactic:
cases hseq with
| seq _ _ _ u _ hS₁ hT₁ =>
  apply BigStep.seq
  { rw [BigStepEquiv] at hS
    rw [← hS]
    assumption }
  { rw [BigStepEquiv] at hT
    rw [← hT]
    assumption }
State after:
no goals

State before:
case mp.seq
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t u : State
hS₁ : (S₁, s) ⟹ u
hT₁ : (T₁, u) ⟹ t
⊢ (S₂; T₂, s) ⟹ t
Tactic:
apply BigStep.seq
State after:
case mp.seq.hS
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t u : State
hS₁ : (S₁, s) ⟹ u
hT₁ : (T₁, u) ⟹ t
⊢ (S₂, s) ⟹ ?mp.seq.t

case mp.seq.hT
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t u : State
hS₁ : (S₁, s) ⟹ u
hT₁ : (T₁, u) ⟹ t
⊢ (T₂, ?mp.seq.t) ⟹ t

case mp.seq.t
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t u : State
hS₁ : (S₁, s) ⟹ u
hT₁ : (T₁, u) ⟹ t
⊢ State

State before:
case mp.seq.hS
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t u : State
hS₁ : (S₁, s) ⟹ u
hT₁ : (T₁, u) ⟹ t
⊢ (S₂, s) ⟹ ?mp.seq.t

case mp.seq.hT
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t u : State
hS₁ : (S₁, s) ⟹ u
hT₁ : (T₁, u) ⟹ t
⊢ (T₂, ?mp.seq.t) ⟹ t

case mp.seq.t
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t u : State
hS₁ : (S₁, s) ⟹ u
hT₁ : (T₁, u) ⟹ t
⊢ State
Tactic:
{ rw [BigStepEquiv] at hS
  rw [← hS]
  assumption }
State after:
case mp.seq.hT
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t u : State
hS₁ : (S₁, s) ⟹ u
hT₁ : (T₁, u) ⟹ t
⊢ (T₂, u) ⟹ t

State before:
case mp.seq.hT
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t u : State
hS₁ : (S₁, s) ⟹ u
hT₁ : (T₁, u) ⟹ t
⊢ (T₂, u) ⟹ t
Tactic:
{ rw [BigStepEquiv] at hT
  rw [← hT]
  assumption }
State after:
no goals

State before:
case mp.seq.hS
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t u : State
hS₁ : (S₁, s) ⟹ u
hT₁ : (T₁, u) ⟹ t
⊢ (S₂, s) ⟹ ?mp.seq.t
Tactic:
rw [BigStepEquiv] at hS
State after:
case mp.seq.hS
S₁ S₂ T₁ T₂ : Stmt
hS✝ : S₁ ~ S₂
hS : ∀ (s t : State), (S₁, s) ⟹ t ↔ (S₂, s) ⟹ t
hT : T₁ ~ T₂
s t u : State
hS₁ : (S₁, s) ⟹ u
hT₁ : (T₁, u) ⟹ t
⊢ (S₂, s) ⟹ ?m.68459 hT s t u hS₁ hT₁

State before:
case mp.seq.hS
S₁ S₂ T₁ T₂ : Stmt
hS✝ : S₁ ~ S₂
hS : ∀ (s t : State), (S₁, s) ⟹ t ↔ (S₂, s) ⟹ t
hT : T₁ ~ T₂
s t u : State
hS₁ : (S₁, s) ⟹ u
hT₁ : (T₁, u) ⟹ t
⊢ (S₂, s) ⟹ ?m.68459 hT s t u hS₁ hT₁
Tactic:
rw [← hS]
State after:
case mp.seq.hS
S₁ S₂ T₁ T₂ : Stmt
hS✝ : S₁ ~ S₂
hS : ∀ (s t : State), (S₁, s) ⟹ t ↔ (S₂, s) ⟹ t
hT : T₁ ~ T₂
s t u : State
hS₁ : (S₁, s) ⟹ u
hT₁ : (T₁, u) ⟹ t
⊢ (S₁, s) ⟹ ?m.68459 hT s t u hS₁ hT₁

S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
⊢ T₁ ~ T₂ → (s t u : State) → (S₁, s) ⟹ u → (T₁, u) ⟹ t → State

State before:
case mp.seq.hS
S₁ S₂ T₁ T₂ : Stmt
hS✝ : S₁ ~ S₂
hS : ∀ (s t : State), (S₁, s) ⟹ t ↔ (S₂, s) ⟹ t
hT : T₁ ~ T₂
s t u : State
hS₁ : (S₁, s) ⟹ u
hT₁ : (T₁, u) ⟹ t
⊢ (S₁, s) ⟹ ?m.68459 hT s t u hS₁ hT₁

S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
⊢ T₁ ~ T₂ → (s t u : State) → (S₁, s) ⟹ u → (T₁, u) ⟹ t → State
Tactic:
assumption
State after:
no goals

State before:
case mp.seq.hT
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t u : State
hS₁ : (S₁, s) ⟹ u
hT₁ : (T₁, u) ⟹ t
⊢ (T₂, u) ⟹ t
Tactic:
rw [BigStepEquiv] at hT
State after:
case mp.seq.hT
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : ∀ (s t : State), (T₁, s) ⟹ t ↔ (T₂, s) ⟹ t
s t u : State
hS₁ : (S₁, s) ⟹ u
hT₁ : (T₁, u) ⟹ t
⊢ (T₂, u) ⟹ t

State before:
case mp.seq.hT
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : ∀ (s t : State), (T₁, s) ⟹ t ↔ (T₂, s) ⟹ t
s t u : State
hS₁ : (S₁, s) ⟹ u
hT₁ : (T₁, u) ⟹ t
⊢ (T₂, u) ⟹ t
Tactic:
rw [← hT]
State after:
case mp.seq.hT
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : ∀ (s t : State), (T₁, s) ⟹ t ↔ (T₂, s) ⟹ t
s t u : State
hS₁ : (S₁, s) ⟹ u
hT₁ : (T₁, u) ⟹ t
⊢ (T₁, u) ⟹ t

State before:
case mp.seq.hT
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : ∀ (s t : State), (T₁, s) ⟹ t ↔ (T₂, s) ⟹ t
s t u : State
hS₁ : (S₁, s) ⟹ u
hT₁ : (T₁, u) ⟹ t
⊢ (T₁, u) ⟹ t
Tactic:
assumption
State after:
no goals

State before:
case mpr
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
⊢ (S₂; T₂, s) ⟹ t → (S₁; T₁, s) ⟹ t
Tactic:
intro hseq
State after:
case mpr
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hseq : (S₂; T₂, s) ⟹ t
⊢ (S₁; T₁, s) ⟹ t

State before:
case mpr
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hseq : (S₂; T₂, s) ⟹ t
⊢ (S₁; T₁, s) ⟹ t
Tactic:
cases hseq with
| seq _ _ _ u _ hS₂ hT₂ =>
  apply BigStep.seq
  { rw [BigStepEquiv] at hS
    rw [hS]
    assumption }
  { rw [BigStepEquiv] at hT
    rw [hT]
    assumption }
State after:
no goals

State before:
case mpr.seq
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t u : State
hS₂ : (S₂, s) ⟹ u
hT₂ : (T₂, u) ⟹ t
⊢ (S₁; T₁, s) ⟹ t
Tactic:
apply BigStep.seq
State after:
case mpr.seq.hS
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t u : State
hS₂ : (S₂, s) ⟹ u
hT₂ : (T₂, u) ⟹ t
⊢ (S₁, s) ⟹ ?mpr.seq.t

case mpr.seq.hT
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t u : State
hS₂ : (S₂, s) ⟹ u
hT₂ : (T₂, u) ⟹ t
⊢ (T₁, ?mpr.seq.t) ⟹ t

case mpr.seq.t
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t u : State
hS₂ : (S₂, s) ⟹ u
hT₂ : (T₂, u) ⟹ t
⊢ State

State before:
case mpr.seq.hS
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t u : State
hS₂ : (S₂, s) ⟹ u
hT₂ : (T₂, u) ⟹ t
⊢ (S₁, s) ⟹ ?mpr.seq.t

case mpr.seq.hT
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t u : State
hS₂ : (S₂, s) ⟹ u
hT₂ : (T₂, u) ⟹ t
⊢ (T₁, ?mpr.seq.t) ⟹ t

case mpr.seq.t
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t u : State
hS₂ : (S₂, s) ⟹ u
hT₂ : (T₂, u) ⟹ t
⊢ State
Tactic:
{ rw [BigStepEquiv] at hS
  rw [hS]
  assumption }
State after:
case mpr.seq.hT
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t u : State
hS₂ : (S₂, s) ⟹ u
hT₂ : (T₂, u) ⟹ t
⊢ (T₁, u) ⟹ t

State before:
case mpr.seq.hT
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t u : State
hS₂ : (S₂, s) ⟹ u
hT₂ : (T₂, u) ⟹ t
⊢ (T₁, u) ⟹ t
Tactic:
{ rw [BigStepEquiv] at hT
  rw [hT]
  assumption }
State after:
no goals

State before:
case mpr.seq.hS
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t u : State
hS₂ : (S₂, s) ⟹ u
hT₂ : (T₂, u) ⟹ t
⊢ (S₁, s) ⟹ ?mpr.seq.t
Tactic:
rw [BigStepEquiv] at hS
State after:
case mpr.seq.hS
S₁ S₂ T₁ T₂ : Stmt
hS✝ : S₁ ~ S₂
hS : ∀ (s t : State), (S₁, s) ⟹ t ↔ (S₂, s) ⟹ t
hT : T₁ ~ T₂
s t u : State
hS₂ : (S₂, s) ⟹ u
hT₂ : (T₂, u) ⟹ t
⊢ (S₁, s) ⟹ ?m.68939 hT s t u hS₂ hT₂

State before:
case mpr.seq.hS
S₁ S₂ T₁ T₂ : Stmt
hS✝ : S₁ ~ S₂
hS : ∀ (s t : State), (S₁, s) ⟹ t ↔ (S₂, s) ⟹ t
hT : T₁ ~ T₂
s t u : State
hS₂ : (S₂, s) ⟹ u
hT₂ : (T₂, u) ⟹ t
⊢ (S₁, s) ⟹ ?m.68939 hT s t u hS₂ hT₂
Tactic:
rw [hS]
State after:
case mpr.seq.hS
S₁ S₂ T₁ T₂ : Stmt
hS✝ : S₁ ~ S₂
hS : ∀ (s t : State), (S₁, s) ⟹ t ↔ (S₂, s) ⟹ t
hT : T₁ ~ T₂
s t u : State
hS₂ : (S₂, s) ⟹ u
hT₂ : (T₂, u) ⟹ t
⊢ (S₂, s) ⟹ ?m.68939 hT s t u hS₂ hT₂

S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
⊢ T₁ ~ T₂ → (s t u : State) → (S₂, s) ⟹ u → (T₂, u) ⟹ t → State

State before:
case mpr.seq.hS
S₁ S₂ T₁ T₂ : Stmt
hS✝ : S₁ ~ S₂
hS : ∀ (s t : State), (S₁, s) ⟹ t ↔ (S₂, s) ⟹ t
hT : T₁ ~ T₂
s t u : State
hS₂ : (S₂, s) ⟹ u
hT₂ : (T₂, u) ⟹ t
⊢ (S₂, s) ⟹ ?m.68939 hT s t u hS₂ hT₂

S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
⊢ T₁ ~ T₂ → (s t u : State) → (S₂, s) ⟹ u → (T₂, u) ⟹ t → State
Tactic:
assumption
State after:
no goals

State before:
case mpr.seq.hT
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t u : State
hS₂ : (S₂, s) ⟹ u
hT₂ : (T₂, u) ⟹ t
⊢ (T₁, u) ⟹ t
Tactic:
rw [BigStepEquiv] at hT
State after:
case mpr.seq.hT
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : ∀ (s t : State), (T₁, s) ⟹ t ↔ (T₂, s) ⟹ t
s t u : State
hS₂ : (S₂, s) ⟹ u
hT₂ : (T₂, u) ⟹ t
⊢ (T₁, u) ⟹ t

State before:
case mpr.seq.hT
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : ∀ (s t : State), (T₁, s) ⟹ t ↔ (T₂, s) ⟹ t
s t u : State
hS₂ : (S₂, s) ⟹ u
hT₂ : (T₂, u) ⟹ t
⊢ (T₁, u) ⟹ t
Tactic:
rw [hT]
State after:
case mpr.seq.hT
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : ∀ (s t : State), (T₁, s) ⟹ t ↔ (T₂, s) ⟹ t
s t u : State
hS₂ : (S₂, s) ⟹ u
hT₂ : (T₂, u) ⟹ t
⊢ (T₂, u) ⟹ t

State before:
case mpr.seq.hT
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : ∀ (s t : State), (T₁, s) ⟹ t ↔ (T₂, s) ⟹ t
s t u : State
hS₂ : (S₂, s) ⟹ u
hT₂ : (T₂, u) ⟹ t
⊢ (T₂, u) ⟹ t
Tactic:
assumption
State after:
no goals