Require Import ssreflect.
Require Import Dialogue.
Set Implicit Arguments.
Set Primitive Projections.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Set Universe Polymorphism.


Record tsig (A : Type) (B : A -> Type) : Type :=
  exist { fst : A; snd : B fst}.

Arguments fst {_ _} _.
Arguments snd {_ _} _.
Notation "{ x : A & P }" := (@tsig A (fun x => P)) : type_scope.

Record tsig2 (A:Type) (P Q : A -> Type) : Type :=
  exist2 { p1 : A; p2 : P p1 ; p3 : Q p1}.

Arguments p1 {_ _ _} _.
Arguments p2 {_ _ _} _.
Arguments p3 {_ _ _} _.
Notation "{ x : A & P & Q }" := (tsig2 A (fun x => P) (fun x => Q)) : type_scope.

Record triple (A : Type) (B : Type) (P : A -> B -> Type) : Type :=
  exist3 { q1 : A; q2 : B ; q3 : P q1 q2}.

Arguments q1 {_ _ _} _.
Arguments q2 {_ _ _} _.
Arguments q3 {_ _ _} _.
Notation "{a : A £ b : B £ P }" := (triple A B (fun a b => P)) : type_scope.


Section Generic.

Fixpoint Generic_aux (n : nat) (b : BranchingNat nat nat) : BranchingNat nat nat  :=
  match b with
  | B0 _ _ => Bêtanat (BNEta _ _) n
  | BS k => Generic_aux (S n) k
  | Bêtanat f x => Bêtanat (fun a => Generic_aux n (f a)) x
  end.


Lemma NaturGen_aux (d : BranchingNat nat nat) (p : nat -> nat) (n : nat) :
  BNdialogue (Generic_aux n d) p = p (n + (BNdialogue d p)).
Proof.
  elim: d n => [ n | d ihd n | f ihd x n] ; simpl.
  - rewrite - plus_n_O.
    induction (p n) ; trivial ; simpl.
    now f_equal.
  - rewrite - plus_n_Sm ; rewrite - plus_Sn_m.
    now rewrite (ihd (S n)).
  - exact: ihd.
Qed.



Lemma Generic_Devale_Dialogue  (n : BranchingNat nat nat) (k : nat) (alpha : nat -> nat) :
  BNdialogue (Generic_aux k  (Devale n alpha)) alpha =
  BNdialogue (Generic_aux k n) alpha.
Proof.
  induction n ; trivial ; simpl.
  exact: (H (alpha x)).
Qed.

End Generic.