прекращение изабеллы с расстоянием действительных чисел

Question

Возможно, кто-то может помочь мне с доказательством окончания в Изабель. Я пытаюсь построить из списка A новый под-список B. Для построения B я читаю снова и снова о целом A. Вынимайте элементы и используйте результат для поиска следующего элемента. Я привел простой пример, чтобы проиллюстрировать это:

приведен список случайных действительных чисел. И мы говорим, что ряд P находится в списке, если элемент из списка выше, чем P.

definition pointOnList :: "real list ⇒ real ⇒ bool" where 
    "pointOnList L P ≡ ∃ i. i < length L ∧ P < L!i" 

создать функцию, которая всегда взять следующий больший элемент.

fun nextPoint :: "real list ⇒ real ⇒ real" where 
    "nextPoint (X#Ls) P = (if (X > P) 
    then (X) 
    else (nextPoint Ls P))" 

И теперь я пытаюсь создать новый отсортированный неполный список по вынимают следующий больший элемент, чем P, но меньше, чем Q с nextPoint и продолжением с этим.

function listBetween :: "real list ⇒ real ⇒ real ⇒ real list" where 
    "pointOnList L P ⟹ pointOnList L Q ⟹ listBetween L P Q = (if(P ≤ Q) 
    then(P # (listBetween L (nextPoint L P) Q)) 
    else([]))" 

я уже продемонстрировал nextPoint всегда возвращает все большее число:

lemma foo: "pointOnList P A ⟹ A < (nextPoint P A)" 

прекращение доказательства с relation "measure (size o fst o snd)“ не работает для действительных чисел ... и теперь я не знаю, как продолжить.

Answer 1

Чтобы показать завершение в Изабель, вы должны показать, что рекурсивные вызовы следуют обоснованному соотношению. Самый простой способ сделать это - дать меру завершения, возвращающую натуральное число, которое становится меньше при каждом вызове. Это не работает с реальными числами, потому что они не имеют оснований - у вас может быть что-то вроде 1 → 1/2 → 1/4 → 1/8 → ...

В качестве меры прекращения действия в вашем случае будет указано количество которые соответствуют условию, то есть length (filter (λx. P ≤ x ∧ x ≤ Q)) l. Однако обратите внимание, что ваше определение не работает, если Q больше всех чисел в списке.

Ваше определение несколько трудоемкое и сложное.Я рекомендую следующее определение:

listBetween L P Q = sort (filter (λx. P ≤ x ∧ x ≤ Q) L) 

или, что то же самое,

listBetween L P Q = sort [x ← L. x ∈ {P..Q}] 

Заметим, однако, что это определение не выбрасывайте несколько экземпляров одного и того же числа, т.е. listBetween L 0 10 [2,1,2] = [1,2,2]. Если вы хотите выбросить их, вы можете использовать remdups.

Также обратите внимание, что что-то вроде pointOnList L P ≡ ∃ i. i < length L ∧ P < L!i в значительной степени никогда не то, что вы хотите - здесь нет необходимости работать с явными индексами. Просто сделайте ∃x∈set L. P < x.

Answer 2

Расторжение аргумент relation "measure (size o fst o snd)" не работает по нескольким причинам:

• С вашей леммы foo вы только доказали, что при увеличении значения. Но для прекращения вам нужна уменьшающаяся мера. Таким образом, вы можете захотеть использовать разницу

  relation "measure (λ (L,P,Q). Q - P)" 
  

• Даже тогда возникает проблема, что measure ожидает отображение в естественных чисел и Q - P вещественное число, так что это не работает. Раньше вы использовали size, но в вашей леме foo ничего не говорится о соединении между size и <. Более того, < не является обоснованным порядком над действительными числами.

• В конце концов, я хотел бы попытаться избежать рассуждений на реалов в этом простом примере на все и взять в качестве меры что-то вроде

  measure (λ (L,P,Q). length [ A . A <- L, P < A])" 
  

  и адаптировать заявление foo соответственно.