Определение отношения равенства для бесконечных деревьев

Question

В coq я могу определить отношения равенства для коиндуктивных типов, чьи компоненты являются парами:

Section Pairs.
Variable (A:Type).
CoInductive Stream :=
  cons : (A * Stream) -> Stream.

CoInductive Stream_eq : Stream -> Stream -> Prop := 
  stream_eq : forall t1 t2 b1 b2, Stream_eq (t1) (t2)
               -> (b1 = b2)
               -> Stream_eq (cons (b1,t1)) (cons (b2,t2)).
End Pairs.

Я также могу сделать это для типов, чьи компоненты являются функциями:

Section Functions.
Variable (A:Type).
CoInductive Useless :=
   cons_useless : (A -> Useless) -> Useless.

CoInductive Useless_eq : Useless -> Useless -> Prop := 
  useless_eq : forall t1 t2, (forall b, Useless_eq (t1 b) (t2 b))
                   -> Useless_eq (cons_useless t1) (cons_useless t2).
End Functions.

Но я не могу определить аналогичные отношения для типов, чьи компоненты являются функциями для пар:

Section FunctionsToPairs.
Variable (A:Type).
Variable (B:Type).
CoInductive InfiniteTree :=
  cons_tree : (A -> B * InfiniteTree) -> InfiniteTree.
CoInductive Tree_eq : InfiniteTree -> InfiniteTree -> Prop := 
  tree_eq : forall (t1:A -> B*InfiniteTree) (t2:A -> B*InfiniteTree), 
     (forall b, let (a1, c1) := (t1 b) in
                let (a2, c2) := (t2 b) in Tree_eq c1 c2 /\ a1 = a2)
                   -> Tree_eq (cons_tree t1) (cons_tree t2).
End FunctionsToPairs.

Я получаю ошибку:

Non strictly positive occurrence of "Tree_eq" in
 "forall t1 t2 : A -> B * InfiniteTree,
  (forall b : A, let (a1, c1) := t1 b in let (a2, c2) := t2 b in Tree_eq c1 c2 /\ a1 = a2) ->
  Tree_eq (cons_tree t1) (cons_tree t2)".

Есть ли способ иметь четко определенные отношения равенства для типа InfiniteTree?

Answer 1

Ваше определение в основном отклонено из-за использования структур ввода, которые не позволяют контролеру установить, что возникновение Tree_eq c1 c2 в конструкторе tree_eq является действительным. Если вы удалите их или напишите их по-другому, определение будет принято Coq.

Например, следующие работы:

CoInductive Tree_eq : InfiniteTree -> InfiniteTree -> Prop := 
  tree_eq : forall (t1:A -> B*InfiniteTree) (t2:A -> B*InfiniteTree), 
     (forall b, let x1 := (t1 b) in
                let x2 := (t2 b) in Tree_eq (snd x1) (snd x2) /\ fst x1 = fst x2)
                   -> Tree_eq (cons_tree t1) (cons_tree t2).

Обратите внимание, что с включенными примитивными проекциями ваше первоначальное определение работает (идея приходит от этого ответа @JasonGross).

Set Primitive Projections.

Record prod {A B} := pair { fst : A ; snd : B }.
Arguments prod : clear implicits.
Arguments pair {A B}.
Add Printing Let prod.
Notation "x * y" := (prod x y) : type_scope.
Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
Hint Resolve pair : core.

Section FunctionsToPairs.
Variable (A:Type).
Variable (B:Type).
CoInductive InfiniteTree :=
  cons_tree : (A -> B * InfiniteTree) -> InfiniteTree.
CoInductive Tree_eq : InfiniteTree -> InfiniteTree -> Prop := 
  tree_eq : forall (t1:A -> B*InfiniteTree) (t2:A -> B*InfiniteTree), 
     (forall b, let (a1, c1) := (t1 b) in
                let (a2, c2) := (t2 b) in Tree_eq c1 c2 /\ a1 = a2)
                   -> Tree_eq (cons_tree t1) (cons_tree t2).
End FunctionsToPairs.

Answer 2

Я думаю, что я, возможно, понял, как это сделать, не изменяя тип InfiniteTree, используя взаимную дедукцию.

CoInductive Tree_eq : InfiniteTree -> InfiniteTree -> Prop := 
  tree_eq : forall (t1:A -> B*InfiniteTree) (t2:A -> B*InfiniteTree), 
                    (forall b,  Pair_eq (t1 b) (t1 b))
                   -> Tree_eq (cons_tree t1) (cons_tree t2)
  with Pair_eq : B*InfiniteTree -> B*InfiniteTree -> Prop :=
    pair_eq : forall b1 b2 t1 t2, b1 = b2 -> Tree_eq t1 t2 -> Pair_eq (b1, t1) (b2, t2).

Недостатком является то, что таким образом, вероятно, сложнее построить доказательства Tree_eq, чем с помощью метода, описанного в ответе Артура.

Answer 3

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

Section FunctionsToPairs.
Variable (A:Type).
Variable (B:Type).
CoInductive InfiniteTree :=
  cons_tree : (A -> B) -> (A -> InfiniteTree) -> InfiniteTree.
CoInductive Tree_eq : InfiniteTree -> InfiniteTree -> Prop :=
  tree_eq : forall (f1 f2 : A -> B) (t1 t2 : A -> InfiniteTree),
    (forall x, f1 x = f2 x) ->
    (forall x, Tree_eq (t1 x) (t2 x)) ->
    Tree_eq (cons_tree f1 t1) (cons_tree f2 t2).
End FunctionsToPairs.