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).