Использование обоснованной индукции для определения факториала - PullRequest
Новая
       5

Использование обоснованной индукции для определения факториала

1 голос
/ 06 апреля 2020

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

Definition fac : nat -> nat := Fix LtWellFounded (fun _ => nat)   (* 'LtWellFounded' is some proof *)
    (fun (n:nat) =>
        match n as n' return (forall (m:nat), m < n' -> nat) -> nat with
        | 0     => fun _ => 1
        | S m   => fun (g : forall (k:nat), k < S m -> nat) => S m *  g m (le_n (S m)) 
        end).

, но тогда, конечно, сразу возникает вопрос о правильности. И, пытаясь доказать, что моя функция везде совпадала с обычной реализацией fac, я понял, что все далеко не тривиально. На самом деле просто показать, что fac 0 = 1: 

Lemma fac0 : fac 0 = 1.
Proof.
    unfold fac, Fix, Fix_F.

Show.

, кажется трудным. У меня осталась цель: 

1 subgoal

  ============================
  (fix Fix_F (x : nat) (a : Acc lt x) {struct a} : nat :=
     match x as n' return ((forall m : nat, m < n' -> nat) -> nat) with
     | 0 => fun _ : forall m : nat, m < 0 -> nat => 1
     | S m =>
         fun g : forall k : nat, k < S m -> nat => S m * g m (le_n (S m))
     end (fun (y : nat) (h : y < x) => Fix_F y (Acc_inv a h))) 0
    (LtWellFounded' 0) = 1

, и я не вижу, как ее уменьшить. Кто-нибудь может предложить путь вперед?

Ответы [ 2 ]

2 голосов
/ 06 апреля 2020

Применение точки fix уменьшается только тогда, когда аргумент, для которого он возвращается, имеет конструктор во главе. destruct (LtWellFounded' 0), чтобы раскрыть конструктор, и тогда это уменьшится до 1 = 1. Или, что еще лучше, убедитесь, что LtWellFounded' прозрачен (его доказательство должно заканчиваться Defined., а не Qed.), и тогда все это доказательство просто reflexivity..

1 голос
/ 09 апреля 2020

Некоторые из указанных вами типов могут быть выведены Coq, поэтому вы также можете написать свой fib в несколько более удобочитаемой форме. Используйте dec, чтобы не забыть, в какой ветке if вы находитесь, и заставить рекурсивную функцию принимать рекурсор fac в качестве аргумента. Это может быть вызвано с меньшими аргументами. Используя refine, вы можете вставлять дыры (как в Agda) и позже получить обязательство по доказательству. 

Require Import Wf_nat PeanoNat Psatz. (* for lt_wf, =? and lia *)

Definition dec b: {b=true}+{b=false}.
  now destruct b; auto.
Defined.

Definition fac : nat -> nat.
  refine (Fix lt_wf _
   (fun n fac =>
      if dec (n =? 0)
      then 1
      else n * (fac (n - 1) _))).

  clear fac. (* otherwise proving fac_S becomes impossible *)
  destruct n; [ inversion e | lia].
Defined.

Lemma fac_S n: fac (S n) = (S n) * fac n.
  unfold fac at 1; rewrite Fix_eq; fold fac.
  now replace (S n - 1) with n by lia.
  now intros x f g H; case dec; intros; rewrite ?H. 
Defined.

Compute fac 8.

дает 

Compute fac 8.
     = 40320
     : nat
...