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