~amiloradovsky/symbolic-dynamics

symbolic-dynamics/Pattern_Sets.v -rw-r--r-- 2.9 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
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
Require Import Symbolic_Dynamics.Patterns.

Section Pattern_Sets.

  Variable 𝕄 : Type.
  Variable 𝔸 : Set.

  Structure pattern_structure :=
    {
      support: Symbolic_Dynamics.Families.Family _;
      pattern: anchored_pattern 𝕄 𝔸 support;
    }.
  Definition subpattern (u v: pattern_structure) :=
    exists (H: support u  support v),
      restriction 𝕄 𝔸 H (pattern v) = (pattern u).
  Definition subpattern' (F G: pattern_structure -> Prop) :=
    exists u v, (F u) /\ (G v) /\ subpattern u v.
  Inductive Singleton_pattern_structure (u: pattern_structure):
    pattern_structure -> Prop :=
    Singleton_pattern_structure_intro: Singleton_pattern_structure u u.
  Inductive generalized_cylinder (F: pattern_structure -> Prop)
            (x: configuration 𝕄 𝔸): Prop :=
    generalized_cylinder_intro:
      subpattern' F (Singleton_pattern_structure {| pattern := x |}) ->
      generalized_cylinder F x.

  (* TODO: how to best express the finiteness? *)

  Notation "'⟦' F '⟧'" := (generalized_cylinder F).

  Import Ensembles.

  Variables F G: Ensembles.Ensemble pattern_structure.

  (* F  G = F  G *)

  Lemma commutes_with_union_0:
    Ensembles.Union _ F G  (Ensembles.Union _ F G).
  Proof.
    unfold "⊆"; intros.
    case H as [HH].
    case HH as (u & _ & Fu & [] & SP).
    case Fu as [u Fu | u Gu];
      [ left; cbv in Fu |- * | right; cbv in Gu |- * ].
    all: constructor.
    all: remember {| pattern := x |} as X; move HeqX at top.
    all: unfold subpattern'.
    all: exists u, X; now repeat split.
  Qed.

  Lemma commutes_with_union_1:
    (Ensembles.Union _ F G)  Ensembles.Union _ F G.
  Proof.
    constructor.
    case H as [? HF|? HG]; [ cbv in HF | cbv in HG ].
    1: case HF as [HF].
    2: case HG as [HG].
    1: case HF as (u & _ & Fu & [] & SPu).
    2: case HG as (v & _ & Gv & [] & SPv).
    all: remember {| pattern := x |} as X; move HeqX at top.
    all: unfold subpattern'.
    - exists u, X. repeat split; [ now left | assumption ].
    - exists v, X. repeat split; [ now right | assumption ].
  Qed.

  Lemma commutes_with_union:
    Ensembles.Union _ F G = Ensembles.Union _ F G.
  Proof.
    apply Ensembles.Extensionality_Ensembles. split.
    - exact commutes_with_union_0.
    - exact commutes_with_union_1.
  Qed.

  (* F  G  F  G *)

  Lemma commutes_with_intersection_0:
    Ensembles.Intersection _ F G  (Ensembles.Intersection _ F G).
  Proof.
    constructor; [ cbv | cbv ].
    all: case H as [HH]; constructor.
    all: unfold subpattern' in *.
    all: remember ({| pattern := x |}) as X; move HeqX at top.
    all: case HH as (u & _ & Fu & [] & SP).
    all: exists u, X.
    all: case Fu as [u Fu Gu]; cbv in Fu, Gu.
    all: repeat split; try assumption.
  Qed.

End Pattern_Sets.