internlm/Lean-Github huggingface dataset:
Theorem: newmans_lemma
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
w1 : A
h1 : refl_trans_clos R y w1 ∧ refl_trans_clos R w w1
w2 : A
h2 : refl_trans_clos R z w2 ∧ refl_trans_clos R w w2
red_x_w : trans_clos R x w
⊢ joins R w1 w2
Tactic:
apply ih
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
w1 : A
h1 : refl_trans_clos R y w1 ∧ refl_trans_clos R w w1
w2 : A
h2 : refl_trans_clos R z w2 ∧ refl_trans_clos R w w2
red_x_w : trans_clos R x w
⊢ trans_clos R x ?y

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
w1 : A
h1 : refl_trans_clos R y w1 ∧ refl_trans_clos R w w1
w2 : A
h2 : refl_trans_clos R z w2 ∧ refl_trans_clos R w w2
red_x_w : trans_clos R x w
⊢ refl_trans_clos R ?y w1 ∧ refl_trans_clos R ?y w2

case y
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
w1 : A
h1 : refl_trans_clos R y w1 ∧ refl_trans_clos R w w1
w2 : A
h2 : refl_trans_clos R z w2 ∧ refl_trans_clos R w w2
red_x_w : trans_clos R x w
⊢ A
Theorem: newmans_lemma
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
w1 : A
h1 : refl_trans_clos R y w1 ∧ refl_trans_clos R w w1
w2 : A
h2 : refl_trans_clos R z w2 ∧ refl_trans_clos R w w2
red_x_w : trans_clos R x w
⊢ trans_clos R x ?y

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
w1 : A
h1 : refl_trans_clos R y w1 ∧ refl_trans_clos R w w1
w2 : A
h2 : refl_trans_clos R z w2 ∧ refl_trans_clos R w w2
red_x_w : trans_clos R x w
⊢ refl_trans_clos R ?y w1 ∧ refl_trans_clos R ?y w2

case y
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
w1 : A
h1 : refl_trans_clos R y w1 ∧ refl_trans_clos R w w1
w2 : A
h2 : refl_trans_clos R z w2 ∧ refl_trans_clos R w w2
red_x_w : trans_clos R x w
⊢ A
Tactic:
. apply red_x_w
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
w1 : A
h1 : refl_trans_clos R y w1 ∧ refl_trans_clos R w w1
w2 : A
h2 : refl_trans_clos R z w2 ∧ refl_trans_clos R w w2
red_x_w : trans_clos R x w
⊢ refl_trans_clos R w w1 ∧ refl_trans_clos R w w2
Theorem: newmans_lemma
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
w1 : A
h1 : refl_trans_clos R y w1 ∧ refl_trans_clos R w w1
w2 : A
h2 : refl_trans_clos R z w2 ∧ refl_trans_clos R w w2
red_x_w : trans_clos R x w
⊢ refl_trans_clos R w w1 ∧ refl_trans_clos R w w2
Tactic:
. aesop
Proof state after:
no goals
Theorem: newmans_lemma
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
w1 : A
h1 : refl_trans_clos R y w1 ∧ refl_trans_clos R w w1
w2 : A
h2 : refl_trans_clos R z w2 ∧ refl_trans_clos R w w2
red_x_w : trans_clos R x w
⊢ trans_clos R x ?y
Tactic:
apply red_x_w
Proof state after:
no goals
Theorem: newmans_lemma
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
w1 : A
h1 : refl_trans_clos R y w1 ∧ refl_trans_clos R w w1
w2 : A
h2 : refl_trans_clos R z w2 ∧ refl_trans_clos R w w2
red_x_w : trans_clos R x w
⊢ refl_trans_clos R w w1 ∧ refl_trans_clos R w w2
Tactic:
aesop
Proof state after:
no goals
Theorem: newmans_lemma
Proof state before:
case intro.intro.intro.intro.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
w1 : A
h1 : refl_trans_clos R y w1 ∧ refl_trans_clos R w w1
w2 : A
h2 : refl_trans_clos R z w2 ∧ refl_trans_clos R w w2
red_x_w : trans_clos R x w
omega : A
h3 : refl_trans_clos R w1 omega ∧ refl_trans_clos R w2 omega
⊢ refl_trans_clos R w1 omega
Tactic:
. apply h3.1
Proof state after:
no goals
Theorem: newmans_lemma
Proof state before:
case intro.intro.intro.intro.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
w1 : A
h1 : refl_trans_clos R y w1 ∧ refl_trans_clos R w w1
w2 : A
h2 : refl_trans_clos R z w2 ∧ refl_trans_clos R w w2
red_x_w : trans_clos R x w
omega : A
h3 : refl_trans_clos R w1 omega ∧ refl_trans_clos R w2 omega
⊢ refl_trans_clos R y ?intro.intro.intro.intro.left.y
Tactic:
apply h1.1
Proof state after:
no goals
Theorem: newmans_lemma
Proof state before:
case intro.intro.intro.intro.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
w1 : A
h1 : refl_trans_clos R y w1 ∧ refl_trans_clos R w w1
w2 : A
h2 : refl_trans_clos R z w2 ∧ refl_trans_clos R w w2
red_x_w : trans_clos R x w
omega : A
h3 : refl_trans_clos R w1 omega ∧ refl_trans_clos R w2 omega
⊢ refl_trans_clos R w1 omega
Tactic:
apply h3.1
Proof state after:
no goals
Theorem: newmans_lemma
Proof state before:
case intro.intro.intro.intro.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
w1 : A
h1 : refl_trans_clos R y w1 ∧ refl_trans_clos R w w1
w2 : A
h2 : refl_trans_clos R z w2 ∧ refl_trans_clos R w w2
red_x_w : trans_clos R x w
omega : A
h3 : refl_trans_clos R w1 omega ∧ refl_trans_clos R w2 omega
⊢ refl_trans_clos R w2 omega
Tactic:
. apply h3.2
Proof state after:
no goals
Theorem: newmans_lemma
Proof state before:
case intro.intro.intro.intro.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
w1 : A
h1 : refl_trans_clos R y w1 ∧ refl_trans_clos R w w1
w2 : A
h2 : refl_trans_clos R z w2 ∧ refl_trans_clos R w w2
red_x_w : trans_clos R x w
omega : A
h3 : refl_trans_clos R w1 omega ∧ refl_trans_clos R w2 omega
⊢ refl_trans_clos R z ?intro.intro.intro.intro.right.y
Tactic:
apply h2.1
Proof state after:
no goals
Theorem: newmans_lemma
Proof state before:
case intro.intro.intro.intro.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
w1 : A
h1 : refl_trans_clos R y w1 ∧ refl_trans_clos R w w1
w2 : A
h2 : refl_trans_clos R z w2 ∧ refl_trans_clos R w w2
red_x_w : trans_clos R x w
omega : A
h3 : refl_trans_clos R w1 omega ∧ refl_trans_clos R w2 omega
⊢ refl_trans_clos R w2 omega
Tactic:
apply h3.2
Proof state after:
no goals
Theorem: confluent_unique_nf
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ confluent R → ∀ (x y z : A), refl_trans_clos R x y → refl_trans_clos R x z → normal R y → normal R z → y = z
Tactic:
intros conf x y z red_x_y red_x_z norm_y norm_z
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf : confluent R
x y z : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
norm_y : normal R y
norm_z : normal R z
⊢ y = z
Theorem: confluent_unique_nf
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf : confluent R
x y z : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
norm_y : normal R y
norm_z : normal R z
⊢ y = z
Tactic:
have wdg_y_z : wedge _ y z := Exists.intro x ⟨ red_x_y, red_x_z ⟩
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf : confluent R
x y z : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
norm_y : normal R y
norm_z : normal R z
wdg_y_z : wedge R y z
⊢ y = z
Theorem: confluent_unique_nf
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf : confluent R
x y z : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
norm_y : normal R y
norm_z : normal R z
wdg_y_z : wedge R y z
⊢ y = z
Tactic:
have h : y ~>*.*<~ z := conf _ _ wdg_y_z
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf : confluent R
x y z : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
norm_y : normal R y
norm_z : normal R z
wdg_y_z : wedge R y z
h : joins R y z
⊢ y = z
Theorem: confluent_unique_nf
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf : confluent R
x y z : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
norm_y : normal R y
norm_z : normal R z
wdg_y_z : wedge R y z
h : joins R y z
⊢ y = z
Tactic:
cases' h with w h
Proof state after:
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf : confluent R
x y z : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
norm_y : normal R y
norm_z : normal R z
wdg_y_z : wedge R y z
w : A
h : refl_trans_clos R y w ∧ refl_trans_clos R z w
⊢ y = z
Theorem: confluent_unique_nf
Proof state before:
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf : confluent R
x y z : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
norm_y : normal R y
norm_z : normal R z
wdg_y_z : wedge R y z
w : A
h : refl_trans_clos R y w ∧ refl_trans_clos R z w
⊢ y = z
Tactic:
cases h
Proof state after:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf : confluent R
x y z : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
norm_y : normal R y
norm_z : normal R z
wdg_y_z : wedge R y z
w : A
left✝ : refl_trans_clos R y w
right✝ : refl_trans_clos R z w
⊢ y = z
Theorem: confluent_unique_nf
Proof state before:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf : confluent R
x y z : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
norm_y : normal R y
norm_z : normal R z
wdg_y_z : wedge R y z
w : A
left✝ : refl_trans_clos R y w
right✝ : refl_trans_clos R z w
⊢ y = z
Tactic:
have eq_y_w : y = w := by apply normal_red <;> trivial
Proof state after:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf : confluent R
x y z : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
norm_y : normal R y
norm_z : normal R z
wdg_y_z : wedge R y z
w : A
left✝ : refl_trans_clos R y w
right✝ : refl_trans_clos R z w
eq_y_w : y = w
⊢ y = z
Theorem: confluent_unique_nf
Proof state before:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf : confluent R
x y z : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
norm_y : normal R y
norm_z : normal R z
wdg_y_z : wedge R y z
w : A
left✝ : refl_trans_clos R y w
right✝ : refl_trans_clos R z w
eq_y_w : y = w
⊢ y = z
Tactic:
have eq_z_w : z = w := by  apply normal_red <;> trivial
Proof state after:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf : confluent R
x y z : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
norm_y : normal R y
norm_z : normal R z
wdg_y_z : wedge R y z
w : A
left✝ : refl_trans_clos R y w
right✝ : refl_trans_clos R z w
eq_y_w : y = w
eq_z_w : z = w
⊢ y = z
Theorem: confluent_unique_nf
Proof state before:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf : confluent R
x y z : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
norm_y : normal R y
norm_z : normal R z
wdg_y_z : wedge R y z
w : A
left✝ : refl_trans_clos R y w
right✝ : refl_trans_clos R z w
eq_y_w : y = w
eq_z_w : z = w
⊢ y = z
Tactic:
simp [*]
Proof state after:
no goals
Theorem: confluent_unique_nf
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf : confluent R
x y z : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
norm_y : normal R y
norm_z : normal R z
wdg_y_z : wedge R y z
w : A
left✝ : refl_trans_clos R y w
right✝ : refl_trans_clos R z w
⊢ y = w
Tactic:
apply normal_red <;> trivial
Proof state after:
no goals
Theorem: confluent_unique_nf
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf : confluent R
x y z : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
norm_y : normal R y
norm_z : normal R z
wdg_y_z : wedge R y z
w : A
left✝ : refl_trans_clos R y w
right✝ : refl_trans_clos R z w
eq_y_w : y = w
⊢ z = w
Tactic:
apply normal_red <;> trivial
Proof state after:
no goals
Theorem: inc_refl_trans_eq
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ ((fun R R' => ∀ (x y : A), R x y → R' x y) (fun x x_1 => R x x_1) fun x x_1 => S x x_1) →
    ((fun R R' => ∀ (x y : A), R x y → R' x y) (fun x x_1 => S x x_1) fun x x_1 => refl_trans_clos R x x_1) →
      (fun R R' => ∀ (x y : A), R x y ↔ R' x y) (fun x x_1 => refl_trans_clos S x x_1) fun x x_1 =>
        refl_trans_clos R x x_1
Tactic:
simp
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ (∀ (x y : A), R x y → S x y) →
    (∀ (x y : A), S x y → refl_trans_clos R x y) → ∀ (x y : A), refl_trans_clos S x y ↔ refl_trans_clos R x y
Theorem: inc_refl_trans_eq
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ (∀ (x y : A), R x y → S x y) →
    (∀ (x y : A), S x y → refl_trans_clos R x y) → ∀ (x y : A), refl_trans_clos S x y ↔ refl_trans_clos R x y
Tactic:
intros r_sub_s s_sub_r_star x y
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y : A
⊢ refl_trans_clos S x y ↔ refl_trans_clos R x y
Theorem: inc_refl_trans_eq
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y : A
⊢ refl_trans_clos S x y ↔ refl_trans_clos R x y
Tactic:
constructor <;> intros steps
Proof state after:
case mp
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y : A
steps : refl_trans_clos S x y
⊢ refl_trans_clos R x y

case mpr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y : A
steps : refl_trans_clos R x y
⊢ refl_trans_clos S x y
Theorem: inc_refl_trans_eq
Proof state before:
case mp
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y : A
steps : refl_trans_clos S x y
⊢ refl_trans_clos R x y

case mpr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y : A
steps : refl_trans_clos R x y
⊢ refl_trans_clos S x y
Tactic:
. induction steps
  . constructor
  . apply refl_trans_clos_transitive
    . apply s_sub_r_star; trivial
    . trivial
Proof state after:
case mpr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y : A
steps : refl_trans_clos R x y
⊢ refl_trans_clos S x y
Theorem: inc_refl_trans_eq
Proof state before:
case mpr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y : A
steps : refl_trans_clos R x y
⊢ refl_trans_clos S x y
Tactic:
. induction steps
  . constructor
  . aesop
Proof state after:
no goals