diff options
Diffstat (limited to 'plugins/romega')
| -rw-r--r-- | plugins/romega/ReflOmegaCore.v | 505 |
1 files changed, 241 insertions, 264 deletions
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index 56ae921e..11d9a071 100644 --- a/plugins/romega/ReflOmegaCore.v +++ b/plugins/romega/ReflOmegaCore.v @@ -86,73 +86,50 @@ Module Z_as_Int <: Int. Definition int := Z. Definition zero := 0. Definition one := 1. - Definition plus := Zplus. - Definition opp := Zopp. - Definition minus := Zminus. - Definition mult := Zmult. + Definition plus := Z.add. + Definition opp := Z.opp. + Definition minus := Z.sub. + Definition mult := Z.mul. Lemma ring : @ring_theory int zero one plus mult minus opp (@eq int). Proof. constructor. - exact Zplus_0_l. - exact Zplus_comm. - exact Zplus_assoc. - exact Zmult_1_l. - exact Zmult_comm. - exact Zmult_assoc. - exact Zmult_plus_distr_l. - unfold minus, Zminus; auto. - exact Zplus_opp_r. + exact Z.add_0_l. + exact Z.add_comm. + exact Z.add_assoc. + exact Z.mul_1_l. + exact Z.mul_comm. + exact Z.mul_assoc. + exact Z.mul_add_distr_r. + unfold minus, Z.sub; auto. + exact Z.add_opp_diag_r. Qed. - Definition le := Zle. - Definition lt := Zlt. - Definition ge := Zge. - Definition gt := Zgt. - Lemma le_lt_iff : forall i j, (i<=j) <-> ~(j<i). - Proof. - split; intros. - apply Zle_not_lt; auto. - rewrite <- Zge_iff_le. - apply Znot_lt_ge; auto. - Qed. - Definition ge_le_iff := Zge_iff_le. - Definition gt_lt_iff := Zgt_iff_lt. + Definition le := Z.le. + Definition lt := Z.lt. + Definition ge := Z.ge. + Definition gt := Z.gt. + Definition le_lt_iff := Z.le_ngt. + Definition ge_le_iff := Z.ge_le_iff. + Definition gt_lt_iff := Z.gt_lt_iff. - Definition lt_trans := Zlt_trans. - Definition lt_not_eq := Zlt_not_eq. + Definition lt_trans := Z.lt_trans. + Definition lt_not_eq := Z.lt_neq. - Definition lt_0_1 := Zlt_0_1. - Definition plus_le_compat := Zplus_le_compat. + Definition lt_0_1 := Z.lt_0_1. + Definition plus_le_compat := Z.add_le_mono. Definition mult_lt_compat_l := Zmult_lt_compat_l. - Lemma opp_le_compat : forall i j, i<=j -> (-j)<=(-i). - Proof. - unfold Zle; intros; rewrite <- Zcompare_opp; auto. - Qed. + Lemma opp_le_compat i j : i<=j -> (-j)<=(-i). + Proof. apply -> Z.opp_le_mono. Qed. - Definition compare := Zcompare. - Definition compare_Eq := Zcompare_Eq_iff_eq. - Lemma compare_Lt : forall i j, compare i j = Lt <-> i<j. - Proof. intros; unfold compare, Zlt; intuition. Qed. - Lemma compare_Gt : forall i j, compare i j = Gt <-> i>j. - Proof. intros; unfold compare, Zgt; intuition. Qed. + Definition compare := Z.compare. + Definition compare_Eq := Z.compare_eq_iff. + Lemma compare_Lt i j : compare i j = Lt <-> i<j. + Proof. reflexivity. Qed. + Lemma compare_Gt i j : compare i j = Gt <-> i>j. + Proof. reflexivity. Qed. - Lemma le_lt_int : forall x y, x<y <-> x<=y+-(1). - Proof. - intros; split; intros. - generalize (Zlt_left _ _ H); simpl; intros. - apply Zle_left_rev; auto. - apply Zlt_0_minus_lt. - generalize (Zplus_le_lt_compat x (y+-1) (-x) (-x+1) H). - rewrite Zplus_opp_r. - rewrite <-Zplus_assoc. - rewrite (Zplus_permute (-1)). - simpl in *. - rewrite Zplus_0_r. - intro H'; apply H'. - replace (-x+1) with (Zsucc (-x)); auto. - apply Zlt_succ. - Qed. + Definition le_lt_int := Z.lt_le_pred. End Z_as_Int. @@ -363,7 +340,7 @@ Module IntProperties (I:Int). Lemma sum1 : forall a b c d : int, 0 = a -> 0 = b -> 0 = a * c + b * d. Proof. - intros; elim H; elim H0; simpl in |- *; auto. + intros; elim H; elim H0; simpl; auto. now rewrite mult_0_l, mult_0_l, plus_0_l. Qed. @@ -1076,34 +1053,34 @@ Proof. | intros; elim beq_nat_true with (1 := H); trivial ]. Qed. -Ltac trivial_case := unfold not in |- *; intros; discriminate. +Ltac trivial_case := unfold not; intros; discriminate. Theorem eq_term_false : forall t1 t2 : term, eq_term t1 t2 = false -> t1 <> t2. Proof. simple induction t1; - [ intros z t2; case t2; try trivial_case; simpl in |- *; unfold not in |- *; + [ intros z t2; case t2; try trivial_case; simpl; unfold not; intros; elim beq_false with (1 := H); simplify_eq H0; auto - | intros t11 H1 t12 H2 t2; case t2; try trivial_case; simpl in |- *; - intros t21 t22 H3; unfold not in |- *; intro H4; + | 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 in |- *; - intros t21 t22 H3; unfold not in |- *; intro H4; + | 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 in |- *; - intros t21 t22 H3; unfold not in |- *; intro H4; + | 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 in |- *; intros t21 H3; - unfold not in |- *; intro H4; elim H1 with (1 := H3); + | 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 in |- *; unfold not in |- *; + | intros n t2; case t2; try trivial_case; simpl; unfold not; intros; elim beq_nat_false with (1 := H); simplify_eq H0; auto ]. Qed. @@ -1123,17 +1100,17 @@ Qed. avait utilisé le test précédent et fait une elimination dessus. *) Ltac elim_eq_term t1 t2 := - pattern (eq_term t1 t2) in |- *; apply bool_eq_ind; intro Aux; + 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 := - pattern (beq t1 t2) in |- *; apply bool_eq_ind; intro Aux; + 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 := - pattern (bgt t1 t2) in |- *; apply bool_eq_ind; intro Aux; + 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 ]. @@ -1209,15 +1186,15 @@ Theorem goal_to_hyps : (interp_hyps envp env l -> False) -> interp_goal envp env l. Proof. simple induction l; - [ simpl in |- *; auto - | simpl in |- *; intros a l1 H1 H2 H3; apply H1; intro H4; apply H2; auto ]. + [ 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 in |- *; [ 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} *) @@ -1257,7 +1234,7 @@ Theorem valid_goal : forall (ep : list Prop) (env : list int) (l : hyps) (a : hyps -> hyps), valid_hyps a -> interp_goal ep env (a l) -> interp_goal ep env l. Proof. - intros; simpl in |- *; apply goal_to_hyps; intro H1; + intros; simpl; apply goal_to_hyps; intro H1; apply (hyps_to_goal ep env (a l) H0); apply H; assumption. Qed. @@ -1282,7 +1259,7 @@ 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 in |- *; + simple induction l; simpl; [ auto | intros h1 l1 H H1; split; [ apply goal_to_hyps; intro H2; apply H1; auto @@ -1293,7 +1270,7 @@ 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 in |- *; + 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 ] ]. @@ -1310,7 +1287,7 @@ Definition valid_list_goal (f : hyps -> lhyps) := Theorem goal_valid : forall f : hyps -> lhyps, valid_list_hyps f -> valid_list_goal f. Proof. - unfold valid_list_goal in |- *; intros f H ep e lp H1; apply goal_to_hyps; + 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. Qed. @@ -1321,8 +1298,8 @@ Theorem append_valid : interp_list_hyps ep e (l1 ++ l2). Proof. intros ep e; simple induction l1; - [ simpl in |- *; intros l2 [H| H]; [ contradiction | trivial ] - | simpl in |- *; intros h1 t1 HR l2 [[H| H]| H]; + [ 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 ] ]. @@ -1338,11 +1315,11 @@ 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 in |- *; simple induction i; - [ simple induction l; simpl in |- *; [ auto | intros; elim H0; auto ] + unfold nth_hyps; simple induction i; + [ simple induction l; simpl; [ auto | intros; elim H0; auto ] | intros n H; simple induction l; - [ simpl in |- *; trivial - | intros; simpl in |- *; apply H; elim H1; auto ] ]. + [ simpl; trivial + | intros; simpl; apply H; elim H1; auto ] ]. Qed. (* Appliquer une opération (valide) sur deux hypothèses extraites de @@ -1355,7 +1332,7 @@ Theorem apply_oper_2_valid : forall (i j : nat) (f : proposition -> proposition -> proposition), valid2 f -> valid_hyps (apply_oper_2 i j f). Proof. - intros i j f Hf; unfold apply_oper_2, valid_hyps in |- *; simpl in |- *; + intros i j f Hf; unfold apply_oper_2, valid_hyps; simpl; intros lp Hlp; split; [ apply Hf; apply nth_valid; assumption | assumption ]. Qed. @@ -1376,14 +1353,14 @@ Theorem apply_oper_1_valid : forall (i : nat) (f : proposition -> proposition), valid1 f -> valid_hyps (apply_oper_1 i f). Proof. - unfold valid_hyps in |- *; intros i f Hf ep e; elim i; + unfold valid_hyps; intros i f Hf ep e; elim i; [ intro lp; case lp; - [ simpl in |- *; trivial - | simpl in |- *; intros p l' (H1, H2); split; + [ simpl; trivial + | simpl; intros p l' (H1, H2); split; [ apply Hf with (1 := H1) | assumption ] ] | intros n Hrec lp; case lp; - [ simpl in |- *; auto - | simpl in |- *; intros p l' (H1, H2); split; + [ simpl; auto + | simpl; intros p l' (H1, H2); split; [ assumption | apply Hrec; assumption ] ] ]. Qed. @@ -1421,14 +1398,14 @@ Definition apply_both (f g : term -> term) (t : term) := Theorem apply_left_stable : forall f : term -> term, term_stable f -> term_stable (apply_left f). Proof. - unfold term_stable in |- *; intros f H e t; case t; auto; simpl in |- *; + unfold term_stable; intros f H e t; case t; auto; simpl; intros; elim H; trivial. Qed. Theorem apply_right_stable : forall f : term -> term, term_stable f -> term_stable (apply_right f). Proof. - unfold term_stable in |- *; intros f H e t; case t; auto; simpl in |- *; + unfold term_stable; intros f H e t; case t; auto; simpl; intros t0 t1; elim H; trivial. Qed. @@ -1436,7 +1413,7 @@ Theorem apply_both_stable : forall f g : term -> term, term_stable f -> term_stable g -> term_stable (apply_both f g). Proof. - unfold term_stable in |- *; intros f g H1 H2 e t; case t; auto; simpl in |- *; + unfold term_stable; intros f g H1 H2 e t; case t; auto; simpl; intros t0 t1; elim H1; elim H2; trivial. Qed. @@ -1444,7 +1421,7 @@ Theorem compose_term_stable : forall f g : term -> term, term_stable f -> term_stable g -> term_stable (fun t : term => f (g t)). Proof. - unfold term_stable in |- *; intros f g Hf Hg e t; elim Hf; apply Hg. + unfold term_stable; intros f g Hf Hg e t; elim Hf; apply Hg. Qed. (* \subsection{Les règles de réécriture} *) @@ -1522,14 +1499,14 @@ Ltac loop t := | (if beq ?X1 ?X2 then _ else _) => let H := fresh "H" in elim_beq X1 X2; intro H; try (rewrite H in *; clear H); - simpl in |- *; auto; Simplify + simpl; auto; Simplify | (if bgt ?X1 ?X2 then _ else _) => let H := fresh "H" in - elim_bgt X1 X2; intro H; simpl in |- *; auto; Simplify + elim_bgt X1 X2; intro H; 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 in |- *; auto; Simplify + simpl; auto; Simplify | (if _ && _ then _ else _) => rewrite andb_if; Simplify | (if negb _ then _ else _) => rewrite negb_if; Simplify | _ => fail @@ -1543,7 +1520,7 @@ with Simplify := match goal with Ltac prove_stable x th := match constr:x with | ?X1 => - unfold term_stable, X1 in |- *; intros; Simplify; simpl in |- *; + unfold term_stable, X1; intros; Simplify; simpl; apply th end. @@ -1663,7 +1640,7 @@ Definition T_OMEGA13 (t : term) := Theorem T_OMEGA13_stable : term_stable T_OMEGA13. Proof. - unfold term_stable, T_OMEGA13 in |- *; intros; Simplify; simpl in |- *; + unfold term_stable, T_OMEGA13; intros; Simplify; simpl; apply OMEGA13. Qed. @@ -1910,16 +1887,16 @@ Fixpoint reduce (t : term) : term := Theorem reduce_stable : term_stable reduce. Proof. - unfold term_stable in |- *; intros e t; elim t; auto; + unfold term_stable; intros e t; elim t; auto; try - (intros t0 H0 t1 H1; simpl in |- *; rewrite H0; rewrite H1; + (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 in |- *; + | intros; auto ])); intros t0 H0; simpl; rewrite H0; case (reduce t0); intros; auto. Qed. @@ -1944,12 +1921,12 @@ Fixpoint fusion (trace : list t_fusion) (t : term) {struct trace} : term := Theorem fusion_stable : forall t : list t_fusion, term_stable (fusion t). Proof. - simple induction t; simpl in |- *; + simple 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 in |- *; intros e t1; rewrite 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 ] @@ -1982,7 +1959,7 @@ 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 in |- *; intros trace e; elim trace; + 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. @@ -1999,7 +1976,7 @@ 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 in |- *; intros trace; elim trace; + 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 ] ]. @@ -2014,7 +1991,7 @@ 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 in |- *; intros trace; elim trace; + 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 ] ]. @@ -2029,7 +2006,7 @@ 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 in |- *; intros trace; elim trace; + 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 ] ]. @@ -2071,12 +2048,12 @@ Fixpoint t_rewrite (s : step) : term -> term := Theorem t_rewrite_stable : forall s : step, term_stable (t_rewrite s). Proof. - simple induction s; simpl in |- *; + 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 in |- *; intros; elim H0; apply H - | unfold term_stable in |- *; 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 @@ -2116,11 +2093,11 @@ Definition constant_not_nul (i : nat) (h : hyps) := Theorem constant_not_nul_valid : forall i : nat, valid_hyps (constant_not_nul i). Proof. - unfold valid_hyps, constant_not_nul in |- *; intros; - generalize (nth_valid ep e i lp); Simplify; simpl in |- *. + unfold valid_hyps, constant_not_nul; intros; + generalize (nth_valid ep e i lp); Simplify; simpl. - elim_beq i1 i0; auto; simpl in |- *; intros H1 H2; - elim H1; symmetry in |- *; auto. + elim_beq i1 i0; auto; simpl; intros H1 H2; + elim H1; symmetry ; auto. Qed. (* \paragraph{[O_CONSTANT_NEG]} *) @@ -2134,8 +2111,8 @@ 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 in |- *; intros; - generalize (nth_valid ep e i lp); Simplify; simpl in |- *. + 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. Qed. @@ -2157,7 +2134,7 @@ Theorem not_exact_divide_valid : forall (k1 k2 : int) (body : term) (t i : nat), valid_hyps (not_exact_divide k1 k2 body t i). Proof. - unfold valid_hyps, not_exact_divide in |- *; intros; + unfold valid_hyps, not_exact_divide; intros; generalize (nth_valid ep e i lp); Simplify. rewrite (scalar_norm_add_stable t e), <-H1. do 2 rewrite <- scalar_norm_add_stable; simpl in *; intros. @@ -2186,16 +2163,16 @@ 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 in |- *; intros t i j ep e l H; + 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 in |- *; intros z z' H1 H2; - generalize (refl_equal (interp_term e (fusion_cancel t (t2 + t4)%term))); - pattern (fusion_cancel t (t2 + t4)%term) at 2 3 in |- *; - case (fusion_cancel t (t2 + t4)%term); simpl in |- *; - auto; intro k; elim (fusion_cancel_stable t); simpl in |- *. + 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. @@ -2250,23 +2227,23 @@ Definition negate_contradict_inv (t i1 i2 : nat) (h : hyps) := Theorem negate_contradict_valid : forall i j : nat, valid_hyps (negate_contradict i j). Proof. - unfold valid_hyps, negate_contradict in |- *; intros i j ep e l H; + 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; auto; case (nth_hyps j l); auto; intros t3 t4; case t3; auto; intros z'; - auto; simpl in |- *; intros H1 H2; Simplify. + auto; simpl; intros H1 H2; 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 in |- *; intros t i j ep e l H; + 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; auto; case (nth_hyps j l); auto; intros t3 t4; case t3; auto; intros z'; - auto; simpl in |- *; intros H1 H2; Simplify; + auto; simpl; intros H1 H2; Simplify; [ rewrite <- scalar_norm_stable in H2; simpl in *; elim (mult_integral (interp_term e t4) (-(1))); intuition; @@ -2333,9 +2310,9 @@ Definition sum (k1 k2 : int) (trace : list t_fusion) Theorem sum_valid : forall (k1 k2 : int) (t : list t_fusion), valid2 (sum k1 k2 t). Proof. - unfold valid2 in |- *; intros k1 k2 t ep e p1 p2; unfold sum in |- *; - Simplify; simpl in |- *; auto; try elim (fusion_stable t); - simpl in |- *; intros; + 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 @@ -2367,10 +2344,10 @@ Definition exact_divide (k : int) (body : term) (t : nat) Theorem exact_divide_valid : forall (k : int) (t : term) (n : nat), valid1 (exact_divide k t n). Proof. - unfold valid1, exact_divide in |- *; intros k1 k2 t ep e p1; + unfold valid1, exact_divide; intros k1 k2 t ep e p1; Simplify; simpl; auto; subst; rewrite <- scalar_norm_stable; simpl; intros; - [ destruct (mult_integral _ _ (sym_eq H0)); intuition + [ destruct (mult_integral _ _ (eq_sym H0)); intuition | contradict H0; rewrite <- H0, mult_0_l; auto ]. Qed. @@ -2397,9 +2374,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 in |- *; intros k1 k2 body t ep e p1; + 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 in |- *. + elim (scalar_norm_add_stable t e); simpl. intro H2; apply mult_le_approx with (3 := H2); assumption. Qed. @@ -2421,9 +2398,9 @@ Definition merge_eq (t : nat) (prop1 prop2 : proposition) := Theorem merge_eq_valid : forall n : nat, valid2 (merge_eq n). Proof. - unfold valid2, merge_eq in |- *; intros n ep e p1 p2; Simplify; simpl in |- *; - auto; elim (scalar_norm_stable n e); simpl in |- *; - intros; symmetry in |- *; apply OMEGA8 with (2 := H0); + 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 ]. Qed. @@ -2440,8 +2417,8 @@ 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 in |- *; intros; - generalize (nth_valid ep e i lp); Simplify; simpl in |- *; + unfold valid_hyps, constant_nul; intros; + generalize (nth_valid ep e i lp); Simplify; simpl; intro H1; absurd (0 = 0); intuition. Qed. @@ -2462,8 +2439,8 @@ Definition state (m : int) (s : step) (prop1 prop2 : proposition) := Theorem state_valid : forall (m : int) (s : step), valid2 (state m s). Proof. - unfold valid2 in |- *; intros m s ep e p1 p2; unfold state in |- *; Simplify; - simpl in |- *; auto; elim (t_rewrite_stable s e); simpl in |- *; + unfold valid2; intros m s ep e p1 p2; unfold state; Simplify; + simpl; auto; elim (t_rewrite_stable s e); simpl; intros H1 H2; elim H1. now rewrite H2, plus_opp_l, plus_0_l, mult_0_l. Qed. @@ -2490,18 +2467,18 @@ Theorem split_ineq_valid : valid_list_hyps f1 -> valid_list_hyps f2 -> valid_list_hyps (split_ineq i t f1 f2). Proof. - unfold valid_list_hyps, split_ineq in |- *; intros i t f1 f2 H1 H2 ep e lp H; + 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 in |- *; auto; intros t1 t2; case t1; simpl in |- *; - auto; intros z; simpl in |- *; auto; intro H3. + 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 in |- *; elim (add_norm_stable t); - simpl in |- *; auto - | intro H4; right; apply H2; simpl in |- *; elim (scalar_norm_add_stable t); - simpl in |- *; auto - | generalize H3; unfold not in |- *; intros E1 E2; apply E1; - symmetry in |- *; trivial ]. + [ 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. @@ -2534,47 +2511,47 @@ Fixpoint execute_omega (t : t_omega) (l : hyps) {struct t} : lhyps := Theorem omega_valid : forall t : t_omega, valid_list_hyps (execute_omega t). Proof. - simple induction t; simpl in |- *; - [ unfold valid_list_hyps in |- *; simpl in |- *; intros; left; + simple induction t; simpl; + [ unfold valid_list_hyps; simpl; intros; left; apply (constant_not_nul_valid n ep e lp H) - | unfold valid_list_hyps in |- *; simpl in |- *; intros; left; + | unfold valid_list_hyps; simpl; intros; left; apply (constant_neg_valid n ep e lp H) - | unfold valid_list_hyps, valid_hyps in |- *; + | 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 in |- *; simpl in |- *; intros; left; + | unfold valid_list_hyps; simpl; intros; left; apply (not_exact_divide_valid i i0 t0 n n0 ep e lp H) - | unfold valid_list_hyps, valid_hyps in |- *; + | 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 in |- *; + | 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 in |- *; simpl in |- *; intros; left; + | unfold valid_list_hyps; simpl; intros; left; apply (contradiction_valid n n0 n1 ep e lp H) - | unfold valid_list_hyps, valid_hyps in |- *; + | 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 in |- *; simpl in |- *; + | 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 in |- *; simpl in |- *; intros i ep e lp H; left; + | 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 in |- *; simpl in |- *; intros i j ep e lp H; left; + | 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 in |- *; simpl in |- *; intros n 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 in |- *; + | 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) ]. Qed. @@ -2596,9 +2573,9 @@ Definition move_right (s : step) (p : proposition) := Theorem move_right_valid : forall s : step, valid1 (move_right s). Proof. - unfold valid1, move_right in |- *; intros s ep e p; Simplify; simpl in |- *; - elim (t_rewrite_stable s e); simpl in |- *; - [ symmetry in |- *; apply egal_left; assumption + 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 @@ -2611,7 +2588,7 @@ Definition do_normalize (i : nat) (s : step) := apply_oper_1 i (move_right s). Theorem do_normalize_valid : forall (i : nat) (s : step), valid_hyps (do_normalize i s). Proof. - intros; unfold do_normalize in |- *; apply apply_oper_1_valid; + intros; unfold do_normalize; apply apply_oper_1_valid; apply move_right_valid. Qed. @@ -2625,7 +2602,7 @@ 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 in |- *; unfold valid_hyps in |- *; + 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 ]. @@ -2654,8 +2631,8 @@ Theorem append_goal : interp_list_goal ep e (l1 ++ l2). Proof. intros ep e; simple induction l1; - [ simpl in |- *; intros l2 (H1, H2); assumption - | simpl in |- *; intros h1 t1 HR l2 ((H1, H2), H3); split; auto ]. + [ simpl; intros l2 (H1, H2); assumption + | simpl; intros h1 t1 HR l2 ((H1, H2), H3); split; auto ]. Qed. (* A simple decidability checker : if the proposition belongs to the @@ -2684,11 +2661,11 @@ 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 in |- *; intros; + simple induction p; simpl; intros; [ apply dec_eq | apply dec_le | left; auto - | right; unfold not in |- *; auto + | right; unfold not; auto | apply dec_not; auto | apply dec_ge | apply dec_gt @@ -2724,7 +2701,7 @@ 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 in |- *; simpl in |- *; + simple induction l; unfold interp_full; simpl; [ auto | intros a l1 H1 c H2 H3; apply H1; auto ]. Qed. @@ -2744,12 +2721,12 @@ 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 in |- *; - pattern (decidability c) in |- *; apply bool_eq_ind; - [ simpl in |- *; intros H H1; apply interp_full_false; intros H2; + 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 in |- *; intro H3; apply hyps_to_goal with (2 := H2); + | 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 ]. @@ -2813,7 +2790,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 in |- *; [ auto | intros; elim H1; intro H2; auto ]. + simple induction l; simpl; [ auto | intros; elim H1; intro H2; auto ]. Qed. Hint Resolve map_cons_val append_valid decidable_correct. @@ -2822,43 +2799,43 @@ Theorem destructure_hyps_valid : forall n : nat, valid_list_hyps (destructure_hyps n). Proof. simple induction n; - [ unfold valid_list_hyps in |- *; simpl in |- *; auto - | unfold valid_list_hyps at 2 in |- *; intros n1 H ep e lp; case lp; - [ simpl in |- *; auto + [ 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 in |- *; intros; apply map_cons_val; simpl in |- *; elim H0; + (simpl; intros; apply map_cons_val; simpl; elim H0; auto); [ intro p'; case p'; try - (simpl in |- *; intros; apply map_cons_val; simpl in |- *; elim H0; + (simpl; intros; apply map_cons_val; simpl; elim H0; auto); - [ simpl in |- *; intros p1 (H1, H2); - pattern (decidability p1) in |- *; apply bool_eq_ind; + [ simpl; intros p1 (H1, H2); + pattern (decidability p1); apply bool_eq_ind; intro H3; - [ apply H; simpl in |- *; split; + [ apply H; simpl; split; [ apply not_not; auto | assumption ] | auto ] - | simpl in |- *; intros p1 p2 (H1, H2); apply H; simpl in |- *; + | simpl; intros p1 p2 (H1, H2); apply H; simpl; elim not_or with (1 := H1); auto - | simpl in |- *; intros p1 p2 (H1, H2); - pattern (decidability p1) in |- *; apply bool_eq_ind; + | 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 in |- *; auto - | intro; right; apply H; simpl in |- *; auto + [ intro; left; apply H; simpl; auto + | intro; right; apply H; simpl; auto | auto ] | auto ] ] - | simpl in |- *; intros p1 p2 (H1, H2); apply append_valid; - (elim H1; intro H3; simpl in |- *; [ left | right ]); - apply H; simpl in |- *; auto - | simpl in |- *; intros; apply H; simpl in |- *; tauto - | simpl in |- *; intros p1 p2 (H1, H2); - pattern (decidability p1) in |- *; apply bool_eq_ind; + | 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 in |- *; apply H; simpl in |- *; auto - | intro H4; right; simpl in |- *; apply H; simpl in |- *; auto + [ intro H4; left; simpl; apply H; simpl; auto + | intro H4; right; simpl; apply H; simpl; auto | auto ] | auto ] ] ] ]. Qed. @@ -2881,8 +2858,8 @@ Theorem p_apply_left_stable : forall f : proposition -> proposition, prop_stable f -> prop_stable (p_apply_left f). Proof. - unfold prop_stable in |- *; intros f H ep e p; split; - (case p; simpl in |- *; auto; intros p1; elim (H ep e p1); tauto). + unfold prop_stable; intros f H ep e p; split; + (case p; simpl; auto; intros p1; elim (H ep e p1); tauto). Qed. Definition p_apply_right (f : proposition -> proposition) @@ -2899,8 +2876,8 @@ Theorem p_apply_right_stable : forall f : proposition -> proposition, prop_stable f -> prop_stable (p_apply_right f). Proof. - unfold prop_stable in |- *; intros f H ep e p; split; - (case p; simpl in |- *; auto; + 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 @@ -2923,42 +2900,42 @@ Theorem p_invert_stable : forall f : proposition -> proposition, prop_stable f -> prop_stable (p_invert f). Proof. - unfold prop_stable in |- *; intros f H ep e p; split; - (case p; simpl in |- *; auto; - [ intros t1 t2; elim (H ep e (NeqTerm t1 t2)); simpl in |- *; + 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 in |- *; tauto - | intros t1 t2; elim (H ep e (GtTerm t1 t2)); simpl in |- *; + 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 in |- *; rewrite le_lt_iff, <- gt_lt_iff; tauto - | intros t1 t2; elim (H ep e (LtTerm t1 t2)); simpl in |- *; + 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 in |- *; rewrite ge_le_iff, le_lt_iff; tauto - | intros t1 t2; elim (H ep e (LeqTerm t1 t2)); simpl in |- *; + 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 in |- *; repeat rewrite le_lt_iff; + unfold decidable; repeat rewrite le_lt_iff; repeat rewrite gt_lt_iff; tauto - | intros t1 t2; elim (H ep e (GeqTerm t1 t2)); simpl in |- *; + | intros t1 t2; elim (H ep e (GeqTerm t1 t2)); simpl; generalize (dec_lt (interp_term e t1) (interp_term e t2)); - unfold decidable in |- *; repeat rewrite ge_le_iff; + unfold decidable; repeat rewrite ge_le_iff; repeat rewrite le_lt_iff; tauto - | intros t1 t2; elim (H ep e (EqTerm t1 t2)); simpl in |- *; + | 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 ]). Qed. Theorem move_right_stable : forall s : step, prop_stable (move_right s). Proof. - unfold move_right, prop_stable in |- *; intros s ep e p; split; - [ Simplify; simpl in |- *; elim (t_rewrite_stable s e); simpl in |- *; - [ symmetry in |- *; apply egal_left; assumption + 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 in |- *; intros; auto; generalize H; elim (t_rewrite_stable s); - simpl in |- *; intro H1; + | case p; simpl; intros; auto; generalize H; elim (t_rewrite_stable s); + simpl; intro H1; [ rewrite (plus_0_r_reverse (interp_term e t0)); rewrite H1; rewrite plus_permute; rewrite plus_opp_r; rewrite plus_0_r; trivial @@ -2969,7 +2946,7 @@ Proof. rewrite plus_opp_r; assumption | rewrite gt_lt_iff; apply lt_left_inv; assumption | apply lt_left_inv; assumption - | unfold not in |- *; intro H2; apply H1; + | unfold not; intro H2; apply H1; rewrite H2; rewrite plus_opp_r; trivial ] ]. Qed. @@ -2985,12 +2962,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 in |- *; + 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 in |- *; simpl in |- *; intros; split; auto ]. + | unfold prop_stable; simpl; intros; split; auto ]. Qed. Fixpoint normalize_hyps (l : list h_step) (lh : hyps) {struct l} : hyps := @@ -3002,11 +2979,11 @@ 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 in |- *; simpl in |- *; + 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 in |- *; intros ep1 e1 p1 H2; + [ unfold valid1; intros ep1 e1 p1 H2; elim (p_rewrite_stable s ep1 e1 p1); auto | assumption ] ]. Qed. @@ -3073,21 +3050,21 @@ Theorem extract_valid : forall s : list direction, valid1 (extract_hyp_pos s) /\ co_valid1 (extract_hyp_neg s). Proof. - unfold valid1, co_valid1 in |- *; simple induction s; + unfold valid1, co_valid1; simple induction s; [ split; - [ simpl in |- *; auto - | intros ep e p1; case p1; simpl in |- *; auto; intro p; - pattern (decidability p) in |- *; apply bool_eq_ind; + [ 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 in |- *; tauto - | simpl in |- *; auto ] ] + 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 in |- *; intros; + case p; auto; simpl; intros; (apply H1; tauto) || (apply H2; tauto) || - (pattern (decidability p0) in |- *; apply bool_eq_ind; + (pattern (decidability p0); apply bool_eq_ind; [ intro H3; generalize (decidable_correct ep e p0 H3); - unfold decidable in |- *; intro H4; apply H1; + unfold decidable; intro H4; apply H1; tauto | intro; tauto ]) ]. Qed. @@ -3117,29 +3094,29 @@ Fixpoint decompose_solve (s : e_step) (h : hyps) {struct s} : lhyps := Theorem decompose_solve_valid : forall s : e_step, valid_list_goal (decompose_solve s). Proof. - intro s; apply goal_valid; unfold valid_list_hyps in |- *; elim s; - simpl in |- *; intros; + 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 in |- *; auto; - [ intro p; case p; simpl in |- *; auto; intros p1 p2 H2; - pattern (decidability p1) in |- *; apply bool_eq_ind; + [ 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 in |- *; tauto - | left; apply H; simpl in |- *; tauto ] - | simpl in |- *; auto ] - | intros p1 p2 H2; apply append_valid; simpl in |- *; elim H2; - [ intros H3; left; apply H; simpl in |- *; auto - | intros H3; right; apply H0; simpl in |- *; auto ] + [ 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) in |- *; apply bool_eq_ind; + 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 in |- *; tauto - | left; apply H; simpl in |- *; tauto ] - | simpl in |- *; auto ] ] + [ 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 in |- *; split; + | 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) ]. @@ -3160,11 +3137,11 @@ Fixpoint reduce_lhyps (lp : lhyps) : lhyps := Theorem reduce_lhyps_valid : valid_lhyps reduce_lhyps. Proof. - unfold valid_lhyps in |- *; intros ep e lp; elim lp; - [ simpl in |- *; auto + unfold valid_lhyps; intros ep e lp; elim lp; + [ simpl; auto | intros a l HR; elim a; - [ simpl in |- *; tauto - | intros a1 l1; case l1; case a1; simpl in |- *; try tauto ] ]. + [ simpl; tauto + | intros a1 l1; case l1; case a1; simpl; try tauto ] ]. Qed. Theorem do_reduce_lhyps : @@ -3184,13 +3161,13 @@ Definition do_concl_to_hyp : interp_goal envp env (concl_to_hyp c :: l) -> interp_goal_concl c envp env l. Proof. - simpl in |- *; intros envp env c l; induction l as [| a l Hrecl]; - [ simpl in |- *; unfold concl_to_hyp in |- *; - pattern (decidability c) in |- *; apply bool_eq_ind; + 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 in |- *; simpl in |- *; tauto - | simpl in |- *; intros H1 H2; elim H2; trivial ] - | simpl in |- *; tauto ]. + unfold decidable; simpl; tauto + | simpl; intros H1 H2; elim H2; trivial ] + | simpl; tauto ]. Qed. Definition omega_tactic (t1 : e_step) (t2 : list h_step) @@ -3203,7 +3180,7 @@ Theorem do_omega : interp_list_goal envp env (omega_tactic t1 t2 c l) -> interp_goal_concl c envp env l. Proof. - unfold omega_tactic in |- *; intros; apply do_concl_to_hyp; + unfold omega_tactic; intros; apply do_concl_to_hyp; apply (normalize_hyps_goal t2); apply (decompose_solve_valid t1); apply do_reduce_lhyps; assumption. Qed. |