internlm/Lean-Github huggingface dataset:
Theorem: QPF.M.congr.coinduction
Proof state before:
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
⊢ (∀ (x y : M (C F)), p x y → ↑(precongr F) p x y) → ∀ (x y : M (C F)), p x y → congr F x y
Tactic:
intro h₀ x y h₁
Proof state after:
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
⊢ congr F x y
Theorem: QPF.M.congr.coinduction
Proof state before:
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
⊢ congr F x y
Tactic:
simp only [congr, pcongr]
Proof state after:
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
⊢ ↑(pgfp (precongr F)) ⊥ x y
Theorem: QPF.M.congr.coinduction
Proof state before:
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
⊢ ↑(pgfp (precongr F)) ⊥ x y
Tactic:
have := (pgfp.coinduction (precongr F) p).2
Proof state after:
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ ↑(pgfp (precongr F)) ⊥ x y
Theorem: QPF.M.congr.coinduction
Proof state before:
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ ↑(pgfp (precongr F)) ⊥ x y
Tactic:
apply this
Proof state after:
case a
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p)

case a
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p x y
Theorem: QPF.M.congr.coinduction
Proof state before:
case a
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p)

case a
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p x y
Tactic:
have : p ≤ p ⊔ pgfp (precongr F) p := by
  simp
Proof state after:
case a
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
this✝ : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
this : p ≤ p ⊔ ↑(pgfp (precongr F)) p
⊢ p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p)

case a
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p x y
Theorem: QPF.M.congr.coinduction
Proof state before:
case a
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
this✝ : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
this : p ≤ p ⊔ ↑(pgfp (precongr F)) p
⊢ p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p)

case a
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p x y
Tactic:
have := (precongr F).2 this
Proof state after:
case a
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
this✝¹ : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
this✝ : p ≤ p ⊔ ↑(pgfp (precongr F)) p
this : ↑(precongr F) p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p)
⊢ p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p)

case a
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p x y
Theorem: QPF.M.congr.coinduction
Proof state before:
case a
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
this✝¹ : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
this✝ : p ≤ p ⊔ ↑(pgfp (precongr F)) p
this : ↑(precongr F) p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p)
⊢ p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p)

case a
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p x y
Tactic:
apply le_trans _ this
Proof state after:
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
this✝¹ : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
this✝ : p ≤ p ⊔ ↑(pgfp (precongr F)) p
this : ↑(precongr F) p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p)
⊢ p ≤ ↑(precongr F) p

case a
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p x y
Theorem: QPF.M.congr.coinduction
Proof state before:
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
this✝¹ : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
this✝ : p ≤ p ⊔ ↑(pgfp (precongr F)) p
this : ↑(precongr F) p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p)
⊢ p ≤ ↑(precongr F) p

case a
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p x y
Tactic:
apply h₀
Proof state after:
case a
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p x y
Theorem: QPF.M.congr.coinduction
Proof state before:
case a
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p x y
Tactic:
assumption
Proof state after:
no goals
Theorem: QPF.M.congr.coinduction
Proof state before:
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p ≤ p ⊔ ↑(pgfp (precongr F)) p
Tactic:
simp
Proof state after:
no goals
Theorem: QPF.M.destruct_corec
Proof state before:
F : Type u₁ → Type u₁
inst : QPF F
α : Type u₁
f : α → F α
x₀ : α
⊢ destruct (corec f x₀) = (fun x => corec f x) <$> f x₀
Tactic:
simp only [destruct, corec, destruct.f, Container.M.destruct_corec, inst.abs_map, inst.abs_repr]
Proof state after:
F : Type u₁ → Type u₁
inst : QPF F
α : Type u₁
f : α → F α
x₀ : α
⊢ (fun x => Quot.mk (congr F) x) <$> (Container.M.corec fun x => repr (f x)) <$> f x₀ =
    (fun x => Quot.mk (congr F) (Container.M.corec (fun x => repr (f x)) x)) <$> f x₀
Theorem: QPF.M.destruct_corec
Proof state before:
F : Type u₁ → Type u₁
inst : QPF F
α : Type u₁
f : α → F α
x₀ : α
⊢ (fun x => Quot.mk (congr F) x) <$> (Container.M.corec fun x => repr (f x)) <$> f x₀ =
    (fun x => Quot.mk (congr F) (Container.M.corec (fun x => repr (f x)) x)) <$> f x₀
Tactic:
rw [←inst.abs_repr (f x₀)]
Proof state after:
F : Type u₁ → Type u₁
inst : QPF F
α : Type u₁
f : α → F α
x₀ : α
⊢ (fun x => Quot.mk (congr F) x) <$> (Container.M.corec fun x => repr (f x)) <$> abs (repr (f x₀)) =
    (fun x => Quot.mk (congr F) (Container.M.corec (fun x => repr (f x)) x)) <$> abs (repr (f x₀))
Theorem: QPF.M.destruct_corec
Proof state before:
F : Type u₁ → Type u₁
inst : QPF F
α : Type u₁
f : α → F α
x₀ : α
⊢ (fun x => Quot.mk (congr F) x) <$> (Container.M.corec fun x => repr (f x)) <$> abs (repr (f x₀)) =
    (fun x => Quot.mk (congr F) (Container.M.corec (fun x => repr (f x)) x)) <$> abs (repr (f x₀))
Tactic:
cases repr (f x₀) with
| mk n k =>
  simp only [←inst.abs_map, Container.Map]
  rfl
Proof state after:
no goals
Theorem: QPF.M.destruct_corec
Proof state before:
case mk
F : Type u₁ → Type u₁
inst : QPF F
α : Type u₁
f : α → F α
x₀ : α
n : (C F).A
k : Container.B (C F) n → α
⊢ (fun x => Quot.mk (congr F) x) <$> (Container.M.corec fun x => repr (f x)) <$> abs { fst := n, snd := k } =
    (fun x => Quot.mk (congr F) (Container.M.corec (fun x => repr (f x)) x)) <$> abs { fst := n, snd := k }
Tactic:
simp only [←inst.abs_map, Container.Map]
Proof state after:
case mk
F : Type u₁ → Type u₁
inst : QPF F
α : Type u₁
f : α → F α
x₀ : α
n : (C F).A
k : Container.B (C F) n → α
⊢ abs { fst := n, snd := (fun x => Quot.mk (congr F) x) ∘ (Container.M.corec fun x => repr (f x)) ∘ k } =
    abs { fst := n, snd := (fun x => Quot.mk (congr F) (Container.M.corec (fun x => repr (f x)) x)) ∘ k }
Theorem: QPF.M.destruct_corec
Proof state before:
case mk
F : Type u₁ → Type u₁
inst : QPF F
α : Type u₁
f : α → F α
x₀ : α
n : (C F).A
k : Container.B (C F) n → α
⊢ abs { fst := n, snd := (fun x => Quot.mk (congr F) x) ∘ (Container.M.corec fun x => repr (f x)) ∘ k } =
    abs { fst := n, snd := (fun x => Quot.mk (congr F) (Container.M.corec (fun x => repr (f x)) x)) ∘ k }
Tactic:
rfl
Proof state after:
no goals
Theorem: QPF.M.map_comp
Proof state before:
F : Type u₁ → Type u₁
inst : QPF F
α β γ : Type u₁
f : β → γ
g : α → β
x : F α
⊢ (f ∘ g) <$> x = f <$> g <$> x
Tactic:
conv =>
  congr
  <;> rw [←inst.abs_repr x]
Proof state after:
F : Type u₁ → Type u₁
inst : QPF F
α β γ : Type u₁
f : β → γ
g : α → β
x : F α
⊢ (f ∘ g) <$> abs (repr x) = f <$> g <$> abs (repr x)
Theorem: QPF.M.map_comp
Proof state before:
F : Type u₁ → Type u₁
inst : QPF F
α β γ : Type u₁
f : β → γ
g : α → β
x : F α
⊢ (f ∘ g) <$> abs (repr x) = f <$> g <$> abs (repr x)
Tactic:
cases repr x
Proof state after:
case mk
F : Type u₁ → Type u₁
inst : QPF F
α β γ : Type u₁
f : β → γ
g : α → β
x : F α
fst✝ : (C F).A
snd✝ : Container.B (C F) fst✝ → α
⊢ (f ∘ g) <$> abs { fst := fst✝, snd := snd✝ } = f <$> g <$> abs { fst := fst✝, snd := snd✝ }
Theorem: QPF.M.map_comp
Proof state before:
case mk
F : Type u₁ → Type u₁
inst : QPF F
α β γ : Type u₁
f : β → γ
g : α → β
x : F α
fst✝ : (C F).A
snd✝ : Container.B (C F) fst✝ → α
⊢ (f ∘ g) <$> abs { fst := fst✝, snd := snd✝ } = f <$> g <$> abs { fst := fst✝, snd := snd✝ }
Tactic:
simp [←inst.abs_map, Container.Map]
Proof state after:
case mk
F : Type u₁ → Type u₁
inst : QPF F
α β γ : Type u₁
f : β → γ
g : α → β
x : F α
fst✝ : (C F).A
snd✝ : Container.B (C F) fst✝ → α
⊢ abs { fst := fst✝, snd := (f ∘ g) ∘ snd✝ } = abs { fst := fst✝, snd := f ∘ g ∘ snd✝ }
Theorem: QPF.M.map_comp
Proof state before:
case mk
F : Type u₁ → Type u₁
inst : QPF F
α β γ : Type u₁
f : β → γ
g : α → β
x : F α
fst✝ : (C F).A
snd✝ : Container.B (C F) fst✝ → α
⊢ abs { fst := fst✝, snd := (f ∘ g) ∘ snd✝ } = abs { fst := fst✝, snd := f ∘ g ∘ snd✝ }
Tactic:
rfl
Proof state after:
no goals
Theorem: Container.Map_spec
Proof state before:
F : Type u₁ → Type u₁
inst : QPF F
α β γ : Type u₁
f : β → γ
g : α → β
x : Obj (QPF.C F) α
⊢ Map (f ∘ g) x = Map f (Map g x)
Tactic:
cases x
Proof state after:
case mk
F : Type u₁ → Type u₁
inst : QPF F
α β γ : Type u₁
f : β → γ
g : α → β
fst✝ : (QPF.C F).A
snd✝ : B (QPF.C F) fst✝ → α
⊢ Map (f ∘ g) { fst := fst✝, snd := snd✝ } = Map f (Map g { fst := fst✝, snd := snd✝ })
Theorem: Container.Map_spec
Proof state before:
case mk
F : Type u₁ → Type u₁
inst : QPF F
α β γ : Type u₁
f : β → γ
g : α → β
fst✝ : (QPF.C F).A
snd✝ : B (QPF.C F) fst✝ → α
⊢ Map (f ∘ g) { fst := fst✝, snd := snd✝ } = Map f (Map g { fst := fst✝, snd := snd✝ })
Tactic:
simp [Map]
Proof state after:
case mk
F : Type u₁ → Type u₁
inst : QPF F
α β γ : Type u₁
f : β → γ
g : α → β
fst✝ : (QPF.C F).A
snd✝ : B (QPF.C F) fst✝ → α
⊢ (f ∘ g) ∘ snd✝ = f ∘ g ∘ snd✝
Theorem: Container.Map_spec
Proof state before:
case mk
F : Type u₁ → Type u₁
inst : QPF F
α β γ : Type u₁
f : β → γ
g : α → β
fst✝ : (QPF.C F).A
snd✝ : B (QPF.C F) fst✝ → α
⊢ (f ∘ g) ∘ snd✝ = f ∘ g ∘ snd✝
Tactic:
rfl
Proof state after:
no goals
Theorem: QPF.M.bisim_lemma
Proof state before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
⊢ ∀ (x y : M F), r x y → x = y
Tactic:
intro x
Proof state after:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x : M F
⊢ ∀ (y : M F), r x y → x = y
Theorem: QPF.M.bisim_lemma
Proof state before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x : M F
⊢ ∀ (y : M F), r x y → x = y
Tactic:
apply Quot.inductionOn (motive := _) x
Proof state after:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x : M F
⊢ ∀ (a : Container.M (C F)) (y : M F), r (Quot.mk (congr F) a) y → Quot.mk (congr F) a = y
Theorem: QPF.M.bisim_lemma
Proof state before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x : M F
⊢ ∀ (a : Container.M (C F)) (y : M F), r (Quot.mk (congr F) a) y → Quot.mk (congr F) a = y
Tactic:
clear x
Proof state after:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
⊢ ∀ (a : Container.M (C F)) (y : M F), r (Quot.mk (congr F) a) y → Quot.mk (congr F) a = y
Theorem: QPF.M.bisim_lemma
Proof state before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
⊢ ∀ (a : Container.M (C F)) (y : M F), r (Quot.mk (congr F) a) y → Quot.mk (congr F) a = y
Tactic:
intro x y
Proof state after:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x : Container.M (C F)
y : M F
⊢ r (Quot.mk (congr F) x) y → Quot.mk (congr F) x = y
Theorem: QPF.M.bisim_lemma
Proof state before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x : Container.M (C F)
y : M F
⊢ r (Quot.mk (congr F) x) y → Quot.mk (congr F) x = y
Tactic:
apply Quot.inductionOn (motive := _) y
Proof state after:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x : Container.M (C F)
y : M F
⊢ ∀ (a : Container.M (C F)), r (Quot.mk (congr F) x) (Quot.mk (congr F) a) → Quot.mk (congr F) x = Quot.mk (congr F) a
Theorem: QPF.M.bisim_lemma
Proof state before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x : Container.M (C F)
y : M F
⊢ ∀ (a : Container.M (C F)), r (Quot.mk (congr F) x) (Quot.mk (congr F) a) → Quot.mk (congr F) x = Quot.mk (congr F) a
Tactic:
clear y
Proof state after:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x : Container.M (C F)
⊢ ∀ (a : Container.M (C F)), r (Quot.mk (congr F) x) (Quot.mk (congr F) a) → Quot.mk (congr F) x = Quot.mk (congr F) a
Theorem: QPF.M.bisim_lemma
Proof state before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x : Container.M (C F)
⊢ ∀ (a : Container.M (C F)), r (Quot.mk (congr F) x) (Quot.mk (congr F) a) → Quot.mk (congr F) x = Quot.mk (congr F) a
Tactic:
intro y h₂
Proof state after:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x y : Container.M (C F)
h₂ : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ Quot.mk (congr F) x = Quot.mk (congr F) y
Theorem: QPF.M.bisim_lemma
Proof state before:
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x y : Container.M (C F)
h₂ : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ Quot.mk (congr F) x = Quot.mk (congr F) y
Tactic:
apply Quot.sound
Proof state after:
case a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x y : Container.M (C F)
h₂ : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ congr F x y
Theorem: QPF.M.bisim_lemma
Proof state before:
case a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x y : Container.M (C F)
h₂ : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ congr F x y
Tactic:
let r' x y := r (Quot.mk _ x) (Quot.mk _ y)
Proof state after:
case a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x y : Container.M (C F)
h₂ : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ congr F x y
Theorem: QPF.M.bisim_lemma
Proof state before:
case a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x y : Container.M (C F)
h₂ : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ congr F x y
Tactic:
apply congr.coinduction F r'
Proof state after:
case a.a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x y : Container.M (C F)
h₂ : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ ∀ (x y : Container.M (C F)), r' x y → ↑(precongr F) r' x y

case a.a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x y : Container.M (C F)
h₂ : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ r' x y
Theorem: QPF.M.bisim_lemma
Proof state before:
case a.a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x y : Container.M (C F)
h₂ : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ ∀ (x y : Container.M (C F)), r' x y → ↑(precongr F) r' x y

case a.a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x y : Container.M (C F)
h₂ : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ r' x y
Tactic:
. clear h₂
  intro x y h₂
  simp only [precongr, map_quot]
  have h₂ := h₁ _ _ h₂
  simp only [destruct, destruct.f] at h₂
  generalize Container.M.destruct x = x at *
  generalize Container.M.destruct y = y at *
  cases x with | mk nx kx =>
  cases y with | mk ny ky =>
  let f : Quot r → Quot r' :=
    by
      apply Quot.lift (Quot.lift (Quot.mk r') _) _
      . intro a b h₃
        apply Quot.sound
        simp only
        rw [Quot.sound h₃]
        apply h₀
      . intro x; apply Quot.inductionOn (motive := _) x; clear x
        intro x y; apply Quot.inductionOn (motive := _) y; clear y
        intro y h
        apply Quot.sound
        apply h
  have : f ∘ Quot.mk r ∘ Quot.mk (congr F) = Quot.mk r' := rfl
  conv =>
    congr
    . rhs
      lhs
      intro i
      rw [←this]
      rfl
    . rhs
      lhs
      intro i
      rw [←this]
  rw [Container.Map_spec, Container.Map_spec, Container.Map_spec, Container.Map_spec]
  rw [inst.abs_map, inst.abs_map, inst.abs_map, inst.abs_map, inst.abs_map, inst.abs_map, h₂]
Proof state after:
case a.a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x y : Container.M (C F)
h₂ : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ r' x y
Theorem: QPF.M.bisim_lemma
Proof state before:
case a.a
F : Type u₁ → Type u₁
inst : QPF F
r : M F → M F → Prop
h₀ : ∀ (x : M F), r x x
h₁ : ∀ (x y : M F), r x y → Quot.mk r <$> destruct x = Quot.mk r <$> destruct y
x y : Container.M (C F)
h₂ : r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
r' : Container.M (C F) → Container.M (C F) → Prop := fun x y => r (Quot.mk (congr F) x) (Quot.mk (congr F) y)
⊢ r' x y
Tactic:
. apply h₂
Proof state after:
no goals