HyPre.pred.Safety

Require Import VectorExtra VectorList.
Import VectorListNotations.
From Coq Require Import Lists.List Lia.
Import ListNotations.

From HyPre Require Import PreSuffix.

Module Safety.

  Section lessdot.

    Context (X : Type).
    Context (order : X -> X -> Prop).

    Infix "⋖" := order (at level 70).

    Definition safety_property (P : X -> Prop) :=
      forall (l1 l2 : X), l1 ⋖ l2 -> P l2 -> P l1.

    Lemma fail_stable (P : X -> Prop)
      : safety_property P -> forall (l1 l2 : X), l1 ⋖ l2 -> ~ P l1 -> ~ P l2.
    Proof.
      firstorder.
    Qed.

  End lessdot.

End Safety.

Import Safety.

Module ListSafety.

  Section x.

    Context {X : Type}.

    Definition list_safety (P : list X -> Prop) := safety_property (list X) prefix P.

  End x.

End ListSafety.

Import ListSafety.
From Coq Require Vectors.Vector.

Module Veclist.

  Section xk.
    Context {X : Type} {k : nat}.

    Definition veclist_prefix : Vector.t (list X) k -> Vector.t (list X) k -> Prop
      := Vector.Forall2 (fun l1 l2 => prefix l1 l2).

    Lemma veclist_prefix_app (a b : Vector.t (list X) k)
      : veclist_prefix a (b +vl+ a).
    Proof.
      unfold veclist_prefix.
      eapply Vec_Forall2_forall2.
      intros.
      rewrite veclist_app_nth.
      eapply prefix_app_r.
      econstructor.
    Qed.

    Definition veclist_safety (P : Vector.t (list X) k -> Prop) :=
      safety_property (Vector.t (list X) k) (veclist_prefix) P.

    Definition strict_veclist_prefix : Vector.t (list X) k -> Vector.t (list X) k -> Prop
      := fun a b => exists i c, veclist_prefix (c :i: a at i) b.

  End xk.

End Veclist.

Module KProp.

  Section xk.
    Context (X : Type) (k : nat) .

    Definition k_property (P : (X -> Prop) -> Prop)
      := (forall (v : Vector.t X k), P (fun x => Vector.In x v)) -> forall (xx : X -> Prop), P xx.

  End xk.

End KProp.
(*
Section StrictPre.

  Variable (A : Type).

  Definition StrictPrefix' :=
    fun (l l' : list A) => exists a : A, Prefix (a :: l) l'.

  Lemma prefix_strictPrefix:
    forall (e : A) (x ϕ : list A), Prefix ϕ x -> StrictPrefix' ϕ (e :: x).
  Proof.
    intros e x ϕ Hϕ1.
    unfold StrictPrefix'. cbn.
    revert dependent e.
    induction Hϕ1; intros.
    - exists e; econstructor.
    - specialize(IHHϕ1 a). destructH. exists a0. econstructor. auto.
  Qed.

  Lemma StrictPrefix_well_founded : well_founded (StrictPrefix').
  Proof.
    unfold well_founded.
    intros.
    induction a.
    - econstructor. intros. unfold StrictPrefix' in *. destructH. inversion H.
    - constructor. intros.
      unfold StrictPrefix' in H.
      destructH. cbn in *. inversion H;subst.
      + subst. auto.
      + eapply IHa. unfold StrictPrefix'. exists a1. cbn. auto.
  Qed.

End StrictPre.
*)