internlm/Lean-Github huggingface dataset:
Theorem: Container.M.bisim.lemma1
Proof 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)
n : Nat
h : ∀ (x y : M C), R x y → approx x n = approx y n
x y : M C
h₁ : R x y
h₂✝ : Approx.node (approx x (Nat.succ n)) = Container.M.node x
h₃✝ : Approx.node (approx y (Nat.succ n)) = Container.M.node y
nodex nodey node : C.A
k₁ k₂ : B C node → M C
eq₁ : destruct x = { fst := node, snd := k₁ }
eq₂ : destruct y = { fst := node, snd := k₂ }
kR : ∀ (i : B C node), R (k₁ i) (k₂ i)
cx : B C node → Approx C n
h₄ : approx x (Nat.succ n) = Approx.MStep node cx
h₂ : node = node
h₆✝ :
  ∀ (i : B C (Approx.node (Approx.MStep node cx))) (j : B C (destruct x).fst),
    HEq i j → cx i = approx (PSigma.snd (destruct x) j) n
cy : B C node → Approx C n
h₅ : approx y (Nat.succ n) = Approx.MStep node cy
h₃ : node = node
h₇ :
  ∀ (i : B C (Approx.node (Approx.MStep node cy))) (j : B C (destruct y).fst),
    HEq i j → cy i = approx (PSigma.snd (destruct y) j) n
i : B C node
h₆ : ∀ (i : B C node), cx i = approx (k₁ i) n
⊢ ∀ (i : B C { fst := node, snd := k₂ }.fst) (j : B C node), HEq i j → PSigma.snd { fst := node, snd := k₂ } i = k₂ j
Tactic:
intro i j heq
Proof 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)
n : Nat
h : ∀ (x y : M C), R x y → approx x n = approx y n
x y : M C
h₁ : R x y
h₂✝ : Approx.node (approx x (Nat.succ n)) = Container.M.node x
h₃✝ : Approx.node (approx y (Nat.succ n)) = Container.M.node y
nodex nodey node : C.A
k₁ k₂ : B C node → M C
eq₁ : destruct x = { fst := node, snd := k₁ }
eq₂ : destruct y = { fst := node, snd := k₂ }
kR : ∀ (i : B C node), R (k₁ i) (k₂ i)
cx : B C node → Approx C n
h₄ : approx x (Nat.succ n) = Approx.MStep node cx
h₂ : node = node
h₆✝ :
  ∀ (i : B C (Approx.node (Approx.MStep node cx))) (j : B C (destruct x).fst),
    HEq i j → cx i = approx (PSigma.snd (destruct x) j) n
cy : B C node → Approx C n
h₅ : approx y (Nat.succ n) = Approx.MStep node cy
h₃ : node = node
h₇ :
  ∀ (i : B C (Approx.node (Approx.MStep node cy))) (j : B C (destruct y).fst),
    HEq i j → cy i = approx (PSigma.snd (destruct y) j) n
i✝ : B C node
h₆ : ∀ (i : B C node), cx i = approx (k₁ i) n
i : B C { fst := node, snd := k₂ }.fst
j : B C node
heq : HEq i j
⊢ PSigma.snd { fst := node, snd := k₂ } i = k₂ j
Theorem: Container.M.bisim.lemma1
Proof 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)
n : Nat
h : ∀ (x y : M C), R x y → approx x n = approx y n
x y : M C
h₁ : R x y
h₂✝ : Approx.node (approx x (Nat.succ n)) = Container.M.node x
h₃✝ : Approx.node (approx y (Nat.succ n)) = Container.M.node y
nodex nodey node : C.A
k₁ k₂ : B C node → M C
eq₁ : destruct x = { fst := node, snd := k₁ }
eq₂ : destruct y = { fst := node, snd := k₂ }
kR : ∀ (i : B C node), R (k₁ i) (k₂ i)
cx : B C node → Approx C n
h₄ : approx x (Nat.succ n) = Approx.MStep node cx
h₂ : node = node
h₆✝ :
  ∀ (i : B C (Approx.node (Approx.MStep node cx))) (j : B C (destruct x).fst),
    HEq i j → cx i = approx (PSigma.snd (destruct x) j) n
cy : B C node → Approx C n
h₅ : approx y (Nat.succ n) = Approx.MStep node cy
h₃ : node = node
h₇ :
  ∀ (i : B C (Approx.node (Approx.MStep node cy))) (j : B C (destruct y).fst),
    HEq i j → cy i = approx (PSigma.snd (destruct y) j) n
i✝ : B C node
h₆ : ∀ (i : B C node), cx i = approx (k₁ i) n
i : B C { fst := node, snd := k₂ }.fst
j : B C node
heq : HEq i j
⊢ PSigma.snd { fst := node, snd := k₂ } i = k₂ j
Tactic:
cases heq
Proof state after:
case refl
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)
n : Nat
h : ∀ (x y : M C), R x y → approx x n = approx y n
x y : M C
h₁ : R x y
h₂✝ : Approx.node (approx x (Nat.succ n)) = Container.M.node x
h₃✝ : Approx.node (approx y (Nat.succ n)) = Container.M.node y
nodex nodey node : C.A
k₁ k₂ : B C node → M C
eq₁ : destruct x = { fst := node, snd := k₁ }
eq₂ : destruct y = { fst := node, snd := k₂ }
kR : ∀ (i : B C node), R (k₁ i) (k₂ i)
cx : B C node → Approx C n
h₄ : approx x (Nat.succ n) = Approx.MStep node cx
h₂ : node = node
h₆✝ :
  ∀ (i : B C (Approx.node (Approx.MStep node cx))) (j : B C (destruct x).fst),
    HEq i j → cx i = approx (PSigma.snd (destruct x) j) n
cy : B C node → Approx C n
h₅ : approx y (Nat.succ n) = Approx.MStep node cy
h₃ : node = node
h₇ :
  ∀ (i : B C (Approx.node (Approx.MStep node cy))) (j : B C (destruct y).fst),
    HEq i j → cy i = approx (PSigma.snd (destruct y) j) n
i✝ : B C node
h₆ : ∀ (i : B C node), cx i = approx (k₁ i) n
i : B C { fst := node, snd := k₂ }.fst
⊢ PSigma.snd { fst := node, snd := k₂ } i = k₂ i
Theorem: Container.M.bisim.lemma1
Proof state before:
case refl
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)
n : Nat
h : ∀ (x y : M C), R x y → approx x n = approx y n
x y : M C
h₁ : R x y
h₂✝ : Approx.node (approx x (Nat.succ n)) = Container.M.node x
h₃✝ : Approx.node (approx y (Nat.succ n)) = Container.M.node y
nodex nodey node : C.A
k₁ k₂ : B C node → M C
eq₁ : destruct x = { fst := node, snd := k₁ }
eq₂ : destruct y = { fst := node, snd := k₂ }
kR : ∀ (i : B C node), R (k₁ i) (k₂ i)
cx : B C node → Approx C n
h₄ : approx x (Nat.succ n) = Approx.MStep node cx
h₂ : node = node
h₆✝ :
  ∀ (i : B C (Approx.node (Approx.MStep node cx))) (j : B C (destruct x).fst),
    HEq i j → cx i = approx (PSigma.snd (destruct x) j) n
cy : B C node → Approx C n
h₅ : approx y (Nat.succ n) = Approx.MStep node cy
h₃ : node = node
h₇ :
  ∀ (i : B C (Approx.node (Approx.MStep node cy))) (j : B C (destruct y).fst),
    HEq i j → cy i = approx (PSigma.snd (destruct y) j) n
i✝ : B C node
h₆ : ∀ (i : B C node), cx i = approx (k₁ i) n
i : B C { fst := node, snd := k₂ }.fst
⊢ PSigma.snd { fst := node, snd := k₂ } i = k₂ i
Tactic:
rfl
Proof state after:
no goals
Theorem: Container.M.bisim.lemma1
Proof 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)
n : Nat
h✝ : ∀ (x y : M C), R x y → approx x n = approx y n
x y : M C
h₁ : R x y
h₂✝ : Approx.node (approx x (Nat.succ n)) = Container.M.node x
h₃✝ : Approx.node (approx y (Nat.succ n)) = Container.M.node y
nodex nodey node : C.A
k₁ k₂ : B C node → M C
eq₁ : destruct x = { fst := node, snd := k₁ }
eq₂ : destruct y = { fst := node, snd := k₂ }
kR : ∀ (i : B C node), R (k₁ i) (k₂ i)
cx : B C node → Approx C n
h₄ : approx x (Nat.succ n) = Approx.MStep node cx
h₂ : node = node
h₆✝ :
  ∀ (i : B C (Approx.node (Approx.MStep node cx))) (j : B C (destruct x).fst),
    HEq i j → cx i = approx (PSigma.snd (destruct x) j) n
cy : B C node → Approx C n
h₅ : approx y (Nat.succ n) = Approx.MStep node cy
h₃ : node = node
h₇ :
  ∀ (i : B C (Approx.node (Approx.MStep node cy))) (j : B C (destruct y).fst),
    HEq i j → cy i = approx (PSigma.snd (destruct y) j) n
i✝ : B C node
h₆ : ∀ (i : B C node), cx i = approx (k₁ i) n
h : ∀ (i : B C (destruct y).fst) (j : B C node), HEq i j → PSigma.snd (destruct y) i = k₂ j
i : B C node
⊢ B C node = B C (destruct y).fst
Tactic:
simp [congrArg (λ x => x.1) eq₂]
Proof state after:
no goals
Theorem: Container.M.bisim.lemma1
Proof 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)
n : Nat
h✝ : ∀ (x y : M C), R x y → approx x n = approx y n
x y : M C
h₁ : R x y
h₂✝ : Approx.node (approx x (Nat.succ n)) = Container.M.node x
h₃✝ : Approx.node (approx y (Nat.succ n)) = Container.M.node y
nodex nodey node : C.A
k₁ k₂ : B C node → M C
eq₁ : destruct x = { fst := node, snd := k₁ }
eq₂ : destruct y = { fst := node, snd := k₂ }
kR : ∀ (i : B C node), R (k₁ i) (k₂ i)
cx : B C node → Approx C n
h₄ : approx x (Nat.succ n) = Approx.MStep node cx
h₂ : node = node
h₆✝ :
  ∀ (i : B C (Approx.node (Approx.MStep node cx))) (j : B C (destruct x).fst),
    HEq i j → cx i = approx (PSigma.snd (destruct x) j) n
cy : B C node → Approx C n
h₅ : approx y (Nat.succ n) = Approx.MStep node cy
h₃ : node = node
h₇ :
  ∀ (i : B C (Approx.node (Approx.MStep node cy))) (j : B C (destruct y).fst),
    HEq i j → cy i = approx (PSigma.snd (destruct y) j) n
i✝ : B C node
h₆ : ∀ (i : B C node), cx i = approx (k₁ i) n
h : ∀ (i : B C (destruct y).fst) (j : B C node), HEq i j → PSigma.snd (destruct y) i = k₂ j
i : B C node
⊢ approx (PSigma.snd (destruct y) (cast (_ : B C node = B C (destruct y).fst) i)) n = approx (k₂ i) n
Tactic:
rw [h]
Proof state after:
case a
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)
n : Nat
h✝ : ∀ (x y : M C), R x y → approx x n = approx y n
x y : M C
h₁ : R x y
h₂✝ : Approx.node (approx x (Nat.succ n)) = Container.M.node x
h₃✝ : Approx.node (approx y (Nat.succ n)) = Container.M.node y
nodex nodey node : C.A
k₁ k₂ : B C node → M C
eq₁ : destruct x = { fst := node, snd := k₁ }
eq₂ : destruct y = { fst := node, snd := k₂ }
kR : ∀ (i : B C node), R (k₁ i) (k₂ i)
cx : B C node → Approx C n
h₄ : approx x (Nat.succ n) = Approx.MStep node cx
h₂ : node = node
h₆✝ :
  ∀ (i : B C (Approx.node (Approx.MStep node cx))) (j : B C (destruct x).fst),
    HEq i j → cx i = approx (PSigma.snd (destruct x) j) n
cy : B C node → Approx C n
h₅ : approx y (Nat.succ n) = Approx.MStep node cy
h₃ : node = node
h₇ :
  ∀ (i : B C (Approx.node (Approx.MStep node cy))) (j : B C (destruct y).fst),
    HEq i j → cy i = approx (PSigma.snd (destruct y) j) n
i✝ : B C node
h₆ : ∀ (i : B C node), cx i = approx (k₁ i) n
h : ∀ (i : B C (destruct y).fst) (j : B C node), HEq i j → PSigma.snd (destruct y) i = k₂ j
i : B C node
⊢ HEq (cast (_ : B C node = B C (destruct y).fst) i) i
Theorem: Container.M.bisim.lemma1
Proof state before:
case a
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)
n : Nat
h✝ : ∀ (x y : M C), R x y → approx x n = approx y n
x y : M C
h₁ : R x y
h₂✝ : Approx.node (approx x (Nat.succ n)) = Container.M.node x
h₃✝ : Approx.node (approx y (Nat.succ n)) = Container.M.node y
nodex nodey node : C.A
k₁ k₂ : B C node → M C
eq₁ : destruct x = { fst := node, snd := k₁ }
eq₂ : destruct y = { fst := node, snd := k₂ }
kR : ∀ (i : B C node), R (k₁ i) (k₂ i)
cx : B C node → Approx C n
h₄ : approx x (Nat.succ n) = Approx.MStep node cx
h₂ : node = node
h₆✝ :
  ∀ (i : B C (Approx.node (Approx.MStep node cx))) (j : B C (destruct x).fst),
    HEq i j → cx i = approx (PSigma.snd (destruct x) j) n
cy : B C node → Approx C n
h₅ : approx y (Nat.succ n) = Approx.MStep node cy
h₃ : node = node
h₇ :
  ∀ (i : B C (Approx.node (Approx.MStep node cy))) (j : B C (destruct y).fst),
    HEq i j → cy i = approx (PSigma.snd (destruct y) j) n
i✝ : B C node
h₆ : ∀ (i : B C node), cx i = approx (k₁ i) n
h : ∀ (i : B C (destruct y).fst) (j : B C node), HEq i j → PSigma.snd (destruct y) i = k₂ j
i : B C node
⊢ HEq (cast (_ : B C node = B C (destruct y).fst) i) i
Tactic:
apply cast_heq
Proof state after:
no goals
Theorem: Container.M.bisim.lemma1
Proof 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)
n : Nat
h✝ : ∀ (x y : M C), R x y → approx x n = approx y n
x y : M C
h₁ : R x y
h₂✝ : Approx.node (approx x (Nat.succ n)) = Container.M.node x
h₃✝ : Approx.node (approx y (Nat.succ n)) = Container.M.node y
nodex nodey node : C.A
k₁ k₂ : B C node → M C
eq₁ : destruct x = { fst := node, snd := k₁ }
eq₂ : destruct y = { fst := node, snd := k₂ }
kR : ∀ (i : B C node), R (k₁ i) (k₂ i)
cx : B C node → Approx C n
h₄ : approx x (Nat.succ n) = Approx.MStep node cx
h₂ : node = node
h₆✝ :
  ∀ (i : B C (Approx.node (Approx.MStep node cx))) (j : B C (destruct x).fst),
    HEq i j → cx i = approx (PSigma.snd (destruct x) j) n
cy : B C node → Approx C n
h₅ : approx y (Nat.succ n) = Approx.MStep node cy
h₃ : node = node
h₇ :
  ∀ (i : B C (Approx.node (Approx.MStep node cy))) (j : B C (destruct y).fst),
    HEq i j → cy i = approx (PSigma.snd (destruct y) j) n
i✝ : B C node
h₆ : ∀ (i : B C node), cx i = approx (k₁ i) n
h : ∀ (i : B C (destruct y).fst) (j : B C node), HEq i j → PSigma.snd (destruct y) i = k₂ j
i : B C node
⊢ HEq i (cast (_ : B C node = B C (destruct y).fst) i)
Tactic:
apply HEq.symm
Proof 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)
n : Nat
h✝ : ∀ (x y : M C), R x y → approx x n = approx y n
x y : M C
h₁ : R x y
h₂✝ : Approx.node (approx x (Nat.succ n)) = Container.M.node x
h₃✝ : Approx.node (approx y (Nat.succ n)) = Container.M.node y
nodex nodey node : C.A
k₁ k₂ : B C node → M C
eq₁ : destruct x = { fst := node, snd := k₁ }
eq₂ : destruct y = { fst := node, snd := k₂ }
kR : ∀ (i : B C node), R (k₁ i) (k₂ i)
cx : B C node → Approx C n
h₄ : approx x (Nat.succ n) = Approx.MStep node cx
h₂ : node = node
h₆✝ :
  ∀ (i : B C (Approx.node (Approx.MStep node cx))) (j : B C (destruct x).fst),
    HEq i j → cx i = approx (PSigma.snd (destruct x) j) n
cy : B C node → Approx C n
h₅ : approx y (Nat.succ n) = Approx.MStep node cy
h₃ : node = node
h₇ :
  ∀ (i : B C (Approx.node (Approx.MStep node cy))) (j : B C (destruct y).fst),
    HEq i j → cy i = approx (PSigma.snd (destruct y) j) n
i✝ : B C node
h₆ : ∀ (i : B C node), cx i = approx (k₁ i) n
h : ∀ (i : B C (destruct y).fst) (j : B C node), HEq i j → PSigma.snd (destruct y) i = k₂ j
i : B C node
⊢ HEq (cast (_ : B C node = B C (destruct y).fst) i) i
Theorem: Container.M.bisim.lemma1
Proof 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)
n : Nat
h✝ : ∀ (x y : M C), R x y → approx x n = approx y n
x y : M C
h₁ : R x y
h₂✝ : Approx.node (approx x (Nat.succ n)) = Container.M.node x
h₃✝ : Approx.node (approx y (Nat.succ n)) = Container.M.node y
nodex nodey node : C.A
k₁ k₂ : B C node → M C
eq₁ : destruct x = { fst := node, snd := k₁ }
eq₂ : destruct y = { fst := node, snd := k₂ }
kR : ∀ (i : B C node), R (k₁ i) (k₂ i)
cx : B C node → Approx C n
h₄ : approx x (Nat.succ n) = Approx.MStep node cx
h₂ : node = node
h₆✝ :
  ∀ (i : B C (Approx.node (Approx.MStep node cx))) (j : B C (destruct x).fst),
    HEq i j → cx i = approx (PSigma.snd (destruct x) j) n
cy : B C node → Approx C n
h₅ : approx y (Nat.succ n) = Approx.MStep node cy
h₃ : node = node
h₇ :
  ∀ (i : B C (Approx.node (Approx.MStep node cy))) (j : B C (destruct y).fst),
    HEq i j → cy i = approx (PSigma.snd (destruct y) j) n
i✝ : B C node
h₆ : ∀ (i : B C node), cx i = approx (k₁ i) n
h : ∀ (i : B C (destruct y).fst) (j : B C node), HEq i j → PSigma.snd (destruct y) i = k₂ j
i : B C node
⊢ HEq (cast (_ : B C node = B C (destruct y).fst) i) i
Tactic:
apply cast_heq
Proof state after:
no goals
Theorem: Container.M.bisim
Proof 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₁
Proof 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
Theorem: Container.M.bisim
Proof 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₂]
Proof 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
Theorem: Container.M.bisim
Proof 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
Proof 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
Theorem: Container.M.bisim
Proof 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₁
Proof state after:
no goals
Theorem: Container.M.bisim
Proof 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
Proof 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
Theorem: Container.M.bisim
Proof 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
Proof 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✝ }
Theorem: Container.M.bisim
Proof 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₂
Proof 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✝ }
Theorem: Container.M.bisim
Proof 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₂]
Proof state after:
no goals
Theorem: Free.by_cases
Proof state before:
F : Type u → Type u
inst : QPF F
R : Type u
motive : Free F R → Sort u_1
pure : (r : R) → motive (Pure.pure r)
free : (f : F (Free F R)) → motive (Free.free f)
⊢ (x : Free F R) → motive x
Tactic:
intro x
Proof state after:
F : Type u → Type u
inst : QPF F
R : Type u
motive : Free F R → Sort u_1
pure : (r : R) → motive (Pure.pure r)
free : (f : F (Free F R)) → motive (Free.free f)
x : Free F R
⊢ motive x
Theorem: Free.by_cases
Proof state before:
F : Type u → Type u
inst : QPF F
R : Type u
motive : Free F R → Sort u_1
pure : (r : R) → motive (Pure.pure r)
free : (f : F (Free F R)) → motive (Free.free f)
x : Free F R
⊢ motive x
Tactic:
rw [←construct_destruct x]
Proof state after:
F : Type u → Type u
inst : QPF F
R : Type u
motive : Free F R → Sort u_1
pure : (r : R) → motive (Pure.pure r)
free : (f : F (Free F R)) → motive (Free.free f)
x : Free F R
⊢ motive (construct (destruct x))
Theorem: Free.by_cases
Proof state before:
F : Type u → Type u
inst : QPF F
R : Type u
motive : Free F R → Sort u_1
pure : (r : R) → motive (Pure.pure r)
free : (f : F (Free F R)) → motive (Free.free f)
x : Free F R
⊢ motive (construct (destruct x))
Tactic:
cases destruct x with
| Pure r =>
  exact pure r
| Free f =>
  exact free f
Proof state after:
no goals
Theorem: Free.by_cases
Proof state before:
case Pure
F : Type u → Type u
inst : QPF F
R : Type u
motive : Free F R → Sort u_1
pure : (r : R) → motive (Pure.pure r)
free : (f : F (Free F R)) → motive (Free.free f)
x : Free F R
r : R
⊢ motive (construct (FreeF.Pure r))
Tactic:
exact pure r
Proof state after:
no goals