(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


(* definit une table a une ou deux dimensions puis la sommation sur la
table *)

Require Import List.
Require Export finite.

Unset Standard Proposition Elimination Names.

Section TABLE1.

(* une table a lements dans F indexee par E est une fonction de E dans
F dans laquelle on ne modifie qu'un terme a la fois *)

Variable E F : Set.
Hypothesis eq_E_dec : eq_dec E.
Variable t : E -> F.
Variable x0 : E.
Variable y0 : F.

Definition change_x0 (x : E) :=
  if eq_E_dec x0 x then y0 else t x.

Lemma here : change_x0 x0 = y0.
Proof.
(* Goal: @eq F (change_x0 x0) y0 *)
 unfold change_x0 in |- *; rewrite case_eq; trivial.
Qed.
	
Lemma elsewhere : forall x : E, x0 <> x -> change_x0 x = t x.
Proof.
(* Goal: forall (x : E) (_ : @In E x L), @eq Z (g x) (change_x0 E Z eq_E_dec f x0 (Z.sub (f x0) (Zpos xH)) x) *)
 intros; unfold change_x0 in |- *.
(* Goal: @eq F (if eq_E_dec x0 x then y0 else t x) (t x) *)
 rewrite case_ineq; trivial.
Qed.

End TABLE1.

Section TABLE2.

(* une table a deux dimensions est indexee par deux ensembles *)

Variable E F G : Set.
Hypothesis eq_E_dec : eq_dec E.
Hypothesis eq_F_dec : eq_dec F.
Variable t : E -> F -> G.
Variable x0 : E.
Variable y0 : F.
Variable z0 : G.

Definition change_x0y0 :=
  change_x0 E (F -> G) eq_E_dec t x0 (change_x0 F G eq_F_dec (t x0) y0 z0).

Lemma here2 : change_x0y0 x0 y0 = z0.
Proof.
(* Goal: forall (x : E) (_ : not (@eq E x x0)), @eq (forall _ : F, G) (change_x0y0 x) (t x) *)
 intros; unfold change_x0y0 in |- *; simpl in |- *.
(* Goal: @eq G (change_x0 E (forall _ : F, G) eq_E_dec t x0 (change_x0 F G eq_F_dec (t x0) y0 z0) x0 y0) z0 *)
 do 2 rewrite here; auto.
Qed.
                     
Remark elsewhere2_x : forall x : E, x <> x0 -> change_x0y0 x = t x.
Proof.
(* Goal: forall (x : E) (_ : not (@eq E x x0)), @eq (forall _ : F, G) (change_x0y0 x) (t x) *)
 intros; unfold change_x0y0 in |- *; simpl in |- *.
(* Goal: @eq G (change_x0 E (forall _ : F, G) eq_E_dec t x0 (change_x0 F G eq_F_dec (t x0) y0 z0) e y) (t e y) *)
 rewrite elsewhere; auto.
Qed.

Remark elsewhere2_y :
 forall y : F,
 y <> y0 -> (fun x : E => change_x0y0 x y) = (fun x : E => t x y).
Proof.
(* Goal: forall (y : F) (_ : not (@eq F y y0)), @eq (forall _ : E, G) (fun x : E => change_x0y0 x y) (fun x : E => t x y) *)
 intros; apply funct_eq.
(* Goal: forall e : E, @eq G (change_x0y0 e y) (t e y) *)
 intros; unfold change_x0y0 in |- *.
(* Goal: @eq G (change_x0 E (forall _ : F, G) eq_E_dec t x0 (change_x0 F G eq_F_dec (t x0) y0 z0) e y) (t e y) *)
 case (eq_E_dec e x0); intros.
(* Goal: @eq G (change_x0 E (forall _ : F, G) eq_E_dec t x0 (change_x0 F G eq_F_dec (t x0) y0 z0) e y) (t e y) *)
(* Goal: @eq G (change_x0 E (forall _ : F, G) eq_E_dec t x0 (change_x0 F G eq_F_dec (t x0) y0 z0) e y) (t e y) *)
 rewrite e0; rewrite here.
(* Goal: @eq G (change_x0 E (forall _ : F, G) eq_E_dec t x0 (change_x0 F G eq_F_dec (t x0) y0 z0) e y) (t e y) *)
 rewrite elsewhere; auto.
	
(* Goal: @eq G (change_x0 E (forall _ : F, G) eq_E_dec t x0 (change_x0 F G eq_F_dec (t x0) y0 z0) e y) (t e y) *)
 rewrite elsewhere; auto.
Qed.

Lemma elsewhere2 :
 forall (x : E) (y : F), x <> x0 \/ y <> y0 -> change_x0y0 x y = t x y. 
Proof.
(* Goal: forall (x : E) (y : F) (_ : or (not (@eq E x x0)) (not (@eq F y y0))), @eq G (change_x0y0 x y) (t x y) *)
 intros; elim H; intros.
(* Goal: @eq G (change_x0y0 x y) (t x y) *)
(* Goal: @eq G (change_x0y0 x y) (t x y) *)
 rewrite elsewhere2_x; auto.

 apply
  f_equal
   with
     (f := fun g : E -> G => g x)
     (x := fun x' : E => change_x0y0 x' y)
     (y := fun x' : E => t x' y). 
(* Goal: @eq (forall _ : E, G) (fun x' : E => change_x0y0 x' y) (fun x' : E => t x' y) *)
 apply elsewhere2_y; auto.
Qed.
	
End TABLE2.
 
Section CHANGE_SUM1.

(* la table est a elements dans Z, il est alors possible de sommer sur
une liste d'index *)

Variable E : Set.
Hypothesis eq_E_dec : eq_dec E.
Variable f : E -> Z.
Variable x0 : E.
Variable y0 : Z.

Lemma sigma_nowhere :
 forall l : list E,
 ~ In x0 l -> sigma E l (change_x0 E Z eq_E_dec f x0 y0) = sigma E l f. 
Proof.
(* Goal: forall (l : list E) (_ : not (@In E x0 l)), @eq Z (sigma E l (change_x0 E Z eq_E_dec f x0 y0)) (sigma E l f) *)
 intros; apply sigma_simpl.
(* Goal: forall (x : E) (_ : @In E x l), @eq Z (change_x0 E Z eq_E_dec f x0 y0 x) (f x) *)
 intros; apply elsewhere.
(* Goal: not (@eq E x0 x) *)
 apply sym_not_eq; apply in_not_in with (l := l); auto.
Qed.

Lemma sigma_change :
 forall l : list E,
 only_once E eq_E_dec x0 l ->
 sigma E l (change_x0 E Z eq_E_dec f x0 y0) = (sigma E l f - f x0 + y0)%Z.
Proof.
(* Goal: forall (l : list E) (_ : only_once E eq_E_dec x0 l), @eq Z (sigma E l (change_x0 E Z eq_E_dec f x0 y0)) (Z.add (Z.sub (sigma E l f) (f x0)) y0) *)
 simple induction l; simpl in |- *.
(* Goal: forall _ : False, @eq Z Z0 (Z.add (Z.opp (f x0)) y0) *)
(* Goal: forall (a : E) (l : list E) (_ : forall _ : only_once E eq_E_dec x0 l, @eq Z (sigma E l (change_x0 E Z eq_E_dec f x0 y0)) (Z.add (Z.sub (sigma E l f) (f x0)) y0)) (_ : if eq_E_dec x0 a then not (@In E x0 l) else only_once E eq_E_dec x0 l), @eq Z (Z.add (change_x0 E Z eq_E_dec f x0 y0 a) (sigma E l (change_x0 E Z eq_E_dec f x0 y0))) (Z.add (Z.sub (Z.add (f a) (sigma E l f)) (f x0)) y0) *)
 contradiction.

(* Goal: forall (a : E) (l : list E) (_ : forall _ : only_once E eq_E_dec x0 l, @eq Z (sigma E l (change_x0 E Z eq_E_dec f x0 y0)) (Z.add (Z.sub (sigma E l f) (f x0)) y0)) (_ : if eq_E_dec x0 a then not (@In E x0 l) else only_once E eq_E_dec x0 l), @eq Z (Z.add (change_x0 E Z eq_E_dec f x0 y0 a) (sigma E l (change_x0 E Z eq_E_dec f x0 y0))) (Z.add (Z.sub (Z.add (f a) (sigma E l f)) (f x0)) y0) *)
 intros a l0 hrec; case (eq_E_dec x0 a); intros.
(* Goal: @eq Z (Z.add (change_x0 E Z eq_E_dec f x0 y0 a) (sigma E l0 (change_x0 E Z eq_E_dec f x0 y0))) (Z.add (Z.sub (Z.add (f a) (sigma E l0 f)) (f x0)) y0) *)
(* Goal: @eq Z (Z.add (change_x0 E Z eq_E_dec f x0 y0 a) (sigma E l0 (change_x0 E Z eq_E_dec f x0 y0))) (Z.add (Z.sub (Z.add (f a) (sigma E l0 f)) (f x0)) y0) *)
 rewrite <- e; rewrite here.
(* Goal: @eq Z (Z.add y0 (sigma E l0 (change_x0 E Z eq_E_dec f x0 y0))) (Z.add (Z.sub (Z.add (f x0) (sigma E l0 f)) (f x0)) y0) *)
(* Goal: @eq Z (Z.add (change_x0 E Z eq_E_dec f x0 y0 a) (sigma E l0 (change_x0 E Z eq_E_dec f x0 y0))) (Z.add (Z.sub (Z.add (f a) (sigma E l0 f)) (f x0)) y0) *)
 rewrite sigma_nowhere.
(* Goal: @eq Z (Z.add (Z.sub (sigma E L f) (f x0)) (Z.sub (f x0) (Zpos xH))) (Z.sub (sigma E L f) (Zpos xH)) *)
(* Goal: only_once E eq_E_dec x0 L *)
 omega.
	
(* Goal: not (@eq E x0 a) *)
 trivial.
	
(* Goal: @eq Z (Z.add (change_x0 E Z eq_E_dec f x0 y0 a) (sigma E l0 (change_x0 E Z eq_E_dec f x0 y0))) (Z.add (Z.sub (Z.add (f a) (sigma E l0 f)) (f x0)) y0) *)
 rewrite elsewhere.
(* Goal: @eq Z (Z.add (f a) (sigma E l0 (change_x0 E Z eq_E_dec f x0 y0))) (Z.add (Z.sub (Z.add (f a) (sigma E l0 f)) (f x0)) y0) *)
(* Goal: not (@eq E x0 a) *)
 rewrite hrec.
(* Goal: @eq Z (Z.add (Z.sub (sigma E L f) (f x0)) (Z.sub (f x0) (Zpos xH))) (Z.sub (sigma E L f) (Zpos xH)) *)
(* Goal: only_once E eq_E_dec x0 L *)
 omega.
	
(* Goal: not (@eq E x0 a) *)
 trivial.

(* Goal: not (@eq E x0 a) *)
 trivial.
Qed.
 	
End CHANGE_SUM1.

Section SUM1_S.

(* l'ensemble d'index etant un ensemble fini, il est possible de
sommer sur cet ensemble, donc d'apres la definition choisie d'ensemble
fini, sur la liste de tout ses elements. On ne s'interesse qu'aux
incrementation ou decrementation d'un element de la table *)

Variable E : Set.
Hypothesis eq_E_dec : eq_dec E.
Variable L : list E.
Hypothesis finite_E : list_of_elements E eq_E_dec L.
Variable f : E -> Z.
Variable x0 : E.

Remark sigma_change_S :
 sigma E L (change_x0 E Z eq_E_dec f x0 (f x0 + 1)%Z) = (sigma E L f + 1)%Z.    
Proof.
(* Goal: @eq Z (sigma E L (change_x0 E Z eq_E_dec f x0 (Z.sub (f x0) (Zpos xH)))) (Z.sub (sigma E L f) (Zpos xH)) *)
 rewrite sigma_change.
(* Goal: @eq Z (Z.add (Z.sub (sigma E L f) (f x0)) (Z.sub (f x0) (Zpos xH))) (Z.sub (sigma E L f) (Zpos xH)) *)
(* Goal: only_once E eq_E_dec x0 L *)
 omega. 
	
(* Goal: @eq Z (g x) (f x) *)
 auto.
Qed.

Lemma sigma__S :
 forall g : E -> Z,
 g x0 = (f x0 + 1)%Z ->
 (forall x : E, x <> x0 -> g x = f x) -> sigma E L g = (sigma E L f + 1)%Z.    
Proof.
(* Goal: forall (g : forall _ : E, Z) (_ : @eq Z (g x0) (Z.add (f x0) (Zpos xH))) (_ : forall (x : E) (_ : not (@eq E x x0)), @eq Z (g x) (f x)), @eq Z (sigma E L g) (Z.add (sigma E L f) (Zpos xH)) *)
 intros; rewrite <- sigma_change_S.
(* Goal: @eq Z (sigma E L g) (sigma E L (change_x0 E Z eq_E_dec f x0 (Z.sub (f x0) (Zpos xH)))) *)
 apply sigma_simpl.
(* Goal: forall (x : E) (_ : @In E x L), @eq Z (g x) (change_x0 E Z eq_E_dec f x0 (Z.sub (f x0) (Zpos xH)) x) *)
 intros; unfold change_x0 in |- *.
(* Goal: @eq Z (g x) (if eq_E_dec x0 x then Z.sub (f x0) (Zpos xH) else f x) *)
 case (eq_E_dec x0 x); simpl in |- *; intro.
(* Goal: @eq Z (g x) (f x) *)
 rewrite <- e; auto.

(* Goal: @eq Z (g x) (f x) *)
 auto.
Qed.
   
Remark sigma_change_pred :
 sigma E L (change_x0 E Z eq_E_dec f x0 (f x0 - 1)%Z) = (sigma E L f - 1)%Z.    
Proof.
(* Goal: @eq Z (sigma E L (change_x0 E Z eq_E_dec f x0 (Z.sub (f x0) (Zpos xH)))) (Z.sub (sigma E L f) (Zpos xH)) *)
 rewrite sigma_change.
(* Goal: @eq Z (Z.add (Z.sub (sigma E L f) (f x0)) (Z.sub (f x0) (Zpos xH))) (Z.sub (sigma E L f) (Zpos xH)) *)
(* Goal: only_once E eq_E_dec x0 L *)
 omega.
		
(* Goal: @eq Z (g x) (f x) *)
 auto.
Qed.
   
Lemma sigma__pred :
 forall g : E -> Z,
 g x0 = (f x0 - 1)%Z ->
 (forall x : E, x <> x0 -> g x = f x) -> sigma E L g = (sigma E L f - 1)%Z.    
Proof.
(* Goal: forall (g : forall _ : E, Z) (_ : @eq Z (g x0) (Z.sub (f x0) (Zpos xH))) (_ : forall (x : E) (_ : not (@eq E x x0)), @eq Z (g x) (f x)), @eq Z (sigma E L g) (Z.sub (sigma E L f) (Zpos xH)) *)
 intros; rewrite <- sigma_change_pred.
(* Goal: @eq Z (sigma E L g) (sigma E L (change_x0 E Z eq_E_dec f x0 (Z.sub (f x0) (Zpos xH)))) *)
 apply sigma_simpl.
(* Goal: forall (x : E) (_ : @In E x L), @eq Z (g x) (change_x0 E Z eq_E_dec f x0 (Z.sub (f x0) (Zpos xH)) x) *)
 intros; unfold change_x0 in |- *.
(* Goal: @eq Z (g x) (if eq_E_dec x0 x then Z.sub (f x0) (Zpos xH) else f x) *)
 case (eq_E_dec x0 x); simpl in |- *; intro.
(* Goal: @eq Z (g x) (f x) *)
 rewrite <- e; auto.

(* Goal: @eq Z (g x) (f x) *)
 auto.
Qed.
 
End SUM1_S.
