Theorem: confluent_unique_nf (Traat/chapter1.lean)

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

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

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

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

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

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

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

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

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

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