[Agda] Bezonas helpon !

[Serge Leblanc]

Saluton, neniu bonvolas helpi min?

Hi, nobody wants to help me?


On 2017-08-06 18:23, Serge Leblanc wrote:
> Dear All,
> I need help to finish these lemmas.
> They have the same meaning, I am right?
> All helpers are welcome!
>
> Estimata ĉiuj,
> Mi bezonas helpon por daŭrigi ci-tiuj pruvojn!
> Ĉu ili havas je la saman signifon! Ĉu mi pravas?
> Ĉiuj helpantoj estas bonvenaj!
>
> Sincere.
> -- 
> Serge Leblanc
> ------------------------------------------------------------------------
> gpg --search-keys 0x67B17A3F
> Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F

-- 
Serge Leblanc
------------------------------------------------------------------------
gpg --search-keys 0x67B17A3F
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170814/bb5a487c/attachment.html>
-------------- next part --------------
module Maximal where

open import Data.Nat public using (ℕ; zero; suc; _⊔_; _≤_; _≥_; z≤n; s≤s)
open import Data.List.NonEmpty using (List⁺; foldr₁; _∷_;  _∷⁺_; [_]; toList)
open import Data.List.Any as Any using (Any; here; there)
open import Data.List.All as All -- using (All)

open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl)

max : List⁺ ℕ → ℕ
max l = foldr₁ _⊔_ l

private
  max² : max [ 2 ] ≡ 2
  max² = refl

  max⁵ : max (4 ∷⁺ 5 ∷⁺ [ 6 ]) ≡ 6
  max⁵ = refl

open import Data.List using (List; [])

proof₁ : (xs : List⁺ ℕ) → All (_≥_ (max xs)) (toList xs)
proof₁ (s ∷ []) = {!  !}
proof₁ (s ∷ l) = {!  !}

open Any.Membership-≡ using (_∈_)

proof₂ : (xs : List⁺ ℕ) → (∀ {x} → x ∈ (toList xs) → (_≥_ (max xs)) x)
proof₂ (s ∷ l) = {!  !}

{-
lookup : ∀ {a p} {A : Set a} {P : A → Set p} {xs : List A} →
         All P xs → (∀ {x : A} → x ∈ xs → P x)
tabulate : ∀ {a p} {A : Set a} {P : A → Set p} {xs} →
                    (∀ {x} → x ∈ xs → P x) → All P xs
-}

open import Function using (id ; _∘_)

iso₁ : ∀ {a p} {A : Set a} {P : A → Set p} {xs} → All P xs → All P xs
iso₁ = tabulate ∘ lookup

proof₀ : ∀ {a p} {A : Set a} {P : A → Set p} →  tabulate ∘ lookup ≡ id
proof₀ = {!   !}
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170814/bb5a487c/attachment.sig>