mc2.v

Require Import Setoid.
Require Import Lia.
Require Import Coq.Program.Equality.
Require Import Coq.Arith.Compare_dec.

Axiom double_neg : forall P, P <-> ~~P.
Lemma fold_not : forall (P: Prop), (P -> False) <-> ~P. intuition auto. Defined.
Axiom forall_exists_duality1 : forall {T} (P: T -> Prop), ~ (exists x, P x) <-> (forall x, ~ P x).
Axiom forall_exists_duality2 : forall {T} (P: T -> Prop), ~ (forall x, P x) <-> (exists x, ~ P x).
Axiom DeMorgan1 : forall (P Q : Prop), ~(P /\ Q) <-> (~P \/ ~Q).
Axiom DeMorgan2 : forall (P Q : Prop), ~(P \/ Q) <-> (~P /\ ~Q).
Ltac classical :=
  repeat match goal with
  | [ H : context[_ -> False] |- _ ] => rewrite (fold_not) in H (* sometimes intuition leaves us with negations like this. *)
  | [ H : context[~(~ _)]|- _ ] => rewrite <-double_neg in H
  | [ H : _ |- _ ] => rewrite DeMorgan1 in H
  | [ H : _ |- _ ] => rewrite DeMorgan2 in H
  | [ H: _ |- _] => erewrite forall_exists_duality1 in H
  | [ H: _ |- _] => erewrite forall_exists_duality2 in H
  | [ H : _ |- context[_ -> False] ] => rewrite (fold_not) (* sometimes intuition leaves us with negations like this. *)
  | [ H : _ |- context[~(~ _)] ] => rewrite <-double_neg
  | [ H : _ |- _ ] => rewrite DeMorgan1
  | [ H : _ |- _ ] => rewrite DeMorgan2
  | [ H: _ |- _] => erewrite forall_exists_duality1
  | [ H: _ |- _] => erewrite forall_exists_duality2
  end; try solve [intuition auto].  

Section LTLdef. 
  Context {T: Type}.
  Inductive LTL : Type :=
  injp_ltl : (T -> Prop) -> LTL
  | false_ltl : LTL
  | true_ltl : LTL
  | imp_ltl : LTL -> LTL -> LTL
  | until_ltl : LTL -> LTL -> LTL
  | next_ltl : LTL -> LTL.
  Definition TemInt : Type := nat -> T.
  Notation "φ U- ψ" := (until_ltl φ ψ) (at level 10).
  Definition from (k: nat): TemInt -> TemInt :=
      fun ζ n =>
        ζ (n+k).
  Notation "ζ ^^ k" := (from k ζ) (at level 10).

  Reserved Notation "ζ ⊨ φ" (at level 50, no associativity).
  Fixpoint models (ζ : TemInt) (φ : LTL) {struct φ}: Prop :=
      match φ with
      | injp_ltl p =>
        p (ζ 0)
      | imp_ltl ψ π =>
        (~(ζ ⊨ ψ) \/ (ζ ⊨ π))
      | next_ltl ψ =>
        (from 1 ζ) ⊨ ψ
      | until_ltl ψ π =>
        (exists (i:nat),
          ζ ^^ i ⊨ π
          /\ (forall j, j < i -> ζ ^^ j ⊨ ψ))
      | false_ltl =>
        False
      | true_ltl =>
        True
      end
  where "ζ ⊨ φ" := (models ζ φ).

  Fixpoint clarke_bm_helper (i k:nat) (ζ : TemInt) (φ : LTL): Prop :=
      match φ with
      | injp_ltl p =>
        p (ζ i)
      | imp_ltl ψ π =>
        (clarke_bm_helper i k ζ ψ) -> (clarke_bm_helper i k ζ π)
      | next_ltl ψ =>
        i < k /\ clarke_bm_helper (S i) k ζ ψ
      | until_ltl ψ π =>
        exists j, i <= j
             /\ j <= k
             /\ clarke_bm_helper j k ζ π
             /\ (forall b, (i <= b /\ b < j) ->
                     clarke_bm_helper b k ζ ψ)
      | false_ltl => False
      | true_ltl => True
      end.

  Definition clarke_bm k ζ φ: Prop := clarke_bm_helper 0 k ζ φ.


  Definition not_ltl (φ : LTL) : LTL := imp_ltl φ false_ltl.
  Definition ev_ltl (φ : LTL): LTL := true_ltl U- φ.
  Definition always_ltl (φ : LTL): LTL := not_ltl (ev_ltl (not_ltl φ)).
  Definition and_ltl (ϕ ψ : LTL) : LTL := not_ltl (imp_ltl ϕ (not_ltl ψ)).

  Theorem and_good : forall ζ ϕ ψ, ζ ⊨ ϕ /\ ζ ⊨ ψ <-> ζ ⊨ (and_ltl ϕ ψ).
  Proof.
    intros.
    split.
    { (* fwd *)
      intro.
      unfold  and_ltl,not_ltl.
      cbn.
      left.
      intro.
      repeat destruct H0; destruct H; auto.
    }
    {
      intro.
      split.
      {
        inversion H;
        cbn in H0;
        intuition auto;
        classical.
      }
      {
        inversion H; cbn in *; intuition auto; classical.
      }
    }
  Defined.

  Lemma ltl_not_good : forall ζ φ, ~ ζ ⊨ φ <-> ζ ⊨ (not_ltl φ).  
    Proof.
      (* Very lightly modified from a proof generated by GPT-3/copilot. *)  
      intros.
      split.
      { 
        intro H.
        unfold not_ltl.
        lazy.
        left.
        intro.
        repeat destruct H0; destruct H; auto.
      }
      {
        intro.
        inversion H; cbn in *; intuition auto; classical.
      }
    Defined.

  Theorem always_iff_loop_inv : forall (φ : LTL) (ζ : TemInt), 
    ζ ⊨ (always_ltl φ) 
    <-> (exists (i : nat), 
          (forall k, k >= i -> ζ ^^ k ⊨ φ -> ζ ^^ (k+1) ⊨ φ) /\ (forall (j : nat), j <= i -> ζ ^^ j ⊨ φ)).
  Proof.
    intros.
    split.
    { 
      intros H.
      exists 0.
      split; intros.
      {
        simpl in H.
        classical.
        destruct H; try solve [intuition auto].
        specialize (H (k+1)).
        classical.
        repeat destruct H; solve [intuition auto].
      } 
      {
        inversion H0.
        simpl in H.
        classical.
        destruct H; try solve [intuition auto].
        specialize (H 0).
        classical.
        repeat destruct H; try solve [intuition auto].
      }
    } 
    {
     intros H.  
     left.
     simpl.
     destruct H as [i [Hpres Hinit]].
     simpl.
     repeat (progress classical || intro).
     left.
     split; [|solve[intuition auto]].
     pose proof (lt_eq_lt_dec x i) as Hcompxi.
     repeat match goal with
            | [ H : context[{_} + {_}] |- _] => destruct H as [H | H]
            end; try solve [eapply Hinit;lia].
     {
      assert (Hstronger : forall n, ζ ^^ (i+n) ⊨ φ).
      {
        induction n.
        { 
          unshelve erewrite (_ : i + 0 = i). lia.
          eapply Hinit.
          auto.
        }
        { 
          unshelve erewrite (_ : i + S n = (i + n) + 1). lia.
          eapply Hpres.
          lia.
          auto.
        }
      }
      remember (x - i) as diff.
      unshelve erewrite (_ : x = i + diff); solve[lia || auto].
     }
    }
Defined.
End LTLdef.

Record Mealy : Type := mkMealy {
                           Σ : Type
                         ; Q : Type
                         ; δ : Q -> Σ -> Q
                         ; Q0 : Q
                         }.

Fixpoint MealyTrace' (M : Mealy) (I : nat -> Σ M) (n : nat) {struct n}: (Q M) :=
    match n with
    | 0 => Q0 M
    | S n' => let q' := MealyTrace' M I n' in (δ M) q' (I n')
    end.

Definition MealyTrace (M : Mealy) (I : nat -> Σ M) : @TemInt (Q M) :=
    fun n => MealyTrace' M I n.

Definition models_upto M k φ :=
      (* M models φ upto k cycles if (clake_bm k ζ φ) holds for all input traces I *)
      forall I, clarke_bm k (MealyTrace M I) φ.

Lemma MealyTrace0isQ0: forall M I, MealyTrace M I 0 = Q0 M.
  auto.
Defined.

Search pair.

Record state_seq (M: Mealy) : Type := {
    states : nat -> Q M;
    inputs : nat -> Σ M;
    len : nat;
    start_ok : (states 0 = Q0 M);
    connected: (forall t, (0 < t /\ t < len) -> (δ M) (states (t - 1)) (inputs (t-1)) = states t);
  }.

Arguments states {M}.
Arguments inputs {M}.
Arguments len {M}.
Arguments start_ok {M}.
Arguments connected {M}.

Lemma mealy_unfold_step : forall M I t,
    t > 0 ->
    (MealyTrace M I t) = δ M (MealyTrace M I (t - 1)) (I (t - 1)).
  intros.
  destruct t.
  { lia. }
  {
    simpl.
    unshelve erewrite (_ : forall k, k - 0 = k). { lia. }
    auto.
  }
Defined.

Definition reachability_diameter (M : Mealy) : Type :=
  (* A reachability diameter D is a natural number such that every state reachable
     in n steps can also be reached in D <= n steps. *)
  { D : nat &
        forall (s : state_seq M) (end_Q : Q M) (_ : s.(states) (s.(len) - 1) = end_Q),
          (D > 0 /\ D <= s.(len) /\ exists (s' : state_seq M ), len s' = D /\ s'.(states) (D-1) = end_Q) }.

Theorem rd_sufficies_bmc_gp_case:
  forall (D: nat) (M: Mealy) (I: nat -> Σ M) (p: Q M -> Prop) (_D : reachability_diameter M),
    D = projT1 _D ->
    models_upto M D (always_ltl (injp_ltl p)) ->
    models (MealyTrace M I) (always_ltl (injp_ltl p)).
Proof.
  intros D M I p _D HD HBoundedModel.
  cbn in *.
  classical.
  left.
  intro.
  classical.
  left.
  split; intuition auto.
  unshelve epose proof (_ : forall I (x : nat),
                             (0 <= x /\
                              x <= D ->
                              (p (MealyTrace M I x)))).
  {
    intros I0 x0 ?.
    unfold models_upto, clarke_bm,clarke_bm_helper in HBoundedModel.
    simpl in HBoundedModel.
    setoid_rewrite forall_exists_duality1 in HBoundedModel.
    repeat setoid_rewrite DeMorgan1 in HBoundedModel.
    specialize (HBoundedModel I0 x0).
    classical.
    repeat match goal with
           | [H : _ \/ _ |- _] => destruct H
           | [H: exists _, _ |- _] => destruct H
           | [H: _ -> False |- _] => eapply H
           end; try solve[lia || auto].

  }
  change (p (MealyTrace M I x)).
  clear HBoundedModel.
  rename H into HBoundedModel.
  unfold reachability_diameter in _D.
  destruct _D as [D' Drd].
  simpl in HD.
  symmetry in HD.
  subst.
  destruct (PeanoNat.Nat.le_decidable x D).
  {
    (* x <= D *)
    specialize (HBoundedModel I x ltac:(lia)); auto.
  }
  {
    unshelve epose proof (_ : x > D) as Hgt.
    solve[lia].
    clear H.

    epose (q := MealyTrace M I x).
    (* constructing the MealyTrace M I state sequence *)
    unshelve epose proof ( _ : { s : state_seq M & (s.(states) (len s - 1) = q /\ s.(len) = (x+1)) }) as MI_seq.
    {
      unshelve econstructor.
      { unshelve econstructor.
        { exact (fun t => (MealyTrace M I t)). }
        {
          exact I.
        }
        {
          exact (x+1).
        }
        {
          simpl.
          auto.
        }
        {
          simpl.
          intros.
          symmetry.
          unshelve rewrite mealy_unfold_step at 1.
          auto.
          intuition auto.
        }
      }
      {
        simpl.
        unshelve erewrite (_ : x+1-1 = x). lia.
        auto.
      }
    }
    (* From MI_seq ending in q, we use that D is a reachability diameter to get
       a new state sequence of length D ending also in q. *)
    destruct MI_seq as [s [Hs H_len_s]].
    specialize (Drd s q Hs).
    destruct Drd as [Dnz [HDlens seq_wit]].
    destruct seq_wit as [s' [len_s'_is_D s'_ends_with_q]].
    (* remember s' as s''. *)
    (* destruct s' as [s'states s'inputs s'len s'start_ok s'connected]; simpl in *. *)


    assert (forall t', t' < s'.(len) -> MealyTrace M s'.(inputs) t' = s'.(states) t') as H.
    {
      induction t'.
      {
        simpl.
        symmetry.
        exact s'.(start_ok).
      }
      {
        intro.
        rewrite mealy_unfold_step.
        unshelve erewrite (_ : S t' - 1 = t').
        lia.
        rewrite IHt'.
        unshelve erewrite (_ : t' = S t' - 1) at 1 2. lia.

        erewrite s'.(connected).
        auto.
        all: lia.
      }
    }
    change (p q).
    rewrite <-s'_ends_with_q.
    erewrite <-H.
    eapply HBoundedModel.
    all: subst; lia.
  }
Qed.