[Agda] Well-foundedness of list of well-founded elements

[How Si Yu]

Yes, I don't know why I make such a typo.

On 3/4/18, Ulf Norell <ulf.norell at gmail.com> wrote:
> I think there's something wrong with your definition of _≪_. It doesn't
> mention _<_, and it's clearly reflexive on non-empty lists:
>
> refl-≪ : ∀ xs → ∃ (λ x → x ∈ xs) → xs ≪ xs
> refl-≪ xs non-empty = non-empty , λ _ i → i
>
> Did you mean
>
> _≪_ : Rel (List A) lzero
> xs ≪ ys = ∃ (λ x → x ∈ ys) × (∀ x → x ∈ xs → ∃ (λ y → y ∈ ys × x < y))
>
> ?
>
> / Ulf
>
>
> On Sun, Mar 4, 2018 at 7:37 AM, How Si Yu <howseeu at gmail.com> wrote:
>
>> Hi, all. given a well-founded relation _<_ on A, define _≪_ on List A
>> where  where xs ≪ ys = ∃ (λ x → x ∈ ys) × (∀ x → x ∈ xs → x ∈ ys). Is
>> it true that _≪_ is well-founded?
>>
>> This is definitely true in classical logic since we can argue in the
>> following way: Assume not. Then there exists an infinite sequence ...
>> ≪ xs3 ≪ xs2 ≪ xs1 ≪ xs0. ∀ i, xs(n+1) ≪ xsn so ∃ x ∈ xsn. If n ≠ 0, ∃
>> y ∈ xs(n-1) st x < y. Continuiting moving rightwards we find a
>> strictly increasing sequence starting at x and ends in xs0. Hence
>> there must exist infinitely such sequences ending at xs0. Since xs0 is
>> finite, ∃ x0 ∈ xs0 where infinitely many such sequences ending at x0.
>> All such sequences besides one pass through xs1. Since xs1 is finite,
>> ∃ x1 ∈ xs1 where infinitely many such sequences pass through x1.
>> Continuing such construction we get an infinite descending chain in A.
>> But _<_ is well-founded. Contradiction.
>>
>> Is this true constructively as well? Thanks a lot! I need it in doing
>> induction in my proof in
>> Agda. Below are codes to make precise my question.
>>
>> open import Data.List.Base using (List; []; _∷_)
>> open import Relation.Binary.Core using (Rel)
>> open import Agda.Primitive using (lzero)
>> open import Induction.WellFounded using (Well-founded)
>> open import Data.Product using (∃; _×_; _,_)
>>
>> postulate A : Set
>> postulate _<_ : Rel A lzero
>>
>> data _∈_ (x : A) : List A → Set where
>>   here : ∀ {xs} → x ∈ (x ∷ xs)
>>   there : ∀ {y xs} → x ∈ xs → x ∈ (y ∷ xs)
>>
>> _≪_ : Rel (List A) lzero
>> xs ≪ ys = ∃ (λ x → x ∈ ys) × (∀ x → x ∈ xs → x ∈ ys)
>>
>> _≪_-wf : Well-founded _<_ → Well-founded _≪_
>> _≪_-wf = {!!}
>>
>> Regards,
>> Si Yu
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>