ReflOmegaCore: revised proofs (mostly bullets instead of ;[|||])

1 files changed, 477 insertions, 602 deletions

diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index 187601fc6..5fa40f46f 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -413,66 +413,51 @@ Module IntProperties (I:Int).
 
  Definition beq i j := match compare i j with Eq => true | _ => false end.
 
- Lemma beq_iff : forall i j, beq i j = true <-> i=j.
+ Lemma beq_iff i j : beq i j = true <-> i=j.
  Proof.
- intros; unfold beq; generalize (compare_Eq i j).
- destruct compare; intuition discriminate.
+ unfold beq. rewrite <- (compare_Eq i j). now destruct compare.
  Qed.
 
- Lemma beq_true : forall i j, beq i j = true -> i=j.
+ Lemma beq_reflect i j : reflect (i=j) (beq i j).
  Proof.
- intros.
- rewrite <- beq_iff; auto.
- Qed.
-
- Lemma beq_false : forall i j, beq i j = false -> i<>j.
- Proof.
- intros.
- intro H'.
- rewrite <- beq_iff in H'; rewrite H' in H; discriminate.
+ apply iff_reflect. symmetry. apply beq_iff.
  Qed.
 
  Lemma eq_dec : forall n m:int, { n=m } + { n<>m }.
  Proof.
-  intros; generalize (beq_iff n m); destruct beq; [left|right]; intuition.
+  intros n m; generalize (beq_iff n m); destruct beq; [left|right]; intuition.
  Qed.
 
  Definition bgt i j := match compare i j with Gt => true | _ => false end.
 
- Lemma bgt_iff : forall i j, bgt i j = true <-> i>j.
+ Lemma bgt_iff i j : bgt i j = true <-> i>j.
  Proof.
- intros; unfold bgt; generalize (compare_Gt i j).
- destruct compare; intuition discriminate.
+ unfold bgt. rewrite <- (compare_Gt i j). now destruct compare.
  Qed.
 
- Lemma bgt_true : forall i j, bgt i j = true -> i>j.
- Proof. intros; now rewrite <- bgt_iff. Qed.
-
- Lemma bgt_false : forall i j, bgt i j = false -> i<=j.
+ Lemma bgt_reflect i j : reflect (i>j) (bgt i j).
  Proof.
-  intros.
-  rewrite le_lt_iff, <-gt_lt_iff, <-bgt_iff; intro H'; now rewrite H' in H.
+ apply iff_reflect. symmetry. apply bgt_iff.
  Qed.
 
  Lemma le_is_lt_or_eq : forall n m, n<=m -> { n<m } + { n=m }.
  Proof.
-  intros.
+  intros n m Hnm.
   destruct (eq_dec n m) as [H'|H'].
-  right; intuition.
-  left; rewrite lt_le_iff.
-  contradict H'.
-  apply le_antisym; auto.
+  - right; intuition.
+  - left; rewrite lt_le_iff.
+    contradict H'.
+    now apply le_antisym.
  Qed.
 
  Lemma le_neq_lt : forall n m, n<=m -> n<>m -> n<m.
  Proof.
-  intros.
-  destruct (le_is_lt_or_eq _ _ H); intuition.
+  intros n m H. now destruct (le_is_lt_or_eq _ _ H).
  Qed.
 
  Lemma le_trans : forall n m p, n<=m -> m<=p -> n<=p.
  Proof.
-  intros n m p; do 3 rewrite le_lt_iff; intros A B C.
+  intros n m p; rewrite 3 le_lt_iff; intros A B C.
   destruct (lt_eq_lt_dec p m) as [[H|H]|H]; subst; auto.
   generalize (lt_trans _ _ _ H C); intuition.
  Qed.
@@ -482,12 +467,12 @@ Module IntProperties (I:Int).
  Lemma le_0_neg : forall n, 0 <= n <-> -n <= 0.
  Proof.
  intros.
- pattern 0 at 2; rewrite <- (mult_0_l (-(1))).
+ rewrite <- (mult_0_l (-(1))) at 2.
  rewrite <- opp_eq_mult_neg_1.
  split; intros.
- apply opp_le_compat; auto.
- rewrite <-(opp_involutive 0), <-(opp_involutive n).
- apply opp_le_compat; auto.
+ - apply opp_le_compat; auto.
+ - rewrite <-(opp_involutive 0), <-(opp_involutive n).
+   apply opp_le_compat; auto.
  Qed.
 
  Lemma le_0_neg' : forall n, n <= 0 <-> 0 <= -n.
@@ -537,12 +522,12 @@ Module IntProperties (I:Int).
  Lemma lt_0_neg : forall n, 0 < n <-> -n < 0.
  Proof.
  intros.
- pattern 0 at 2; rewrite <- (mult_0_l (-(1))).
+ rewrite <- (mult_0_l (-(1))) at 2.
  rewrite <- opp_eq_mult_neg_1.
  split; intros.
- apply opp_lt_compat; auto.
- rewrite <-(opp_involutive 0), <-(opp_involutive n).
- apply opp_lt_compat; auto.
+ - apply opp_lt_compat; auto.
+ - rewrite <-(opp_involutive 0), <-(opp_involutive n).
+   apply opp_lt_compat; auto.
  Qed.
 
  Lemma lt_0_neg' : forall n, n < 0 <-> 0 < -n.
@@ -557,67 +542,50 @@ Module IntProperties (I:Int).
  apply mult_lt_compat_l; auto.
  Qed.
 
- Lemma mult_integral : forall n m, n * m = 0 -> n = 0 \/ m = 0.
+ Lemma mult_integral_r n m : 0 < n -> n * m = 0 -> m = 0.
  Proof.
- intros.
- destruct (lt_eq_lt_dec n 0) as [[Hn|Hn]|Hn]; auto;
-  destruct (lt_eq_lt_dec m 0) as [[Hm|Hm]|Hm]; auto; exfalso.
-
- rewrite lt_0_neg' in Hn.
- rewrite lt_0_neg' in Hm.
- generalize (mult_lt_0_compat _ _ Hn Hm).
- rewrite <- opp_mult_distr_r, mult_comm, <- opp_mult_distr_r, opp_involutive.
- rewrite mult_comm, H.
- exact (lt_irrefl 0).
-
- rewrite lt_0_neg' in Hn.
- generalize (mult_lt_0_compat _ _ Hn Hm).
- rewrite mult_comm, <- opp_mult_distr_r, mult_comm.
- rewrite H.
- rewrite opp_eq_mult_neg_1, mult_0_l.
- exact (lt_irrefl 0).
-
- rewrite lt_0_neg' in Hm.
- generalize (mult_lt_0_compat _ _ Hn Hm).
- rewrite <- opp_mult_distr_r.
- rewrite H.
- rewrite opp_eq_mult_neg_1, mult_0_l.
- exact (lt_irrefl 0).
-
- generalize (mult_lt_0_compat _ _ Hn Hm).
- rewrite H.
- exact (lt_irrefl 0).
- Qed.
-
- Lemma mult_le_compat :
-   forall i j k l, i<=j -> k<=l -> 0<=i -> 0<=k -> i*k<=j*l.
- Proof.
- intros.
- destruct (le_is_lt_or_eq _ _ H1).
+ intros Hn H.
+ destruct (lt_eq_lt_dec 0 m) as [[Hm| <- ]|Hm]; auto; exfalso.
+ - generalize (mult_lt_0_compat _ _ Hn Hm).
+   rewrite H.
+   exact (lt_irrefl 0).
+ - rewrite lt_0_neg' in Hm.
+   generalize (mult_lt_0_compat _ _ Hn Hm).
+   rewrite <- opp_mult_distr_r, opp_eq_mult_neg_1, H, mult_0_l.
+   exact (lt_irrefl 0).
+ Qed.
 
- apply le_trans with (i*l).
- destruct (le_is_lt_or_eq _ _ H0); [ | subst; apply le_refl].
- apply lt_le_weak.
- apply mult_lt_compat_l; auto.
+ Lemma mult_integral n m : n * m = 0 -> n = 0 \/ m = 0.
+ Proof.
+ intros H.
+ destruct (lt_eq_lt_dec 0 n) as [[Hn|Hn]|Hn].
+ - right; apply (mult_integral_r n m); trivial.
+ - now left.
+ - right; apply (mult_integral_r (-n) m).
+   + now apply lt_0_neg'.
+   + rewrite mult_comm, <- opp_mult_distr_r, mult_comm, H.
+     now rewrite opp_eq_mult_neg_1, mult_0_l.
+ Qed.
 
- generalize (le_trans _ _ _ H2 H0); clear H0 H1 H2; intros.
- rewrite (mult_comm i), (mult_comm j).
- destruct (le_is_lt_or_eq _ _ H0);
-  [ | subst; do 2 rewrite mult_0_l; apply le_refl].
- destruct (le_is_lt_or_eq _ _ H);
-  [ | subst; apply le_refl].
- apply lt_le_weak.
- apply mult_lt_compat_l; auto.
+ Lemma mult_le_compat_l i j k :
+   0<=k -> i<=j -> k*i <= k*j.
+ Proof.
+ intros Hk Hij.
+ apply le_is_lt_or_eq in Hk. apply le_is_lt_or_eq in Hij.
+ destruct Hk as [Hk | <-], Hij as [Hij | <-];
+  rewrite ? mult_0_l; try apply le_refl.
+ now apply lt_le_weak, mult_lt_compat_l.
+ Qed.
 
- subst i.
- rewrite mult_0_l.
- generalize (le_trans _ _ _ H2 H0); clear H0 H1 H2; intros.
- destruct (le_is_lt_or_eq _ _ H);
-  [ | subst; rewrite mult_0_l; apply le_refl].
- destruct (le_is_lt_or_eq _ _ H0);
-  [ | subst; rewrite mult_comm, mult_0_l; apply le_refl].
- apply lt_le_weak.
- apply mult_lt_0_compat; auto.
+ Lemma mult_le_compat i j k l :
+   i<=j -> k<=l -> 0<=i -> 0<=k -> i*k<=j*l.
+ Proof.
+ intros Hij Hkl Hi Hk.
+ apply le_trans with (i*l).
+ - now apply mult_le_compat_l.
+ - rewrite (mult_comm i), (mult_comm j).
+   apply mult_le_compat_l; trivial.
+   now apply le_trans with k.
  Qed.
 
  Lemma sum5 :
@@ -724,26 +692,26 @@ Module IntProperties (I:Int).
  rewrite gt_lt_iff in H,H0.
  destruct (lt_eq_lt_dec z 0) as [[G|G]|G].
 
- rewrite lt_0_neg' in G.
- generalize (plus_le_lt_compat _ _ _ _ (le_refl (z*y)) H0).
- rewrite H'.
- pattern y at 2; rewrite <-(mult_1_l y), <-mult_plus_distr_r.
- intros.
- rewrite le_lt_int in G.
- rewrite <- opp_plus_distr in G.
- assert (0 < y) by (apply lt_trans with x; auto).
- generalize (mult_le_compat _ _ _ _ G (lt_le_weak _ _ H2) (le_refl 0) (le_refl 0)).
- rewrite mult_0_l, mult_comm, <- opp_mult_distr_r, mult_comm, <-le_0_neg', le_lt_iff.
- intuition.
+ - rewrite lt_0_neg' in G.
+   generalize (plus_le_lt_compat _ _ _ _ (le_refl (z*y)) H0).
+   rewrite H'.
+   rewrite <-(mult_1_l y) at 2. rewrite <-mult_plus_distr_r.
+   intros.
+   rewrite le_lt_int in G.
+   rewrite <- opp_plus_distr in G.
+   assert (0 < y) by (apply lt_trans with x; auto).
+   generalize (mult_le_compat _ _ _ _ G (lt_le_weak _ _ H2) (le_refl 0) (le_refl 0)).
+   rewrite mult_0_l, mult_comm, <- opp_mult_distr_r, mult_comm, <-le_0_neg', le_lt_iff.
+   intuition.
 
- subst; rewrite mult_0_l, plus_0_l in H'; subst.
- apply (lt_not_eq _ _ H); auto.
+ - subst; rewrite mult_0_l, plus_0_l in H'; subst.
+   apply (lt_not_eq _ _ H); auto.
 
- apply (lt_not_eq 0 (z*y+x)); auto.
- rewrite <- (plus_0_l 0).
- apply plus_lt_compat; auto.
- apply mult_lt_0_compat; auto.
- apply lt_trans with x; auto.
+ - apply (lt_not_eq 0 (z*y+x)); auto.
+   rewrite <- (plus_0_l 0).
+   apply plus_lt_compat; auto.
+   apply mult_lt_0_compat; auto.
+   apply lt_trans with x; auto.
  Qed.
 
  Lemma OMEGA19 : forall x, x<>0 -> 0 <= x + -(1) \/ 0 <= x * -(1) + -(1).
@@ -759,32 +727,28 @@ Module IntProperties (I:Int).
  apply opp_lt_compat; auto.
  Qed.
 
- Lemma mult_le_approx :
-  forall n m p, n > 0 -> n > p -> 0 <= m * n + p -> 0 <= m.
+ Lemma pos_ge_1 n : 0 < n -> 1 <= n.
+ Proof.
+ intros. apply plus_le_reg_r with (-(1)). rewrite opp_def.
+ now apply le_lt_int.
+ Qed.
+
+ Lemma mult_le_approx n m p :
+  n > 0 -> n > p -> 0 <= m * n + p -> 0 <= m.
  Proof.
- intros n m p.
  do 2 rewrite gt_lt_iff.
- do 2 rewrite le_lt_iff; intros.
- contradict H1.
- rewrite lt_0_neg' in H1.
+ do 2 rewrite le_lt_iff; intros Hn Hpn H Hm. destruct H.
+ apply lt_0_neg', pos_ge_1 in Hm.
  rewrite lt_0_neg'.
- rewrite opp_plus_distr.
- rewrite mult_comm, opp_mult_distr_r.
+ rewrite opp_plus_distr, mult_comm, opp_mult_distr_r.
  rewrite le_lt_int.
  rewrite <- plus_assoc, (plus_comm (-p)), plus_assoc.
  apply lt_left.
  rewrite le_lt_int.
- rewrite le_lt_int in H0.
- apply le_trans with (n+-(1)); auto.
+ apply le_trans with (n+-(1)); [ now apply le_lt_int | ].
  apply plus_le_compat; [ | apply le_refl ].
- rewrite le_lt_int in H1.
- generalize (mult_le_compat _ _ _ _ (lt_le_weak _ _ H) H1 (le_refl 0) (le_refl 0)).
- rewrite mult_0_l.
- rewrite mult_plus_distr_l.
- rewrite <- opp_eq_mult_neg_1.
- intros.
- generalize (plus_le_compat _ _ _ _ (le_refl n) H2).
- now rewrite plus_permute, opp_def, plus_0_r, plus_0_r.
+ rewrite <- (mult_1_l n) at 1. rewrite mult_comm.
+ apply mult_le_compat_l; auto using lt_le_weak.
  Qed.
 
  (* Some decidabilities *)
@@ -1013,11 +977,9 @@ Inductive e_step : Set :=
 (* \subsection{Efficient decidable equality} *)
 (* For each reified data-type, we define an efficient equality test.
    It is not the one produced by [Decide Equality].
-
-   Then we prove two theorem allowing elimination of such equalities :
+   Then we prove the correctness of this test :
    \begin{verbatim}
-   (t1,t2: typ) (eq_typ t1 t2) = true -> t1 = t2.
-   (t1,t2: typ) (eq_typ t1 t2) = false -> ~ t1 = t2.
+   forall t1 t2 : term; eq_term t1 t2 = true <-> t1 = t2.
    \end{verbatim} *)
 
 (* \subsubsection{Reified terms} *)
@@ -1037,61 +999,19 @@ Fixpoint eq_term (t1 t2 : term) {struct t2} : bool :=
 
 Close Scope romega_scope.
 
-Theorem eq_term_true : forall t1 t2 : term, eq_term t1 t2 = true -> t1 = t2.
-Proof.
- induction t1; destruct t2; simpl in *; try discriminate;
- (rewrite andb_true_iff; intros (H1,H2)) || intros H; f_equal;
- auto using beq_true, beq_nat_true.
-Qed.
-
-Theorem eq_term_refl : forall t0 : term, eq_term t0 t0 = true.
+Theorem eq_term_iff (t t' : term) :
+ eq_term t t' = true <-> t = t'.
 Proof.
- induction t0; simpl in *; try (apply andb_true_iff; split); trivial.
- - now apply beq_iff.
- - now apply beq_nat_true_iff.
+ revert t'. induction t; destruct t'; simpl in *;
+ rewrite ?andb_true_iff, ?beq_iff, ?Nat.eqb_eq, ?IHt, ?IHt1, ?IHt2;
+  intuition congruence.
 Qed.
 
-Ltac trivial_case := unfold not; intros; discriminate.
-
-Theorem eq_term_false :
- forall t1 t2 : term, eq_term t1 t2 = false -> t1 <> t2.
+Theorem eq_term_reflect (t t' : term) : reflect (t=t') (eq_term t t').
 Proof.
- intros t1 t2 H E. subst t2. now rewrite eq_term_refl in H.
+ apply iff_reflect. symmetry. apply eq_term_iff.
 Qed.
 
-(* \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. *)
-
-(* 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. *)
-
-Ltac elim_eq_term t1 t2 :=
-  let Aux := fresh "Aux" in
-  pattern (eq_term t1 t2); apply bool_eq_ind; intro Aux;
-   [ generalize (eq_term_true t1 t2 Aux); clear Aux
-   | generalize (eq_term_false t1 t2 Aux); clear Aux ].
-
-Ltac elim_beq t1 t2 :=
-  let Aux := fresh "Aux" in
-  pattern (beq t1 t2); apply bool_eq_ind; intro Aux;
-   [ generalize (beq_true t1 t2 Aux); clear Aux
-   | generalize (beq_false t1 t2 Aux); clear Aux ].
-
-Ltac elim_bgt t1 t2 :=
-  let Aux := fresh "Aux" in
-  pattern (bgt t1 t2); apply bool_eq_ind; intro Aux;
-  [ generalize (bgt_true t1 t2 Aux); clear Aux
-  | generalize (bgt_false t1 t2 Aux); clear Aux ].
-
-
 (* \subsection{Interprétations}
    \subsubsection{Interprétation des termes dans Z} *)
 
@@ -1162,16 +1082,18 @@ Theorem goal_to_hyps :
  forall (envp : list Prop) (env : list int) (l : hyps),
  (interp_hyps envp env l -> False) -> interp_goal envp env l.
 Proof.
- simple induction l;
- [ simpl; auto
- | simpl; intros a l1 H1 H2 H3; apply H1; intro H4; apply H2; auto ].
+ simple induction l.
+ - simpl; auto.
+ - simpl; intros a l1 H1 H2 H3; apply H1; intro H4; apply H2; auto.
 Qed.
 
 Theorem hyps_to_goal :
  forall (envp : list Prop) (env : list int) (l : hyps),
  interp_goal envp env l -> interp_hyps envp env l -> False.
 Proof.
- simple induction l; simpl; [ auto | intros; apply H; elim H1; auto ].
+ simple induction l; simpl.
+ - auto.
+ - intros; apply H; elim H1; auto.
 Qed.
 
 (* \subsection{Manipulations sur les hypothèses} *)
@@ -1236,21 +1158,22 @@ Theorem list_goal_to_hyps :
  forall (envp : list Prop) (env : list int) (l : lhyps),
  (interp_list_hyps envp env l -> False) -> interp_list_goal envp env l.
 Proof.
- simple 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 ] ].
+ simple 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.
 Qed.
 
 Theorem list_hyps_to_goal :
  forall (envp : list Prop) (env : list int) (l : lhyps),
  interp_list_goal envp env l -> interp_list_hyps envp env l -> False.
 Proof.
- simple induction l; simpl;
- [ auto
- | intros h1 l1 H (H1, H2) H3; elim H3; intro H4;
-    [ apply hyps_to_goal with (1 := H1); assumption | auto ] ].
+ simple induction l; simpl.
+ - auto.
+ - intros h1 l1 H (H1, H2) H3; elim H3; intro H4.
+   + apply hyps_to_goal with (1 := H1); assumption.
+   + auto.
 Qed.
 
 Definition valid_list_hyps (f : hyps -> lhyps) :=
@@ -1274,29 +1197,25 @@ Theorem append_valid :
  interp_list_hyps ep e l1 \/ interp_list_hyps ep e l2 ->
  interp_list_hyps ep e (l1 ++ l2).
 Proof.
- intros ep e; simple 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 ] ].
-
+ induction l1; simpl in *.
+ - now intros l2 [H| H].
+ - intros l2 [[H| H]| H].
+   + auto.
+   + right; apply IHl1; now left.
+   + right; apply IHl1; now right.
 Qed.
 
 (* \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.
-Unset Printing Notations.
+
 Theorem nth_valid :
  forall (ep : list Prop) (e : list int) (i : nat) (l : hyps),
  interp_hyps ep e l -> interp_proposition ep e (nth_hyps i l).
 Proof.
- unfold nth_hyps; simple induction i;
- [ simple induction l; simpl; [ auto | intros; elim H0; auto ]
- | intros n H; simple induction l;
-    [ simpl; trivial
-    | intros; simpl; apply H; elim H1; auto ] ].
+ unfold nth_hyps. induction i; destruct l; simpl in *; try easy.
+ intros (H1,H2). now apply IHi.
 Qed.
 
 (* Appliquer une opération (valide) sur deux hypothèses extraites de
@@ -1310,7 +1229,9 @@ Theorem apply_oper_2_valid :
  valid2 f -> valid_hyps (apply_oper_2 i j f).
 Proof.
  intros i j f Hf; unfold apply_oper_2, valid_hyps; simpl;
- intros lp Hlp; split; [ apply Hf; apply nth_valid; assumption | assumption ].
+ intros lp Hlp; split.
+ - apply Hf; apply nth_valid; assumption.
+ - assumption.
 Qed.
 
 (* Modifier une hypothèse par application d'une opération valide *)
@@ -1330,15 +1251,17 @@ Theorem apply_oper_1_valid :
  forall (i : nat) (f : proposition -> proposition),
  valid1 f -> valid_hyps (apply_oper_1 i f).
 Proof.
- 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 ] ] ].
+ 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.
 Qed.
 
 (* \subsubsection{Manipulations de termes} *)
@@ -1443,49 +1366,26 @@ Ltac loop t :=
   (* Propositions *)
   | (EqTerm ?X1 ?X2) => loop X1 || loop X2
   | (LeqTerm ?X1 ?X2) => loop X1 || loop X2
-  (* Termes *)
+  (* Terms *)
   | (?X1 + ?X2)%term => loop X1 || loop X2
   | (?X1 - ?X2)%term => loop X1 || loop X2
   | (?X1 * ?X2)%term => loop X1 || loop X2
   | (- ?X1)%term => loop X1
   | (Tint ?X1) => loop X1
   (* Eliminations *)
-  | match ?X1 with
-    | EqTerm _ _ => _
-    | LeqTerm _ _ => _
-    | TrueTerm => _
-    | FalseTerm => _
-    | Tnot _ => _
-    | GeqTerm _ _ => _
-    | GtTerm _ _ => _
-    | LtTerm _ _ => _
-    | NeqTerm _ _ => _
-    | Tor _ _ => _
-    | Tand _ _ => _
-    | Timp _ _ => _
-    | Tprop _ => _
-    end => destruct X1; auto; Simplify
-  | match ?X1 with
-    | Tint _ => _
-    | (_ + _)%term => _
-    | (_ * _)%term => _
-    | (_ - _)%term => _
-    | (- _)%term => _
-    | [_]%term => _
-    end => destruct X1; auto; Simplify
   | (if beq ?X1 ?X2 then _ else _) =>
       let H := fresh "H" in
-      elim_beq X1 X2; intro H; try (rewrite H in *; clear H);
-       simpl; auto; Simplify
+      case (beq_reflect X1 X2); intro H;
+      try (rewrite H in *; clear H); simpl; auto; Simplify
   | (if bgt ?X1 ?X2 then _ else _) =>
-      let H := fresh "H" in
-      elim_bgt X1 X2; intro H; simpl; auto; Simplify
+      case (bgt_reflect X1 X2); intro; simpl; auto; Simplify
   | (if eq_term ?X1 ?X2 then _ else _) =>
       let H := fresh "H" in
-      elim_eq_term X1 X2; intro H; try (rewrite H in *; clear H);
-       simpl; auto; Simplify
+      case (eq_term_reflect X1 X2); intro H;
+      try (rewrite H in *; clear H); simpl; auto; Simplify
   | (if _ && _ then _ else _) => rewrite andb_if; Simplify
   | (if negb _ then _ else _) => rewrite negb_if; Simplify
+  | match ?X1 with _ => _ end => destruct X1; auto; Simplify
   | _ => fail
   end
 
@@ -1829,52 +1729,43 @@ Fixpoint reduce (t : term) : term :=
   match t with
   | (x + y)%term =>
       match reduce x with
-      | Tint x' =>
+      | Tint xi as xr =>
           match reduce y with
-          | Tint y' => Tint (x' + y')
-          | y' => (Tint x' + y')%term
+          | Tint yi => Tint (xi + yi)
+          | yr => (xr + yr)%term
           end
-      | x' => (x' + reduce y)%term
+      | xr => (xr + reduce y)%term
       end
   | (x * y)%term =>
       match reduce x with
-      | Tint x' =>
+      | Tint xi as xr =>
           match reduce y with
-          | Tint y' => Tint (x' * y')
-          | y' => (Tint x' * y')%term
+          | Tint yi => Tint (xi * yi)
+          | yr => (xr * yr)%term
           end
-      | x' => (x' * reduce y)%term
+      | xr => (xr * reduce y)%term
       end
   | (x - y)%term =>
       match reduce x with
-      | Tint x' =>
+      | Tint xi as xr =>
           match reduce y with
-          | Tint y' => Tint (x' - y')
-          | y' => (Tint x' - y')%term
+          | Tint yi => Tint (xi - yi)
+          | yr => (xr - yr)%term
           end
-      | x' => (x' - reduce y)%term
+      | xr => (xr - reduce y)%term
       end
   | (- x)%term =>
       match reduce x with
-      | Tint x' => Tint (- x')
-      | x' => (- x')%term
+      | Tint xi => Tint (- xi)
+      | xr => (- xr)%term
       end
   | _ => t
   end.
 
 Theorem reduce_stable : term_stable reduce.
 Proof.
- 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.
+ red. intros e t; induction t; simpl; auto;
+  do 2 destruct reduce; simpl; f_equal; auto.
 Qed.
 
 (* \subsubsection{Fusions}
@@ -1898,17 +1789,20 @@ Fixpoint fusion (trace : list t_fusion) (t : term) {struct trace} : term :=
 
 Theorem fusion_stable : forall trace : list t_fusion, term_stable (fusion trace).
 Proof.
- simple induction trace; 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 ] ] ].
+ simple induction trace; 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.
 Qed.
 
 (* \paragraph{Fusion de deux équations dont une sans coefficient} *)
@@ -1936,9 +1830,9 @@ Fixpoint fusion_cancel (trace : nat) (t : term) {struct trace} : term :=
 
 Theorem fusion_cancel_stable : forall t : nat, term_stable (fusion_cancel t).
 Proof.
- 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) ].
+ 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).
 Qed.
 
 (* \subsubsection{Opérations affines sur une équation} *)
@@ -1953,10 +1847,11 @@ Fixpoint scalar_norm_add (trace : nat) (t : term) {struct trace} : term :=
 Theorem scalar_norm_add_stable :
  forall t : nat, term_stable (scalar_norm_add t).
 Proof.
- 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 ] ].
+ 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.
 Qed.
 
 (* \paragraph{Multiplication scalaire} *)
@@ -1968,10 +1863,11 @@ Fixpoint scalar_norm (trace : nat) (t : term) {struct trace} : term :=
 
 Theorem scalar_norm_stable : forall t : nat, term_stable (scalar_norm t).
 Proof.
- 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 ] ].
+ 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.
 Qed.
 
 (* \paragraph{Somme d'une constante} *)
@@ -1983,10 +1879,11 @@ Fixpoint add_norm (trace : nat) (t : term) {struct trace} : term :=
 
 Theorem add_norm_stable : forall t : nat, term_stable (add_norm t).
 Proof.
- 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 ] ].
+ 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.
 Qed.
 
 (* \subsection{La fonction de normalisation des termes (moteur de réécriture)} *)
@@ -2025,34 +1922,34 @@ Fixpoint t_rewrite (s : step) : term -> term :=
 
 Theorem t_rewrite_stable : forall s : step, term_stable (t_rewrite s).
 Proof.
- simple 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_comm_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_comm_stable ].
+ simple 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_comm_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_comm_stable.
 Qed.
 
 (* \subsection{tactiques de résolution d'un but omega normalisé}
@@ -2085,9 +1982,9 @@ Definition constant_neg (i : nat) (h : hyps) :=
 
 Theorem constant_neg_valid : forall i : nat, valid_hyps (constant_neg i).
 Proof.
- unfold valid_hyps, constant_neg; intros;
- generalize (nth_valid ep e i lp); Simplify; simpl.
- rewrite gt_lt_iff in H0; rewrite le_lt_iff; intuition.
+ unfold valid_hyps, constant_neg. intros.
+ generalize (nth_valid ep e i lp). Simplify; simpl.
+ rewrite gt_lt_iff in *; rewrite le_lt_iff; intuition.
 Qed.
 
 (* \paragraph{[NOT_EXACT_DIVIDE]} *)
@@ -2112,8 +2009,9 @@ Proof.
  generalize (nth_valid ep e i lp); Simplify.
  rewrite (scalar_norm_add_stable t0 e), <-H1.
  do 2 rewrite <- scalar_norm_add_stable; simpl in *; intros.
- absurd (interp_term e body * k1 + k2 = 0);
- [ now apply OMEGA4 | symmetry; auto ].
+ absurd (interp_term e body * k1 + k2 = 0).
+ - now apply OMEGA4.
+ - symmetry; auto.
 Qed.
 
 (* \paragraph{[O_CONTRADICTION]} *)
@@ -2137,19 +2035,19 @@ Definition contradiction (t i j : nat) (l : hyps) :=
 Theorem contradiction_valid :
  forall t i j : nat, valid_hyps (contradiction t i j).
 Proof.
- 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; case (nth_hyps j l);
- auto; intros t3 t4; case t3; auto;
- simpl; intros z z' H1 H2;
- generalize (eq_refl (interp_term e (fusion_cancel t (t2 + t4)%term)));
- pattern (fusion_cancel t (t2 + t4)%term) at 2 3;
- case (fusion_cancel t (t2 + t4)%term); simpl;
- auto; intro k; elim (fusion_cancel_stable t); simpl.
- Simplify; intro H3.
- generalize (OMEGA2 _ _ H2 H1); rewrite H3.
- rewrite gt_lt_iff in H0; rewrite le_lt_iff; intuition.
+ unfold valid_hyps, contradiction; intros t i j ep e l H.
+ generalize (nth_valid _ _ i _ H) (nth_valid _ _ j _ H).
+ case (nth_hyps i l); trivial. intros t1 t2.
+ case t1; trivial. clear t1; intros x1.
+ case (nth_hyps j l); trivial. intros t3 t4.
+ case t3; trivial. clear t3; intros x3.
+ destruct fusion_cancel as [ t0 | | | | | ] eqn:E; trivial.
+ change t0 with (interp_term e (Tint t0)).
+ rewrite <- E, <- fusion_cancel_stable.
+ Simplify.
+ intros H1 H2.
+ generalize (OMEGA2 _ _ H1 H2).
+ rewrite gt_lt_iff in *; rewrite le_lt_iff. intuition.
 Qed.
 
 (* \paragraph{[O_NEGATE_CONTRADICT]} *)
@@ -2202,31 +2100,28 @@ Theorem negate_contradict_valid :
  forall i j : nat, valid_hyps (negate_contradict i j).
 Proof.
  unfold valid_hyps, negate_contradict; intros i j ep e l H;
- generalize (nth_valid _ _ i _ H); generalize (nth_valid _ _ j _ H);
+ generalize (nth_valid _ _ i _ H) (nth_valid _ _ j _ H);
  case (nth_hyps i l); auto; intros t1 t2; case t1;
  auto; intros z; auto; case (nth_hyps j l);
  auto; intros t3 t4; case t3; auto; intros z';
- auto; simpl; intros H1 H2; Simplify.
+ auto; simpl; intros; Simplify.
 Qed.
 
 Theorem negate_contradict_inv_valid :
  forall t i j : nat, valid_hyps (negate_contradict_inv t i j).
 Proof.
  unfold valid_hyps, negate_contradict_inv; intros t i j ep e l H;
- generalize (nth_valid _ _ i _ H); generalize (nth_valid _ _ j _ H);
+ generalize (nth_valid _ _ i _ H) (nth_valid _ _ j _ H);
  case (nth_hyps i l); auto; intros t1 t2; case t1;
  auto; intros z; auto; case (nth_hyps j l);
  auto; intros t3 t4; case t3; auto; intros z';
- auto; simpl; intros H1 H2; Simplify;
- [
- rewrite <- scalar_norm_stable in H2; simpl in *;
- elim (mult_integral (interp_term e t4) (-(1))); intuition;
- elim minus_one_neq_zero; auto
- |
- elim H2; clear H2;
- rewrite <- scalar_norm_stable; simpl in *;
- now rewrite <- H1, mult_0_l
- ].
+ auto; simpl; intros H1 H2; Simplify.
+ - rewrite <- scalar_norm_stable in H1; simpl in *;
+   elim (mult_integral (interp_term e t4) (-(1))); intuition;
+   elim minus_one_neq_zero; auto.
+ - elim H1; clear H1;
+   rewrite <- scalar_norm_stable; simpl in *;
+   now rewrite <- H2, mult_0_l.
 Qed.
 
 (* \subsubsection{Tactiques générant une nouvelle équation} *)
@@ -2286,12 +2181,12 @@ Theorem sum_valid :
 Proof.
  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 plus_comm; apply sum2; try assumption; apply sum4; assumption
- | apply sum3; try assumption; apply sum4; assumption
- | apply sum5; auto ].
+ simpl; intros.
+ - apply sum1; assumption.
+ - apply sum2; try assumption; apply sum4; assumption.
+ - rewrite plus_comm; apply sum2; try assumption; apply sum4; assumption.
+ - apply sum3; try assumption; apply sum4; assumption.
+ - apply sum5; auto.
 Qed.
 
 (* \paragraph{[O_EXACT_DIVIDE]}
@@ -2320,10 +2215,9 @@ Theorem exact_divide_valid :
 Proof.
  unfold valid1, exact_divide; intros k1 k2 t ep e p1;
  Simplify; simpl; auto; subst;
- rewrite <- scalar_norm_stable; simpl; intros;
- [ destruct (mult_integral _ _ (eq_sym H0)); intuition
- | contradict H0; rewrite <- H0, mult_0_l; auto
- ].
+ rewrite <- scalar_norm_stable; simpl; intros.
+ - destruct (mult_integral _ _ (eq_sym H0)); intuition.
+ - contradict H0; rewrite <- H0, mult_0_l; auto.
 Qed.
 
 
@@ -2348,9 +2242,9 @@ Theorem divide_and_approx_valid :
  forall (k1 k2 : int) (body : term) (t : nat),
  valid1 (divide_and_approx k1 k2 body t).
 Proof.
- unfold valid1, divide_and_approx; intros k1 k2 body t ep e p1;
- Simplify; simpl; auto; subst;
- elim (scalar_norm_add_stable t e); simpl.
+ unfold valid1, divide_and_approx.
+ intros k1 k2 body t ep e p1. Simplify. subst.
+ elim (scalar_norm_add_stable t e). simpl.
  intro H2; apply mult_le_approx with (3 := H2); assumption.
 Qed.
 
@@ -2374,8 +2268,9 @@ Theorem merge_eq_valid : forall n : nat, valid2 (merge_eq n).
 Proof.
  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 opp_eq_mult_neg_1; trivial ].
+ intros; symmetry ; apply OMEGA8 with (2 := H0).
+ - assumption.
+ - elim opp_eq_mult_neg_1; trivial.
 Qed.
 
 
@@ -2392,8 +2287,7 @@ Definition constant_nul (i : nat) (h : hyps) :=
 Theorem constant_nul_valid : forall i : nat, valid_hyps (constant_nul i).
 Proof.
  unfold valid_hyps, constant_nul; intros;
- generalize (nth_valid ep e i lp); Simplify; simpl;
- intro H1; absurd (0 = 0); intuition.
+ generalize (nth_valid ep e i lp); Simplify; simpl; intuition.
 Qed.
 
 (* \paragraph{[O_STATE]} *)
@@ -2446,13 +2340,13 @@ Proof.
  simpl; auto; intros t1 t2; case t1; simpl;
  auto; intros z; simpl; auto; intro H3.
  Simplify.
- 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 not; intros E1 E2; apply E1;
-    symmetry ; trivial ].
+ 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 not; intros E1 E2; apply E1;
+    symmetry ; trivial.
 Qed.
 
 
@@ -2485,49 +2379,49 @@ Fixpoint execute_omega (t : t_omega) (l : hyps) {struct t} : lhyps :=
 
 Theorem omega_valid : forall tr : t_omega, valid_list_hyps (execute_omega tr).
 Proof.
- simple induction tr; 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;
+ simple induction tr; 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 _ _ _ _ _ ep e lp H)
- | unfold valid_list_hyps, valid_hyps;
+        (divide_and_approx_valid k1 k2 body n) ep e lp H).
+ - unfold valid_list_hyps; simpl; intros; left;
+    apply (not_exact_divide_valid _ _ _ _ _ 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;
+        (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;
+        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;
+        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;
+        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) ].
+    apply (apply_oper_2_valid i1 i2 (state m s) (state_valid m s) ep e lp H).
 Qed.
 
 
@@ -2548,13 +2442,13 @@ Definition move_right (s : step) (p : proposition) :=
 Theorem move_right_valid : forall s : step, valid1 (move_right s).
 Proof.
  unfold valid1, move_right; intros s ep e p; Simplify; simpl;
- elim (t_rewrite_stable s e); simpl;
- [ symmetry ; apply egal_left; assumption
- | intro; apply le_left; assumption
- | intro; apply le_left; rewrite <- ge_le_iff; assumption
- | intro; apply lt_left; rewrite <- gt_lt_iff; assumption
- | intro; apply lt_left; assumption
- | intro; apply ne_left_2; assumption ].
+ elim (t_rewrite_stable s e); simpl.
+ - symmetry ; apply egal_left; assumption.
+ - intro; apply le_left; assumption.
+ - intro; apply le_left; rewrite <- ge_le_iff; assumption.
+ - intro; apply lt_left; rewrite <- gt_lt_iff; assumption.
+ - intro; apply lt_left; assumption.
+ - intro; apply ne_left_2; assumption.
 Qed.
 
 Definition do_normalize (i : nat) (s : step) := apply_oper_1 i (move_right s).
@@ -2576,10 +2470,10 @@ Fixpoint do_normalize_list (l : list step) (i : nat)
 Theorem do_normalize_list_valid :
  forall (l : list step) (i : nat), valid_hyps (do_normalize_list l i).
 Proof.
- simple 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 ].
+ simple 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.
 Qed.
 
 Theorem normalize_goal :
@@ -2604,9 +2498,9 @@ Theorem append_goal :
  interp_list_goal ep e l1 /\ interp_list_goal ep e l2 ->
  interp_list_goal ep e (l1 ++ l2).
 Proof.
- intros ep e; simple induction l1;
- [ simpl; intros l2 (H1, H2); assumption
- | simpl; intros h1 t1 HR l2 ((H1, H2), H3); split; auto ].
+ intros ep e; induction l1; simpl.
+ - intros l2 (H1, H2); assumption.
+ - intros l2 ((H1, H2), H3); split; auto.
 Qed.
 
 (* A simple decidability checker : if the proposition belongs to the
@@ -2635,20 +2529,20 @@ Theorem decidable_correct :
  forall (ep : list Prop) (e : list int) (p : proposition),
  decidability p = true -> decidable (interp_proposition ep e p).
 Proof.
- simple induction p; simpl; intros;
- [ apply dec_eq
- | apply dec_le
- | left; auto
- | right; unfold not; auto
- | apply dec_not; auto
- | apply dec_ge
- | apply dec_gt
- | apply dec_lt
- | apply dec_ne
- | 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 ].
+ simple induction p; simpl; intros.
+ - apply dec_eq.
+ - apply dec_le.
+ - left; auto.
+ - right; unfold not; auto.
+ - apply dec_not; auto.
+ - apply dec_ge.
+ - apply dec_gt.
+ - apply dec_lt.
+ - apply dec_ne.
+ - 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.
 Qed.
 
 (* An interpretation function for a complete goal with an explicit
@@ -2675,8 +2569,9 @@ Theorem interp_full_false :
  forall (ep : list Prop) (e : list int) (l : hyps) (c : proposition),
  (interp_hyps ep e l -> interp_proposition ep e c) -> interp_full ep e (l, c).
 Proof.
- simple induction l; unfold interp_full; simpl;
- [ auto | intros a l1 H1 c H2 H3; apply H1; auto ].
+ simple induction l; unfold interp_full; simpl.
+ - auto.
+ - intros a l1 H1 c H2 H3; apply H1; auto.
 Qed.
 
 (* Push the conclusion in the list of hypothesis using a double negation
@@ -2695,15 +2590,13 @@ Theorem to_contradict_valid :
  forall (ep : list Prop) (e : list int) (lc : hyps * proposition),
  interp_goal ep e (to_contradict lc) -> interp_full ep e lc.
 Proof.
- intros ep e lc; case lc; intros l c; simpl;
- pattern (decidability c); apply bool_eq_ind;
- [ simpl; intros H H1; apply interp_full_false; intros H2;
-    apply not_not;
-    [ apply decidable_correct; assumption
-    | unfold not at 1; 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 ].
+ intros ep e (l,c); simpl.
+ destruct decidability eqn:H; simpl;
+  intros H1; apply interp_full_false; intros H2.
+ - apply not_not.
+    + now apply decidable_correct.
+    + intro; apply hyps_to_goal with (2 := H2); auto.
+ - now elim hyps_to_goal with (1 := H1).
 Qed.
 
 (* [map_cons x l] adds [x] at the head of each list in [l] (which is a list
@@ -2764,7 +2657,7 @@ Theorem map_cons_val :
  interp_proposition ep e p ->
  interp_list_hyps ep e l -> interp_list_hyps ep e (map_cons _ p l).
 Proof.
- simple induction l; simpl; [ auto | intros; elim H1; intro H2; auto ].
+ induction l; simpl; intuition.
 Qed.
 
 Hint Resolve map_cons_val append_valid decidable_correct.
@@ -2772,46 +2665,38 @@ Hint Resolve map_cons_val append_valid decidable_correct.
 Theorem destructure_hyps_valid :
  forall n : nat, valid_list_hyps (destructure_hyps n).
 Proof.
- simple induction n;
- [ unfold valid_list_hyps; simpl; auto
- | unfold valid_list_hyps at 2; intros n1 H ep e lp; case lp;
-    [ simpl; auto
-    | intros p l; case p;
+ simple induction n.
+ - unfold valid_list_hyps; simpl; auto.
+ - unfold valid_list_hyps at 2; 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';
+          auto).
+       * intro p'; case p'; simpl;
           try
            (simpl; intros; apply map_cons_val; simpl; elim H0;
-             auto);
-          [ simpl; intros p1 (H1, H2);
-             pattern (decidability p1); apply bool_eq_ind;
-             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_eq_ind;
-             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;
+             auto).
+          { simpl; intros p1 (H1, H2).
+            destruct decidability eqn:H3; auto.
+            apply H; simpl; split; auto.
+            apply not_not; auto. }
+          { simpl; intros p1 p2 (H1, H2); apply H; simpl;
+             elim not_or with (1 := H1); auto. }
+          { simpl; intros p1 p2 (H1, H2).
+            destruct decidability eqn:H3; auto.
+            apply append_valid; elim not_and with (2 := H1); auto.
+            - intro; left; apply H; simpl; auto.
+            - intro; right; apply H; simpl; 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_eq_ind;
-          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 ] ] ] ].
+          apply H; simpl; auto.
+       * simpl; intros; apply H; simpl; tauto.
+       * simpl; intros p1 p2 (H1, H2).
+         destruct decidability eqn:H3; auto.
+         apply append_valid; elim imp_simp with (2 := H1); auto.
+         { intro; left; simpl; apply H; simpl; auto. }
+         { intro; right; simpl; apply H; simpl; auto. }
 Qed.
 
 Definition prop_stable (f : proposition -> proposition) :=
@@ -2850,12 +2735,12 @@ Theorem p_apply_right_stable :
  forall f : proposition -> proposition,
  prop_stable f -> prop_stable (p_apply_right f).
 Proof.
- 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 ]).
+ unfold prop_stable; intros f H ep e p.
+ case p; simpl; try tauto.
+ - intros p1; rewrite (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.
 Qed.
 
 Definition p_invert (f : proposition -> proposition)
@@ -2874,54 +2759,44 @@ Theorem p_invert_stable :
  forall f : proposition -> proposition,
  prop_stable f -> prop_stable (p_invert f).
 Proof.
- 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;
-      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;
-      generalize (dec_gt (interp_term e t1) (interp_term e t2));
-      unfold decidable; rewrite le_lt_iff, <- gt_lt_iff; tauto
-   | intros t1 t2; elim (H ep e (LtTerm t1 t2)); simpl;
-      generalize (dec_lt (interp_term e t1) (interp_term e t2));
-      unfold decidable; rewrite ge_le_iff, le_lt_iff; tauto
-   | intros t1 t2; elim (H ep e (LeqTerm t1 t2)); simpl;
-      generalize (dec_gt (interp_term e t1) (interp_term e t2));
-      unfold decidable; repeat rewrite le_lt_iff;
-      repeat rewrite gt_lt_iff; tauto
-   | intros t1 t2; elim (H ep e (GeqTerm t1 t2)); simpl;
-      generalize (dec_lt (interp_term e t1) (interp_term e t2));
-      unfold decidable; repeat rewrite ge_le_iff;
-      repeat rewrite le_lt_iff; 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; tauto ]).
+ unfold prop_stable; intros f H ep e p.
+ case p; simpl; try tauto; intros t1 t2; rewrite <- (H ep e); simpl.
+ - generalize (dec_eq (interp_term e t1) (interp_term e t2));
+   unfold decidable; try tauto.
+ - generalize (dec_gt (interp_term e t1) (interp_term e t2));
+   unfold decidable; rewrite le_lt_iff, <- gt_lt_iff; tauto.
+ - generalize (dec_lt (interp_term e t1) (interp_term e t2));
+   unfold decidable; rewrite ge_le_iff, le_lt_iff; tauto.
+ - generalize (dec_gt (interp_term e t1) (interp_term e t2));
+   unfold decidable; rewrite ?le_lt_iff, ?gt_lt_iff; tauto.
+ - generalize (dec_lt (interp_term e t1) (interp_term e t2));
+   unfold decidable; rewrite ?ge_le_iff, ?le_lt_iff; tauto.
+ - reflexivity.
 Qed.
 
 Theorem move_right_stable : forall s : step, prop_stable (move_right s).
 Proof.
- unfold move_right, prop_stable; intros s ep e p; split;
- [ Simplify; simpl; elim (t_rewrite_stable s e); simpl;
-    [ symmetry ; apply egal_left; assumption
-    | intro; apply le_left; assumption
-    | intro; apply le_left; rewrite <- ge_le_iff; assumption
-    | intro; apply lt_left; rewrite <- gt_lt_iff; assumption
-    | intro; apply lt_left; assumption
-    | intro; apply ne_left_2; assumption ]
- | case p; simpl; intros; auto; generalize H; elim (t_rewrite_stable s);
-    simpl; intro H1;
-    [ rewrite (plus_0_r_reverse (interp_term e t1)); rewrite H1;
-       rewrite plus_permute; rewrite plus_opp_r;
-       rewrite plus_0_r; trivial
-    | apply (fun a b => plus_le_reg_r a b (- interp_term e t0));
-       rewrite plus_opp_r; assumption
-    | rewrite ge_le_iff;
-       apply (fun a b => plus_le_reg_r a b (- interp_term e t1));
-       rewrite plus_opp_r; assumption
-    | rewrite gt_lt_iff; apply lt_left_inv; assumption
-    | apply lt_left_inv; assumption
-    | unfold not; intro H2; apply H1;
-       rewrite H2; rewrite plus_opp_r; trivial ] ].
+ unfold move_right, prop_stable; intros s ep e p; split.
+ - Simplify; simpl; elim (t_rewrite_stable s e); simpl.
+    + symmetry ; apply egal_left; assumption.
+    + intro; apply le_left; assumption.
+    + intro; apply le_left; rewrite <- ge_le_iff; assumption.
+    + intro; apply lt_left; rewrite <- gt_lt_iff; assumption.
+    + intro; apply lt_left; assumption.
+    + intro; apply ne_left_2; assumption.
+ - case p; simpl; intros; auto; generalize H; elim (t_rewrite_stable s);
+   simpl; intro H1.
+   + rewrite (plus_0_r_reverse (interp_term e t1)); rewrite H1;
+     now rewrite plus_permute, plus_opp_r, plus_0_r.
+   + apply (fun a b => plus_le_reg_r a b (- interp_term e t0));
+     rewrite plus_opp_r; assumption.
+   + rewrite ge_le_iff;
+     apply (fun a b => plus_le_reg_r a b (- interp_term e t1));
+     rewrite plus_opp_r; assumption.
+   + rewrite gt_lt_iff; apply lt_left_inv; assumption.
+   + apply lt_left_inv; assumption.
+   + unfold not; intro H2; apply H1;
+     rewrite H2, plus_opp_r; trivial.
 Qed.
 
 
@@ -2936,12 +2811,12 @@ Fixpoint p_rewrite (s : p_step) : proposition -> proposition :=
 
 Theorem p_rewrite_stable : forall s : p_step, prop_stable (p_rewrite s).
 Proof.
- simple 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 ].
+ simple 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.
 Qed.
 
 Fixpoint normalize_hyps (l : list h_step) (lh : hyps) {struct l} : hyps :=
@@ -2953,13 +2828,13 @@ Fixpoint normalize_hyps (l : list h_step) (lh : hyps) {struct l} : hyps :=
 Theorem normalize_hyps_valid :
  forall l : list h_step, valid_hyps (normalize_hyps l).
 Proof.
- simple 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 ] ].
+ simple 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.
 Qed.
 
 Theorem normalize_hyps_goal :
@@ -3024,23 +2899,22 @@ Theorem extract_valid :
  forall s : list direction,
  valid1 (extract_hyp_pos s) /\ co_valid1 (extract_hyp_neg s).
 Proof.
- unfold valid1, co_valid1; simple induction s;
- [ split;
-    [ simpl; auto
-    | intros ep e p1; case p1; simpl; auto; intro p;
-       pattern (decidability p); apply bool_eq_ind;
-       [ 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;
+ unfold valid1, co_valid1; simple induction s.
+ - split.
+   + simpl; auto.
+   + intros ep e p1; case p1; simpl; auto; intro p.
+     destruct decidability eqn: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) ||
       (apply H2; tauto) ||
-        (pattern (decidability p0); apply bool_eq_ind;
-          [ intro H3; generalize (decidable_correct ep e p0 H3);
-             unfold decidable; intro H4; apply H1;
-             tauto
-          | intro; tauto ]) ].
+        (destruct decidability eqn:H3; try tauto;
+         generalize (decidable_correct ep e p0 H3);
+         unfold decidable; intro H4; apply H1;
+         tauto).
 Qed.
 
 Fixpoint decompose_solve (s : e_step) (h : hyps) {struct s} : lhyps :=
@@ -3069,31 +2943,32 @@ Theorem decompose_solve_valid :
  forall s : e_step, valid_list_goal (decompose_solve s).
 Proof.
  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_eq_ind;
-          [ 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 ]
-       | intros p1 p2 H2;
-         pattern (decidability p1); apply bool_eq_ind;
-          [ 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 ] ]
-    | 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) ].
+ 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.
+          destruct decidability eqn: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. }
+       * intros p1 p2 H2;
+         destruct decidability eqn: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. }
+    + elim (extract_valid l); intros H2 H3.
+      apply H2, nth_valid; auto.
+ - intros; apply H; simpl; split; auto.
+   elim (extract_valid l); intros H2 H3.
+   apply H2; apply nth_valid; auto.
+ - apply omega_valid with (1 := H).
 Qed.
 
 (* \subsection{La dernière étape qui élimine tous les séquents inutiles} *)
@@ -3111,11 +2986,11 @@ Fixpoint reduce_lhyps (lp : lhyps) : lhyps :=
 
 Theorem reduce_lhyps_valid : valid_lhyps reduce_lhyps.
 Proof.
- 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 ] ].
+ 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; tauto.
 Qed.
 
 Theorem do_reduce_lhyps :
@@ -3135,13 +3010,13 @@ Definition do_concl_to_hyp :
   interp_goal envp env (concl_to_hyp c :: l) ->
   interp_goal_concl c envp env l.
 Proof.
- simpl; intros envp env c l; induction l as [| a l Hrecl];
- [ simpl; unfold concl_to_hyp;
-    pattern (decidability c); apply bool_eq_ind;
-    [ intro H; generalize (decidable_correct envp env c H);
-       unfold decidable; simpl; tauto
-    | simpl; intros H1 H2; elim H2; trivial ]
- | simpl; tauto ].
+ simpl; intros envp env c l; induction l as [| a l Hrecl].
+ - simpl; unfold concl_to_hyp;
+    destruct decidability eqn:H.
+    + generalize (decidable_correct envp env c H);
+      unfold decidable; simpl; tauto.
+    + simpl; intros H2; elim H2; trivial.
+ - simpl; tauto.
 Qed.
 
 Definition omega_tactic (t1 : e_step) (t2 : list h_step)