(* ----------------------------------------------------------------------------define a Set of n elements 
-----------------------------------------------------------------------------*)


Set Implicit Arguments.
Unset Strict Implicit.

Inductive Finset : nat -> Set :=
  | fb : forall n : nat, Finset (S n)
  | fs : forall n : nat, Finset n -> Finset (S n).

Require Export JMeq.


Theorem Finset_decompose_aux :
 forall (n : nat) (x : Finset (S n)),
 JMeq x (fb n) \/ (exists y : Finset n, JMeq x (fs y)).
intros n x.
change
  (JMeq x (fb (pred (S n))) \/
   (exists y : Finset (pred (S n)), JMeq x (fs y))) 
 in |- *.
case x.
intros n'; left; reflexivity.
intros n' y; right; exists y; reflexivity.
Qed.
 
Theorem Finset_decompose :
 forall (n : nat) (x : Finset (S n)),
 x = fb n \/ (exists y : Finset n, x = fs y).
intros n x; elim (Finset_decompose_aux x).
intros Heq; left; rewrite Heq; reflexivity.
intros (y, Heq); right; exists y; rewrite Heq; reflexivity.
Qed.


Theorem Finset_decompose_aux_sumor :
 forall (n : nat) (x : Finset (S n)),
 {JMeq x (fb n)} + {exists y : Finset n, JMeq x (fs y)}.
intros n x.
change
  ({JMeq x (fb (pred (S n)))} +
  {exists y : Finset (pred (S n)), JMeq x (fs y)}) in |- *.
case x.
intros n'; left; reflexivity.
intros n' y; right; exists y; reflexivity.
Qed.
 
Theorem Finset_decompose_sumor :
 forall (n : nat) (x : Finset (S n)),
 {x = fb n} + {exists y : Finset n, x = fs y}.
intros n x; elim (Finset_decompose_aux_sumor x).
intros Heq; left; rewrite Heq; reflexivity.
intro H.
right.
elim H.
intros.
exists x0.
rewrite H0.
reflexivity.
Qed.


Theorem injection_fs :
 forall (n : nat) (y x' : Finset n), fs y = fs x' -> y = x'.
intros n y x' Heq.
cut (JMeq y x').
intros Heq2; rewrite Heq2; reflexivity.
change
  (JMeq
     (match
        fs y in (Finset p) return (Finset (pred p) -> Finset (pred p))
      with
      | fs p z => fun x : Finset p => z
      | fb p => fun x : Finset p => x
      end y) x') in |- *.
rewrite Heq.
reflexivity.
Qed.

Theorem not_eq_fs :
 forall (n : nat) (y x' : Finset n), y <> x' -> fs y <> fs x'.
intros n y x' Hneq Heq; apply Hneq; apply injection_fs; assumption.
Qed.


(*----------------------other proof possible ------------------------------*)
Definition fs_pred_aux (n : nat) (x : Finset n) (y : Finset (S n)) : Prop :=
  match y with
  | fb _ => False
  | fs n' z => JMeq z x
  end.

Lemma fin_inj : forall (n : nat) (x x' : Finset n), x <> x' -> fs x <> fs x'.
intros.
red in |- *.
intros.
absurd (fs_pred_aux x (fs x)).
rewrite H0.
simpl in |- *.
assert (JMeq x' x -> x' = x).
apply JMeq_eq.
intuition.
simpl in |- *.
reflexivity.
Qed.
(*------------------------------------------------------------------------*)

Section pred.
Variable k1 : nat.
Definition Pred_fins (x : Finset k1) : Prop :=
  match x with
  | fs _ _ => True
  | fb _ => False
  end.
End pred.

Lemma neq_fb_fs : forall (n : nat) (x : Finset n), fs x <> fb n.
unfold not in |- *.
intros.
absurd (Pred_fins (fb n)).
simpl in |- *.
auto.
rewrite <- H.
simpl in |- *.
auto.
Qed.

Section Fins2list.
Variable A:Type.

Lemma finset_Sn_n_A: forall (n : nat) ,((Finset (S n)) ->  A) -> (Finset n) ->  A.
intros.
apply X.
apply (fs  H).
Defined.

Lemma last_elt_An: forall (n : nat) ,((Finset (S n)) ->  A) ->  A.
intros.
apply X.
apply (fb n).
Defined.

Require Import listT.
Definition Finset2list(n:nat)(f:Finset n->A):listT A.
induction n.
simpl;intros.
apply (nilT A).
simpl;intros.
assert (Finset n->A).
apply (finset_Sn_n_A f).
apply (consT  (last_elt_An f) (IHn X)).
Defined.

End Fins2list.

Axiom dec_eq_fins : forall (k : nat) (a b : Finset k), {a = b} + {a <> b}.


(*
Fixpoint compo_fs(i n:nat){struct i}:Finset (n-i)->Finset n:=
fun x:Finset (n-i)=>match i return Finset (n-i)->Finset n with 
  O  =>fun y :Finset n=>y
 |S m=>fs (compo_fs m n)
 end.
*)

Definition compo_fs(i n:nat)(x:Finset (n-i)):Finset n.
intros i .
induction i;simpl.
intro;case n.
simpl.
intro h;apply h.
simpl;intros.
apply x.
intro;generalize (fun x:Finset (pred n-i)=>(fs (IHi (pred n) x))).
case n;simpl;intros.
apply x.
apply (H x).
Defined.

(*
Fixpoint ith_elt_fins(i n:nat){struct i}:Finset n:=
match i return (Finset (S (n-1))) with 
     O    =>fb (n-1)
  |S m  =>compo_fs (S m) n (ith_elt_fins m (n-(S m)))
end.
*)

Variable OF:Finset 0.
Definition ith_elt_fins(i n:nat):Finset n.
intro i;induction i.
intros.
case n.
apply OF.
intros.
apply (fb n0).
intros.
apply (compo_fs (IHi (n-(S i)))).
Defined.

(*il faut prendre m=n pr avoir la liste des n elts de Finset n *)
Fixpoint list_elt_fins(n m:nat){struct m}:listT (Finset n):=
match m with 
  O  =>consT (ith_elt_fins 0 n) (nilT _)
 |S m=>consT (ith_elt_fins m n) (list_elt_fins n  m)
end.

Lemma compo_fs_0:forall (i:nat)(e:Finset 0),compo_fs (i:=i) (n:=0) e=e.
induction i;simpl;auto with * .
Qed.

(*
Lemma eq_fs_ith:forall  x n:nat,x<>0->fs (ith_elt_fins x n) = ith_elt_fins x (S n).
induction x.
simpl;intros;intuition.
induction n.
simpl;intros.
rewrite compo_fs_0;auto with *.
intro.
*)

Axiom eq_fins_ith_elt:forall (n:nat)(e:Finset n),n<>0->(exists i:nat, e=ith_elt_fins i n).
(*
simpl;intros.
elim e.
simpl;intros.
exists 0.
simpl;auto with * .
simpl;intros.
elim H0.
simpl;intros.
rewrite H1.
*)