Доказательства эквивалентности между не-хвостом-рекурсивными и хвостовой рекурсией функциями

Question

у меня есть рекурсивная функция *, которая похожа на «опциональную карту», ​​со следующей подписью:

omap (f : option Z -> list nat) (l : list Z) : option (list nat) 

Я определил эквивалент (по модулю хвостовая рекурсивная функция (omap_tr ниже), и я хотел бы доказать, что оба они эквивалентны, по крайней мере, в случае Some.

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

* Функция была упрощена; например, None кажется бесполезным здесь, но это необходимо в исходной функции.

код

Вот код (упрощенный) не-хвост рекурсивной функции, наряду с примером функции f:

Fixpoint omap (f : option Z -> list nat) (l : list Z) : option (list nat) := 
    match l with 
    | nil => Some nil 
    | z :: zr => 
    let nr1 := f (Some z) in 
    let nr2 := match omap f zr with 
       | None => nil 
       | Some nr' => nr' 
       end in 
    Some (nr1 ++ nr2) 
    end. 

Let f (oz : option Z) : list nat := 
    match oz with 
    | None => nil 
    | Some z => Z.to_nat z :: nil 
    end. 

Например, omap f просто преобразует Z целые числа, чтобы nat целые:

Compute omap f (1 :: 2 :: 3 :: 4 :: nil)%Z. 

= Some (1%nat :: 2%nat :: 3%nat :: 4%nat :: nil) : option (list nat) 

Я выполнил то, что я считаю, это стандартный аккумулятор основанное преобразование, добавление acc параметра как к f и omap:

Fixpoint omap_tr (f_tr : option Z -> list nat -> list nat) (l : list Z) 
       (acc : list nat) : option (list nat) := 
    match l with 
    | nil => Some acc 
    | z :: zr => let nr1 := f_tr (Some z) acc in 
       omap_tr f_tr zr nr1 
    end. 

Let f_tr rz acc := 
    match rz with 
    | None => acc 
    | Some z => Z.to_nat z :: acc 
    end. 

Это похоже на работу, несмотря на возвращении перевернутого списка. Вот пример его использования, с непустым аккумулятора:

Compute match omap_tr f_tr (3 :: 4 :: nil)%Z (rev (1 :: 2 :: nil))%nat with 
      | Some r => Some (rev r) 
      | None => None 
     end. 

= Some (1%nat :: 2%nat :: 3%nat :: 4%nat :: nil) : option (list nat) 

Моя первая попытка включала nil аккумулятор:

Lemma omap_tr_failed: 
    forall l res, 
    omap_tr f_tr l nil = Some res -> 
    omap f l = Some (rev res). 

Но я не смог сделать индукцию. Я предполагаю, что это должно быть потому, что инвариант недостаточно силен для обработки общего случая.

Тем не менее, мне кажется, что любой из следующих лемм должно быть доказуемо, но я боюсь, что они также не достаточно сильны, чтобы дать доказательство:

Lemma omap_tr': 
    forall l acc res, 
    omap_tr f_tr l acc = Some (res ++ acc) -> 
    omap f l = Some (rev res). 

Lemma omap_tr'': 
    forall l acc res, 
    omap_tr f_tr l acc = Some res -> 
    exists res', 
     omap f l = Some res' /\ 
     res = (rev res') ++ acc. 

Если стандартная двойная индукция позволяют этим леммы, которые должны быть доказаны напрямую, или мне нужны более сильные инварианты?

Answer 1

Да, ваш omap_tr'' инвариант отлично работает для вашей леммы. Возможно, вы забыли обобщить более acc и res, прежде чем делать индукцию, или забыли применить некоторые факты перезаписи о app и rev?

Lemma omap_tr'': 
    forall l acc res, 
    omap_tr f_tr l acc = Some res -> 
    exists res', 
     omap f l = Some res' /\ 
     res = (rev res') ++ acc. 
Proof. 
    induction l as [|x l IH]; intros acc res; simpl. 
    - intros H. inversion H; subst acc; clear H. 
    exists []; eauto. 
    - intros H. apply IH in H. 
    destruct H as (res' & H & ?). subst res. 
    rewrite H. 
    eexists; split; eauto. 
    simpl. now rewrite <- app_assoc. 
Qed. 

Lemma omap_tr_correct : 
    forall l res, 
    omap_tr f_tr l [] = Some res -> 
    omap f l = Some (rev res). 
Proof. 
    intros l res H. apply omap_tr'' in H. 
    destruct H as (res' & ? & E). 
    subst res. 
    now rewrite app_nil_r, rev_involutive. 
Qed.