Theorem: Container.M.bisim (CoInd/M.lean)

State before:
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
⊢ ∀ (x y : M C), R x y → x = y
Tactic:
intro x y h₁
State after:
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
x y : M C
h₁ : R x y
⊢ x = y

State before:
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
x y : M C
h₁ : R x y
⊢ x = y
Tactic:
suffices h₂: x.approx = y.approx by
  cases x
  cases y
  simp only  at h₂
  simp [h₂]
State after:
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
x y : M C
h₁ : R x y
⊢ x.approx = y.approx

State before:
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
x y : M C
h₁ : R x y
⊢ x.approx = y.approx
Tactic:
funext n
State after:
case h
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
x y : M C
h₁ : R x y
n : Nat
⊢ approx x n = approx y n

State before:
case h
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
x y : M C
h₁ : R x y
n : Nat
⊢ approx x n = approx y n
Tactic:
apply bisim.lemma1 R h₀ x y n h₁
State after:
no goals

State before:
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
x y : M C
h₁ : R x y
h₂ : x.approx = y.approx
⊢ x = y
Tactic:
cases x
State after:
case mk
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
y : M C
approx✝ : (n : Nat) → Approx C n
agrees✝ : ∀ (n : Nat), Agree (approx✝ n) (approx✝ (Nat.succ n))
h₁ : R { approx := approx✝, agrees := agrees✝ } y
h₂ : { approx := approx✝, agrees := agrees✝ }.approx = y.approx
⊢ { approx := approx✝, agrees := agrees✝ } = y

State before:
case mk
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
y : M C
approx✝ : (n : Nat) → Approx C n
agrees✝ : ∀ (n : Nat), Agree (approx✝ n) (approx✝ (Nat.succ n))
h₁ : R { approx := approx✝, agrees := agrees✝ } y
h₂ : { approx := approx✝, agrees := agrees✝ }.approx = y.approx
⊢ { approx := approx✝, agrees := agrees✝ } = y
Tactic:
cases y
State after:
case mk.mk
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
approx✝¹ : (n : Nat) → Approx C n
agrees✝¹ : ∀ (n : Nat), Agree (approx✝¹ n) (approx✝¹ (Nat.succ n))
approx✝ : (n : Nat) → Approx C n
agrees✝ : ∀ (n : Nat), Agree (approx✝ n) (approx✝ (Nat.succ n))
h₁ : R { approx := approx✝¹, agrees := agrees✝¹ } { approx := approx✝, agrees := agrees✝ }
h₂ : { approx := approx✝¹, agrees := agrees✝¹ }.approx = { approx := approx✝, agrees := agrees✝ }.approx
⊢ { approx := approx✝¹, agrees := agrees✝¹ } = { approx := approx✝, agrees := agrees✝ }

State before:
case mk.mk
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
approx✝¹ : (n : Nat) → Approx C n
agrees✝¹ : ∀ (n : Nat), Agree (approx✝¹ n) (approx✝¹ (Nat.succ n))
approx✝ : (n : Nat) → Approx C n
agrees✝ : ∀ (n : Nat), Agree (approx✝ n) (approx✝ (Nat.succ n))
h₁ : R { approx := approx✝¹, agrees := agrees✝¹ } { approx := approx✝, agrees := agrees✝ }
h₂ : { approx := approx✝¹, agrees := agrees✝¹ }.approx = { approx := approx✝, agrees := agrees✝ }.approx
⊢ { approx := approx✝¹, agrees := agrees✝¹ } = { approx := approx✝, agrees := agrees✝ }
Tactic:
simp only  at h₂
State after:
case mk.mk
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
approx✝¹ : (n : Nat) → Approx C n
agrees✝¹ : ∀ (n : Nat), Agree (approx✝¹ n) (approx✝¹ (Nat.succ n))
approx✝ : (n : Nat) → Approx C n
agrees✝ : ∀ (n : Nat), Agree (approx✝ n) (approx✝ (Nat.succ n))
h₁ : R { approx := approx✝¹, agrees := agrees✝¹ } { approx := approx✝, agrees := agrees✝ }
h₂ : approx✝¹ = approx✝
⊢ { approx := approx✝¹, agrees := agrees✝¹ } = { approx := approx✝, agrees := agrees✝ }

State before:
case mk.mk
C : Container
R : M C → M C → Prop
h₀ :
  ∀ (x y : M C),
    R x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (i : B C node), R (k₁ i) (k₂ i)
approx✝¹ : (n : Nat) → Approx C n
agrees✝¹ : ∀ (n : Nat), Agree (approx✝¹ n) (approx✝¹ (Nat.succ n))
approx✝ : (n : Nat) → Approx C n
agrees✝ : ∀ (n : Nat), Agree (approx✝ n) (approx✝ (Nat.succ n))
h₁ : R { approx := approx✝¹, agrees := agrees✝¹ } { approx := approx✝, agrees := agrees✝ }
h₂ : approx✝¹ = approx✝
⊢ { approx := approx✝¹, agrees := agrees✝¹ } = { approx := approx✝, agrees := agrees✝ }
Tactic:
simp [h₂]
State after:
no goals