internlm/Lean-Github huggingface dataset:
Theorem: LoVe.BigStepEquiv.skip_assign_id
Proof state before:
case mpr
x : String
s t : State
hskip : (Stmt.skip, s) ⟹ t
⊢ (Stmt.assign x fun s => s x, s) ⟹ t
Tactic:
cases hskip
Proof state after:
case mpr.skip
x : String
s : State
⊢ (Stmt.assign x fun s => s x, s) ⟹ s
Theorem: LoVe.BigStepEquiv.skip_assign_id
Proof state before:
case mpr.skip
x : String
s : State
⊢ (Stmt.assign x fun s => s x, s) ⟹ s
Tactic:
simp [*]
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.seq_skip_left
Proof state before:
S : Stmt
⊢ Stmt.skip; S ~ S
Tactic:
intro s t
Proof state after:
S : Stmt
s t : State
⊢ (Stmt.skip; S, s) ⟹ t ↔ (S, s) ⟹ t
Theorem: LoVe.BigStepEquiv.seq_skip_left
Proof state before:
S : Stmt
s t : State
⊢ (Stmt.skip; S, s) ⟹ t ↔ (S, s) ⟹ t
Tactic:
apply Iff.intro
Proof state after:
case mp
S : Stmt
s t : State
⊢ (Stmt.skip; S, s) ⟹ t → (S, s) ⟹ t

case mpr
S : Stmt
s t : State
⊢ (S, s) ⟹ t → (Stmt.skip; S, s) ⟹ t
Theorem: LoVe.BigStepEquiv.seq_skip_left
Proof state before:
case mp
S : Stmt
s t : State
⊢ (Stmt.skip; S, s) ⟹ t → (S, s) ⟹ t

case mpr
S : Stmt
s t : State
⊢ (S, s) ⟹ t → (Stmt.skip; S, s) ⟹ t
Tactic:
{ intro hseq
  cases hseq with
  | seq _ _ _ u _ hs hS =>
    cases hs
    assumption }
Proof state after:
case mpr
S : Stmt
s t : State
⊢ (S, s) ⟹ t → (Stmt.skip; S, s) ⟹ t
Theorem: LoVe.BigStepEquiv.seq_skip_left
Proof state before:
case mpr
S : Stmt
s t : State
⊢ (S, s) ⟹ t → (Stmt.skip; S, s) ⟹ t
Tactic:
{ intro hS
  apply BigStep.seq
  { apply BigStep.skip }
  { assumption } }
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.seq_skip_left
Proof state before:
case mp
S : Stmt
s t : State
⊢ (Stmt.skip; S, s) ⟹ t → (S, s) ⟹ t
Tactic:
intro hseq
Proof state after:
case mp
S : Stmt
s t : State
hseq : (Stmt.skip; S, s) ⟹ t
⊢ (S, s) ⟹ t
Theorem: LoVe.BigStepEquiv.seq_skip_left
Proof state before:
case mp
S : Stmt
s t : State
hseq : (Stmt.skip; S, s) ⟹ t
⊢ (S, s) ⟹ t
Tactic:
cases hseq with
| seq _ _ _ u _ hs hS =>
  cases hs
  assumption
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.seq_skip_left
Proof state before:
case mp.seq
S : Stmt
s t u : State
hs : (Stmt.skip, s) ⟹ u
hS : (S, u) ⟹ t
⊢ (S, s) ⟹ t
Tactic:
cases hs
Proof state after:
case mp.seq.skip
S : Stmt
s t : State
hS : (S, s) ⟹ t
⊢ (S, s) ⟹ t
Theorem: LoVe.BigStepEquiv.seq_skip_left
Proof state before:
case mp.seq.skip
S : Stmt
s t : State
hS : (S, s) ⟹ t
⊢ (S, s) ⟹ t
Tactic:
assumption
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.seq_skip_left
Proof state before:
case mpr
S : Stmt
s t : State
⊢ (S, s) ⟹ t → (Stmt.skip; S, s) ⟹ t
Tactic:
intro hS
Proof state after:
case mpr
S : Stmt
s t : State
hS : (S, s) ⟹ t
⊢ (Stmt.skip; S, s) ⟹ t
Theorem: LoVe.BigStepEquiv.seq_skip_left
Proof state before:
case mpr
S : Stmt
s t : State
hS : (S, s) ⟹ t
⊢ (Stmt.skip; S, s) ⟹ t
Tactic:
apply BigStep.seq
Proof state after:
case mpr.hS
S : Stmt
s t : State
hS : (S, s) ⟹ t
⊢ (Stmt.skip, s) ⟹ ?mpr.t

case mpr.hT
S : Stmt
s t : State
hS : (S, s) ⟹ t
⊢ (S, ?mpr.t) ⟹ t

case mpr.t
S : Stmt
s t : State
hS : (S, s) ⟹ t
⊢ State
Theorem: LoVe.BigStepEquiv.seq_skip_left
Proof state before:
case mpr.hS
S : Stmt
s t : State
hS : (S, s) ⟹ t
⊢ (Stmt.skip, s) ⟹ ?mpr.t

case mpr.hT
S : Stmt
s t : State
hS : (S, s) ⟹ t
⊢ (S, ?mpr.t) ⟹ t

case mpr.t
S : Stmt
s t : State
hS : (S, s) ⟹ t
⊢ State
Tactic:
{ apply BigStep.skip }
Proof state after:
case mpr.hT
S : Stmt
s t : State
hS : (S, s) ⟹ t
⊢ (S, s) ⟹ t
Theorem: LoVe.BigStepEquiv.seq_skip_left
Proof state before:
case mpr.hT
S : Stmt
s t : State
hS : (S, s) ⟹ t
⊢ (S, s) ⟹ t
Tactic:
{ assumption }
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.seq_skip_left
Proof state before:
case mpr.hS
S : Stmt
s t : State
hS : (S, s) ⟹ t
⊢ (Stmt.skip, s) ⟹ ?mpr.t
Tactic:
apply BigStep.skip
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.seq_skip_left
Proof state before:
case mpr.hT
S : Stmt
s t : State
hS : (S, s) ⟹ t
⊢ (S, s) ⟹ t
Tactic:
assumption
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.seq_skip_right
Proof state before:
S : Stmt
⊢ S; Stmt.skip ~ S
Tactic:
intro s t
Proof state after:
S : Stmt
s t : State
⊢ (S; Stmt.skip, s) ⟹ t ↔ (S, s) ⟹ t
Theorem: LoVe.BigStepEquiv.seq_skip_right
Proof state before:
S : Stmt
s t : State
⊢ (S; Stmt.skip, s) ⟹ t ↔ (S, s) ⟹ t
Tactic:
apply Iff.intro
Proof state after:
case mp
S : Stmt
s t : State
⊢ (S; Stmt.skip, s) ⟹ t → (S, s) ⟹ t

case mpr
S : Stmt
s t : State
⊢ (S, s) ⟹ t → (S; Stmt.skip, s) ⟹ t
Theorem: LoVe.BigStepEquiv.seq_skip_right
Proof state before:
case mp
S : Stmt
s t : State
⊢ (S; Stmt.skip, s) ⟹ t → (S, s) ⟹ t

case mpr
S : Stmt
s t : State
⊢ (S, s) ⟹ t → (S; Stmt.skip, s) ⟹ t
Tactic:
{ intro hseq
  cases hseq with
  | seq _ _ _ u _ hS hs =>
    cases hs
    assumption }
Proof state after:
case mpr
S : Stmt
s t : State
⊢ (S, s) ⟹ t → (S; Stmt.skip, s) ⟹ t
Theorem: LoVe.BigStepEquiv.seq_skip_right
Proof state before:
case mpr
S : Stmt
s t : State
⊢ (S, s) ⟹ t → (S; Stmt.skip, s) ⟹ t
Tactic:
{ intro h
  apply BigStep.seq
  { assumption }
  { apply BigStep.skip } }
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.seq_skip_right
Proof state before:
case mp
S : Stmt
s t : State
⊢ (S; Stmt.skip, s) ⟹ t → (S, s) ⟹ t
Tactic:
intro hseq
Proof state after:
case mp
S : Stmt
s t : State
hseq : (S; Stmt.skip, s) ⟹ t
⊢ (S, s) ⟹ t
Theorem: LoVe.BigStepEquiv.seq_skip_right
Proof state before:
case mp
S : Stmt
s t : State
hseq : (S; Stmt.skip, s) ⟹ t
⊢ (S, s) ⟹ t
Tactic:
cases hseq with
| seq _ _ _ u _ hS hs =>
  cases hs
  assumption
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.seq_skip_right
Proof state before:
case mp.seq
S : Stmt
s t u : State
hS : (S, s) ⟹ u
hs : (Stmt.skip, u) ⟹ t
⊢ (S, s) ⟹ t
Tactic:
cases hs
Proof state after:
case mp.seq.skip
S : Stmt
s t : State
hS : (S, s) ⟹ t
⊢ (S, s) ⟹ t
Theorem: LoVe.BigStepEquiv.seq_skip_right
Proof state before:
case mp.seq.skip
S : Stmt
s t : State
hS : (S, s) ⟹ t
⊢ (S, s) ⟹ t
Tactic:
assumption
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.seq_skip_right
Proof state before:
case mpr
S : Stmt
s t : State
⊢ (S, s) ⟹ t → (S; Stmt.skip, s) ⟹ t
Tactic:
intro h
Proof state after:
case mpr
S : Stmt
s t : State
h : (S, s) ⟹ t
⊢ (S; Stmt.skip, s) ⟹ t
Theorem: LoVe.BigStepEquiv.seq_skip_right
Proof state before:
case mpr
S : Stmt
s t : State
h : (S, s) ⟹ t
⊢ (S; Stmt.skip, s) ⟹ t
Tactic:
apply BigStep.seq
Proof state after:
case mpr.hS
S : Stmt
s t : State
h : (S, s) ⟹ t
⊢ (S, s) ⟹ ?mpr.t

case mpr.hT
S : Stmt
s t : State
h : (S, s) ⟹ t
⊢ (Stmt.skip, ?mpr.t) ⟹ t

case mpr.t
S : Stmt
s t : State
h : (S, s) ⟹ t
⊢ State
Theorem: LoVe.BigStepEquiv.seq_skip_right
Proof state before:
case mpr.hS
S : Stmt
s t : State
h : (S, s) ⟹ t
⊢ (S, s) ⟹ ?mpr.t

case mpr.hT
S : Stmt
s t : State
h : (S, s) ⟹ t
⊢ (Stmt.skip, ?mpr.t) ⟹ t

case mpr.t
S : Stmt
s t : State
h : (S, s) ⟹ t
⊢ State
Tactic:
{ assumption }
Proof state after:
case mpr.hT
S : Stmt
s t : State
h : (S, s) ⟹ t
⊢ (Stmt.skip, t) ⟹ t
Theorem: LoVe.BigStepEquiv.seq_skip_right
Proof state before:
case mpr.hT
S : Stmt
s t : State
h : (S, s) ⟹ t
⊢ (Stmt.skip, t) ⟹ t
Tactic:
{ apply BigStep.skip }
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.seq_skip_right
Proof state before:
case mpr.hS
S : Stmt
s t : State
h : (S, s) ⟹ t
⊢ (S, s) ⟹ ?mpr.t
Tactic:
assumption
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.seq_skip_right
Proof state before:
case mpr.hT
S : Stmt
s t : State
h : (S, s) ⟹ t
⊢ (Stmt.skip, t) ⟹ t
Tactic:
apply BigStep.skip
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.if_seq_while_skip
Proof state before:
B : State → Prop
S : Stmt
⊢ Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip ~ Stmt.whileDo B S
Tactic:
intro s t
Proof state after:
B : State → Prop
S : Stmt
s t : State
⊢ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ t ↔ (Stmt.whileDo B S, s) ⟹ t
Theorem: LoVe.BigStepEquiv.if_seq_while_skip
Proof state before:
B : State → Prop
S : Stmt
s t : State
⊢ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ t ↔ (Stmt.whileDo B S, s) ⟹ t
Tactic:
apply Iff.intro
Proof state after:
case mp
B : State → Prop
S : Stmt
s t : State
⊢ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ t → (Stmt.whileDo B S, s) ⟹ t

case mpr
B : State → Prop
S : Stmt
s t : State
⊢ (Stmt.whileDo B S, s) ⟹ t → (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ t
Theorem: LoVe.BigStepEquiv.if_seq_while_skip
Proof state before:
case mp
B : State → Prop
S : Stmt
s t : State
⊢ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ t → (Stmt.whileDo B S, s) ⟹ t

case mpr
B : State → Prop
S : Stmt
s t : State
⊢ (Stmt.whileDo B S, s) ⟹ t → (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ t
Tactic:
{ intro hif
  cases hif with
  | if_true _ _ _ _ _ hB hseq =>
    cases hseq with
    | seq _ _ _ u _ hS hT =>
      apply BigStep.while_true <;>
        assumption
  | if_false _ _ _ _ _ hB hskip =>
    cases hskip
    apply BigStep.while_false
    assumption }
Proof state after:
case mpr
B : State → Prop
S : Stmt
s t : State
⊢ (Stmt.whileDo B S, s) ⟹ t → (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ t
Theorem: LoVe.BigStepEquiv.if_seq_while_skip
Proof state before:
case mpr
B : State → Prop
S : Stmt
s t : State
⊢ (Stmt.whileDo B S, s) ⟹ t → (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ t
Tactic:
{ intro hwhile
  cases hwhile with
  | while_true _ _ _ u _ hB hS hw =>
    apply BigStep.if_true
    exact hB
    apply BigStep.seq <;>
      assumption
  | while_false _ _ _ hB =>
    apply BigStep.if_false
    exact hB
    apply BigStep.skip }
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.if_seq_while_skip
Proof state before:
case mp
B : State → Prop
S : Stmt
s t : State
⊢ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ t → (Stmt.whileDo B S, s) ⟹ t
Tactic:
intro hif
Proof state after:
case mp
B : State → Prop
S : Stmt
s t : State
hif : (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ t
⊢ (Stmt.whileDo B S, s) ⟹ t
Theorem: LoVe.BigStepEquiv.if_seq_while_skip
Proof state before:
case mp
B : State → Prop
S : Stmt
s t : State
hif : (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ t
⊢ (Stmt.whileDo B S, s) ⟹ t
Tactic:
cases hif with
| if_true _ _ _ _ _ hB hseq =>
  cases hseq with
  | seq _ _ _ u _ hS hT =>
    apply BigStep.while_true <;>
      assumption
| if_false _ _ _ _ _ hB hskip =>
  cases hskip
  apply BigStep.while_false
  assumption
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.if_seq_while_skip
Proof state before:
case mp.if_true
B : State → Prop
S : Stmt
s t : State
hB : B s
hseq : (S; Stmt.whileDo B S, s) ⟹ t
⊢ (Stmt.whileDo B S, s) ⟹ t
Tactic:
cases hseq with
| seq _ _ _ u _ hS hT =>
  apply BigStep.while_true <;>
    assumption
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.if_seq_while_skip
Proof state before:
case mp.if_true.seq
B : State → Prop
S : Stmt
s t : State
hB : B s
u : State
hS : (S, s) ⟹ u
hT : (Stmt.whileDo B S, u) ⟹ t
⊢ (Stmt.whileDo B S, s) ⟹ t
Tactic:
apply BigStep.while_true <;>
  assumption
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.if_seq_while_skip
Proof state before:
case mp.if_false
B : State → Prop
S : Stmt
s t : State
hB : ¬B s
hskip : (Stmt.skip, s) ⟹ t
⊢ (Stmt.whileDo B S, s) ⟹ t
Tactic:
cases hskip
Proof state after:
case mp.if_false.skip
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ (Stmt.whileDo B S, s) ⟹ s
Theorem: LoVe.BigStepEquiv.if_seq_while_skip
Proof state before:
case mp.if_false.skip
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ (Stmt.whileDo B S, s) ⟹ s
Tactic:
apply BigStep.while_false
Proof state after:
case mp.if_false.skip.hcond
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ ¬B s
Theorem: LoVe.BigStepEquiv.if_seq_while_skip
Proof state before:
case mp.if_false.skip.hcond
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ ¬B s
Tactic:
assumption
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.if_seq_while_skip
Proof state before:
case mpr
B : State → Prop
S : Stmt
s t : State
⊢ (Stmt.whileDo B S, s) ⟹ t → (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ t
Tactic:
intro hwhile
Proof state after:
case mpr
B : State → Prop
S : Stmt
s t : State
hwhile : (Stmt.whileDo B S, s) ⟹ t
⊢ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ t
Theorem: LoVe.BigStepEquiv.if_seq_while_skip
Proof state before:
case mpr
B : State → Prop
S : Stmt
s t : State
hwhile : (Stmt.whileDo B S, s) ⟹ t
⊢ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ t
Tactic:
cases hwhile with
| while_true _ _ _ u _ hB hS hw =>
  apply BigStep.if_true
  exact hB
  apply BigStep.seq <;>
    assumption
| while_false _ _ _ hB =>
  apply BigStep.if_false
  exact hB
  apply BigStep.skip
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.if_seq_while_skip
Proof state before:
case mpr.while_true
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ u
hw : (Stmt.whileDo B S, u) ⟹ t
⊢ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ t
Tactic:
apply BigStep.if_true
Proof state after:
case mpr.while_true.hcond
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ u
hw : (Stmt.whileDo B S, u) ⟹ t
⊢ B s

case mpr.while_true.hbody
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ u
hw : (Stmt.whileDo B S, u) ⟹ t
⊢ (S; Stmt.whileDo B S, s) ⟹ t
Theorem: LoVe.BigStepEquiv.if_seq_while_skip
Proof state before:
case mpr.while_true.hcond
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ u
hw : (Stmt.whileDo B S, u) ⟹ t
⊢ B s

case mpr.while_true.hbody
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ u
hw : (Stmt.whileDo B S, u) ⟹ t
⊢ (S; Stmt.whileDo B S, s) ⟹ t
Tactic:
exact hB
Proof state after:
case mpr.while_true.hbody
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ u
hw : (Stmt.whileDo B S, u) ⟹ t
⊢ (S; Stmt.whileDo B S, s) ⟹ t
Theorem: LoVe.BigStepEquiv.if_seq_while_skip
Proof state before:
case mpr.while_true.hbody
B : State → Prop
S : Stmt
s t u : State
hB : B s
hS : (S, s) ⟹ u
hw : (Stmt.whileDo B S, u) ⟹ t
⊢ (S; Stmt.whileDo B S, s) ⟹ t
Tactic:
apply BigStep.seq <;>
  assumption
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.if_seq_while_skip
Proof state before:
case mpr.while_false
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ (Stmt.ifThenElse B (S; Stmt.whileDo B S) Stmt.skip, s) ⟹ s
Tactic:
apply BigStep.if_false
Proof state after:
case mpr.while_false.hcond
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ ¬B s

case mpr.while_false.hbody
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ (Stmt.skip, s) ⟹ s
Theorem: LoVe.BigStepEquiv.if_seq_while_skip
Proof state before:
case mpr.while_false.hcond
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ ¬B s

case mpr.while_false.hbody
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ (Stmt.skip, s) ⟹ s
Tactic:
exact hB
Proof state after:
case mpr.while_false.hbody
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ (Stmt.skip, s) ⟹ s
Theorem: LoVe.BigStepEquiv.if_seq_while_skip
Proof state before:
case mpr.while_false.hbody
B : State → Prop
S : Stmt
s : State
hB : ¬B s
⊢ (Stmt.skip, s) ⟹ s
Tactic:
apply BigStep.skip
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.seq_congr
Proof state before:
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
⊢ S₁; T₁ ~ S₂; T₂
Tactic:
intro s t
Proof state after:
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
⊢ (S₁; T₁, s) ⟹ t ↔ (S₂; T₂, s) ⟹ t
Theorem: LoVe.BigStepEquiv.seq_congr
Proof 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
Proof 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
Theorem: LoVe.BigStepEquiv.seq_congr
Proof 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 } }
Proof 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
Theorem: LoVe.BigStepEquiv.seq_congr
Proof 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 } }
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.seq_congr
Proof 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
Proof 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
Theorem: LoVe.BigStepEquiv.seq_congr
Proof 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 }
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.seq_congr
Proof 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
Proof 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
Theorem: LoVe.BigStepEquiv.seq_congr
Proof 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 }
Proof 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
Theorem: LoVe.BigStepEquiv.seq_congr
Proof 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 }
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.seq_congr
Proof 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
Proof 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₁
Theorem: LoVe.BigStepEquiv.seq_congr
Proof 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]
Proof 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
Theorem: LoVe.BigStepEquiv.seq_congr
Proof 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
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.seq_congr
Proof 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
Proof 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
Theorem: LoVe.BigStepEquiv.seq_congr
Proof 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]
Proof 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
Theorem: LoVe.BigStepEquiv.seq_congr
Proof 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
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.seq_congr
Proof 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
Proof 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
Theorem: LoVe.BigStepEquiv.seq_congr
Proof 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 }
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.seq_congr
Proof 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
Proof 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
Theorem: LoVe.BigStepEquiv.seq_congr
Proof 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 }
Proof 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
Theorem: LoVe.BigStepEquiv.seq_congr
Proof 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 }
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.seq_congr
Proof 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
Proof 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₂