(* ** Abstract specification using Hoare triples *)

From Undecidability.TM Require Import TM Util.TM_facts.

(* Abstract Assertions over Tapes *)
Definition Assert (sig : Type) (n : nat) : Type := tapes sig n -> Prop.

(* {P} pM {fun c => Q c} means that whenever pM starts with tapes that satisfy P and terminates in label c and tapes tp' that satisfy Q c. *)

Definition Triple_Rel {sig : finType} {n : nat} {F : Type} (P : Assert sig n) (Q : F -> Assert sig n) : pRel sig F n :=
  fun tin '(yout, tout) => P tin -> Q yout tout.

Inductive Triple {sig : finType} {n : nat} {F : Type} P (pM : pTM sig F n) Q :=
  TripleI : pM ⊨ Triple_Rel P Q -> Triple P pM Q.

Lemma TripleE {sig : finType} {n : nat} {F : Type} P (pM : pTM sig F n) Q:
  Triple P pM Q -> pM ⊨ Triple_Rel P Q.
Proof. now inversion 1. Qed.

Lemma Triple_iff {sig : finType} {n : nat} {F : Type} P (pM : pTM sig F n) Q:
  Triple P pM Q <-> pM ⊨ Triple_Rel P Q.
Proof. split;eauto using TripleE,TripleI. Qed.

(* Triples for total correctness have an additional time parameter in the precondition.
The following definition relates such a precondition to a termination relation: *)

Definition Triple_TRel {sig : finType} {n : nat} (P : Assert sig n) (k : nat) : tRel sig n :=
  fun tin k' => P tin /\ k <= k'.

Inductive TripleT {sig : finType} {n : nat} {F : Type} (P : Assert sig n) (k : nat) (pM : pTM sig F n) (Q : F -> Assert sig n) :=
 TripleTI : Triple P pM Q -> projT1 pM ↓ Triple_TRel P k -> TripleT P k pM Q.

 Lemma TripleTE {sig : finType} {n : nat} {F : Type} P k (pM : pTM sig F n) Q:
  TripleT P k pM Q -> Triple P pM Q /\ projT1 pM ↓ Triple_TRel P k.
Proof. now inversion 1. Qed.

Lemma TripleT_iff {sig : finType} {n : nat} {F : Type} P k (pM : pTM sig F n) Q:
  TripleT P k pM Q <-> (Triple P pM Q /\ projT1 pM ↓ Triple_TRel P k).
Proof. split;firstorder eauto using TripleTE,TripleTI. Qed.

Lemma TripleT_Triple {sig : finType} {n : nat} {F : Type} P k (pM : pTM sig F n) Q :
  TripleT P k pM Q ->
  Triple P pM Q.
Proof. now intros ?%TripleTE. Qed.

#[export] Hint Resolve TripleT_Triple : core.

Lemma Triple_False {sig : finType} {n : nat} {F : Type} (pM : pTM sig F n) Q :
  Triple (fun _ => False) pM Q.
Proof. hnf. firstorder. Qed.

#[export] Hint Resolve Triple_False : core.

Lemma TripleT_False {sig : finType} {n : nat} {F : Type} k (pM : pTM sig F n) Q :
  TripleT (fun _ => False) k pM Q.
Proof. hnf. firstorder. Qed.

#[export] Hint Resolve TripleT_False : core.

Lemma Triple_True {sig : finType} {n : nat} {F : Type} (pM : pTM sig F n) P :
  Triple P pM (fun _ _ => True).
Proof. hnf. firstorder. Qed.

#[export] Hint Resolve Triple_True : core.

(* *** Conversion lemmas from realisation to Hoare triples *)

Lemma Realise_Triple {sig : finType} {n : nat} {F : Type} (P : Assert sig n) (pM : pTM sig F n) (Q : F -> Assert sig n) (R : pRel sig F n) :
  pM ⊨ R ->
  (forall tin yout tout, R tin (yout, tout) -> P tin -> Q yout tout) ->
  Triple P pM Q.
Proof.
  intros H1 H2. apply TripleI. unfold Triple_Rel. eapply Realise_monotone.
  + eapply H1.
  + intros tin (yout, tout). firstorder.
Qed.

Lemma Realise_TripleT {sig : finType} {n : nat} {F : Type} (P : Assert sig n) (k : nat) (pM : pTM sig F n) (Q : F -> Assert sig n) (R : pRel sig F n) (T : tRel sig n) :
  pM ⊨ R ->
  projT1 pM ↓ T ->
  (forall tin yout tout, R tin (yout, tout) -> P tin -> Q yout tout) ->
  (forall tin k', P tin -> k <= k' -> T tin k') ->
  TripleT P k pM Q.
Proof.
  intros H1 H2. split.
  - eapply Realise_Triple; eauto.
  - unfold Triple_TRel. eapply TerminatesIn_monotone; eauto.
    intros tin k' (?&Hk). firstorder.
Qed.

Lemma Triple_Realise {sig : finType} {n : nat} {F : Type} (P : Assert sig n) (pM : pTM sig F n) (Q : F -> Assert sig n) :
  Triple P pM Q ->
  pM ⊨ (fun tin '(yout,tout) => P tin -> Q yout tout).
Proof.
  intros ?%TripleE. now unfold Triple_Rel in *.
Qed.

Lemma TripleT_Realise {sig : finType} {n : nat} {F : Type} (P : Assert sig n) k (pM : pTM sig F n) (Q : F -> Assert sig n) :
  TripleT P k pM Q ->
  pM ⊨ (fun tin '(yout,tout) => P tin -> Q yout tout).
Proof.
  intros ?%TripleTE. now apply Triple_Realise .
Qed.

Lemma TripleT_TerminatesIn {sig : finType} {n : nat} {F : Type} (P : Assert sig n) (k : nat) (pM : pTM sig F n) (Q : F -> Assert sig n):
  TripleT P k pM Q ->
  projT1 pM ↓ (fun tin k' => P tin /\ k <= k').
Proof.
  intros ?%TripleTE. unfold Triple_TRel in *. tauto.
Qed.

(* A convienient lemma to convert constant-time realisation to a Hoare triple. Note that the reverse doesn't hold. *)
Lemma RealiseIn_TripleT {sig : finType} {n : nat} {F : Type} (P : Assert sig n) k (pM : pTM sig F n) (Q : F -> Assert sig n) (R : pRel sig F n) :
  pM ⊨c(k) R ->
  (forall tin yout tout, R tin (yout, tout) -> P tin -> Q yout tout) ->
  TripleT P k pM Q.
Proof.
  intros H1 H2. split.
  - eapply Realise_Triple.
    + eapply RealiseIn_Realise; eauto.
    + firstorder.
  - unfold Triple_TRel. eapply TerminatesIn_monotone.
    + eapply Realise_total. apply H1.
    + now intros tin k' (H&Hk).
Qed.

Inductive Entails (sig : Type) (n : nat) (P1 P2 : Assert sig n) :=
  EntailsI : (forall tin, P1 tin -> P2 tin) -> Entails P1 P2.

Lemma EntailsE (sig : Type) (n : nat) (P1 P2 : Assert sig n):
Entails P1 P2 -> (forall tin, P1 tin -> P2 tin).
Proof. now inversion 1. Qed.

Arguments Entails {_ _} _ _.

Lemma Entails_iff (sig : Type) (n : nat) (P1 P2 : Assert sig n):
Entails P1 P2 <-> (forall tin, P1 tin -> P2 tin).
Proof. split;firstorder eauto using EntailsE,EntailsI. Qed.

#[export] Hint Resolve EntailsI : core.

Instance Entails_PO (sig : Type) (n : nat): PreOrder (@Entails sig n).
Proof. split;hnf. all:setoid_rewrite Entails_iff. all:eauto. Qed.

(* *** Consequence Rule *)

Lemma Consequence (sig : finType) (n : nat) (F : Type) (P1 P2 : Assert sig n) (Q1 Q2 : F -> Assert sig n) (pM : pTM sig F n) :
  Triple P2 pM Q2 ->
  Entails P1 P2 ->
  (forall y, Entails (Q2 y) (Q1 y)) ->
  Triple P1 pM Q1.
Proof.
  intros H1%TripleE H2 H3. apply TripleI. setoid_rewrite Entails_iff in H2. setoid_rewrite Entails_iff in H3.
  eapply Realise_monotone.
  { apply H1. }
  { intros tin (yout, tout) H4. cbn in H4. cbn. intros H5. auto.
  }
Qed.

Lemma asPointwise A X (R: A -> A -> Prop) f g: (forall (x:X), R (f x) (g x)) -> pointwise_relation X R f g.
Proof. now cbv. Qed.

Instance Triple_Entails_Proper sig n F: Proper (Entails --> eq ==> pointwise_relation F Entails ==> Basics.impl) (@Triple sig n F).
Proof. repeat intro. subst. eapply Consequence;eauto. Qed.

Lemma Consequence_pre (sig : finType) (n : nat) (F : Type) (P1 P2 : Assert sig n) (Q : F -> Assert sig n) (pM : pTM sig F n) :
  Triple P2 pM Q ->
  Entails P1 P2 ->
  Triple P1 pM Q.
Proof. now intros ? ->. Qed.

Lemma Consequence_post (sig : finType) (n : nat) (F : Type) (P : Assert sig n) (Q1 Q2 : F -> Assert sig n) (pM : pTM sig F n) :
  Triple P pM Q2 ->
  (forall y, Entails (Q2 y) (Q1 y)) ->
  Triple P pM Q1.
Proof. now intros ? <-%asPointwise. Qed.

Lemma ConsequenceT (sig : finType) (n : nat) (F : Type) (P1 P2 : Assert sig n) (k1 k2 : nat) (Q1 Q2 : F -> Assert sig n) (pM : pTM sig F n) :
  TripleT P2 k2 pM Q2 ->
  Entails P1 P2 ->
  (forall y, Entails (Q2 y) (Q1 y)) ->
  k2 <= k1 ->
  TripleT P1 k1 pM Q1.
Proof.
  intros (H0&H1)%TripleTE H2 H3%asPointwise H4.
  split. now rewrite H2, <- H3.
  - eapply TerminatesIn_monotone.
    + apply H1.
    + unfold Triple_TRel. intros tin k (H&H'). split. 2: lia. setoid_rewrite Entails_iff in H2. eauto.
Qed.

Instance TripleT_Entails_Proper sig n F: Proper (Entails --> le ==> eq ==> pointwise_relation F Entails ==> Basics.impl) (@TripleT sig n F).
Proof. repeat intro. subst. eapply ConsequenceT;eauto. Qed.

Lemma ConsequenceT_post (sig : finType) (n : nat) (F : Type) (P : Assert sig n) (k : nat) (Q1 Q2 : F -> Assert sig n) (pM : pTM sig F n) :
  TripleT P k pM Q2 ->
  (forall y, Entails (Q2 y) (Q1 y)) ->
  TripleT P k pM Q1.
Proof. intros. eapply ConsequenceT; eauto. Qed.

Lemma ConsequenceT_pre (sig : finType) (n : nat) (F : Type) (P1 P2 : Assert sig n) (k1 k2 : nat) (Q : F -> Assert sig n) (pM : pTM sig F n) :
  TripleT P2 k2 pM Q ->
  Entails P1 P2 ->
  k2 <= k1 ->
  TripleT P1 k1 pM Q.
Proof. intros. eapply ConsequenceT; eauto. Qed.

(* *** Introducing Quantors *)

(* Many, may boring rules... I hope we won't ever need one of these. *)

Lemma Triple_exists_pre {sig : finType} {n : nat} {F : Type} (pM : pTM sig F n)
      (X : Type) (P : X -> Assert sig n) (Q : F -> Assert sig n) :
  (forall (x : X), Triple (P x) pM Q) ->
  Triple (fun tin => exists x : X, P x tin) pM (Q).
Proof. setoid_rewrite Triple_iff. unfold Triple_Rel. firstorder. Qed.

Lemma Triple_exists_con {sig : finType} {n : nat} {F : Type} (pM : pTM sig F n)
      (X : Type) (P : Assert sig n) (Q : X -> F -> Assert sig n) :
  (exists (x : X), Triple P pM (Q x)) ->
  Triple P pM (fun yout tout => exists x : X, Q x yout tout).
Proof. setoid_rewrite Triple_iff. unfold Triple_Rel. firstorder. Qed.

Lemma Triple_forall_pre {sig : finType} {n : nat} {F : Type} (pM : pTM sig F n)
      (X : Type) (P : X -> Assert sig n) (Q : F -> Assert sig n) :
  (exists (x : X), Triple (P x) pM Q) ->
  Triple (fun tin => forall x : X, P x tin) pM (Q).
Proof. setoid_rewrite Triple_iff. unfold Triple_Rel. firstorder. Qed.

Lemma Triple_forall_con {sig : finType} {n : nat} {F : Type} (pM : pTM sig F n)
      (X : Type) (P : Assert sig n) (Q : X -> F -> Assert sig n) :
  (forall (x : X), Triple P pM (Q x)) ->
  Triple P pM (fun yout tout => forall x : X, Q x yout tout).
Proof. setoid_rewrite Triple_iff. unfold Triple_Rel. firstorder. Qed.

Lemma Triple_eta_pre {sig : finType} {n : nat} {F : Type} (pM : pTM sig F n)
      (P : Assert sig n) (Q : F -> Assert sig n) :
  Triple P pM Q ->
  Triple (fun tin => P tin) pM Q.
Proof. exact id. Qed.

Lemma Triple_eta_con {sig : finType} {n : nat} {F : Type} (pM : pTM sig F n)
      (P : Assert sig n) (Q : F -> Assert sig n) :
  Triple P pM Q ->
  Triple P pM (fun yout => Q yout).
Proof. exact id. Qed.

Lemma Triple_eta_con2 {sig : finType} {n : nat} {F : Type} (pM : pTM sig F n)
      (P : Assert sig n) (Q : F -> Assert sig n) :
  Triple P pM Q ->
  Triple P pM (fun yout tout => Q yout tout).
Proof. exact id. Qed.

Lemma Triple_and_pre {sig : finType} {n : nat} {F : Type} (pM : pTM sig F n)
      (P1 : Assert sig n) (P2 : Prop) (Q : F -> Assert sig n) :
  (P2 -> Triple P1 pM Q) ->
  Triple (fun tin => P2 /\ P1 tin) pM Q.
Proof. setoid_rewrite Triple_iff. unfold Triple_Rel. firstorder. Qed.

Lemma Triple_and_con {sig : finType} {n : nat} {F : Type} (pM : pTM sig F n)
      (P : Assert sig n) (Q1 : F -> Assert sig n) (Q2 : Prop) :
  Triple P pM Q1 ->
  Q2 ->
  Triple P pM (fun yout tout => Q2 /\ Q1 yout tout).
Proof. setoid_rewrite Triple_iff. unfold Triple_Rel. firstorder. Qed.

(* The same for TripleT *)

Lemma TripleT_exists_pre {sig : finType} {n : nat} {F : Type} (pM : pTM sig F n)
      (X : Type) (P : X -> Assert sig n) (Q : F -> Assert sig n) k :
  (forall (x : X), TripleT (P x) k pM Q) ->
  TripleT (fun tin => exists x : X, P x tin) k pM (Q).
Proof. setoid_rewrite TripleT_iff;setoid_rewrite Triple_iff. unfold Triple_Rel,Triple_TRel. firstorder. Qed.

Lemma TripleT_exists_con {sig : finType} {n : nat} {F : Type} (pM : pTM sig F n)
      (X : Type) (P : Assert sig n) (Q : X -> F -> Assert sig n) k :
  (exists (x : X), TripleT P k pM (Q x)) ->
  TripleT P k pM (fun yout tout => exists x : X, Q x yout tout).
Proof. setoid_rewrite TripleT_iff;setoid_rewrite Triple_iff. unfold Triple_Rel,Triple_TRel. firstorder. Qed.

Lemma TripleT_forall_pre {sig : finType} {n : nat} {F : Type} (pM : pTM sig F n)
      (X : Type) (P : X -> Assert sig n) (Q : F -> Assert sig n) k :
  (exists (x : X), TripleT (P x) k pM Q) ->
  TripleT (fun tin => forall x : X, P x tin) k pM (Q).
Proof. setoid_rewrite TripleT_iff;setoid_rewrite Triple_iff. unfold Triple_Rel,Triple_TRel. firstorder. Qed.

Lemma TripleT_forall_con {sig : finType} {n : nat} {F : Type} (pM : pTM sig F n)
      (X : Type) (P : Assert sig n) (Q : X -> F -> Assert sig n) k {inhX: inhabitedC X} :
  (forall (x : X), TripleT P k pM (Q x)) ->
  TripleT P k pM (fun yout tout => forall x : X, Q x yout tout).
Proof.
  intros H; split.
  - apply Triple_forall_con. apply H.
  - apply H. apply default.
Qed.

Lemma TripleT_eta_pre {sig : finType} {n : nat} {F : Type} (pM : pTM sig F n)
      (P : Assert sig n) (Q : F -> Assert sig n) k :
  TripleT P k pM Q ->
  TripleT (fun tin => P tin) k pM Q.
Proof. exact id. Qed.

Lemma TripleT_eta_con {sig : finType} {n : nat} {F : Type} (pM : pTM sig F n)
      (P : Assert sig n) (Q : F -> Assert sig n) k :
  TripleT P k pM Q ->
  TripleT P k pM (fun yout => Q yout).
Proof. exact id. Qed.

Lemma TripleT_eta_con2 {sig : finType} {n : nat} {F : Type} (pM : pTM sig F n)
      (P : Assert sig n) (Q : F -> Assert sig n) k :
  TripleT P k pM Q ->
  TripleT P k pM (fun yout tout => Q yout tout).
Proof. exact id. Qed.

Lemma TripleT_and_pre {sig : finType} {n : nat} {F : Type} (pM : pTM sig F n)
      (P1 : Assert sig n) (P2 : Prop) (Q : F -> Assert sig n) k :
  (P2 -> TripleT P1 k pM Q) ->
  TripleT (fun tin => P2 /\ P1 tin) k pM Q.
Proof. setoid_rewrite TripleT_iff;setoid_rewrite Triple_iff. unfold Triple_Rel,Triple_TRel. firstorder. Qed.

Lemma TripleT_and_con {sig : finType} {n : nat} {F : Type} (pM : pTM sig F n)
      (P : Assert sig n) (Q1 : F -> Assert sig n) (Q2 : Prop) k :
  TripleT P k pM Q1 ->
  Q2 ->
  TripleT P k pM (fun yout tout => Q2 /\ Q1 yout tout).
Proof. setoid_rewrite TripleT_iff;setoid_rewrite Triple_iff. unfold Triple_Rel,Triple_TRel. firstorder. Qed.

(* In gernal, we shouldn't rely on the definition of Triple and TripleT. *)

(* TODO: This makes problems in HoareRegister.v. *)