# Library Multiplier.Circ

Require Import GFP.
Require Import Streams.

Section Circuits.

Variable TI TR TO : Set.

Variable output : TI TR TO.
Variable update : TI TR TR.

Definition CIRC (ri : TR) (si : Str TI) : Str TO :=
STRCOIT _ _
(fun x : Str TI × TR
let (s, r) return (TO × (Str TI × TR)) := x in
(output (HD _ s) r, (TL _ s, update (HD _ s) r)))
(si, ri).
Let Circ := CIRC.

Theorem Hd_Circ :
(r : TR) (si : Str TI), HD _ (Circ r si) = output (HD _ si) r.
trivial with v62.
Qed.

Theorem Tl_Circ :
(r : TR) (si : Str TI),
TL _ (Circ r si) = Circ (update (HD _ si) r) (TL _ si).
trivial with v62.
Qed.

Definition Reg : Str TI × TR TR.
simple destruct 1; trivial with v62.
Defined.

Definition Input : Str TI × TR Str TI.
simple destruct 1; trivial with v62.
Defined.

Section CircProof.
Variable i0 : Str TI.
Variable r0 : TR.
Variable P : nat TO Prop.

Variable inv : nat TR Prop.
Hypothesis inv_init : inv 0 r0.
Hint Resolve inv_init.

Let inv_aux (n : nat) (s : Str TO) : Prop :=
r : TR, inv n r s = Circ r (NTHTL _ i0 n).

Remark inv_aux_init : inv_aux 0 (Circ r0 i0).
r0; auto with v62.
Qed.
Hint Resolve inv_aux_init.

Hypothesis
inv_stable :
(n : nat) (r : TR),
inv n r
P n (output (NTH _ i0 n) r) inv (S n) (update (NTH _ i0 n) r).

Remark inv_aux_stable :
(n : nat) (s : Str TO),
inv_aux n s P n (HD _ s) inv_aux (S n) (TL _ s).
simple induction 1; simple induction 1; intros.
rewrite H2; rewrite Tl_Circ; rewrite Hd_Circ.
elim (inv_stable n x); intros; trivial with v62.
split; trivial with v62.
(update (NTH _ i0 n) x); auto with v62.
Qed.
Hint Resolve inv_aux_stable.

Theorem Circ_property : n : nat, P n (NTH _ (Circ r0 i0) n).
intro; apply All_Q_Nth with (Inv := inv_aux); auto with v62.
Qed.

End CircProof.

End Circuits.

Notation Circ := (CIRC _ _ _) (only parsing).