internlm/Lean-Github huggingface dataset:
Theorem: LoVe.BigStepEquiv.seq_congr
Proof 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]
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₂

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 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
Proof state after:
no goals
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
Proof 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
Theorem: LoVe.BigStepEquiv.seq_congr
Proof 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]
Proof 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
Theorem: LoVe.BigStepEquiv.seq_congr
Proof 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
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
⊢ Stmt.ifThenElse B S₁ T₁ ~ Stmt.ifThenElse B S₂ T₂
Tactic:
intro s t
Proof state after:
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
⊢ (Stmt.ifThenElse B S₁ T₁, s) ⟹ t ↔ (Stmt.ifThenElse B S₂ T₂, s) ⟹ t
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
⊢ (Stmt.ifThenElse B S₁ T₁, s) ⟹ t ↔ (Stmt.ifThenElse B S₂ T₂, s) ⟹ t
Tactic:
apply Iff.intro
Proof state after:
case mp
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
⊢ (Stmt.ifThenElse B S₁ T₁, s) ⟹ t → (Stmt.ifThenElse B S₂ T₂, s) ⟹ t

case mpr
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
⊢ (Stmt.ifThenElse B S₂ T₂, s) ⟹ t → (Stmt.ifThenElse B S₁ T₁, s) ⟹ t
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
case mp
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
⊢ (Stmt.ifThenElse B S₁ T₁, s) ⟹ t → (Stmt.ifThenElse B S₂ T₂, s) ⟹ t

case mpr
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
⊢ (Stmt.ifThenElse B S₂ T₂, s) ⟹ t → (Stmt.ifThenElse B S₁ T₁, s) ⟹ t
Tactic:
{ intro hif
  cases hif with
  | if_true _ _ _ _ _ hB hS₁ =>
    apply BigStep.if_true
    { assumption }
    { rw [BigStepEquiv] at hS
      rw [← hS]
      assumption }
  | if_false _ _ _ _ _ hB hT₁ =>
    apply BigStep.if_false
    { assumption }
    { rw [BigStepEquiv] at hT
      rw [← hT]
      assumption } }
Proof state after:
case mpr
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
⊢ (Stmt.ifThenElse B S₂ T₂, s) ⟹ t → (Stmt.ifThenElse B S₁ T₁, s) ⟹ t
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
case mpr
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
⊢ (Stmt.ifThenElse B S₂ T₂, s) ⟹ t → (Stmt.ifThenElse B S₁ T₁, s) ⟹ t
Tactic:
{ intro hif
  cases hif with
  | if_true _ _ _ _ _ hB hS₂ =>
    apply BigStep.if_true
    { assumption }
    { rw [BigStepEquiv] at hS
      rw [hS]
      assumption }
  | if_false _ _ _ _ _ hB hT₂ =>
    apply BigStep.if_false
    { assumption }
    { rw [BigStepEquiv] at hT
      rw [hT]
      assumption } }
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
case mp
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
⊢ (Stmt.ifThenElse B S₁ T₁, s) ⟹ t → (Stmt.ifThenElse B S₂ T₂, s) ⟹ t
Tactic:
intro hif
Proof state after:
case mp
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hif : (Stmt.ifThenElse B S₁ T₁, s) ⟹ t
⊢ (Stmt.ifThenElse B S₂ T₂, s) ⟹ t
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
case mp
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hif : (Stmt.ifThenElse B S₁ T₁, s) ⟹ t
⊢ (Stmt.ifThenElse B S₂ T₂, s) ⟹ t
Tactic:
cases hif with
| if_true _ _ _ _ _ hB hS₁ =>
  apply BigStep.if_true
  { assumption }
  { rw [BigStepEquiv] at hS
    rw [← hS]
    assumption }
| if_false _ _ _ _ _ hB hT₁ =>
  apply BigStep.if_false
  { assumption }
  { rw [BigStepEquiv] at hT
    rw [← hT]
    assumption }
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
case mp.if_true
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₁ : (S₁, s) ⟹ t
⊢ (Stmt.ifThenElse B S₂ T₂, s) ⟹ t
Tactic:
apply BigStep.if_true
Proof state after:
case mp.if_true.hcond
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₁ : (S₁, s) ⟹ t
⊢ B s

case mp.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₁ : (S₁, s) ⟹ t
⊢ (S₂, s) ⟹ t
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
case mp.if_true.hcond
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₁ : (S₁, s) ⟹ t
⊢ B s

case mp.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₁ : (S₁, s) ⟹ t
⊢ (S₂, s) ⟹ t
Tactic:
{ assumption }
Proof state after:
case mp.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₁ : (S₁, s) ⟹ t
⊢ (S₂, s) ⟹ t
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
case mp.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₁ : (S₁, s) ⟹ t
⊢ (S₂, s) ⟹ t
Tactic:
{ rw [BigStepEquiv] at hS
  rw [← hS]
  assumption }
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
case mp.if_true.hcond
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₁ : (S₁, s) ⟹ t
⊢ B s
Tactic:
assumption
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
case mp.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₁ : (S₁, s) ⟹ t
⊢ (S₂, s) ⟹ t
Tactic:
rw [BigStepEquiv] at hS
Proof state after:
case mp.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : ∀ (s t : State), (S₁, s) ⟹ t ↔ (S₂, s) ⟹ t
hT : T₁ ~ T₂
s t : State
hB : B s
hS₁ : (S₁, s) ⟹ t
⊢ (S₂, s) ⟹ t
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
case mp.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : ∀ (s t : State), (S₁, s) ⟹ t ↔ (S₂, s) ⟹ t
hT : T₁ ~ T₂
s t : State
hB : B s
hS₁ : (S₁, s) ⟹ t
⊢ (S₂, s) ⟹ t
Tactic:
rw [← hS]
Proof state after:
case mp.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : ∀ (s t : State), (S₁, s) ⟹ t ↔ (S₂, s) ⟹ t
hT : T₁ ~ T₂
s t : State
hB : B s
hS₁ : (S₁, s) ⟹ t
⊢ (S₁, s) ⟹ t
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
case mp.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : ∀ (s t : State), (S₁, s) ⟹ t ↔ (S₂, s) ⟹ t
hT : T₁ ~ T₂
s t : State
hB : B s
hS₁ : (S₁, s) ⟹ t
⊢ (S₁, s) ⟹ t
Tactic:
assumption
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
case mp.if_false
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₁ : (T₁, s) ⟹ t
⊢ (Stmt.ifThenElse B S₂ T₂, s) ⟹ t
Tactic:
apply BigStep.if_false
Proof state after:
case mp.if_false.hcond
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₁ : (T₁, s) ⟹ t
⊢ ¬B s

case mp.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₁ : (T₁, s) ⟹ t
⊢ (T₂, s) ⟹ t
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
case mp.if_false.hcond
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₁ : (T₁, s) ⟹ t
⊢ ¬B s

case mp.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₁ : (T₁, s) ⟹ t
⊢ (T₂, s) ⟹ t
Tactic:
{ assumption }
Proof state after:
case mp.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₁ : (T₁, s) ⟹ t
⊢ (T₂, s) ⟹ t
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
case mp.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₁ : (T₁, s) ⟹ t
⊢ (T₂, s) ⟹ t
Tactic:
{ rw [BigStepEquiv] at hT
  rw [← hT]
  assumption }
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
case mp.if_false.hcond
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₁ : (T₁, s) ⟹ t
⊢ ¬B s
Tactic:
assumption
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
case mp.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₁ : (T₁, s) ⟹ t
⊢ (T₂, s) ⟹ t
Tactic:
rw [BigStepEquiv] at hT
Proof state after:
case mp.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : ∀ (s t : State), (T₁, s) ⟹ t ↔ (T₂, s) ⟹ t
s t : State
hB : ¬B s
hT₁ : (T₁, s) ⟹ t
⊢ (T₂, s) ⟹ t
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
case mp.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : ∀ (s t : State), (T₁, s) ⟹ t ↔ (T₂, s) ⟹ t
s t : State
hB : ¬B s
hT₁ : (T₁, s) ⟹ t
⊢ (T₂, s) ⟹ t
Tactic:
rw [← hT]
Proof state after:
case mp.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : ∀ (s t : State), (T₁, s) ⟹ t ↔ (T₂, s) ⟹ t
s t : State
hB : ¬B s
hT₁ : (T₁, s) ⟹ t
⊢ (T₁, s) ⟹ t
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
case mp.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : ∀ (s t : State), (T₁, s) ⟹ t ↔ (T₂, s) ⟹ t
s t : State
hB : ¬B s
hT₁ : (T₁, s) ⟹ t
⊢ (T₁, s) ⟹ t
Tactic:
assumption
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
case mpr
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
⊢ (Stmt.ifThenElse B S₂ T₂, s) ⟹ t → (Stmt.ifThenElse B S₁ T₁, s) ⟹ t
Tactic:
intro hif
Proof state after:
case mpr
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hif : (Stmt.ifThenElse B S₂ T₂, s) ⟹ t
⊢ (Stmt.ifThenElse B S₁ T₁, s) ⟹ t
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
case mpr
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hif : (Stmt.ifThenElse B S₂ T₂, s) ⟹ t
⊢ (Stmt.ifThenElse B S₁ T₁, s) ⟹ t
Tactic:
cases hif with
| if_true _ _ _ _ _ hB hS₂ =>
  apply BigStep.if_true
  { assumption }
  { rw [BigStepEquiv] at hS
    rw [hS]
    assumption }
| if_false _ _ _ _ _ hB hT₂ =>
  apply BigStep.if_false
  { assumption }
  { rw [BigStepEquiv] at hT
    rw [hT]
    assumption }
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
case mpr.if_true
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₂ : (S₂, s) ⟹ t
⊢ (Stmt.ifThenElse B S₁ T₁, s) ⟹ t
Tactic:
apply BigStep.if_true
Proof state after:
case mpr.if_true.hcond
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₂ : (S₂, s) ⟹ t
⊢ B s

case mpr.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₂ : (S₂, s) ⟹ t
⊢ (S₁, s) ⟹ t
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
case mpr.if_true.hcond
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₂ : (S₂, s) ⟹ t
⊢ B s

case mpr.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₂ : (S₂, s) ⟹ t
⊢ (S₁, s) ⟹ t
Tactic:
{ assumption }
Proof state after:
case mpr.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₂ : (S₂, s) ⟹ t
⊢ (S₁, s) ⟹ t
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
case mpr.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₂ : (S₂, s) ⟹ t
⊢ (S₁, s) ⟹ t
Tactic:
{ rw [BigStepEquiv] at hS
  rw [hS]
  assumption }
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
case mpr.if_true.hcond
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₂ : (S₂, s) ⟹ t
⊢ B s
Tactic:
assumption
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
case mpr.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : B s
hS₂ : (S₂, s) ⟹ t
⊢ (S₁, s) ⟹ t
Tactic:
rw [BigStepEquiv] at hS
Proof state after:
case mpr.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : ∀ (s t : State), (S₁, s) ⟹ t ↔ (S₂, s) ⟹ t
hT : T₁ ~ T₂
s t : State
hB : B s
hS₂ : (S₂, s) ⟹ t
⊢ (S₁, s) ⟹ t
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
case mpr.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : ∀ (s t : State), (S₁, s) ⟹ t ↔ (S₂, s) ⟹ t
hT : T₁ ~ T₂
s t : State
hB : B s
hS₂ : (S₂, s) ⟹ t
⊢ (S₁, s) ⟹ t
Tactic:
rw [hS]
Proof state after:
case mpr.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : ∀ (s t : State), (S₁, s) ⟹ t ↔ (S₂, s) ⟹ t
hT : T₁ ~ T₂
s t : State
hB : B s
hS₂ : (S₂, s) ⟹ t
⊢ (S₂, s) ⟹ t
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
case mpr.if_true.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : ∀ (s t : State), (S₁, s) ⟹ t ↔ (S₂, s) ⟹ t
hT : T₁ ~ T₂
s t : State
hB : B s
hS₂ : (S₂, s) ⟹ t
⊢ (S₂, s) ⟹ t
Tactic:
assumption
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
case mpr.if_false
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₂ : (T₂, s) ⟹ t
⊢ (Stmt.ifThenElse B S₁ T₁, s) ⟹ t
Tactic:
apply BigStep.if_false
Proof state after:
case mpr.if_false.hcond
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₂ : (T₂, s) ⟹ t
⊢ ¬B s

case mpr.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₂ : (T₂, s) ⟹ t
⊢ (T₁, s) ⟹ t
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
case mpr.if_false.hcond
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₂ : (T₂, s) ⟹ t
⊢ ¬B s

case mpr.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₂ : (T₂, s) ⟹ t
⊢ (T₁, s) ⟹ t
Tactic:
{ assumption }
Proof state after:
case mpr.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₂ : (T₂, s) ⟹ t
⊢ (T₁, s) ⟹ t
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
case mpr.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₂ : (T₂, s) ⟹ t
⊢ (T₁, s) ⟹ t
Tactic:
{ rw [BigStepEquiv] at hT
  rw [hT]
  assumption }
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
case mpr.if_false.hcond
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₂ : (T₂, s) ⟹ t
⊢ ¬B s
Tactic:
assumption
Proof state after:
no goals
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
case mpr.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : T₁ ~ T₂
s t : State
hB : ¬B s
hT₂ : (T₂, s) ⟹ t
⊢ (T₁, s) ⟹ t
Tactic:
rw [BigStepEquiv] at hT
Proof state after:
case mpr.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : ∀ (s t : State), (T₁, s) ⟹ t ↔ (T₂, s) ⟹ t
s t : State
hB : ¬B s
hT₂ : (T₂, s) ⟹ t
⊢ (T₁, s) ⟹ t
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
case mpr.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : ∀ (s t : State), (T₁, s) ⟹ t ↔ (T₂, s) ⟹ t
s t : State
hB : ¬B s
hT₂ : (T₂, s) ⟹ t
⊢ (T₁, s) ⟹ t
Tactic:
rw [hT]
Proof state after:
case mpr.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : ∀ (s t : State), (T₁, s) ⟹ t ↔ (T₂, s) ⟹ t
s t : State
hB : ¬B s
hT₂ : (T₂, s) ⟹ t
⊢ (T₂, s) ⟹ t
Theorem: LoVe.BigStepEquiv.if_congr
Proof state before:
case mpr.if_false.hbody
B : State → Prop
S₁ S₂ T₁ T₂ : Stmt
hS : S₁ ~ S₂
hT : ∀ (s t : State), (T₁, s) ⟹ t ↔ (T₂, s) ⟹ t
s t : State
hB : ¬B s
hT₂ : (T₂, s) ⟹ t
⊢ (T₂, s) ⟹ t
Tactic:
assumption
Proof state after:
no goals
Theorem: LoVe.FnExp.preservation
Proof state before:
e e' : FnExp
τ : FnType
⊢ e ∶ τ → e ⇒ e' → e' ∶ τ
Tactic:
intro htp hstep
Proof state after:
e e' : FnExp
τ : FnType
htp : e ∶ τ
hstep : e ⇒ e'
⊢ e' ∶ τ
Theorem: LoVe.FnExp.preservation
Proof state before:
e e' : FnExp
τ : FnType
htp : e ∶ τ
hstep : e ⇒ e'
⊢ e' ∶ τ
Tactic:
induction hstep generalizing τ with
| @appArg f f' x h ih =>
  cases htp with
  | appZero hf hx =>
    apply HasType.appZero
    . exact ih hf
    . exact hx
  | @appSucc _ _ n hf hx =>
    apply HasType.appSucc
    . exact ih hf
    . exact hx
| @appZero x =>
  cases htp with
  | appZero => assumption
  | appSucc hf hx => cases hf
| @appSucc _ n =>
  cases htp with
  | appZero hf hx => cases hf
  | appSucc hf hx =>
    cases hf
    exact HasType.fn
Proof state after:
no goals
Theorem: LoVe.FnExp.preservation
Proof state before:
case appArg
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
τ : FnType
htp : app f x ∶ τ
⊢ app f' x ∶ τ
Tactic:
cases htp with
| appZero hf hx =>
  apply HasType.appZero
  . exact ih hf
  . exact hx
| @appSucc _ _ n hf hx =>
  apply HasType.appSucc
  . exact ih hf
  . exact hx
Proof state after:
no goals
Theorem: LoVe.FnExp.preservation
Proof state before:
case appArg.appZero
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
hf : f ∶ function 0
hx : x ∶ argument
⊢ app f' x ∶ argument
Tactic:
apply HasType.appZero
Proof state after:
case appArg.appZero.a
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
hf : f ∶ function 0
hx : x ∶ argument
⊢ f' ∶ function 0

case appArg.appZero.a
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
hf : f ∶ function 0
hx : x ∶ argument
⊢ x ∶ argument
Theorem: LoVe.FnExp.preservation
Proof state before:
case appArg.appZero.a
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
hf : f ∶ function 0
hx : x ∶ argument
⊢ f' ∶ function 0

case appArg.appZero.a
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
hf : f ∶ function 0
hx : x ∶ argument
⊢ x ∶ argument
Tactic:
. exact ih hf
Proof state after:
case appArg.appZero.a
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
hf : f ∶ function 0
hx : x ∶ argument
⊢ x ∶ argument
Theorem: LoVe.FnExp.preservation
Proof state before:
case appArg.appZero.a
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
hf : f ∶ function 0
hx : x ∶ argument
⊢ x ∶ argument
Tactic:
. exact hx
Proof state after:
no goals
Theorem: LoVe.FnExp.preservation
Proof state before:
case appArg.appZero.a
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
hf : f ∶ function 0
hx : x ∶ argument
⊢ f' ∶ function 0
Tactic:
exact ih hf
Proof state after:
no goals
Theorem: LoVe.FnExp.preservation
Proof state before:
case appArg.appZero.a
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
hf : f ∶ function 0
hx : x ∶ argument
⊢ x ∶ argument
Tactic:
exact hx
Proof state after:
no goals
Theorem: LoVe.FnExp.preservation
Proof state before:
case appArg.appSucc
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
⊢ app f' x ∶ function n
Tactic:
apply HasType.appSucc
Proof state after:
case appArg.appSucc.a
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
⊢ f' ∶ function (Nat.succ n)

case appArg.appSucc.a
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
⊢ x ∶ argument
Theorem: LoVe.FnExp.preservation
Proof state before:
case appArg.appSucc.a
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
⊢ f' ∶ function (Nat.succ n)

case appArg.appSucc.a
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
⊢ x ∶ argument
Tactic:
. exact ih hf
Proof state after:
case appArg.appSucc.a
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
⊢ x ∶ argument
Theorem: LoVe.FnExp.preservation
Proof state before:
case appArg.appSucc.a
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
⊢ x ∶ argument
Tactic:
. exact hx
Proof state after:
no goals
Theorem: LoVe.FnExp.preservation
Proof state before:
case appArg.appSucc.a
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
⊢ f' ∶ function (Nat.succ n)
Tactic:
exact ih hf
Proof state after:
no goals
Theorem: LoVe.FnExp.preservation
Proof state before:
case appArg.appSucc.a
e e' f f' x : FnExp
h : f ⇒ f'
ih : ∀ {τ : FnType}, f ∶ τ → f' ∶ τ
n : ℕ
hf : f ∶ function (Nat.succ n)
hx : x ∶ argument
⊢ x ∶ argument
Tactic:
exact hx
Proof state after:
no goals
Theorem: LoVe.FnExp.preservation
Proof state before:
case appZero
e e' x : FnExp
τ : FnType
htp : app (fn 0) x ∶ τ
⊢ x ∶ τ
Tactic:
cases htp with
| appZero => assumption
| appSucc hf hx => cases hf
Proof state after:
no goals
Theorem: LoVe.FnExp.preservation
Proof state before:
case appZero.appZero
e e' x : FnExp
a✝¹ : fn 0 ∶ function 0
a✝ : x ∶ argument
⊢ x ∶ argument
Tactic:
assumption
Proof state after:
no goals
Theorem: LoVe.FnExp.preservation
Proof state before:
case appZero.appSucc
e e' x : FnExp
n✝ : ℕ
hf : fn 0 ∶ function (Nat.succ n✝)
hx : x ∶ argument
⊢ x ∶ function n✝
Tactic:
cases hf
Proof state after:
no goals
Theorem: LoVe.FnExp.preservation
Proof state before:
case appSucc
e e' x✝ : FnExp
n : ℕ
τ : FnType
htp : app (fn (Nat.succ n)) x✝ ∶ τ
⊢ fn n ∶ τ
Tactic:
cases htp with
| appZero hf hx => cases hf
| appSucc hf hx =>
  cases hf
  exact HasType.fn
Proof state after:
no goals
Theorem: LoVe.FnExp.preservation
Proof state before:
case appSucc.appZero
e e' x✝ : FnExp
n : ℕ
hf : fn (Nat.succ n) ∶ function 0
hx : x✝ ∶ argument
⊢ fn n ∶ argument
Tactic:
cases hf
Proof state after:
no goals
Theorem: LoVe.FnExp.preservation
Proof state before:
case appSucc.appSucc
e e' x✝ : FnExp
n n✝ : ℕ
hf : fn (Nat.succ n) ∶ function (Nat.succ n✝)
hx : x✝ ∶ argument
⊢ fn n ∶ function n✝
Tactic:
cases hf
Proof state after:
case appSucc.appSucc.fn
e e' x✝ : FnExp
n : ℕ
hx : x✝ ∶ argument
⊢ fn n ∶ function n
Theorem: LoVe.FnExp.preservation
Proof state before:
case appSucc.appSucc.fn
e e' x✝ : FnExp
n : ℕ
hx : x✝ ∶ argument
⊢ fn n ∶ function n
Tactic:
exact HasType.fn
Proof state after:
no goals
Theorem: LoVe.FnExp.progress
Proof state before:
e : FnExp
τ : FnType
⊢ e ∶ τ → Value e ∨ ∃ e', e ⇒ e'
Tactic:
intro htp
Proof state after:
e : FnExp
τ : FnType
htp : e ∶ τ
⊢ Value e ∨ ∃ e', e ⇒ e'