Расширение рекурсивных функций в Coq

Фон

Я понимаю, что редукция Йота используется для уменьшения/расширения рекурсивных функций. Например, при следующем применении простой рекурсивной функции (факториал над натуральными числами):

((fix fact (n:nat):nat := match n with | O => 1 | S m => n * fact m end) 2)

Сокращение йоты расширяет рекурсивный вызов, эффективно повторяя рекурсивную функцию один раз:

Eval lazy iota in ((fix fact (n:nat):nat := match n with | O => 1 | S m => n * fact m end) 2).
 = (fun n:nat =>
    match n with
    | 0 => 1
    | S m =>
        n *
        (fix fact (m : nat) : nat :=
           match m with
           | 0 => 1
           | S m0 => m * fact m0
           end) m
    end) 2.

Это поведение хорошо обобщается на взаимно рекурсивные функции. Например, учитывая следующие определения взаимно рекурсивных функций:

Fixpoint even (n:nat):Prop := match n with | O => True | S m => odd m end
  with odd (n:nat):Prop := match n with | O => False | S m => even m end.

Сокращение йоты будет правильно расширяться по рекурсивным вызовам до четных или нечетных соответственно. Чтобы увидеть это, подумайте:

Theorem even_2 : even 2.
1 subgoal
==========
even 2
> lazy delta.

1 subgoal
==========
(fix even (n:nat):Prop := match n with ... end
 with odd (n:nat):Prop := match n with ... end
 for even) 2
> lazy iota.

1 subgoal
==========
(fun n:nat =>
  match n with
    | O => True
    | S m => (fix even (o:nat):Prop := match o with ... end
              with odd (o:nat):Prop := match o with ... end
              for odd) m
  end) 2

Проблема

Очевидно, это правильное поведение. К сожалению и, по-видимому, необъяснимо, Coq не будет применять сокращение йота в случаях, когда рекурсивная функция либо не применяется к аргументу, либо аргумент универсально квантифицируется. Например, следующее не работает:

Theorem even_n : forall n:nat, even n.
1 subgoal
==========
forall n:nat, even n
> intro n.

1 subgoal
n : nat
==========
even n
> lazy delta.

1 subgoal
==========
(fix even (n:nat):Prop := match n with ... end
 with odd (n:nat):Prop := match n with ... end
 for even) n
> lazy iota. (* FAILS TO REDUCE! *)

1 subgoal
==========
(fix even (n:nat):Prop := match n with ... end
 with odd (n:nat):Prop := match n with ... end
 for even) n

Я не вижу причин, по которым сокращение Iota должно зависеть от окружающего контекста, и пробовал несколько вариантов вышеизложенного, пытаясь заставить Coq to Iota уменьшить рекурсивные функции. К сожалению, ничего не получилось.

Как заставить Coq применять йота-редукции к рекурсивным функциям, которые либо не применяются ни к каким аргументам, либо применяются к универсальным количественным аргументам?

Любая помощь будет оценена по достоинству. Спасибо, - Ларри


computer-science theorem-proving coq lambda-calculus
person Larry Lee    schedule 23.04.2015    source источник
comment
Ваше определение odd и even кажется неверным: они оба определяют константный предикат fun n => False!   -  person Arthur Azevedo De Amorim    schedule 23.04.2015

Ответы (1)


arrow_upward
8
arrow_downward

Проблема здесь в том, что правило iota ограничено для точек фиксации: руководство Coq явно указывает, что iota может применяться к фиксированной точке только в том случае, если убывающий аргумент начинается с конструктора.

Это сделано для того, чтобы исчисление индуктивных построений было сильно нормализующим как система перезаписи: если бы мы всегда могли применять йоту, то можно было бы бесконечно расширять рекурсивные вхождения определяемой функции.

На практике, если вы хотите упростить такую ​​фиксированную точку, вы можете сделать две вещи:

  1. Уничтожьте рекурсивный аргумент (в вашем случае n) вручную, а затем уменьшите. В некоторых случаях это проще сделать, но требует рассмотрения многих случаев.

  2. Докажите лемму об упрощении и сделайте переписывание вместо редукции. Например, вы могли бы доказать лемму вида odd n <-> ~ even n, которая может помочь вам в некоторых случаях. Вы также можете явно доказать развертывание в виде леммы (на этот раз, используя исходное определение even):

    Goal forall n, even n = match n with | O => False | S m => odd m end.
now destruct n.
Qed.
person Arthur Azevedo De Amorim    schedule 23.04.2015
comment
Спасибо Артур, ваш ответ именно то, что я хотел знать. Я понимаю, почему Coq вводит это ограничение, и я ценю предложенный вами обходной путь. - person Larry Lee; 24.04.2015