(* 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                                                     *)


(*FINITE*)

(*definit les ensembles finis et la sommation *)

Require Import List.
Require Export bibli.

Unset Standard Proposition Elimination Names.

Section DEFIN.

(* un ensemble fini est un ensemble tel qu'il existe une liste
contenant chaque element une fois et une seule *)

Variable E : Set.

Hypothesis eq_E_dec : eq_dec E.

Fixpoint only_once (x : E) (l : list E) {struct l} : Prop :=
  match l with
  | nil => False
  | y :: l' =>
      if eq_E_dec x y then ~ In x l' else only_once x l'
  end.

Definition list_of_elements (l : list E) := forall x : E, only_once x l.

Lemma only_once_in : forall (l : list E) (x : E), only_once x l -> In x l.
Proof.
(* Goal: forall (l : list E) (f g : forall _ : E, Z) (_ : forall (x : E) (_ : not (@eq E x x0)) (_ : @In E x l), @eq Z (f x) (g x)), @eq Z (sigma_but l f) (sigma_but l g) *)
 simple induction l.
(* Goal: not (@eq E a x0) *)
(* Goal: or (@eq E a a) (@In E a l0) *)
 auto.
(* Goal: forall (a : E) (l : list E) (_ : forall (x : E) (_ : only_once x l), @In E x l) (x : E) (_ : only_once x (@cons E a l)), @In E x (@cons E a l) *)
 simpl in |- *; intros a l0 hrec x.
(* Goal: not (@eq E a x0) *)
(* Goal: or (@eq E a a) (@In E a l0) *)
 case (eq_E_dec x a); auto.
Qed.

Lemma equality_from_membership :
 forall (x y : E) (l : list E), In y l -> ~ In x l -> x <> y.
Proof.
(* Goal: forall (l : list E) (f g : forall _ : E, Z) (_ : forall (x : E) (_ : not (@eq E x x0)) (_ : @In E x l), @eq Z (f x) (g x)), @eq Z (sigma_but l f) (sigma_but l g) *)
  simple induction l.
(* Goal: forall _ : only_once E eq_E_dec x0 (@nil E), @eq Z (sigma E (@nil E) f) (Z.add (sigma_but (@nil E) f) (f x0)) *)
(* Goal: forall (a : E) (l : list E) (_ : forall _ : only_once E eq_E_dec x0 l, @eq Z (sigma E l f) (Z.add (sigma_but l f) (f x0))) (_ : only_once E eq_E_dec x0 (@cons E a l)), @eq Z (sigma E (@cons E a l) f) (Z.add (sigma_but (@cons E a l) f) (f x0)) *)
  simpl in |- *; intuition.
  
(* Goal: forall (a : E) (l : list E) (_ : forall (_ : @In E y l) (_ : not (@In E x l)), not (@eq E x y)) (_ : @In E y (@cons E a l)) (_ : not (@In E x (@cons E a l))), not (@eq E x y) *)
  intros a l' H.
(* Goal: @eq Z (sigma E (@cons E a l0) f) (Z.add (sigma_but (@cons E a l0) f) (f x0)) *)
  simpl in |- *.
(* Goal: forall (_ : or (@eq E a y) (@In E y l')) (_ : not (or (@eq E a x) (@In E x l'))), not (@eq E x y) *)
  case (eq_E_dec a y).
(* Goal: forall _ : @eq E a x0, @eq Z (sigma_but l0 f0) (sigma_but l0 g) *)
(* Goal: forall _ : not (@eq E a x0), @eq Z (Z.add (f0 a) (sigma_but l0 f0)) (Z.add (g a) (sigma_but l0 g)) *)
  intro e.
(* Goal: forall _ : if eq_E_dec x0 a then not (@In E x0 l0) else only_once E eq_E_dec x0 l0, not (@In E x0 l0) *)
(* Goal: forall _ : not (@eq E a x0), @eq Z (sigma E (@cons E a l0) f) (Z.add (sigma_but (@cons E a l0) f) (f x0)) *)
  rewrite e.
(* Goal: forall (_ : or (@eq E y y) (@In E y l')) (_ : not (or (@eq E y x) (@In E x l'))), not (@eq E x y) *)
(* Goal: forall (_ : not (@eq E a y)) (_ : or (@eq E a y) (@In E y l')) (_ : not (or (@eq E a x) (@In E x l'))), not (@eq E x y) *)
  intro H0.
(* Goal: forall (_ : not (@eq E x0 x0)) (_ : only_once E eq_E_dec x0 l0), not (@In E x0 l0) *)
(* Goal: forall _ : not (@eq E a x0), @eq Z (sigma E (@cons E a l0) f) (Z.add (sigma_but (@cons E a l0) f) (f x0)) *)
  intuition.
  
(* Goal: forall (_ : not (@eq E a y)) (_ : or (@eq E a y) (@In E y l')) (_ : not (or (@eq E a x) (@In E x l'))), not (@eq E x y) *)
  intros n H0 H1.
(* Goal: not (@eq E x y) *)
  apply H.
(* Goal: not (@eq E a x0) *)
(* Goal: or (@eq E a a) (@In E a l0) *)
  auto.
(* Goal: forall (_ : not (@eq E x0 x0)) (_ : only_once E eq_E_dec x0 l0), not (@In E x0 l0) *)
(* Goal: forall _ : not (@eq E a x0), @eq Z (sigma E (@cons E a l0) f) (Z.add (sigma_but (@cons E a l0) f) (f x0)) *)
  intuition.
(* Goal: forall (_ : not (@eq E x0 x0)) (_ : only_once E eq_E_dec x0 l0), not (@In E x0 l0) *)
(* Goal: forall _ : not (@eq E a x0), @eq Z (sigma E (@cons E a l0) f) (Z.add (sigma_but (@cons E a l0) f) (f x0)) *)
  intuition.
Qed.


End DEFIN.

Section SUM.

(* on definit la somme d'une fonction de E dans F sur une liste
d'elements de E par induction, puis on demontre quelques proprietes
elementaires *)

Variable E : Set.

Fixpoint sigma (l1 : list E) : (E -> Z) -> Z :=
  fun f : E -> Z =>
  match l1 with
  | nil => 0%Z
  | e :: l2 => (f e + sigma l2 f)%Z
  end.
	
Lemma sigma_null : forall l : list E, sigma l (fun e : E => 0%Z) = 0%Z.
Proof. 
(* Goal: not (@eq E a x0) *)
(* Goal: or (@eq E a a) (@In E a l0) *)
 simple induction l; auto.  
Qed.

Lemma sigma_pos :
 forall (f : E -> Z) (l : list E),
 (forall x_ : E, (f x_ >= 0)%Z) -> (sigma l f >= 0)%Z.
Proof.
(* Goal: @eq Z (sigma E (@cons E a l0) f) (Z.add (sigma_but (@cons E a l0) f) (f x0)) *)
 intros; elim l; simpl in |- *.
(* Goal: @eq Z (Z.add (f a) (Z.add (sigma_but l0 f) (f x0))) (Z.add (Z.add (f a) (sigma_but l0 f)) (f x0)) *)
(* Goal: only_once E eq_E_dec x0 l0 *)
(* Goal: not (@eq E a x0) *)
 omega.

(* Goal: @eq Z (Z.add (f a) (Z.add (sigma_but l0 f) (f x0))) (Z.add (Z.add (f a) (sigma_but l0 f)) (f x0)) *)
(* Goal: only_once E eq_E_dec x0 l0 *)
(* Goal: not (@eq E a x0) *)
 intros; generalize (H a); omega.
Qed.

Lemma le_sigma :
 forall (l : list E) (f : E -> Z) (x : E),
 (forall x_ : E, (f x_ >= 0)%Z) -> In x l -> (f x <= sigma l f)%Z.
Proof.
(* Goal: forall (l : list E) (f g : forall _ : E, Z) (_ : forall x : E, Z.le (f x) (g x)), Z.le (sigma l f) (sigma l g) *)
 simple induction l; simpl in |- *; intros.
(* Goal: Z.le (f x) Z0 *)
(* Goal: Z.le (f x) (Z.add (f a) (sigma l0 f)) *)
 contradiction.

(* Goal: Z.le (f x) (Z.add (f a) (sigma l0 f)) *)
 decompose [or] H1.
(* Goal: @eq Z (Z.add (f a) (Z.add (sigma_but l0 f) (f x0))) (Z.add (Z.add (f a) (sigma_but l0 f)) (f x0)) *)
(* Goal: only_once E eq_E_dec x0 l0 *)
(* Goal: not (@eq E a x0) *)
 rewrite H2; generalize (sigma_pos f l0 H0); omega.

(* Goal: @eq Z (Z.add (f a) (Z.add (sigma_but l0 f) (f x0))) (Z.add (Z.add (f a) (sigma_but l0 f)) (f x0)) *)
(* Goal: only_once E eq_E_dec x0 l0 *)
(* Goal: not (@eq E a x0) *)
 generalize (H0 a); generalize (H f x H0 H2); omega.
Qed.

Lemma sigma_simpl :
 forall (l : list E) (f g : E -> Z),
 (forall x : E, In x l -> f x = g x) -> sigma l f = sigma l g.
Proof.
(* Goal: forall (l : list E) (f g : forall _ : E, Z) (_ : forall (x : E) (_ : not (@eq E x x0)) (_ : @In E x l), @eq Z (f x) (g x)), @eq Z (sigma_but l f) (sigma_but l g) *)
 simple induction l.
(* Goal: not (@eq E a x0) *)
(* Goal: or (@eq E a a) (@In E a l0) *)
 auto.

(* Goal: forall (a : E) (l : list E) (_ : forall (f g : forall _ : E, Z) (_ : forall (x : E) (_ : not (@eq E x x0)) (_ : @In E x l), @eq Z (f x) (g x)), @eq Z (sigma_but l f) (sigma_but l g)) (f g : forall _ : E, Z) (_ : forall (x : E) (_ : not (@eq E x x0)) (_ : @In E x (@cons E a l)), @eq Z (f x) (g x)), @eq Z (sigma_but (@cons E a l) f) (sigma_but (@cons E a l) g) *)
 simpl in |- *; intros.
(* Goal: @eq Z (Z.add (f a) (sigma l0 f)) (Z.add (g a) (sigma l0 g)) *)
 rewrite (H f g).
(* Goal: not (@eq E a x0) *)
(* Goal: or (@eq E a a) (@In E a l0) *)
 rewrite (H0 a); auto.

(* Goal: not (@eq E a x0) *)
(* Goal: or (@eq E a a) (@In E a l0) *)
 auto.
Qed.

Remark le_sigma_sigma :
 forall (l : list E) (f g : E -> Z),
 (forall x : E, (f x <= g x)%Z) -> (sigma l f <= sigma l g)%Z.
Proof.
(* Goal: forall (l : list E) (f g : forall _ : E, Z) (_ : forall x : E, Z.le (f x) (g x)), Z.le (sigma l f) (sigma l g) *)
 simple induction l; simpl in |- *; intros.
(* Goal: Z.le Z0 Z0 *)
(* Goal: Z.le (Z.add (f a) (sigma l0 f)) (Z.add (g a) (sigma l0 g)) *)
 trivial with zarith.

(* Goal: @eq Z (Z.add (f a) (Z.add (sigma_but l0 f) (f x0))) (Z.add (Z.add (f a) (sigma_but l0 f)) (f x0)) *)
(* Goal: only_once E eq_E_dec x0 l0 *)
(* Goal: not (@eq E a x0) *)
 generalize (H f g H0); generalize (H0 a); omega.
Qed.

Lemma ge_sigma_sigma :
 forall (l : list E) (f g : E -> Z),
 (forall x : E, (f x >= g x)%Z) -> (sigma l f >= sigma l g)%Z.
Proof.
(* Goal: forall (l : list E) (f g : forall _ : E, Z) (_ : forall x : E, Z.ge (f x) (g x)), Z.ge (sigma l f) (sigma l g) *)
 intros; apply Zle_ge; apply le_sigma_sigma; intros; apply Zge_le; trivial.
Qed.

Hypothesis eq_E_dec : eq_dec E.

Lemma lt_sigma_sigma :
 forall (l : list E) (f g : E -> Z),
 (forall x : E, (f x <= g x)%Z) ->
 (exists y : E, (f y < g y)%Z /\ In y l) -> (sigma l f < sigma l g)%Z.
Proof.
(* Goal: forall (a : E) (l : list E) (_ : forall (f g : forall _ : E, Z) (_ : forall (x : E) (_ : not (@eq E x x0)) (_ : @In E x l), @eq Z (f x) (g x)), @eq Z (sigma_but l f) (sigma_but l g)) (f g : forall _ : E, Z) (_ : forall (x : E) (_ : not (@eq E x x0)) (_ : @In E x (@cons E a l)), @eq Z (f x) (g x)), @eq Z (sigma_but (@cons E a l) f) (sigma_but (@cons E a l) g) *)
 intros; elim H0; elim l; simpl in |- *; intros.
(* Goal: Z.le (f x) Z0 *)
(* Goal: Z.le (f x) (Z.add (f a) (sigma l0 f)) *)
 elim H1; contradiction.

(* Goal: Z.lt (Z.add (f a) (sigma l0 f)) (Z.add (g a) (sigma l0 g)) *)
 decompose [and or] H2.
(* Goal: @eq Z (Z.add (f a) (Z.add (sigma_but l0 f) (f x0))) (Z.add (Z.add (f a) (sigma_but l0 f)) (f x0)) *)
(* Goal: only_once E eq_E_dec x0 l0 *)
(* Goal: not (@eq E a x0) *)
 rewrite H5; generalize (le_sigma_sigma l0 f g H); omega.

(* Goal: Z.lt (Z.add (f a) (sigma l0 f)) (Z.add (g a) (sigma l0 g)) *)
 cut (sigma l0 f < sigma l0 g)%Z.
(* Goal: @eq Z (Z.add (f a) (Z.add (sigma_but l0 f) (f x0))) (Z.add (Z.add (f a) (sigma_but l0 f)) (f x0)) *)
(* Goal: only_once E eq_E_dec x0 l0 *)
(* Goal: not (@eq E a x0) *)
 generalize (H a); omega.

(* Goal: not (@eq E a x0) *)
(* Goal: or (@eq E a a) (@In E a l0) *)
 apply (H1 x); auto.
Qed.

End SUM.

Section SIGMA_BUT.

Variable E : Set.

Variable x0 : E.

Hypothesis eq_E_dec : eq_dec E.

Variable f : E -> Z.


Fixpoint sigma_but (l1 : list E) : (E -> Z) -> Z :=
  fun f : E -> Z =>
  match l1 with
  | nil => 0%Z
  | e :: l2 =>
      if eq_E_dec e x0
      then sigma_but l2 f
      else (f e + sigma_but l2 f)%Z
  end.


Lemma sigma_but_pos :
 forall (f : E -> Z) (l : list E),
 (forall x_ : E, (f x_ >= 0)%Z) -> (sigma_but l f >= 0)%Z.
Proof.
(* Goal: @eq Z (sigma E (@cons E a l0) f) (Z.add (sigma_but (@cons E a l0) f) (f x0)) *)
  intros; elim l; simpl in |- *.
(* Goal: @eq Z (Z.add (f a) (Z.add (sigma_but l0 f) (f x0))) (Z.add (Z.add (f a) (sigma_but l0 f)) (f x0)) *)
(* Goal: only_once E eq_E_dec x0 l0 *)
(* Goal: not (@eq E a x0) *)
  omega.
(* Goal: forall (a : E) (l : list E) (_ : Z.ge (sigma_but l f0) Z0), Z.ge (if eq_E_dec a x0 then sigma_but l f0 else Z.add (f0 a) (sigma_but l f0)) Z0 *)
  intros a l0 H0.
(* Goal: Z.ge (if eq_E_dec a x0 then sigma_but l0 f0 else Z.add (f0 a) (sigma_but l0 f0)) Z0 *)
  case (eq_E_dec a x0); intro.
(* Goal: not (@eq E a x0) *)
(* Goal: or (@eq E a a) (@In E a l0) *)
  auto.
(* Goal: @eq Z (Z.add (f a) (Z.add (sigma_but l0 f) (f x0))) (Z.add (Z.add (f a) (sigma_but l0 f)) (f x0)) *)
(* Goal: only_once E eq_E_dec x0 l0 *)
(* Goal: not (@eq E a x0) *)
  generalize (H a); omega.
Qed.


Lemma sigma_sigma_but_not_in :
 forall l : list E, ~ In x0 l -> sigma E l f = sigma_but l f.
Proof.
(* Goal: forall (l : list E) (f g : forall _ : E, Z) (_ : forall (x : E) (_ : not (@eq E x x0)) (_ : @In E x l), @eq Z (f x) (g x)), @eq Z (sigma_but l f) (sigma_but l g) *)
  simple induction l.
(* Goal: @eq Z (sigma E (@cons E a l0) f) (Z.add (sigma_but (@cons E a l0) f) (f x0)) *)
  simpl in |- *.
(* Goal: not (@eq E a x0) *)
(* Goal: or (@eq E a a) (@In E a l0) *)
  auto.
  
(* Goal: forall (a : E) (l : list E) (_ : forall _ : only_once E eq_E_dec x0 l, @eq Z (sigma E l f) (Z.add (sigma_but l f) (f x0))) (_ : only_once E eq_E_dec x0 (@cons E a l)), @eq Z (sigma E (@cons E a l) f) (Z.add (sigma_but (@cons E a l) f) (f x0)) *)
  intros a l0 H H0.
(* Goal: @eq Z (if eq_E_dec a x0 then sigma_but l0 f0 else Z.add (f0 a) (sigma_but l0 f0)) (if eq_E_dec a x0 then sigma_but l0 g else Z.add (g a) (sigma_but l0 g)) *)
  case (eq_E_dec a x0).
(* Goal: forall _ : @eq E a x0, @eq Z (sigma E (@cons E a l0) f) (sigma_but (@cons E a l0) f) *)
(* Goal: forall _ : not (@eq E a x0), @eq Z (sigma E (@cons E a l0) f) (sigma_but (@cons E a l0) f) *)
  intros e.
(* Goal: @eq Z (sigma E (@cons E a l0) f) (sigma_but (@cons E a l0) f) *)
(* Goal: forall _ : not (@eq E a x0), @eq Z (sigma E (@cons E a l0) f) (sigma_but (@cons E a l0) f) *)
  elim H0.
(* Goal: @eq Z (sigma E (@cons E a l0) f) (Z.add (sigma_but (@cons E a l0) f) (f x0)) *)
  rewrite e; simpl in |- *.
(* Goal: not (@eq E a x0) *)
(* Goal: or (@eq E a a) (@In E a l0) *)
  left; auto.
  
(* Goal: forall _ : not (@eq E a x0), @eq Z (sigma E (@cons E a l0) f) (Z.add (sigma_but (@cons E a l0) f) (f x0)) *)
  intros n.
(* Goal: @eq Z (sigma E (@cons E a l0) f) (Z.add (sigma_but (@cons E a l0) f) (f x0)) *)
  simpl in |- *.
(* Goal: @eq Z (Z.add (f a) (sigma E l0 f)) (Z.add (if eq_E_dec a x0 then sigma_but l0 f else Z.add (f a) (sigma_but l0 f)) (f x0)) *)
  rewrite case_ineq.
(* Goal: @eq Z (Z.add (f a) (sigma E l0 f)) (Z.add (Z.add (f a) (sigma_but l0 f)) (f x0)) *)
(* Goal: not (@eq E a x0) *)
  rewrite H.
(* Goal: not (@eq E a x0) *)
(* Goal: or (@eq E a a) (@In E a l0) *)
  auto.
  
(* Goal: not (@In E x0 l0) *)
(* Goal: not (@eq E a x0) *)
  generalize H0.
(* Goal: @eq Z (sigma E (@cons E a l0) f) (Z.add (sigma_but (@cons E a l0) f) (f x0)) *)
  simpl in |- *.
(* Goal: forall _ : not (or (@eq E a x0) (@In E x0 l0)), not (@In E x0 l0) *)
(* Goal: not (@eq E a x0) *)
  intro H1.
(* Goal: not (@In E x0 l0) *)
(* Goal: not (@eq E a x0) *)
  generalize H1.
(* Goal: forall (_ : not (@eq E x0 x0)) (_ : only_once E eq_E_dec x0 l0), not (@In E x0 l0) *)
(* Goal: forall _ : not (@eq E a x0), @eq Z (sigma E (@cons E a l0) f) (Z.add (sigma_but (@cons E a l0) f) (f x0)) *)
  intuition.
  
(* Goal: not (@eq E a x0) *)
(* Goal: or (@eq E a a) (@In E a l0) *)
  auto.
Qed.



Lemma sigma_sigma_but :
 forall l : list E,
 only_once E eq_E_dec x0 l -> sigma E l f = (sigma_but l f + f x0)%Z.
Proof.
(* Goal: forall (l : list E) (f g : forall _ : E, Z) (_ : forall (x : E) (_ : not (@eq E x x0)) (_ : @In E x l), @eq Z (f x) (g x)), @eq Z (sigma_but l f) (sigma_but l g) *)
  simple induction l.
(* Goal: forall _ : only_once E eq_E_dec x0 (@nil E), @eq Z (sigma E (@nil E) f) (Z.add (sigma_but (@nil E) f) (f x0)) *)
(* Goal: forall (a : E) (l : list E) (_ : forall _ : only_once E eq_E_dec x0 l, @eq Z (sigma E l f) (Z.add (sigma_but l f) (f x0))) (_ : only_once E eq_E_dec x0 (@cons E a l)), @eq Z (sigma E (@cons E a l) f) (Z.add (sigma_but (@cons E a l) f) (f x0)) *)
  simpl in |- *; intuition.
  
(* Goal: forall (a : E) (l : list E) (_ : forall _ : only_once E eq_E_dec x0 l, @eq Z (sigma E l f) (Z.add (sigma_but l f) (f x0))) (_ : only_once E eq_E_dec x0 (@cons E a l)), @eq Z (sigma E (@cons E a l) f) (Z.add (sigma_but (@cons E a l) f) (f x0)) *)
  intros a l0 H H0.
(* Goal: @eq Z (if eq_E_dec a x0 then sigma_but l0 f0 else Z.add (f0 a) (sigma_but l0 f0)) (if eq_E_dec a x0 then sigma_but l0 g else Z.add (g a) (sigma_but l0 g)) *)
  case (eq_E_dec a x0).
(* Goal: @eq Z (sigma E (@cons E a l0) f) (Z.add (sigma_but (@cons E a l0) f) (f x0)) *)
  intro; rewrite e; simpl in |- *.
(* Goal: @eq Z (Z.add (f x0) (sigma E l0 f)) (Z.add (if eq_E_dec x0 x0 then sigma_but l0 f else Z.add (f x0) (sigma_but l0 f)) (f x0)) *)
(* Goal: forall _ : not (@eq E a x0), @eq Z (sigma E (@cons E a l0) f) (Z.add (sigma_but (@cons E a l0) f) (f x0)) *)
  rewrite case_eq.
(* Goal: @eq Z (Z.add (f x0) (sigma E l0 f)) (Z.add (sigma_but l0 f) (f x0)) *)
(* Goal: forall _ : not (@eq E a x0), @eq Z (sigma E (@cons E a l0) f) (Z.add (sigma_but (@cons E a l0) f) (f x0)) *)
  rewrite sigma_sigma_but_not_in.
(* Goal: @eq Z (Z.add (f a) (Z.add (sigma_but l0 f) (f x0))) (Z.add (Z.add (f a) (sigma_but l0 f)) (f x0)) *)
(* Goal: only_once E eq_E_dec x0 l0 *)
(* Goal: not (@eq E a x0) *)
  omega.
  
(* Goal: @eq Z (sigma E (@cons E a l0) f) (Z.add (sigma_but (@cons E a l0) f) (f x0)) *)
  generalize H0; simpl in |- *.
(* Goal: forall _ : if eq_E_dec x0 a then not (@In E x0 l0) else only_once E eq_E_dec x0 l0, not (@In E x0 l0) *)
(* Goal: forall _ : not (@eq E a x0), @eq Z (sigma E (@cons E a l0) f) (Z.add (sigma_but (@cons E a l0) f) (f x0)) *)
  rewrite e.
(* Goal: forall _ : if eq_E_dec x0 x0 then not (@In E x0 l0) else only_once E eq_E_dec x0 l0, not (@In E x0 l0) *)
(* Goal: forall _ : not (@eq E a x0), @eq Z (sigma E (@cons E a l0) f) (Z.add (sigma_but (@cons E a l0) f) (f x0)) *)
  case (eq_E_dec x0 x0).
(* Goal: not (@eq E a x0) *)
(* Goal: or (@eq E a a) (@In E a l0) *)
  auto.
  
(* Goal: forall (_ : not (@eq E x0 x0)) (_ : only_once E eq_E_dec x0 l0), not (@In E x0 l0) *)
(* Goal: forall _ : not (@eq E a x0), @eq Z (sigma E (@cons E a l0) f) (Z.add (sigma_but (@cons E a l0) f) (f x0)) *)
  intuition.
  
(* Goal: forall _ : not (@eq E a x0), @eq Z (sigma E (@cons E a l0) f) (Z.add (sigma_but (@cons E a l0) f) (f x0)) *)
  intros n.
(* Goal: @eq Z (sigma E (@cons E a l0) f) (Z.add (sigma_but (@cons E a l0) f) (f x0)) *)
  simpl in |- *.
(* Goal: @eq Z (Z.add (f a) (sigma E l0 f)) (Z.add (if eq_E_dec a x0 then sigma_but l0 f else Z.add (f a) (sigma_but l0 f)) (f x0)) *)
  rewrite case_ineq.
(* Goal: @eq Z (Z.add (f a) (sigma E l0 f)) (Z.add (Z.add (f a) (sigma_but l0 f)) (f x0)) *)
(* Goal: not (@eq E a x0) *)
  rewrite H.
(* Goal: @eq Z (Z.add (f a) (Z.add (sigma_but l0 f) (f x0))) (Z.add (Z.add (f a) (sigma_but l0 f)) (f x0)) *)
(* Goal: only_once E eq_E_dec x0 l0 *)
(* Goal: not (@eq E a x0) *)
  omega.
  
(* Goal: @eq Z (sigma E (@cons E a l0) f) (Z.add (sigma_but (@cons E a l0) f) (f x0)) *)
  generalize H0; simpl in |- *.
(* Goal: forall _ : if eq_E_dec x0 a then not (@In E x0 l0) else only_once E eq_E_dec x0 l0, only_once E eq_E_dec x0 l0 *)
(* Goal: not (@eq E a x0) *)
  case (eq_E_dec x0 a).
(* Goal: forall (_ : @eq E x0 a) (_ : not (@In E x0 l0)), only_once E eq_E_dec x0 l0 *)
(* Goal: forall (_ : not (@eq E x0 a)) (_ : only_once E eq_E_dec x0 l0), only_once E eq_E_dec x0 l0 *)
(* Goal: not (@eq E a x0) *)
  intros e H1.
(* Goal: only_once E eq_E_dec x0 l0 *)
(* Goal: forall (_ : not (@eq E x0 a)) (_ : only_once E eq_E_dec x0 l0), only_once E eq_E_dec x0 l0 *)
(* Goal: not (@eq E a x0) *)
  rewrite e in n.
(* Goal: only_once E eq_E_dec x0 l0 *)
(* Goal: forall (_ : not (@eq E x0 a)) (_ : only_once E eq_E_dec x0 l0), only_once E eq_E_dec x0 l0 *)
(* Goal: not (@eq E a x0) *)
  elim n.
(* Goal: not (@eq E a x0) *)
(* Goal: or (@eq E a a) (@In E a l0) *)
  auto.
  
(* Goal: forall (_ : not (@eq E x0 a)) (_ : only_once E eq_E_dec x0 l0), only_once E eq_E_dec x0 l0 *)
(* Goal: not (@eq E a x0) *)
  intro n0.
(* Goal: not (@eq E a x0) *)
(* Goal: or (@eq E a a) (@In E a l0) *)
  auto.
  
(* Goal: not (@eq E a x0) *)
(* Goal: or (@eq E a a) (@In E a l0) *)
  auto.
Qed.

Lemma sigma_but_simpl :
 forall (l : list E) (f g : E -> Z),
 (forall x : E, x <> x0 -> In x l -> f x = g x) ->
 sigma_but l f = sigma_but l g.
Proof.
(* Goal: forall (l : list E) (f g : forall _ : E, Z) (_ : forall (x : E) (_ : not (@eq E x x0)) (_ : @In E x l), @eq Z (f x) (g x)), @eq Z (sigma_but l f) (sigma_but l g) *)
  simple induction l.
(* Goal: not (@eq E a x0) *)
(* Goal: or (@eq E a a) (@In E a l0) *)
  auto.
  
(* Goal: forall (a : E) (l : list E) (_ : forall (f g : forall _ : E, Z) (_ : forall (x : E) (_ : not (@eq E x x0)) (_ : @In E x l), @eq Z (f x) (g x)), @eq Z (sigma_but l f) (sigma_but l g)) (f g : forall _ : E, Z) (_ : forall (x : E) (_ : not (@eq E x x0)) (_ : @In E x (@cons E a l)), @eq Z (f x) (g x)), @eq Z (sigma_but (@cons E a l) f) (sigma_but (@cons E a l) g) *)
  simpl in |- *; intros.
(* Goal: @eq Z (if eq_E_dec a x0 then sigma_but l0 f0 else Z.add (f0 a) (sigma_but l0 f0)) (if eq_E_dec a x0 then sigma_but l0 g else Z.add (g a) (sigma_but l0 g)) *)
  case (eq_E_dec a x0).
(* Goal: forall _ : @eq E a x0, @eq Z (sigma_but l0 f0) (sigma_but l0 g) *)
(* Goal: forall _ : not (@eq E a x0), @eq Z (Z.add (f0 a) (sigma_but l0 f0)) (Z.add (g a) (sigma_but l0 g)) *)
  intro e.
(* Goal: @eq Z (sigma_but l0 f0) (sigma_but l0 g) *)
(* Goal: forall _ : not (@eq E a x0), @eq Z (Z.add (f0 a) (sigma_but l0 f0)) (Z.add (g a) (sigma_but l0 g)) *)
  apply (H f0 g).
(* Goal: forall (x : E) (_ : not (@eq E x x0)) (_ : @In E x l0), @eq Z (f0 x) (g x) *)
(* Goal: not (@eq E a x0) *)
(* Goal: or (@eq E a a) (@In E a l0) *)
  intros x H1 H2.
(* Goal: @eq Z (f0 x) (g x) *)
(* Goal: not (@eq E a x0) *)
(* Goal: or (@eq E a a) (@In E a l0) *)
  apply H0.
(* Goal: not (@eq E a x0) *)
(* Goal: or (@eq E a a) (@In E a l0) *)
  auto.
  
(* Goal: not (@eq E a x0) *)
(* Goal: or (@eq E a a) (@In E a l0) *)
  right; auto.
  
(* Goal: forall _ : not (@eq E a x0), @eq Z (Z.add (f0 a) (sigma_but l0 f0)) (Z.add (g a) (sigma_but l0 g)) *)
  intro n.
(* Goal: @eq Z (Z.add (f0 a) (sigma_but l0 f0)) (Z.add (g a) (sigma_but l0 g)) *)
  rewrite H0.
(* Goal: @eq Z (Z.add (g a) (sigma_but l0 f0)) (Z.add (g a) (sigma_but l0 g)) *)
(* Goal: not (@eq E a x0) *)
(* Goal: or (@eq E a a) (@In E a l0) *)
  rewrite (H f0 g).
(* Goal: not (@eq E a x0) *)
(* Goal: or (@eq E a a) (@In E a l0) *)
  auto.
  
(* Goal: forall (x : E) (_ : not (@eq E x x0)) (_ : @In E x l0), @eq Z (f0 x) (g x) *)
(* Goal: not (@eq E a x0) *)
(* Goal: or (@eq E a a) (@In E a l0) *)
  intros x H1 H2.
(* Goal: @eq Z (f0 x) (g x) *)
(* Goal: not (@eq E a x0) *)
(* Goal: or (@eq E a a) (@In E a l0) *)
  apply H0.
(* Goal: not (@eq E a x0) *)
(* Goal: or (@eq E a a) (@In E a l0) *)
  auto.
  
(* Goal: not (@eq E a x0) *)
(* Goal: or (@eq E a a) (@In E a l0) *)
  right; auto.
  
(* Goal: not (@eq E a x0) *)
(* Goal: or (@eq E a a) (@In E a l0) *)
  auto.
  
(* Goal: not (@eq E a x0) *)
(* Goal: or (@eq E a a) (@In E a l0) *)
  left; auto.
Qed.



End SIGMA_BUT.
