律师在AGDA中的固定点定理

发布于 2025-02-01 03:57:35 字数 551 浏览 2 评论 0原文

surjective : {A : _} {B : _} → (A → B) → Set
surjective {B = B} f = (b : B) → ∃ λ a → f a ≡ b

fixedPoint : {A : _} → (A → A) -> Set
fixedPoint f = ∃ λ a → f a ≡ a

lawvere : {A : _} {B : _}
        → (ϕ : A → A → B) → (surjective ϕ) → (f : B → B) →
        fixedPoint f
lawvere = ?

有关如何处理涉及存在的类似证据的一般提示也将有所帮助。

原文

I was struggling to prove a more basic version of lawvere's fixed point theorem in agda. Precisely I am trying to figure out the proof for the bottom theorem.

surjective : {A : _} {B : _} → (A → B) → Set
surjective {B = B} f = (b : B) → ∃ λ a → f a ≡ b

fixedPoint : {A : _} → (A → A) -> Set
fixedPoint f = ∃ λ a → f a ≡ a

lawvere : {A : _} {B : _}
        → (ϕ : A → A → B) → (surjective ϕ) → (f : B → B) →
        fixedPoint f
lawvere = ?

General tips about how to approach similar proofs involving existentials would also be helpful.

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

乞讨 2025-02-08 03:57:35

我认为我的问题是犹豫不决地使用对AGDA中经常遇到麻烦的方程推理。我最终发现的解决方案是：

lawvere : {A : _} {B : _}
        → (ϕ : A → A → B) → (surjective ϕ) → (f : B → B) →
        fixedPoint f
lawvere {A} {B} ϕ surj f = ϕ p p , sym proof
  where
    q = λ a → f (ϕ a a)
    p = Σ.fst (surj q)
    proof =
      begin
        ϕ p p
      ≡⟨ (cong-app (Σ.snd (surj q)) p) ⟩
        q p
      ≡⟨ refl ⟩
        (λ a → f (ϕ a a)) p
      ≡⟨ refl ⟩
        f (ϕ p p)
      ∎

I think my problem was hesitancy to use equational reasoning which I often have trouble with in agda. The solution I eventually found was:

lawvere : {A : _} {B : _}
        → (ϕ : A → A → B) → (surjective ϕ) → (f : B → B) →
        fixedPoint f
lawvere {A} {B} ϕ surj f = ϕ p p , sym proof
  where
    q = λ a → f (ϕ a a)
    p = Σ.fst (surj q)
    proof =
      begin
        ϕ p p
      ≡⟨ (cong-app (Σ.snd (surj q)) p) ⟩
        q p
      ≡⟨ refl ⟩
        (λ a → f (ϕ a a)) p
      ≡⟨ refl ⟩
        f (ϕ p p)
      ∎

回复收藏 0 原文

~没有更多了~