internlm/Lean-Github huggingface dataset:
Theorem: normalizing_normal
Proof state before:
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
Tactic:
cases h''
Proof state after:
case pos.intro.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
left✝ : refl_trans_clos R y z
right✝ : normal R z
⊢ ∃ y, refl_trans_clos R x y ∧ normal R y
Theorem: normalizing_normal
Proof state before:
case pos.intro.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
left✝ : refl_trans_clos R y z
right✝ : normal R z
⊢ ∃ y, refl_trans_clos R x y ∧ normal R y
Tactic:
exists z
Proof state after:
case pos.intro.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
left✝ : refl_trans_clos R y z
right✝ : normal R z
⊢ refl_trans_clos R x z ∧ normal R z
Theorem: normalizing_normal
Proof state before:
case pos.intro.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
left✝ : refl_trans_clos R y z
right✝ : normal R z
⊢ refl_trans_clos R x z ∧ normal R z
Tactic:
constructor <;> aesop
Proof state after:
no goals
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
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
⊢ refl_trans_clos R x x ∧ normal R x
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
⊢ refl_trans_clos R x x ∧ normal R x
Tactic:
constructor
Proof state after:
case neg.left
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
⊢ refl_trans_clos R x x

case neg.right
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
⊢ normal R x
Theorem: normalizing_normal
Proof state before:
case neg.left
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
⊢ refl_trans_clos R x x

case neg.right
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
⊢ normal R x
Tactic:
. constructor
Proof state after:
case neg.right
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
⊢ normal R x
Theorem: normalizing_normal
Proof state before:
case neg.right
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
⊢ normal R x
Tactic:
. apply h
Proof state after:
no goals
Theorem: normalizing_normal
Proof state before:
case neg.left
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
⊢ refl_trans_clos R x x
Tactic:
constructor
Proof state after:
no goals
Theorem: normalizing_normal
Proof state before:
case neg.right
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
⊢ normal R x
Tactic:
apply h
Proof state after:
no goals
Theorem: refl_trans_sym_refl_trans
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ ∀ (R : A → A → Prop), (fun R R' => ∀ (x y : A), R x y → R' x y) (refl_trans_clos R) (refl_trans_sym_clos R)
Tactic:
intros R x y red
Proof state after:
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
R : A → A → Prop
x y : A
red : refl_trans_clos R x y
⊢ refl_trans_sym_clos R x y
Theorem: refl_trans_sym_refl_trans
Proof state before:
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
R : A → A → Prop
x y : A
red : refl_trans_clos R x y
⊢ refl_trans_sym_clos R x y
Tactic:
induction red
Proof state after:
case refl
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
R : A → A → Prop
x y a✝ : A
⊢ refl_trans_sym_clos R a✝ a✝

case step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
R : A → A → Prop
x y a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
a_ih✝ : refl_trans_sym_clos R b✝ c✝
⊢ refl_trans_sym_clos R a✝² c✝
Theorem: refl_trans_sym_refl_trans
Proof state before:
case refl
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
R : A → A → Prop
x y a✝ : A
⊢ refl_trans_sym_clos R a✝ a✝

case step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
R : A → A → Prop
x y a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
a_ih✝ : refl_trans_sym_clos R b✝ c✝
⊢ refl_trans_sym_clos R a✝² c✝
Tactic:
constructor
Proof state after:
case step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
R : A → A → Prop
x y a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
a_ih✝ : refl_trans_sym_clos R b✝ c✝
⊢ refl_trans_sym_clos R a✝² c✝
Theorem: refl_trans_sym_refl_trans
Proof state before:
case step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
R : A → A → Prop
x y a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
a_ih✝ : refl_trans_sym_clos R b✝ c✝
⊢ refl_trans_sym_clos R a✝² c✝
Tactic:
apply refl_trans_sym_clos.trans <;> try trivial
Proof state after:
case step.a
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
R : A → A → Prop
x y a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
a_ih✝ : refl_trans_sym_clos R b✝ c✝
⊢ refl_trans_sym_clos R a✝² b✝
Theorem: refl_trans_sym_refl_trans
Proof state before:
case step.a
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
R : A → A → Prop
x y a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
a_ih✝ : refl_trans_sym_clos R b✝ c✝
⊢ refl_trans_sym_clos R a✝² b✝
Tactic:
aesop
Proof state after:
no goals
Theorem: refl_trans_sym_refl_trans
Proof state before:
case step.a
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
R : A → A → Prop
x y a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
a_ih✝ : refl_trans_sym_clos R b✝ c✝
⊢ refl_trans_sym_clos R ?step.b c✝
Tactic:
trivial
Proof state after:
no goals
Theorem: wedge_inc_refl_sym_trans
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ (fun R R' => ∀ (x y : A), R x y → R' x y) (wedge R) fun x x_1 => refl_trans_sym_clos R x x_1
Tactic:
intros x y wedge
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
wedge : _root_.wedge R x y
⊢ refl_trans_sym_clos R x y
Theorem: wedge_inc_refl_sym_trans
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
wedge : _root_.wedge R x y
⊢ refl_trans_sym_clos R x y
Tactic:
cases' wedge with w h
Proof state after:
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h : refl_trans_clos R w x ∧ refl_trans_clos R w y
⊢ refl_trans_sym_clos R x y
Theorem: wedge_inc_refl_sym_trans
Proof state before:
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h : refl_trans_clos R w x ∧ refl_trans_clos R w y
⊢ refl_trans_sym_clos R x y
Tactic:
cases' h with h1 h2
Proof state after:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ refl_trans_sym_clos R x y
Theorem: wedge_inc_refl_sym_trans
Proof state before:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ refl_trans_sym_clos R x y
Tactic:
apply (refl_trans_sym_clos.trans _ w)
Proof state after:
case intro.intro.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ refl_trans_sym_clos R x w

case intro.intro.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ refl_trans_sym_clos R w y
Theorem: wedge_inc_refl_sym_trans
Proof state before:
case intro.intro.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ refl_trans_sym_clos R x w

case intro.intro.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ refl_trans_sym_clos R w y
Tactic:
. apply refl_trans_sym_clos.inv
  apply refl_trans_sym_refl_trans; trivial
Proof state after:
case intro.intro.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ refl_trans_sym_clos R w y
Theorem: wedge_inc_refl_sym_trans
Proof state before:
case intro.intro.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ refl_trans_sym_clos R w y
Tactic:
. apply refl_trans_sym_refl_trans; trivial
Proof state after:
no goals
Theorem: wedge_inc_refl_sym_trans
Proof state before:
case intro.intro.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ refl_trans_sym_clos R x w
Tactic:
apply refl_trans_sym_clos.inv
Proof state after:
case intro.intro.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ refl_trans_sym_clos R w x
Theorem: wedge_inc_refl_sym_trans
Proof state before:
case intro.intro.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ refl_trans_sym_clos R w x
Tactic:
apply refl_trans_sym_refl_trans
Proof state after:
case intro.intro.a.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ refl_trans_clos R w x
Theorem: wedge_inc_refl_sym_trans
Proof state before:
case intro.intro.a.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ refl_trans_clos R w x
Tactic:
trivial
Proof state after:
no goals
Theorem: wedge_inc_refl_sym_trans
Proof state before:
case intro.intro.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ refl_trans_sym_clos R w y
Tactic:
apply refl_trans_sym_refl_trans
Proof state after:
case intro.intro.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ refl_trans_clos R w y
Theorem: wedge_inc_refl_sym_trans
Proof state before:
case intro.intro.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ refl_trans_clos R w y
Tactic:
trivial
Proof state after:
no goals
Theorem: church_rosser_implies_confluent
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ church_rosser R → confluent R
Tactic:
intros cr y z wedge
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
cr : church_rosser R
y z : A
wedge : _root_.wedge R y z
⊢ joins R y z
Theorem: church_rosser_implies_confluent
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
cr : church_rosser R
y z : A
wedge : _root_.wedge R y z
⊢ joins R y z
Tactic:
aesop
Proof state after:
no goals
Theorem: swap_joins
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
⊢ joins R x y → joins R y x
Tactic:
intros joins
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
joins : _root_.joins R x y
⊢ _root_.joins R y x
Theorem: swap_joins
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
joins : _root_.joins R x y
⊢ _root_.joins R y x
Tactic:
cases' joins with z h
Proof state after:
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
h : refl_trans_clos R x z ∧ refl_trans_clos R y z
⊢ joins R y x
Theorem: swap_joins
Proof state before:
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
h : refl_trans_clos R x z ∧ refl_trans_clos R y z
⊢ joins R y x
Tactic:
cases h
Proof state after:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
left✝ : refl_trans_clos R x z
right✝ : refl_trans_clos R y z
⊢ joins R y x
Theorem: swap_joins
Proof state before:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
left✝ : refl_trans_clos R x z
right✝ : refl_trans_clos R y z
⊢ joins R y x
Tactic:
exists z
Proof state after:
no goals
Theorem: red_joins
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
⊢ R x y → joins R y z → joins R x z
Tactic:
intros red_x_y joins_y_z
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
red_x_y : R x y
joins_y_z : joins R y z
⊢ joins R x z
Theorem: red_joins
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
red_x_y : R x y
joins_y_z : joins R y z
⊢ joins R x z
Tactic:
cases' joins_y_z with w h
Proof state after:
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
red_x_y : R x y
w : A
h : refl_trans_clos R y w ∧ refl_trans_clos R z w
⊢ joins R x z
Theorem: red_joins
Proof state before:
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
red_x_y : R x y
w : A
h : refl_trans_clos R y w ∧ refl_trans_clos R z w
⊢ joins R x z
Tactic:
cases h
Proof state after:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
red_x_y : R x y
w : A
left✝ : refl_trans_clos R y w
right✝ : refl_trans_clos R z w
⊢ joins R x z
Theorem: red_joins
Proof state before:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
red_x_y : R x y
w : A
left✝ : refl_trans_clos R y w
right✝ : refl_trans_clos R z w
⊢ joins R x z
Tactic:
exists w
Proof state after:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
red_x_y : R x y
w : A
left✝ : refl_trans_clos R y w
right✝ : refl_trans_clos R z w
⊢ refl_trans_clos R x w ∧ refl_trans_clos R z w
Theorem: red_joins
Proof state before:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
red_x_y : R x y
w : A
left✝ : refl_trans_clos R y w
right✝ : refl_trans_clos R z w
⊢ refl_trans_clos R x w ∧ refl_trans_clos R z w
Tactic:
aesop
Proof state after:
no goals
Theorem: reds_joins_left
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
⊢ refl_trans_clos R x y → joins R y z → joins R x z
Tactic:
intros red_x_y joins_y_z
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
red_x_y : refl_trans_clos R x y
joins_y_z : joins R y z
⊢ joins R x z
Theorem: reds_joins_left
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
red_x_y : refl_trans_clos R x y
joins_y_z : joins R y z
⊢ joins R x z
Tactic:
induction' red_x_y with _ _ _ _ _ _ ih
Proof state after:
case refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝ : A
joins_y_z : joins R a✝ z
⊢ joins R a✝ z

case step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
ih : joins R c✝ z → joins R b✝ z
joins_y_z : joins R c✝ z
⊢ joins R a✝² z
Theorem: reds_joins_left
Proof state before:
case refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝ : A
joins_y_z : joins R a✝ z
⊢ joins R a✝ z

case step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
ih : joins R c✝ z → joins R b✝ z
joins_y_z : joins R c✝ z
⊢ joins R a✝² z
Tactic:
. trivial
Proof state after:
case step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
ih : joins R c✝ z → joins R b✝ z
joins_y_z : joins R c✝ z
⊢ joins R a✝² z
Theorem: reds_joins_left
Proof state before:
case step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
ih : joins R c✝ z → joins R b✝ z
joins_y_z : joins R c✝ z
⊢ joins R a✝² z
Tactic:
. apply red_joins
  . trivial
  . have h' := ih joins_y_z
    trivial
Proof state after:
no goals
Theorem: reds_joins_left
Proof state before:
case refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝ : A
joins_y_z : joins R a✝ z
⊢ joins R a✝ z
Tactic:
trivial
Proof state after:
no goals
Theorem: reds_joins_left
Proof state before:
case step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
ih : joins R c✝ z → joins R b✝ z
joins_y_z : joins R c✝ z
⊢ joins R a✝² z
Tactic:
apply red_joins
Proof state after:
case step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
ih : joins R c✝ z → joins R b✝ z
joins_y_z : joins R c✝ z
⊢ R a✝² ?step.y

case step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
ih : joins R c✝ z → joins R b✝ z
joins_y_z : joins R c✝ z
⊢ joins R ?step.y z

case step.y
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
ih : joins R c✝ z → joins R b✝ z
joins_y_z : joins R c✝ z
⊢ A
Theorem: reds_joins_left
Proof state before:
case step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
ih : joins R c✝ z → joins R b✝ z
joins_y_z : joins R c✝ z
⊢ R a✝² ?step.y

case step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
ih : joins R c✝ z → joins R b✝ z
joins_y_z : joins R c✝ z
⊢ joins R ?step.y z

case step.y
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
ih : joins R c✝ z → joins R b✝ z
joins_y_z : joins R c✝ z
⊢ A
Tactic:
. trivial
Proof state after:
case step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
ih : joins R c✝ z → joins R b✝ z
joins_y_z : joins R c✝ z
⊢ joins R b✝ z
Theorem: reds_joins_left
Proof state before:
case step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
ih : joins R c✝ z → joins R b✝ z
joins_y_z : joins R c✝ z
⊢ joins R b✝ z
Tactic:
. have h' := ih joins_y_z
  trivial
Proof state after:
no goals
Theorem: reds_joins_left
Proof state before:
case step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
ih : joins R c✝ z → joins R b✝ z
joins_y_z : joins R c✝ z
⊢ R a✝² ?step.y
Tactic:
trivial
Proof state after:
no goals
Theorem: reds_joins_left
Proof state before:
case step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
ih : joins R c✝ z → joins R b✝ z
joins_y_z : joins R c✝ z
⊢ joins R b✝ z
Tactic:
have h' := ih joins_y_z
Proof state after:
case step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
ih : joins R c✝ z → joins R b✝ z
joins_y_z : joins R c✝ z
h' : joins R b✝ z
⊢ joins R b✝ z
Theorem: reds_joins_left
Proof state before:
case step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
ih : joins R c✝ z → joins R b✝ z
joins_y_z : joins R c✝ z
h' : joins R b✝ z
⊢ joins R b✝ z
Tactic:
trivial
Proof state after:
no goals
Theorem: reds_joins_right
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x z y : A
⊢ refl_trans_clos R x z → joins R y z → joins R y x
Tactic:
intros red_x_y joins_y_z
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x z y : A
red_x_y : refl_trans_clos R x z
joins_y_z : joins R y z
⊢ joins R y x
Theorem: reds_joins_right
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x z y : A
red_x_y : refl_trans_clos R x z
joins_y_z : joins R y z
⊢ joins R y x
Tactic:
apply swap_joins
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x z y : A
red_x_y : refl_trans_clos R x z
joins_y_z : joins R y z
⊢ joins R x y
Theorem: reds_joins_right
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x z y : A
red_x_y : refl_trans_clos R x z
joins_y_z : joins R y z
⊢ joins R x y
Tactic:
have joins_z_y := swap_joins _ joins_y_z
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x z y : A
red_x_y : refl_trans_clos R x z
joins_y_z : joins R y z
joins_z_y : joins R z y
⊢ joins R x y
Theorem: reds_joins_right
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x z y : A
red_x_y : refl_trans_clos R x z
joins_y_z : joins R y z
joins_z_y : joins R z y
⊢ joins R x y
Tactic:
apply (reds_joins_left _) <;> trivial
Proof state after:
no goals
Theorem: semi_confluent_implies_confluent
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ semi_confluent R → confluent R
Tactic:
intros semi x y wedge
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x y : A
wedge : _root_.wedge R x y
⊢ joins R x y
Theorem: semi_confluent_implies_confluent
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x y : A
wedge : _root_.wedge R x y
⊢ joins R x y
Tactic:
cases' wedge with w h
Proof state after:
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x y w : A
h : refl_trans_clos R w x ∧ refl_trans_clos R w y
⊢ joins R x y
Theorem: semi_confluent_implies_confluent
Proof state before:
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x y w : A
h : refl_trans_clos R w x ∧ refl_trans_clos R w y
⊢ joins R x y
Tactic:
cases' h with h1 h2
Proof state after:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ joins R x y
Theorem: semi_confluent_implies_confluent
Proof state before:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ joins R x y
Tactic:
revert h2 y
Proof state after:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x w : A
h1 : refl_trans_clos R w x
⊢ ∀ (y : A), refl_trans_clos R w y → joins R x y