HyPre.pred.HyperSemantics

From Coq Require Import Program.Equality.

From HyPre Require Export
     VectorList
     VectorNat
     Semantics.
From HyPre Require Export VectorPair.

Section with_sem.
  Context {k : nat}.
  Context {Input St : Type}.
  Context (sem : Input -> list St -> Prop).
  Context (Hsem : rad_semantics sem).

  Lemma vsem_leneq_eq i (vsl1 vsl2 : Vector.t (list St) k)
    : Vector.Forall2 sem i vsl1 -> Vector.Forall2 sem i vsl2 -> vl_len vsl1 = vl_len vsl2 -> vsl1 = vsl2.
  Proof.
    intros Hsem1 Hsem2 Hlen.
    dependent induction Hsem1;
      dependent destruction Hsem2;
      cbn in *.
    - reflexivity.
    - dependent destruction Hlen.
      f_equal.
      + eapply sem_leneq_eq;eauto.
      + eapply IHHsem1;eauto.
  Qed.

End with_sem.