~amiloradovsky/symbolic-dynamics

symbolic-dynamics/Decidable.v -rw-r--r-- 1.7 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
(* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
 * Some properties out there may essentially depend on the finiteness
 * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *)

Require Import Symbolic_Dynamics.Families.

Section Decidable.

  Variable 𝕄 : Type.

  Definition decidable_support (U : Family 𝕄) :=
    forall x, (True -> U x) + (U x -> False).

  (* In practice, we're going to only consider finite supports,
     they're decidable (by checking for equality with each element *)

  Definition Add {U : Type} (B : Family U) (x : U) : Family U :=
    Families.Union _ B (Families.Singleton _ x).
  Inductive Finite {U : Type} :
    Family U -> Type :=
    | Empty_is_finite : Finite (Families.Empty U)
    | Union_is_finite : forall A: Family U,
        Finite A -> forall x: U, ~ inhabited (A x) ->
                                 Finite (Add A x).

  Hypothesis decidable_equality_on_the_index :
    forall x y : 𝕄, (x = y) + (x <> y).

  Fixpoint finite_is_decidable (U: Family 𝕄)
           (H: Finite U) {struct H}: decidable_support U.
  Proof.
    intros. intro.
    destruct H.
    - (* the support is empty *)
      right. contradiction.
    - destruct (finite_is_decidable A H x).
      + (* the element is in the space *)
        left. constructor. now apply a.
      + destruct (decidable_equality_on_the_index x x0).
        * (* the element is added *)
          subst x0. left. right. constructor.
        * right. intros. inversion X.
          contradiction.
          now destruct X0.
  Qed.

  (* Finite or not, here we're only considering the decidable ones *)
  Hypothesis decidable_supports : forall U, decidable_support U.

End Decidable.