internlm/Lean-Github huggingface dataset:
Theorem: normalizes_ind
Proof state before:
case h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
h' : ∃ f, f 0 = x ∧ ∀ (n : ℕ), ¬P (f n) ∧ R (f n) (f (n + 1))
⊢ ∃ xs, xs 0 = x ∧ ∀ (n : ℕ), R (xs n) (xs (n + 1))
Tactic:
match h' with
  | Exists.intro xs ⟨P0, P1⟩ =>
    exists xs; aesop
Proof state after:
no goals
Theorem: normalizes_ind
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
⊢ ∃ f, f 0 = x ∧ ∀ (n : ℕ), ¬P (f n) ∧ R (f n) (f (n + 1))
Tactic:
apply (dependent_choice''  (λ a ↦ ¬ P a))
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
⊢ ¬P x

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
⊢ ∀ (a : A), ¬P a → ∃ b, ¬P b ∧ R a b
Theorem: normalizes_ind
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
⊢ ¬P x

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
⊢ ∀ (a : A), ¬P a → ∃ b, ¬P b ∧ R a b
Tactic:
. exact h
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
⊢ ∀ (a : A), ¬P a → ∃ b, ¬P b ∧ R a b
Theorem: normalizes_ind
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
⊢ ∀ (a : A), ¬P a → ∃ b, ¬P b ∧ R a b
Tactic:
. intros a npa
  apply Classical.byContradiction
  simp; intros p
  apply npa
  apply IH; intros y ry
  apply Classical.byContradiction; intros npy
  apply (p y npy ry)
Proof state after:
no goals
Theorem: normalizes_ind
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
⊢ ¬P x
Tactic:
exact h
Proof state after:
no goals
Theorem: normalizes_ind
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
⊢ ∀ (a : A), ¬P a → ∃ b, ¬P b ∧ R a b
Tactic:
intros a npa
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
⊢ ∃ b, ¬P b ∧ R a b
Theorem: normalizes_ind
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
⊢ ∃ b, ¬P b ∧ R a b
Tactic:
apply Classical.byContradiction
Proof state after:
case a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
⊢ (¬∃ b, ¬P b ∧ R a b) → False
Theorem: normalizes_ind
Proof state before:
case a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
⊢ (¬∃ b, ¬P b ∧ R a b) → False
Tactic:
simp
Proof state after:
case a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
⊢ (∀ (x : A), ¬P x → ¬R a x) → False
Theorem: normalizes_ind
Proof state before:
case a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
⊢ (∀ (x : A), ¬P x → ¬R a x) → False
Tactic:
intros p
Proof state after:
case a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
p : ∀ (x : A), ¬P x → ¬R a x
⊢ False
Theorem: normalizes_ind
Proof state before:
case a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
p : ∀ (x : A), ¬P x → ¬R a x
⊢ False
Tactic:
apply npa
Proof state after:
case a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
p : ∀ (x : A), ¬P x → ¬R a x
⊢ P a
Theorem: normalizes_ind
Proof state before:
case a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
p : ∀ (x : A), ¬P x → ¬R a x
⊢ P a
Tactic:
apply IH
Proof state after:
case a.h.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
p : ∀ (x : A), ¬P x → ¬R a x
⊢ ∀ (y : A), R a y → P y
Theorem: normalizes_ind
Proof state before:
case a.h.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
p : ∀ (x : A), ¬P x → ¬R a x
⊢ ∀ (y : A), R a y → P y
Tactic:
intros y ry
Proof state after:
case a.h.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
p : ∀ (x : A), ¬P x → ¬R a x
y : A
ry : R a y
⊢ P y
Theorem: normalizes_ind
Proof state before:
case a.h.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
p : ∀ (x : A), ¬P x → ¬R a x
y : A
ry : R a y
⊢ P y
Tactic:
apply Classical.byContradiction
Proof state after:
case a.h.a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
p : ∀ (x : A), ¬P x → ¬R a x
y : A
ry : R a y
⊢ ¬P y → False
Theorem: normalizes_ind
Proof state before:
case a.h.a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
p : ∀ (x : A), ¬P x → ¬R a x
y : A
ry : R a y
⊢ ¬P y → False
Tactic:
intros npy
Proof state after:
case a.h.a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
p : ∀ (x : A), ¬P x → ¬R a x
y : A
ry : R a y
npy : ¬P y
⊢ False
Theorem: normalizes_ind
Proof state before:
case a.h.a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
a : A
npa : ¬P a
p : ∀ (x : A), ¬P x → ¬R a x
y : A
ry : R a y
npy : ¬P y
⊢ False
Tactic:
apply (p y npy ry)
Proof state after:
no goals
Theorem: normalizes_ind
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
h' : ∃ f, f 0 = x ∧ ∀ (n : ℕ), ¬P (f n) ∧ R (f n) (f (n + 1))
xs : ℕ → A
P0 : xs 0 = x
P1 : ∀ (n : ℕ), ¬P (xs n) ∧ R (xs n) (xs (n + 1))
⊢ ∃ xs, xs 0 = x ∧ ∀ (n : ℕ), R (xs n) (xs (n + 1))
Tactic:
exists xs
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
h' : ∃ f, f 0 = x ∧ ∀ (n : ℕ), ¬P (f n) ∧ R (f n) (f (n + 1))
xs : ℕ → A
P0 : xs 0 = x
P1 : ∀ (n : ℕ), ¬P (xs n) ∧ R (xs n) (xs (n + 1))
⊢ xs 0 = x ∧ ∀ (n : ℕ), R (xs n) (xs (n + 1))
Theorem: normalizes_ind
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
h' : ∃ f, f 0 = x ∧ ∀ (n : ℕ), ¬P (f n) ∧ R (f n) (f (n + 1))
xs : ℕ → A
P0 : xs 0 = x
P1 : ∀ (n : ℕ), ¬P (xs n) ∧ R (xs n) (xs (n + 1))
⊢ xs 0 = x ∧ ∀ (n : ℕ), R (xs n) (xs (n + 1))
Tactic:
aesop
Proof state after:
no goals
Theorem: normalizing_ind
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → normalizing R → ∀ (x : A), P x
Tactic:
intros P IH norm x
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
norm : normalizing R
x : A
⊢ P x
Theorem: normalizing_ind
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
norm : normalizing R
x : A
⊢ P x
Tactic:
apply normalizes_ind
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
norm : normalizing R
x : A
⊢ ∀ (x : A), (∀ (y : A), ?R x y → P y) → P x

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
norm : normalizing R
x : A
⊢ normalizes ?R x

case R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
norm : normalizing R
x : A
⊢ A → A → Prop
Theorem: normalizing_ind
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
norm : normalizing R
x : A
⊢ ∀ (x : A), (∀ (y : A), ?R x y → P y) → P x

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
norm : normalizing R
x : A
⊢ normalizes ?R x

case R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
norm : normalizing R
x : A
⊢ A → A → Prop
Tactic:
. apply IH
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
norm : normalizing R
x : A
⊢ normalizes (fun x y => R x y) x
Theorem: normalizing_ind
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
norm : normalizing R
x : A
⊢ normalizes (fun x y => R x y) x
Tactic:
. apply norm
Proof state after:
no goals
Theorem: normalizing_ind
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
norm : normalizing R
x : A
⊢ ∀ (x : A), (∀ (y : A), ?R x y → P y) → P x
Tactic:
apply IH
Proof state after:
no goals
Theorem: normalizing_ind
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
norm : normalizing R
x : A
⊢ normalizes (fun x y => R x y) x
Tactic:
apply norm
Proof state after:
no goals
Theorem: ind_normalizing
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ (∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x) → normalizing R
Tactic:
intros ih x
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x : A
⊢ normalizes R x
Theorem: ind_normalizing
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x : A
⊢ normalizes R x
Tactic:
apply ih
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x : A
⊢ ∀ (x : A), (∀ (y : A), R x y → normalizes R y) → normalizes R x
Theorem: ind_normalizing
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x : A
⊢ ∀ (x : A), (∀ (y : A), R x y → normalizes R y) → normalizes R x
Tactic:
intros x red_norm div
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
div : diverge_from R x
⊢ False
Theorem: ind_normalizing
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
div : diverge_from R x
⊢ False
Tactic:
cases div
Proof state after:
case a.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
w✝ : ℕ → A
h✝ : w✝ 0 = x ∧ ∀ (n : ℕ), R (w✝ n) (w✝ (n + 1))
⊢ False
Theorem: ind_normalizing
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ False
Tactic:
case a.intro f h =>
  apply red_norm
  . simp [← h.1]
    apply h.2 0
  . exists (λ n ↦ f (n+1))
    simp
    intros n; apply h.2
Proof state after:
no goals
Theorem: ind_normalizing
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ False
Tactic:
apply red_norm
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ R x ?y

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ diverge_from R ?y

case y
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ A
Theorem: ind_normalizing
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ R x ?y

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ diverge_from R ?y

case y
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ A
Tactic:
. simp [← h.1]
  apply h.2 0
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ diverge_from R (f (0 + 1))
Theorem: ind_normalizing
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ diverge_from R (f (0 + 1))
Tactic:
. exists (λ n ↦ f (n+1))
  simp
  intros n; apply h.2
Proof state after:
no goals
Theorem: ind_normalizing
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ R x ?y
Tactic:
simp [← h.1]
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ R (f 0) ?y
Theorem: ind_normalizing
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ R (f 0) ?y
Tactic:
apply h.2 0
Proof state after:
no goals
Theorem: ind_normalizing
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ diverge_from R (f (0 + 1))
Tactic:
exists (λ n ↦ f (n+1))
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ (fun n => f (n + 1)) 0 = f (0 + 1) ∧ ∀ (n : ℕ), R ((fun n => f (n + 1)) n) ((fun n => f (n + 1)) (n + 1))
Theorem: ind_normalizing
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ (fun n => f (n + 1)) 0 = f (0 + 1) ∧ ∀ (n : ℕ), R ((fun n => f (n + 1)) n) ((fun n => f (n + 1)) (n + 1))
Tactic:
simp
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ ∀ (n : ℕ), R (f (n + 1)) (f (n + 1 + 1))
Theorem: ind_normalizing
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
⊢ ∀ (n : ℕ), R (f (n + 1)) (f (n + 1 + 1))
Tactic:
intros n
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
n : ℕ
⊢ R (f (n + 1)) (f (n + 1 + 1))
Theorem: ind_normalizing
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
f : ℕ → A
h : f 0 = x ∧ ∀ (n : ℕ), R (f n) (f (n + 1))
n : ℕ
⊢ R (f (n + 1)) (f (n + 1 + 1))
Tactic:
apply h.2
Proof state after:
no goals
Theorem: red_ref_trans_clos
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ ∀ (x y z : A), R x y → refl_trans_clos R y z → refl_trans_clos R x z
Tactic:
intros x y z red_x_y h
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
red_x_y : R x y
h : refl_trans_clos R y z
⊢ refl_trans_clos R x z
Theorem: red_ref_trans_clos
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
red_x_y : R x y
h : refl_trans_clos R y z
⊢ refl_trans_clos R x z
Tactic:
apply refl_trans_clos.step _ _ <;> trivial
Proof state after:
no goals
Theorem: normalizing_normal
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
⊢ normalizes R x → ∃ y, refl_trans_clos R x y ∧ normal R y
Tactic:
apply normalizes_ind
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
⊢ ∀ (x : A),
    (∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1) → ∃ y, refl_trans_clos R x y ∧ normal R y
Theorem: normalizing_normal
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
⊢ ∀ (x : A),
    (∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1) → ∃ y, refl_trans_clos R x y ∧ normal R y
Tactic:
intros x h
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
⊢ ∃ y, refl_trans_clos R x y ∧ normal R y
Theorem: normalizing_normal
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
⊢ ∃ y, refl_trans_clos R x y ∧ normal R y
Tactic:
by_cases (∃ y, x ~> y)
Proof state after:
case pos
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h✝ : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
h : ∃ y, R x y
⊢ ∃ y, refl_trans_clos R x y ∧ normal R y

case neg
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h✝ : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
h : ¬∃ y, R x y
⊢ ∃ y, refl_trans_clos R x y ∧ normal R y
Theorem: normalizing_normal
Proof state before:
case pos
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h✝ : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
h : ∃ y, R x y
⊢ ∃ y, refl_trans_clos R x y ∧ normal R y

case neg
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h✝ : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
h : ¬∃ y, R x y
⊢ ∃ y, refl_trans_clos R x y ∧ normal R y
Tactic:
. cases' h with y h'
  cases' h _ h' with z h''
  cases h''
  exists z
  constructor <;> aesop
Proof state after:
case neg
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h✝ : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
h : ¬∃ y, R x y
⊢ ∃ y, refl_trans_clos R x y ∧ normal R y
Theorem: normalizing_normal
Proof state before:
case neg
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h✝ : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
h : ¬∃ y, R x y
⊢ ∃ y, refl_trans_clos R x y ∧ normal R y
Tactic:
. exists x; constructor
  . constructor
  . apply h
Proof state after:
no goals
Theorem: normalizing_normal
Proof state before:
case pos
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h✝ : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
h : ∃ y, R x y
⊢ ∃ y, refl_trans_clos R x y ∧ normal R y
Tactic:
cases' h with y h'
Proof state after:
case pos.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
y : A
h' : R x y
⊢ ∃ y, refl_trans_clos R x y ∧ normal R y
Theorem: normalizing_normal
Proof state before:
case pos.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
y : A
h' : R x y
⊢ ∃ y, refl_trans_clos R x y ∧ normal R y
Tactic:
cases' h _ h' with z h''
Proof state after:
case pos.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
y : A
h' : R x y
z : A
h'' : refl_trans_clos R y z ∧ normal R z
⊢ ∃ y, refl_trans_clos R x y ∧ normal R y