File ModelIsomorphism

From MatchingLogic Require Export Surj
                                  monotonic.

Import MatchingLogic.Substitution.Notations.

Section isomorphism.
  Open Scope ml_scope.

  (* Polymorphic Cumulative *)
  Record ModelIsomorphism {Σ : Signature} {M₁ M₂ : Model} : Type := mkModelIsomorphism
      {
          mi_f : (Domain M₁) → (Domain M₂) ;
          mi_inj :> Inj (=) (=) mi_f ;
          mi_surj :> Surj' (=) mi_f ;
          mi_sym : ∀ (s : symbols),
              mi_f <$> (sym_interp M₁ s) ≡ sym_interp M₂ s ;
          mi_app : ∀ (x y : Domain M₁),
              mi_f <$> (@app_interp Σ M₁ x y) ≡ @app_interp Σ M₂ (mi_f x) (mi_f y) ;
      }.

  Definition isom {Σ : Signature} : relation Model :=
      λ M₁ M₂, ∃ (r : @ModelIsomorphism _ M₁ M₂), True.

  Definition ModelIsomorphism_refl {Σ : Signature} (M : Model) : @ModelIsomorphism _ M M.

  Definition ModelIsomorphism_sym {Σ : Signature} (M₁ M₂ : Model) (i : @ModelIsomorphism _ M₁ M₂)
  : @ModelIsomorphism _ M₂ M₁.

  Program Definition ModelIsomorphism_trans {Σ : Signature} (M₁ M₂ M₃ : Model)
      (i : @ModelIsomorphism _ M₁ M₂)
      (j : @ModelIsomorphism _ M₂ M₃)
      : @ModelIsomorphism _ M₁ M₃
      :=
      {|
          mi_f := (mi_f j) ∘ (mi_f i)
      |}.

  #[global]
  Instance ModelIsomorphism_equiv {Σ : Signature} : Equivalence isom.

  (*
  [global] Instance ModelIsomorphism_sym_cancel {Σ : Signature} (M₁ M₂ : Model) (i : @ModelIsomorphism _M₁ M₂) : Cancel (=) (mi_f i) (mi_f (ModelIsomorphism_sym i)). Proof. unfold Cancel. intros x. unfold ModelIsomorphism_sym. simpl. Qed. *)

  Lemma fmap_app_ext {Σ : Signature} (M : Model) (X Y : propset (Domain M))
      (B : Type) (f : (Domain M) → B)
      :
      f <$> app_ext X Y ≡ {[ e | ∃ le re : M, le ∈ X ∧ re ∈ Y ∧ e ∈ (f <$> (app_interp _ le re)) ]}.

  Lemma update_evar_val_compose
      {Σ : Signature} (M₁ M₂ : Model) (ρ : @Valuation Σ M₁) (x : evar) (m : Domain M₁)
      (f : Domain M₁ → Domain M₂)
      :
      (update_evar_val x (f m)
               {|
                 evar_valuation := f ∘ evar_valuation ρ;
                 svar_valuation := λ X : svar, f <$> svar_valuation ρ X
               |})
      =
      {|
      evar_valuation := f ∘ evar_valuation (update_evar_val x m ρ);
      svar_valuation := λ X : svar, f <$> svar_valuation (update_evar_val x m ρ) X ;
      |}.

  Lemma update_svar_val_compose
      {Σ : Signature} (M₁ M₂ : Model) (ρ : @Valuation Σ M₁) (X : svar) (ms : propset (Domain M₁))
      (f : Domain M₁ → Domain M₂)
      :
      (update_svar_val X (f <$> ms)
      {| evar_valuation := f ∘ evar_valuation ρ ;
         svar_valuation := λ X : svar, (f <$> (svar_valuation ρ X)) ;
      |})
      =
      {|
        evar_valuation := f ∘ evar_valuation (update_svar_val X ms ρ) ;
        svar_valuation := λ Y : svar, f <$> (svar_valuation (update_svar_val X ms ρ) Y) ;
      |}.

  Theorem isomorphism_preserves_semantics
      {Σ : Signature}
      (M₁ M₂ : Model)
      (i : @ModelIsomorphism _ M₁ M₂)
      :
      ∀ (ϕ : Pattern) (ρ : @Valuation _ M₁),
          ((mi_f i) <$> (@eval Σ M₁ ρ ϕ))
          ≡@{propset (Domain M₂)} (@eval Σ M₂ (mkValuation ((mi_f i) ∘ (evar_valuation ρ)) (λ X, (mi_f i) <$> (svar_valuation ρ X))) ϕ).
End isomorphism.