summaryrefslogtreecommitdiff
path: root/contrib7/romega/ReflOmegaCore.v
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
commit3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch)
treead89c6bb57ceee608fcba2bb3435b74e0f57919e /contrib7/romega/ReflOmegaCore.v
parent018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff)
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'contrib7/romega/ReflOmegaCore.v')
-rw-r--r--contrib7/romega/ReflOmegaCore.v2602
1 files changed, 0 insertions, 2602 deletions
diff --git a/contrib7/romega/ReflOmegaCore.v b/contrib7/romega/ReflOmegaCore.v
deleted file mode 100644
index 81baa8d9..00000000
--- a/contrib7/romega/ReflOmegaCore.v
+++ /dev/null
@@ -1,2602 +0,0 @@
-(*************************************************************************
-
- 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.