Discussion:
Well-foundedness of list of well-founded elements
(too old to reply)
How Si Yu
2018-03-04 06:37:24 UTC
Permalink
Raw Message
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
Ulf Norell
2018-03-04 08:45:59 UTC
Permalink
Raw Message
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
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
https://lists.chalmers.se/mailman/listinfo/agda
How Si Yu
2018-03-04 13:11:56 UTC
Permalink
Raw Message
Yes, I don't know why I make such a typo.
I think there's something wrong with your definition of _≪_. It doesn't
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
Post by How Si Yu
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
https://lists.chalmers.se/mailman/listinfo/agda
Loading...