examples.v
(* FILE: SAMPLED_STREAMS/examples.v _ Sylvain Boulmé _ LIP6 _ Spring 2001 *)
(* Coq V6.3.1 *)
Implicit Arguments On.
Require lucid_ops.
Require sp_rec.
Require Arith.
Require Refine.
(* rec0 basis for "Auto" *)
Hints Resolve rec0_wf: sp_rec0.
Hint rec0_inv_r: sp_rec0 := Extern 4 (sp_eq ? ?) Refine (rec0_inv ? ?).
Hints Resolve sp_inf_refl: sp_rec0.
Hints Resolve glob_nfstwf_S_n_n: sp_rec0'.
Definition
Nat := [c]
(<c>rec0 [N](`(0)` fby (ext `S` N))).
Check Nat.
Lemma
Nat_inv: (c:clock)(sp_eq (Nat c) (`O` fby (ext `S` (Nat c)))).
Proof.
Auto with sp_rec0.
Qed.
Definition
Nat_on := [c; lc]
(<c>rec0 [N](merge lc (`(0)` fby ((ext `S` N) when lc)) `(0)`)).
Check Nat_on.
Lemma
Nat_on_inv: (c:clock; lc: (samplStr bool c))
(sp_wf lc)
->(sp_eq (Nat_on lc) (merge lc (`(0)` fby ((ext `S` (Nat_on lc)) when lc)) `(0)`)).
Proof.
Auto 10 with sp_rec0.
Qed.
Definition
Nat_mod := [c; lc]
(<c>rec0 [N](merge lc ((`(0)` fby (ext `S` N)) when lc) `(0)`)).
Check Nat_mod.
Lemma
Nat_mod_inv: (c:clock; lc: (samplStr bool c))
(sp_wf lc)
->(sp_eq (Nat_mod lc) (merge lc ((`(0)` fby (ext `S` (Nat_mod lc))) when lc) `(0)`)).
Proof.
Auto 10 with sp_rec0.
Qed.
Definition
Fib := [c]
(<c>rec0 [fib]
(`(1)` fby (ext (ext `plus` fib) (`(0)` fby fib)))).
Lemma
Fib_inv:
(c:clock)
(sp_eq (Fib c)
(`(1)` fby (ext (ext `plus` (Fib c))
(`(0)` fby (Fib c))))).
Proof.
Intros; Refine (rec0_inv ? ?); Auto 10 with sp_rec0.
Intros; Apply sp_fby_glob_nfstwf; Auto with sp_rec0.
Apply sp_extend_glob_nfstwf; Auto with sp_rec0.
Apply glob_nfstwf_S_n_n; Auto with sp_rec0.
Qed.
Definition
half := [c]
(<c>rec0 [half] `true` fby (sp_not half)).
Check half.
Definition
hold :=
[A; c; ydef:(samplStr A c); lc; x]
(rec0 [y](merge lc x ((ydef fby y) when (sp_not lc)))).
Check hold.
Definition
over := [c;x](hold `(1)` 4!(half c) x).
Check over.
(* Example wrong_clocked *)
(* rejected by typecheck => it is expected !
Check ([c:clock;x:(samplStr nat c)]
(ext (ext `plus` x) (x when (half ?)))).
*)
Require EqNat.
(* clock example *)
Section Counter.
Variable c: clock.
Variable n: (samplStr nat c).
Hypothesis n_wf:(sp_wf n).
Definition
acc_aux:=[count]
(<c>rec0 [acc] `(1)` fby (sp_if count `(1)` (ext `S` acc))).
Lemma
acc_lfp:
(m:nat; count1,count2:(samplStr bool c))
(sp_inf m count1 count2)
-> (sp_inf m (acc_aux count1) (acc_aux count2)).
Proof.
Intros; Unfold acc_aux; Apply rec0_lfp.
Auto with sp_rec0.
Qed.
Hints Resolve glob_nfstwf_n_le: sp_rec0.
Lemma
acc_glob_nfstwf:
(m:nat; count:(samplStr bool c))
(glob_nfstwf m count)
-> (glob_nfstwf (S m) (acc_aux count)).
Proof.
Intros; Unfold acc_aux; Apply rec0_glob_nfstwf.
Intros; Apply sp_fby_glob_nfstwf.
Auto with sp_rec0.
Apply sp_if_glob_nfstwf; EAuto with arith sp_rec0.
Auto with sp_rec0.
Auto with sp_rec0.
Qed.
Hints Resolve acc_lfp acc_glob_nfstwf: sp_rec0.
Definition
counter:=
(rec0 [count](ext (ext `beq_nat` n) (acc_aux count))).
Lemma
counter_wf: (sp_wf counter).
Proof.
Unfold counter; Auto 10 with sp_rec0.
Qed.
Hints Resolve counter_wf : sp_rec0.
Lemma
counter_inv:
(sp_eq counter (ext (ext `beq_nat` n) (acc_aux counter))).
Proof.
Auto 10 with sp_rec0.
Qed.
Lemma
acc_aux_count_inv:
(sp_eq (acc_aux counter)
`(1)` fby (sp_if counter `(1)` (ext `S` (acc_aux counter)))).
Proof.
Auto 10 with sp_rec0.
Qed.
End Counter.
Check counter.
Definition
filter1 := [A;c;n;top:(samplStr A c)](top when (counter n)).
Check filter1.
Definition
minute := [A;c; sec:(samplStr A c)](filter1 `(60)` sec).
Check minute.
Definition
hour := [A;c; sec:(samplStr A c)](filter1 `(60)` (minute sec)).
Check hour.
Section MachineACafe.
Definition
sumbool2bool :=
[A,B:Prop;x:{A}+{B}]Cases x of (left _) => true | (right _) => false end.
Require Compare_dec.
Definition
nat_le :=[n,m](sumbool2bool (le_lt_dec n m)).
Variable c: clock.
Variable piece_ins:(samplStr nat c).
Variable appui_bouton: (samplStr bool c).
Hypothesis piece_ins_wf: (sp_wf piece_ins).
Hypothesis appui_bouton_wf: (sp_wf appui_bouton).
Definition
servir_cafe_aux :=
[pnbp](ext (ext `andb` appui_bouton)
(ext (ext `nat_le` `(2)`) pnbp)).
Definition
nombre_pieces :=
[pnbp](ext (ext `minus` (ext (ext `plus` piece_ins) pnbp))
(sp_if (servir_cafe_aux pnbp) `(2)` `(0)`)).
Definition
prec_nombre_pieces := (rec0 [np](`(0)` fby (nombre_pieces np))).
Lemma
pnp_inv:(sp_eq prec_nombre_pieces
(`(0)` fby (nombre_pieces prec_nombre_pieces))).
Proof.
Refine (rec0_inv ? ?); Unfold nombre_pieces; Unfold servir_cafe_aux;
Auto 10 with sp_rec0.
Qed.
Definition
servir_cafe:=(servir_cafe_aux prec_nombre_pieces).
End MachineACafe.
Definition
first := [A; c; x:(samplStr A c)]
(rec0 [fst](x fby fst)).
Lemma
first_wf:(A:Set; c:clock; x:(samplStr A c))
(sp_wf x)->(sp_wf (first x)).
Unfold first; Auto with sp_rec0.
Qed.
Hints Resolve first_wf: sp_rec0.
(**************** rec1 examples ************************)
Definition
counter1_aux :=
[c:clock][n]
(rec1 3![_]c
[count: (samplStr ? c)->(samplStr ? c); acc]
(sp_if (ext (ext `beq_nat` acc) n)
(`true` fby (count `(1)`))
(`false` fby (count (ext `S` acc))))).
Lemma
counter1_aux_inv:
(c:clock; n,acc:(samplStr nat c))
(sp_wf n)->(sp_wf acc)->
(sp_eq (counter1_aux n acc)
(sp_if (ext (ext `beq_nat` acc) n)
(`true` fby (counter1_aux n `(1)`))
(`false` fby (counter1_aux n (ext `S` acc))))).
Proof.
Intros c n acc H1 H2;
Refine (rec1_inv
3![_:(samplStr nat c)]c
5
? ? ?);
Auto with sampled_str sp_rec0.
Qed.
Definition
counter1 :(c:clock)(samplStr nat c)->(samplStr bool c)
:= [c; n](counter1_aux n `(1)`).
Check counter1.
Syntactic Definition
Dpair := [P](existS ? P ?).
Section Generic_sieve.
Variable A: Set.
Variable filter:(c:clock)(samplStr A c)->(samplStr bool c).
Hypothesis filter_wf:
(c:clock; x:(samplStr A c))(sp_wf x)->(sp_wf (filter x)).
Hypothesis filter_is_fst_true:
(c:clock; x:(samplStr A c))(is_fst_value true (filter x)).
Definition
sieve' := [c; x:(samplStr ? c)]
(rec1 3!ProjS1
[sieve;p:{c:clock & (samplStr A c)}]
let x = (ProjS2 p)
in
(merge (filter x)
(`true` fby `false`)
(sieve (Dpair [c](samplStr A c) (x when (sp_not (filter x))))))
(Dpair [c](samplStr A c) x)).
Lemma
sieve'_inv: (c:clock; x:(samplStr A c))
(sp_wf x)->
(sp_eq (sieve' x)
(merge (filter x) (`true` fby `false`)
(sieve' (x when (sp_not (filter x)))))).
Proof.
Unfold sieve'; Intros c x H1;
Refine (rec1_inv
5)
? ? ?); Try (Simpl; Auto; Fail); Clear H1 x c.
Intros s1 s2 n H1 p; Case p; Simpl; Intros c x H2.
Apply sp_merge_lfp; Auto with sampled_str.
Apply H1 with x:=(Dpair [c:clock](samplStr A c) (x when (sp_not (filter x))));
Simpl; Unfold sp_not; Auto with sampled_str.
Intros n s H1 p; Case p; Simpl; Intros c x H2;
Apply sp_merge_true_loc_nfstwf; Auto with sampled_str.
Apply H1 with x:=(Dpair [c:clock](samplStr A c) (x when (sp_not (filter x))));
Simpl; Unfold sp_not; Auto with sampled_str.
Qed.
Definition
sieve: (c:clock)(samplStr A c)->(samplStr bool c)
:=sieve'.
Lemma
sieve_inv: (c:clock; x:(samplStr A c))
(sp_wf x)->
(sp_eq (sieve x)
(merge (filter x) (`true` fby `false`)
(sieve (x when (sp_not (filter x)))))).
Proof sieve'_inv.
End Generic_sieve.
Section My_Reset.
(* redefinition de arrow *)
Definition
arrow := [A;c; x,y:(samplStr A c)](sp_if (`true` fby `false`) x y).
(* un autre repeat_until *)
Definition
o_repeat_until := [c;lc]
(<c>rec0 [rpu](arrow `true` (ext (ext `andb` (sp_not lc))
(`true` fby rpu)))).
(* le vrai !! *)
Definition
repeat_until := [c;lc]
(<c>rec0 [rpu]`true` --> (ext (ext `andb` (sp_not lc)) (pre rpu))).
Lemma
repeat_until_wf:
(c:clock; lc:(samplStr bool c))
(sp_wf lc)
->(sp_wf (repeat_until lc)).
Proof.
Unfold repeat_until; Intros c lc H; Apply rec0_wf.
Intros; Unfold sp_not; Apply sp_arrow_extend2_pre_glob_nfstwf; Auto with sp_rec0.
Qed.
Lemma
repeat_until_inv:
(c:clock; lc:(samplStr bool c))
(sp_wf lc)
->(sp_eq (repeat_until lc)
(`true` --> (ext (ext `andb` (sp_not lc))
(pre (repeat_until lc))))).
Proof.
Unfold repeat_until; Intros c lc H; Refine (rec0_inv ? ?); Intros;
Unfold sp_not.
Apply sp_arrow_extend2_pre_lfp; Auto with sp_rec0.
Apply sp_arrow_extend2_pre_glob_nfstwf; Auto with sp_rec0.
Qed.
Hints Resolve repeat_until_wf repeat_until_inv: sp_rec0.
Lemma
repeat_is_fst_value_true:
(c:clock; lc:(samplStr bool c))
(sp_wf lc)
->(is_fst_value true (repeat_until lc)).
Proof.
Intros c lc H; Apply is_fst_value_sp_eq with
s1:=(`true` --> (ext (ext `andb` (sp_not lc))
(pre (repeat_until lc))));
Auto with sampled_str sp_rec0.
Qed.
Variable A,B: Set.
Variable f: (c:clock)(samplStr A c)->(samplStr B c).
Hypothesis f_wf: (c:clock; x:(samplStr A c))(sp_wf x)->(sp_wf (f x)).
Definition
reset':
(c:clock)(samplStr A c)-> (samplStr bool c) -> (samplStr B c)
:= [c; x;lc]
(rec1 3!ProjS1
[reset; p:{ c:clock & ((samplStr A c) * (samplStr bool c)) }]
let (x,lc)=(ProjS2 p)
in
let c0 = (repeat_until lc)
in
(merge c0 (f (x when c0))
(reset (Dpair [c:clock](samplStr A c)*(samplStr bool c)
((x when (sp_not c0)),(lc when (sp_not c0))))))
(Dpair [c:clock](samplStr A c)*(samplStr bool c) (x,lc))).
Definition
reset := [c; x: (samplStr ? c);lc]
(rec1 3!ProjS1
[reset; p:{ c:clock & ((samplStr A c) * (samplStr bool c)) }]
let (x,lc)=(ProjS2 p)
in
let c0 = (repeat_until lc)
in
(merge c0 (f (x when c0))
(reset (Dpair [c:clock](samplStr A c)*(samplStr bool c)
((x when (sp_not c0)),(lc when (sp_not c0))))))
(Dpair [c:clock](samplStr A c)*(samplStr bool c) (x,lc))).
Lemma
reset_inv: (c:clock; x:(samplStr A c); lc:(samplStr bool c))
let c0 = (repeat_until lc)
in
(sp_wf x)->
(sp_wf lc)->
(sp_eq (reset x lc)
(merge c0 (f (x when c0))
(reset (x when (sp_not c0)) (lc when (sp_not c0))))).
Proof.
Unfold reset; Intros c x lc H1 H2;
Refine (rec1_inv
5!([p:{ c:clock & ((samplStr A c) * (samplStr bool c)) }]
let (x,lc)=(ProjS2 p)
in (sp_wf x)/\(sp_wf lc))
? ? ?); Try (Simpl; Auto; Fail); Clear H2 H1 lc x c.
Intros s1 s2 n H1 p; Case p; Simpl; Intros c p'; Case p'; Simpl; Clear p p';
Intros x lc H2; Case H2; Intros;
Apply sp_merge_lfp; Auto with sampled_str sp_rec0.
Apply H1 with x:=(Dpair [c:clock](samplStr A c)*(samplStr bool c)
let c0 = (repeat_until lc)
in ((x when (sp_not c0)), (lc when (sp_not c0))));
Simpl; Unfold sp_not; Auto with sampled_str sp_rec0.
Intros n s H1 p; Case p; Intros c p'; Case p'; Simpl; Clear p p';
Intros x lc H2; Case H2; Intros.
Apply sp_merge_true_loc_nfstwf; Auto with sampled_str sp_rec0.
Apply repeat_is_fst_value_true; Auto.
Apply H1 with x:=(Dpair [c:clock](samplStr A c)*(samplStr bool c)
let c0 = (repeat_until lc)
in ((x when (sp_not c0)), (lc when (sp_not c0))));
Simpl; Unfold sp_not; Auto with sampled_str sp_rec0.
Qed.
End My_Reset.
Check reset'.
Definition
expb := [c]
(<c>rec0 [expb](`true` fby (merge expb (`false` fby `true`)
(`true` fby `false`)))).
(*
Lemma expb_inv: (c:clock)(sp_eq (expb c) (`true` fby (merge (expb c)
(`false` fby `true`)
(`true` fby `false`)))).
Proof.
Intros; Refine (rec0_inv ? ?).
2:(Intros; Apply sp_fby_glob_nfstwf; Auto with sp_rec0; Apply sp_merge_glob_nfstwf;
Auto with sp_rec0; Apply glob_nfstwf_S_n_n; Auto with sp_rec0).
Intros; Apply sp_fby_lfp; Auto with sp_rec0.
Intros; Apply sp_merge_lfp; Auto with sp_rec0.
Intros; Apply sp_fby_lfp; Auto with sp_rec0.
Abort.
Qed.
*)
(*
Definition essaif := [c; x:(samplStr ? c)](ext (ext `plus` x) (Nat ?)).
Definition essaic := (const true).
Definition essaielt := (sp_cons 2!essaic (Any O) `(1)`).
Definition essailc :=
(rec0 [x:(samplStr ? essaic)](`true` fby `false` fby x)).
Definition essai:=(sp_reset essaif essaielt (sp_const false essaic)).
Eval Compute in (sp_nth (0) essai).
Eval Compute in (sp_nth (1) essai).
Eval Compute in (sp_nth (2) essai).
Eval Compute in (sp_nth (3) essai).
Eval Compute in (sp_nth (4) essai).
Reset essai.
Definition essai:=(sp_reset essaif essaielt (sp_const true essaic)).
Eval Compute in (sp_nth (0) essai).
Eval Compute in (sp_nth (1) essai).
Eval Compute in (sp_nth (2) essai).
Eval Compute in (sp_nth (3) essai).
Eval Compute in (sp_nth (4) essai).
Eval Compute in (sp_nth (5) essai).
Eval Compute in (sp_nth (6) essai).
Eval Compute in (sp_nth (7) essai).
Reset essai.
Definition essai:=(sp_reset essaif essaielt essailc).
Eval Compute in (sp_nth (0) essai).
Eval Compute in (sp_nth (1) essai).
Eval Compute in (sp_nth (2) essai).
Eval Compute in (sp_nth (3) essai).
Eval Compute in (sp_nth (4) essai).
Eval Compute in (sp_nth (5) essai).
*)
(*
Definition essaif := [c; x:(samplStr ? c)](ext (ext `plus` x) (Nat ?)).
Definition essaic := (const true).
Definition essaielt := (sp_const O essaic).
Definition essailc := (sp_const false essaic).
Definition essai:=(my_reset (Build_my_reset_arg essaif essaielt essailc)).
Eval Compute in (sp_nth (0) essai).
Eval Compute in (sp_nth (1) essai).
Eval Compute in (sp_nth (2) essai).
Eval Compute in (sp_nth (3) essai).
*)
05/07/101, 15:41