internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.UnionFind.equiv_union
Proof state before:
a b : Nat
self : UnionFind
x y : Fin (size self)
⊢ Equiv
      (link (find (find self x).fst { val := ↑y, isLt := ⋯ }).fst { val := root self ↑x, isLt := ⋯ }
        (find (find self x).fst { val := ↑y, isLt := ⋯ }).2.val ⋯)
      a b ↔
    Equiv self a b ∨ Equiv self a ↑x ∧ Equiv self (↑y) b ∨ Equiv self a ↑y ∧ Equiv self (↑x) b
Tactic:
rw [equiv_link (by simp [← root_eq_self, root_root])]
Proof state after:
a b : Nat
self : UnionFind
x y : Fin (size self)
⊢ Equiv (find (find self x).fst { val := ↑y, isLt := ⋯ }).fst a b ∨
      Equiv (find (find self x).fst { val := ↑y, isLt := ⋯ }).fst a ↑{ val := root self ↑x, isLt := ⋯ } ∧
          Equiv (find (find self x).fst { val := ↑y, isLt := ⋯ }).fst
            (↑(find (find self x).fst { val := ↑y, isLt := ⋯ }).2.val) b ∨
        Equiv (find (find self x).fst { val := ↑y, isLt := ⋯ }).fst a
            ↑(find (find self x).fst { val := ↑y, isLt := ⋯ }).2.val ∧
          Equiv (find (find self x).fst { val := ↑y, isLt := ⋯ }).fst (↑{ val := root self ↑x, isLt := ⋯ }) b ↔
    Equiv self a b ∨ Equiv self a ↑x ∧ Equiv self (↑y) b ∨ Equiv self a ↑y ∧ Equiv self (↑x) b
Theorem: Lean4Lean.UnionFind.equiv_union
Proof state before:
a b : Nat
self : UnionFind
x y : Fin (size self)
⊢ Equiv (find (find self x).fst { val := ↑y, isLt := ⋯ }).fst a b ∨
      Equiv (find (find self x).fst { val := ↑y, isLt := ⋯ }).fst a ↑{ val := root self ↑x, isLt := ⋯ } ∧
          Equiv (find (find self x).fst { val := ↑y, isLt := ⋯ }).fst
            (↑(find (find self x).fst { val := ↑y, isLt := ⋯ }).2.val) b ∨
        Equiv (find (find self x).fst { val := ↑y, isLt := ⋯ }).fst a
            ↑(find (find self x).fst { val := ↑y, isLt := ⋯ }).2.val ∧
          Equiv (find (find self x).fst { val := ↑y, isLt := ⋯ }).fst (↑{ val := root self ↑x, isLt := ⋯ }) b ↔
    Equiv self a b ∨ Equiv self a ↑x ∧ Equiv self (↑y) b ∨ Equiv self a ↑y ∧ Equiv self (↑x) b
Tactic:
simp [equiv_find]
Proof state after:
no goals
Theorem: Lean4Lean.UnionFind.equiv_union
Proof state before:
a b : Nat
self : UnionFind
x y : Fin (size self)
⊢ parent (find (find self x).fst { val := ↑y, isLt := ⋯ }).fst ↑{ val := root self ↑x, isLt := ⋯ } =
    ↑{ val := root self ↑x, isLt := ⋯ }
Tactic:
simp [← root_eq_self, root_root]
Proof state after:
no goals
Theorem: Lean4Lean.ParRed.weakN
Proof state before:
E : Extra
HE : Extra.IsWeakN E
n k : Nat
Γ Γ' : List VExpr
e1 e2 : VExpr
W : Ctx.LiftN n k Γ Γ'
H : ParRed E Γ e1 e2
⊢ ParRed E Γ' (liftN n e1 k) (liftN n e2 k)
Tactic:
induction H generalizing k Γ' with
| bvar | sort | const => exact rfl
| app _ _ ih1 ih2 => exact .app (ih1 W) (ih2 W)
| lam _ _ ih1 ih2 => exact .lam (ih1 W) (ih2 W.succ)
| forallE _ _ ih1 ih2 => exact .forallE (ih1 W) (ih2 W.succ)
| beta _ _ ih1 ih2 =>
  simp [liftN, liftN_inst_hi]
  exact .beta (ih1 W.succ) (ih2 W)
| extra _ ih =>
  refine .extra fun a a' h => ?_
  obtain ⟨_, _, h', rfl, rfl⟩ := HE W h
  exact ih _ _ h' W
Proof state after:
no goals
Theorem: Lean4Lean.ParRed.weakN
Proof state before:
case const
E : Extra
HE : Extra.IsWeakN E
n : Nat
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
c✝ : Name
ls✝ : List VLevel
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ ParRed E Γ' (liftN n (VExpr.const c✝ ls✝) k) (liftN n (VExpr.const c✝ ls✝) k)
Tactic:
exact rfl
Proof state after:
no goals
Theorem: Lean4Lean.ParRed.weakN
Proof state before:
case app
E : Extra
HE : Extra.IsWeakN E
n : Nat
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
f✝ f'✝ a✝² a'✝ : VExpr
a✝¹ : ParRed E Γ✝ f✝ f'✝
a✝ : ParRed E Γ✝ a✝² a'✝
ih1 : ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k Γ✝ Γ' → ParRed E Γ' (liftN n f✝ k) (liftN n f'✝ k)
ih2 : ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k Γ✝ Γ' → ParRed E Γ' (liftN n a✝² k) (liftN n a'✝ k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ ParRed E Γ' (liftN n (VExpr.app f✝ a✝²) k) (liftN n (VExpr.app f'✝ a'✝) k)
Tactic:
exact .app (ih1 W) (ih2 W)
Proof state after:
no goals
Theorem: Lean4Lean.ParRed.weakN
Proof state before:
case lam
E : Extra
HE : Extra.IsWeakN E
n : Nat
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
A✝ A'✝ body✝ body'✝ : VExpr
a✝¹ : ParRed E Γ✝ A✝ A'✝
a✝ : ParRed E (A✝ :: Γ✝) body✝ body'✝
ih1 : ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k Γ✝ Γ' → ParRed E Γ' (liftN n A✝ k) (liftN n A'✝ k)
ih2 : ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k (A✝ :: Γ✝) Γ' → ParRed E Γ' (liftN n body✝ k) (liftN n body'✝ k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ ParRed E Γ' (liftN n (VExpr.lam A✝ body✝) k) (liftN n (VExpr.lam A'✝ body'✝) k)
Tactic:
exact .lam (ih1 W) (ih2 W.succ)
Proof state after:
no goals
Theorem: Lean4Lean.ParRed.weakN
Proof state before:
case forallE
E : Extra
HE : Extra.IsWeakN E
n : Nat
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
A✝ A'✝ B✝ B'✝ : VExpr
a✝¹ : ParRed E Γ✝ A✝ A'✝
a✝ : ParRed E (A✝ :: Γ✝) B✝ B'✝
ih1 : ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k Γ✝ Γ' → ParRed E Γ' (liftN n A✝ k) (liftN n A'✝ k)
ih2 : ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k (A✝ :: Γ✝) Γ' → ParRed E Γ' (liftN n B✝ k) (liftN n B'✝ k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ ParRed E Γ' (liftN n (VExpr.forallE A✝ B✝) k) (liftN n (VExpr.forallE A'✝ B'✝) k)
Tactic:
exact .forallE (ih1 W) (ih2 W.succ)
Proof state after:
no goals
Theorem: Lean4Lean.ParRed.weakN
Proof state before:
case beta
E : Extra
HE : Extra.IsWeakN E
n : Nat
Γ : List VExpr
e1 e2 A✝ : VExpr
Γ✝ : List VExpr
e₁✝ e₁'✝ e₂✝ e₂'✝ : VExpr
a✝¹ : ParRed E (A✝ :: Γ✝) e₁✝ e₁'✝
a✝ : ParRed E Γ✝ e₂✝ e₂'✝
ih1 : ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k (A✝ :: Γ✝) Γ' → ParRed E Γ' (liftN n e₁✝ k) (liftN n e₁'✝ k)
ih2 : ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k Γ✝ Γ' → ParRed E Γ' (liftN n e₂✝ k) (liftN n e₂'✝ k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ ParRed E Γ' (liftN n (VExpr.app (VExpr.lam A✝ e₁✝) e₂✝) k) (liftN n (inst e₁'✝ e₂'✝) k)
Tactic:
simp [liftN, liftN_inst_hi]
Proof state after:
case beta
E : Extra
HE : Extra.IsWeakN E
n : Nat
Γ : List VExpr
e1 e2 A✝ : VExpr
Γ✝ : List VExpr
e₁✝ e₁'✝ e₂✝ e₂'✝ : VExpr
a✝¹ : ParRed E (A✝ :: Γ✝) e₁✝ e₁'✝
a✝ : ParRed E Γ✝ e₂✝ e₂'✝
ih1 : ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k (A✝ :: Γ✝) Γ' → ParRed E Γ' (liftN n e₁✝ k) (liftN n e₁'✝ k)
ih2 : ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k Γ✝ Γ' → ParRed E Γ' (liftN n e₂✝ k) (liftN n e₂'✝ k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ ParRed E Γ' (VExpr.app (VExpr.lam (liftN n A✝ k) (liftN n e₁✝ (k + 1))) (liftN n e₂✝ k))
    (inst (liftN n e₁'✝ (k + 1)) (liftN n e₂'✝ k))
Theorem: Lean4Lean.ParRed.weakN
Proof state before:
case beta
E : Extra
HE : Extra.IsWeakN E
n : Nat
Γ : List VExpr
e1 e2 A✝ : VExpr
Γ✝ : List VExpr
e₁✝ e₁'✝ e₂✝ e₂'✝ : VExpr
a✝¹ : ParRed E (A✝ :: Γ✝) e₁✝ e₁'✝
a✝ : ParRed E Γ✝ e₂✝ e₂'✝
ih1 : ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k (A✝ :: Γ✝) Γ' → ParRed E Γ' (liftN n e₁✝ k) (liftN n e₁'✝ k)
ih2 : ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k Γ✝ Γ' → ParRed E Γ' (liftN n e₂✝ k) (liftN n e₂'✝ k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ ParRed E Γ' (VExpr.app (VExpr.lam (liftN n A✝ k) (liftN n e₁✝ (k + 1))) (liftN n e₂✝ k))
    (inst (liftN n e₁'✝ (k + 1)) (liftN n e₂'✝ k))
Tactic:
exact .beta (ih1 W.succ) (ih2 W)
Proof state after:
no goals
Theorem: Lean4Lean.ParRed.weakN
Proof state before:
case extra
E : Extra
HE : Extra.IsWeakN E
n : Nat
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e✝ e'✝ : VExpr
a✝ : ∀ (a a' : VExpr), E Γ✝ e✝ e'✝ a a' → ParRed E Γ✝ a a'
ih :
  ∀ (a a' : VExpr),
    E Γ✝ e✝ e'✝ a a' → ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k Γ✝ Γ' → ParRed E Γ' (liftN n a k) (liftN n a' k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
⊢ ParRed E Γ' (liftN n e✝ k) (liftN n e'✝ k)
Tactic:
refine .extra fun a a' h => ?_
Proof state after:
case extra
E : Extra
HE : Extra.IsWeakN E
n : Nat
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e✝ e'✝ : VExpr
a✝ : ∀ (a a' : VExpr), E Γ✝ e✝ e'✝ a a' → ParRed E Γ✝ a a'
ih :
  ∀ (a a' : VExpr),
    E Γ✝ e✝ e'✝ a a' → ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k Γ✝ Γ' → ParRed E Γ' (liftN n a k) (liftN n a' k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
a a' : VExpr
h : E Γ' (liftN n e✝ k) (liftN n e'✝ k) a a'
⊢ ParRed E Γ' a a'
Theorem: Lean4Lean.ParRed.weakN
Proof state before:
case extra
E : Extra
HE : Extra.IsWeakN E
n : Nat
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e✝ e'✝ : VExpr
a✝ : ∀ (a a' : VExpr), E Γ✝ e✝ e'✝ a a' → ParRed E Γ✝ a a'
ih :
  ∀ (a a' : VExpr),
    E Γ✝ e✝ e'✝ a a' → ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k Γ✝ Γ' → ParRed E Γ' (liftN n a k) (liftN n a' k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
a a' : VExpr
h : E Γ' (liftN n e✝ k) (liftN n e'✝ k) a a'
⊢ ParRed E Γ' a a'
Tactic:
obtain ⟨_, _, h', rfl, rfl⟩ := HE W h
Proof state after:
case extra.intro.intro.intro.intro
E : Extra
HE : Extra.IsWeakN E
n : Nat
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e✝ e'✝ : VExpr
a✝ : ∀ (a a' : VExpr), E Γ✝ e✝ e'✝ a a' → ParRed E Γ✝ a a'
ih :
  ∀ (a a' : VExpr),
    E Γ✝ e✝ e'✝ a a' → ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k Γ✝ Γ' → ParRed E Γ' (liftN n a k) (liftN n a' k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
w✝¹ w✝ : VExpr
h' : E Γ✝ e✝ e'✝ w✝¹ w✝
h : E Γ' (liftN n e✝ k) (liftN n e'✝ k) (liftN n w✝¹ k) (liftN n w✝ k)
⊢ ParRed E Γ' (liftN n w✝¹ k) (liftN n w✝ k)
Theorem: Lean4Lean.ParRed.weakN
Proof state before:
case extra.intro.intro.intro.intro
E : Extra
HE : Extra.IsWeakN E
n : Nat
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e✝ e'✝ : VExpr
a✝ : ∀ (a a' : VExpr), E Γ✝ e✝ e'✝ a a' → ParRed E Γ✝ a a'
ih :
  ∀ (a a' : VExpr),
    E Γ✝ e✝ e'✝ a a' → ∀ {k : Nat} {Γ' : List VExpr}, Ctx.LiftN n k Γ✝ Γ' → ParRed E Γ' (liftN n a k) (liftN n a' k)
k : Nat
Γ' : List VExpr
W : Ctx.LiftN n k Γ✝ Γ'
w✝¹ w✝ : VExpr
h' : E Γ✝ e✝ e'✝ w✝¹ w✝
h : E Γ' (liftN n e✝ k) (liftN n e'✝ k) (liftN n w✝¹ k) (liftN n w✝ k)
⊢ ParRed E Γ' (liftN n w✝¹ k) (liftN n w✝ k)
Tactic:
exact ih _ _ h' W
Proof state after:
no goals
Theorem: Lean4Lean.ParRed.instN
Proof state before:
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
k : Nat
Γ₁ Γ : List VExpr
e1 e2 : VExpr
W : Ctx.InstN Γ₀ a1 A₀ k Γ₁ Γ
H : ParRed E Γ₁ e1 e2
⊢ ParRed E Γ (inst e1 a1 k) (inst e2 a2 k)
Tactic:
induction H generalizing Γ k with
| @bvar _ i =>
  dsimp [inst]
  induction W generalizing i with
  | zero =>
    cases i with simp [inst_lift]
    | zero => exact H0
    | succ h => exact rfl
  | succ _ ih =>
    cases i with simp
    | zero => exact rfl
    | succ h => exact ih.weakN HE.1 .one
| sort | const => exact rfl
| app _ _ ih1 ih2 => exact .app (ih1 W) (ih2 W)
| lam _ _ ih1 ih2 => exact .lam (ih1 W) (ih2 W.succ)
| forallE _ _ ih1 ih2 => exact .forallE (ih1 W) (ih2 W.succ)
| beta _ _ ih1 ih2 =>
  simp [inst, inst0_inst_hi]
  exact .beta (ih1 W.succ) (ih2 W)
| extra _ ih =>
  refine .extra fun a a' h => ?_
  obtain ⟨_, _, h', rfl, rfl⟩ := HE.2 W h
  exact ih _ _ h' W
Proof state after:
no goals
Theorem: Lean4Lean.ParRed.instN
Proof state before:
case bvar
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
i k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ
⊢ ParRed E Γ (inst (VExpr.bvar i) a1 k) (inst (VExpr.bvar i) a2 k)
Tactic:
dsimp [inst]
Proof state after:
case bvar
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
i k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ
⊢ ParRed E Γ (instVar i a1 k) (instVar i a2 k)
Theorem: Lean4Lean.ParRed.instN
Proof state before:
case bvar
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
i k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ
⊢ ParRed E Γ (instVar i a1 k) (instVar i a2 k)
Tactic:
induction W generalizing i with
| zero =>
  cases i with simp [inst_lift]
  | zero => exact H0
  | succ h => exact rfl
| succ _ ih =>
  cases i with simp
  | zero => exact rfl
  | succ h => exact ih.weakN HE.1 .one
Proof state after:
no goals
Theorem: Lean4Lean.ParRed.instN
Proof state before:
case bvar.zero
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
k : Nat
Γ : List VExpr
i : Nat
⊢ ParRed E Γ₀ (instVar i a1) (instVar i a2)
Tactic:
cases i with simp [inst_lift]
| zero => exact H0
| succ h => exact rfl
Proof state after:
no goals
Theorem: Lean4Lean.ParRed.instN
Proof state before:
case bvar.zero.zero
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
k : Nat
Γ : List VExpr
⊢ ParRed E Γ₀ a1 a2
Tactic:
exact H0
Proof state after:
no goals
Theorem: Lean4Lean.ParRed.instN
Proof state before:
case bvar.zero.succ
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
k : Nat
Γ : List VExpr
h : Nat
⊢ ParRed E Γ₀ (VExpr.bvar h) (VExpr.bvar h)
Tactic:
exact rfl
Proof state after:
no goals
Theorem: Lean4Lean.ParRed.instN
Proof state before:
case bvar.succ
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : List VExpr
e1 e2 : VExpr
Γ✝¹ : List VExpr
k : Nat
Γ : List VExpr
k✝ : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.InstN Γ₀ a1 A₀ k✝ Γ✝ Γ'✝
ih : ∀ {i : Nat}, ParRed E Γ'✝ (instVar i a1 k✝) (instVar i a2 k✝)
i : Nat
⊢ ParRed E (inst A✝ a1 k✝ :: Γ'✝) (instVar i a1 (k✝ + 1)) (instVar i a2 (k✝ + 1))
Tactic:
cases i with simp
| zero => exact rfl
| succ h => exact ih.weakN HE.1 .one
Proof state after:
no goals
Theorem: Lean4Lean.ParRed.instN
Proof state before:
case bvar.succ.zero
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : List VExpr
e1 e2 : VExpr
Γ✝¹ : List VExpr
k : Nat
Γ : List VExpr
k✝ : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.InstN Γ₀ a1 A₀ k✝ Γ✝ Γ'✝
ih : ∀ {i : Nat}, ParRed E Γ'✝ (instVar i a1 k✝) (instVar i a2 k✝)
⊢ ParRed E (inst A✝ a1 k✝ :: Γ'✝) (VExpr.bvar 0) (VExpr.bvar 0)
Tactic:
exact rfl
Proof state after:
no goals
Theorem: Lean4Lean.ParRed.instN
Proof state before:
case bvar.succ.succ
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : List VExpr
e1 e2 : VExpr
Γ✝¹ : List VExpr
k : Nat
Γ : List VExpr
k✝ : Nat
Γ✝ Γ'✝ : List VExpr
A✝ : VExpr
a✝ : Ctx.InstN Γ₀ a1 A₀ k✝ Γ✝ Γ'✝
ih : ∀ {i : Nat}, ParRed E Γ'✝ (instVar i a1 k✝) (instVar i a2 k✝)
h : Nat
⊢ ParRed E (inst A✝ a1 k✝ :: Γ'✝) (lift (instVar h a1 k✝)) (lift (instVar h a2 k✝))
Tactic:
exact ih.weakN HE.1 .one
Proof state after:
no goals
Theorem: Lean4Lean.ParRed.instN
Proof state before:
case const
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
c✝ : Name
ls✝ : List VLevel
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ
⊢ ParRed E Γ (inst (VExpr.const c✝ ls✝) a1 k) (inst (VExpr.const c✝ ls✝) a2 k)
Tactic:
exact rfl
Proof state after:
no goals
Theorem: Lean4Lean.ParRed.instN
Proof state before:
case app
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
f✝ f'✝ a✝² a'✝ : VExpr
a✝¹ : ParRed E Γ✝ f✝ f'✝
a✝ : ParRed E Γ✝ a✝² a'✝
ih1 : ∀ {k : Nat} {Γ : List VExpr}, Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ → ParRed E Γ (inst f✝ a1 k) (inst f'✝ a2 k)
ih2 : ∀ {k : Nat} {Γ : List VExpr}, Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ → ParRed E Γ (inst a✝² a1 k) (inst a'✝ a2 k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ
⊢ ParRed E Γ (inst (VExpr.app f✝ a✝²) a1 k) (inst (VExpr.app f'✝ a'✝) a2 k)
Tactic:
exact .app (ih1 W) (ih2 W)
Proof state after:
no goals
Theorem: Lean4Lean.ParRed.instN
Proof state before:
case lam
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
A✝ A'✝ body✝ body'✝ : VExpr
a✝¹ : ParRed E Γ✝ A✝ A'✝
a✝ : ParRed E (A✝ :: Γ✝) body✝ body'✝
ih1 : ∀ {k : Nat} {Γ : List VExpr}, Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ → ParRed E Γ (inst A✝ a1 k) (inst A'✝ a2 k)
ih2 : ∀ {k : Nat} {Γ : List VExpr}, Ctx.InstN Γ₀ a1 A₀ k (A✝ :: Γ✝) Γ → ParRed E Γ (inst body✝ a1 k) (inst body'✝ a2 k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ
⊢ ParRed E Γ (inst (VExpr.lam A✝ body✝) a1 k) (inst (VExpr.lam A'✝ body'✝) a2 k)
Tactic:
exact .lam (ih1 W) (ih2 W.succ)
Proof state after:
no goals
Theorem: Lean4Lean.ParRed.instN
Proof state before:
case forallE
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
A✝ A'✝ B✝ B'✝ : VExpr
a✝¹ : ParRed E Γ✝ A✝ A'✝
a✝ : ParRed E (A✝ :: Γ✝) B✝ B'✝
ih1 : ∀ {k : Nat} {Γ : List VExpr}, Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ → ParRed E Γ (inst A✝ a1 k) (inst A'✝ a2 k)
ih2 : ∀ {k : Nat} {Γ : List VExpr}, Ctx.InstN Γ₀ a1 A₀ k (A✝ :: Γ✝) Γ → ParRed E Γ (inst B✝ a1 k) (inst B'✝ a2 k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ
⊢ ParRed E Γ (inst (VExpr.forallE A✝ B✝) a1 k) (inst (VExpr.forallE A'✝ B'✝) a2 k)
Tactic:
exact .forallE (ih1 W) (ih2 W.succ)
Proof state after:
no goals
Theorem: Lean4Lean.ParRed.instN
Proof state before:
case beta
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : List VExpr
e1 e2 A✝ : VExpr
Γ✝ : List VExpr
e₁✝ e₁'✝ e₂✝ e₂'✝ : VExpr
a✝¹ : ParRed E (A✝ :: Γ✝) e₁✝ e₁'✝
a✝ : ParRed E Γ✝ e₂✝ e₂'✝
ih1 : ∀ {k : Nat} {Γ : List VExpr}, Ctx.InstN Γ₀ a1 A₀ k (A✝ :: Γ✝) Γ → ParRed E Γ (inst e₁✝ a1 k) (inst e₁'✝ a2 k)
ih2 : ∀ {k : Nat} {Γ : List VExpr}, Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ → ParRed E Γ (inst e₂✝ a1 k) (inst e₂'✝ a2 k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ
⊢ ParRed E Γ (inst (VExpr.app (VExpr.lam A✝ e₁✝) e₂✝) a1 k) (inst (inst e₁'✝ e₂'✝) a2 k)
Tactic:
simp [inst, inst0_inst_hi]
Proof state after:
case beta
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : List VExpr
e1 e2 A✝ : VExpr
Γ✝ : List VExpr
e₁✝ e₁'✝ e₂✝ e₂'✝ : VExpr
a✝¹ : ParRed E (A✝ :: Γ✝) e₁✝ e₁'✝
a✝ : ParRed E Γ✝ e₂✝ e₂'✝
ih1 : ∀ {k : Nat} {Γ : List VExpr}, Ctx.InstN Γ₀ a1 A₀ k (A✝ :: Γ✝) Γ → ParRed E Γ (inst e₁✝ a1 k) (inst e₁'✝ a2 k)
ih2 : ∀ {k : Nat} {Γ : List VExpr}, Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ → ParRed E Γ (inst e₂✝ a1 k) (inst e₂'✝ a2 k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ
⊢ ParRed E Γ (VExpr.app (VExpr.lam (inst A✝ a1 k) (inst e₁✝ a1 (k + 1))) (inst e₂✝ a1 k))
    (inst (inst e₁'✝ a2 (k + 1)) (inst e₂'✝ a2 k))
Theorem: Lean4Lean.ParRed.instN
Proof state before:
case beta
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : List VExpr
e1 e2 A✝ : VExpr
Γ✝ : List VExpr
e₁✝ e₁'✝ e₂✝ e₂'✝ : VExpr
a✝¹ : ParRed E (A✝ :: Γ✝) e₁✝ e₁'✝
a✝ : ParRed E Γ✝ e₂✝ e₂'✝
ih1 : ∀ {k : Nat} {Γ : List VExpr}, Ctx.InstN Γ₀ a1 A₀ k (A✝ :: Γ✝) Γ → ParRed E Γ (inst e₁✝ a1 k) (inst e₁'✝ a2 k)
ih2 : ∀ {k : Nat} {Γ : List VExpr}, Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ → ParRed E Γ (inst e₂✝ a1 k) (inst e₂'✝ a2 k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ
⊢ ParRed E Γ (VExpr.app (VExpr.lam (inst A✝ a1 k) (inst e₁✝ a1 (k + 1))) (inst e₂✝ a1 k))
    (inst (inst e₁'✝ a2 (k + 1)) (inst e₂'✝ a2 k))
Tactic:
exact .beta (ih1 W.succ) (ih2 W)
Proof state after:
no goals
Theorem: Lean4Lean.ParRed.instN
Proof state before:
case extra
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e✝ e'✝ : VExpr
a✝ : ∀ (a a' : VExpr), E Γ✝ e✝ e'✝ a a' → ParRed E Γ✝ a a'
ih :
  ∀ (a a' : VExpr),
    E Γ✝ e✝ e'✝ a a' → ∀ {k : Nat} {Γ : List VExpr}, Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ → ParRed E Γ (inst a a1 k) (inst a' a2 k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ
⊢ ParRed E Γ (inst e✝ a1 k) (inst e'✝ a2 k)
Tactic:
refine .extra fun a a' h => ?_
Proof state after:
case extra
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e✝ e'✝ : VExpr
a✝ : ∀ (a a' : VExpr), E Γ✝ e✝ e'✝ a a' → ParRed E Γ✝ a a'
ih :
  ∀ (a a' : VExpr),
    E Γ✝ e✝ e'✝ a a' → ∀ {k : Nat} {Γ : List VExpr}, Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ → ParRed E Γ (inst a a1 k) (inst a' a2 k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ
a a' : VExpr
h : E Γ (inst e✝ a1 k) (inst e'✝ a2 k) a a'
⊢ ParRed E Γ a a'
Theorem: Lean4Lean.ParRed.instN
Proof state before:
case extra
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e✝ e'✝ : VExpr
a✝ : ∀ (a a' : VExpr), E Γ✝ e✝ e'✝ a a' → ParRed E Γ✝ a a'
ih :
  ∀ (a a' : VExpr),
    E Γ✝ e✝ e'✝ a a' → ∀ {k : Nat} {Γ : List VExpr}, Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ → ParRed E Γ (inst a a1 k) (inst a' a2 k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ
a a' : VExpr
h : E Γ (inst e✝ a1 k) (inst e'✝ a2 k) a a'
⊢ ParRed E Γ a a'
Tactic:
obtain ⟨_, _, h', rfl, rfl⟩ := HE.2 W h
Proof state after:
case extra.intro.intro.intro.intro
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e✝ e'✝ : VExpr
a✝ : ∀ (a a' : VExpr), E Γ✝ e✝ e'✝ a a' → ParRed E Γ✝ a a'
ih :
  ∀ (a a' : VExpr),
    E Γ✝ e✝ e'✝ a a' → ∀ {k : Nat} {Γ : List VExpr}, Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ → ParRed E Γ (inst a a1 k) (inst a' a2 k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ
w✝¹ w✝ : VExpr
h' : E Γ✝ e✝ e'✝ w✝¹ w✝
h : E Γ (inst e✝ a1 k) (inst e'✝ a2 k) (inst w✝¹ a1 k) (inst w✝ a2 k)
⊢ ParRed E Γ (inst w✝¹ a1 k) (inst w✝ a2 k)
Theorem: Lean4Lean.ParRed.instN
Proof state before:
case extra.intro.intro.intro.intro
E : Extra
Γ₀ : List VExpr
a1 a2 : VExpr
HE : Extra.IsInstN E
H0 : ParRed E Γ₀ a1 a2
A₀ : VExpr
Γ₁ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e✝ e'✝ : VExpr
a✝ : ∀ (a a' : VExpr), E Γ✝ e✝ e'✝ a a' → ParRed E Γ✝ a a'
ih :
  ∀ (a a' : VExpr),
    E Γ✝ e✝ e'✝ a a' → ∀ {k : Nat} {Γ : List VExpr}, Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ → ParRed E Γ (inst a a1 k) (inst a' a2 k)
k : Nat
Γ : List VExpr
W : Ctx.InstN Γ₀ a1 A₀ k Γ✝ Γ
w✝¹ w✝ : VExpr
h' : E Γ✝ e✝ e'✝ w✝¹ w✝
h : E Γ (inst e✝ a1 k) (inst e'✝ a2 k) (inst w✝¹ a1 k) (inst w✝ a2 k)
⊢ ParRed E Γ (inst w✝¹ a1 k) (inst w✝ a2 k)
Tactic:
exact ih _ _ h' W
Proof state after:
no goals
Theorem: Lean4Lean.NormalEq.defeq
Proof state before:
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
H : NormalEq TY Γ e1 e2
⊢ TY.IsDefEq Γ e1 e2
Tactic:
induction H with
| refl h => exact TY.refl h
| sortDF h1 h2 h3 => exact TY.sortDF h1 h2 h3
| appDF hf₁ _ ha₁ _ _ _ ih1 ih2 => exact TY.appDF hf₁ ih1 ha₁ ih2
| lamDF hA hA₁ _ _ ihA ihB =>
  have ⟨_, hB⟩ := TY.has_type ihB
  exact TY.trans (TY.symm <| TY.lamDF hA (TY.symm hA₁) (TY.refl hB))
    (TY.lamDF hA (TY.trans (TY.symm hA₁) ihA) ihB)
| forallEDF hA hA₁ _ hB₁ _ ihA ihB =>
  exact TY.trans (TY.symm <| TY.forallEDF hA (TY.symm hA₁) hB₁ (TY.refl hB₁))
    (TY.forallEDF hA (TY.trans (TY.symm hA₁) ihA) hB₁ ihB)
| etaL h1 _ ih =>
  have ⟨_, AB⟩ := TY.is_type h1
  have ⟨_, _, hA, _⟩ := TY.forallE_inv AB
  exact TY.trans (TY.lamDF hA (TY.refl hA) ih) (TY.eta h1)
| etaR h1 _ ih =>
  have ⟨_, AB⟩ := TY.is_type h1
  have ⟨_, _, hA, _⟩ := TY.forallE_inv AB
  exact TY.trans (TY.symm (TY.eta h1)) (TY.lamDF hA (TY.refl hA) ih)
| proofIrrel h1 h2 h3 => exact TY.proofIrrel h1 h2 h3
Proof state after:
no goals
Theorem: Lean4Lean.NormalEq.defeq
Proof state before:
case refl
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
Γ✝ : List VExpr
e✝ A✝ : VExpr
h : TY.HasType Γ✝ e✝ A✝
⊢ TY.IsDefEq Γ✝ e✝ e✝
Tactic:
exact TY.refl h
Proof state after:
no goals
Theorem: Lean4Lean.NormalEq.defeq
Proof state before:
case sortDF
TY : Typing
Γ : List VExpr
e1 e2 : VExpr
l₁✝ l₂✝ : VLevel
Γ✝ : List VExpr
h1 : VLevel.WF TY.univs l₁✝
h2 : VLevel.WF TY.univs l₂✝
h3 : l₁✝ ≈ l₂✝
⊢ TY.IsDefEq Γ✝ (sort l₁✝) (sort l₂✝)
Tactic:
exact TY.sortDF h1 h2 h3
Proof state after:
no goals