CODEWITHSUNDEEP
coq
Vinothkumar Raman
Vinothkumar Raman

Reputation: 301

Coq unification on record params

I have defined topology space like this,

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).

But when I try to define,

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)

It throws unification error. Which I understand why it cant be done, But Is it possible for me to hint Coq that, the point field inside the t is P somehow ((Point t) = P)?

Upvotes: 0

Views: 60

Answers (1)

Li-yao Xia
Li-yao Xia

Reputation: 33429

So the problem is that in exists t : Topology, forall x : P, ... we would like Point t to be judgementally equal to P, which is bound farther up. I don't think that is possible, so I would propose as alternatives (that you may have already considered):

  • Index the topology by its point field, redefining Topology as Topology (Point : Type)

  • Relate point fields via bijections: exists (t : Topology) (f : P <-> Point Topology), forall x : P, In (Open t) (f x) <-> In closed x

Upvotes: 1

Related Questions