~amiloradovsky/symbolic-dynamics

symbolic-dynamics/Patterns.v -rw-r--r-- 2.5 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
(* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
 * Patterns, their supports, cylinders, and languages
 * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *)

(* This module is concerned with a specific topological space, namely,
   the product of identical copies of a set with discrete topology *)
(* Since the usual union of ensembles isn't sufficient to define
   concatenation of patterns, we use type families for the supports,
   and not ensembles. So one should pay attention to the difference. *)

Require Import Unicode.Utf8_core.
Require Symbolic_Dynamics.Families.  (* needed for the concatenation *)
Require FunctionalExtensionality.  (* equality of functions *)
Require Ensembles.

Notation "A '⊆' B" := (Families.Included _ A B) (at level  70,
                                                 no associativity).
Notation "A '⊇' B" := (Families.Included _ B A) (at level  70,
                                                 no associativity).

Section Patterns.

  Variable 𝕄 : Type.  (* the "time" domain, e.g. N^d or Z^d (d: nat) *)
  Variable 𝔸 : Set.  (* the alphabet, the space of the symbols,
                        the equality of symbols is proof-irrelevant *)

  (* Definition anchored_pattern (U: Ensemble 𝕄) := ex U -> 𝔸. *)
  (* Definition anchored_pattern (U: Ensemble 𝕄) := sig U -> 𝔸. *)
  Definition anchored_pattern
             (U: Symbolic_Dynamics.Families.Family 𝕄) := sigT U -> 𝔸.
  (* Here Family T defines the support of the (anchored) pattern:
     namely, all such values of t: T for which (U t) is inhabited *)

  Import FunctionalExtensionality.

  Definition empty_pattern := anchored_pattern (Families.Empty 𝕄).
  Lemma only_one_empty_pattern: forall p q: empty_pattern, p = q.
  Proof. intros p q. cbv in p, q.
         apply functional_extensionality; intro.
         destruct x. contradiction. Qed.

  Definition full_pattern := anchored_pattern (Families.Full _).
  Definition configuration := full_pattern.  (* for the symmetry *)

  Definition always_in_full: forall {U X}, X  Families.Full U.
  Proof. constructor. Defined.

  Definition restriction
             {U V: Symbolic_Dynamics.Families.Family 𝕄} (H: U  V)
             (v: anchored_pattern V): anchored_pattern U.
  Proof. intro. apply v. destruct X. exists x. apply (H x u). Defined.
  (* The direct definitions, without resorting to the tactic language,
     would be much shorter, but the verbosity is hopefully helpful *)
  (* Also, maybe this should be an inductive type, and not a function *)

End Patterns.