semantics.tower.ex_similarity

Require Import base ord tower.tarski tower.associated_closure tower.tower.

Lemma prod_exEc T (X : clat) I (P : I -> Prop) (F : I -> T -> X) (x : T) :
  (∃ i | P i, F i) x = (∃ i | P i, F i x).
Proof.
  rewrite prod_exE. f_equal; fext=> i. exact: prod_exE.
Qed.

Structure lts (Σ : Type) := mk_lts
  { lts_nodes :> Type
  ; step : Σ -> Rel lts_nodes
  }.
Arguments mk_lts {Σ} lts_nodes step.

Section Similarity.
Variable Σ : Type.
Variable (A B : lts Σ).

Definition sim (R : A -> B -> Prop) (a : A) (b : B) :=
  forall σ a', step σ a a' -> exists2 b', step σ b b' & R a' b'.
Definition similar := gfp sim.

Lemma similar_def (a : A) (b : B) :
  similar a b = exists2 R : A -> B -> Prop, (forall a' b', R a' b' -> sim R a' b') & R a b.
Proof.
  by rewrite/similar gfp_def !prod_exEc prop_exEc.
Qed.

End Similarity.

Definition loop : lts unit :=
  mk_lts unit (fun _ _ _ => True).

Definition countable_branching : lts unit :=
  mk_lts (option nat) (fun _ from to =>
    match from, to with
    | None, Some _ => True
    | Some n, Some m => n = m.+1
    | _, _ => False
    end).

Definition nsim {Σ} {A B : lts Σ} (n : nat) : A -> B -> Prop :=
  iter n (@sim Σ A B) (fun _ _ => True).

Lemma loop_countable_branching_nsim n :
  @nsim unit loop countable_branching n tt None.
Proof.
  case: n => //= n [] [] _. exists (Some n). exact I.
  elim: n => //= n ih [] [] _. exists (Some n). by []. exact ih.
Qed.

Lemma loop_countable_branching_not_similar :
  ~@similar unit loop countable_branching tt None.
Proof.
  rewrite similar_def.
  case=> R rs /rs/(_ tt tt I)[/=[]//n _]. elim: n.
  - by case/rs/(_ tt tt I) => /=-[].
  - move=> n ih /rs/(_ tt tt I) -[/=[]//m[<-{m}]]. exact ih.
Qed.

(*Section TypeSimilarity.
  Variables (Σ : Type) (A B : lts Σ).
  Definition tsim (R : A -> B -> Type) a b : Type :=
    forall σ a', step σ a a' -> { b' : B & (step σ b b' * R a' b')type }) ->
      tsimilarity R a b.

  Lemma tsimilarity_coind F :
    (forall R a b, F R a b ->
       forall (η : forall σ c c' d, R c d -> step σ c c' -> { d' & step σ d d' }) σ a',
         step σ a a' ->
         { b' &
           (step σ b b' *
            F (@dependent_back_sim R (fun σ c c' d r st => (η σ c c' d r st).1)) a' b')*)