Mefresa.Dec.WellTypedDecidability

Decidability - Well Formed and Well Typed Architectures

Most of the work was made in ContingencyDecidabilty and CardinalityDecidability. Here, we just put it together in a nice and easy way.

Require Export Mefresa.Dec.ContingencyDecidability.
Require Export Mefresa.Dec.CardinalityDecidability.

Definition well_typed_bool s :=
  sound_cardinality_bool s &&
  sound_contingency_bool s.

Theorem well_typed_correctness:
  forall s, well_typed s <-> well_typed_bool s = true.
Proof.
  intros.
  unfold well_typed;
  unfold well_typed_bool.
  rewrite sound_cardinality_reflection.
  rewrite sound_contigency_reflection.
  destruct (sound_cardinality_bool s);
  destruct (sound_contingency_bool s); intuition.
Qed.

Require Import Coq.Logic.Decidable.
Theorem well_typed_dec:
  forall s, decidable (well_typed s).
Proof.
  intros.
  unfold decidable.
  rewrite well_typed_correctness.
  destruct (well_typed_bool s); auto.
Qed.