Theorem: diamond_implies_confluent (Traat/chapter1.lean)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ diamond R → confluent R
Tactic:
intros sc
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
⊢ confluent R

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
⊢ confluent R
Tactic:
apply semi_confluent_implies_confluent
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
⊢ semi_confluent R

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
⊢ semi_confluent R
Tactic:
unfold semi_confluent
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

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
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

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
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

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
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✝

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
State after:
no goals

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
State after:
no goals

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 _
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✝

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
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

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
State after:
no goals

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
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

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)
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

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
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

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
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

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
State after:
no goals