path: root/contrib7/romega/ReflOmegaCore.v

(*************************************************************************

   PROJET RNRT Calife - 2001
   Author: Pierre Crégut - France Télécom R&D
   Licence du projet : LGPL version 2.1

 *************************************************************************)

Require Arith.
Require PolyList.
Require Bool.
Require ZArith.
Require Import OmegaLemmas.

(* \subsection{Definition of basic types} *)

(* \subsubsection{Environment of propositions (lists) *)
Inductive PropList : Type := 
  Pnil : PropList | Pcons : Prop -> PropList -> PropList.

(* Access function for the environment with a default *)
Fixpoint nthProp [n:nat; l:PropList] : Prop -> Prop :=
  [default]Cases n l of
    O (Pcons x l') => x
  | O other => default
  | (S m) Pnil => default
  | (S m) (Pcons x t) => (nthProp m t default)
  end.
   
(* \subsubsection{Définition of reified integer expressions}
   Terms are either:
   \begin{itemize}
   \item integers [Tint]
   \item variables [Tvar]
   \item operation over integers (addition, product, opposite, subtraction)
   The last two are translated in additions and products. *)

Inductive term : Set :=
   Tint : Z -> term
 | Tplus : term -> term -> term
 | Tmult : term -> term -> term
 | Tminus : term -> term -> term
 | Topp : term -> term
 | Tvar : nat -> term
.

(* \subsubsection{Definition of reified goals} *)
(* Very restricted definition of handled predicates that should be extended
   to cover a wider set of operations.
   Taking care of negations and disequations require solving more than a
   goal in parallel. This is a major improvement over previous versions. *)

Inductive proposition : Set :=
  EqTerm : term -> term -> proposition (* egalité entre termes *)
| LeqTerm : term -> term -> proposition (* plus petit ou egal *)
| TrueTerm : proposition (* vrai *)
| FalseTerm : proposition (* faux *)
| Tnot : proposition -> proposition (* négation *)
| GeqTerm : term -> term -> proposition
| GtTerm : term -> term -> proposition
| LtTerm : term -> term -> proposition
| NeqTerm: term -> term -> proposition
| Tor : proposition -> proposition -> proposition
| Tand : proposition -> proposition -> proposition
| Timp : proposition -> proposition -> proposition
| Tprop : nat -> proposition
.

(* Definition of goals as a list of hypothesis *)
Syntactic Definition hyps := (list proposition).      

(* Definition of lists of subgoals  (set of open goals) *)
Syntactic Definition lhyps := (list hyps).

(* a syngle goal packed in a subgoal list *)
Syntactic Definition singleton :=  [a: hyps] (cons a (nil hyps)).

(* an absurd goal *)
Definition absurd := (cons FalseTerm (nil proposition)).

(* \subsubsection{Traces for merging equations}
   This inductive type describes how the monomial of two equations should be
   merged when the equations are added.

   For [F_equal], both equations have the same head variable and coefficient
   must be added, furthermore if coefficients are opposite, [F_cancel] should
   be used to collapse the term. [F_left] and [F_right] indicate which monomial
   should be put first in the result *)

Inductive t_fusion : Set :=
    F_equal : t_fusion | F_cancel : t_fusion
  | F_left : t_fusion  | F_right : t_fusion.

(* \subsubsection{Rewriting steps to normalize terms} *)
Inductive step : Set := 
 (* apply the rewriting steps to both subterms of an operation *)
 | C_DO_BOTH : step -> step -> step
 (* apply the rewriting step to the first branch *)
 | C_LEFT : step -> step
 (* apply the rewriting step to the second branch *)
 | C_RIGHT : step -> step
 (* apply two steps consecutively to a term *)
 | C_SEQ : step -> step -> step
 (* empty step *)
 | C_NOP : step
 (* the following operations correspond to actual rewriting *)
 | C_OPP_PLUS : step
 | C_OPP_OPP : step
 | C_OPP_MULT_R : step
 | C_OPP_ONE : step
 (* This is a special step that reduces the term (computation) *)
 | C_REDUCE : step
 | C_MULT_PLUS_DISTR : step
 | C_MULT_OPP_LEFT : step
 | C_MULT_ASSOC_R : step
 | C_PLUS_ASSOC_R : step
 | C_PLUS_ASSOC_L : step
 | C_PLUS_PERMUTE : step
 | C_PLUS_SYM : step
 | C_RED0 : step
 | C_RED1 : step
 | C_RED2 : step
 | C_RED3 : step
 | C_RED4 : step
 | C_RED5 : step
 | C_RED6 : step
 | C_MULT_ASSOC_REDUCED : step
 | C_MINUS :step
 | C_MULT_SYM : step
.

(* \subsubsection{Omega steps} *)
(* The following inductive type describes steps as they can be found in
   the trace coming from the decision procedure Omega. *)

Inductive t_omega : Set :=
   (* n = 0 n!= 0 *)
 | O_CONSTANT_NOT_NUL : nat -> t_omega
 | O_CONSTANT_NEG : nat -> t_omega
   (* division et approximation of an equation *)
 | O_DIV_APPROX : Z -> Z -> term -> nat -> t_omega -> nat -> t_omega
   (* no solution because no exact division *)
 | O_NOT_EXACT_DIVIDE :  Z -> Z -> term -> nat -> nat -> t_omega
   (* exact division *)
 | O_EXACT_DIVIDE : Z -> term -> nat -> t_omega -> nat -> t_omega
 | O_SUM : Z -> nat -> Z -> nat -> (list t_fusion) -> t_omega -> t_omega
 | O_CONTRADICTION : nat -> nat -> nat -> t_omega
 | O_MERGE_EQ : nat -> nat -> nat -> t_omega -> t_omega
 | O_SPLIT_INEQ : nat -> nat -> t_omega -> t_omega -> t_omega
 | O_CONSTANT_NUL : nat -> t_omega 
 | O_NEGATE_CONTRADICT : nat -> nat -> t_omega
 | O_NEGATE_CONTRADICT_INV : nat -> nat -> nat -> t_omega
 | O_STATE : Z -> step -> nat -> nat -> t_omega -> t_omega.

(* \subsubsection{Règles pour normaliser les hypothèses} *)
(* Ces règles indiquent comment normaliser les propositions utiles 
   de chaque hypothèse utile avant la décomposition des hypothèses et 
   incluent l'étape d'inversion pour la suppression des négations *)
Inductive p_step : Set :=
  P_LEFT : p_step -> p_step
| P_RIGHT :  p_step -> p_step
| P_INVERT :  step -> p_step
| P_STEP : step -> p_step
| P_NOP : p_step
.
(* Liste des normalisations a effectuer : avec un constructeur dans le
   type [p_step] permettant
   de parcourir à la fois les branches gauches et droit, on pourrait n'avoir
   qu'une normalisation par hypothèse. Et comme toutes les hypothèses sont 
   utiles (sinon on ne les incluerait pas), on pourrait remplacer [h_step] 
   par une simple liste *)

Inductive h_step : Set := pair_step : nat -> p_step -> h_step.

(* \subsubsection{Règles pour décomposer les hypothèses} *)
(* Ce type permet de se diriger dans les constructeurs logiques formant les
   prédicats des hypothèses pour aller les décomposer. Ils permettent
   en particulier d'extraire une hypothèse d'une conjonction avec
   éventuellement le bon niveau de négations. *)

Inductive direction : Set :=
   D_left : direction
 | D_right : direction
 | D_mono : direction.

(* Ce type permet d'extraire les composants utiles des hypothèses : que ce
   soit des hypothèses générées par éclatement d'une disjonction, ou 
   des équations. Le constructeur terminal indique comment résoudre le système
   obtenu en recourrant au type de trace d'Omega [t_omega] *)

Inductive e_step : Set :=
   E_SPLIT : nat -> (list direction) -> e_step -> e_step -> e_step
 | E_EXTRACT : nat -> (list direction) -> e_step -> e_step
 | E_SOLVE : t_omega -> e_step.

(* \subsection{Egalité décidable efficace} *)
(* Pour chaque type de donnée réifié, on calcule un test d'égalité efficace.
   Ce n'est pas le cas de celui rendu par [Decide Equality].
   
   Puis on prouve deux théorèmes permettant d'éliminer de telles égalités :
   \begin{verbatim}
   (t1,t2: typ) (eq_typ t1 t2) = true -> t1 = t2.
   (t1,t2: typ) (eq_typ t1 t2) = false -> ~ t1 = t2.
   \end{verbatim} *)

(* Ces deux tactiques permettent de résoudre pas mal de cas. L'une pour
   les théorèmes positifs, l'autre pour les théorèmes négatifs *)

Tactic Definition absurd_case := Simpl; Intros; Discriminate.
Tactic Definition trivial_case := Unfold not; Intros; Discriminate.

(* \subsubsection{Entiers naturels} *)

Fixpoint eq_nat [t1,t2: nat] : bool := 
  Cases t1 of
    O => Cases t2 of O => true | _ => false end
  | (S n1)=> Cases t2 of O => false | (S n2)  => (eq_nat n1 n2) end
  end.

Theorem eq_nat_true : (t1,t2: nat) (eq_nat t1 t2) = true -> t1 = t2.

Induction t1; [
  Intro t2; Case t2; [ Trivial | absurd_case ]
| Intros n H t2; Case t2; 
    [ absurd_case |  Simpl; Intros; Rewrite (H n0); [ Trivial | Assumption]]].

Save.
  
Theorem eq_nat_false : (t1,t2: nat) (eq_nat t1 t2) = false -> ~t1 = t2.

Induction t1; [
  Intro t2; Case t2;
   [ Simpl;Intros; Discriminate | trivial_case ]
| Intros n H t2; Case t2; Simpl; Unfold not; Intros; [
    Discriminate
  | Elim (H n0 H0); Simplify_eq H1; Trivial]].

Save.
                                   

(* \subsubsection{Entiers positifs} *)

Fixpoint eq_pos [p1,p2 : positive] : bool := 
  Cases p1 of
    (xI n1) => Cases p2 of (xI n2) => (eq_pos n1 n2) | _ => false end
  | (xO n1) =>  Cases p2 of (xO n2) => (eq_pos n1 n2) | _ => false end
  | xH =>  Cases p2 of xH => true | _ => false end
  end.

Theorem eq_pos_true : (t1,t2: positive) (eq_pos t1 t2) = true -> t1 = t2.

Induction t1; [
  Intros p H t2; Case t2; [
    Simpl; Intros; Rewrite (H p0 H0); Trivial | absurd_case | absurd_case ]
| Intros p H t2; Case t2; [
    absurd_case | Simpl; Intros; Rewrite (H p0 H0); Trivial | absurd_case ]
| Intro t2; Case t2; [ absurd_case | absurd_case | Auto ]].

Save.
  
Theorem eq_pos_false : (t1,t2: positive) (eq_pos t1 t2) = false -> ~t1 = t2.

Induction t1; [
  Intros p H t2; Case t2; [
    Simpl; Unfold not; Intros; Elim (H p0 H0); Simplify_eq H1; Auto
  | trivial_case | trivial_case ]
| Intros p H t2; Case t2; [
    trivial_case 
  | Simpl; Unfold not; Intros; Elim (H p0 H0); Simplify_eq H1; Auto
  | trivial_case ]
| Intros t2; Case t2; [ trivial_case | trivial_case  | absurd_case ]].
Save.

(* \subsubsection{Entiers relatifs} *)

Definition eq_Z [z1,z2: Z] : bool :=
  Cases z1 of
     ZERO     => Cases z2 of ZERO => true | _ => false end
   | (POS p1) => Cases z2 of (POS p2) => (eq_pos p1 p2) | _ => false end
   | (NEG p1) => Cases z2 of (NEG p2) => (eq_pos p1 p2) | _ => false end
  end.

Theorem eq_Z_true : (t1,t2: Z) (eq_Z t1 t2) = true -> t1 = t2.

Induction t1; [
  Intros t2; Case t2; [ Auto | absurd_case | absurd_case ]
| Intros p t2; Case t2; [
    absurd_case | Simpl; Intros; Rewrite (eq_pos_true p p0 H); Trivial 
  | absurd_case ]
| Intros p t2; Case t2; [
    absurd_case | absurd_case
  | Simpl; Intros; Rewrite (eq_pos_true p p0 H); Trivial ]].

Save.

Theorem eq_Z_false : (t1,t2: Z) (eq_Z t1 t2) = false -> ~(t1 = t2).

Induction t1; [
  Intros t2; Case t2; [ absurd_case | trivial_case | trivial_case ]
| Intros p t2; Case t2; [
    absurd_case
  | Simpl; Unfold not; Intros; Elim (eq_pos_false p p0 H); Simplify_eq H0; Auto
  | trivial_case ]
| Intros p t2; Case t2; [
    absurd_case | trivial_case 
  | Simpl; Unfold not; Intros; Elim (eq_pos_false p p0 H); 
    Simplify_eq H0; Auto]].
Save.

(* \subsubsection{Termes réifiés} *)

Fixpoint eq_term [t1,t2: term] : bool := 
   Cases t1 of
      (Tint st1) =>
         Cases t2 of (Tint st2) => (eq_Z st1 st2) | _ => false end
    | (Tplus st11 st12) =>
         Cases t2 of
            (Tplus st21 st22) => 
               (andb (eq_term st11 st21) (eq_term st12 st22))
         | _ => false 
         end
    | (Tmult st11 st12) =>
         Cases t2 of
            (Tmult st21 st22) => 
               (andb (eq_term st11 st21) (eq_term st12 st22))
         | _ => false 
         end
    | (Tminus st11 st12) =>
         Cases t2 of
            (Tminus st21 st22) => 
               (andb (eq_term st11 st21) (eq_term st12 st22))
         | _ => false 
         end
    | (Topp st1) =>
         Cases t2 of (Topp st2) => (eq_term st1 st2) | _ => false end
    | (Tvar st1) =>
         Cases t2 of (Tvar st2) => (eq_nat st1 st2) | _ => false end
   end.  

Theorem eq_term_true : (t1,t2: term) (eq_term t1 t2) = true -> t1 = t2.


Induction t1; Intros until t2; Case t2; Try absurd_case; Simpl; [
  Intros; Elim eq_Z_true with 1 := H; Trivial
| Intros t21 t22 H3; Elim andb_prop with 1:= H3; Intros H4 H5; 
  Elim H with 1 := H4; Elim H0 with 1 := H5; Trivial
| Intros t21 t22 H3; Elim andb_prop with 1:= H3; Intros H4 H5;
  Elim H with 1 := H4; Elim H0 with 1 := H5; Trivial
| Intros t21 t22 H3; Elim andb_prop with 1:= H3; Intros H4 H5; 
  Elim H with 1 := H4; Elim H0 with 1 := H5; Trivial
| Intros t21 H3; Elim H with 1 := H3; Trivial
| Intros; Elim eq_nat_true with 1 := H; Trivial ].

Save.

Theorem eq_term_false : (t1,t2: term) (eq_term t1 t2) = false -> ~(t1 = t2).

Induction t1; [
  Intros z t2; Case t2; Try trivial_case; Simpl; Unfold not; Intros;
  Elim eq_Z_false with 1:=H; Simplify_eq H0; Auto
| Intros t11 H1 t12 H2 t2; Case t2; Try trivial_case; Simpl; Intros t21 t22 H3;
  Unfold not; Intro H4; Elim andb_false_elim with 1:= H3; Intros H5; 
  [ Elim H1 with 1 := H5; Simplify_eq H4; Auto |
    Elim H2 with 1 := H5; Simplify_eq H4; Auto ]
| Intros t11 H1 t12 H2 t2; Case t2; Try trivial_case; Simpl; Intros t21 t22 H3;
  Unfold not; Intro H4; Elim andb_false_elim with 1:= H3; Intros H5; 
  [ Elim H1 with 1 := H5; Simplify_eq H4; Auto |
    Elim H2 with 1 := H5; Simplify_eq H4; Auto ]
| Intros t11 H1 t12 H2 t2; Case t2; Try trivial_case; Simpl; Intros t21 t22 H3;
  Unfold not; Intro H4; Elim andb_false_elim with 1:= H3; Intros H5; 
  [ Elim H1 with 1 := H5; Simplify_eq H4; Auto |
    Elim H2 with 1 := H5; Simplify_eq H4; Auto ]
| Intros t11 H1 t2; Case t2; Try trivial_case; Simpl; Intros t21 H3;
  Unfold not; Intro H4; Elim H1 with 1 := H3; Simplify_eq H4; Auto 
| Intros n t2; Case t2; Try trivial_case; Simpl; Unfold not; Intros;
  Elim eq_nat_false with 1:=H; Simplify_eq H0; Auto ].

Save.

(* \subsubsection{Tactiques pour éliminer ces tests} 

   Si on se contente de faire un [Case (eq_typ t1 t2)] on perd 
   totalement dans chaque branche le fait que [t1=t2] ou [~t1=t2].

   Initialement, les développements avaient été réalisés avec les
   tests rendus par [Decide Equality], c'est à dire un test rendant
   des termes du type [{t1=t2}+{~t1=t2}]. Faire une élimination sur un 
   tel test préserve bien l'information voulue mais calculatoirement de
   telles fonctions sont trop lentes. *)

(* Le théorème suivant permet de garder dans les hypothèses la valeur
   du booléen lors de l'élimination. *)

Theorem bool_ind2 : 
   (P:(bool->Prop)) (b:bool)
     (b = true -> (P true))->
     (b = false -> (P false)) -> (P b).

Induction b; Auto.
Save.

(* Les tactiques définies si après se comportent exactement comme si on
   avait utilisé le test précédent et fait une elimination dessus. *)

Tactic Definition Elim_eq_term t1 t2 :=
  Pattern (eq_term t1 t2); Apply bool_ind2; Intro Aux; [
    Generalize (eq_term_true t1 t2 Aux); Clear Aux
  | Generalize (eq_term_false t1 t2 Aux); Clear Aux ].

Tactic Definition Elim_eq_Z t1 t2 :=
  Pattern (eq_Z t1 t2); Apply bool_ind2; Intro Aux; [
    Generalize (eq_Z_true t1 t2 Aux); Clear Aux
  | Generalize (eq_Z_false t1 t2 Aux); Clear Aux ].

Tactic Definition Elim_eq_pos t1 t2 :=
  Pattern (eq_pos t1 t2); Apply bool_ind2; Intro Aux; [
    Generalize (eq_pos_true t1 t2 Aux); Clear Aux
  | Generalize (eq_pos_false t1 t2 Aux); Clear Aux ].

(* \subsubsection{Comparaison sur Z} *)

(* Sujet très lié au précédent : on introduit la tactique d'élimination
   avec son théorème *)

Theorem relation_ind2 : 
   (P:(relation->Prop)) (b:relation)
     (b = EGAL -> (P EGAL))->
     (b = INFERIEUR -> (P INFERIEUR))->
     (b = SUPERIEUR -> (P SUPERIEUR)) -> (P b).

Induction b; Auto.
Save.

Tactic Definition Elim_Zcompare t1 t2 :=
  Pattern (Zcompare t1 t2); Apply relation_ind2.

(* \subsection{Interprétations}
   \subsubsection{Interprétation des termes dans Z} *)

Fixpoint interp_term [env:(list Z); t:term] : Z :=
  Cases t of
    (Tint x) => x
  | (Tplus t1 t2) => (Zplus (interp_term env t1) (interp_term env t2))
  | (Tmult t1 t2) => (Zmult (interp_term env t1) (interp_term env t2))
  | (Tminus t1 t2) => (Zminus (interp_term env t1) (interp_term env t2))
  | (Topp t) => (Zopp (interp_term env t))
  | (Tvar n) => (nth n env ZERO)
  end.

(* \subsubsection{Interprétation des prédicats} *) 
Fixpoint interp_proposition 
    [envp : PropList; env: (list Z); p:proposition] : Prop := 
  Cases p of
    (EqTerm t1 t2) => ((interp_term env t1) = (interp_term env t2))
  | (LeqTerm t1 t2) => `(interp_term env t1) <= (interp_term env t2)`
  | TrueTerm => True
  | FalseTerm => False
  | (Tnot p') => ~(interp_proposition envp env p')
  | (GeqTerm t1 t2) => `(interp_term env t1) >= (interp_term env t2)`
  | (GtTerm t1 t2) => `(interp_term env t1) > (interp_term env t2)`
  | (LtTerm t1 t2) => `(interp_term env t1) < (interp_term env t2)`
  | (NeqTerm t1 t2) => `(Zne (interp_term env t1) (interp_term env t2))`

  | (Tor p1 p2) => 
	(interp_proposition envp env p1) \/ (interp_proposition envp env p2)
  | (Tand p1 p2) =>
	(interp_proposition envp env p1) /\ (interp_proposition envp env p2)
  | (Timp p1 p2) =>
	(interp_proposition envp env p1) -> (interp_proposition envp env p2)
  | (Tprop n) => (nthProp n envp True)
  end.

(* \subsubsection{Inteprétation des listes d'hypothèses}
   \paragraph{Sous forme de conjonction}
   Interprétation sous forme d'une conjonction d'hypothèses plus faciles
   à manipuler individuellement *)

Fixpoint interp_hyps [envp: PropList; env : (list Z); l: hyps] : Prop :=
  Cases l of 
     nil => True
   | (cons p' l') => 
	(interp_proposition envp env p') /\ (interp_hyps envp env l')
  end.

(* \paragraph{sous forme de but}
   C'est cette interpétation que l'on utilise sur le but (car on utilise
   [Generalize] et qu'une conjonction est forcément lourde (répétition des
   types dans les conjonctions intermédiaires) *)

Fixpoint interp_goal_concl [envp: PropList;env : (list Z); c: proposition; l: hyps] : Prop :=
  Cases l of 
     nil => (interp_proposition envp env c)
   | (cons p' l') => 
	(interp_proposition envp env p') -> (interp_goal_concl envp env c l')
  end.

Syntactic Definition interp_goal  :=
  [envp: PropList;env : (list Z); l: hyps]
	(interp_goal_concl envp env FalseTerm l).

(* Les théorèmes qui suivent assurent la correspondance entre les deux
   interprétations. *)

Theorem goal_to_hyps : 
  (envp: PropList; env : (list Z); l: hyps) 
     ((interp_hyps envp env l) -> False) -> (interp_goal envp env l).

Induction l; [
  Simpl; Auto
| Simpl; Intros a l1 H1 H2 H3; Apply H1; Intro H4; Apply H2; Auto ].
Save.

Theorem hyps_to_goal : 
  (envp: PropList; env : (list Z); l: hyps) 
     (interp_goal envp env l) -> ((interp_hyps envp env l) -> False).

Induction l; Simpl; [
  Auto
| Intros; Apply H; Elim H1; Auto ].
Save.
      
(* \subsection{Manipulations sur les hypothèses} *)

(* \subsubsection{Définitions de base de stabilité pour la réflexion} *)
(* Une opération laisse un terme stable si l'égalité est préservée *)
Definition term_stable [f: term -> term] :=
 (e: (list Z); t:term) (interp_term e t) = (interp_term e (f t)).

(* Une opération est valide sur une hypothèse, si l'hypothèse implique le
   résultat de l'opération. \emph{Attention : cela ne concerne que des 
   opérations sur les hypothèses et non sur les buts (contravariance)}.
   On définit la validité pour une opération prenant une ou deux propositions
   en argument (cela suffit pour omega). *)

Definition valid1 [f: proposition -> proposition] :=
  (ep : PropList; e: (list Z)) (p1: proposition) 
    (interp_proposition ep e p1) -> (interp_proposition ep e (f p1)).

Definition valid2 [f: proposition -> proposition -> proposition] :=
  (ep : PropList; e: (list Z)) (p1,p2: proposition) 
    (interp_proposition ep e p1) -> (interp_proposition ep e p2) ->
      (interp_proposition ep e (f p1 p2)).

(* Dans cette notion de validité, la fonction prend directement une 
   liste de propositions et rend une nouvelle liste de proposition. 
   On reste contravariant *)

Definition valid_hyps [f: hyps -> hyps] :=
  (ep : PropList; e : (list Z))
    (lp: hyps) (interp_hyps ep e lp) -> (interp_hyps ep e (f lp)).

(* Enfin ce théorème élimine la contravariance et nous ramène à une 
   opération sur les buts *)

 Theorem valid_goal :
  (ep: PropList; env : (list Z); l: hyps; a : hyps -> hyps) 
    (valid_hyps a) -> (interp_goal ep env (a l)) -> (interp_goal ep env l).

Intros; Simpl; Apply goal_to_hyps; Intro H1;
Apply (hyps_to_goal ep env (a l) H0); Apply H; Assumption.
Save.

(* \subsubsection{Généralisation a des listes de buts (disjonctions)} *)


Fixpoint interp_list_hyps [envp: PropList; env: (list Z); l : lhyps] : Prop :=
   Cases l of
      nil => False
    | (cons h l') => (interp_hyps envp env h) \/ (interp_list_hyps envp env l')
   end.

Fixpoint interp_list_goal [envp: PropList; env: (list Z);l : lhyps] : Prop :=
   Cases l of
      nil => True
    | (cons h l') => (interp_goal envp env h) /\ (interp_list_goal envp env l')
   end.

Theorem list_goal_to_hyps : 
  (envp: PropList; env: (list Z); l: lhyps)
    ((interp_list_hyps envp env l) -> False) -> (interp_list_goal envp env l).

Induction l; Simpl; [
  Auto
| Intros h1 l1 H H1; Split; [
    Apply goal_to_hyps; Intro H2; Apply H1; Auto
  | Apply H; Intro H2; Apply H1; Auto ]].
Save.

Theorem list_hyps_to_goal : 
  (envp: PropList; env: (list Z); l: lhyps)
    (interp_list_goal envp env l) -> ((interp_list_hyps envp env l) -> False).

Induction l; Simpl; [
  Auto
|  Intros h1 l1 H (H1,H2) H3; Elim H3; Intro H4; [
     Apply hyps_to_goal with 1 := H1; Assumption
   | Auto ]].
Save.

Definition valid_list_hyps [f: hyps -> lhyps] :=
  (ep : PropList; e : (list Z)) (lp: hyps)
    (interp_hyps ep e lp) -> (interp_list_hyps ep e (f lp)).

Definition valid_list_goal [f: hyps -> lhyps] :=
  (ep : PropList; e : (list Z)) (lp: hyps) 
     (interp_list_goal ep e (f lp)) -> (interp_goal ep e lp) .

Theorem goal_valid : 
  (f: hyps -> lhyps) (valid_list_hyps f) -> (valid_list_goal f).

Unfold valid_list_goal; Intros f H ep e lp H1; Apply goal_to_hyps;
Intro H2; Apply list_hyps_to_goal with 1:=H1; Apply (H ep e lp); Assumption.
Save.
 
Theorem append_valid :
  (ep: PropList; e: (list Z)) (l1,l2:lhyps)
     (interp_list_hyps ep e l1) \/ (interp_list_hyps ep e l2) ->
     (interp_list_hyps ep e (app l1 l2)).

Intros ep e; Induction l1; [
  Simpl; Intros l2 [H | H]; [ Contradiction | Trivial ]
| Simpl; Intros h1 t1 HR l2 [[H | H] | H] ;[
    Auto
  | Right; Apply (HR l2); Left; Trivial
  | Right; Apply (HR l2); Right; Trivial ]].

Save.

(* \subsubsection{Opérateurs valides sur les hypothèses} *)

(* Extraire une hypothèse de la liste *)
Definition nth_hyps [n:nat; l: hyps] := (nth n l TrueTerm).

Theorem nth_valid :
  (ep: PropList; e: (list Z); i:nat; l: hyps) 
     (interp_hyps ep e l) -> (interp_proposition ep e (nth_hyps i l)).

Unfold nth_hyps; Induction i; [
  Induction l; Simpl; [ Auto | Intros; Elim H0; Auto ]
| Intros n H; Induction l;
    [ Simpl; Trivial | Intros; Simpl; Apply H; Elim H1; Auto ]].
Save.

(* Appliquer une opération (valide) sur deux hypothèses extraites de 
   la liste et ajouter le résultat à la liste. *)
Definition apply_oper_2 
  [i,j : nat; f : proposition -> proposition -> proposition ] :=
  [l: hyps] (cons (f (nth_hyps i l)  (nth_hyps j l)) l).

Theorem apply_oper_2_valid :
  (i,j : nat; f : proposition -> proposition -> proposition )
    (valid2 f) -> (valid_hyps (apply_oper_2 i j f)).

Intros i j f Hf; Unfold apply_oper_2 valid_hyps; Simpl; Intros lp Hlp; Split;
  [ Apply Hf; Apply nth_valid; Assumption | Assumption].
Save.

(* Modifier une hypothèse par application d'une opération valide *)

Fixpoint apply_oper_1 [i:nat] : (proposition -> proposition) -> hyps -> hyps :=
  [f : (proposition -> proposition); l : hyps] 
    Cases l of 
       nil => (nil proposition)
    | (cons p l') =>
	 Cases i of
           O => (cons (f p) l')
         | (S j) => (cons p (apply_oper_1 j f l'))
         end
    end.

Theorem apply_oper_1_valid :
  (i : nat; f : proposition -> proposition )
    (valid1 f) -> (valid_hyps (apply_oper_1 i f)).

Unfold valid_hyps; Intros i f Hf ep e; Elim i; [
  Intro lp; Case lp; [
    Simpl; Trivial
  | Simpl; Intros p l' (H1, H2); Split; [ Apply Hf with 1:=H1 | Assumption ]]
| Intros n Hrec lp; Case lp; [
    Simpl; Auto
  | Simpl; Intros p l' (H1, H2); 
    Split; [ Assumption | Apply Hrec; Assumption ]]].

Save.

(* \subsubsection{Manipulations de termes} *)
(* Les fonctions suivantes permettent d'appliquer une fonction de
   réécriture sur un sous terme du terme principal. Avec la composition,
   cela permet de construire des réécritures complexes proches des 
   tactiques de conversion *)

Definition apply_left [f: term -> term; t : term]:= 
  Cases t of
    (Tplus x y) => (Tplus (f x) y)
  | (Tmult x y) => (Tmult (f x) y)
  | (Topp x) => (Topp (f x))
  | x => x
  end.

Definition apply_right [f: term -> term; t : term]:= 
  Cases t of
    (Tplus x y) => (Tplus x (f y))
  | (Tmult x y) => (Tmult x (f y))
  | x => x
  end.

Definition apply_both [f,g: term -> term; t : term]:= 
  Cases t of
    (Tplus x y) => (Tplus (f x) (g y))
  | (Tmult x y) => (Tmult (f x) (g y))
  | x => x
  end.

(* Les théorèmes suivants montrent la stabilité (conditionnée) des 
   fonctions. *)

Theorem apply_left_stable :
  (f: term -> term) (term_stable f) -> (term_stable (apply_left f)).

Unfold term_stable; Intros f H e t; Case t; Auto; Simpl; 
Intros;  Elim H; Trivial.
Save.

Theorem apply_right_stable :
  (f: term -> term) (term_stable f) -> (term_stable (apply_right f)).

Unfold term_stable; Intros f H e t; Case t; Auto; Simpl; 
Intros t0 t1; Elim H; Trivial.
Save.

Theorem apply_both_stable :
  (f,g: term -> term) (term_stable f) -> (term_stable g) -> 
     (term_stable (apply_both f g)).

Unfold term_stable; Intros f g H1 H2 e t; Case t; Auto; Simpl; 
Intros t0 t1; Elim H1; Elim H2; Trivial.
Save.

Theorem compose_term_stable :
  (f,g: term -> term) (term_stable f) -> (term_stable g) -> 
    (term_stable [t: term](f (g t))).

Unfold term_stable; Intros f g Hf Hg e t; Elim Hf; Apply Hg.
Save.

(* \subsection{Les règles de réécriture} *)
(* Chacune des règles de réécriture est accompagnée par sa preuve de 
   stabilité. Toutes ces preuves ont la même forme : il faut analyser 
   suivant la forme du terme (élimination de chaque Case). On a besoin d'une
   élimination uniquement dans les cas d'utilisation d'égalité décidable. 

   Cette tactique itère la décomposition des Case. Elle est
   constituée de deux fonctions s'appelant mutuellement :
   \begin{itemize} 
    \item une fonction d'enrobage qui lance la recherche sur le but,
    \item une fonction récursive qui décompose ce but. Quand elle a trouvé un
          Case, elle l'élimine. 
   \end{itemize}  
   Les motifs sur les cas sont très imparfaits et dans certains cas, il
   semble que cela ne marche pas. On aimerait plutot un motif de la
   forme [ Case (?1 :: T) of _ end ] permettant de s'assurer que l'on 
   utilise le bon type.

   Chaque élimination introduit correctement exactement le nombre d'hypothèses
   nécessaires et conserve dans le cas d'une égalité la connaissance du
   résultat du test en faisant la réécriture. Pour un test de comparaison,
   on conserve simplement le résultat.

   Cette fonction déborde très largement la résolution des réécritures
   simples et fait une bonne partie des preuves des pas de Omega.
*)

(* \subsubsection{La tactique pour prouver la stabilité} *)

Recursive Tactic Definition loop t := (
  Match t With
  (* Global *)
    [(?1 = ?2)] -> (loop ?1) Orelse (loop ?2)
  | [ ? -> ?1 ] ->  (loop ?1)
  (* Interpretations *)
  | [ (interp_hyps ? ? ?1) ] -> (loop ?1)
  | [ (interp_list_hyps ? ? ?1) ] -> (loop ?1)
  | [ (interp_proposition ? ? ?1) ] -> (loop ?1)
  | [ (interp_term ? ?1) ] -> (loop ?1)
  (* Propositions *)
  | [(EqTerm ?1 ?2)] -> (loop ?1) Orelse (loop ?2)
  | [(LeqTerm ?1 ?2)] -> (loop ?1) Orelse (loop ?2)
  (* Termes *)
  | [(Tplus ?1 ?2)] -> (loop ?1) Orelse (loop ?2)
  | [(Tminus ?1 ?2)] -> (loop ?1) Orelse (loop ?2)
  | [(Tmult ?1 ?2)] -> (loop ?1) Orelse (loop ?2)
  | [(Topp ?1)] -> (loop ?1)
  | [(Tint ?1)] -> (loop ?1)
  (* Eliminations *)
  |  [(Cases ?1 of
        | (EqTerm _ _) => ?
        | (LeqTerm _ _) => ?
        | TrueTerm => ?
        | FalseTerm => ?
        | (Tnot _) => ?
        | (GeqTerm _ _) => ?
        | (GtTerm _ _) => ?
        | (LtTerm _ _) => ?
        | (NeqTerm _ _) => ?
        | (Tor _ _) => ?
        | (Tand _ _) => ?
        | (Timp _ _) => ?
        | (Tprop _) => ?
        end)] -> 
       (Case ?1; [ Intro; Intro | Intro; Intro | Idtac | Idtac 
                 | Intro | Intro; Intro | Intro; Intro | Intro; Intro
                 | Intro; Intro
                 | Intro;Intro | Intro;Intro | Intro;Intro | Intro  ]);
        Auto; Simplify
  | [(Cases ?1 of
        (Tint _) => ?
      | (Tplus _ _) => ?
      | (Tmult _ _) => ?
      | (Tminus _ _) => ?
      | (Topp _) => ?
      | (Tvar _) => ?
      end)] -> 
       (Case ?1; [ Intro | Intro; Intro | Intro; Intro | Intro; Intro | 
                   Intro | Intro ]); Auto; Simplify
  | [(Cases (Zcompare ?1 ?2) of
        EGAL => ?
      | INFERIEUR => ?
      | SUPERIEUR => ?
      end)] -> 
       (Elim_Zcompare ?1 ?2) ; Intro ; Auto; Simplify
  | [(Cases ?1 of ZERO => ? | (POS _) => ? | (NEG _) => ? end)] -> 
       (Case ?1; [ Idtac | Intro | Intro ]); Auto; Simplify
  | [(if (eq_Z ?1 ?2) then ? else ?)] -> 
       ((Elim_eq_Z ?1 ?2); Intro H; [Rewrite H; Clear H | Clear H]);
       Simpl; Auto; Simplify
  | [(if (eq_term ?1 ?2) then ? else ?)] -> 
       ((Elim_eq_term ?1 ?2); Intro H; [Rewrite H; Clear H | Clear H]); 
       Simpl; Auto; Simplify
  | [(if (eq_pos ?1 ?2) then ? else ?)] -> 
       ((Elim_eq_pos ?1 ?2); Intro H; [Rewrite H; Clear H | Clear H]);
       Simpl; Auto; Simplify
  | _ -> Fail)
And Simplify := (
  Match Context With [|- ?1 ] -> Try (loop ?1) | _ -> Idtac).


Tactic Definition ProveStable x th :=
  (Match x With [?1] -> Unfold term_stable ?1; Intros; Simplify; Simpl; Apply th).

(* \subsubsection{Les règles elle mêmes} *)
Definition Tplus_assoc_l [t: term] :=
  Cases t of
    (Tplus n (Tplus m p)) => (Tplus (Tplus n m) p)
  | _ => t
  end.

Theorem  Tplus_assoc_l_stable : (term_stable  Tplus_assoc_l).

(ProveStable Tplus_assoc_l Zplus_assoc_l).
Save.

Definition Tplus_assoc_r [t: term] :=
  Cases t of
    (Tplus (Tplus n m) p) => (Tplus n (Tplus m p))
  | _ => t
  end.

Theorem  Tplus_assoc_r_stable : (term_stable  Tplus_assoc_r).

(ProveStable Tplus_assoc_r Zplus_assoc_r).
Save.

Definition Tmult_assoc_r [t: term] :=
  Cases t of
    (Tmult (Tmult n m) p) => (Tmult n (Tmult m p))
  | _ => t
  end.

Theorem  Tmult_assoc_r_stable : (term_stable  Tmult_assoc_r).

(ProveStable Tmult_assoc_r Zmult_assoc_r).
Save.

Definition Tplus_permute [t: term] :=
  Cases t of
    (Tplus n (Tplus m p)) => (Tplus m (Tplus n p))
  | _ => t
  end.

Theorem  Tplus_permute_stable : (term_stable  Tplus_permute).

(ProveStable Tplus_permute Zplus_permute).
Save.

Definition Tplus_sym [t: term] :=
  Cases t of
    (Tplus x y) => (Tplus y x)
  | _ => t
  end.

Theorem Tplus_sym_stable : (term_stable Tplus_sym).

(ProveStable Tplus_sym Zplus_sym).
Save.

Definition Tmult_sym [t: term] :=
  Cases t of
    (Tmult x y) => (Tmult y x)
  | _ => t
  end.

Theorem Tmult_sym_stable : (term_stable Tmult_sym).

(ProveStable Tmult_sym Zmult_sym).
Save.

Definition T_OMEGA10 [t: term] :=
  Cases t of
    (Tplus (Tmult (Tplus (Tmult v (Tint c1)) l1) (Tint k1))
           (Tmult (Tplus (Tmult v' (Tint c2)) l2) (Tint k2))) =>
	Case (eq_term v v') of
	    (Tplus (Tmult v (Tint (Zplus (Zmult c1 k1) (Zmult c2 k2)))) 
                   (Tplus (Tmult l1 (Tint k1)) (Tmult l2 (Tint k2))))
           t
        end
  | _ => t
  end.

Theorem  T_OMEGA10_stable : (term_stable  T_OMEGA10).

(ProveStable T_OMEGA10 OMEGA10).
Save.

Definition T_OMEGA11 [t: term] :=
  Cases t of
    (Tplus (Tmult (Tplus (Tmult v1 (Tint c1)) l1) (Tint k1)) l2) =>
	(Tplus (Tmult v1 (Tint (Zmult c1 k1))) (Tplus (Tmult l1 (Tint k1)) l2))
  | _ => t
  end.

Theorem  T_OMEGA11_stable : (term_stable  T_OMEGA11).

(ProveStable T_OMEGA11 OMEGA11).
Save.

Definition T_OMEGA12 [t: term] :=
  Cases t of
    (Tplus l1 (Tmult (Tplus (Tmult v2 (Tint c2)) l2) (Tint k2))) =>
        (Tplus (Tmult v2 (Tint (Zmult c2 k2))) (Tplus l1 (Tmult l2 (Tint k2))))
  | _ => t
  end.

Theorem  T_OMEGA12_stable : (term_stable  T_OMEGA12).

(ProveStable T_OMEGA12 OMEGA12).
Save. 

Definition T_OMEGA13 [t: term] :=
  Cases t of
    (Tplus (Tplus (Tmult v (Tint (POS x))) l1) 
	   (Tplus (Tmult v' (Tint (NEG x'))) l2)) =>
	Case (eq_term v v') of
	  Case (eq_pos x x') of
	    (Tplus l1 l2)
            t
	  end
	  t
	end
  | (Tplus (Tplus (Tmult v (Tint (NEG x))) l1) 
	   (Tplus (Tmult v' (Tint (POS x'))) l2)) =>
	Case (eq_term v v') of
	  Case (eq_pos x x') of
	    (Tplus l1 l2)
             t
	  end
	  t
	end

  | _ => t
  end.

Theorem  T_OMEGA13_stable : (term_stable  T_OMEGA13).

Unfold term_stable T_OMEGA13; Intros; Simplify; Simpl; 
  [ Apply OMEGA13 | Apply OMEGA14 ].
Save.

Definition T_OMEGA15 [t: term] :=
  Cases t of
    (Tplus (Tplus (Tmult v (Tint c1)) l1) 
	   (Tmult (Tplus (Tmult v' (Tint c2)) l2) (Tint k2))) =>
	Case (eq_term v v') of
	  (Tplus (Tmult v (Tint (Zplus c1 (Zmult c2 k2))))
	                  (Tplus l1 (Tmult l2 (Tint k2))))
	  t
	end
  | _ => t
  end.

Theorem  T_OMEGA15_stable : (term_stable  T_OMEGA15).

(ProveStable T_OMEGA15 OMEGA15).
Save.

Definition T_OMEGA16 [t: term] :=
  Cases t of
    (Tmult (Tplus (Tmult v (Tint c)) l) (Tint k)) =>
       (Tplus (Tmult v (Tint (Zmult c k))) (Tmult l (Tint k)))
  | _ => t
  end.


Theorem  T_OMEGA16_stable : (term_stable  T_OMEGA16).

(ProveStable T_OMEGA16 OMEGA16).
Save.

Definition Tred_factor5 [t: term] := 
   Cases t of
      (Tplus (Tmult x (Tint ZERO)) y) => y
   | _ => t
   end.

Theorem Tred_factor5_stable : (term_stable  Tred_factor5).


(ProveStable Tred_factor5 Zred_factor5).
Save.

Definition Topp_plus [t: term] :=
  Cases t of
    (Topp (Tplus x y)) => (Tplus (Topp x) (Topp y))
  | _ => t
  end.

Theorem Topp_plus_stable : (term_stable Topp_plus).

(ProveStable Topp_plus Zopp_Zplus).
Save.


Definition Topp_opp [t: term] :=
  Cases t of
    (Topp (Topp x)) => x
  | _ => t
  end.

Theorem Topp_opp_stable : (term_stable Topp_opp).

(ProveStable Topp_opp Zopp_Zopp).
Save.

Definition Topp_mult_r [t: term] :=
  Cases t of
    (Topp (Tmult x (Tint k))) => (Tmult x (Tint (Zopp k)))
  | _ => t
  end.

Theorem Topp_mult_r_stable : (term_stable Topp_mult_r).

(ProveStable Topp_mult_r Zopp_Zmult_r).
Save.

Definition Topp_one [t: term] :=
  Cases t of
    (Topp x) => (Tmult x (Tint `-1`))
  | _ => t
  end.

Theorem Topp_one_stable : (term_stable Topp_one).

(ProveStable Topp_one Zopp_one).
Save.

Definition Tmult_plus_distr  [t: term] :=
  Cases t of
    (Tmult (Tplus n m) p) => (Tplus (Tmult n p) (Tmult m p))
  | _ => t
  end.

Theorem Tmult_plus_distr_stable : (term_stable Tmult_plus_distr).

(ProveStable Tmult_plus_distr Zmult_plus_distr).
Save.

Definition Tmult_opp_left [t: term] :=
  Cases t of
    (Tmult (Topp x) (Tint y)) => (Tmult x (Tint (Zopp y)))
  | _ => t
  end.

Theorem Tmult_opp_left_stable : (term_stable Tmult_opp_left).

(ProveStable Tmult_opp_left Zmult_Zopp_left).
Save.

Definition Tmult_assoc_reduced [t: term] :=
  Cases t of
    (Tmult (Tmult n (Tint m)) (Tint p)) => (Tmult n (Tint (Zmult m p)))
  | _ => t
  end.

Theorem  Tmult_assoc_reduced_stable : (term_stable  Tmult_assoc_reduced).

(ProveStable Tmult_assoc_reduced Zmult_assoc_r).
Save.

Definition Tred_factor0 [t: term] := (Tmult t (Tint `1`)).

Theorem  Tred_factor0_stable : (term_stable  Tred_factor0).

(ProveStable Tred_factor0 Zred_factor0).
Save.

Definition Tred_factor1 [t: term] :=
  Cases t of
    (Tplus x y) => 
	Case (eq_term x y) of
	  (Tmult x (Tint `2`))
	  t
        end
  | _ => t
  end.

Theorem  Tred_factor1_stable : (term_stable  Tred_factor1).

(ProveStable Tred_factor1 Zred_factor1).
Save.

Definition Tred_factor2 [t: term] :=
  Cases t of
    (Tplus x (Tmult y (Tint k))) => 
	Case (eq_term x y) of
	  (Tmult x (Tint (Zplus `1` k)))
	  t
        end
  | _ => t
  end.

(* Attention : il faut rendre opaque [Zplus] pour éviter que la tactique
   de simplification n'aille trop loin et défasse [Zplus 1 k] *)

Opaque Zplus.

Theorem  Tred_factor2_stable : (term_stable  Tred_factor2).
(ProveStable Tred_factor2 Zred_factor2).
Save.

Definition Tred_factor3 [t: term] :=
  Cases t of
    (Tplus (Tmult x (Tint k)) y) => 
	Case (eq_term x y) of
	  (Tmult x (Tint `1+k`))
	  t
        end
  | _ => t
  end.

Theorem  Tred_factor3_stable : (term_stable  Tred_factor3).

(ProveStable Tred_factor3 Zred_factor3).
Save.


Definition Tred_factor4 [t: term] :=
  Cases t of
    (Tplus (Tmult x (Tint k1)) (Tmult y (Tint k2))) => 
	Case (eq_term x y) of
	  (Tmult x (Tint `k1+k2`))
	  t
        end
  | _ => t
  end.

Theorem  Tred_factor4_stable : (term_stable  Tred_factor4).

(ProveStable Tred_factor4 Zred_factor4).
Save.

Definition Tred_factor6 [t: term] := (Tplus t (Tint `0`)).

Theorem  Tred_factor6_stable : (term_stable  Tred_factor6).

(ProveStable Tred_factor6 Zred_factor6).
Save.

Transparent Zplus.

Definition Tminus_def [t:term] :=
  Cases t of
    (Tminus x y) => (Tplus x (Topp y))
  | _ => t
  end.

Theorem  Tminus_def_stable : (term_stable  Tminus_def).

(* Le théorème ne sert à rien. Le but est prouvé avant. *)
(ProveStable Tminus_def False).
Save.

(* \subsection{Fonctions de réécriture complexes} *)

(* \subsubsection{Fonction de réduction} *)
(* Cette fonction réduit un terme dont la forme normale est un entier. Il
   suffit pour cela d'échanger le constructeur [Tint] avec les opérateurs
   réifiés. La réduction est ``gratuite''.  *)

Fixpoint reduce [t:term] : term :=
  Cases t of
     (Tplus x y) =>
	 Cases (reduce x) of
	   (Tint x') =>
	      Cases (reduce y) of
	        (Tint y') => (Tint (Zplus x' y'))
              | y' => (Tplus (Tint x') y')
              end
         | x' => (Tplus x' (reduce y))
	 end
  | (Tmult x y) =>
	 Cases (reduce x) of
	   (Tint x') =>
	      Cases (reduce y) of
	        (Tint y') => (Tint (Zmult x' y'))
              | y' => (Tmult (Tint x') y')
              end
         | x' => (Tmult x' (reduce y))
	 end
  | (Tminus x y) =>
	 Cases (reduce x) of
	   (Tint x') =>
	      Cases (reduce y) of
	        (Tint y') => (Tint (Zminus x' y'))
              | y' => (Tminus (Tint x') y')
              end
         | x' => (Tminus x' (reduce y))
	 end
  | (Topp x) =>
        Cases (reduce x) of
	  (Tint x') => (Tint (Zopp x'))
	| x' => (Topp x')
	end
  | _ => t
  end.

Theorem reduce_stable : (term_stable reduce).

Unfold term_stable; Intros e t; Elim t; Auto; 
Try (Intros t0 H0 t1 H1; Simpl; Rewrite H0; Rewrite H1; (
 Case (reduce t0); [ 
   Intro z0; Case (reduce t1); Intros; Auto
 | Intros; Auto
 | Intros; Auto
 | Intros; Auto
 | Intros; Auto
 | Intros; Auto ]));
Intros t0 H0; Simpl; Rewrite H0; Case (reduce t0); Intros; Auto.
Save.

(* \subsubsection{Fusions}
    \paragraph{Fusion de deux équations} *)
(* On donne une somme de deux équations qui sont supposées normalisées. 
   Cette fonction prend une trace de fusion en argument et transforme
   le terme en une équation normalisée. C'est une version très simplifiée
   du moteur de réécriture [rewrite]. *)

Fixpoint fusion [trace : (list t_fusion)] : term -> term := [t: term]
  Cases trace of
    nil => (reduce t)
  | (cons step trace') =>
	Cases step of
        | F_equal => 
	    (apply_right (fusion trace') (T_OMEGA10 t))
        | F_cancel => 
	    (fusion trace' (Tred_factor5 (T_OMEGA10 t)))
        | F_left => 
	    (apply_right (fusion trace') (T_OMEGA11 t))
        | F_right =>
	    (apply_right (fusion trace') (T_OMEGA12 t))
	end
  end.
    
Theorem fusion_stable : (t : (list t_fusion)) (term_stable (fusion t)).

Induction t; Simpl; [
  Exact reduce_stable
| Intros stp l H; Case stp; [
    Apply compose_term_stable; 
      [ Apply apply_right_stable; Assumption | Exact T_OMEGA10_stable ]
  | Unfold term_stable; Intros e t1; Rewrite T_OMEGA10_stable; 
    Rewrite Tred_factor5_stable; Apply H
  | Apply compose_term_stable; 
      [ Apply apply_right_stable; Assumption | Exact T_OMEGA11_stable ]
  | Apply compose_term_stable;
      [ Apply apply_right_stable; Assumption | Exact T_OMEGA12_stable ]]].

Save.

(* \paragraph{Fusion de deux équations dont une sans coefficient} *)

Definition fusion_right [trace : (list t_fusion)] : term -> term := [t: term]
  Cases trace of
    nil => (reduce t)  (* Il faut mettre un compute *)
  | (cons step trace') =>
	Cases step of
        | F_equal => 
	    (apply_right (fusion trace') (T_OMEGA15 t))
        | F_cancel => 
	    (fusion trace' (Tred_factor5 (T_OMEGA15 t)))
        | F_left => 
	    (apply_right (fusion trace') (Tplus_assoc_r t))
        | F_right =>
	    (apply_right (fusion trace') (T_OMEGA12 t))
	end
  end.

(* \paragraph{Fusion avec anihilation} *)
(* Normalement le résultat est une constante *)

Fixpoint fusion_cancel [trace:nat] : term -> term := [t:term]
  Cases trace of
    O => (reduce t)
  | (S trace') => (fusion_cancel trace' (T_OMEGA13 t))
  end.

Theorem fusion_cancel_stable : (t:nat) (term_stable (fusion_cancel t)).

Unfold term_stable fusion_cancel; Intros trace e; Elim trace; [
  Exact (reduce_stable e)
| Intros n H t; Elim H; Exact (T_OMEGA13_stable e t) ].
Save. 

(* \subsubsection{Opérations afines sur une équation} *)
(* \paragraph{Multiplication scalaire et somme d'une constante} *)

Fixpoint scalar_norm_add [trace:nat] : term -> term := [t: term]
  Cases trace of
    O => (reduce t)
  | (S trace') => (apply_right (scalar_norm_add trace') (T_OMEGA11 t))
  end.

Theorem scalar_norm_add_stable : (t:nat) (term_stable (scalar_norm_add t)).

Unfold term_stable scalar_norm_add; Intros trace; Elim trace; [
  Exact reduce_stable
| Intros n H e t; Elim apply_right_stable; 
    [ Exact (T_OMEGA11_stable e t) | Exact H ]].
Save.
   
(* \paragraph{Multiplication scalaire} *)
Fixpoint scalar_norm [trace:nat] : term -> term := [t: term]
  Cases trace of
    O => (reduce t)
  | (S trace') => (apply_right (scalar_norm trace') (T_OMEGA16 t))
  end.

Theorem scalar_norm_stable : (t:nat) (term_stable (scalar_norm t)).

Unfold term_stable scalar_norm; Intros trace; Elim trace; [
  Exact reduce_stable
| Intros n H e t; Elim apply_right_stable;
    [ Exact (T_OMEGA16_stable e t) | Exact H ]].
Save.

(* \paragraph{Somme d'une constante} *)
Fixpoint add_norm [trace:nat] : term -> term := [t: term]
  Cases trace of
    O => (reduce t)
  | (S trace') => (apply_right (add_norm trace') (Tplus_assoc_r t))
  end.

Theorem add_norm_stable : (t:nat) (term_stable (add_norm t)).

Unfold term_stable add_norm; Intros trace; Elim trace; [
  Exact reduce_stable
| Intros n H e t; Elim apply_right_stable;
    [ Exact (Tplus_assoc_r_stable e t) | Exact H ]].
Save.

(* \subsection{La fonction de normalisation des termes (moteur de réécriture)} *)


Fixpoint rewrite [s: step] : term -> term :=
  Cases s of 
   | (C_DO_BOTH s1 s2) => (apply_both (rewrite s1) (rewrite s2))
   | (C_LEFT s) => (apply_left (rewrite s))
   | (C_RIGHT s) => (apply_right (rewrite s))
   | (C_SEQ s1 s2) => [t: term] (rewrite s2 (rewrite s1 t))
   | C_NOP => [t:term] t
   | C_OPP_PLUS => Topp_plus
   | C_OPP_OPP => Topp_opp
   | C_OPP_MULT_R => Topp_mult_r
   | C_OPP_ONE => Topp_one
   | C_REDUCE => reduce
   | C_MULT_PLUS_DISTR => Tmult_plus_distr
   | C_MULT_OPP_LEFT => Tmult_opp_left
   | C_MULT_ASSOC_R => Tmult_assoc_r
   | C_PLUS_ASSOC_R => Tplus_assoc_r
   | C_PLUS_ASSOC_L => Tplus_assoc_l
   | C_PLUS_PERMUTE => Tplus_permute
   | C_PLUS_SYM => Tplus_sym
   | C_RED0 => Tred_factor0
   | C_RED1 => Tred_factor1
   | C_RED2 => Tred_factor2
   | C_RED3 => Tred_factor3
   | C_RED4 => Tred_factor4
   | C_RED5 => Tred_factor5
   | C_RED6 => Tred_factor6
   | C_MULT_ASSOC_REDUCED => Tmult_assoc_reduced
   | C_MINUS => Tminus_def
   | C_MULT_SYM => Tmult_sym
  end.

Theorem rewrite_stable : (s:step) (term_stable (rewrite s)).

Induction s; Simpl; [
  Intros; Apply apply_both_stable; Auto
| Intros; Apply apply_left_stable; Auto
| Intros; Apply apply_right_stable; Auto
| Unfold term_stable; Intros; Elim H0; Apply H
| Unfold term_stable; Auto
| Exact Topp_plus_stable
| Exact Topp_opp_stable
| Exact Topp_mult_r_stable
| Exact Topp_one_stable
| Exact reduce_stable
| Exact Tmult_plus_distr_stable
| Exact Tmult_opp_left_stable
| Exact Tmult_assoc_r_stable
| Exact Tplus_assoc_r_stable
| Exact Tplus_assoc_l_stable
| Exact Tplus_permute_stable
| Exact Tplus_sym_stable
| Exact Tred_factor0_stable
| Exact Tred_factor1_stable
| Exact Tred_factor2_stable
| Exact Tred_factor3_stable
| Exact Tred_factor4_stable
| Exact Tred_factor5_stable
| Exact Tred_factor6_stable
| Exact Tmult_assoc_reduced_stable
| Exact Tminus_def_stable
| Exact Tmult_sym_stable ].
Save.

(* \subsection{tactiques de résolution d'un but omega normalisé} 
   Trace de la procédure 
\subsubsection{Tactiques générant une contradiction}
\paragraph{[O_CONSTANT_NOT_NUL]} *)

Definition constant_not_nul [i:nat; h: hyps] :=
  Cases (nth_hyps i h) of
     (EqTerm (Tint ZERO) (Tint n)) =>
	Case (eq_Z n ZERO) of
	    h
            absurd
        end
   | _ => h
  end.

Theorem constant_not_nul_valid : 
  (i:nat) (valid_hyps (constant_not_nul i)).

Unfold valid_hyps constant_not_nul; Intros;
Generalize (nth_valid ep e i lp); Simplify; Simpl; (Elim_eq_Z z0 ZERO); Auto;
Simpl; Intros H1 H2; Elim H1; Symmetry; Auto.
Save.   

(* \paragraph{[O_CONSTANT_NEG]} *)

Definition constant_neg [i:nat; h: hyps] :=
   Cases (nth_hyps i h) of
      (LeqTerm (Tint ZERO) (Tint (NEG n))) => absurd
   | _ => h
   end.

Theorem constant_neg_valid : (i:nat) (valid_hyps (constant_neg i)).

Unfold valid_hyps constant_neg; Intros;
Generalize (nth_valid ep e i lp); Simplify; Simpl; Unfold Zle; Simpl;
Intros H1; Elim H1; [ Assumption | Trivial ].
Save.   

(* \paragraph{[NOT_EXACT_DIVIDE]} *)
Definition not_exact_divide [k1,k2:Z; body:term; t:nat; i : nat; l:hyps] :=
  Cases (nth_hyps i l) of
      (EqTerm (Tint ZERO) b) =>
         Case (eq_term
	         (scalar_norm_add t (Tplus (Tmult body (Tint k1)) (Tint k2))) b) of
	   Cases (Zcompare k2 ZERO) of
	     SUPERIEUR =>
	       Cases (Zcompare k1 k2) of
		 SUPERIEUR => absurd
	       | _ => l
	       end
	   | _ => l
           end
	   l
         end
   | _ => l
   end.

Theorem not_exact_divide_valid : (k1,k2:Z; body:term; t:nat; i:nat) 
	(valid_hyps (not_exact_divide k1 k2 body t i)).

Unfold valid_hyps not_exact_divide; Intros; Generalize (nth_valid ep e i lp);
Simplify;
(Elim_eq_term '(scalar_norm_add t (Tplus (Tmult body (Tint k1)) (Tint k2)))
	     't1); Auto; 
Simplify; 
Intro H2; Elim H2; Simpl; Elim (scalar_norm_add_stable t e); Simpl;
Intro H4; Absurd `(interp_term e body)*k1+k2 = 0`; [
   Apply OMEGA4; Assumption | Symmetry; Auto ].

Save.

(* \paragraph{[O_CONTRADICTION]} *)

Definition contradiction [t: nat; i,j:nat;l:hyps] :=
  Cases (nth_hyps i l) of
    (LeqTerm  (Tint ZERO) b1) =>
	Cases (nth_hyps j l) of 
	  (LeqTerm  (Tint ZERO) b2) => 
	     Cases (fusion_cancel t (Tplus b1 b2)) of
	       (Tint k) =>
		  Cases (Zcompare ZERO k) of
	            SUPERIEUR => absurd
	          | _ => l
                  end
             | _ => l
             end
         | _ => l 
        end
  | _ => l 
  end.

Theorem contradiction_valid : (t,i,j: nat) (valid_hyps (contradiction t i j)).

Unfold valid_hyps contradiction; Intros t i j ep e l H;
Generalize (nth_valid ? ? i ? H); Generalize (nth_valid ? ? j ? H);
Case (nth_hyps i l); Auto; Intros t1 t2; Case t1; Auto; Intros z; Case z; Auto;
Case (nth_hyps j l); Auto; Intros t3 t4; Case t3; Auto; Intros z'; Case z'; 
Auto; Simpl; Intros H1 H2;
Generalize (refl_equal Z (interp_term e (fusion_cancel t (Tplus t2 t4))));
Pattern 2 3 (fusion_cancel t (Tplus t2 t4));
Case (fusion_cancel t (Tplus t2 t4)); 
Simpl; Auto; Intro k; Elim (fusion_cancel_stable t);
Simpl; Intro E; Generalize (OMEGA2 ? ? H2 H1); Rewrite E; Case k; 
Auto;Unfold Zle; Simpl; Intros p H3; Elim H3; Auto.

Save.

(* \paragraph{[O_NEGATE_CONTRADICT]} *)

Definition negate_contradict [i1,i2:nat; h:hyps]:=
  Cases (nth_hyps i1 h) of
    (EqTerm (Tint ZERO) b1) =>
	Cases (nth_hyps i2 h) of
           (NeqTerm (Tint ZERO) b2) =>
	      Cases (eq_term b1 b2) of
	         true => absurd
              |  false => h
	    end
        | _ => h
        end
  | (NeqTerm (Tint ZERO) b1) =>
	Cases (nth_hyps i2 h) of
           (EqTerm (Tint ZERO) b2) =>
	      Cases (eq_term b1 b2) of
	         true => absurd
              |  false => h
	    end
        | _ => h
        end
  | _ => h
  end.

Definition negate_contradict_inv [t:nat; i1,i2:nat; h:hyps]:=
  Cases (nth_hyps i1 h) of
    (EqTerm (Tint ZERO) b1) =>
	Cases (nth_hyps i2 h) of
           (NeqTerm (Tint ZERO) b2) =>
              Cases (eq_term b1 (scalar_norm t (Tmult b2 (Tint `-1`)))) of
	         true => absurd
              |  false => h
	    end
        | _ => h
        end
  | (NeqTerm (Tint ZERO) b1) =>
	Cases (nth_hyps i2 h) of
           (EqTerm (Tint ZERO) b2) =>
              Cases (eq_term b1 (scalar_norm t (Tmult b2 (Tint `-1`)))) of
	         true => absurd
              |  false => h
	    end
        | _ => h
        end
  | _ => h
  end.

Theorem negate_contradict_valid :
  (i,j:nat) (valid_hyps (negate_contradict i j)).

Unfold valid_hyps negate_contradict; Intros i j ep e l H;
Generalize (nth_valid ? ? i ? H); Generalize (nth_valid ? ? j ? H);
Case (nth_hyps i l); Auto; Intros t1 t2; Case t1; Auto; Intros z; Case z; Auto;
Case (nth_hyps j l); Auto; Intros t3 t4; Case t3; Auto; Intros z'; Case z'; 
Auto; Simpl; Intros H1 H2; [
  (Elim_eq_term t2 t4); Intro H3; [ Elim H1; Elim H3; Assumption | Assumption ]
| (Elim_eq_term t2 t4); Intro H3; 
    [ Elim H2; Rewrite H3; Assumption | Assumption ]].

Save.

Theorem negate_contradict_inv_valid :
  (t,i,j:nat) (valid_hyps (negate_contradict_inv t i j)).


Unfold valid_hyps negate_contradict_inv; Intros t i j ep e l H;
Generalize (nth_valid ? ? i ? H); Generalize (nth_valid ? ? j ? H);
Case (nth_hyps i l); Auto; Intros t1 t2; Case t1; Auto; Intros z; Case z; Auto;
Case (nth_hyps j l); Auto; Intros t3 t4; Case t3; Auto; Intros z'; Case z'; 
Auto; Simpl; Intros H1 H2;
(Pattern (eq_term t2 (scalar_norm t (Tmult t4 (Tint (NEG xH))))); Apply bool_ind2; Intro Aux; [
  Generalize (eq_term_true t2 (scalar_norm t (Tmult t4 (Tint (NEG xH)))) Aux);
  Clear Aux
| Generalize (eq_term_false t2 (scalar_norm t (Tmult t4 (Tint (NEG xH)))) Aux);
  Clear Aux ]); [
   Intro H3; Elim H1; Generalize H2; Rewrite H3; 
   Rewrite <- (scalar_norm_stable t e); Simpl; Elim (interp_term e t4) ; 
   Simpl; Auto; Intros p H4; Discriminate H4
 | Auto 
 | Intro H3; Elim H2; Rewrite H3; Elim (scalar_norm_stable t e); Simpl;
   Elim H1; Simpl; Trivial
 | Auto ].

Save.

(* \subsubsection{Tactiques générant une nouvelle équation} *)
(* \paragraph{[O_SUM]}
 C'est une oper2 valide mais elle traite plusieurs cas à la fois (suivant
 les opérateurs de comparaison des deux arguments) d'où une
 preuve un peu compliquée. On utilise quelques lemmes qui sont des 
 généralisations des théorèmes utilisés par OMEGA. *)

Definition sum [k1,k2: Z; trace: (list t_fusion); prop1,prop2:proposition]:=
  Cases prop1 of
    (EqTerm (Tint ZERO) b1) =>
	Cases prop2 of
          (EqTerm (Tint ZERO) b2) =>
	    (EqTerm 
	       (Tint ZERO) 
	       (fusion trace 
	               (Tplus (Tmult b1 (Tint k1)) (Tmult b2 (Tint k2)))))
        | (LeqTerm (Tint ZERO) b2) =>
	    Cases (Zcompare k2 ZERO) of
	       SUPERIEUR =>
		 (LeqTerm 
		    (Tint ZERO) 
		    (fusion trace 
			 (Tplus (Tmult b1 (Tint k1)) (Tmult b2 (Tint k2)))))
            | _ => TrueTerm
           end
       | _ => TrueTerm
       end
  | (LeqTerm (Tint ZERO) b1) =>
      Cases (Zcompare k1 ZERO) of
        SUPERIEUR =>
	  Cases prop2 of
	    (EqTerm (Tint ZERO) b2) =>
	      (LeqTerm 
		 (Tint ZERO) 
		 (fusion trace 
			 (Tplus (Tmult b1 (Tint k1)) (Tmult b2 (Tint k2)))))
	  | (LeqTerm (Tint ZERO) b2) =>
	       Cases (Zcompare k2 ZERO) of
		  SUPERIEUR =>
		    (LeqTerm 
		       (Tint ZERO) 
		       (fusion trace 
			    (Tplus (Tmult b1 (Tint k1)) 
                                   (Tmult b2 (Tint k2)))))
	       | _ => TrueTerm
	      end
	 | _ => TrueTerm
	 end
     | _ => TrueTerm
     end
  | (NeqTerm (Tint ZERO) b1) =>
       Cases prop2 of
	 (EqTerm (Tint ZERO) b2) =>
	    Case (eq_Z k1 ZERO) of
	       TrueTerm
	       (NeqTerm 
		  (Tint ZERO) 
		  (fusion trace 
			  (Tplus (Tmult b1 (Tint k1)) (Tmult b2 (Tint k2)))))
	    end
      | _ => TrueTerm
      end
  | _ => TrueTerm
  end.

Theorem sum1 :
  (a,b,c,d:Z) (`0 = a`) -> (`0 = b`) -> (`0 = a*c + b*d`).

Intros; Elim H; Elim H0; Simpl; Auto.
Save.
  
Theorem sum2 :
  (a,b,c,d:Z)  (`0 <= d`) -> (`0 = a`) -> (`0 <= b`) ->(`0 <= a*c + b*d`).

Intros; Elim H0; Simpl; Generalize H H1; Case b; Case d; 
Unfold Zle; Simpl; Auto.  
Save.

Theorem sum3 :
  (a,b,c,d:Z)  (`0 <= c`) -> (`0 <= d`) -> (`0 <= a`) -> (`0 <= b`) ->(`0 <= a*c + b*d`).

Intros a b c d; Case a; Case b; Case c; Case d; Unfold Zle; Simpl; Auto. 
Save.

Theorem sum4 : (k:Z) (Zcompare k `0`)=SUPERIEUR -> (`0 <= k`).

Intro; Case k; Unfold Zle; Simpl; Auto; Intros; Discriminate.  
Save.

Theorem sum5 :
  (a,b,c,d:Z) (`c <> 0`) -> (`0 <> a`) -> (`0 = b`) -> (`0 <> a*c + b*d`).

Intros a b c d H1 H2 H3; Elim H3; Simpl; Rewrite Zplus_sym;
Simpl; Generalize H1 H2; Case a; Case c; Simpl; Intros; Try Discriminate;
Assumption.
Save.


Theorem sum_valid : (k1,k2:Z; t:(list t_fusion)) (valid2 (sum k1 k2 t)).

Unfold valid2; Intros k1 k2 t ep e p1 p2; Unfold sum; Simplify; Simpl; Auto;
Try (Elim (fusion_stable t)); Simpl; Intros; [
  Apply sum1; Assumption
| Apply sum2; Try Assumption; Apply sum4; Assumption
| Rewrite Zplus_sym; Apply sum2; Try Assumption; Apply sum4; Assumption
| Apply sum3; Try Assumption; Apply sum4; Assumption
| (Elim_eq_Z k1 ZERO); Simpl; Auto; Elim (fusion_stable t); Simpl; Intros;
  Unfold Zne; Apply sum5; Assumption].
Save.

(* \paragraph{[O_EXACT_DIVIDE]}
   c'est une oper1 valide mais on préfère une substitution a ce point la *)

Definition exact_divide [k:Z; body:term; t: nat; prop:proposition] :=
   Cases prop of
      (EqTerm (Tint ZERO) b) =>
         Case (eq_term (scalar_norm t (Tmult body (Tint k))) b) of
	   Case (eq_Z k ZERO) of
	      TrueTerm
	      (EqTerm (Tint ZERO) body)
           end
           TrueTerm
         end
   | _ => TrueTerm
   end.

Theorem exact_divide_valid :
  (k:Z) (t:term) (n:nat) (valid1 (exact_divide k t n)).


Unfold valid1 exact_divide; Intros k1 k2 t ep e p1; Simplify;Simpl; Auto;
(Elim_eq_term  '(scalar_norm t (Tmult k2 (Tint k1))) 't1); Simpl; Auto;
(Elim_eq_Z 'k1 'ZERO); Simpl; Auto;  Intros H1 H2; Elim H2; 
Elim scalar_norm_stable; Simpl; Generalize H1; Case (interp_term e k2);
Try Trivial; (Case k1; Simpl; [
  Intros; Absurd `0 = 0`; Assumption
| Intros p2 p3 H3 H4; Discriminate H4
| Intros p2 p3 H3 H4; Discriminate H4 ]).

Save.



(* \paragraph{[O_DIV_APPROX]}
  La preuve reprend le schéma de la précédente mais on
  est sur une opération de type valid1 et non sur une opération terminale. *)

Definition divide_and_approx [k1,k2:Z; body:term; t:nat; prop:proposition] :=
  Cases prop of
      (LeqTerm (Tint ZERO) b) =>
         Case (eq_term
                (scalar_norm_add t (Tplus (Tmult body (Tint k1)) (Tint k2))) b) of
	   Cases (Zcompare k1 ZERO) of
	     SUPERIEUR =>
	       Cases (Zcompare k1 k2) of
		 SUPERIEUR =>(LeqTerm (Tint ZERO) body)
	       | _ => prop
	       end
	   | _ => prop
           end
	   prop
         end
   | _ => prop
   end.

Theorem divide_and_approx_valid : (k1,k2:Z; body:term; t:nat) 
	(valid1 (divide_and_approx k1 k2 body t)).

Unfold valid1 divide_and_approx; Intros k1 k2 body t ep e p1;Simplify;
(Elim_eq_term '(scalar_norm_add t (Tplus (Tmult body (Tint k1)) (Tint k2))) 't1); Simplify; Auto;  Intro E; Elim E; Simpl; 
Elim (scalar_norm_add_stable t e); Simpl; Intro H1; 
Apply Zmult_le_approx with 3 := H1; Assumption.
Save.

(* \paragraph{[MERGE_EQ]} *)

Definition merge_eq [t: nat; prop1, prop2: proposition] :=
  Cases prop1 of
     (LeqTerm (Tint ZERO) b1) =>
	Cases prop2 of
     	  (LeqTerm (Tint ZERO) b2) =>
             Case (eq_term b1 (scalar_norm t (Tmult b2 (Tint `-1`)))) of
	        (EqTerm (Tint ZERO) b1)
 	       	TrueTerm
	     end
        | _ => TrueTerm
	end
  | _ => TrueTerm
  end.

Theorem merge_eq_valid : (n:nat) (valid2 (merge_eq n)).

Unfold valid2 merge_eq; Intros n ep e p1 p2; Simplify; Simpl; Auto;
Elim (scalar_norm_stable n e); Simpl; Intros; Symmetry; 
Apply OMEGA8 with 2 := H0; [ Assumption | Elim Zopp_one; Trivial ].
Save.



(* \paragraph{[O_CONSTANT_NUL]} *)

Definition constant_nul [i:nat; h: hyps] :=
  Cases (nth_hyps i h) of
     (NeqTerm (Tint ZERO) (Tint ZERO)) => absurd
   | _ => h
  end.

Theorem constant_nul_valid : 
  (i:nat) (valid_hyps (constant_nul i)).

Unfold valid_hyps constant_nul; Intros; Generalize (nth_valid ep e i lp);
Simplify; Simpl; Unfold Zne; Intro H1; Absurd `0=0`; Auto.
Save.

(* \paragraph{[O_STATE]} *)

Definition state [m:Z;s:step; prop1,prop2:proposition] :=
  Cases prop1 of
     (EqTerm (Tint ZERO) b1) =>
	Cases prop2 of
	   (EqTerm (Tint ZERO) (Tplus b2 (Topp b3))) =>
	      (EqTerm (Tint ZERO) (rewrite s (Tplus b1 (Tmult (Tplus (Topp b3) b2) (Tint m)))))
	| _ => TrueTerm
	end
  | _ => TrueTerm
  end.

Theorem state_valid : (m:Z; s:step) (valid2 (state m s)).

Unfold valid2; Intros m s ep e p1 p2; Unfold state; Simplify; Simpl;Auto;
Elim (rewrite_stable s e); Simpl; Intros H1 H2; Elim H1;
Rewrite (Zplus_sym `-(interp_term e t5)` `(interp_term e t3)`);
Elim H2; Simpl; Reflexivity.

Save.

(* \subsubsection{Tactiques générant plusieurs but}
   \paragraph{[O_SPLIT_INEQ]} 
   La seule pour le moment (tant que la normalisation n'est pas réfléchie). *)

Definition split_ineq  [i,t: nat; f1,f2:hyps -> lhyps;  l:hyps] :=
  Cases (nth_hyps i l) of
    (NeqTerm  (Tint ZERO) b1) =>
       (app (f1 (cons (LeqTerm (Tint ZERO) (add_norm t (Tplus b1 (Tint `-1`)))) l))
            (f2 (cons (LeqTerm (Tint ZERO) 
                               (scalar_norm_add t 
	                         (Tplus (Tmult b1 (Tint `-1`)) (Tint `-1`))))
                      l)))
  | _ => (cons l (nil ?))
  end.

Theorem split_ineq_valid : 
  (i,t: nat; f1,f2: hyps -> lhyps) 
    (valid_list_hyps f1) ->(valid_list_hyps f2) -> 
      (valid_list_hyps (split_ineq i t f1 f2)).

Unfold valid_list_hyps split_ineq; Intros i t f1 f2 H1 H2 ep e lp H; 
Generalize (nth_valid ? ? i ? H); 
Case (nth_hyps i lp); Simpl; Auto; Intros t1 t2; Case t1; Simpl; Auto;
Intros z; Case z; Simpl; Auto;
Intro H3; Apply append_valid;Elim (OMEGA19 (interp_term e t2)) ;[
  Intro H4; Left; Apply H1; Simpl; Elim (add_norm_stable t); Simpl; Auto
| Intro H4; Right; Apply H2; Simpl; Elim (scalar_norm_add_stable t); 
  Simpl; Auto
| Generalize H3; Unfold Zne not; Intros E1 E2; Apply E1; Symmetry; Trivial ].
Save.


(* \subsection{La fonction de rejeu de la trace} *)

Fixpoint execute_omega [t: t_omega] : hyps -> lhyps := 
  [l : hyps] Cases t of
   | (O_CONSTANT_NOT_NUL n) => (singleton (constant_not_nul n l))
   | (O_CONSTANT_NEG n) => (singleton (constant_neg n l))
   | (O_DIV_APPROX  k1 k2 body t cont n) =>
       (execute_omega cont 
	  (apply_oper_1 n (divide_and_approx k1 k2 body t) l))
   | (O_NOT_EXACT_DIVIDE  k1 k2 body t i) =>
       (singleton (not_exact_divide k1 k2 body t i l))
   | (O_EXACT_DIVIDE k body t cont n) =>
       (execute_omega cont (apply_oper_1 n (exact_divide k body t) l))
   | (O_SUM k1 i1 k2 i2 t cont) =>
       (execute_omega cont (apply_oper_2 i1 i2 (sum k1 k2 t) l))
   | (O_CONTRADICTION t i j) =>
       (singleton (contradiction t i j l))
   | (O_MERGE_EQ t i1 i2 cont) =>
       (execute_omega cont (apply_oper_2 i1 i2 (merge_eq t) l))
   | (O_SPLIT_INEQ t i cont1 cont2) =>
       (split_ineq i t (execute_omega cont1) (execute_omega cont2) l)
   | (O_CONSTANT_NUL i) => (singleton (constant_nul i l))
   | (O_NEGATE_CONTRADICT i j) =>  (singleton (negate_contradict i j l))
   | (O_NEGATE_CONTRADICT_INV t i j) => (singleton (negate_contradict_inv t i j l))
   | (O_STATE m s i1 i2 cont) =>
       (execute_omega cont (apply_oper_2 i1 i2 (state m s) l))
  end.

Theorem omega_valid : (t: t_omega) (valid_list_hyps (execute_omega t)).

Induction t; Simpl; [
  Unfold valid_list_hyps; Simpl; Intros; Left; 
  Apply (constant_not_nul_valid n ep e lp H)
| Unfold valid_list_hyps; Simpl; Intros; Left; 
  Apply (constant_neg_valid n ep e lp H)
| Unfold valid_list_hyps valid_hyps; Intros k1 k2 body n t' Ht' m ep e lp H; 
  Apply Ht';
  Apply (apply_oper_1_valid m (divide_and_approx k1 k2 body n)
	  (divide_and_approx_valid k1 k2 body n) ep e lp H)
| Unfold valid_list_hyps; Simpl; Intros; Left; 
  Apply (not_exact_divide_valid z z0 t0 n n0 ep e lp H)
| Unfold valid_list_hyps valid_hyps; Intros k body n t' Ht' m ep e lp H; 
  Apply Ht';
  Apply (apply_oper_1_valid m (exact_divide k body n)
	  (exact_divide_valid k body n) ep e lp H)
| Unfold valid_list_hyps valid_hyps; Intros k1 i1 k2 i2 trace t' Ht' ep e lp H;
  Apply Ht'; 
  Apply (apply_oper_2_valid i1 i2 (sum k1 k2 trace) 
	  (sum_valid k1 k2 trace) ep e lp H)
| Unfold valid_list_hyps; Simpl; Intros; Left; 
  Apply (contradiction_valid n n0 n1 ep e lp H)
| Unfold valid_list_hyps valid_hyps; Intros trace i1 i2 t' Ht' ep e lp H; 
  Apply Ht';
  Apply (apply_oper_2_valid i1 i2 (merge_eq trace) 
          (merge_eq_valid trace) ep e lp H) 
| Intros t' i k1 H1 k2 H2; Unfold valid_list_hyps; Simpl; Intros ep e lp H;
  Apply (split_ineq_valid i t' (execute_omega k1) (execute_omega k2) 
	 H1 H2 ep e lp H)
| Unfold valid_list_hyps; Simpl; Intros i ep e lp H; Left; 
  Apply (constant_nul_valid i ep e lp H)
| Unfold valid_list_hyps; Simpl; Intros i j ep e lp H; Left; 
  Apply (negate_contradict_valid i j ep e lp H)
| Unfold valid_list_hyps; Simpl; Intros n i j ep e lp H; Left; 
  Apply (negate_contradict_inv_valid n i j ep e lp H)
| Unfold valid_list_hyps valid_hyps; Intros m s i1 i2 t' Ht' ep e lp H; Apply Ht';
  Apply (apply_oper_2_valid i1 i2 (state m s) (state_valid m s) ep e lp H)
].
Save.


(* \subsection{Les opérations globales sur le but} 
   \subsubsection{Normalisation} *)

Definition move_right [s: step; p:proposition] :=
  Cases p of
     (EqTerm t1 t2) => (EqTerm (Tint ZERO) (rewrite s (Tplus t1 (Topp t2))))
   | (LeqTerm t1 t2) => (LeqTerm (Tint ZERO) (rewrite s (Tplus t2 (Topp t1))))
   | (GeqTerm t1 t2) => (LeqTerm (Tint ZERO) (rewrite s (Tplus t1 (Topp t2))))
   | (LtTerm t1 t2) =>
        (LeqTerm (Tint ZERO)
	         (rewrite s (Tplus (Tplus t2 (Tint `-1`)) (Topp t1))))
   | (GtTerm t1 t2) => 
        (LeqTerm (Tint ZERO)
                 (rewrite s (Tplus (Tplus t1 (Tint `-1`)) (Topp t2))))
   | (NeqTerm t1 t2) => (NeqTerm (Tint ZERO) (rewrite s (Tplus t1 (Topp t2))))
   | p => p
  end.

Theorem Zne_left_2 : (x,y:Z)(Zne x y)->(Zne `0` `x+(-y)`).
Unfold Zne not; Intros x y H1 H2; Apply H1; Apply (Zsimpl_plus_l `-y`);
Rewrite Zplus_sym; Elim H2; Rewrite Zplus_inverse_l; Trivial.
Save.

Theorem move_right_valid : (s: step) (valid1 (move_right s)).

Unfold valid1 move_right; Intros s ep e p; Simplify; Simpl;
Elim (rewrite_stable s e); Simpl; [
  Symmetry; Apply Zegal_left; Assumption
| Intro; Apply Zle_left; Assumption 
| Intro; Apply Zge_left; Assumption
| Intro; Apply Zgt_left; Assumption
| Intro; Apply Zlt_left; Assumption
| Intro; Apply Zne_left_2; Assumption
].
Save.

Definition do_normalize [i:nat; s: step] := (apply_oper_1 i (move_right s)).

Theorem do_normalize_valid : (i:nat; s:step) (valid_hyps (do_normalize i s)).

Intros; Unfold do_normalize; Apply apply_oper_1_valid; Apply move_right_valid.
Save.

Fixpoint do_normalize_list [l:(list step)] : nat -> hyps -> hyps := 
  [i:nat; h:hyps] Cases l of
    (cons s l') => (do_normalize_list l' (S i) (do_normalize i s h))
  | nil => h
  end.

Theorem do_normalize_list_valid : 
  (l:(list step); i:nat) (valid_hyps (do_normalize_list l i)).

Induction l; Simpl; Unfold valid_hyps; [
  Auto
| Intros a l' Hl' i ep e lp H; Unfold valid_hyps in Hl'; Apply Hl';
  Apply (do_normalize_valid i a ep e lp); Assumption ].
Save.

Theorem normalize_goal :
  (s: (list step); ep: PropList; env : (list Z); l: hyps)
    (interp_goal ep env (do_normalize_list s O l)) -> 
      (interp_goal ep env l).

Intros; Apply valid_goal with 2:=H; Apply do_normalize_list_valid.
Save.

(* \subsubsection{Exécution de la trace} *)

Theorem execute_goal :
  (t : t_omega; ep: PropList; env : (list Z); l: hyps)
    (interp_list_goal ep env (execute_omega t l)) -> (interp_goal ep env l).

Intros; Apply (goal_valid (execute_omega t) (omega_valid t) ep env l H).
Save.


Theorem append_goal :
  (ep: PropList; e: (list Z)) (l1,l2:lhyps)
     (interp_list_goal ep e l1) /\ (interp_list_goal ep e l2) ->
     (interp_list_goal ep e (app l1 l2)).

Intros ep e; Induction l1; [
  Simpl; Intros l2 (H1, H2); Assumption
| Simpl; Intros h1 t1 HR l2 ((H1 , H2), H3) ; Split; Auto].

Save.

Require Decidable.

(* A simple decidability checker : if the proposition belongs to the
   simple grammar describe below then it is decidable. Proof is by 
   induction and uses well known theorem about arithmetic and propositional
   calculus *)

Fixpoint decidability [p:proposition] : bool :=
  Cases p of
    (EqTerm _ _) => true
  | (LeqTerm _ _) => true
  | (GeqTerm _ _) => true
  | (GtTerm _ _) => true
  | (LtTerm _ _) => true
  | (NeqTerm _ _) => true
  | (FalseTerm) => true
  | (TrueTerm) => true
  | (Tnot t) => (decidability t)
  | (Tand t1 t2) => (andb (decidability t1) (decidability t2))
  | (Timp t1 t2) => (andb (decidability t1) (decidability t2))
  | (Tor t1 t2) =>  (andb (decidability t1) (decidability t2))
  | (Tprop _) => false
  end
.

Theorem decidable_correct :
  (ep: PropList) (e: (list Z)) (p:proposition)
    (decidability p)=true -> (decidable (interp_proposition ep e p)).

Induction p; Simpl; Intros; [
  Apply dec_eq
| Apply dec_Zle
| Left;Auto
| Right; Unfold not; Auto
| Apply dec_not; Auto
| Apply dec_Zge
| Apply dec_Zgt
| Apply dec_Zlt
| Apply dec_Zne
| Apply dec_or; Elim andb_prop with 1 := H1; Auto
| Apply dec_and; Elim andb_prop with 1 := H1; Auto
| Apply dec_imp; Elim andb_prop with 1 := H1; Auto
| Discriminate H].

Save.

(* An interpretation function for a complete goal with an explicit
   conclusion. We use an intermediate fixpoint. *)

Fixpoint interp_full_goal 
    [envp: PropList;env : (list Z); c : proposition; l: hyps] : Prop :=
  Cases l of 
     nil => (interp_proposition envp env c)
   | (cons p' l') => 
	(interp_proposition envp env p') -> (interp_full_goal envp env c l')
  end.

Definition interp_full 
    [ep: PropList;e : (list Z); lc : (hyps * proposition)] : Prop :=
      Cases lc of (l,c) => (interp_full_goal ep e c l) end.

(* Relates the interpretation of a complete goal with the interpretation
   of its hypothesis and conclusion *)

Theorem interp_full_false :
  (ep: PropList; e : (list Z); l: hyps; c : proposition) 
    ((interp_hyps ep e l) -> (interp_proposition ep e c)) -> 
	(interp_full ep e (l,c)).

Induction l; Unfold interp_full; Simpl; [
  Auto
| Intros a l1 H1 c H2 H3; Apply H1; Auto].

Save.

(* Push the conclusion in the list of hypothesis using a double negation
   If the decidability cannot be "proven", then just forget about the 
   conclusion (equivalent of replacing it with false) *)

Definition to_contradict [lc : hyps * proposition] :=
   Cases lc of
      (l,c) => (if (decidability c) then (cons (Tnot c) l) else l)
   end.

(* The previous operation is valid in the sense that the new list of
   hypothesis implies the original goal *)

Theorem to_contradict_valid :
  (ep: PropList; e : (list Z); lc: hyps * proposition)
	(interp_goal ep e (to_contradict lc)) -> (interp_full ep e lc).

Intros ep e lc; Case lc; Intros l c; Simpl; (Pattern (decidability c));
Apply bool_ind2; [
   Simpl; Intros H H1; Apply interp_full_false; Intros H2; Apply not_not; [
     Apply decidable_correct; Assumption
   | Unfold 1 not; Intro H3; Apply hyps_to_goal with 2:=H2; Auto]
| Intros H1 H2; Apply interp_full_false; Intro H3; Elim hyps_to_goal with 1:= H2; Assumption ].
Save.

(* [map_cons x l] adds [x] at the head of each list in [l] (which is a list
   of lists *)

Fixpoint map_cons [A:Set; x:A; l:(list (list A))] : (list (list A)) :=
  Cases l of
    nil => (nil ?)
  | (cons l ll) => (cons (cons x l) (map_cons A x ll))
  end.

(* This function breaks up a list of hypothesis in a list of simpler 
   list of hypothesis that together implie the original one. The goal
   of all this is to transform the goal in a list of solvable problems. 
   Note that :
	- we need a way to drive the analysis as some hypotheis may not
          require a split. 
        - this procedure must be perfectly mimicked by the ML part otherwise
          hypothesis will get desynchronised and this will be a mess.
 *)
 
Fixpoint destructure_hyps [nn: nat] : hyps -> lhyps :=
  [ll:hyps]Cases nn of
    O => (cons ll (nil ?))
  | (S n) =>
       Cases ll of 
	  nil => (cons (nil ?) (nil ?))
       | (cons (Tor p1 p2) l) => 
	    (app (destructure_hyps n (cons p1 l))
	         (destructure_hyps n (cons p2 l)))
       | (cons (Tand p1 p2) l) => 
	    (destructure_hyps n (cons p1 (cons p2 l)))
       | (cons (Timp p1 p2) l) =>
	    (if (decidability p1) then 
	      (app (destructure_hyps n (cons (Tnot p1) l))
		   (destructure_hyps n (cons p2 l)))
	     else (map_cons ? (Timp p1 p2) (destructure_hyps n l)))
       | (cons (Tnot p) l) =>
	    Cases p of 
	       (Tnot p1) =>
		    (if (decidability p1) then (destructure_hyps n (cons p1 l))
		     else (map_cons ? (Tnot (Tnot p1)) (destructure_hyps n l)))
 	    | (Tor p1 p2) =>
		  (destructure_hyps n (cons (Tnot p1) (cons (Tnot p2) l)))
 	    | (Tand p1 p2) =>
   	         (if (decidability p1) then 
 		    (app (destructure_hyps n (cons (Tnot p1) l))
			 (destructure_hyps n (cons (Tnot p2) l)))
		 else (map_cons ? (Tnot p) (destructure_hyps n l)))
	    | _ =>  (map_cons ? (Tnot p) (destructure_hyps n l))
	    end
       | (cons x l) => (map_cons ? x (destructure_hyps n l))
       end
  end.

Theorem map_cons_val : 
  (ep: PropList; e : (list Z))
  (p:proposition;l:lhyps) 
	(interp_proposition ep e p) ->
	(interp_list_hyps ep e l) ->
	(interp_list_hyps ep e (map_cons ? p l) ).

Induction l; Simpl; [ Auto | Intros; Elim H1;  Intro H2; Auto ].
Save.

Hints Resolve map_cons_val append_valid decidable_correct.

Theorem destructure_hyps_valid : 
  (n:nat) (valid_list_hyps (destructure_hyps n)).

Induction n; [
  Unfold valid_list_hyps; Simpl; Auto
| Unfold 2 valid_list_hyps; Intros n1 H  ep e lp; Case lp; [
    Simpl; Auto
  | Intros p l; Case p; 
    Try (Simpl; Intros; Apply map_cons_val; Simpl; Elim H0; Auto); [
      Intro p'; Case p';
      Try (Simpl; Intros; Apply map_cons_val; Simpl; Elim H0; Auto); [
	Simpl; Intros p1 (H1,H2);  Pattern (decidability p1); Apply bool_ind2;
	Intro H3; [
	  Apply H; Simpl; Split; [ Apply not_not; Auto | Assumption ]
        | Auto]
      | Simpl; Intros p1 p2 (H1,H2); Apply H; Simpl; 
	Elim not_or with 1 := H1; Auto
      | Simpl; Intros p1 p2 (H1,H2);Pattern (decidability p1); Apply bool_ind2;
        Intro H3; [
	  Apply append_valid; Elim not_and with 2 := H1; [
	    Intro; Left; Apply H; Simpl; Auto
	  | Intro; Right; Apply H; Simpl; Auto
          | Auto ]
        | Auto ]]
    | Simpl; Intros p1 p2 (H1, H2); Apply append_valid; 
      (Elim H1; Intro H3; Simpl; [ Left | Right ]); Apply H; Simpl; Auto 
    | Simpl; Intros; Apply H; Simpl; Tauto
    | Simpl; Intros p1 p2 (H1, H2); Pattern (decidability p1); Apply bool_ind2;
      Intro H3; [ 
	Apply append_valid; Elim imp_simp with 2:=H1; [
	  Intro H4; Left; Simpl; Apply H; Simpl; Auto
	| Intro H4; Right; Simpl; Apply H; Simpl; Auto
	| Auto ]
      | Auto ]]]].

Save.

Definition prop_stable [f: proposition -> proposition] :=
  (ep: PropList; e: (list Z); p:proposition) 
     (interp_proposition ep e p) <-> (interp_proposition ep e (f p)).

Definition p_apply_left [f: proposition -> proposition; p : proposition]:= 
  Cases p of
    (Timp x y) => (Timp (f x) y)
  | (Tor x y) => (Tor (f x) y)
  | (Tand x y) => (Tand (f x) y)
  | (Tnot x) => (Tnot (f x))
  | x => x
  end.

Theorem p_apply_left_stable :
  (f : proposition -> proposition) 
    (prop_stable f) -> (prop_stable (p_apply_left f)).

Unfold prop_stable; Intros f H ep e p; Split; 
(Case p; Simpl; Auto; Intros p1; Elim (H ep e p1); Tauto).
Save.

Definition p_apply_right [f: proposition -> proposition; p : proposition]:= 
  Cases p of
    (Timp x y) => (Timp x (f y))
  | (Tor x y) => (Tor x (f y))
  | (Tand x y) => (Tand x (f y))
  | (Tnot x) => (Tnot (f x))
  | x => x
  end.

Theorem p_apply_right_stable :
  (f : proposition -> proposition) 
    (prop_stable f) -> (prop_stable (p_apply_right f)).

Unfold prop_stable; Intros f H ep e p; Split; 
(Case p; Simpl; Auto; [
   Intros p1; Elim (H ep e p1); Tauto
 | Intros p1 p2; Elim (H ep e p2); Tauto
 | Intros p1 p2; Elim (H ep e p2); Tauto
 | Intros p1 p2; Elim (H ep e p2); Tauto
 ]).
Save.

Definition p_invert [f : proposition -> proposition; p : proposition] := 
Cases p of
  (EqTerm x y) => (Tnot (f (NeqTerm x y)))
| (LeqTerm x y) => (Tnot (f (GtTerm x y)))
| (GeqTerm x y) => (Tnot (f (LtTerm x y)))
| (GtTerm x y) => (Tnot (f (LeqTerm x y)))
| (LtTerm x y) => (Tnot (f (GeqTerm x y)))
| (NeqTerm x y) => (Tnot (f (EqTerm x y)))
| x => x
end.

Theorem p_invert_stable :
  (f : proposition -> proposition) 
    (prop_stable f) -> (prop_stable (p_invert f)).

Unfold prop_stable; Intros f H ep e p; Split;(Case p; Simpl; Auto; [
  Intros t1 t2; Elim (H ep e (NeqTerm t1 t2)); Simpl; Unfold Zne; 
  Generalize (dec_eq (interp_term e t1) (interp_term e t2)); 
  Unfold decidable; Tauto
| Intros t1 t2; Elim (H ep e (GtTerm t1 t2)); Simpl; Unfold Zgt; 
  Generalize (dec_Zgt (interp_term e t1) (interp_term e t2)); 
  Unfold decidable Zgt Zle; Tauto
| Intros t1 t2; Elim (H ep e (LtTerm t1 t2)); Simpl; Unfold Zlt; 
  Generalize (dec_Zlt (interp_term e t1) (interp_term e t2)); 
  Unfold decidable Zge; Tauto
| Intros t1 t2; Elim (H ep e (LeqTerm t1 t2)); Simpl; 
  Generalize (dec_Zgt (interp_term e t1) (interp_term e t2)); Unfold Zle Zgt;
  Unfold decidable; Tauto
| Intros t1 t2; Elim (H ep e (GeqTerm t1 t2)); Simpl;
  Generalize (dec_Zlt (interp_term e t1) (interp_term e t2));  Unfold Zge Zlt; 
  Unfold decidable; Tauto
| Intros t1 t2; Elim (H ep e (EqTerm t1 t2)); Simpl;
  Generalize (dec_eq (interp_term e t1) (interp_term e t2)); 
  Unfold decidable Zne; Tauto ]).
Save.

Theorem Zlt_left_inv : (x,y:Z) `0 <= ((y + (-1)) + (-x))` ->  `x<y`.

Intros; Apply Zlt_S_n; Apply Zle_lt_n_Sm; 
Apply (Zsimpl_le_plus_r (Zplus `-1` (Zopp x))); Rewrite Zplus_assoc_l; 
Unfold Zs; Rewrite (Zplus_assoc_r x); Rewrite (Zplus_assoc_l y); Simpl;
Rewrite Zero_right; Rewrite Zplus_inverse_r; Assumption.
Save.

Theorem move_right_stable : (s: step) (prop_stable (move_right s)).

Unfold move_right prop_stable; Intros s ep e p; Split; [
    Simplify; Simpl; Elim (rewrite_stable s e); Simpl; [
    Symmetry; Apply Zegal_left; Assumption
  | Intro; Apply Zle_left; Assumption
  | Intro; Apply Zge_left; Assumption
  | Intro; Apply Zgt_left; Assumption
  | Intro; Apply Zlt_left; Assumption
  | Intro; Apply Zne_left_2; Assumption ]
| Case p; Simpl; Intros; Auto; Generalize H; Elim (rewrite_stable s); Simpl; 
  Intro H1; [
    Rewrite (Zplus_n_O (interp_term e t0)); Rewrite H1; Rewrite Zplus_permute;
    Rewrite Zplus_inverse_r; Rewrite Zero_right; Trivial
  | Apply (Zsimpl_le_plus_r (Zopp (interp_term e t))); Rewrite Zplus_inverse_r;
    Assumption
  | Apply Zle_ge; Apply (Zsimpl_le_plus_r (Zopp (interp_term e t0))); 
    Rewrite Zplus_inverse_r; Assumption
  | Apply Zlt_gt; Apply Zlt_left_inv; Assumption
  | Apply Zlt_left_inv; Assumption
  | Unfold Zne not; Unfold Zne in H1; Intro H2; Apply H1; Rewrite H2;
    Rewrite Zplus_inverse_r; Trivial ]].
Save.


Fixpoint p_rewrite [s: p_step] : proposition -> proposition :=
  Cases s of 
   | (P_LEFT s) => (p_apply_left (p_rewrite s))
   | (P_RIGHT s) => (p_apply_right (p_rewrite s))
   | (P_STEP s) => (move_right s)
   | (P_INVERT s) => (p_invert (move_right s))
   | P_NOP => [p:proposition]p
  end.

Theorem p_rewrite_stable : (s : p_step) (prop_stable (p_rewrite s)).


Induction s; Simpl; [
  Intros; Apply p_apply_left_stable; Trivial
| Intros; Apply p_apply_right_stable; Trivial
| Intros; Apply p_invert_stable; Apply move_right_stable
| Apply move_right_stable
| Unfold prop_stable; Simpl; Intros; Split; Auto ].
Save.

Fixpoint normalize_hyps [l: (list h_step)] : hyps -> hyps :=
  [lh:hyps] Cases l of
    nil => lh
  | (cons (pair_step i s) r) =>
	 (normalize_hyps r (apply_oper_1 i (p_rewrite s) lh))
  end.

Theorem normalize_hyps_valid : 
  (l: (list h_step)) (valid_hyps (normalize_hyps l)).

Induction l; Unfold valid_hyps; Simpl; [
  Auto
| Intros n_s r; Case n_s; Intros n s H ep e lp H1; Apply H; 
  Apply apply_oper_1_valid; [
    Unfold valid1; Intros ep1 e1 p1 H2; Elim (p_rewrite_stable s ep1 e1 p1);
    Auto
  | Assumption ]].
Save.

Theorem normalize_hyps_goal :
  (s: (list h_step); ep: PropList; env : (list Z); l: hyps)
    (interp_goal ep env (normalize_hyps s l)) -> 
      (interp_goal ep env l).

Intros; Apply valid_goal with 2:=H; Apply normalize_hyps_valid.
Save.

Fixpoint extract_hyp_pos [s: (list direction)] : proposition -> proposition :=
  [p: proposition]
  Cases s of 
   | (cons D_left l) =>
	Cases p of
          (Tand x y) => (extract_hyp_pos l x)
        | _ => p
        end
   | (cons D_right l) =>
	Cases p of
          (Tand x y) => (extract_hyp_pos l y)
        | _ => p
        end
   | (cons D_mono l) =>
	Cases p of
          (Tnot x ) => (extract_hyp_neg l x)
        | _ => p
        end
   | _ => p
  end
with extract_hyp_neg [s: (list direction)] : proposition -> proposition :=
  [p: proposition]
  Cases s of 
   | (cons D_left l) =>
	Cases p of
          (Tor x y) => (extract_hyp_neg l x)
	| (Timp x y) =>
	    (if (decidability x) then (extract_hyp_pos l x) else (Tnot p))
        | _ => (Tnot p)
        end
   | (cons D_right l) =>
	Cases p of
          (Tor x y) => (extract_hyp_neg l y)
	| (Timp x y) => (extract_hyp_neg l y)
        | _ => (Tnot p)
        end
   | (cons D_mono l) =>
	Cases p of
          (Tnot x) => 
	     (if (decidability x) then (extract_hyp_pos l x) else (Tnot p))
        | _ => (Tnot p)
        end
   | _ => 
	Cases p of
	  (Tnot x) => (if (decidability x) then x else (Tnot p))
        | _ => (Tnot p) 
	end
  end.

Definition co_valid1 [f: proposition -> proposition] :=
  (ep : PropList; e: (list Z)) (p1: proposition) 
     (interp_proposition ep e (Tnot p1)) -> (interp_proposition ep e (f p1)).

Theorem extract_valid : 
  (s: (list direction))
    ((valid1 (extract_hyp_pos s)) /\ (co_valid1 (extract_hyp_neg s))).

Unfold valid1 co_valid1; Induction s; [
  Split; [
    Simpl; Auto
  | Intros ep e p1; Case p1; Simpl; Auto; Intro p; Pattern (decidability p);
    Apply bool_ind2; [
      Intro H; Generalize (decidable_correct ep e p H); Unfold decidable; Tauto
    | Simpl; Auto]]
| Intros a s' (H1,H2);  Simpl in H2; Split; Intros ep e p; Case a; Auto; 
  Case p; Auto; Simpl; Intros; 
  (Apply H1; Tauto) Orelse (Apply H2; Tauto) Orelse
  (Pattern (decidability p0); Apply bool_ind2; [
     Intro H3; Generalize (decidable_correct ep e p0 H3);Unfold decidable;
     Intro H4; Apply H1; Tauto
   | Intro; Tauto ])].

Save.

Fixpoint decompose_solve [s: e_step] : hyps -> lhyps := 
 [h:hyps]
 Cases s of 
   (E_SPLIT i dl s1 s2) => 
	(Cases (extract_hyp_pos dl (nth_hyps i h)) of
	   (Tor x y) => 
	      (app (decompose_solve s1 (cons x h)) 
	           (decompose_solve s2 (cons y h)))
	|  (Tnot (Tand x y)) => 
	      (if (decidability x) then
		      (app (decompose_solve s1 (cons (Tnot x) h)) 
		           (decompose_solve s2 (cons (Tnot y) h)))
		else (cons h (nil hyps)))
	| _ => (cons h (nil hyps))
	end)
 | (E_EXTRACT i dl s1) =>
     (decompose_solve s1 (cons (extract_hyp_pos dl (nth_hyps i h)) h))
 | (E_SOLVE t) => (execute_omega t h)
 end.

Theorem decompose_solve_valid : 
   (s:e_step)(valid_list_goal (decompose_solve s)).

Intro s; Apply goal_valid; Unfold valid_list_hyps; Elim s; Simpl; Intros; [
  Cut (interp_proposition ep e1 (extract_hyp_pos l (nth_hyps n lp))); [
    Case (extract_hyp_pos l (nth_hyps n lp)); Simpl; Auto; [
      Intro p; Case p; Simpl;Auto; Intros p1 p2 H2;
      Pattern (decidability p1); Apply bool_ind2; [
        Intro H3; Generalize (decidable_correct ep e1 p1 H3); 
        Intro H4; Apply append_valid; Elim H4; Intro H5; [
          Right; Apply H0; Simpl; Tauto
        | Left; Apply H; Simpl; Tauto ]
      | Simpl; Auto]
    | Intros p1 p2 H2; Apply append_valid; Simpl; Elim H2; [
        Intros H3; Left; Apply H; Simpl; Auto
      | Intros H3; Right; Apply H0; Simpl; Auto ]]
  | Elim (extract_valid l); Intros H2 H3; Apply H2; Apply nth_valid; Auto]
| Intros; Apply H; Simpl; Split; [
    Elim (extract_valid l); Intros H2 H3; Apply H2; Apply nth_valid; Auto
  | Auto ]
| Apply omega_valid with 1:= H].

Save.

(* \subsection{La dernière étape qui élimine tous les séquents inutiles} *)

Definition valid_lhyps [f: lhyps -> lhyps] :=
  (ep : PropList; e : (list Z)) (lp: lhyps)
    (interp_list_hyps ep e lp) -> (interp_list_hyps ep e (f lp)).

Fixpoint reduce_lhyps [lp:lhyps] : lhyps :=
   Cases lp of
     (cons (cons FalseTerm nil) lp') => (reduce_lhyps lp')
   | (cons x lp') => (cons x (reduce_lhyps lp'))
   | nil => (nil hyps)
   end.

Theorem reduce_lhyps_valid : (valid_lhyps reduce_lhyps).

Unfold valid_lhyps; Intros ep e lp; Elim lp; [
  Simpl; Auto
| Intros a l HR; Elim a; [
    Simpl; Tauto
  | Intros a1 l1; Case l1; Case a1; Simpl; Try Tauto]].
Save.

Theorem do_reduce_lhyps : 
  (envp: PropList; env: (list Z); l: lhyps)
    (interp_list_goal envp env (reduce_lhyps l)) ->
	 (interp_list_goal envp env l).

Intros envp env l H; Apply list_goal_to_hyps; Intro H1; 
Apply list_hyps_to_goal with 1 := H; Apply reduce_lhyps_valid; Assumption.
Save.

Definition concl_to_hyp := [p:proposition]
  (if (decidability p) then (Tnot p) else TrueTerm).

Definition do_concl_to_hyp :
  (envp: PropList; env: (list Z); c : proposition; l:hyps)
    (interp_goal envp env (cons (concl_to_hyp c) l)) ->
       (interp_goal_concl envp env c l).

Simpl; Intros envp env c l; Induction l; [
  Simpl; Unfold concl_to_hyp; Pattern (decidability c); Apply bool_ind2; [
    Intro H; Generalize (decidable_correct envp env c H); Unfold decidable;
    Simpl; Tauto
  | Simpl; Intros H1 H2; Elim H2; Trivial]
| Simpl; Tauto ].
Save.

Definition omega_tactic := 
  [t1:e_step ; t2:(list h_step) ; c:proposition; l:hyps] 
    (reduce_lhyps 
      (decompose_solve t1 (normalize_hyps t2 (cons (concl_to_hyp c) l)))).

Theorem do_omega:
  (t1: e_step ; t2: (list h_step);
   envp: PropList; env: (list Z); c: proposition; l:hyps)
    (interp_list_goal envp env (omega_tactic t1 t2 c l)) ->
       (interp_goal_concl envp env c l).

Unfold omega_tactic; Intros; Apply do_concl_to_hyp; 
Apply (normalize_hyps_goal t2); Apply (decompose_solve_valid t1); 
Apply do_reduce_lhyps; Assumption.
Save.