450 lines
12 KiB
Coq
450 lines
12 KiB
Coq
(* https://www.labri.fr/perso/casteran/CoqArt/chapter13.pdf *)
|
||
(* https://github.com/coq-contribs/ltl *)
|
||
|
||
|
||
(* Require Import Streams. *)
|
||
|
||
(* Lemma unfoldStream {A: Type}: forall s: Stream A, *)
|
||
(* s = match s with *)
|
||
(* | Cons x ss => Cons x ss *)
|
||
(* end. *)
|
||
(* Proof. *)
|
||
(* intros s. *)
|
||
(* now destruct s. *)
|
||
(* Qed. *)
|
||
|
||
(* Require Import ssreflect. *)
|
||
|
||
(* Goal *)
|
||
(* const 3 = Cons 3 (const 3). *)
|
||
(* Proof. *)
|
||
(* rewrite {1}(unfoldStream (const 3)). *)
|
||
(* rewrite //=. *)
|
||
(* Qed. *)
|
||
|
||
(* Goal *)
|
||
(* const 3 = Cons 3 (const 3). *)
|
||
(* Proof. *)
|
||
(* rewrite (unfoldStream (const 3)). *)
|
||
(* simpl. *)
|
||
(* unfold const. *)
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
(* https://www.labri.fr/perso/casteran/CoqArt/chapter13.pdf *)
|
||
Require Import ssreflect.
|
||
|
||
(* Module LtlNotations. *)
|
||
(* Declare Scope ltl_scope. *)
|
||
(* Delimit Scope ltl_scope with ltl. *)
|
||
|
||
(* Reserved Notation "⊤". *)
|
||
(* Reserved Notation "⊥". *)
|
||
|
||
(* Reserved Notation "'↑' p" (at level 15). *)
|
||
(* Reserved Notation "'¬' p" := (not p) (at level 20): ltl_scope. *)
|
||
(* Reserved Notation "'X' p" := (next p) (at level 25, right associativity): ltl_scope. *)
|
||
(* Reserved Infix "∨" := or (at level 35, right associativity): ltl_scope. *)
|
||
(* Reserved Infix "U" := until (at level 45, right associativity): ltl_scope. *)
|
||
|
||
(* Infix "∧" := and (at level 30, right associativity): ltl_scope. *)
|
||
(* Infix "→" := impl (at level 25, right associativity): ltl_scope. *)
|
||
(* Notation "'◇' p" := (eventually p) (at level 60, right associativity): ltl_scope. *)
|
||
(* Notation "'□' p" := (always p) (at level 60, right associativity): ltl_scope. *)
|
||
(* End LtlNotations. *)
|
||
|
||
|
||
Section streams.
|
||
Context {A: Type}.
|
||
|
||
(* Finite and infinite words possible *)
|
||
CoInductive stream {A: Type}: Type :=
|
||
| SNil: stream
|
||
| SCons: A -> stream -> stream.
|
||
#[global] Arguments stream: clear implicits.
|
||
|
||
(* Constant stream *)
|
||
CoFixpoint const (a:A): stream A := SCons a (const a).
|
||
|
||
(* Concatenate two streams *)
|
||
CoFixpoint sapp (a b: stream A): stream A :=
|
||
match a with
|
||
| SNil => b
|
||
| SCons x a' => SCons x (sapp a' b)
|
||
end.
|
||
|
||
(* An inductive predicate. Keeps consuming. *)
|
||
Inductive isFinite {A: Type}: stream A -> Prop :=
|
||
| IsFinDone: isFinite SNil
|
||
| IsFinMore: forall (s: stream A) (a:A),
|
||
isFinite s -> isFinite (SCons a s).
|
||
|
||
(* A coinductive predicate. Keeps producing. *)
|
||
CoInductive isInfinite {A: Type}: stream A -> Prop :=
|
||
| IsInfin: forall (s: stream A) (a:A),
|
||
isInfinite s -> isInfinite (SCons a s).
|
||
End streams.
|
||
|
||
Module Ltl.
|
||
Section Foo.
|
||
Context {A: Type}.
|
||
|
||
Definition sProp: Type := stream A -> Prop.
|
||
|
||
Inductive atom (P: A -> Prop): sProp :=
|
||
| Atom: forall (a:A) (s: stream A),
|
||
P a -> atom P (SCons a s).
|
||
|
||
Inductive next (p: sProp): sProp :=
|
||
| Next: forall (a:A) (s: stream A),
|
||
p s -> next p (SCons a s).
|
||
|
||
(* Strict eventually *)
|
||
(* Inductive eventually (p: sProp): sProp := *)
|
||
(* | FDone: forall (a: A) (s: stream A), *)
|
||
(* p (SCons a s) -> eventually p (SCons a s) *)
|
||
(* | FMore: forall (a: A) (s: stream A), *)
|
||
(* eventually p s -> eventually p (SCons a s). *)
|
||
|
||
(* CoInductive always (p: sProp): sProp := *)
|
||
(* | Always: forall (s: stream A) (a: A), *)
|
||
(* always p s -> always p (SCons a s). *)
|
||
|
||
CoInductive until (p q: sProp): sProp :=
|
||
| UDone: forall (s: stream A) (a: A),
|
||
q s -> until p q (SCons a s)
|
||
| UMore: forall (s: stream A) (a: A),
|
||
p s -> until p q s -> until p q (SCons a s).
|
||
|
||
Definition not (p: sProp): sProp := fun s => not (p s).
|
||
Definition or (p q: sProp): sProp := fun s => (p s) \/ (q s).
|
||
|
||
Definition and (p q: sProp): sProp := or (not p) (not q).
|
||
Definition impl (p q: sProp): sProp := or (not p) q.
|
||
Definition eventually (p: sProp): sProp := until (fun _ => True) p.
|
||
Definition always (p: sProp): sProp := until p (fun _ => False).
|
||
End Foo.
|
||
End Ltl.
|
||
|
||
|
||
Section streamLemmas.
|
||
Context {A: Type}.
|
||
|
||
Lemma unfoldStream: forall s: stream A,
|
||
s = match s with
|
||
| SNil => SNil
|
||
| SCons x ss => SCons x ss
|
||
end.
|
||
Proof. by move => s; case: s. Qed.
|
||
|
||
Lemma sappSNil: forall (s: stream A),
|
||
sapp SNil s = s.
|
||
Proof.
|
||
move => s.
|
||
rewrite (unfoldStream (sapp SNil s)).
|
||
by case: s.
|
||
Qed.
|
||
End streamLemmas.
|
||
|
||
Section Lemmas.
|
||
Context (A: Type).
|
||
Import Ltl.
|
||
|
||
Definition satisfies (P: stream A -> Prop) (s: stream A): Prop := P s.
|
||
|
||
Definition XdistributiveOr (p q: sProp): forall s: stream A,
|
||
(next (or p q)) s ->
|
||
(next p) s \/ (next q) s.
|
||
Proof.
|
||
move => s H.
|
||
elim: H.
|
||
move => a s'.
|
||
rewrite /or => H.
|
||
case: H.
|
||
- move => H; left; by apply Next.
|
||
- move => H; right; by apply Next.
|
||
Qed.
|
||
|
||
Lemma nextStream: forall (p: sProp) (s: stream A) (a: A),
|
||
next p (SCons a s) -> p s.
|
||
Proof.
|
||
move => p s a H.
|
||
case: H.
|
||
move => _ s'.
|
||
Abort.
|
||
|
||
|
||
Definition XdistributiveU (p q: sProp): forall s: stream A,
|
||
(next (until p q)) s ->
|
||
(until (next p) (next q)) s.
|
||
Proof.
|
||
move => s H.
|
||
case: s H.
|
||
move => H; first by inversion H.
|
||
move => a s.
|
||
Abort.
|
||
|
||
|
||
(* Definition UdistributiveOr (p q r: sProp): forall s: stream A, *)
|
||
(* (until (or p q)) r s -> *)
|
||
(* (until p) s \/ (until q) s. *)
|
||
(* Proof. *)
|
||
|
||
(* Definition GdistributiveOr (p q: sProp): forall s: stream A, *)
|
||
(* (always (or p q)) s -> *)
|
||
(* (always p) s \/ (always q) s. *)
|
||
(* Proof. *)
|
||
(* rewrite /always. *)
|
||
(* move => s H. *)
|
||
(* case: H; first by move => s' a. *)
|
||
(* move => s' a H. *)
|
||
(* rewrite /or. *)
|
||
(* move => HH. *)
|
||
(* case: HH; first by move => s'' a'. *)
|
||
(* split. *)
|
||
|
||
|
||
Theorem nextRepeat: forall (a b: A),
|
||
(next (atom (fun x => x = b))) (SCons a (const b)).
|
||
Proof.
|
||
move => a b.
|
||
apply Next.
|
||
rewrite (unfoldStream (const b)).
|
||
rewrite /const.
|
||
by apply Atom.
|
||
Qed.
|
||
|
||
Theorem prefixEventually: forall (pre post: stream A) (p: sProp),
|
||
isFinite pre ->
|
||
satisfies (eventually p) post ->
|
||
satisfies (eventually p) (sapp pre post).
|
||
Proof.
|
||
move => pre post p HpreFin.
|
||
rewrite /satisfies.
|
||
case: HpreFin.
|
||
- move => H.
|
||
case: H.
|
||
+ move => a s.
|
||
rewrite sappSNil.
|
||
apply FDone.
|
||
+ move => a s.
|
||
rewrite sappSNil.
|
||
apply FMore.
|
||
- move => s a HsFin.
|
||
+ case: HsFin.
|
||
*
|
||
Abort.
|
||
|
||
Theorem alwaysInfinite: forall (s: stream A) (p: sProp),
|
||
satisfies (always p) s -> isInfinite s.
|
||
Proof.
|
||
move => s p.
|
||
rewrite /satisfies.
|
||
move => H.
|
||
case: H.
|
||
move => s' a H.
|
||
apply IsInfin.
|
||
cofix HH.
|
||
case: HH.
|
||
move => s2 a2 H2.
|
||
apply IsInfin.
|
||
apply H2.
|
||
Fail Qed.
|
||
Abort.
|
||
End Lemmas.
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
|
||
(* https://github.com/coq-contribs/ltl *)
|
||
Require Import Streams.
|
||
Require Import ssreflect.
|
||
|
||
Module Ltl.
|
||
Context {A: Type}.
|
||
|
||
Definition sProp: Type := Stream A -> Prop.
|
||
|
||
(* Fundamental operators *)
|
||
|
||
CoInductive until (p q: sProp): sProp :=
|
||
| UMore: forall s: Stream A,
|
||
q s -> until p q s
|
||
| UDone: forall s: Stream A,
|
||
p s -> until p q (tl s) -> until p q s.
|
||
|
||
Definition atom (p: A -> Prop): sProp := fun s => p (hd s).
|
||
Definition not (p: sProp): sProp := fun s => not (p s).
|
||
Definition next (p: sProp): sProp := fun s => p (tl s).
|
||
Definition or (p q: sProp): sProp := fun s => (p s) \/ (q s).
|
||
|
||
|
||
(* Derived operators *)
|
||
Definition and (p q: sProp): sProp := or (not p) (not q).
|
||
Definition impl (p q: sProp): sProp := or (not p) q.
|
||
Definition eventually (p: sProp): sProp := until (fun _ => True) p.
|
||
Definition always (p: sProp): sProp := until p (fun _ => False).
|
||
(* Definition and (p q: sProp): sProp := ¬p ∨ ¬q. *)
|
||
(* Definition impl (p q: sProp): sProp := ¬p ∨ q. *)
|
||
(* Definition eventually (p: sProp): sProp := ⊤ U p. *)
|
||
(* Definition always (p: sProp): sProp := p U ⊥. *)
|
||
End Ltl.
|
||
#[global] Arguments sProp: clear implicits.
|
||
|
||
Module LtlNotations.
|
||
Import Ltl.
|
||
Declare Scope ltl_scope.
|
||
Delimit Scope ltl_scope with ltl.
|
||
|
||
Notation "⊤" := (fun _ => True): ltl_scope.
|
||
Notation "⊥" := (fun _ => False): ltl_scope.
|
||
|
||
Notation "'↑' p" := (atom p) (at level 15): ltl_scope.
|
||
Notation "'¬' p" := (not p) (at level 20): ltl_scope.
|
||
Notation "'X' p" := (next p) (at level 25, right associativity): ltl_scope.
|
||
Infix "∨" := or (at level 35, right associativity): ltl_scope.
|
||
Infix "U" := until (at level 45, right associativity): ltl_scope.
|
||
|
||
Infix "∧" := and (at level 30, right associativity): ltl_scope.
|
||
Infix "→" := impl (at level 25, right associativity): ltl_scope.
|
||
Notation "'◇' p" := (eventually p) (at level 60, right associativity): ltl_scope.
|
||
Notation "'□' p" := (always p) (at level 60, right associativity): ltl_scope.
|
||
End LtlNotations.
|
||
|
||
Section lemmas.
|
||
Import LtlNotations.
|
||
Open Scope ltl_scope.
|
||
|
||
Context (A: Type).
|
||
Definition left_distributive1 (a b: sProp A): forall s: Stream A,
|
||
(X (a ∨ b)) s ->
|
||
(X a) s \/ (X b) s.
|
||
Proof.
|
||
move => s H.
|
||
Abort.
|
||
|
||
End lemmas.
|
||
|
||
|
||
|
||
|
||
(* Module Syn. *)
|
||
(* (1* Inductive t {A: Type}: Stream A -> Type := *1) *)
|
||
(* (1* | Atom: forall s:Stream A, *1) *)
|
||
(* (1* Prop -> t s *1) *)
|
||
(* (1* | Next: forall (s:Stream A) (a:A), *1) *)
|
||
(* (1* t s -> t (Streams.Cons a s) *1) *)
|
||
(* (1* | Not: forall s:Stream A, *1) *)
|
||
(* (1* t s -> t s *1) *)
|
||
(* (1* | Or: forall s:Stream A, *1) *)
|
||
(* (1* t s -> t s -> t s *1) *)
|
||
(* (1* | Until: t -> t -> t. *1) *)
|
||
|
||
(* Inductive t {A: Type}: Type := *)
|
||
(* | Atom: (A -> Prop) -> t *)
|
||
(* | Next: t -> t *)
|
||
(* | Not: t -> t *)
|
||
(* | Or: t -> t -> t *)
|
||
(* | Until: t -> t -> t. *)
|
||
(* #[global] Arguments t: clear implicits. *)
|
||
(* End Syn. *)
|
||
|
||
(* Module Sem. *)
|
||
(* Import Syn. *)
|
||
(* Context (A: Type). *)
|
||
|
||
(* Definition sProp: Type := Stream A -> Prop. *)
|
||
|
||
(* CoInductive until (p q: sProp): sProp := *)
|
||
(* | UMore: forall s: Stream A, *)
|
||
(* q s -> until p q s *)
|
||
(* | UDone: forall s: Stream A, *)
|
||
(* p s -> until p q (tl s) -> until p q s. *)
|
||
|
||
(* Definition atom (p: A -> Prop): sProp := fun s => p (hd s). *)
|
||
(* Definition next (p: sProp): sProp := fun s => p (tl s). *)
|
||
(* Definition not (p: sProp): sProp := fun s => not (p s). *)
|
||
(* Definition or (p q: sProp): sProp := fun s => (p s) \/ (q s). *)
|
||
|
||
(* Fixpoint denote (p: Syn.t A): sProp := *)
|
||
(* match p with *)
|
||
(* | Atom p => atom p *)
|
||
(* | Next p => next (denote p) *)
|
||
(* | Not p => not (denote p) *)
|
||
(* | Or p q => or (denote p) (denote q) *)
|
||
(* | Until p q => until (denote p) (denote q) *)
|
||
(* end. *)
|
||
|
||
(* (1* CoInductive t {A: Type}: Syn.t A -> Prop := *1) *)
|
||
(* (1* | Atom (p: Prop): t (Syn.Atom p) *1) *)
|
||
(* (1* | Next (p: Syn.t A): t (Syn.Next p) *1) *)
|
||
(* (1* | Not (p: Syn.t A): t (Syn.Not p) *1) *)
|
||
(* (1* | Or (p q: Syn.t A): t (Syn.Or p q) *1) *)
|
||
(* (1* | UDone (p q: Syn.t A): t (Syn.Until p q) *1) *)
|
||
(* (1* | UMore (p q: Syn.t A): t (Syn.Until p q). *1) *)
|
||
(* (1* (2* #[global] Arguments t: clear implicits. *2) *1) *)
|
||
|
||
(* (1* Check @tl. *1) *)
|
||
(* (1* CoFixpoint foo {A: Type} (s: Stream A): forall (f: Syn.t A), t f. *1) *)
|
||
(* (1* refine (fun f => *1) *)
|
||
(* (1* match f with *1) *)
|
||
(* (1* | Syn.Atom p => Atom p *1) *)
|
||
(* (1* | Syn.Next p => _ *1) *)
|
||
(* (1* | Syn.Not p => _ *1) *)
|
||
(* (1* | Syn.Or p q => _ *1) *)
|
||
(* (1* | Syn.Until p q => _ *1) *)
|
||
(* (1* end). *1) *)
|
||
(* (1* - Check foo _ (tl s) p. *1) *)
|
||
|
||
(* (1* (2* w ⊨ p : Prop *2) *1) *)
|
||
|
||
(* (1* (2* Fixpoint foo {A: Type} (s: Stream A) (f: Syn.t A): Prop := *2) *1) *)
|
||
(* (1* (2* match f with *2) *1) *)
|
||
(* (1* (2* | Atom p => p *2) *1) *)
|
||
(* (1* (2* | Next p => foo (tl s) p *2) *1) *)
|
||
(* (1* (2* | Not p => not (foo s p) *2) *1) *)
|
||
(* (1* (2* | Or p q => (foo s p) \/ (foo s q) *2) *1) *)
|
||
(* (1* (2* | Until p q => True *2) *1) *)
|
||
(* (1* (2* end. *2) *1) *)
|
||
|
||
|
||
|
||
|
||
(* End Sem. *)
|