~amiloradovsky/symbolic-dynamics

symbolic-dynamics/Concatenation.v -rw-r--r-- 6.2 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
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
Require Import Symbolic_Dynamics.Pattern_Sets.

Section Patterns_Concatenation.

  Variable 𝕄 : Type.
  Variable 𝔸 : Set.

  Import Symbolic_Dynamics.Patterns.

  Section Flat_Definition.

    Variables U V: Symbolic_Dynamics.Families.Family 𝕄.

    Definition concatenation
               (u: anchored_pattern 𝕄 𝔸 U)
               (v: anchored_pattern 𝕄 𝔸 V):
      anchored_pattern 𝕄 𝔸 (Families.Union _ U V).
    Proof.
      intro.
      destruct X as [x UV].
      destruct UV as [x Ux | x Vx].
      - apply u. now exists x.
      - apply v. now exists x.
    Defined.
    (*
      Here we define a pattern on the union (sum) of the spaces,
      whose elements are introduced by either of the constructors.
      We're also able to destruct the elements of the union
      to perform the case analysis (construct by recursion).
      Therefore, if an element "is in" the union,
      we always know which one of the spaces it "came from",
      and thus don't have the ambiguity on the intersection:
      since there is no intersection... the union is always disjoint!
     *)
    Lemma concatenation_is_commutative
          (u: anchored_pattern 𝕄 𝔸 U)
          (v: anchored_pattern 𝕄 𝔸 V):
      concatenation u v = concatenation u v.
    Proof. reflexivity. Qed.

  End Flat_Definition.

  Definition concatenation_of_pattern_structures
             (u v: pattern_structure 𝕄 𝔸) :=
    Build_pattern_structure 𝕄 𝔸
      _ (concatenation _ _ (pattern 𝕄 𝔸 u) (pattern 𝕄 𝔸 v)).

  Inductive concatenation'
            (F G: Ensembles.Ensemble (pattern_structure 𝕄 𝔸)) :
    Ensembles.Ensemble (pattern_structure 𝕄 𝔸) :=
    concatenation'_intro: forall u v,
      F u -> G v -> concatenation'
                      F G (concatenation_of_pattern_structures u v).

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

  Variables F G: Ensembles.Ensemble (pattern_structure 𝕄 𝔸).

  Import FunctionalExtensionality.

  Lemma commutes_with_intersection_1:
    Ensembles.Included _ (concatenation' F G)
                       (Ensembles.Intersection _ F G) ->
    (Ensembles.Intersection _ F G)  Ensembles.Intersection _ F G.
  Proof.
    unfold "⊆". intros Hconcat ? ?.
    case H as [? HF HG]; cbv in HF, HG.
    case HF as [HF]; case HG as [HG]; constructor.
    unfold subpattern' in *.
    remember {| pattern := x |} as X; move HeqX at top.
    case HF as (u & _ & Fu & [] & SPu).
    case HG as (v & _ & Gv & [] & SPv).
    pose (w := Build_pattern_structure
                 𝕄 𝔸 _ (concatenation
                          _ _ (pattern 𝕄 𝔸 u) (pattern 𝕄 𝔸 v))).
    exists w. exists X.
    specialize (Hconcat w).
    split.
    - apply Hconcat. constructor. all: assumption.
    - repeat split.
      unfold subpattern.
      assert (HX: forall x : 𝕄,
                 support _ _ w x -> support _ _ X x) by now subst X.
      exists HX.
      apply functional_extensionality; intro Hw.
      destruct Hw as [y Hy].
      subst w.
      subst X.
      unfold concatenation.
      cbn.
      destruct SPu as [Iu Eu]. rewrite <- Eu.
      destruct SPv as [Iv Ev]. rewrite <- Ev.
      cbn.
      destruct Hy.
      all: repeat f_equal; destruct HX.
      + now case Iu.
      + now case Iv.
  Qed.
  (* TODO: show that the additional condition is necessary *)

  (* F  G = F  G *)

  Lemma intersection_is_in_concatenation:
    Ensembles.Intersection _ F G  concatenation' F G.
  Proof.
    unfold "⊆". intros.
    case H as [? HF HG]; cbv in HF, HG.
    case HF as [HF]; case HG as [HG]; constructor.
    unfold subpattern' in *.
    remember {| pattern := x |} as X; move HeqX at top.
    case HF as (u & _ & Fu & [] & SPu).
    case HG as (v & _ & Gv & [] & SPv).
    eexists. exists X.
    repeat split. exact Fu. exact Gv. clear F G Fu Gv.
    unfold subpattern in *.
    case SPu as [Hu Eu].
    case SPv as [Hv Ev].
    subst X; cbn in *.
    assert (H: (Families.Union _ (support _ _ u) (support _ _ v))
                  (Families.Full _)) by constructor.
    exists H.
    apply functional_extensionality; intro Huv.
    destruct Huv as [t ht].
    rewrite <- Eu, <- Ev; cbv; clear.
    case ht as [t ?|t ?]; cbn; clear.
    all: f_equal.
    all: destruct H as [t]; clear.
    - now case Hu.
    - now case Hv.
  Qed.

  Lemma concatenation_is_in_intersection:
    concatenation' F G  Ensembles.Intersection _ F G.
  Proof.
    unfold "⊆". intros.
    constructor. all: cbv.
    all: destruct H; constructor.
    all: remember ({| pattern := x |}) as X; move HeqX at top.
    all: unfold subpattern' in *.
    all: destruct H as (y & _ & CFGy & [] & SP).
    all: destruct CFGy as [u v Fu Gv].
    1: exists u, X. 2: exists v, X.
    all: repeat split.
    all: try assumption; clear F G Fu Gv.
    all: unfold subpattern in *.
    all: destruct SP as [H RE].
    1: assert (Hu: support _ _ u  support _ _ X).
    1: {
      unfold "⊆". intros x' ?.
      subst X. cbv. constructor.
    }
    2: assert (Hv: support _ _ v  support _ _ X).
    2: {
      unfold "⊆". intros x' ?.
      subst X. cbv. constructor.
    }
    1: exists Hu. 2: exists Hv.
    all: subst X; cbn in *.
    all: unfold restriction in *; unfold concatenation in RE.
    (* Now get rid of the union (in the hypotheses) *)
    1: unfold "⊆" in Hu, H.
    2: unfold "⊆" in Hv, H.
    all: apply functional_extensionality; intro Hux.
    all: destruct Hux as [t ht].
    1: pose (h := Families.Union_intro_0 _ _ (support _ _ v) _ ht).
    2: pose (h := Families.Union_intro_1 _ (support _ _ u) _ _ ht).
    all: assert (RE'' := equal_f RE); clear RE.
    all: specialize (RE'' (existT _ t h)).
    all: cbn in RE''.
    all: rewrite <- RE''; clear.
    all: f_equal; clear.
    all: induction H as [t].
    all: specialize (H t h); clear.
    - now case Hu.
    - now case Hv.
  Qed.

  Lemma concatenation_commutes_with_intersection:
    concatenation' F G = Ensembles.Intersection _ F G.
  Proof.
    apply Ensembles.Extensionality_Ensembles. split.
    - exact concatenation_is_in_intersection.
    - exact intersection_is_in_concatenation.
  Qed.

End Patterns_Concatenation.