internlm/Lean-Github huggingface dataset:
Theorem: QPF.M.construct_destruct
Proof state before:
case h₀
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀ : R x y
⊢ liftr F R (destruct x) (destruct y)
Tactic:
have h₀ := congrArg destruct h₀
Proof state after:
case h₀
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = destruct (construct (destruct y))
⊢ liftr F R (destruct x) (destruct y)
Theorem: QPF.M.construct_destruct
Proof state before:
case h₀
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = destruct (construct (destruct y))
⊢ liftr F R (destruct x) (destruct y)
Tactic:
simp [liftr]
Proof state after:
case h₀
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = destruct (construct (destruct y))
⊢ ∃ z, (fun x => (↑x).fst) <$> z = destruct x ∧ (fun x => (↑x).snd) <$> z = destruct y
Theorem: QPF.M.construct_destruct
Proof state before:
case h₀
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = destruct (construct (destruct y))
⊢ ∃ z, (fun x => (↑x).fst) <$> z = destruct x ∧ (fun x => (↑x).snd) <$> z = destruct y
Tactic:
simp only [construct, destruct_corec, construct.automaton] at h₀
Proof state after:
case h₀
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ ∃ z, (fun x => (↑x).fst) <$> z = destruct x ∧ (fun x => (↑x).snd) <$> z = destruct y
Theorem: QPF.M.construct_destruct
Proof state before:
case h₀
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ ∃ z, (fun x => (↑x).fst) <$> z = destruct x ∧ (fun x => (↑x).snd) <$> z = destruct y
Tactic:
exists Functor.map (λ a => ⟨⟨construct <| destruct a, a⟩, by simp⟩) (destruct y)
Proof state after:
case h₀
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ (fun x => (↑x).fst) <$>
        (fun a =>
            { val := (construct (destruct a), a),
              property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
          destruct y =
      destruct x ∧
    (fun x => (↑x).snd) <$>
        (fun a =>
            { val := (construct (destruct a), a),
              property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
          destruct y =
      destruct y
Theorem: QPF.M.construct_destruct
Proof state before:
case h₀
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ (fun x => (↑x).fst) <$>
        (fun a =>
            { val := (construct (destruct a), a),
              property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
          destruct y =
      destruct x ∧
    (fun x => (↑x).snd) <$>
        (fun a =>
            { val := (construct (destruct a), a),
              property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
          destruct y =
      destruct y
Tactic:
rw [h₀]
Proof state after:
case h₀
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ (fun x => (↑x).fst) <$>
        (fun a =>
            { val := (construct (destruct a), a),
              property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
          destruct y =
      (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y ∧
    (fun x => (↑x).snd) <$>
        (fun a =>
            { val := (construct (destruct a), a),
              property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
          destruct y =
      destruct y
Theorem: QPF.M.construct_destruct
Proof state before:
case h₀
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ (fun x => (↑x).fst) <$>
        (fun a =>
            { val := (construct (destruct a), a),
              property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
          destruct y =
      (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y ∧
    (fun x => (↑x).snd) <$>
        (fun a =>
            { val := (construct (destruct a), a),
              property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
          destruct y =
      destruct y
Tactic:
constructor
Proof state after:
case h₀.left
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ (fun x => (↑x).fst) <$>
      (fun a =>
          { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
        destruct y =
    (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y

case h₀.right
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ (fun x => (↑x).snd) <$>
      (fun a =>
          { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
        destruct y =
    destruct y
Theorem: QPF.M.construct_destruct
Proof state before:
case h₀.left
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ (fun x => (↑x).fst) <$>
      (fun a =>
          { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
        destruct y =
    (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y

case h₀.right
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ (fun x => (↑x).snd) <$>
      (fun a =>
          { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
        destruct y =
    destruct y
Tactic:
. simp only [←QPF.map_comp]
  rfl
Proof state after:
case h₀.right
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ (fun x => (↑x).snd) <$>
      (fun a =>
          { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
        destruct y =
    destruct y
Theorem: QPF.M.construct_destruct
Proof state before:
case h₀.right
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ (fun x => (↑x).snd) <$>
      (fun a =>
          { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
        destruct y =
    destruct y
Tactic:
. rw [←QPF.M.map_comp]
  have : inst.map id (destruct y) = destruct y := by rw [QPF.map_id]
  apply Eq.trans _ this
  apply congrFun
  funext _
  rfl
Proof state after:
no goals
Theorem: QPF.M.construct_destruct
Proof state before:
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
a : M F
⊢ (construct (destruct a), a).fst = construct (destruct (construct (destruct a), a).snd)
Tactic:
simp
Proof state after:
no goals
Theorem: QPF.M.construct_destruct
Proof state before:
case h₀.left
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ (fun x => (↑x).fst) <$>
      (fun a =>
          { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
        destruct y =
    (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
Tactic:
simp only [←QPF.map_comp]
Proof state after:
case h₀.left
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ ((fun x => (↑x).fst) ∘ fun a =>
        { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
      destruct y =
    ((fun x => corec (Functor.map destruct) x) ∘ destruct) <$> destruct y
Theorem: QPF.M.construct_destruct
Proof state before:
case h₀.left
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ ((fun x => (↑x).fst) ∘ fun a =>
        { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
      destruct y =
    ((fun x => corec (Functor.map destruct) x) ∘ destruct) <$> destruct y
Tactic:
rfl
Proof state after:
no goals
Theorem: QPF.M.construct_destruct
Proof state before:
case h₀.right
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ (fun x => (↑x).snd) <$>
      (fun a =>
          { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
        destruct y =
    destruct y
Tactic:
rw [←QPF.M.map_comp]
Proof state after:
case h₀.right
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ ((fun x => (↑x).snd) ∘ fun a =>
        { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
      destruct y =
    destruct y
Theorem: QPF.M.construct_destruct
Proof state before:
case h₀.right
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ ((fun x => (↑x).snd) ∘ fun a =>
        { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
      destruct y =
    destruct y
Tactic:
have : inst.map id (destruct y) = destruct y := by rw [QPF.map_id]
Proof state after:
case h₀.right
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
this : id <$> destruct y = destruct y
⊢ ((fun x => (↑x).snd) ∘ fun a =>
        { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
      destruct y =
    destruct y
Theorem: QPF.M.construct_destruct
Proof state before:
case h₀.right
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
this : id <$> destruct y = destruct y
⊢ ((fun x => (↑x).snd) ∘ fun a =>
        { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
      destruct y =
    destruct y
Tactic:
apply Eq.trans _ this
Proof state after:
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
this : id <$> destruct y = destruct y
⊢ ((fun x => (↑x).snd) ∘ fun a =>
        { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
      destruct y =
    id <$> destruct y
Theorem: QPF.M.construct_destruct
Proof state before:
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
this : id <$> destruct y = destruct y
⊢ ((fun x => (↑x).snd) ∘ fun a =>
        { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
      destruct y =
    id <$> destruct y
Tactic:
apply congrFun
Proof state after:
case h
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
this : id <$> destruct y = destruct y
⊢ Functor.map
      ((fun x => (↑x).snd) ∘ fun a =>
        { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) =
    Functor.map id
Theorem: QPF.M.construct_destruct
Proof state before:
case h
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
this : id <$> destruct y = destruct y
⊢ Functor.map
      ((fun x => (↑x).snd) ∘ fun a =>
        { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) =
    Functor.map id
Tactic:
funext _
Proof state after:
case h.h
F : Type u₁ → Type u₁
inst : QPF F
x✝¹ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
this : id <$> destruct y = destruct y
x✝ : F (M F)
⊢ ((fun x => (↑x).snd) ∘ fun a =>
        { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
      x✝ =
    id <$> x✝
Theorem: QPF.M.construct_destruct
Proof state before:
case h.h
F : Type u₁ → Type u₁
inst : QPF F
x✝¹ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
this : id <$> destruct y = destruct y
x✝ : F (M F)
⊢ ((fun x => (↑x).snd) ∘ fun a =>
        { val := (construct (destruct a), a), property := (_ : construct (destruct a) = construct (destruct a)) }) <$>
      x✝ =
    id <$> x✝
Tactic:
rfl
Proof state after:
no goals
Theorem: QPF.M.construct_destruct
Proof state before:
F : Type u₁ → Type u₁
inst : QPF F
x✝ : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
x y : M F
h₀✝ : R x y
h₀ : destruct x = (fun x => corec (Functor.map destruct) x) <$> destruct <$> destruct y
⊢ id <$> destruct y = destruct y
Tactic:
rw [QPF.map_id]
Proof state after:
no goals
Theorem: QPF.M.construct_destruct
Proof state before:
case a
F : Type u₁ → Type u₁
inst : QPF F
x : M F
R : M F → M F → Prop := fun x y => x = construct (destruct y)
⊢ R (construct (destruct x)) x
Tactic:
rfl
Proof state after:
no goals
Theorem: Container.M.destruct_corec
Proof state before:
C : Container
α : Type u₃
f : α → Obj C α
x₀ : α
⊢ destruct (corec f x₀) = Map (corec f) (f x₀)
Tactic:
simp only [corec, destruct]
Proof state after:
C : Container
α : Type u₃
f : α → Obj C α
x₀ : α
⊢ {
      fst :=
        node
          { approx := Approx.corec f x₀,
            agrees := (_ : ∀ (n : Nat), Agree (Approx.corec f x₀ n) (Approx.corec f x₀ (Nat.succ n))) },
      snd :=
        children
          { approx := Approx.corec f x₀,
            agrees := (_ : ∀ (n : Nat), Agree (Approx.corec f x₀ n) (Approx.corec f x₀ (Nat.succ n))) } } =
    Map
      (fun x₀ =>
        { approx := Approx.corec f x₀,
          agrees := (_ : ∀ (n : Nat), Agree (Approx.corec f x₀ n) (Approx.corec f x₀ (Nat.succ n))) })
      (f x₀)
Theorem: Container.M.destruct_corec
Proof state before:
C : Container
α : Type u₃
f : α → Obj C α
x₀ : α
⊢ {
      fst :=
        node
          { approx := Approx.corec f x₀,
            agrees := (_ : ∀ (n : Nat), Agree (Approx.corec f x₀ n) (Approx.corec f x₀ (Nat.succ n))) },
      snd :=
        children
          { approx := Approx.corec f x₀,
            agrees := (_ : ∀ (n : Nat), Agree (Approx.corec f x₀ n) (Approx.corec f x₀ (Nat.succ n))) } } =
    Map
      (fun x₀ =>
        { approx := Approx.corec f x₀,
          agrees := (_ : ∀ (n : Nat), Agree (Approx.corec f x₀ n) (Approx.corec f x₀ (Nat.succ n))) })
      (f x₀)
Tactic:
rfl
Proof state after:
no goals
Theorem: Container.Eq_from_Heq
Proof state before:
C : Container
α β : Sort u₁
i : α
j : β
h₀ : α = β
h : HEq i j
⊢ cast h₀ i = j
Tactic:
cases h
Proof state after:
case refl
C : Container
α : Sort u₁
i : α
h₀ : α = α
⊢ cast h₀ i = i
Theorem: Container.Eq_from_Heq
Proof state before:
case refl
C : Container
α : Sort u₁
i : α
h₀ : α = α
⊢ cast h₀ i = i
Tactic:
apply eq_of_heq
Proof state after:
case refl.h
C : Container
α : Sort u₁
i : α
h₀ : α = α
⊢ HEq (cast h₀ i) i
Theorem: Container.Eq_from_Heq
Proof state before:
case refl.h
C : Container
α : Sort u₁
i : α
h₀ : α = α
⊢ HEq (cast h₀ i) i
Tactic:
apply cast_heq
Proof state after:
no goals
Theorem: Container.M.bisim.lemma0
Proof state before:
C : Container
⊢ ∀ (x : M C) (n : Nat) (i : B C (Approx.node (approx x (Nat.succ n)))) (j : B C (destruct x).fst),
    HEq i j → Approx.children (approx x (Nat.succ n)) i = approx (PSigma.snd (destruct x) j) n
Tactic:
intro x n i j heq
Proof state after:
C : Container
x : M C
n : Nat
i : B C (Approx.node (approx x (Nat.succ n)))
j : B C (destruct x).fst
heq : HEq i j
⊢ Approx.children (approx x (Nat.succ n)) i = approx (PSigma.snd (destruct x) j) n
Theorem: Container.M.bisim.lemma0
Proof state before:
C : Container
x : M C
n : Nat
i : B C (Approx.node (approx x (Nat.succ n)))
j : B C (destruct x).fst
heq : HEq i j
⊢ Approx.children (approx x (Nat.succ n)) i = approx (PSigma.snd (destruct x) j) n
Tactic:
have : i = cast (by rw [node_thm]; simp [destruct]) j := by
  have : C.B x.destruct.fst = C.B (x.approx (.succ n)).node := by rw [node_thm]; simp [destruct]
  rw [Eq_from_Heq j i]
  apply HEq.symm
  assumption
Proof state after:
C : Container
x : M C
n : Nat
i : B C (Approx.node (approx x (Nat.succ n)))
j : B C (destruct x).fst
heq : HEq i j
this : i = cast (_ : B C (destruct x).fst = B C (Approx.node (approx x (Nat.succ n)))) j
⊢ Approx.children (approx x (Nat.succ n)) i = approx (PSigma.snd (destruct x) j) n
Theorem: Container.M.bisim.lemma0
Proof state before:
C : Container
x : M C
n : Nat
i : B C (Approx.node (approx x (Nat.succ n)))
j : B C (destruct x).fst
heq : HEq i j
this : i = cast (_ : B C (destruct x).fst = B C (Approx.node (approx x (Nat.succ n)))) j
⊢ Approx.children (approx x (Nat.succ n)) i = approx (PSigma.snd (destruct x) j) n
Tactic:
simp only [this, children, Approx.node, destruct]
Proof state after:
no goals
Theorem: Container.M.bisim.lemma0
Proof state before:
C : Container
x : M C
n : Nat
i : B C (Approx.node (approx x (Nat.succ n)))
j : B C (destruct x).fst
heq : HEq i j
⊢ B C (destruct x).fst = B C (Approx.node (approx x (Nat.succ n)))
Tactic:
rw [node_thm]
Proof state after:
C : Container
x : M C
n : Nat
i : B C (Approx.node (approx x (Nat.succ n)))
j : B C (destruct x).fst
heq : HEq i j
⊢ B C (destruct x).fst = B C (node x)
Theorem: Container.M.bisim.lemma0
Proof state before:
C : Container
x : M C
n : Nat
i : B C (Approx.node (approx x (Nat.succ n)))
j : B C (destruct x).fst
heq : HEq i j
⊢ B C (destruct x).fst = B C (node x)
Tactic:
simp [destruct]
Proof state after:
no goals
Theorem: Container.M.bisim.lemma0
Proof state before:
C : Container
x : M C
n : Nat
i : B C (Approx.node (approx x (Nat.succ n)))
j : B C (destruct x).fst
heq : HEq i j
⊢ i = cast (_ : B C (destruct x).fst = B C (Approx.node (approx x (Nat.succ n)))) j
Tactic:
have : C.B x.destruct.fst = C.B (x.approx (.succ n)).node := by rw [node_thm]; simp [destruct]
Proof state after:
C : Container
x : M C
n : Nat
i : B C (Approx.node (approx x (Nat.succ n)))
j : B C (destruct x).fst
heq : HEq i j
this : B C (destruct x).fst = B C (Approx.node (approx x (Nat.succ n)))
⊢ i = cast (_ : B C (destruct x).fst = B C (Approx.node (approx x (Nat.succ n)))) j
Theorem: Container.M.bisim.lemma0
Proof state before:
C : Container
x : M C
n : Nat
i : B C (Approx.node (approx x (Nat.succ n)))
j : B C (destruct x).fst
heq : HEq i j
this : B C (destruct x).fst = B C (Approx.node (approx x (Nat.succ n)))
⊢ i = cast (_ : B C (destruct x).fst = B C (Approx.node (approx x (Nat.succ n)))) j
Tactic:
rw [Eq_from_Heq j i]
Proof state after:
case h
C : Container
x : M C
n : Nat
i : B C (Approx.node (approx x (Nat.succ n)))
j : B C (destruct x).fst
heq : HEq i j
this : B C (destruct x).fst = B C (Approx.node (approx x (Nat.succ n)))
⊢ HEq j i
Theorem: Container.M.bisim.lemma0
Proof state before:
case h
C : Container
x : M C
n : Nat
i : B C (Approx.node (approx x (Nat.succ n)))
j : B C (destruct x).fst
heq : HEq i j
this : B C (destruct x).fst = B C (Approx.node (approx x (Nat.succ n)))
⊢ HEq j i
Tactic:
apply HEq.symm
Proof state after:
case h.h
C : Container
x : M C
n : Nat
i : B C (Approx.node (approx x (Nat.succ n)))
j : B C (destruct x).fst
heq : HEq i j
this : B C (destruct x).fst = B C (Approx.node (approx x (Nat.succ n)))
⊢ HEq i j
Theorem: Container.M.bisim.lemma0
Proof state before:
case h.h
C : Container
x : M C
n : Nat
i : B C (Approx.node (approx x (Nat.succ n)))
j : B C (destruct x).fst
heq : HEq i j
this : B C (destruct x).fst = B C (Approx.node (approx x (Nat.succ n)))
⊢ HEq i j
Tactic:
assumption
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)
⊢ ∀ (x y : M C) (n : Nat), R x y → approx x n = approx y n
Tactic:
intro x y n 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
n : Nat
h₁ : R x y
⊢ approx x n = approx y n