Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype.

Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.

Section definitions.

(*Definition of simplex*)
(*For each (i,j), two simplices are created. ConjijList is the union of this pair of simplices*)

Definition set1ij (i j:nat):= ((i::j::nil)::((i+1)::j::nil)::((i+1)::(j+1)::nil)::nil).

Definition set2ij (i j:nat):= ((i::j::nil)::(i::(j+1)::nil)::((i+1)::(j+1)::nil)::nil).

Definition setijList (i j:nat):= (set1ij i j):: (set2ij i j):: nil.



(*Function to create facets given a sequence of sequences of booleans*)

(*Step 1: generate the simplices correponding to a sequence. 
This sequence will be the sequence i of the sequence of sequences*)

Fixpoint step1 (i j:nat)(ss: seq bool):= 
match ss with
nil => nil
| a::b  => if (a==true)
               then (setijList i j) ++ (step1 i (S j) b)
           else (step1 i (S j) b)
end.

Functional Scheme step1_ind := Induction for step1 Sort Prop.


(*Step 2: generate every simplices for the different sequences of ss*)
Fixpoint step2 (i:nat) (ss:seq(seq bool)):=
match ss with
nil => nil
|a::b => (step1 i 0 a) ++ (step2 (S i) b)
end.

Functional Scheme step2_ind := Induction for step2 Sort Prop.


(*Step 3: generate every the simplices of a sequence of sequences*)
Definition createfacets (ss:seq (seq bool)) := step2 0 ss.

Eval compute in (createfacets ((true::false::nil)::(false::true::nil)::nil)).

End definitions.


(*Auxiliar lemmas to prove the poperties which createfacets has to satisfy*)
Section lemmas.

Lemma differentset12 (i j i1 j1:nat): set1ij i j != set2ij i1 j1. 
Proof.
rewrite eqseq_cons. 
case H: ([:: i, j & [::]] == [:: i1, j1 & [::]]). 
  rewrite /=. rewrite !eqseq_cons in H.
  move: H; move/andP; move=> [H H1]. move: H1. move/andP; move=> [H1 H2].
  move: H H1. move/eqP; move=> ->. move/eqP; move=> ->.
  rewrite eqseq_cons. rewrite negb_and. apply/orP. 
  have: ([:: i1 + 1, j1 & [::]] != [:: i1, j1 + 1 & [::]]) = true.
    rewrite eqseq_cons. rewrite negb_and. apply/orP. 
    rewrite addn1. left. 
    have: i1 < i1.+1. by done. move=> H3. rewrite neq_ltn. by apply/orP; right.
  move=> H. rewrite H. apply/orP. by done.
by rewrite /=.
Qed.


Lemma equals11 (i j i1 j1: nat) : (set1ij i j = set1ij i1 j1) -> ((i1==i)/\(j1==j)).
Proof.
rewrite /set1ij //=. move/eqP. rewrite eqseq_cons; move=> H1.
case HH: (([:: i, j & [::]] == [:: i1, j1 & [::]])); last first.
  by rewrite HH /= in H1.
rewrite !eqseq_cons in HH.
move: HH. move/andP. move=> [H2 H3]. move: H3. move/andP. move=> [H3 _].
move: H2; move/eqP; move=> ->. move: H3; move/eqP; move=> ->.
by done.
Qed.


Lemma equals22 (i j i1 j1: nat) : (set2ij i j = set2ij i1 j1) -> ((i1==i)/\(j1==j)).
Proof.
rewrite /set1ij //=. move/eqP. rewrite eqseq_cons.
move=> H1.
case HH: (([:: i, j & [::]] == [:: i1, j1 & [::]])); last first.
  by rewrite HH /= in H1.
rewrite !eqseq_cons in HH.
move: HH. move/andP. move=> [H2 H3]. move: H3. move/andP. move=> [H3 _].
move: H2; move/eqP; move=> ->. move: H3; move/eqP; move=> ->.
by done.
Qed.



Fixpoint schemaAux1 (k:nat)(s : seq bool) := 
match s with
nil => k
| a::b  => if (a==true)
              then (schemaAux1 k.+1 b)
              else (schemaAux1 k.+1 b)
end.

Functional Scheme schemaAux1_ind := Induction for schemaAux1 Sort Prop.


Lemma aux1: forall (s:seq bool)(i j k:nat),
 (set1ij i j) \in (step1 i k s) -> (j>=k).
Proof.
move=> s i j k.
functional induction (schemaAux1 k s).
    by done.
  case H: (j==k).
    have: j = k. by move: H; move/eqP => ->. 
    by move=> ->.
  rewrite /step1 e0 mem_cat. move/orP => [H1|H2].
    move:H1; rewrite inE; move/orP=>[H1|H2].
      move:H1; move/eqP => H1. move: (equals11 H1).
      move=> [H2 H3]. move: H3; move/eqP=> H3; rewrite H3 in H. by move: H; move/eqP. 
    move: (differentset12 i j i k); move/eqP => H3.
    move:H2. rewrite inE. move/eqP. move=> H1. by rewrite H1 in H3.
  move:H2; rewrite -/step1. move=> H1; move: (IHn H1) => H2. by apply: (ltnW H2).
rewrite /step1 e0 /=. rewrite -/step1. move=> H1; move: (IHn H1) => H2. 
  by apply: (ltnW H2).
Qed.



Lemma aux2: forall (s:seq bool)(i j i1 k :nat),
   set1ij i j \in step1 i1 k s -> (i==i1).
Proof.
move=> s i j i1 k.
functional induction (schemaAux1 k s).
    by done.
  rewrite /step1 e0 mem_cat. move/orP=>[H1|H1].
    move:H1; rewrite inE; move/orP=>[H1|H1].
      move:H1; move/eqP=> H1. move: (equals11 H1)=>[H2 H3]. by move:H2; move/eqP=> ->. 
    move: H1. rewrite inE. move/eqP=> H1. move:(differentset12 i j i1 k). by rewrite H1; move/eqP. 
  rewrite -/step1 in H1. by apply: (IHn H1).
rewrite /step1 e0. rewrite -/step1; move=> H. by apply: (IHn H).
Qed.



Fixpoint schemaAux3 (k :nat)(s:seq(seq bool)):= 
match s with
nil => k
| a::b  =>  (schemaAux3 k.+1 b)
end.

Functional Scheme schemaAux3_ind := Induction for schemaAux3 Sort Prop.


Lemma aux3: forall (s:seq(seq bool))(i j k:nat),
  (set1ij i j \in step2 k s) -> (i>=k). 
Proof.
move=> s i j k.
functional induction (schemaAux3 k s).
  by done.
  case H: (k==i).
    move: H; move/eqP. by move=>->. 
  rewrite /step2 mem_cat. move/orP => [H1|H2].
  move: (aux2 H1). move/eqP => H2. rewrite H2 in H. by move: H; move/eqP.
rewrite -/step2 in H2. move: (IHn H2)=> H1. 
by rewrite leq_eqVlt H /=.
Qed.

End lemmas.



(*PROPERTIES*)
Section properties.


(*------------*)

(*The five following lemmas are need to prove the property 1. *)

(*The property 1: If one of the generated simplices (set1ij) are in the set of all the facets. 
The analogue simplice (set2ij) is also in the set of all the facets.*)
(*The following lemmas prove this property for smaller sets which are included in the function 
createfacets*)


Lemma p11: forall i j i1 j1, ((set1ij i j)\in (setijList i1 j1)) ->
        ((set2ij i j)\in (setijList i1 j1)).
Proof.
move => i j i1 j1. 
rewrite  !inE /=.
move/orP. move=> [H|H].
  move: H. move/eqP. move=> H. move: (equals11 H). move=> [H1 H2].
  move: H1 H2. move/eqP => ->. move/eqP => ->. by apply/orP; right.
move: (differentset12 i j i1 j1) => H1. by rewrite H in H1.
Qed.


Lemma p12: forall (i j i1 j1:nat)(ss: seq bool), ((set1ij i j)\in (step1 i1 j1 ss)) 
   -> ((set2ij i j)\in (step1 i1 j1 ss)).
Proof.
move => i j i1 j1 ss. 
pattern j1, ss, (step1 i1 j1 ss). 
apply : step1_ind.
      by done.
    move=> j0 ss0 a b H H1 H2.
    rewrite !mem_cat; move/orP => [H4|H4].
    apply/orP; left. by apply:p11.
  apply/orP; right. by apply: (H2 H4).
by done.
Qed.


Lemma p13: forall (i j k:nat)(ss: seq (seq bool)), ((set1ij i j)\in (step2 k ss)) -> ((set2ij i j)\in (step2 k ss)).
Proof.
move=> i j k ss. 
pattern k ,ss ,(step2 k ss). 
apply : step2_ind.
  move=> i0 r0 i00 omm. by done.
move=> i0 r0 n0 i0n HH H1.
rewrite !mem_cat. move/orP=>[H3|H3].
  apply/orP; left. by rewrite p12.
apply/orP; right. by apply: (H1 H3).
Qed.


Lemma p14 : forall (i j:nat)(ss: seq (seq bool)), ((set1ij i j)\in (createfacets ss)) -> ((set1ij i j)\in (step2  0 ss)).
Proof.
by rewrite /createfacets.
Qed.

Lemma p15 : forall (i j:nat)(ss: seq (seq bool)),  
     ((set2ij i j)\in (step2 0 ss)) -> ((set2ij i j) \in (createfacets ss)).
Proof.
by rewrite /createfacets.
Qed.


(*PROPERTY 1*)
Lemma prop1 (i j:nat)(ss: seq (seq bool)): ((set1ij i j)\in (createfacets ss)) -> ((set2ij i j)\in (createfacets ss)).
Proof.
move=> H. move: (p14 H). move=> H1. 
move: (p13 H1) => H3.
by apply: (p15 H3).
Qed.



(* ------------------- *)

(*The five following lemmas are need to prove the property 2. *)

(*The property 2: If one of the generated simplices (set2ij) are in the set of all the facets. 
The analogue simplice (set1ij) is also in the set of all the facets.*)

(*The following lemmas prove this property for smaller sets which are included in the function 
createfacets*)

Lemma p21: forall (i j i1 j1: nat), ((set2ij i j)\in (setijList i1 j1)) ->
        ((set1ij i j)\in (setijList i1 j1)).
Proof.
move => i j i1 j1.
rewrite /= !inE.
move/orP => [H|H].
  move: (differentset12 i1 j1 i j); move/eqP => H1.
  move: H; move/eqP => H. by rewrite H in H1.
move: H; move/eqP=> H. move: (equals22 H) => [H1 H2].
move: H1; move/eqP=> ->. move: H2; move/eqP=> ->.
by apply/orP; left.
Qed.


Lemma p22: forall (i j i1 j1:nat)(ss: seq bool), ((set2ij i j)\in (step1 i1 j1 ss)) 
   -> ((set1ij i j)\in (step1 i1 j1 ss)).
Proof.
move=> i j i1 j1 ss.
functional induction (step1 i1 j1 ss); first by done. (*; try by done.*)
  rewrite !mem_cat; move/orP =>[H|H]; apply/orP.
    by left; rewrite p21.
  by right; apply: (IHs H).
by done.
Qed.


Lemma p23: forall (i j k:nat)(ss: seq (seq bool)), ((set2ij i j)\in (step2 k ss)) -> ((set1ij i j)\in (step2 k ss)).
Proof.
move=> i j k ss.
functional induction (step2  k ss); first by done.
rewrite !mem_cat; move/orP =>[H|H]; apply/orP.
by left; rewrite p22.
by right; apply: (IHs H).
Qed.


Lemma p24: forall (i j:nat)(ss: seq (seq bool)), ((set2ij i j)\in (createfacets ss)) -> ((set2ij i j)\in (step2 0 ss)).
Proof.
by rewrite /createfacets.
Qed.


Lemma p25: forall (i j:nat)(ss: seq (seq bool)), 
     ((set1ij i j)\in (step2 0 ss)) -> ((set1ij i j)\in (createfacets ss)).
Proof.
by rewrite /createfacets.
Qed.

(*PROPERTY 2*)
Lemma prop2: forall (i j:nat)(ss:seq (seq bool)), ((set2ij i j) \in (createfacets ss)) -> ((set1ij i j)\in (createfacets ss)).
Proof.
move=> i j ss H; move: (p24 H) => H1. 
move: (p23 H1). move=> H3.
by apply: (p25 H3).
Qed.




(*-----------------------*)

(*the three following lemmas to prove the property 3 with two schemas of induction*)

(*The property 3: if the position (i,j) of the sequence of sequences is true, the generated simplice
 with the function setijList are in the set of all the facets. But, thanks to the previous properties
you only need to prove that one of simplices (set1ij or set2ij) are in the set of all the faces*)

(*The following lemmas prove this property for smaller sets (set generated by step1 and set generated
by step 2) which are included in the function createfacets*)

Fixpoint schema31 (j k :nat) (s : seq bool):= 
match s with
nil => j
| a::b  => if (a==true)
              then (schema31 j.+1 k.-1 b)
              else (schema31 j.+1 k.-1 b)
end.

Functional Scheme schema31_ind := Induction for schema31 Sort Prop.
Functional Scheme nth_ind := Induction for nth Sort Prop.


Lemma prop31: forall (s: seq bool)(k:nat)(i j:nat), 
 (nth false s k)  -> ((set1ij i (j+k)) \in (step1 i j s)).
Proof.
move=> s k i j.
functional induction (schema31 j k s).
    by rewrite nth_nil.
  case k0 : k.
    rewrite addn0; move => nth.
    rewrite //= e0 inE. by apply/orP; left.
  rewrite k0 /= in IHn. rewrite /=; move=> H.
  rewrite e0 inE. apply/orP; right. rewrite inE; apply/orP; right. 
  rewrite addSnnS in IHn. by apply: (IHn H).
case k0: k.
  rewrite addn0 /nth. move => H. by rewrite H in e0.
rewrite k0 /= in IHn. rewrite /=; move=> H.
rewrite e0. rewrite addSnnS in IHn.
by apply: (IHn H). 
Qed.


Lemma prop32: forall (s:seq bool)(k:nat)(i:nat), 
 (nth false s k)-> ((set1ij i k) \in (step1 i 0 s)).
Proof.
move=> s k i H1.
by apply: prop31.
Qed.



Fixpoint schema33 (k i :nat) (ss : seq (seq bool)):= 
match ss with
nil => k
| a::b  => (schema33 k.-1 i.+1 b)
end.

Functional Scheme schema33_ind := Induction for schema33 Sort Prop.


Lemma prop33: forall (s:seq (seq bool))(k:nat)(i j:nat),
  (nth false (nth nil s k) j) -> ((set1ij (i+k) j) \in (step2 i s)).
Proof.
move=> s k i j.
functional induction (schema33 k i s).
  by rewrite !nth_nil.
case k0: k.
  rewrite addn0; move => nth1. 
  rewrite //=  mem_cat. rewrite /= in nth1. apply/orP; left. 
  move: (@prop31 (_x) j i 0 nth1). by rewrite add0n. 
rewrite /=; move=> H. rewrite k0 in IHn. 
rewrite /= addSnnS in IHn. 
rewrite mem_cat; apply/orP; right.
by apply: (IHn H).
Qed.


(*PROPERTY 3*)
Lemma prop3: forall (s:seq (seq bool))(i j:nat),
  (nth false (nth nil s i) j) -> ((set1ij i j) \in (createfacets s)).
Proof.
rewrite /createfacets.
move=> s i j H.
move: (prop33 0 H). by rewrite add0n.
Qed.


(*--------------*)

(*the three following lemmas to prove the property 4*)

(*The property 4: if the generated simplices with the function setijList are in the set of all 
the facets then the position (i,j) of the sequence of sequences values true. As it's said before
you only need to prove that if one of simplices (set1ij or set2ij) are in the set of all the facets,
the position (i,j) of the sequence of sequences values true.*)

(*The following lemmas prove this property for smaller sets (set generated by step1 and set generated
by step 2) which are included in the function createfacets*)

Fixpoint schema41 (j k :nat)(s : seq bool) := 
match s with
nil => j
| a::b  => if (a==true)
              then (schema41 j.+1 k.-1 b)
              else (schema41 j.+1 k.-1 b)
end.

Functional Scheme schema41_ind := Induction for schema41 Sort Prop.


Lemma prop41: forall (s:(seq bool))(i j k:nat),
  ((set1ij i (j+k)) \in (step1 i j s)) -> (nth false s k).
Proof.
move=> s i j k.
functional induction (schema41 j k s);first by done.
  case k0 : k => [ | n].
    rewrite addn0 //=. move => nth. by move: e0; move/eqP.
  rewrite k0 addSnnS /= in IHn. 
  move:e0; move/eqP => e0; rewrite e0 inE. move/orP=>[H|H].
    move: H. 
    move/eqP => H. move: (equals11 H)=>[H1 H2]. 
    have: j < j +n.+1. rewrite -{1}(addn0 j). by rewrite ltn_add2l. 
    move:H2. move/eqP=>H2. rewrite -H2. by rewrite ltnn.
  move: H; rewrite inE.
  move: (differentset12 i (j+n.+1) i j)=> H. move/orP=>[H1|H1].
    by rewrite H1 in H.
  move: H1; rewrite -/step1; move=> H1.
  by apply: (IHn H1).
case k0: k.
  rewrite addn0 /step1 e0 -/step1.
  rewrite addSnnS in IHn.
  move=> H; move: (aux1 H). by rewrite ltnn.
rewrite /step1  e0. rewrite k0 addSnnS /= in IHn.
move=> H. by apply: (IHn H).
Qed.

Lemma prop42: forall (s:seq bool)(k:nat)(i:nat), 
 ((set1ij i k) \in (step1 i 0 s)) -> (nth false s k).
Proof.
move=> s k i.
by apply: prop41.
Qed.


Lemma prop43: forall (s:seq (seq bool))(k:nat)(i j:nat),
   ((set1ij (i+k) j) \in (step2 i s)) -> (nth false (nth nil s k) j).
Proof.
move=> s k i j.
functional induction (schema33 k i s);first by done.
case k0 : k =>[|n].
  rewrite addn0 /step2 mem_cat;  move/orP=>[H1|H1].
    by apply: (prop42 H1).
  rewrite -/step2 in H1.
  move: (aux3 H1). by rewrite -{2}(addn0 i)  -(addn1 i)  (leq_add2l i 1 0). 
rewrite /= mem_cat. rewrite /= addSnnS k0 in IHn. 
move/orP=>[H1|H1].
  move: (aux2 H1). rewrite -{2}(addn0 i)  (eqn_addl i n.+1 0). by done.
by apply: (IHn H1).
Qed.


(*PROPERTY 4*)
Lemma prop4: forall (s:seq (seq bool))(i j:nat),
  ((set1ij i j) \in (createfacets s)) -> (nth false (nth nil s i) j).
Proof.
rewrite /createfacets.
move=> s i j H.
by apply: (prop43 H).
Qed.