~amiloradovsky/symbolic-dynamics

symbolic-dynamics/Families.v -rw-r--r-- 2.4 KiB View raw
5857f238Andrew Miloradovsky .build.yml: continuous integration for SourceHut 7 months ago
                                                                                
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
(* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
 * Type families, a.k.a. constructive predicates and sets...
 *
 * This module is essentially an adaptation of Ensembles for Type,
 * to get over the issue with "indestructibility of propositions":
 * i.e. case analysis is not allowed for the ordinary disjunction.
 * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *)

Section Families.

  Variable U: Type.  (* a universe, the index type of the family *)

  Definition Family := U -> Type.
  (* Families may be thought of as predicates, and sets as well:
     The legend is that for every element of U there is given a type,
     empty or not; respectively, the predicate is false or true *)

  Inductive Empty: Family := .  (* i.e. the empty type on every index *)
  Inductive Full: Family := Full_intro: forall x: U, Full x.
  (* i.e. whatever element of U is taken, the type is non-empty *)

  Definition Included (A B: Family): Type := forall x: U, A x -> B x.
  Definition Same (A B: Family): Type :=
    (Included A B) * (Included B A).  (* a.k.a. equivalence *)

  Lemma Empty_is_a_subtype (A: Family): Included Empty A.
  Proof. unfold Included. intros. contradict X. Qed.
  Lemma Full_is_a_supertype (A: Family): Included A Full.
  Proof. unfold Included. intros. apply Full_intro. Qed.
  Definition Emptiness (A: Family) := Included A Empty.
  Definition Fullness (A: Family) := Included Full A.

  Inductive Intersection (A B: Family): Family :=
    Intersection_intro: forall x: U, A x -> B x -> (Intersection A B) x.
  Inductive Union (A B: Family): Family :=
    | Union_intro_0: forall x: U, A x -> (Union A B) x
    | Union_intro_1: forall x: U, B x -> (Union A B) x.
  (* The (co)product is defined via currying & recursion principles;
     alternatively, these might be defined via A + B and A * B *)

  Definition Disjoint (A B: Family): Type :=
    Emptiness (Intersection A B).
  Definition Covering (A B: Family): Type :=
    Fullness (Union A B).

  Inductive Singleton (x: U): Family :=
    Singleton_intro: Singleton x x.  (* a.k.a. reflexivity *)

  (** Extensionality Axiom *)

  Axiom Extensionality_Families: forall A B: Family, Same A B -> A = B.

End Families.

Hint Unfold Included Same Emptiness Covering Disjoint Covering:
  families.

Hint Resolve Full_intro Intersection_intro Union_intro_0 Union_intro_1
     Singleton_intro Extensionality_Families: families.