Base.v
``````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.
``````