есть ли что-нибудь похожее на тактику simpl для Program Fixpoint s? В частности, как можно доказать следующее тривиальное утверждение? Program Fixpoint bla (n:nat) {measure n} := match n with | 0 => 0 | S n' => S (bla n') end. Lemma...

Какие бывают размерные типы в Агде? Я пытался прочитать статью о MiniAgda , но не смог продолжить по следующим причинам: Почему типы данных являются универсальными по размеру? Насколько мне известно, размер - это глубина дерева индукции....

Кажется, они служат схожим целям. Единственное отличие, которое я заметил до сих пор, заключается в том, что, хотя Program Fixpoint принимает составную меру, такую ​​как {measure (length l1 + length l2) } , Function , кажется, отвергает это и...

Скажем, у меня есть следующее Program Fixpoint : From Coq Require Import List Program. Import ListNotations. Program Fixpoint f l {measure (length l)}: list nat := let f_rec := (f (tl l) ) in match hd_error l with | Some n => n :: f_rec |...

Coq, в отличие от многих других, принимает необязательный явный параметр, который можно использовать для указания убывающей структуры определения фиксированной точки. Из спецификации Gallina, 1.3.4, Fixpoint ident params {struct ident0 } :...