(*T* \usection{State Predicates} *T*)

(*T* The module |state_pred| introduces the type |s_prop| of state
predicates, i.e. propositions depending on states. *T*)

Definition s_prop := (st->Prop).

(*T* The usual logical operators are lifted from |Prop| to |s_prop| in
the natural way. *T*)

Definition s_true := [p:st] 
  True.
Definition s_false := [p:st] 
  False.
Definition s_or := [p,q:s_prop]
  [s:st] (p s) \/ (q s).
Definition s_or3 := [p,q,r:s_prop]
  [s:st] (p s) \/ (q s) \/ (r s).
Definition s_and := [p,q:s_prop]
  [s:st] (p s) /\ (q s).
Definition s_and3 := [p,q,r:s_prop]
  [s:st] (p s) /\ (q s) /\ (r s).
Definition s_imp := [p,q:s_prop]
  [s:st] (p s) -> (q s).
Definition s_iff := [p,q:s_prop]
  [s:st] (p s) <-> (q s).
Definition s_not := [p:s_prop]
  [s:st] ~(p s).
Definition s_ex := [T:Type][P:T->s_prop] 
  [s:st] (ExT [t:T] ((P t) s)).
Definition s_all := [T:Type][P:T->s_prop] 
  [s:st] (t:T)((P t) s).
Definition s_all_nat := [b:nat][P:nat->s_prop]
  [s:st] ((i:nat)(lt i b)->((P i) s)).

Definition everywhere := [p:s_prop] (s:st)(p s).

(*T* An exception is the operator |everywhere|, which does not produce
a state predicate but a (state-independent) proposition.  *T*)

(*T* In addition to the type |s_prop| of state predicates we introduce
the type |ds_| \linebreak |prop| of dependent state predicates,
i.e. state predicates that are conditional in another state
predicate. More precisely, |(ds_prop r)| for some |r:s_prop| denotes
the type of propositions that do not only depend on a state |s| but
can also assume that |(r s)| holds.  Again the standard logical
oparators are lifed to this new type.  *T*)

Definition ds_prop := [r:s_prop](s:st)(r s)->Prop.

Definition ds_or := 
  [r:s_prop][dp:(ds_prop r)][dq:(ds_prop r)]
  [s:st][prf:(r s)]((dp s prf) \/ (dq s prf)).
Definition ds_and := 
  [r:s_prop][dp:(ds_prop r)][dq:(ds_prop r)]
  [s:st][prf:(r s)]((dp s prf) /\ (dq s prf)).
Definition ds_not := 
  [r:s_prop][dp:(ds_prop r)]
  [s:st][prf:(r s)]~(dp s prf).
Definition ds_true := 
  [r:s_prop]
  [s:st][prf:(r s)]True.
Definition ds_false := 
  [r:s_prop]
  [s:st][prf:(r s)]False.
Definition ds_ex := 
  [r:s_prop][d:(ds_prop r)]
  [s:st](ExT [prf:(r s)] (d s prf)).
Definition ds_all :=
  [r:s_prop][d:(ds_prop r)]
  [s:st](prf:(r s))(d s prf).

(*T* The following operator allows us to cast the proof of a dependent
predicate from |(ds_prop r')| to a proof of |(ds_prop r)| if |r|
implies |r'|. *T*)

Definition ds_cast := [r,r':s_prop]
  [imp:(everywhere (s_imp r r'))][dp:(ds_prop r')]
  [s:st][prf:(r s)](dp s (imp s prf)).

(*BEGIN-H*)

Tactic Definition log_unfold := 
[<:tactic:< 
  (Try Unfold everywhere ;
   Try Unfold s_imp ;
   Try Unfold s_and ;
   Try Unfold s_or ;
   Try Unfold s_not ;
   Try Unfold s_true;
   Try Unfold s_false;
   Try Unfold s_or3;
   Try Unfold s_and3;
   Try Unfold s_iff;
   Try Unfold s_ex;
   Try Unfold s_all;
   Try Unfold s_all_nat;
   Try Unfold ds_prop;
   Try Unfold ds_or;
   Try Unfold ds_and;
   Try Unfold ds_not;
   Try Unfold ds_true;
   Try Unfold ds_false;
   Try Unfold ds_ex;
   Try Unfold ds_all;
   Try Unfold ds_cast)
>>].

Tactic Definition ECI [$H] := 
[<:tactic:< 
(Elim $H; Clear $H; Intros)
>>].

Tactic Definition GCI [$H $I] := 
[<:tactic:< 
(Generalize ($H $I); Clear $H; Intros)
>>].

(*END-H*)

(*T* Theorems about logical operators on propositions |Prop| have
obvious counterparts at the level of state predicates |s_prop| and
dependent state predicates |ds_prop| that we have omitted here. *T*)

(*BEGIN-H*)

Theorem s_imp_p_p : (p:s_prop)
  (everywhere (s_imp p p)).

Unfold everywhere s_imp.
Intros.
Assumption.
Qed.

Theorem s_imp_false : (p:s_prop)
  (everywhere (s_imp s_false p)).

Intros.
Unfold everywhere s_imp s_false.
Intros.
Elim H.
Qed.

Theorem s_imp_true : (p:s_prop)
  (everywhere (s_imp p s_true)).

Intros.
Unfold everywhere s_imp s_true.
Intros.
Exact I.
Qed.

Theorem s_iff_imp : (p,q:s_prop)
  (everywhere (s_iff p q))->(everywhere (s_imp p q)).

Unfold everywhere s_iff s_imp.
Intros.
Specialize (H s).
Intro.
Elim H1.
Intros.
Apply H2.
Assumption.
Qed.

Theorem s_iff_refl : (p:s_prop)
  (everywhere (s_iff p p)).

Unfold everywhere s_iff.
Intros.
Split.
Intros.
Exact H.
Intros.
Exact H.
Qed.

Theorem s_iff_sym : (p,q:s_prop)
  (everywhere (s_iff p q))->(everywhere (s_iff q p)).

Unfold everywhere.
Unfold s_iff.
Intros.
Specialize (H s).
Intro.
Elim H0.
Intros.
Split.
Assumption.
Assumption.
Qed.

Theorem s_iff_trans : (p,q,r:s_prop)
  (everywhere (s_iff p q))->(everywhere (s_iff q r))->
  (everywhere (s_iff p r)).

Unfold everywhere s_iff.
Intros.
Specialize (H s).
Specialize (H0 s).
Intros.
Split.
Elim H1.
Elim H2.
Intros.
Auto.
Elim H1.
Elim H2.
Intros.
Auto.
Qed.

Theorem s_imp_and_l : (p,q:s_prop)
  (everywhere (s_imp (s_and p q) p)).

Unfold everywhere s_imp s_and.
Intros.
Elim H.
Intros.
Assumption.
Qed.

Theorem s_imp_and_r : (p,q:s_prop)
  (everywhere (s_imp (s_and p q) q)).

Unfold everywhere s_imp s_and.
Intros.
Elim H.
Intros.
Assumption.
Qed.

Theorem s_imp_or_l : (p,q:s_prop)
  (everywhere (s_imp p (s_or p q))).

Unfold everywhere s_imp s_or.
Intros.
Left.
Assumption.
Qed.

Theorem s_imp_or_r : (p,q:s_prop)
  (everywhere (s_imp q (s_or p q))).
 
Unfold everywhere s_imp s_or.
Intros.
Right.
Assumption.
Qed.

(*END-H*)

(*T* The axiom |classic| has the following counterpart at the level of
state predicates: *T*)

Theorem s_classic : (p:s_prop)(everywhere (s_or p (s_not p))).

Unfold everywhere s_or s_not.
Unfold everywhere s_or s_not.
Intros.
Apply classic.
Qed.

(*T* Also, logical extensionality can be lifted from propositions to
state predicates, if we assume functional extensionality for
|s_prop|. *T*)

Axiom s_prop_extensionality : (p,q:s_prop)
  ((s : st)(p s)==(q s))->(p==q).

Theorem s_log_extensionality : (p,q:s_prop)
  (everywhere (s_iff p q))->(p==q).

Unfold everywhere.
Unfold s_iff.
Intros.
Apply s_prop_extensionality.
Intros.
Apply log_extensionality.
Apply H.
Qed.