Объединение Coq по рекордным параметрам - PullRequest
Новая
       7

Объединение Coq по рекордным параметрам

0 голосов
/ 29 октября 2018

Я определил топологическое пространство следующим образом, 

Require Export Ensembles.
Arguments Full_set {U}.
Arguments Empty_set {U}.
Arguments In {U}.
Arguments Intersection {U}.
Arguments Union {U}.
Arguments Complement {U}.

Definition Family A := Ensemble (Ensemble A).
Inductive FamilyUnion {T : Type} (F: Family T) : Ensemble T :=
  | family_union_intro: forall (S:Ensemble T) (x:T),
      In F S -> In S x -> In (FamilyUnion F) x.

Inductive FamilyIntersection {T: Type} (F: Family T) : Ensemble T :=
  | family_intersect_intro : forall x, (forall (S:Ensemble T), (In F S) -> (In S x)) -> (In (FamilyIntersection F) x).

Record Topology : Type := mkTopology
{

          Point: Type;
          Open: Ensemble (Ensemble Point) ;
          EmptyOpen: (In Open Empty_set) ;
          FullOpen: (In Open Full_set) ;
          IntersectionOpen: forall x y,  (In Open x) -> (In Open y) -> (In Open (Intersection x y)) ;
          UnionOpen: forall F: (Family Point), (forall x: (Ensemble Point), (In F x) -> (In Open x)) -> In Open (FamilyUnion F)
}.


Definition Closed (T: Topology) := forall C: (Ensemble (Point T)),  In (Open T) (Complement C).

Но когда я пытаюсь определить, 

Theorem TopologyViaClosedSet {P: Type} (closed: Ensemble (Ensemble P)) 
    (emptyClosed: (In closed Empty_set)) 
    (fullClosed: (In closed Full_set)) 
    (unionClosed: (forall x y,  (In closed x) -> (In closed y) -> (In closed (Union x y)))) 
    (intersectionClosed: (forall F:(Family P), (forall x: (Ensemble P), (In F x) -> (In closed x)) -> (In closed (FamilyIntersection F)))) : 
    exists t: Topology,  forall x,  (In (Open t) x) <-> (In closed x)

Выдает ошибку объединения. Что я понимаю, почему это не может быть сделано, но могу ли я намекнуть Coq, что поле точки внутри t как-то P ((Point t) = P)?

1 Ответ

0 голосов
/ 29 октября 2018

Таким образом, проблема в том, что в exists t : Topology, forall x : P, ... мы бы хотели, чтобы Point t был по справедливости равен P, что связано еще дальше. Я не думаю, что это возможно, поэтому я бы предложил в качестве альтернативы (которые вы, возможно, уже рассмотрели):

  • Индексировать топологию по ее точечному полю, переопределяя Topology как Topology (Point : Type)

  • Связать точечные поля с помощью биекций: exists (t : Topology) (f : P <-> Point Topology), forall x : P, In (Open t) (f x) <-> In closed x

...