Coq не признает равенство зависимого списка - PullRequest
Новая
       51

Coq не признает равенство зависимого списка

0 голосов
/ 06 марта 2019

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

У меня есть определение списка: 

Inductive list (A : Type) (f : A -> A -> A) : A -> Type :=
  |Acons : forall {x : A} (y' : A) (cons' : list f x), list f (f x y')
  |Anil : forall (x: A) (y : A), list f (f x y).

И это определения: 

Definition t_list (T : Type) := (T -> T -> T) -> T -> T.
Definition nil {A : Type} (f : A -> A -> A) (d : A) := d.
Definition cons {A : Type} (v' : A) (c_cons : t_list _) (f : A -> A -> A) (v'' : A) :=
  f (c_cons f v'') v'.

Fixpoint list_correspodence (A : Type) (v' : A) (z : A -> A -> A) (xs : list func v'):=
  let fix curry_list {y : A} {z' : A -> A -> A} (l : list z' y) := 
      match l with
        |Acons x y => cons x (curry_list y)
        |Anil _ _ y  => cons y nil
      end in (@curry_list _ _ xs) z (let fix minimal_case {y' : A} {functor : A -> A -> A} (a : list functor y') {struct a} :=
                                    match a with
                                      |Acons x y => minimal_case y
                                      |Anil _ x _ => x
                                    end in minimal_case xs).

Theorem z_next_list_coorresp : forall {A} (z : A -> A -> A) (x y' : A) (x' : list z x), z (list_correspodence x') y' = list_correspodence (Acons y' x').
intros.
generalize (Acons y' x').
intros.
unfold list_correspodence.
(*reflexivity should works ?*)
Qed.

z_next_list_coorres - это фактически лемма, мне нужно доказать цель в другой теории (v'_list x = (list_correspodence x)).

Я пытался с некоторыми ограниченными областями доказать list_correspodence и работает хорошо, кажется, что определения равны, но для coq нет.

1 Ответ

1 голос
/ 06 марта 2019

Здесь list_correspondence является ложным Fixpoint (то есть fix) (он не делает рекурсивных вызовов), и это мешает сокращению.

Вы можете принудительно уменьшить fix, уничтожив его убывающий аргумент: 

destruct x'.
- reflexivity.
- reflexivity.

Или вы можете избежать использования Fixpoint в первую очередь.Вместо этого используйте Definition.

Здесь вы можете столкнуться со странной ошибкой с неявными аргументами, которой можно избежать, добавив сигнатуру типа (как показано ниже) или не пометив неявные аргументы локальной функции curry_list: 

Definition list_correspodence (A : Type) (v' : A) (func : A -> A -> A) (xs : list func v')
  : A :=
 (* ^ add this *)
...