internlm/Lean-Github huggingface dataset:
Theorem: Free.by_cases
Proof state before:
case Free
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
f : F (Free F R)
⊢ motive (construct (FreeF.Free f))
Tactic:
exact free f
Proof state after:
no goals
Theorem: Free.destruct_pure
Proof state before:
F : Type u → Type u
inst : QPF F
R : Type u
r : R
⊢ destruct (pure r) = FreeF.Pure r
Tactic:
simp [pure, destruct_construct]
Proof state after:
no goals
Theorem: Free.destruct_free
Proof state before:
F : Type u → Type u
inst : QPF F
R : Type u
f : F (Free F R)
⊢ destruct (free f) = FreeF.Free f
Tactic:
simp [free, destruct_construct]
Proof state after:
no goals
Theorem: Free.bind_inr.internal
Proof state before:
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
⊢ ∀ (x y : Free F S), corec (bind.automaton k) (Sum.inr x) = y → x = y
Tactic:
apply QPF.M.bisim (λ x y => corec (bind.automaton k) (.inr x) = y)
Proof state after:
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
⊢ ∀ (x y : QPF.M (FreeF F S)),
    corec (bind.automaton k) (Sum.inr x) = y →
      QPF.M.liftr (FreeF F S) (fun x y => corec (bind.automaton k) (Sum.inr x) = y) (QPF.M.destruct x)
        (QPF.M.destruct y)
Theorem: Free.bind_inr.internal
Proof state before:
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
⊢ ∀ (x y : QPF.M (FreeF F S)),
    corec (bind.automaton k) (Sum.inr x) = y →
      QPF.M.liftr (FreeF F S) (fun x y => corec (bind.automaton k) (Sum.inr x) = y) (QPF.M.destruct x)
        (QPF.M.destruct y)
Tactic:
. intro x y h₁
  induction h₁
  rw [corec, QPF.M.destruct_corec]
  conv =>
    congr
    . skip
    . skip
    . rhs
      simp only [bind.automaton]
  exists (λ x => ⟨⟨x, corec (bind.automaton k) (.inr x)⟩, by rfl⟩) <$> destruct x
  rw [destruct]
  constructor
  . simp only [←QPF.map_comp, Function.comp]
    apply Eq.trans _ (QPF.map_id _)
    rfl
  . simp only [←QPF.map_comp, Function.comp]
    rfl
Proof state after:
no goals
Theorem: Free.bind_inr.internal
Proof state before:
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
⊢ ∀ (x y : QPF.M (FreeF F S)),
    corec (bind.automaton k) (Sum.inr x) = y →
      QPF.M.liftr (FreeF F S) (fun x y => corec (bind.automaton k) (Sum.inr x) = y) (QPF.M.destruct x)
        (QPF.M.destruct y)
Tactic:
intro x y h₁
Proof state after:
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
h₁ : corec (bind.automaton k) (Sum.inr x) = y
⊢ QPF.M.liftr (FreeF F S) (fun x y => corec (bind.automaton k) (Sum.inr x) = y) (QPF.M.destruct x) (QPF.M.destruct y)
Theorem: Free.bind_inr.internal
Proof state before:
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
h₁ : corec (bind.automaton k) (Sum.inr x) = y
⊢ QPF.M.liftr (FreeF F S) (fun x y => corec (bind.automaton k) (Sum.inr x) = y) (QPF.M.destruct x) (QPF.M.destruct y)
Tactic:
induction h₁
Proof state after:
case refl
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ QPF.M.liftr (FreeF F S) (fun x y => corec (bind.automaton k) (Sum.inr x) = y) (QPF.M.destruct x)
    (QPF.M.destruct (corec (bind.automaton k) (Sum.inr x)))
Theorem: Free.bind_inr.internal
Proof state before:
case refl
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ QPF.M.liftr (FreeF F S) (fun x y => corec (bind.automaton k) (Sum.inr x) = y) (QPF.M.destruct x)
    (QPF.M.destruct (corec (bind.automaton k) (Sum.inr x)))
Tactic:
rw [corec, QPF.M.destruct_corec]
Proof state after:
case refl
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ QPF.M.liftr (FreeF F S) (fun x y => QPF.M.corec (bind.automaton k) (Sum.inr x) = y) (QPF.M.destruct x)
    ((fun x => QPF.M.corec (bind.automaton k) x) <$> bind.automaton k (Sum.inr x))
Theorem: Free.bind_inr.internal
Proof state before:
case refl
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ QPF.M.liftr (FreeF F S) (fun x y => QPF.M.corec (bind.automaton k) (Sum.inr x) = y) (QPF.M.destruct x)
    ((fun x => QPF.M.corec (bind.automaton k) x) <$> bind.automaton k (Sum.inr x))
Tactic:
conv =>
  congr
  . skip
  . skip
  . rhs
    simp only [bind.automaton]
Proof state after:
case refl
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ QPF.M.liftr (FreeF F S) (fun x y => QPF.M.corec (bind.automaton k) (Sum.inr x) = y) (QPF.M.destruct x)
    ((fun x => QPF.M.corec (bind.automaton k) x) <$> Sum.inr <$> destruct x)
Theorem: Free.bind_inr.internal
Proof state before:
case refl
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ QPF.M.liftr (FreeF F S) (fun x y => QPF.M.corec (bind.automaton k) (Sum.inr x) = y) (QPF.M.destruct x)
    ((fun x => QPF.M.corec (bind.automaton k) x) <$> Sum.inr <$> destruct x)
Tactic:
exists (λ x => ⟨⟨x, corec (bind.automaton k) (.inr x)⟩, by rfl⟩) <$> destruct x
Proof state after:
case refl
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => (↑x).fst) <$>
        (fun x =>
            { val := (x, corec (bind.automaton k) (Sum.inr x)),
              property :=
                (_ :
                  QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst) =
                    QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst)) }) <$>
          destruct x =
      QPF.M.destruct x ∧
    (fun x => (↑x).snd) <$>
        (fun x =>
            { val := (x, corec (bind.automaton k) (Sum.inr x)),
              property :=
                (_ :
                  QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst) =
                    QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst)) }) <$>
          destruct x =
      (fun x => QPF.M.corec (bind.automaton k) x) <$> Sum.inr <$> destruct x
Theorem: Free.bind_inr.internal
Proof state before:
case refl
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => (↑x).fst) <$>
        (fun x =>
            { val := (x, corec (bind.automaton k) (Sum.inr x)),
              property :=
                (_ :
                  QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst) =
                    QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst)) }) <$>
          destruct x =
      QPF.M.destruct x ∧
    (fun x => (↑x).snd) <$>
        (fun x =>
            { val := (x, corec (bind.automaton k) (Sum.inr x)),
              property :=
                (_ :
                  QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst) =
                    QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst)) }) <$>
          destruct x =
      (fun x => QPF.M.corec (bind.automaton k) x) <$> Sum.inr <$> destruct x
Tactic:
rw [destruct]
Proof state after:
case refl
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => (↑x).fst) <$>
        (fun x =>
            { val := (x, corec (bind.automaton k) (Sum.inr x)),
              property :=
                (_ :
                  QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst) =
                    QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst)) }) <$>
          QPF.M.destruct x =
      QPF.M.destruct x ∧
    (fun x => (↑x).snd) <$>
        (fun x =>
            { val := (x, corec (bind.automaton k) (Sum.inr x)),
              property :=
                (_ :
                  QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst) =
                    QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst)) }) <$>
          QPF.M.destruct x =
      (fun x => QPF.M.corec (bind.automaton k) x) <$> Sum.inr <$> QPF.M.destruct x
Theorem: Free.bind_inr.internal
Proof state before:
case refl
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => (↑x).fst) <$>
        (fun x =>
            { val := (x, corec (bind.automaton k) (Sum.inr x)),
              property :=
                (_ :
                  QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst) =
                    QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst)) }) <$>
          QPF.M.destruct x =
      QPF.M.destruct x ∧
    (fun x => (↑x).snd) <$>
        (fun x =>
            { val := (x, corec (bind.automaton k) (Sum.inr x)),
              property :=
                (_ :
                  QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst) =
                    QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst)) }) <$>
          QPF.M.destruct x =
      (fun x => QPF.M.corec (bind.automaton k) x) <$> Sum.inr <$> QPF.M.destruct x
Tactic:
constructor
Proof state after:
case refl.left
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => (↑x).fst) <$>
      (fun x =>
          { val := (x, corec (bind.automaton k) (Sum.inr x)),
            property :=
              (_ :
                QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst) =
                  QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst)) }) <$>
        QPF.M.destruct x =
    QPF.M.destruct x

case refl.right
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => (↑x).snd) <$>
      (fun x =>
          { val := (x, corec (bind.automaton k) (Sum.inr x)),
            property :=
              (_ :
                QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst) =
                  QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst)) }) <$>
        QPF.M.destruct x =
    (fun x => QPF.M.corec (bind.automaton k) x) <$> Sum.inr <$> QPF.M.destruct x
Theorem: Free.bind_inr.internal
Proof state before:
case refl.left
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => (↑x).fst) <$>
      (fun x =>
          { val := (x, corec (bind.automaton k) (Sum.inr x)),
            property :=
              (_ :
                QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst) =
                  QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst)) }) <$>
        QPF.M.destruct x =
    QPF.M.destruct x

case refl.right
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => (↑x).snd) <$>
      (fun x =>
          { val := (x, corec (bind.automaton k) (Sum.inr x)),
            property :=
              (_ :
                QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst) =
                  QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst)) }) <$>
        QPF.M.destruct x =
    (fun x => QPF.M.corec (bind.automaton k) x) <$> Sum.inr <$> QPF.M.destruct x
Tactic:
. simp only [←QPF.map_comp, Function.comp]
  apply Eq.trans _ (QPF.map_id _)
  rfl
Proof state after:
case refl.right
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => (↑x).snd) <$>
      (fun x =>
          { val := (x, corec (bind.automaton k) (Sum.inr x)),
            property :=
              (_ :
                QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst) =
                  QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst)) }) <$>
        QPF.M.destruct x =
    (fun x => QPF.M.corec (bind.automaton k) x) <$> Sum.inr <$> QPF.M.destruct x
Theorem: Free.bind_inr.internal
Proof state before:
case refl.right
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => (↑x).snd) <$>
      (fun x =>
          { val := (x, corec (bind.automaton k) (Sum.inr x)),
            property :=
              (_ :
                QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst) =
                  QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst)) }) <$>
        QPF.M.destruct x =
    (fun x => QPF.M.corec (bind.automaton k) x) <$> Sum.inr <$> QPF.M.destruct x
Tactic:
. simp only [←QPF.map_comp, Function.comp]
  rfl
Proof state after:
no goals
Theorem: Free.bind_inr.internal
Proof state before:
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x✝ y x : QPF.M (FreeF F S)
⊢ (fun x y => QPF.M.corec (bind.automaton k) (Sum.inr x) = y) (x, corec (bind.automaton k) (Sum.inr x)).fst
    (x, corec (bind.automaton k) (Sum.inr x)).snd
Tactic:
rfl
Proof state after:
no goals
Theorem: Free.bind_inr.internal
Proof state before:
case refl.left
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => (↑x).fst) <$>
      (fun x =>
          { val := (x, corec (bind.automaton k) (Sum.inr x)),
            property :=
              (_ :
                QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst) =
                  QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst)) }) <$>
        QPF.M.destruct x =
    QPF.M.destruct x
Tactic:
simp only [←QPF.map_comp, Function.comp]
Proof state after:
case refl.left
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => x) <$> QPF.M.destruct x = QPF.M.destruct x
Theorem: Free.bind_inr.internal
Proof state before:
case refl.left
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => x) <$> QPF.M.destruct x = QPF.M.destruct x
Tactic:
apply Eq.trans _ (QPF.map_id _)
Proof state after:
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => x) <$> QPF.M.destruct x = id <$> QPF.M.destruct x
Theorem: Free.bind_inr.internal
Proof state before:
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => x) <$> QPF.M.destruct x = id <$> QPF.M.destruct x
Tactic:
rfl
Proof state after:
no goals
Theorem: Free.bind_inr.internal
Proof state before:
case refl.right
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => (↑x).snd) <$>
      (fun x =>
          { val := (x, corec (bind.automaton k) (Sum.inr x)),
            property :=
              (_ :
                QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst) =
                  QPF.M.corec (bind.automaton k) (Sum.inr (x, corec (bind.automaton k) (Sum.inr x)).fst)) }) <$>
        QPF.M.destruct x =
    (fun x => QPF.M.corec (bind.automaton k) x) <$> Sum.inr <$> QPF.M.destruct x
Tactic:
simp only [←QPF.map_comp, Function.comp]
Proof state after:
case refl.right
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => corec (bind.automaton k) (Sum.inr x)) <$> QPF.M.destruct x =
    (fun x => QPF.M.corec (bind.automaton k) (Sum.inr x)) <$> QPF.M.destruct x
Theorem: Free.bind_inr.internal
Proof state before:
case refl.right
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x y : QPF.M (FreeF F S)
⊢ (fun x => corec (bind.automaton k) (Sum.inr x)) <$> QPF.M.destruct x =
    (fun x => QPF.M.corec (bind.automaton k) (Sum.inr x)) <$> QPF.M.destruct x
Tactic:
rfl
Proof state after:
no goals
Theorem: Free.bind_inr
Proof state before:
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
⊢ ∀ (x : Free F S), corec (bind.automaton k) (Sum.inr x) = x
Tactic:
intro x
Proof state after:
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x : Free F S
⊢ corec (bind.automaton k) (Sum.inr x) = x
Theorem: Free.bind_inr
Proof state before:
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x : Free F S
⊢ corec (bind.automaton k) (Sum.inr x) = x
Tactic:
have := Free.bind_inr.internal k x (corec (bind.automaton k) (.inr x)) (by rfl)
Proof state after:
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x : Free F S
this : x = corec (bind.automaton k) (Sum.inr x)
⊢ corec (bind.automaton k) (Sum.inr x) = x
Theorem: Free.bind_inr
Proof state before:
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x : Free F S
this : x = corec (bind.automaton k) (Sum.inr x)
⊢ corec (bind.automaton k) (Sum.inr x) = x
Tactic:
conv =>
  rhs
  rw [this]
Proof state after:
no goals
Theorem: Free.bind_inr
Proof state before:
F : Type u → Type u
inst : QPF F
R S : Type u
k : R → Free F S
x : Free F S
⊢ corec (bind.automaton k) (Sum.inr x) = corec (bind.automaton k) (Sum.inr x)
Tactic:
rfl
Proof state after:
no goals
Theorem: Free.pure_bind
Proof state before:
F : Type u → Type u
inst : QPF F
R S : Type u
x : R
k : R → Free F S
⊢ pure x >>= k = k x
Tactic:
simp only [pure, bind]
Proof state after:
F : Type u → Type u
inst : QPF F
R S : Type u
x : R
k : R → Free F S
⊢ corec (bind.automaton k) (Sum.inl (construct (FreeF.Pure x))) = k x
Theorem: Free.pure_bind
Proof state before:
F : Type u → Type u
inst : QPF F
R S : Type u
x : R
k : R → Free F S
⊢ corec (bind.automaton k) (Sum.inl (construct (FreeF.Pure x))) = k x
Tactic:
conv =>
  lhs
  rw [←construct_destruct (corec (bind.automaton k) (.inl (construct <| .Pure x)))]
  rw [destruct_corec]
  rhs
  rhs
  simp only [bind.automaton, destruct_construct]
Proof state after:
F : Type u → Type u
inst : QPF F
R S : Type u
x : R
k : R → Free F S
⊢ construct (corec (bind.automaton k) <$> Sum.inr <$> destruct (k x)) = k x
Theorem: Free.pure_bind
Proof state before:
F : Type u → Type u
inst : QPF F
R S : Type u
x : R
k : R → Free F S
⊢ construct (corec (bind.automaton k) <$> Sum.inr <$> destruct (k x)) = k x
Tactic:
simp only [←QPF.map_comp, Function.comp]
Proof state after:
F : Type u → Type u
inst : QPF F
R S : Type u
x : R
k : R → Free F S
⊢ construct ((fun x => corec (bind.automaton k) (Sum.inr x)) <$> destruct (k x)) = k x
Theorem: Free.pure_bind
Proof state before:
F : Type u → Type u
inst : QPF F
R S : Type u
x : R
k : R → Free F S
⊢ construct ((fun x => corec (bind.automaton k) (Sum.inr x)) <$> destruct (k x)) = k x
Tactic:
conv =>
  lhs
  congr
  lhs
  intro x
  rw [bind_inr]
Proof state after:
F : Type u → Type u
inst : QPF F
R S : Type u
x : R
k : R → Free F S
⊢ construct ((fun x => x) <$> destruct (k x)) = k x
Theorem: Free.pure_bind
Proof state before:
F : Type u → Type u
inst : QPF F
R S : Type u
x : R
k : R → Free F S
⊢ construct ((fun x => x) <$> destruct (k x)) = k x
Tactic:
have := QPF.map_id (destruct (k x))
Proof state after:
F : Type u → Type u
inst : QPF F
R S : Type u
x : R
k : R → Free F S
this : id <$> destruct (k x) = destruct (k x)
⊢ construct ((fun x => x) <$> destruct (k x)) = k x
Theorem: Free.pure_bind
Proof state before:
F : Type u → Type u
inst : QPF F
R S : Type u
x : R
k : R → Free F S
this : id <$> destruct (k x) = destruct (k x)
⊢ construct ((fun x => x) <$> destruct (k x)) = k x
Tactic:
simp only [id] at this
Proof state after:
F : Type u → Type u
inst : QPF F
R S : Type u
x : R
k : R → Free F S
this : (fun a => a) <$> destruct (k x) = destruct (k x)
⊢ construct ((fun x => x) <$> destruct (k x)) = k x
Theorem: Free.pure_bind
Proof state before:
F : Type u → Type u
inst : QPF F
R S : Type u
x : R
k : R → Free F S
this : (fun a => a) <$> destruct (k x) = destruct (k x)
⊢ construct ((fun x => x) <$> destruct (k x)) = k x
Tactic:
rw [this, construct_destruct]
Proof state after:
no goals
Theorem: Free.free_bind
Proof state before:
F : Type u → Type u
inst : QPF F
R S : Type u
f : F (Free F R)
k : R → Free F S
⊢ free f >>= k = free (flip bind k <$> f)
Tactic:
simp only [free, bind, flip]
Proof state after:
F : Type u → Type u
inst : QPF F
R S : Type u
f : F (Free F R)
k : R → Free F S
⊢ corec (bind.automaton k) (Sum.inl (construct (FreeF.Free f))) =
    construct (FreeF.Free ((fun a => corec (bind.automaton k) (Sum.inl a)) <$> f))
Theorem: Free.free_bind
Proof state before:
F : Type u → Type u
inst : QPF F
R S : Type u
f : F (Free F R)
k : R → Free F S
⊢ corec (bind.automaton k) (Sum.inl (construct (FreeF.Free f))) =
    construct (FreeF.Free ((fun a => corec (bind.automaton k) (Sum.inl a)) <$> f))
Tactic:
conv =>
  lhs
  rw [←construct_destruct (corec (bind.automaton k) (.inl (construct <| .Free f)))]
  rw [destruct_corec]
  rhs
  rhs
  simp only [bind.automaton, destruct_construct]
Proof state after:
F : Type u → Type u
inst : QPF F
R S : Type u
f : F (Free F R)
k : R → Free F S
⊢ construct (corec (bind.automaton k) <$> FreeF.Free (Sum.inl <$> f)) =
    construct (FreeF.Free ((fun a => corec (bind.automaton k) (Sum.inl a)) <$> f))
Theorem: Free.free_bind
Proof state before:
F : Type u → Type u
inst : QPF F
R S : Type u
f : F (Free F R)
k : R → Free F S
⊢ construct (corec (bind.automaton k) <$> FreeF.Free (Sum.inl <$> f)) =
    construct (FreeF.Free ((fun a => corec (bind.automaton k) (Sum.inl a)) <$> f))
Tactic:
apply congrArg
Proof state after:
case h
F : Type u → Type u
inst : QPF F
R S : Type u
f : F (Free F R)
k : R → Free F S
⊢ corec (bind.automaton k) <$> FreeF.Free (Sum.inl <$> f) =
    FreeF.Free ((fun a => corec (bind.automaton k) (Sum.inl a)) <$> f)
Theorem: Free.free_bind
Proof state before:
case h
F : Type u → Type u
inst : QPF F
R S : Type u
f : F (Free F R)
k : R → Free F S
⊢ corec (bind.automaton k) <$> FreeF.Free (Sum.inl <$> f) =
    FreeF.Free ((fun a => corec (bind.automaton k) (Sum.inl a)) <$> f)
Tactic:
simp only [Functor.map, ←QPF.map_comp, Function.comp]
Proof state after:
no goals
Theorem: Free.bind_pure.internal
Proof state before:
F : Type u → Type u
inst : QPF F
R : Type u
⊢ ∀ (x y : Free F R), x >>= pure = y → x = y
Tactic:
apply QPF.M.bisim
Proof state after:
case h₀
F : Type u → Type u
inst : QPF F
R : Type u
⊢ ∀ (x y : QPF.M (FreeF F R)),
    x >>= pure = y → QPF.M.liftr (FreeF F R) (fun x y => x >>= pure = y) (QPF.M.destruct x) (QPF.M.destruct y)
Theorem: Free.bind_pure.internal
Proof state before:
case h₀
F : Type u → Type u
inst : QPF F
R : Type u
⊢ ∀ (x y : QPF.M (FreeF F R)),
    x >>= pure = y → QPF.M.liftr (FreeF F R) (fun x y => x >>= pure = y) (QPF.M.destruct x) (QPF.M.destruct y)
Tactic:
intro x y h₁
Proof state after:
case h₀
F : Type u → Type u
inst : QPF F
R : Type u
x y : QPF.M (FreeF F R)
h₁ : x >>= pure = y
⊢ QPF.M.liftr (FreeF F R) (fun x y => x >>= pure = y) (QPF.M.destruct x) (QPF.M.destruct y)
Theorem: Free.bind_pure.internal
Proof state before:
case h₀
F : Type u → Type u
inst : QPF F
R : Type u
x y : QPF.M (FreeF F R)
h₁ : x >>= pure = y
⊢ QPF.M.liftr (FreeF F R) (fun x y => x >>= pure = y) (QPF.M.destruct x) (QPF.M.destruct y)
Tactic:
induction h₁
Proof state after:
case h₀.refl
F : Type u → Type u
inst : QPF F
R : Type u
x y : QPF.M (FreeF F R)
⊢ QPF.M.liftr (FreeF F R) (fun x y => x >>= pure = y) (QPF.M.destruct x) (QPF.M.destruct (x >>= pure))
Theorem: Free.bind_pure.internal
Proof state before:
case h₀.refl
F : Type u → Type u
inst : QPF F
R : Type u
x y : QPF.M (FreeF F R)
⊢ QPF.M.liftr (FreeF F R) (fun x y => x >>= pure = y) (QPF.M.destruct x) (QPF.M.destruct (x >>= pure))
Tactic:
exists (λ x => ⟨(x, bind x Free.Monad.pure), by rfl⟩) <$> destruct x
Proof state after:
case h₀.refl
F : Type u → Type u
inst : QPF F
R : Type u
x y : QPF.M (FreeF F R)
⊢ (fun x => (↑x).fst) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct x =
      QPF.M.destruct x ∧
    (fun x => (↑x).snd) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct x =
      QPF.M.destruct (x >>= pure)