[Agda] Bezonas helpon !

[Serge Leblanc]

Dear, I succeeded completing the proof1: ∀ xs → All (_≥_ (max "xs))
(toList xs)" using "tabulate". Can anyone show me a simple method?

Sincerely thank you,

Estimata, mi sukcesis plenumi pruvon "proof₁′ : ∀ xs → All (_≥_ (max″
xs)) (toList xs)" per uzado de 'tabulate'. Ĉu ekzistas pli simpla metodo ?

Sinceran dankon,

proof₁′ : ∀ xs → All (_≥_ (max″ xs)) (toList xs)
proof₁′ (h ∷ t) = tabulate helper  
  where
    helper′ : ∀ {x xs}  → x ∈ xs → (∀ x₀ → max″ (x₀ ∷ xs) ≥ x)
    helper′ {x} (here {x′} {xs′} px) x₀ = begin
      x ≤⟨ lemma₄ (x₀ ∷ xs′)  x ⟩
      Data.List.foldl _⊔_ (x ⊔ x₀) xs′ ≡⟨ cong (λ s → Data.List.foldl
_⊔_ s xs′) (⊔-comm x x₀) ⟩
      Data.List.foldl _⊔_ (x₀ ⊔ x) xs′ ≡⟨ cong (λ s → Data.List.foldl
_⊔_ (x₀ ⊔ s) xs′) px ⟩
      Data.List.foldl _⊔_ (x₀ ⊔ x′) xs′
      ∎
      where open Data.Nat.≤-Reasoning
    helper′ {x} (there {x′} {xs′} pxs) x₀ = helper′ pxs (x₀ ⊔ x′)

    helper : {x : ℕ} → x ∈ (h ∷ t) → max″ (h ∷ t) ≥ x
    helper {x} (here px) = begin
      x ≡⟨ px ⟩
      h ≤⟨ lemma₄ t h ⟩
      max″ (h ∷ t)
      ∎
      where open Data.Nat.≤-Reasoning
    helper {x} (there pxs) = (helper′ pxs h)

-- 
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/20170914/7b48a4e9/attachment.html>
-------------- next part --------------
module Maximal where

open import Data.Nat public using (ℕ; zero; suc; _⊔_; _≤_; _≥_; z≤n; s≤s)
open import Data.Nat.Properties public using (m≤m⊔n)
open import Data.List using (List; []; _∷_; _∷ʳ_; _++_)
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; cong; sym )



open import Relation.Binary
open DecTotalOrder Data.Nat.decTotalOrder using () renaming (refl to ≤-refl)

--open import Function using (id)


foldr : ∀ {a} {A : Set a} → (A → A → A) → List⁺ A → A
foldr {A = A} c (n ∷ l) = foldr′ n l
  where
    foldr′ : A → List A → A
    foldr′ n [] = n
    foldr′ n (x ∷ xs) = c n (foldr′ x xs)

foldl : ∀ {a} {A : Set a} → (A → A → A) → List⁺ A → A
foldl {A = A} c (n ∷ l) = foldl′ n l
  where
    foldl′ : A → List A → A
    foldl′ n [] = n
    foldl′ n (x ∷ xs) = foldl′ (c n x) xs

foldl″ : ∀ {a} {A : Set a} → (A → A → A) → List⁺ A → A
foldl″ f (h ∷ t) = Data.List.foldl f h t


max : List⁺ ℕ → ℕ
max l = foldl _⊔_ l

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

max″ : List⁺ ℕ → ℕ
max″ (h ∷ t) = Data.List.foldl _⊔_ h t

private

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

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

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

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

  module Examples (_⊙_ : ℕ → ℕ → ℕ)
                  (a b c : ℕ)
                  where

      left₁ : foldl _⊙_ (a ∷⁺ b ∷⁺ [ c ]) ≡ ((a ⊙ b) ⊙ c)
      left₁ = refl

      left₂ : foldl″ _⊙_ (a ∷⁺ b ∷⁺ [ c ]) ≡ ((a ⊙ b) ⊙ c)
      left₂ = refl

      right₁ : foldr _⊙_ (a ∷⁺ b ∷⁺ [ c ]) ≡ (a ⊙ (b ⊙ c))
      right₁ = refl


⊔-right-identity : ∀ n → n ⊔ 0 ≡ n
⊔-right-identity zero = refl
⊔-right-identity (suc n) = refl

⊔-comm : ∀ x y → x ⊔ y ≡ y ⊔ x
⊔-comm zero y = sym (⊔-right-identity y)
⊔-comm (suc x) zero = refl
⊔-comm (suc x) (suc y) = cong suc (⊔-comm x y)

⊔-asso : ∀ x y z → x ⊔ (y ⊔ z) ≡ (x ⊔ y) ⊔ z
⊔-asso zero _ _ = refl
⊔-asso (suc x) zero _ = refl
⊔-asso (suc x) (suc y) zero = refl
⊔-asso (suc x) (suc y) (suc z) = cong suc (⊔-asso x y z)

--open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl; cong; cong₂)
--open PropEq.≡-Reasoning -- renaming (_≡⟨_⟩_ to _≡[_]_)

private

  abstract
    lemma₂ : ∀ x₀ x₁ xs → Data.List.foldl _⊔_ x₀ (x₁ ∷ xs) ≡ Data.List.foldl _⊔_ (x₀ ⊔ x₁) xs
    lemma₂ x₀ x₁ xs = refl
 

lemma₃ : ∀ x₀ x₁ xs → x₀ ⊔ max″ (x₁ ∷ xs) ≡ max″ (x₀ ∷ x₁ ∷ xs)
lemma₃ x₀ x₁ [] = refl
lemma₃ x₀ x₁ (h ∷ t) = begin
  x₀ ⊔ Data.List.foldl _⊔_ (x₁ ⊔ h) t ≡⟨ lemma₃ x₀ (x₁ ⊔ h) t ⟩
  Data.List.foldl _⊔_ (x₀ ⊔ (x₁ ⊔ h)) t ≡⟨ cong (λ s → Data.List.foldl _⊔_ s t) (⊔-asso x₀ x₁ h) ⟩
  Data.List.foldl _⊔_ (x₀ ⊔ x₁ ⊔ h) t 
  ∎
  where open PropEq.≡-Reasoning

lemma₄ : ∀ xs x → max″ (x ∷ xs) ≥ x
lemma₄ [] x = ≤-refl
lemma₄ (x₁ ∷ xs) x = begin
  x ≤⟨ m≤m⊔n x (Data.List.foldl _⊔_ x₁ xs) ⟩
  x ⊔ Data.List.foldl _⊔_ x₁ xs ≡⟨ lemma₃ x x₁ xs ⟩
  Data.List.foldl _⊔_ (x ⊔ x₁) xs
  ∎
  where open Data.Nat.≤-Reasoning


lemma₅ : ∀ xs x → max″ (x ∷⁺ xs) ≥ max″ xs
lemma₅ (h ∷ t) x = begin
  Data.List.foldl _⊔_ h t ≤⟨ m≤m⊔n (Data.List.foldl _⊔_ h t) x ⟩
  Data.List.foldl _⊔_ h t ⊔ x ≡⟨ ⊔-comm (Data.List.foldl _⊔_ h t) x ⟩
  x ⊔ Data.List.foldl _⊔_ h t ≡⟨ lemma₃ x h t ⟩
  Data.List.foldl _⊔_ (x ⊔ h) t
  ∎
  where open Data.Nat.≤-Reasoning

lemma₆ : ∀ xs x₁ x → max″ (x ∷ x₁ ∷ xs) ≥ x₁
lemma₆ xs x₁ x = begin
  x₁ ≤⟨ lemma₄ (x ∷ xs) x₁ ⟩
  Data.List.foldl _⊔_ (x₁ ⊔ x) xs ≡⟨ cong (λ s → Data.List.foldl _⊔_ s xs) (⊔-comm x₁ x) ⟩
  Data.List.foldl _⊔_ (x ⊔ x₁) xs
  ∎
  where open Data.Nat.≤-Reasoning

lemma₆′ : ∀ xs x x₀ → max″ (x ∷ x₀ ∷ xs) ≥ max″ (x ∷ xs)
lemma₆′ xs x x₀ = begin
  Data.List.foldl _⊔_ x xs ≤⟨ lemma₅ (x ∷ xs) x₀ ⟩
  Data.List.foldl _⊔_ (x₀ ⊔ x) xs ≡⟨ cong (λ s → Data.List.foldl _⊔_ s xs) (⊔-comm x₀ x) ⟩
  Data.List.foldl _⊔_ (x ⊔ x₀) xs
  ∎
  where open Data.Nat.≤-Reasoning


right-identity : ∀ {a} {A : Set a} (xs : List A) → xs ++ [] ≡ xs
right-identity [] = refl
right-identity (x ∷ xs) = cong (_∷_ x) (right-identity xs)

lemma₇ : ∀ xs₀ xs₁ → max″ (xs₀ ++⁺ xs₁) ≥ max″ xs₁
lemma₇ [] xs₁ = ≤-refl
lemma₇ (x₀ ∷ xs₀) xs₁ = begin
  max″ xs₁ ≤⟨ lemma₇ xs₀ xs₁ ⟩
  max″ (xs₀ ++⁺ xs₁) ≤⟨ lemma₅ (xs₀ ++⁺ xs₁) x₀ ⟩
  max″ (x₀ ∷⁺ xs₀ ++⁺ xs₁)
  ∎
  where open Data.Nat.≤-Reasoning


≤-trans : ∀ {i j k} → i ≤ j → j ≤ k → i ≤ k
≤-trans z≤n _ = z≤n
≤-trans (s≤s i≤j) (s≤s j≤k) = s≤s (≤-trans i≤j j≤k )

lemma₈ : ∀ xs₀ xs x → max″ (xs₀ ++⁺ x ∷ xs) ≥ x
lemma₈ xs₀ xs x = ≤-trans (lemma₄ xs x) (lemma₇ xs₀ (x ∷ xs))

open Any.Membership-≡

proof₁′ : ∀ xs → All (_≥_ (max″ xs)) (toList xs)
proof₁′ (h ∷ t) = tabulate helper   
  where
    helper′ : ∀ {x xs}  → x ∈ xs → (∀ x₀ → max″ (x₀ ∷ xs) ≥ x) 
    helper′ {x} (here {x′} {xs′} px) x₀ = begin
      x ≤⟨ lemma₄ (x₀ ∷ xs′)  x ⟩
      Data.List.foldl _⊔_ (x ⊔ x₀) xs′ ≡⟨ cong (λ s → Data.List.foldl _⊔_ s xs′) (⊔-comm x x₀) ⟩
      Data.List.foldl _⊔_ (x₀ ⊔ x) xs′ ≡⟨ cong (λ s → Data.List.foldl _⊔_ (x₀ ⊔ s) xs′) px ⟩
      Data.List.foldl _⊔_ (x₀ ⊔ x′) xs′
      ∎
      where open Data.Nat.≤-Reasoning
    helper′ {x} (there {x′} {xs′} pxs) x₀ = helper′ pxs (x₀ ⊔ x′)

    helper : {x : ℕ} → x ∈ (h ∷ t) → max″ (h ∷ t) ≥ x
    helper {x} (here px) = begin
      x ≡⟨ px ⟩
      h ≤⟨ lemma₄ t h ⟩
      max″ (h ∷ t)
      ∎
      where open Data.Nat.≤-Reasoning
    helper {x} (there pxs) = (helper′ pxs h)

proof₁ : (xs : List⁺ ℕ) → All (_≥_ (max″ xs)) (toList xs)
proof₁ (x ∷ []) = {! lemma₄ [] x ∷ []!}
proof₁ (x ∷ x₁ ∷ xs₁) = {! proof₁ (x  ∷ xs₁) !}
-------------- 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/20170914/7b48a4e9/attachment.sig>