How Si Yu

2018-03-04 06:37:24 UTC

Permalink

Hi, all. given a well-founded relation _<_ on A, define _≪_ on List ARaw Message

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