internlm/Lean-Github huggingface dataset:
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 w : A
h1 : refl_trans_clos R w x
⊢ ∀ (y : A), refl_trans_clos R w y → joins R x y
Tactic:
induction' h1 with z x y y' red_x_y _red_y_y' ih <;> intros z red_x_z
Proof state after:
case intro.intro.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x w z✝ z : A
red_x_z : refl_trans_clos R z✝ z
⊢ joins R z✝ z

case intro.intro.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x✝ w x y y' : A
red_x_y : R x y
_red_y_y' : refl_trans_clos R y y'
ih : ∀ (y_1 : A), refl_trans_clos R y y_1 → joins R y' y_1
z : A
red_x_z : refl_trans_clos R x z
⊢ joins R y' z
Theorem: semi_confluent_implies_confluent
Proof state before:
case intro.intro.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x w z✝ z : A
red_x_z : refl_trans_clos R z✝ z
⊢ joins R z✝ z

case intro.intro.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x✝ w x y y' : A
red_x_y : R x y
_red_y_y' : refl_trans_clos R y y'
ih : ∀ (y_1 : A), refl_trans_clos R y y_1 → joins R y' y_1
z : A
red_x_z : refl_trans_clos R x z
⊢ joins R y' z
Tactic:
. exists z; aesop
Proof state after:
case intro.intro.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x✝ w x y y' : A
red_x_y : R x y
_red_y_y' : refl_trans_clos R y y'
ih : ∀ (y_1 : A), refl_trans_clos R y y_1 → joins R y' y_1
z : A
red_x_z : refl_trans_clos R x z
⊢ joins R y' z
Theorem: semi_confluent_implies_confluent
Proof state before:
case intro.intro.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x✝ w x y y' : A
red_x_y : R x y
_red_y_y' : refl_trans_clos R y y'
ih : ∀ (y_1 : A), refl_trans_clos R y y_1 → joins R y' y_1
z : A
red_x_z : refl_trans_clos R x z
⊢ joins R y' z
Tactic:
. have h := semi x y z red_x_y red_x_z
  cases' h with z' h
  cases' h with h1 h2
  have ih := ih z' h1
  apply reds_joins_right <;> trivial
Proof state after:
no goals
Theorem: semi_confluent_implies_confluent
Proof state before:
case intro.intro.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x w z✝ z : A
red_x_z : refl_trans_clos R z✝ z
⊢ joins R z✝ z
Tactic:
exists z
Proof state after:
case intro.intro.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x w z✝ z : A
red_x_z : refl_trans_clos R z✝ z
⊢ refl_trans_clos R z✝ z ∧ refl_trans_clos R z z
Theorem: semi_confluent_implies_confluent
Proof state before:
case intro.intro.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x w z✝ z : A
red_x_z : refl_trans_clos R z✝ z
⊢ refl_trans_clos R z✝ z ∧ refl_trans_clos R z z
Tactic:
aesop
Proof state after:
no goals
Theorem: semi_confluent_implies_confluent
Proof state before:
case intro.intro.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x✝ w x y y' : A
red_x_y : R x y
_red_y_y' : refl_trans_clos R y y'
ih : ∀ (y_1 : A), refl_trans_clos R y y_1 → joins R y' y_1
z : A
red_x_z : refl_trans_clos R x z
⊢ joins R y' z
Tactic:
have h := semi x y z red_x_y red_x_z
Proof state after:
case intro.intro.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x✝ w x y y' : A
red_x_y : R x y
_red_y_y' : refl_trans_clos R y y'
ih : ∀ (y_1 : A), refl_trans_clos R y y_1 → joins R y' y_1
z : A
red_x_z : refl_trans_clos R x z
h : joins R y z
⊢ joins R y' z
Theorem: semi_confluent_implies_confluent
Proof state before:
case intro.intro.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x✝ w x y y' : A
red_x_y : R x y
_red_y_y' : refl_trans_clos R y y'
ih : ∀ (y_1 : A), refl_trans_clos R y y_1 → joins R y' y_1
z : A
red_x_z : refl_trans_clos R x z
h : joins R y z
⊢ joins R y' z
Tactic:
cases' h with z' h
Proof state after:
case intro.intro.step.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x✝ w x y y' : A
red_x_y : R x y
_red_y_y' : refl_trans_clos R y y'
ih : ∀ (y_1 : A), refl_trans_clos R y y_1 → joins R y' y_1
z : A
red_x_z : refl_trans_clos R x z
z' : A
h : refl_trans_clos R y z' ∧ refl_trans_clos R z z'
⊢ joins R y' z
Theorem: semi_confluent_implies_confluent
Proof state before:
case intro.intro.step.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x✝ w x y y' : A
red_x_y : R x y
_red_y_y' : refl_trans_clos R y y'
ih : ∀ (y_1 : A), refl_trans_clos R y y_1 → joins R y' y_1
z : A
red_x_z : refl_trans_clos R x z
z' : A
h : refl_trans_clos R y z' ∧ refl_trans_clos R z z'
⊢ joins R y' z
Tactic:
cases' h with h1 h2
Proof state after:
case intro.intro.step.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x✝ w x y y' : A
red_x_y : R x y
_red_y_y' : refl_trans_clos R y y'
ih : ∀ (y_1 : A), refl_trans_clos R y y_1 → joins R y' y_1
z : A
red_x_z : refl_trans_clos R x z
z' : A
h1 : refl_trans_clos R y z'
h2 : refl_trans_clos R z z'
⊢ joins R y' z
Theorem: semi_confluent_implies_confluent
Proof state before:
case intro.intro.step.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x✝ w x y y' : A
red_x_y : R x y
_red_y_y' : refl_trans_clos R y y'
ih : ∀ (y_1 : A), refl_trans_clos R y y_1 → joins R y' y_1
z : A
red_x_z : refl_trans_clos R x z
z' : A
h1 : refl_trans_clos R y z'
h2 : refl_trans_clos R z z'
⊢ joins R y' z
Tactic:
have ih := ih z' h1
Proof state after:
case intro.intro.step.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x✝ w x y y' : A
red_x_y : R x y
_red_y_y' : refl_trans_clos R y y'
ih✝ : ∀ (y_1 : A), refl_trans_clos R y y_1 → joins R y' y_1
z : A
red_x_z : refl_trans_clos R x z
z' : A
h1 : refl_trans_clos R y z'
h2 : refl_trans_clos R z z'
ih : joins R y' z'
⊢ joins R y' z
Theorem: semi_confluent_implies_confluent
Proof state before:
case intro.intro.step.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x✝ w x y y' : A
red_x_y : R x y
_red_y_y' : refl_trans_clos R y y'
ih✝ : ∀ (y_1 : A), refl_trans_clos R y y_1 → joins R y' y_1
z : A
red_x_z : refl_trans_clos R x z
z' : A
h1 : refl_trans_clos R y z'
h2 : refl_trans_clos R z z'
ih : joins R y' z'
⊢ joins R y' z
Tactic:
apply reds_joins_right <;> trivial
Proof state after:
no goals
Theorem: diamond_implies_confluent
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ diamond R → confluent R
Tactic:
intros sc
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
⊢ confluent R
Theorem: diamond_implies_confluent
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
⊢ confluent R
Tactic:
apply semi_confluent_implies_confluent
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
⊢ semi_confluent R
Theorem: diamond_implies_confluent
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
⊢ semi_confluent R
Tactic:
unfold semi_confluent
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
⊢ ∀ (x y z : A), R x y → refl_trans_clos R x z → joins R y z
Theorem: diamond_implies_confluent
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
⊢ ∀ (x y z : A), R x y → refl_trans_clos R x z → joins R y z
Tactic:
intros x y z red h
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
x y z : A
red : R x y
h : refl_trans_clos R x z
⊢ joins R y z
Theorem: diamond_implies_confluent
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
x y z : A
red : R x y
h : refl_trans_clos R x z
⊢ joins R y z
Tactic:
revert y
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
x z : A
h : refl_trans_clos R x z
⊢ ∀ (y : A), R x y → joins R y z
Theorem: diamond_implies_confluent
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
x z : A
h : refl_trans_clos R x z
⊢ ∀ (y : A), R x y → joins R y z
Tactic:
induction h
Proof state after:
case a.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
x z a✝ : A
⊢ ∀ (y : A), R a✝ y → joins R y a✝

case a.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
x z a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
a_ih✝ : ∀ (y : A), R b✝ y → joins R y c✝
⊢ ∀ (y : A), R a✝² y → joins R y c✝
Theorem: diamond_implies_confluent
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
x z a✝ : A
⊢ ∀ (y : A), R a✝ y → joins R y a✝
Tactic:
case a.refl _ =>
  intros y _
  exists y; aesop
Proof state after:
no goals
Theorem: diamond_implies_confluent
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
x z a b c : A
red_a_b : R a b
_red_b_c : refl_trans_clos R b c
ih : ∀ (y : A), R b y → joins R y c
⊢ ∀ (y : A), R a y → joins R y c
Tactic:
case a.step a b c red_a_b _red_b_c ih =>
  intros d red_a_d
  have h := (sc _ _ _ red_a_b red_a_d)
  cases' h with e h
  cases' h with red_b_e red_d_e
  apply red_joins <;> aesop
Proof state after:
no goals
Theorem: diamond_implies_confluent
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
x z a✝ : A
⊢ ∀ (y : A), R a✝ y → joins R y a✝
Tactic:
intros y _
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
x z a✝ y : A
red✝ : R a✝ y
⊢ joins R y a✝
Theorem: diamond_implies_confluent
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
x z a✝ y : A
red✝ : R a✝ y
⊢ joins R y a✝
Tactic:
exists y
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
x z a✝ y : A
red✝ : R a✝ y
⊢ refl_trans_clos R y y ∧ refl_trans_clos R a✝ y
Theorem: diamond_implies_confluent
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
x z a✝ y : A
red✝ : R a✝ y
⊢ refl_trans_clos R y y ∧ refl_trans_clos R a✝ y
Tactic:
aesop
Proof state after:
no goals
Theorem: diamond_implies_confluent
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
x z a b c : A
red_a_b : R a b
_red_b_c : refl_trans_clos R b c
ih : ∀ (y : A), R b y → joins R y c
⊢ ∀ (y : A), R a y → joins R y c
Tactic:
intros d red_a_d
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
x z a b c : A
red_a_b : R a b
_red_b_c : refl_trans_clos R b c
ih : ∀ (y : A), R b y → joins R y c
d : A
red_a_d : R a d
⊢ joins R d c
Theorem: diamond_implies_confluent
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
x z a b c : A
red_a_b : R a b
_red_b_c : refl_trans_clos R b c
ih : ∀ (y : A), R b y → joins R y c
d : A
red_a_d : R a d
⊢ joins R d c
Tactic:
have h := (sc _ _ _ red_a_b red_a_d)
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
x z a b c : A
red_a_b : R a b
_red_b_c : refl_trans_clos R b c
ih : ∀ (y : A), R b y → joins R y c
d : A
red_a_d : R a d
h : ∃ w, R b w ∧ R d w
⊢ joins R d c
Theorem: diamond_implies_confluent
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
x z a b c : A
red_a_b : R a b
_red_b_c : refl_trans_clos R b c
ih : ∀ (y : A), R b y → joins R y c
d : A
red_a_d : R a d
h : ∃ w, R b w ∧ R d w
⊢ joins R d c
Tactic:
cases' h with e h
Proof state after:
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
x z a b c : A
red_a_b : R a b
_red_b_c : refl_trans_clos R b c
ih : ∀ (y : A), R b y → joins R y c
d : A
red_a_d : R a d
e : A
h : R b e ∧ R d e
⊢ joins R d c
Theorem: diamond_implies_confluent
Proof state before:
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
x z a b c : A
red_a_b : R a b
_red_b_c : refl_trans_clos R b c
ih : ∀ (y : A), R b y → joins R y c
d : A
red_a_d : R a d
e : A
h : R b e ∧ R d e
⊢ joins R d c
Tactic:
cases' h with red_b_e red_d_e
Proof state after:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
x z a b c : A
red_a_b : R a b
_red_b_c : refl_trans_clos R b c
ih : ∀ (y : A), R b y → joins R y c
d : A
red_a_d : R a d
e : A
red_b_e : R b e
red_d_e : R d e
⊢ joins R d c
Theorem: diamond_implies_confluent
Proof state before:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
x z a b c : A
red_a_b : R a b
_red_b_c : refl_trans_clos R b c
ih : ∀ (y : A), R b y → joins R y c
d : A
red_a_d : R a d
e : A
red_b_e : R b e
red_d_e : R d e
⊢ joins R d c
Tactic:
apply red_joins <;> aesop
Proof state after:
no goals
Theorem: confluent_implies_weakly_confluent
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ confluent R → weakly_confluent R
Tactic:
intros confl x y z red_x_y red_x_z
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y z : A
red_x_y : R x y
red_x_z : R x z
⊢ joins R y z
Theorem: confluent_implies_weakly_confluent
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y z : A
red_x_y : R x y
red_x_z : R x z
⊢ joins R y z
Tactic:
apply confl
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y z : A
red_x_y : R x y
red_x_z : R x z
⊢ wedge R y z
Theorem: confluent_implies_weakly_confluent
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y z : A
red_x_y : R x y
red_x_z : R x z
⊢ wedge R y z
Tactic:
exists x
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y z : A
red_x_y : R x y
red_x_z : R x z
⊢ refl_trans_clos R x y ∧ refl_trans_clos R x z
Theorem: confluent_implies_weakly_confluent
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y z : A
red_x_y : R x y
red_x_z : R x z
⊢ refl_trans_clos R x y ∧ refl_trans_clos R x z
Tactic:
constructor <;> apply refl_trans_clos.step <;> try constructor
Proof state after:
case a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y z : A
red_x_y : R x y
red_x_z : R x z
⊢ R x y

case a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y z : A
red_x_y : R x y
red_x_z : R x z
⊢ R x z
Theorem: confluent_implies_weakly_confluent
Proof state before:
case a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y z : A
red_x_y : R x y
red_x_z : R x z
⊢ R x y

case a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y z : A
red_x_y : R x y
red_x_z : R x z
⊢ R x z
Tactic:
. trivial
Proof state after:
case a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y z : A
red_x_y : R x y
red_x_z : R x z
⊢ R x z
Theorem: confluent_implies_weakly_confluent
Proof state before:
case a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y z : A
red_x_y : R x y
red_x_z : R x z
⊢ R x z
Tactic:
. trivial
Proof state after:
no goals
Theorem: confluent_implies_weakly_confluent
Proof state before:
case a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y z : A
red_x_y : R x y
red_x_z : R x z
⊢ refl_trans_clos R ?a.right.b✝ z
Tactic:
constructor
Proof state after:
no goals
Theorem: confluent_implies_weakly_confluent
Proof state before:
case a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y z : A
red_x_y : R x y
red_x_z : R x z
⊢ R x y
Tactic:
trivial
Proof state after:
no goals
Theorem: confluent_implies_weakly_confluent
Proof state before:
case a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y z : A
red_x_y : R x y
red_x_z : R x z
⊢ R x z
Tactic:
trivial
Proof state after:
no goals
Theorem: confluent_implies_church_rosser
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ confluent R → church_rosser R
Tactic:
intros confl
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
⊢ church_rosser R
Theorem: confluent_implies_church_rosser
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
⊢ church_rosser R
Tactic:
unfold church_rosser
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
⊢ ∀ (x y : A), refl_trans_sym_clos R x y → joins R x y
Theorem: confluent_implies_church_rosser
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
⊢ ∀ (x y : A), refl_trans_sym_clos R x y → joins R x y
Tactic:
intros x y red_x_y
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y : A
red_x_y : refl_trans_sym_clos R x y
⊢ joins R x y
Theorem: confluent_implies_church_rosser
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y : A
red_x_y : refl_trans_sym_clos R x y
⊢ joins R x y
Tactic:
induction red_x_y
Proof state after:
case refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y a✝ : A
⊢ joins R a✝ a✝

case base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y a✝¹ b✝ : A
a✝ : R a✝¹ b✝
⊢ joins R a✝¹ b✝

case trans
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y a✝² b✝ c✝ : A
a✝¹ : refl_trans_sym_clos R a✝² b✝
a✝ : refl_trans_sym_clos R b✝ c✝
a_ih✝¹ : joins R a✝² b✝
a_ih✝ : joins R b✝ c✝
⊢ joins R a✝² c✝

case inv
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y a✝¹ b✝ : A
a✝ : refl_trans_sym_clos R b✝ a✝¹
a_ih✝ : joins R b✝ a✝¹
⊢ joins R a✝¹ b✝
Theorem: confluent_implies_church_rosser
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y x : A
⊢ joins R x x
Tactic:
case refl x =>
  exists x ; repeat constructor
Proof state after:
no goals
Theorem: confluent_implies_church_rosser
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y✝ x y : A
red_x_y : R x y
⊢ joins R x y
Tactic:
case base x y red_x_y =>
  exists y; constructor <;> aesop
Proof state after:
no goals
Theorem: confluent_implies_church_rosser
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y✝ x y z : A
red_x_y : refl_trans_sym_clos R x y
red_y_z : refl_trans_sym_clos R y z
joins_x_y : joins R x y
joins_y_z : joins R y z
⊢ joins R x z
Tactic:
case trans x y z red_x_y red_y_z joins_x_y joins_y_z =>
  cases' joins_x_y with w1 h1
  cases' h1 with h11 h12
  cases' joins_y_z with w2 h2
  cases' h2 with h21 h22
  have h' : wedge R w1 w2 := by
    exists y
  have h := confl w1 w2 h'
  cases' h with w h''
  exists w; cases' h'' with h3 h4
  constructor <;> apply refl_trans_clos_transitive <;> trivial
Proof state after:
no goals
Theorem: confluent_implies_church_rosser
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y a✝¹ b✝ : A
a✝ : refl_trans_sym_clos R b✝ a✝¹
h : joins R b✝ a✝¹
⊢ joins R a✝¹ b✝
Tactic:
case inv _ h =>
  cases' h with w h'
  cases' h' with h1 h2
  exists w
Proof state after:
no goals
Theorem: confluent_implies_church_rosser
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y x : A
⊢ joins R x x
Tactic:
exists x
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y x : A
⊢ refl_trans_clos R x x ∧ refl_trans_clos R x x
Theorem: confluent_implies_church_rosser
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y x : A
⊢ refl_trans_clos R x x ∧ refl_trans_clos R x x
Tactic:
repeat constructor
Proof state after:
no goals
Theorem: confluent_implies_church_rosser
Proof state before:
case right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y x : A
⊢ refl_trans_clos R x x
Tactic:
constructor
Proof state after:
no goals
Theorem: confluent_implies_church_rosser
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y✝ x y : A
red_x_y : R x y
⊢ joins R x y
Tactic:
exists y
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y✝ x y : A
red_x_y : R x y
⊢ refl_trans_clos R x y ∧ refl_trans_clos R y y
Theorem: confluent_implies_church_rosser
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y✝ x y : A
red_x_y : R x y
⊢ refl_trans_clos R x y ∧ refl_trans_clos R y y
Tactic:
constructor <;> aesop
Proof state after:
no goals
Theorem: confluent_implies_church_rosser
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y✝ x y z : A
red_x_y : refl_trans_sym_clos R x y
red_y_z : refl_trans_sym_clos R y z
joins_x_y : joins R x y
joins_y_z : joins R y z
⊢ joins R x z
Tactic:
cases' joins_x_y with w1 h1
Proof state after:
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y✝ x y z : A
red_x_y : refl_trans_sym_clos R x y
red_y_z : refl_trans_sym_clos R y z
joins_y_z : joins R y z
w1 : A
h1 : refl_trans_clos R x w1 ∧ refl_trans_clos R y w1
⊢ joins R x z
Theorem: confluent_implies_church_rosser
Proof state before:
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y✝ x y z : A
red_x_y : refl_trans_sym_clos R x y
red_y_z : refl_trans_sym_clos R y z
joins_y_z : joins R y z
w1 : A
h1 : refl_trans_clos R x w1 ∧ refl_trans_clos R y w1
⊢ joins R x z
Tactic:
cases' h1 with h11 h12
Proof state after:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y✝ x y z : A
red_x_y : refl_trans_sym_clos R x y
red_y_z : refl_trans_sym_clos R y z
joins_y_z : joins R y z
w1 : A
h11 : refl_trans_clos R x w1
h12 : refl_trans_clos R y w1
⊢ joins R x z
Theorem: confluent_implies_church_rosser
Proof state before:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y✝ x y z : A
red_x_y : refl_trans_sym_clos R x y
red_y_z : refl_trans_sym_clos R y z
joins_y_z : joins R y z
w1 : A
h11 : refl_trans_clos R x w1
h12 : refl_trans_clos R y w1
⊢ joins R x z
Tactic:
cases' joins_y_z with w2 h2
Proof state after:
case intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y✝ x y z : A
red_x_y : refl_trans_sym_clos R x y
red_y_z : refl_trans_sym_clos R y z
w1 : A
h11 : refl_trans_clos R x w1
h12 : refl_trans_clos R y w1
w2 : A
h2 : refl_trans_clos R y w2 ∧ refl_trans_clos R z w2
⊢ joins R x z
Theorem: confluent_implies_church_rosser
Proof state before:
case intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y✝ x y z : A
red_x_y : refl_trans_sym_clos R x y
red_y_z : refl_trans_sym_clos R y z
w1 : A
h11 : refl_trans_clos R x w1
h12 : refl_trans_clos R y w1
w2 : A
h2 : refl_trans_clos R y w2 ∧ refl_trans_clos R z w2
⊢ joins R x z
Tactic:
cases' h2 with h21 h22
Proof state after:
case intro.intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y✝ x y z : A
red_x_y : refl_trans_sym_clos R x y
red_y_z : refl_trans_sym_clos R y z
w1 : A
h11 : refl_trans_clos R x w1
h12 : refl_trans_clos R y w1
w2 : A
h21 : refl_trans_clos R y w2
h22 : refl_trans_clos R z w2
⊢ joins R x z
Theorem: confluent_implies_church_rosser
Proof state before:
case intro.intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y✝ x y z : A
red_x_y : refl_trans_sym_clos R x y
red_y_z : refl_trans_sym_clos R y z
w1 : A
h11 : refl_trans_clos R x w1
h12 : refl_trans_clos R y w1
w2 : A
h21 : refl_trans_clos R y w2
h22 : refl_trans_clos R z w2
⊢ joins R x z
Tactic:
have h' : wedge R w1 w2 := by
  exists y
Proof state after:
case intro.intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y✝ x y z : A
red_x_y : refl_trans_sym_clos R x y
red_y_z : refl_trans_sym_clos R y z
w1 : A
h11 : refl_trans_clos R x w1
h12 : refl_trans_clos R y w1
w2 : A
h21 : refl_trans_clos R y w2
h22 : refl_trans_clos R z w2
h' : wedge R w1 w2
⊢ joins R x z