add a bunch of new stuff
This commit is contained in:
parent
9a69fea179
commit
25dc1bf9ad
|
|
@ -0,0 +1,86 @@
|
|||
{-
|
||||
Tolerating monitor
|
||||
|
||||
Examine if sum of values in two input streams exceed a limit.
|
||||
If limit is exceeded, see if it comes back to confirmance with a fixed
|
||||
number of cycles and if it doesn't give False. Else keep giving True.
|
||||
-}
|
||||
|
||||
import Clash.Prelude
|
||||
import Clash.Explicit.Testbench -- For simulation and testing
|
||||
|
||||
-- | Monitor state
|
||||
data State
|
||||
= Good -- ^ No intolerable violation
|
||||
| Bad -- ^ Violation beyond tolerance
|
||||
| Tolerating Word -- ^ Tolerating violation
|
||||
deriving (Generic, NFDataX)
|
||||
|
||||
monTf
|
||||
:: (Num a, Ord a)
|
||||
=> Word -- ^ Tolerance limit (inclusive)
|
||||
-> (a, a) -- ^ Lowest and highest allowed values
|
||||
-> State -- ^ Current state
|
||||
-> (a, a) -- ^ Input values
|
||||
-> (State, Bool) -- ^ Next state and output
|
||||
monTf limit (low, high) s (a, b) = case s of
|
||||
Good ->
|
||||
if outsideLimits res then
|
||||
(Tolerating 1, True)
|
||||
else
|
||||
(Good, True)
|
||||
Bad -> (Bad, False)
|
||||
Tolerating failCount ->
|
||||
if outsideLimits res then
|
||||
--if failCount > limit then -- Spec mismatch. Tolerance is inclusive
|
||||
if failCount == limit then
|
||||
(Bad, False)
|
||||
else
|
||||
(Tolerating (failCount+1), True)
|
||||
else
|
||||
(Good, True)
|
||||
where
|
||||
res = a + b
|
||||
outsideLimits val = val < low && val > high
|
||||
|
||||
mon
|
||||
:: SystemClockResetEnable
|
||||
=> Signal System (Signed 8, Signed 8)
|
||||
-> Signal System Bool
|
||||
mon = mealy tf Good
|
||||
where
|
||||
tf = monTf 2 (10, 20)
|
||||
|
||||
topEntity
|
||||
:: Clock System
|
||||
-> Reset System
|
||||
-> Enable System
|
||||
-> Signal System (Signed 8, Signed 8)
|
||||
-> Signal System Bool
|
||||
topEntity = exposeClockResetEnable mon
|
||||
|
||||
|
||||
testBench :: Signal System Bool
|
||||
testBench = done
|
||||
where
|
||||
testInput = stimuliGenerator clk rst
|
||||
$(listToVecTH [(10, 15) :: (Signed 8, Signed 8),
|
||||
(25, 12),
|
||||
(23, 30),
|
||||
(1, 4)])
|
||||
expectedOutput = outputVerifier' clk rst
|
||||
$(listToVecTH [True,
|
||||
True,
|
||||
False,
|
||||
False])
|
||||
done = expectedOutput (topEntity clk rst (enableGen) testInput)
|
||||
clk = tbSystemClockGen (not <$> done)
|
||||
rst = systemResetGen
|
||||
|
||||
{-
|
||||
λ> import qualified Data.List
|
||||
λ> Data.List.take 5 $ sample testBench
|
||||
[False,False,False,False,False]
|
||||
-}
|
||||
|
||||
--Data.List.take 5 $ sample $ exposeClockResetEnable mon
|
||||
|
|
@ -0,0 +1,102 @@
|
|||
-- Inspired by https://github.com/coq-community/reglang/blob/master/theories/nfa.v
|
||||
|
||||
import Clash.Prelude
|
||||
import qualified Prelude
|
||||
import qualified Data.List
|
||||
|
||||
data Re a
|
||||
= Eps
|
||||
| Char (a -> Bool)
|
||||
| Cat (Re a) (Re a)
|
||||
| Alt (Re a) (Re a)
|
||||
| Star (Re a)
|
||||
|
||||
-- ============================================================
|
||||
|
||||
lshift :: [a] -> [Either a b]
|
||||
lshift = Prelude.map Left
|
||||
|
||||
rshift :: [b] -> [Either a b]
|
||||
rshift = Prelude.map Right
|
||||
|
||||
-------------------------------------------------------------
|
||||
|
||||
data Nfa a = Nfa {
|
||||
start :: [a]
|
||||
, final :: [a]
|
||||
, tfun :: a -> Maybe Char -> a -> Bool
|
||||
}
|
||||
|
||||
-------------------------------------------------------------
|
||||
|
||||
eps :: Nfa ()
|
||||
eps = Nfa {
|
||||
start = [()]
|
||||
, final = [()]
|
||||
, tfun = \ s c d -> case (c, s, d) of
|
||||
(Nothing, (), ()) -> True
|
||||
otherwise -> False
|
||||
-- () to () possible but not by consuming `c'
|
||||
}
|
||||
|
||||
char :: (Char -> Bool) -> Nfa Bool
|
||||
char f = Nfa {
|
||||
start = [False]
|
||||
, final = [True]
|
||||
, tfun = \ s c d -> case (c, s, d) of
|
||||
(Just c, False, True) -> f c
|
||||
(Nothing, False, False) -> True
|
||||
(Nothing, True, True) -> True
|
||||
otherwise -> False
|
||||
}
|
||||
|
||||
cat :: (Eq a, Eq b) => Nfa a -> Nfa b -> Nfa (Either a b)
|
||||
cat a1 a2 = Nfa {
|
||||
start = lshift (start a1)
|
||||
, final = rshift (final a2)
|
||||
, tfun = \ s c d -> case (c, s, d) of
|
||||
(Just c', Left s, Left d) -> (tfun a1) s c d
|
||||
(Just c', Right s, Right d) -> (tfun a2) s c d
|
||||
|
||||
-- The epsilon transition
|
||||
(Nothing, Left s, Right d) ->
|
||||
if Prelude.elem s (final a1) && Prelude.elem d (start a2) then True
|
||||
else False
|
||||
otherwise -> False
|
||||
}
|
||||
|
||||
-- if ∃st ∈ (start a1) and st ∈ (final a1) then
|
||||
-- (start a1) ++
|
||||
-- else
|
||||
-- start a1
|
||||
|
||||
alt :: Nfa a -> Nfa b -> Nfa (Either a b)
|
||||
alt a1 a2 = Nfa {
|
||||
start = (Data.List.++) (lshift (start a1)) (rshift (start a2))
|
||||
, final = (Data.List.++) (lshift (final a1)) (rshift (final a2))
|
||||
, tfun = \ s c d -> case (c, s, d) of
|
||||
(_, Left s, Left d) -> (tfun a1) s c d
|
||||
(_, Right s, Right d) -> (tfun a2) s c d
|
||||
otherwise -> False
|
||||
}
|
||||
|
||||
star :: Eq a => Nfa a -> Nfa a
|
||||
star au = Nfa {
|
||||
start = start au
|
||||
, final = (Data.List.++) (start au) (final au)
|
||||
, tfun = \ s c d -> case (c, s, d) of
|
||||
(Nothing, _, _) ->
|
||||
if Prelude.elem s (final au) && Prelude.elem d (start au) then True
|
||||
else False
|
||||
otherwise -> (tfun au) s c d
|
||||
}
|
||||
|
||||
-------------------------------------------------------------
|
||||
|
||||
-- re2nfa :: Re a -> Nfa st
|
||||
-- re2nfa r = case r of
|
||||
-- Eps -> eps
|
||||
-- Char f -> char f
|
||||
-- Cat r1 r2 -> cat (re2nfa r1) (re2nfa r2)
|
||||
-- Alt r1 r2 -> alt (re2nfa r1) (re2nfa r2)
|
||||
-- Star rr -> star (re2nfa rr)
|
||||
|
|
@ -0,0 +1,105 @@
|
|||
Require Import Extraction.
|
||||
Extraction Language Haskell.
|
||||
|
||||
Require Import ExtrHaskellBasic.
|
||||
Require Import ExtrHaskellNatInt.
|
||||
|
||||
|
||||
Inductive state: Type :=
|
||||
| Good | Bad
|
||||
| Tolerating: nat -> state.
|
||||
|
||||
Definition gtb (a b: nat): bool := Nat.ltb b a.
|
||||
|
||||
(* Goal *)
|
||||
(* forall (a b:nat), Nat.ltb a b = gtb a b. *)
|
||||
(* Proof. *)
|
||||
(* intros a b. *)
|
||||
(* induction a. *)
|
||||
(* - induction b. *)
|
||||
(* + trivial. *)
|
||||
(* + simpl. *)
|
||||
|
||||
(*
|
||||
p = (a+b) <= high && low >= (a+b)
|
||||
~p;~p;~p |-> o=False
|
||||
|
||||
~p; X ~p; X X ~p ??????
|
||||
*)
|
||||
Definition monTf (limit: nat) (bounds: nat * nat) (st: state) (ab: nat * nat): state * bool :=
|
||||
let a := fst ab in
|
||||
let b := snd ab in
|
||||
let low := fst bounds in
|
||||
let high := snd bounds in
|
||||
let res := a + b in
|
||||
let outsideLimits :=
|
||||
orb (Nat.ltb res low) (gtb res high) in
|
||||
match st with
|
||||
| Good =>
|
||||
if outsideLimits then (Tolerating 1, true)
|
||||
else (Good, true)
|
||||
| Bad => (Bad, false)
|
||||
| Tolerating failCount =>
|
||||
if outsideLimits then
|
||||
(*if failCount > limit then -- Spec mismatch. Tolerance is inclusive*)
|
||||
if Nat.eqb failCount limit then (Bad, false)
|
||||
else (Tolerating (S failCount), true)
|
||||
else (Good, true)
|
||||
end.
|
||||
|
||||
Extract Inductive nat => "Int" [ "0" "succ" ]
|
||||
"(\fO fS n -> if n == 0 then fO () else fS (n - 1))".
|
||||
|
||||
(** ExtrHaskBasic **)
|
||||
|
||||
Extract Inductive bool => "Bool" [ "True" "False" ].
|
||||
Extract Inductive option => "Maybe" [ "Just" "Nothing" ].
|
||||
Extract Inductive unit => "()" [ "()" ].
|
||||
Extract Inductive list => "([])" [ "([])" "(:)" ].
|
||||
Extract Inductive prod => "(,)" [ "(,)" ].
|
||||
|
||||
Extract Inductive sumbool => "Bool" [ "True" "False" ].
|
||||
Extract Inductive sumor => "Maybe" [ "Just" "Nothing" ].
|
||||
Extract Inductive sum => "Either" [ "Left" "Right" ].
|
||||
|
||||
Extract Inlined Constant andb => "(&&)".
|
||||
Extract Inlined Constant orb => "(||)".
|
||||
Extract Inlined Constant negb => "not".
|
||||
|
||||
(** ExtrHaskellNatNum *)
|
||||
|
||||
Extract Inlined Constant Nat.add => "(+)".
|
||||
Extract Inlined Constant Nat.mul => "(*)".
|
||||
Extract Inlined Constant Nat.max => "max".
|
||||
Extract Inlined Constant Nat.min => "min".
|
||||
Extract Inlined Constant Init.Nat.add => "(+)".
|
||||
Extract Inlined Constant Init.Nat.mul => "(*)".
|
||||
Extract Inlined Constant Init.Nat.max => "max".
|
||||
Extract Inlined Constant Init.Nat.min => "min".
|
||||
Extract Inlined Constant Compare_dec.lt_dec => "(<)".
|
||||
Extract Inlined Constant Compare_dec.leb => "(<=)".
|
||||
Extract Inlined Constant Compare_dec.le_lt_dec => "(<=)".
|
||||
Extract Inlined Constant Nat.eqb => "(==)".
|
||||
Extract Inlined Constant EqNat.eq_nat_decide => "(==)".
|
||||
Extract Inlined Constant Peano_dec.eq_nat_dec => "(==)".
|
||||
|
||||
Extract Constant Nat.pred => "(\n -> max 0 (pred n))".
|
||||
Extract Constant Nat.sub => "(\n m -> max 0 (n - m))".
|
||||
Extract Constant Init.Nat.pred => "(\n -> max 0 (pred n))".
|
||||
Extract Constant Init.Nat.sub => "(\n m -> max 0 (n - m))".
|
||||
|
||||
Extract Constant Nat.div => "(\n m -> if m == 0 then 0 else div n m)".
|
||||
Extract Constant Nat.modulo => "(\n m -> if m == 0 then n else mod n m)".
|
||||
Extract Constant Init.Nat.div => "(\n m -> if m == 0 then 0 else div n m)".
|
||||
Extract Constant Init.Nat.modulo => "(\n m -> if m == 0 then n else mod n m)".
|
||||
|
||||
(** Own *)
|
||||
|
||||
Extract Inlined Constant Nat.eqb => "(==)".
|
||||
Extract Inlined Constant Nat.leb => "(<=)".
|
||||
Extract Inlined Constant Nat.ltb => "(<)".
|
||||
Extract Inlined Constant gtb => "(>)".
|
||||
Extract Inlined Constant fst => "fst".
|
||||
Extract Inlined Constant snd => "snd".
|
||||
|
||||
Recursive Extraction monTf.
|
||||
|
|
@ -26,7 +26,7 @@ Infix "⇒" := Arrow (at level 25, right associativity): ty_scope.
|
|||
Inductive ref {A: Type}: A -> list A -> Type :=
|
||||
| Here: forall (a:A) (ls:list A),
|
||||
ref a (a::ls)
|
||||
| Further: forall (a x: A) (ls: list A),
|
||||
| Further: forall {a: A} {ls: list A} (x: A),
|
||||
ref a ls -> ref a (x::ls).
|
||||
|
||||
(* Theorem refListNonNil: forall {A: Type} (a:A) (ls: list A), *)
|
||||
|
|
@ -38,8 +38,9 @@ Inductive ref {A: Type}: A -> list A -> Type :=
|
|||
|
||||
Inductive env: list type -> Type :=
|
||||
| ENil: env []
|
||||
| ECons: forall (τs: list type) (τ: type),
|
||||
| ECons: forall {τs: list type} {τ: type},
|
||||
typeDe τ -> env τs -> env (τ::τs).
|
||||
(* ⣤ ‼ *)
|
||||
|
||||
(* Fixpoint lookup {t: type} {ts: list type} (en: env ts): ref t ts -> typeDe t. refine ( *)
|
||||
(* match en with *)
|
||||
|
|
@ -57,8 +58,8 @@ Inductive env: list type -> Type :=
|
|||
(* https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Lookup.20env.20with.20dependent.20types *)
|
||||
Equations lookupEnv {τ: type} {τs: list type}
|
||||
(en: env τs) (rf: ref τ τs): typeDe τ :=
|
||||
lookupEnv (ECons _ _ v _) (Here _ _) := v ;
|
||||
lookupEnv (ECons _ _ _ en') (Further _ _ _ rf') := lookupEnv en' rf'.
|
||||
lookupEnv (ECons v _) (Here _ _) := v ;
|
||||
lookupEnv (ECons _ en') (Further _ rf') := lookupEnv en' rf'.
|
||||
|
||||
(* Print lookupEnv. *)
|
||||
|
||||
|
|
@ -93,7 +94,7 @@ Module LC.
|
|||
| App _ _ _ tm1 tm2 =>
|
||||
fun en => (termDe tm1 en) (termDe tm2 en)
|
||||
| Abs _ _ _ f =>
|
||||
fun en v => termDe f (ECons _ _ v en)
|
||||
fun en v => termDe f (ECons v en)
|
||||
end.
|
||||
|
||||
(* This would've worked too. *)
|
||||
|
|
@ -105,30 +106,89 @@ Module LC.
|
|||
(* Print termDe. *)
|
||||
End LC.
|
||||
|
||||
Compute typeDe (Arrow BVal (Arrow NVal BVal)).
|
||||
Compute typeDe (Arrow (Arrow BVal NVal) BVal).
|
||||
|
||||
Module SKI.
|
||||
Open Scope ty_scope.
|
||||
|
||||
Inductive term: forall (τ: type), env τs -> typeDe τ -> Type :=
|
||||
| I: forall X: type,
|
||||
term (X ⇒ X)
|
||||
(fun x: typeDe X => x)
|
||||
| K: forall X Y: type,
|
||||
term (X ⇒ Y ⇒ X)
|
||||
(fun (x:typeDe X) (y: typeDe Y) => x)
|
||||
| S: forall X Y Z: type,
|
||||
term ((X ⇒ Y ⇒ Z) ⇒
|
||||
(X ⇒ Y) ⇒
|
||||
(X ⇒ Z))
|
||||
(fun (f: typeDe (X ⇒ Y ⇒ Z))
|
||||
(g: typeDe (X ⇒ Y))
|
||||
(x: typeDe X) => (f x) (g x))
|
||||
| App: forall (X Y: type) (f: typeDe (X ⇒ Y)) (x: typeDe X),
|
||||
term (X ⇒ Y) f -> term X x -> term Y (f x)
|
||||
| Var: forall (X Y: type) (f: typeDe (X ⇒ Y)),
|
||||
term (X ⇒ Y) f -> term X x -> term (X ⇒ Y) f.
|
||||
Inductive term {τs: list type}: forall (τ: type),
|
||||
(env τs -> typeDe τ) -> Type :=
|
||||
| I: forall (τ: type),
|
||||
term (τ ⇒ τ)
|
||||
(fun (en: env τs) (x: ⟦τ⟧) => x)
|
||||
| K: forall (τ1 τ2: type),
|
||||
term (τ1 ⇒ τ2 ⇒ τ1)
|
||||
(fun (en: env τs) (x1: ⟦τ1⟧) (x2: ⟦τ2⟧) => x1)
|
||||
| S: forall (τa τb τx: type),
|
||||
term ((τx ⇒ τa ⇒ τb) ⇒ (τx ⇒ τa) ⇒ τx ⇒ τb)
|
||||
(fun (en: env τs)
|
||||
(f: ⟦τx ⇒ τa ⇒ τb⟧) (g: ⟦τx ⇒ τa⟧) (x: ⟦τx⟧) =>
|
||||
(f x) (g x))
|
||||
| Var: forall (τ: type)
|
||||
(rf: ref τ τs),
|
||||
term τ (fun (en: env τs) => lookupEnv en rf)
|
||||
| App: forall {τa τb: type} {f: ⟦τa ⇒ τb⟧} {b: ⟦τb⟧},
|
||||
term (τa ⇒ τb) (fun en: env τs => f) ->
|
||||
term τb (fun en: env τs => b) ->
|
||||
term ((τa ⇒ τb) ⇒ τa ⇒ τb)
|
||||
(fun (en: env τs) (f: ⟦τa ⇒ τb⟧) (a: ⟦τa⟧) => f a).
|
||||
#[global] Arguments term: clear implicits.
|
||||
|
||||
(* Equations abs {σ τ: type} {τs: list type} {f: env (σ::τs) -> typeDe τ} *)
|
||||
(* (t: term (σ::τs) τ f) *)
|
||||
(* : term τs (σ ⇒ τ) (fun (en: env τs) => (fun (x: ⟦σ⟧) => f (ECons x en))) := *)
|
||||
(* abs (I _) => App (K _ _) (I _). *)
|
||||
(* abs (K _ _ _) => _; *)
|
||||
(* abs (S _ _ _ _) => _; *)
|
||||
(* abs (Var _ _ rf) => _; *)
|
||||
(* abs (App _ _) => _. *)
|
||||
|
||||
Fixpoint abs {σ τ: type} {τs: list type} {f: env (σ::τs) -> typeDe τ}
|
||||
(tm: term (σ::τs) τ f)
|
||||
: term τs (σ ⇒ τ) (fun (en: env τs) => (fun (x: ⟦σ⟧) => f (ECons x en))).
|
||||
refine (
|
||||
match tm with
|
||||
| I ty => _
|
||||
| K _ _ => _
|
||||
| S _ _ _ => _
|
||||
| Var _ rf => _
|
||||
| App _ _ => _
|
||||
end).
|
||||
- Check (App (K _ _) (I ty)).
|
||||
Check (@App τs _ _ _ _ (K τ σ) (I _)).
|
||||
Check (App (K _ σ) (I ty)).
|
||||
shelve.
|
||||
-
|
||||
refine (App (K _ _) (I _)).
|
||||
|
||||
|
||||
(* Inductive term: forall (τs: list type) (τ: type), env τs -> typeDe τ -> Type := *)
|
||||
(* | I: forall (τs: list type) (τ: type) (en: env τs), *)
|
||||
(* term τs (τ ⇒ τ) en (fun x: ⟦τ⟧ => x) *)
|
||||
(* | K: forall (τs: list type) (τ1 τ2: type) (en: env τs), *)
|
||||
(* term τs (τ1 ⇒ τ2 ⇒ τ1) en (fun (x1: ⟦τ1⟧) (x2: ⟦τ2⟧) => x1) *)
|
||||
(* | S: forall (τs: list type) (τa τb τx: type) (en: env τs), *)
|
||||
(* term τs ((τx ⇒ τa ⇒ τb) ⇒ (τx ⇒ τa) ⇒ τx ⇒ τb) en *)
|
||||
(* (fun (f: ⟦τx ⇒ τa ⇒ τb⟧) (g: ⟦τx ⇒ τa⟧) (x: ⟦τx⟧) => (f x) (g x)). *)
|
||||
|
||||
|
||||
(* Inductive term: forall (τs: list type) (τ: type), *)
|
||||
(* env τs -> typeDe τ -> Type := *)
|
||||
(* | I: forall (τs: list type) (X: type) (en: env τs), *)
|
||||
(* term τs (X ⇒ X) en *)
|
||||
(* (fun x: typeDe X => x) *)
|
||||
(* | K: forall (τs: list type) (X Y: type), *)
|
||||
(* term τs (X ⇒ Y ⇒ X) *)
|
||||
(* (fun (x:typeDe X) (y: typeDe Y) => x) *)
|
||||
(* | S: forall (τs: list type) (X Y Z: type), *)
|
||||
(* term τs ((X ⇒ Y ⇒ Z) ⇒ *)
|
||||
(* (X ⇒ Y) ⇒ *)
|
||||
(* (X ⇒ Z)) *)
|
||||
(* (fun (f: typeDe (X ⇒ Y ⇒ Z)) *)
|
||||
(* (g: typeDe (X ⇒ Y)) *)
|
||||
(* (x: typeDe X) => (f x) (g x)) *)
|
||||
(* | App: forall (X Y: type) (f: typeDe (X ⇒ Y)) (x: typeDe X), *)
|
||||
(* term (X ⇒ Y) f -> term X x -> term Y (f x) *)
|
||||
(* | Var: forall (X Y: type) (f: typeDe (X ⇒ Y)), *)
|
||||
(* term (X ⇒ Y) f -> term X x -> term (X ⇒ Y) f. *)
|
||||
|
||||
(* Inductive term: forall (τ: type), typeDe τ -> Type := *)
|
||||
(* | I: forall X: type, *)
|
||||
|
|
|
|||
|
|
@ -0,0 +1,361 @@
|
|||
(* 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. *)
|
||||
Inductive isInfinite {A: Type}: stream A -> Prop :=
|
||||
| IsInfin: forall (s: stream A) (a:A),
|
||||
isInfinite s -> isInfinite (SCons a s).
|
||||
End streams.
|
||||
|
||||
Section streamLemmas.
|
||||
Lemma unfoldStream {A: Type}: forall s: stream A,
|
||||
s = match s with
|
||||
| SNil => SNil
|
||||
| SCons x ss => SCons x ss
|
||||
end.
|
||||
Proof.
|
||||
move => s.
|
||||
by case: s.
|
||||
Qed.
|
||||
End streamLemmas.
|
||||
|
||||
Section ltl.
|
||||
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).
|
||||
End ltl.
|
||||
|
||||
|
||||
Section Lemmas.
|
||||
Context (A: Type).
|
||||
|
||||
Definition satisfies (P: stream A -> Prop) (s: stream A): Prop := P s.
|
||||
(*
|
||||
(cofix const (a0 : A) : stream A := SCons a0 (const a0)) a =
|
||||
SCons a ((cofix const (a0 : A) : stream A := SCons a0 (const a0)) a)
|
||||
*)
|
||||
(* rewrite {1}/const. *)
|
||||
(*
|
||||
(cofix const (a0 : A) : stream A := SCons a0 (const a0)) a =
|
||||
SCons a (const a)
|
||||
*)
|
||||
|
||||
Theorem nextRepeat: forall (a b: A),
|
||||
satisfies (next (atom (fun x => x = b))) (SCons a (const b)).
|
||||
Proof.
|
||||
move => a b.
|
||||
rewrite /satisfies.
|
||||
apply Next.
|
||||
rewrite (unfoldStream (const b)).
|
||||
rewrite /const.
|
||||
by apply Atom.
|
||||
Qed.
|
||||
|
||||
Theorem prefixEventually: forall (pre post: stream A) (P: sProp),
|
||||
isFinite pre ->
|
||||
satisfies P post ->
|
||||
satisfies P (sapp pre post).
|
||||
Proof.
|
||||
move => pre post P preFin.
|
||||
Abort.
|
||||
|
||||
Theorem alwaysInfinite: forall (s: stream A) (P: sProp),
|
||||
always P s -> isInfinite s.
|
||||
Proof.
|
||||
move => s P H.
|
||||
case: H.
|
||||
|
||||
rewrite (unfoldStream s).
|
||||
apply IsInfin.
|
||||
Abort.
|
||||
End Lemmas.
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
(* https://github.com/coq-contribs/ltl *)
|
||||
Require Import Streams.
|
||||
Require Import ssreflect.
|
||||
|
||||
Section 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.
|
||||
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. *)
|
||||
|
|
@ -0,0 +1,20 @@
|
|||
(* https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Type.20class.20constraint.20in.20record.20type.20member *)
|
||||
|
||||
Inductive myBool: Type := mtrue | mfalse.
|
||||
|
||||
Class Eq (A: Type) := {
|
||||
eqbC: A -> A -> bool
|
||||
}.
|
||||
|
||||
#[export] Instance eqmBool : Eq myBool := {
|
||||
eqbC := fun x y =>
|
||||
match x, y with
|
||||
| mtrue, mtrue => true
|
||||
| mfalse, mfalse => true
|
||||
| _, _ => false
|
||||
end
|
||||
}.
|
||||
|
||||
Record myRec := {
|
||||
eqElem {A: Type} `{Eq A}: A -> A -> bool
|
||||
}.
|
||||
Loading…
Reference in New Issue