Theorem: Free.bind_pure.internal (CoInd/QPF/FreeMonads.lean)

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

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

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

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

State before:
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)
Tactic:
cases x using by_cases with
| pure r =>
  have : destruct (pure r) = .Pure r := by
    exact @destruct_construct F _ R (FreeF.Pure r)
  simp only [Functor.map, this, pure_bind r]
  constructor <;> rfl
| free f =>
  have : destruct (free f) = .Free f := by
    exact @destruct_construct F _ R (FreeF.Free f)
  simp only [Functor.map, this, free_bind, ←QPF.map_comp, Function.comp]
  constructor
  . conv =>
      rhs
      congr
      rw [←QPF.map_id f]
    rw [free, construct, QPF.M.destruct_construct]
    rfl
  . simp only [free, construct, QPF.M.destruct_construct]
    rfl
State after:
no goals

State before:
F : Type u → Type u
inst : QPF F
R : Type u
x✝ y x : QPF.M (FreeF F R)
⊢ (fun x y => x >>= pure = y) (x, x >>= pure).fst (x, x >>= pure).snd
Tactic:
rfl
State after:
no goals

State before:
case h₀.refl.pure
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
r : R
⊢ (fun x => (↑x).fst) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct (pure r) =
      QPF.M.destruct (pure r) ∧
    (fun x => (↑x).snd) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct (pure r) =
      QPF.M.destruct (pure r >>= pure)
Tactic:
have : destruct (pure r) = .Pure r := by
  exact @destruct_construct F _ R (FreeF.Pure r)
State after:
case h₀.refl.pure
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
r : R
this : destruct (pure r) = FreeF.Pure r
⊢ (fun x => (↑x).fst) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct (pure r) =
      QPF.M.destruct (pure r) ∧
    (fun x => (↑x).snd) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct (pure r) =
      QPF.M.destruct (pure r >>= pure)

State before:
case h₀.refl.pure
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
r : R
this : destruct (pure r) = FreeF.Pure r
⊢ (fun x => (↑x).fst) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct (pure r) =
      QPF.M.destruct (pure r) ∧
    (fun x => (↑x).snd) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct (pure r) =
      QPF.M.destruct (pure r >>= pure)
Tactic:
simp only [Functor.map, this, pure_bind r]
State after:
case h₀.refl.pure
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
r : R
this : destruct (pure r) = FreeF.Pure r
⊢ FreeF.Pure r = QPF.M.destruct (pure r) ∧ FreeF.Pure r = QPF.M.destruct (pure r)

State before:
case h₀.refl.pure
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
r : R
this : destruct (pure r) = FreeF.Pure r
⊢ FreeF.Pure r = QPF.M.destruct (pure r) ∧ FreeF.Pure r = QPF.M.destruct (pure r)
Tactic:
constructor <;> rfl
State after:
no goals

State before:
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
r : R
⊢ destruct (pure r) = FreeF.Pure r
Tactic:
exact @destruct_construct F _ R (FreeF.Pure r)
State after:
no goals

State before:
case h₀.refl.free
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
⊢ (fun x => (↑x).fst) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct (free f) =
      QPF.M.destruct (free f) ∧
    (fun x => (↑x).snd) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct (free f) =
      QPF.M.destruct (free f >>= pure)
Tactic:
have : destruct (free f) = .Free f := by
  exact @destruct_construct F _ R (FreeF.Free f)
State after:
case h₀.refl.free
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ (fun x => (↑x).fst) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct (free f) =
      QPF.M.destruct (free f) ∧
    (fun x => (↑x).snd) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct (free f) =
      QPF.M.destruct (free f >>= pure)

State before:
case h₀.refl.free
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ (fun x => (↑x).fst) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct (free f) =
      QPF.M.destruct (free f) ∧
    (fun x => (↑x).snd) <$>
        (fun x =>
            { val := (x, x >>= pure),
              property := (_ : (x, x >>= pure).fst >>= pure = (x, x >>= pure).fst >>= pure) }) <$>
          destruct (free f) =
      QPF.M.destruct (free f >>= pure)
Tactic:
simp only [Functor.map, this, free_bind, ←QPF.map_comp, Function.comp]
State after:
case h₀.refl.free
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x) <$> f) = QPF.M.destruct (free f) ∧
    FreeF.Free ((fun x => x >>= pure) <$> f) = QPF.M.destruct (free (flip bind pure <$> f))

State before:
case h₀.refl.free
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x) <$> f) = QPF.M.destruct (free f) ∧
    FreeF.Free ((fun x => x >>= pure) <$> f) = QPF.M.destruct (free (flip bind pure <$> f))
Tactic:
constructor
State after:
case h₀.refl.free.left
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x) <$> f) = QPF.M.destruct (free f)

case h₀.refl.free.right
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x >>= pure) <$> f) = QPF.M.destruct (free (flip bind pure <$> f))

State before:
case h₀.refl.free.left
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x) <$> f) = QPF.M.destruct (free f)

case h₀.refl.free.right
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x >>= pure) <$> f) = QPF.M.destruct (free (flip bind pure <$> f))
Tactic:
. conv =>
    rhs
    congr
    rw [←QPF.map_id f]
  rw [free, construct, QPF.M.destruct_construct]
  rfl
State after:
case h₀.refl.free.right
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x >>= pure) <$> f) = QPF.M.destruct (free (flip bind pure <$> f))

State before:
case h₀.refl.free.right
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x >>= pure) <$> f) = QPF.M.destruct (free (flip bind pure <$> f))
Tactic:
. simp only [free, construct, QPF.M.destruct_construct]
  rfl
State after:
no goals

State before:
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
⊢ destruct (free f) = FreeF.Free f
Tactic:
exact @destruct_construct F _ R (FreeF.Free f)
State after:
no goals

State before:
case h₀.refl.free.left
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x) <$> f) = QPF.M.destruct (free f)
Tactic:
conv =>
  rhs
  congr
  rw [←QPF.map_id f]
State after:
case h₀.refl.free.left
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x) <$> f) = QPF.M.destruct (free (id <$> f))

State before:
case h₀.refl.free.left
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x) <$> f) = QPF.M.destruct (free (id <$> f))
Tactic:
rw [free, construct, QPF.M.destruct_construct]
State after:
case h₀.refl.free.left
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x) <$> f) = FreeF.Free (id <$> f)

State before:
case h₀.refl.free.left
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x) <$> f) = FreeF.Free (id <$> f)
Tactic:
rfl
State after:
no goals

State before:
case h₀.refl.free.right
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x >>= pure) <$> f) = QPF.M.destruct (free (flip bind pure <$> f))
Tactic:
simp only [free, construct, QPF.M.destruct_construct]
State after:
case h₀.refl.free.right
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x >>= pure) <$> f) = FreeF.Free (flip bind pure <$> f)

State before:
case h₀.refl.free.right
F : Type u → Type u
inst : QPF F
R : Type u
y : QPF.M (FreeF F R)
f : F (Free F R)
this : destruct (free f) = FreeF.Free f
⊢ FreeF.Free ((fun x => x >>= pure) <$> f) = FreeF.Free (flip bind pure <$> f)
Tactic:
rfl
State after:
no goals