Theorem: confluent_implies_church_rosser (Traat/chapter1.lean)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ confluent R → church_rosser R
Tactic:
intros confl
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
⊢ church_rosser R

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
⊢ church_rosser R
Tactic:
unfold church_rosser
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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
h' : wedge R w1 w2
⊢ joins R x z
Tactic:
have h := confl w1 w2 h'
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
h : joins R w1 w2
⊢ joins R x z

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
h' : wedge R w1 w2
h : joins R w1 w2
⊢ joins R x z
Tactic:
cases' h with w h''
State after:
case intro.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
w : A
h'' : refl_trans_clos R w1 w ∧ refl_trans_clos R w2 w
⊢ joins R x z

State before:
case intro.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
w : A
h'' : refl_trans_clos R w1 w ∧ refl_trans_clos R w2 w
⊢ joins R x z
Tactic:
exists w
State after:
case intro.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
w : A
h'' : refl_trans_clos R w1 w ∧ refl_trans_clos R w2 w
⊢ refl_trans_clos R x w ∧ refl_trans_clos R z w

State before:
case intro.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
w : A
h'' : refl_trans_clos R w1 w ∧ refl_trans_clos R w2 w
⊢ refl_trans_clos R x w ∧ refl_trans_clos R z w
Tactic:
cases' h'' with h3 h4
State after:
case intro.intro.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
w : A
h3 : refl_trans_clos R w1 w
h4 : refl_trans_clos R w2 w
⊢ refl_trans_clos R x w ∧ refl_trans_clos R z w

State before:
case intro.intro.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
w : A
h3 : refl_trans_clos R w1 w
h4 : refl_trans_clos R w2 w
⊢ refl_trans_clos R x w ∧ refl_trans_clos R z w
Tactic:
constructor <;> apply refl_trans_clos_transitive <;> trivial
State after:
no goals

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
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
⊢ wedge R w1 w2
Tactic:
exists y
State after:
no goals

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:
cases' h with w h'
State after:
case intro
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✝¹
w : A
h' : refl_trans_clos R b✝ w ∧ refl_trans_clos R a✝¹ w
⊢ joins R a✝¹ b✝

State before:
case intro
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✝¹
w : A
h' : refl_trans_clos R b✝ w ∧ refl_trans_clos R a✝¹ w
⊢ joins R a✝¹ b✝
Tactic:
cases' h' with h1 h2
State after:
case intro.intro
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✝¹
w : A
h1 : refl_trans_clos R b✝ w
h2 : refl_trans_clos R a✝¹ w
⊢ joins R a✝¹ b✝

State before:
case intro.intro
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✝¹
w : A
h1 : refl_trans_clos R b✝ w
h2 : refl_trans_clos R a✝¹ w
⊢ joins R a✝¹ b✝
Tactic:
exists w
State after:
no goals