### Profile

Statistics
| Branch: | Tag: | Revision:

## lustrec / optim / lustre.v @ 6a93d814

 1 ```Require Import Arith. ``` ```Require Import Omega. ``` ```Require Import Bool. ``` ```Require Import Compare_dec. ``` ```Require Import Wf_nat. ``` ```Require Import Wellfounded. ``` ```Require Import Relation_Definitions. ``` ```Require Import Recdef. ``` ```Require Import StreamsLib. ``` ```Lemma eq_Z_effective : effective (fun (x y : Z) => x = y). ``` ```Proof. ``` ```unfold effective. ``` ```repeat decide equality. ``` ```Qed. ``` ```Lemma eq_bool_effective : effective (fun (x y : bool) => x = y). ``` ```Proof. ``` ```unfold effective. ``` ```repeat decide equality. ``` ```Qed. ``` ```Lemma eq_unit_effective : effective (fun (x y : unit) => x = y). ``` ```Proof. ``` ```unfold effective. ``` ```repeat decide equality. ``` ```Qed. ``` ```Lemma eq_pair_effective : forall {A B}, ``` ``` effective (fun (x y : A) => x = y) -> effective (fun (x y : B) => x = y) -> effective (fun (x y : A * B) => x = y). ``` ```Proof. ``` ```unfold effective. ``` ```repeat decide equality. ``` ```Qed. ``` ```Definition par {A B} (rA : relation A) (rB : relation B) := fun ab ab' => rA (fst ab) (fst ab') /\ rB (snd ab) (snd ab'). ``` ```Theorem gt_par_comm : forall {A B} (leA : relation A) (leB : relation B), ``` ``` inclusion _ (par (gt leA) (gt leB)) (gt (par leA leB)) . ``` ```Proof. ``` ```unfold gt, par, inclusion. ``` ```intuition. ``` ```Qed. ``` ```Theorem wf_par : forall {A B} (rA : relation A) (rB : relation B), ``` ``` well_founded rA -> well_founded rB -> well_founded (par rA rB). ``` ```Proof. ``` ```unfold well_founded, par. ``` ```intros A B rA rB. ``` ```intros Ha Hb ab. ``` ```destruct ab as (a, b). ``` ```revert Hb b. ``` ```induction (Ha a). ``` ```intros. ``` ```apply Acc_intro. ``` ```intros. ``` ```destruct y. ``` ```apply H0. ``` ``` intuition. ``` ``` assumption. ``` ```Qed. ``` ```Theorem wf_gt_par : forall {A B} (rA : relation A) (rB : relation B), ``` ``` well_founded (gt rA) -> well_founded (gt rB) -> well_founded (par (gt rA) (gt rB)). ``` ```Proof. ``` ```unfold well_founded, par, gt. ``` ```intros A B rA rB. ``` ```intros Ha Hb ab. ``` ```destruct ab as (a, b). ``` ```revert Hb b. ``` ```induction (Ha a). ``` ```intros. ``` ```apply Acc_intro. ``` ```destruct y. ``` ```intuition. ``` ```Qed. ``` ```Definition cross {A B C D} (f : A -> B) (g : C -> D) : A * C -> B * D := fun ac => (f (fst ac), g (snd ac)). ``` ```Theorem le_par : forall {A B} (leA : relation A) (leB : relation B) (f : A -> A) (g : B -> B) a b, ``` ``` leA a (f a) -> leB b (g b) -> (par leA leB) (a, b) ((cross f g) (a, b)). ``` ```Proof. ``` ```unfold par, cross. ``` ```intuition. ``` ```Qed. ``` ```Lemma rel_pair_effective : forall {A B} {rA : relation A} {rB : relation B}, ``` ``` effective rA -> effective rB -> effective (par rA rB). ``` ```Proof. ``` ```unfold effective. ``` ```intros. ``` ```unfold par. ``` ```destruct a1. ``` ```destruct a2. ``` ```destruct (X a a0). ``` ``` destruct (X0 b b0). ``` ``` intuition. ``` ``` intuition. ``` ``` intuition. ``` ```Qed. ``` ```Inductive element {A : Type} : Type := ``` ```| Bot : @element A ``` ```| Elt : A -> @element A ``` ```| Top : @element A. ``` ```Definition measure_elt {A} (e : @element A) : nat := ``` ``` match e with ``` ``` | Bot => 2 ``` ``` | Elt _ => 1 ``` ``` | Top => 0 ``` ``` end. ``` ```Definition union_elt {A} (eqA : effective (fun x y => x = y)) (e1 e2 : @element A) : @element A := ``` ``` match (e1, e2) with ``` ``` | (Bot , _ ) => e2 ``` ``` | (_ , Bot ) => e1 ``` ``` | (Elt a1, Elt a2) => if eqA a1 a2 then Elt a1 else Top ``` ``` | (_ , _ ) => Top ``` ``` end. ``` ```Definition apply_elt {A B} (ef : @element (A -> B)) (ex : @element A) : @element B := ``` ``` match (ef, ex) with ``` ``` | (Top , _ ) => Top ``` ``` | (_ , Top ) => Top ``` ``` | (Bot , _ ) => Bot ``` ``` | (_ , Bot ) => Bot ``` ``` | (Elt f, Elt x) => Elt (f x) ``` ``` end. ``` ```Definition merge_elt {A} (ec : @element bool) (e1 e2 : @element A) : @element A := ``` ``` match (e1, e2) with ``` ``` | (Bot , _ ) => e2 ``` ``` | (_ , Bot ) => e1 ``` ``` | (_ , _ ) => Top ``` ``` end. ``` ```Definition when_elt {A} (e1 : @element A) (e2 : @element bool) : @element A := ``` ``` match (e1, e2) with ``` ``` | (_ , Top ) => Top ``` ``` | (Top , _ ) => Top ``` ``` | (_ , Elt true) => e1 ``` ``` | (_ , _ ) => Bot ``` ``` end. ``` ```Definition ite_elt {A} (e1 : @element bool) (e2 : @element A) (e3 : @element A) : @element A := ``` ``` match (e1, e2, e3) with ``` ``` | (Top , _ , _ ) => Top ``` ``` | (_ , Top, _ ) => Top ``` ``` | (_ , _ , Top) => Top ``` ``` | (Elt true , _ , _ ) => e2 ``` ``` | (Elt false, _ , _ ) => e3 ``` ``` | (Bot , _ , _ ) => Bot ``` ``` end. ``` ```Definition undef {A} := lift (@Bot A). ``` ```Fixpoint slice {A} (s : Stream (@element A)) (n : nat) {struct n} : Stream (@element A) := ``` ``` match n with ``` ``` | O => undef ``` ``` | S p => Cons (hd s) (slice (tl s) p) ``` ``` end. ``` ```Theorem slice_bisim : forall {A} (s1 s2 : Stream (@element A)), EqSt s1 s2 -> forall n, EqSt (slice s1 n) (slice s2 n). ``` ```Proof. ``` ```cofix proof. ``` ```destruct s1; destruct s2; intros. ``` ```destruct n; simpl. ``` ``` apply EqSt_reflex. ``` ``` ``` ``` inversion H. ``` ``` apply eqst. ``` ``` exact H0. ``` ``` ``` ``` apply proof. ``` ``` exact H1. ``` ```Qed. ``` ```Definition bisim_upto {A} (n : nat) : relation (Stream (@element A)) := ``` ``` fun s1 => fun s2 => EqSt (slice s1 n) (slice s2 n). ``` ```Theorem bisim_bisim_upto : forall {A} (s1 s2 : Stream (@element A)), ``` ``` EqSt s1 s2 -> forall n, bisim_upto n s1 s2. ``` ```Proof. ``` ```unfold bisim_upto. ``` ```cofix proof. ``` ```intros. ``` ```destruct s1; destruct s2. ``` ```destruct n; simpl. ``` ``` apply EqSt_reflex. ``` ``` ``` ``` inversion H. ``` ``` apply eqst. ``` ``` exact H0. ``` ``` ``` ``` apply proof. ``` ``` exact H1. ``` ```Qed. ``` ```Theorem bisim_upto_bisim : forall {A} (s1 s2 : Stream (@element A)), ``` ``` (forall n, bisim_upto n s1 s2) -> EqSt s1 s2. ``` ```Proof. ``` ```unfold bisim_upto. ``` ```cofix proof. ``` ```intros. ``` ```destruct s1; destruct s2. ``` ```apply eqst. ``` ``` destruct (H 1). ``` ``` exact H0. ``` ``` ``` ``` apply proof. ``` ``` intro n. ``` ``` destruct (H (S n)). ``` ``` assumption. ``` ```Qed. ``` ```Definition le_elt {A} (e1 e2 : @element A) := ``` ``` measure_elt e1 >= measure_elt e2. ``` ```Theorem le_elt_mono : forall {A} eqA (x y : @element A), le_elt x (union_elt eqA x y). ``` ```Proof. ``` ```unfold le_elt. ``` ```destruct x; destruct y; simpl; auto with arith. ``` ```unfold union_elt. ``` ```destruct eqA; auto with arith. ``` ```Qed. ``` ```Theorem le_elt_effective : forall {A}, effective (@le_elt A). ``` ```Proof. ``` ```unfold effective, le_elt. ``` ```intros A a1 a2. ``` ```apply ge_dec. ``` ```Qed. ``` ```Theorem gt_elt_acc : forall {A}, well_founded (gt (@le_elt A)). ``` ```Proof. ``` ```unfold gt, le_elt. ``` ```intro A. ``` ```eapply wf_incl. ``` ``` intros x y H. ``` ``` destruct H. ``` ``` apply not_ge. ``` ``` apply H0. ``` ``` eapply well_founded_lt_compat. ``` ``` intros x y H. ``` ``` apply H. ``` ```Qed. ``` ```(* ``` ```Definition lt_elt {A} (e1 e2 : @element A) := ``` ``` measure_elt e1 > measure_elt e2. ``` ```Theorem not_le_lt_elt : forall {A} (e1 e2 : @element A), ``` ``` ~ le_elt e1 e2 -> lt_elt e2 e1. ``` ```Proof. ``` ```unfold le_elt, lt_elt. ``` ```intros. ``` ```omega. ``` ```Qed. ``` ```Theorem lt_not_le_elt : forall {A} (e1 e2 : @element A), ``` ``` lt_elt e1 e2 -> ~ le_elt e2 e1. ``` ```Proof. ``` ```unfold le_elt, lt_elt. ``` ```intros. ``` ```omega. ``` ```Qed. ``` ```Definition gt_elt {A} (e1 e2 : @element A) := lt_elt e2 e1. ``` ```Theorem le_elt_dec : forall {A} (e1 e2 : @element A), { le_elt e1 e2 } + { lt_elt e2 e1 }. ``` ```Proof. ``` ```unfold lt_elt, le_elt, ge in |- *. ``` ```intros. ``` ```apply le_lt_dec. ``` ```Qed. ``` ```Theorem le_elt_effective : forall {A}, effective (@element A) le_elt. ``` ```Proof. ``` ```unfold effective in |- *. ``` ```intros A a1 a2. ``` ```destruct (le_elt_dec a1 a2). ``` ``` left; assumption. ``` ``` ``` ``` right; apply lt_not_le_elt; assumption. ``` ```Defined. ``` ```Theorem gt_elt_acc : forall {A}, well_founded (gt (@le_elt A)). ``` ```Proof. ``` ```unfold gt_elt, lt_elt in |- *. ``` ```intro A. ``` ```eapply well_founded_lt_compat. ``` ```unfold gt in |- *. ``` ```intros x y H. ``` ```apply H. ``` ```Qed. ``` ```Theorem gt_hd_acc : forall {A}, well_founded (lift_hd (@element A) gt_elt). ``` ```Proof. ``` ```intro A. ``` ```unfold lift_hd. ``` ```apply wf_inverse_image. ``` ```exact gt_elt_acc. ``` ```Qed. ``` ```*) ``` ```Fixpoint list2type (l : list Set) : Set := ``` ``` match l with ``` ``` | nil => unit ``` ``` | cons t q => (t * list2type q)%type ``` ``` end. ``` ```Module Signal. ``` ```Definition t A := Stream (@element A). ``` ```Definition clock := Stream bool. ``` ```(* ``` ```Variable A : Set. ``` ```Variable eqA_effective : effective A (fun x y => x=y). ``` ```Theorem eq_elt_effective : effective element (fun x y => x=y). ``` ```Proof. ``` ```unfold effective in |- *. ``` ```unfold effective in eqA_effective. ``` ```decide equality. ``` ```Defined. ``` ```*) ``` ```Definition union {A} eqA (s1 s2 : t A) := apply (apply (lift (union_elt eqA)) s1) s2. ``` ```Definition loop {A} eqA (f : t A -> t A) : t A := ``` ``` rec eqA f undef. ``` ```Definition lift {A} (v : A) : t A := lift (Elt v). ``` ```Definition apply {A B} (f : t (A -> B)) (a : t A) : t B := ``` ``` StreamsLib.apply (StreamsLib.apply (StreamsLib.lift (@apply_elt A B)) f) a. ``` ```Definition when {A} (s : t A) (w : t bool) : t A := StreamsLib.apply (StreamsLib.apply (StreamsLib.lift (@when_elt A)) s) w. ``` ```CoFixpoint pre {A} (old : @element A) (s : t A) : t A := ``` ``` Cons old (pre (hd s) (tl s)). ``` ```Definition _arrow : t bool := Cons (Elt true) (lift false). ``` ```Definition ite {A} (s_if : t bool) (s_then s_else : t A) : t A := ``` ``` StreamsLib.apply (StreamsLib.apply (StreamsLib.apply (StreamsLib.lift (@ite_elt A)) s_if) s_then) s_else. ``` ```Lemma hd_ite : forall {A}, forall (cs : t bool) (ts es : t A), ``` ``` hd (ite cs ts es) = ite_elt (hd cs) (hd ts) (hd es). ``` ```Proof. ``` ```destruct cs; destruct ts; destruct es. ``` ```reflexivity. ``` ```Qed. ``` ```Lemma tl_ite : forall {A}, forall (cs : t bool) (ts es : t A), ``` ``` tl (ite cs ts es) = ite (tl cs) (tl ts) (tl es). ``` ```Proof. ``` ```destruct cs; destruct ts; destruct es. ``` ```reflexivity. ``` ```Qed. ``` ```Theorem eqst_ite : forall {A}, forall (c1 c2 : t bool) (t1 t2 e1 e2 : t A), ``` ``` EqSt c1 c2 -> EqSt t1 t2 -> EqSt e1 e2 -> EqSt (ite c1 t1 e1) (ite c2 t2 e2). ``` ```Proof. ``` ```intros. ``` ```apply eqst_apply. ``` ``` apply eqst_apply. ``` ``` apply eqst_apply. ``` ``` apply EqSt_reflex. ``` ``` assumption. ``` ``` assumption. ``` ``` assumption. ``` ```Qed. ``` ```Definition correct {A} (s : t A) := ForAll (fun s => ~ hd s = Top) s. ``` ```Definition causal {A B} (f : t A -> t B) := ``` ``` forall (s1 s2 : t A) n, bisim_upto n s1 s2 -> bisim_upto n (f s1) (f s2). ``` ```End Signal. ``` ```Require Import Bool. ``` ```Definition bnot (s : Stream bool) := apply (lift negb) s. ``` ```Definition band (s1 s2 : Stream bool) := apply (apply (lift andb) s1) s2. ``` ```Definition bor (s1 s2 : Stream bool) := apply (apply (lift orb) s1) s2. ``` ```Require Import ZArith. ``` ```Definition iplus (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => (i1 + i2)%Z)) s1) s2. ``` ```Definition iminus (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => (i1 - i2)%Z)) s1) s2. ``` ```Definition imult (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => (i1 * i2)%Z)) s1) s2. ``` ```Definition idiv (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => (i1 / i2)%Z)) s1) s2. ``` ```Definition imod (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => Zmod i1 i2)) s1) s2. ``` ```Definition ieq (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => match (i1 ?= i2)%Z with Eq => true | _ => false end)) s1) s2. ``` ```Definition ilt (s1 s2 : Stream Z) := apply (apply (lift (fun i1 i2 => match (i1 ?= i2)%Z with Lt => true | _ => false end)) s1) s2. ``` ```(* sémantiques du noeud f: ``` ``` node f(x : int) returns (y, cpt : int) ``` ``` let ``` ``` y = x + 1; ``` ``` cpt = (0 -> pre cpt)+ 1; ``` ``` tel ``` ```*) ``` ```Definition denot_f (x : Signal.t Z) := ``` ``` Signal.loop ``` ``` (eq_pair_effective eq_Z_effective eq_Z_effective) ``` ``` (fun y_cpt => let (y , cpt) := unzip y_cpt in ``` ``` let y' := iplus x (Signal.lift 1%Z) in ``` ``` let cpt' := iplus (Signal.ite Signal._arrow (lift 0%Z) (Signal.pre cpt)) (lift 1%Z) in ``` ``` zip (y', cpt')). ``` ```(* sémantique dénotationnelle de f *) ``` ```Definition denot_f (x cpt y : Stream Z) := ``` ``` (EqSt y (iplus x (lift 1%Z))) /\ (EqSt cpt (iplus (ite _arrow (lift 0%Z) (pre cpt)) (lift 1%Z))). ``` ```(* sémantique axiomatique de f, simplifiée *) ``` ```Definition mem_f := (bool * Z)%type. ``` ```Definition ni_2 (mem : mem_f) := fst mem. ``` ```Definition __f_2 (mem : mem_f) := snd mem. ``` ```Definition init_f (mem : mem_f) := ni_2 mem = true. ``` ```Definition trans_f (x cpt y : Z) (mem_in mem_out : mem_f) := ``` ``` (cpt = ((if bool_dec (ni_2 mem_in) true then 0 else (__f_2 mem_in)) + 1)%Z) ``` ``` /\ (y = (x + 1)%Z) ``` ``` /\ (ni_2 mem_out) = false ``` ``` /\ (__f_2 mem_out) = cpt. ``` ```Definition trans_f' (s s' : (Z * (Z * Z)) * mem_f) := ``` ``` match s, s' with ``` ``` | ((x, (cpt, y)), mem), ((x', (cpt', y')), mem') => trans_f x cpt y mem mem' ``` ``` end. ``` ```Lemma Cons_inj : forall {A}, forall a a' (s s' : Stream A), Cons a s = Cons a' s' -> a = a' /\ s = s'. ``` ```Proof. ``` ```intros. ``` ```injection H. ``` ```intuition. ``` ```Qed. ``` ```Theorem raffinement : forall (x cpt y : Stream Z) (mem : Stream mem_f), ``` ``` (init_f (hd mem) /\ transition trans_f' (zip ((zip (x, (zip (cpt, y)))), mem))) ``` ``` -> ``` ``` denot_f x cpt y. ``` ```Proof. ``` ```intros. ``` ```apply zip_pair. ``` ```revert x cpt y mem H. ``` ```cofix proof. ``` ```intros. ``` ```intros. ``` ```split. ``` ``` revert x cpt y mem H. ``` ``` cofix proof. ``` ``` intros. ``` ``` destruct H. ``` ``` destruct x as (x0, x'); destruct cpt as (cpt0, cpt'); destruct y as (y0, y'). ``` ``` destruct mem as (mem0, mem'). ``` ``` inversion H0. ``` ``` apply eqst. ``` ``` simpl. ``` ``` unfold zip in H1. ``` ``` simpl in H1. ``` ``` generalize (f_equal (@hd _) H1). ``` ``` simpl. ``` ``` intro. ``` ``` subst. ``` ``` generalize (f_equal (@tl _) H1). ``` ``` simpl. ``` ```Qed. ```