From 7509f5c8eab84fda5a9029329c6b70758259765f Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Wed, 17 May 2017 13:39:59 +0200 Subject: ROmega : merge O_CONSTANT* into a single O_BAD_CONSTANT --- plugins/romega/ReflOmegaCore.v | 71 +++++---------------- plugins/romega/const_omega.ml | 4 +- plugins/romega/const_omega.mli | 4 +- plugins/romega/refl_omega.ml | 136 ++++++++++++++++++----------------------- 4 files changed, 77 insertions(+), 138 deletions(-) (limited to 'plugins/romega') diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index 0476c385c..057752271 100644 --- a/plugins/romega/ReflOmegaCore.v +++ b/plugins/romega/ReflOmegaCore.v @@ -1454,20 +1454,17 @@ Qed. [0<>...] or inequations [0<=...]. First, the final steps leading to a contradiction: - - [O_CONSTANT_NOT_NUL i] : - equation i is [0=k] with a non-nul constant [k]. - - [O_CONSTANT_NUL i] : disequation i is [0<>0]. - - [O_CONSTANT_NEG i] : - inequation i is [0<=k] with a negative constant [k]. + - [O_BAD_CONSTANT i] : hypothesis i has a constant body + and this constant is not compatible with the kind of i. - [O_CONTRADICTION i j] : inequations i and j have a sum which is a negative constant. - Shortcut for [(O_SUM 1 i 1 j (O_CONSTANT_NEG 0))]. + Shortcut for [(O_SUM 1 i 1 j (O_BAD_CONSTANT 0))]. - [O_NEGATE_CONTRADICT i j] : equation i and disequation j (or vice-versa) have the same body. - Shortcut for [(O_SUM 1 i (-1) j (O_CONSTANT_NUL 0))]. + Shortcut for [(O_SUM 1 i (-1) j (O_BAD_CONSTANT 0))]. - [O_NEGATE_CONTRADICT_INV i j] : equation i and disequation j (or vice-versa) have opposite bodies. - Shortcut for [(O_SUM 1 i 1 j (O_CONSTANT_NUL 0))]. + Shortcut for [(O_SUM 1 i 1 j (O_BAD_CONSTANT 0))]. - [O_NOT_EXACT_DIVIDE i k1 k2 t] : equation i has a body equivalent to [k1*t+k2] with [0 t_omega - | O_CONSTANT_NUL : idx -> t_omega - | O_CONSTANT_NEG : idx -> t_omega + | O_BAD_CONSTANT : idx -> t_omega | O_CONTRADICTION : idx -> idx -> t_omega | O_NEGATE_CONTRADICT : idx -> idx -> t_omega | O_NEGATE_CONTRADICT_INV : idx -> idx -> t_omega @@ -1512,51 +1507,21 @@ Inductive t_omega : Set := (** First, the final steps, leading to a contradiction *) -(** [O_CONSTANT_NOT_NUL] *) +(** [O_BAD_CONSTANT] *) -Definition constant_not_nul (i : nat) (h : hyps) := +Definition bad_constant (i : nat) (h : hyps) := match nth_hyps i h with - | EqTerm (Tint Nul) (Tint n) => - if beq n Nul then h else absurd + | EqTerm (Tint Nul) (Tint n) => if beq n Nul then h else absurd + | NeqTerm (Tint Nul) (Tint n) => if beq n Nul then absurd else h + | LeqTerm (Tint Nul) (Tint n) => if bgt Nul n then absurd else h | _ => h end. -Theorem constant_not_nul_valid : - forall i : nat, valid_hyps (constant_not_nul i). +Theorem bad_constant_valid i : valid_hyps (bad_constant i). Proof. - unfold valid_hyps, constant_not_nul; intros i ep e lp H. + unfold valid_hyps, bad_constant; intros ep e lp H. generalize (nth_valid ep e i lp H); Simplify. -Qed. - -(** [O_CONSTANT_NUL] *) - -Definition constant_nul (i : nat) (h : hyps) := - match nth_hyps i h with - | NeqTerm (Tint Null) (Tint Null') => - if beq Null Null' then absurd else h - | _ => h - end. - -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; intuition. -Qed. - -(** [O_CONSTANT_NEG] *) - -Definition constant_neg (i : nat) (h : hyps) := - match nth_hyps i h with - | LeqTerm (Tint Nul) (Tint Neg) => - if bgt Nul Neg then absurd else h - | _ => h - end. - -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 *; rewrite le_lt_iff; intuition. + rewrite gt_lt_iff in *. rewrite le_lt_iff. intuition. Qed. (** [O_CONTRADICTION] *) @@ -1889,9 +1854,7 @@ Qed. Fixpoint execute_omega (t : t_omega) (l : hyps) {struct t} : lhyps := match t with - | O_CONSTANT_NOT_NUL n => singleton (constant_not_nul n l) - | O_CONSTANT_NUL i => singleton (constant_nul i l) - | O_CONSTANT_NEG n => singleton (constant_neg n l) + | O_BAD_CONSTANT i => singleton (bad_constant i l) | O_CONTRADICTION i j => singleton (contradiction i j l) | O_NEGATE_CONTRADICT i j => singleton (negate_contradict i j l) | O_NEGATE_CONTRADICT_INV i j => @@ -1915,9 +1878,7 @@ 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; unfold valid_list_hyps, valid_hyps; simpl. - - intros; left; now apply constant_not_nul_valid. - - intros; left; now apply constant_nul_valid. - - intros; left; now apply constant_neg_valid. + - intros; left; now apply bad_constant_valid. - intros; left; now apply contradiction_valid. - intros; left; now apply negate_contradict_valid. - intros; left; now apply negate_contradict_inv_valid. diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 4fd224e2b..fa92903ba 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -101,8 +101,7 @@ let coq_p_and = lazy (constant "Tand") let coq_p_imp = lazy (constant "Timp") let coq_p_prop = lazy (constant "Tprop") -let coq_s_constant_not_nul = lazy (constant "O_CONSTANT_NOT_NUL") -let coq_s_constant_neg = lazy (constant "O_CONSTANT_NEG") +let coq_s_bad_constant = lazy (constant "O_BAD_CONSTANT") let coq_s_div_approx = lazy (constant "O_DIV_APPROX") let coq_s_not_exact_divide = lazy (constant "O_NOT_EXACT_DIVIDE") let coq_s_exact_divide = lazy (constant "O_EXACT_DIVIDE") @@ -111,7 +110,6 @@ let coq_s_state = lazy (constant "O_STATE") let coq_s_contradiction = lazy (constant "O_CONTRADICTION") let coq_s_merge_eq = lazy (constant "O_MERGE_EQ") let coq_s_split_ineq =lazy (constant "O_SPLIT_INEQ") -let coq_s_constant_nul =lazy (constant "O_CONSTANT_NUL") let coq_s_negate_contradict =lazy (constant "O_NEGATE_CONTRADICT") let coq_s_negate_contradict_inv =lazy (constant "O_NEGATE_CONTRADICT_INV") diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli index 787ace603..ba8b097fe 100644 --- a/plugins/romega/const_omega.mli +++ b/plugins/romega/const_omega.mli @@ -42,8 +42,7 @@ val coq_p_and : Term.constr lazy_t val coq_p_imp : Term.constr lazy_t val coq_p_prop : Term.constr lazy_t -val coq_s_constant_not_nul : Term.constr lazy_t -val coq_s_constant_neg : Term.constr lazy_t +val coq_s_bad_constant : Term.constr lazy_t val coq_s_div_approx : Term.constr lazy_t val coq_s_not_exact_divide : Term.constr lazy_t val coq_s_exact_divide : Term.constr lazy_t @@ -52,7 +51,6 @@ val coq_s_state : Term.constr lazy_t val coq_s_contradiction : Term.constr lazy_t val coq_s_merge_eq : Term.constr lazy_t val coq_s_split_ineq : Term.constr lazy_t -val coq_s_constant_nul : Term.constr lazy_t val coq_s_negate_contradict : Term.constr lazy_t val coq_s_negate_contradict_inv : Term.constr lazy_t diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 7a48b9788..45b141f92 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -855,87 +855,69 @@ let mk_direction_list l = (* \section{Rejouer l'historique} *) -let get_hyp env_hyp i = +let hyp_idx env_hyp i = let rec loop count = function | [] -> failwith (Printf.sprintf "get_hyp %d" i) - | CCEqua i' :: _ when Int.equal i i' -> count + | CCEqua i' :: _ when Int.equal i i' -> mk_nat count | _ :: l -> loop (succ count) l in loop 0 env_hyp -let replay_history env env_hyp = - let rec loop env_hyp t = - match t with - | CONTRADICTION (e1,e2) :: l -> - mkApp (Lazy.force coq_s_contradiction, - [| mk_nat (get_hyp env_hyp e1.id); - mk_nat (get_hyp env_hyp e2.id) |]) - | DIVIDE_AND_APPROX (e1,e2,k,d) :: l -> - mkApp (Lazy.force coq_s_div_approx, - [| mk_nat (get_hyp env_hyp e1.id); Z.mk k; Z.mk d; - reified_of_omega env e2.body e2.constant; - loop env_hyp l |]) - | NOT_EXACT_DIVIDE (e1,k) :: l -> - let e2_constant = floor_div e1.constant k in - let d = e1.constant - e2_constant * k in - let e2_body = map_eq_linear (fun c -> c / k) e1.body in - mkApp (Lazy.force coq_s_not_exact_divide, - [| mk_nat (get_hyp env_hyp e1.id); Z.mk k; Z.mk d; - reified_of_omega env e2_body e2_constant |]) - | EXACT_DIVIDE (e1,k) :: l -> - let e2_body = map_eq_linear (fun c -> c / k) e1.body in - let e2_constant = floor_div e1.constant k in - mkApp (Lazy.force coq_s_exact_divide, - [| mk_nat (get_hyp env_hyp e1.id); Z.mk k; - reified_of_omega env e2_body e2_constant; - loop env_hyp l |]) - | (MERGE_EQ(e3,e1,e2)) :: l -> - let n1 = get_hyp env_hyp e1.id and n2 = get_hyp env_hyp e2 in - mkApp (Lazy.force coq_s_merge_eq, - [| mk_nat n1; mk_nat n2; - loop (CCEqua e3:: env_hyp) l |]) - | SUM(e3,(k1,e1),(k2,e2)) :: l -> - let n1 = get_hyp env_hyp e1.id - and n2 = get_hyp env_hyp e2.id in - mkApp (Lazy.force coq_s_sum, - [| Z.mk k1; mk_nat n1; Z.mk k2; - mk_nat n2; (loop (CCEqua e3 :: env_hyp) l) |]) - | CONSTANT_NOT_NUL(e,k) :: l -> - mkApp (Lazy.force coq_s_constant_not_nul, - [| mk_nat (get_hyp env_hyp e) |]) - | CONSTANT_NEG(e,k) :: l -> - mkApp (Lazy.force coq_s_constant_neg, - [| mk_nat (get_hyp env_hyp e) |]) - | STATE {st_new_eq=new_eq; st_def =def; - st_orig=orig; st_coef=m; - st_var=sigma } :: l -> - let n1 = get_hyp env_hyp orig.id - and n2 = get_hyp env_hyp def.id in - mkApp (Lazy.force coq_s_state, - [| Z.mk m; mk_nat n1; mk_nat n2; - loop (CCEqua new_eq.id :: env_hyp) l |]) - | HYP _ :: l -> loop env_hyp l - | CONSTANT_NUL e :: l -> - mkApp (Lazy.force coq_s_constant_nul, - [| mk_nat (get_hyp env_hyp e) |]) - | NEGATE_CONTRADICT(e1,e2,true) :: l -> - mkApp (Lazy.force coq_s_negate_contradict, - [| mk_nat (get_hyp env_hyp e1.id); - mk_nat (get_hyp env_hyp e2.id) |]) - | NEGATE_CONTRADICT(e1,e2,false) :: l -> - mkApp (Lazy.force coq_s_negate_contradict_inv, - [| mk_nat (get_hyp env_hyp e1.id); - mk_nat (get_hyp env_hyp e2.id) |]) - | SPLIT_INEQ(e,(e1,l1),(e2,l2)) :: l -> - let i = get_hyp env_hyp e.id in - let r1 = loop (CCEqua e1 :: env_hyp) l1 in - let r2 = loop (CCEqua e2 :: env_hyp) l2 in - mkApp (Lazy.force coq_s_split_ineq, - [| mk_nat i; r1 ; r2 |]) - | (FORGET_C _ | FORGET _ | FORGET_I _) :: l -> - loop env_hyp l - | (WEAKEN _ ) :: l -> failwith "not_treated" - | [] -> failwith "no contradiction" - in loop env_hyp +let rec reify_trace env env_hyp = function + | CONSTANT_NOT_NUL(e,_) :: [] + | CONSTANT_NEG(e,_) :: [] + | CONSTANT_NUL e :: [] -> + mkApp (Lazy.force coq_s_bad_constant,[| hyp_idx env_hyp e |]) + | NEGATE_CONTRADICT(e1,e2,direct) :: [] -> + let c = if direct then coq_s_negate_contradict + else coq_s_negate_contradict_inv + in + mkApp (Lazy.force c, [| hyp_idx env_hyp e1.id; hyp_idx env_hyp e2.id |]) + | CONTRADICTION (e1,e2) :: [] -> + mkApp (Lazy.force coq_s_contradiction, + [| hyp_idx env_hyp e1.id; hyp_idx env_hyp e2.id |]) + | NOT_EXACT_DIVIDE (e1,k) :: [] -> + let e2_constant = floor_div e1.constant k in + let d = e1.constant - e2_constant * k in + let e2_body = map_eq_linear (fun c -> c / k) e1.body in + mkApp (Lazy.force coq_s_not_exact_divide, + [| hyp_idx env_hyp e1.id; Z.mk k; Z.mk d; + reified_of_omega env e2_body e2_constant |]) + | DIVIDE_AND_APPROX (e1,e2,k,d) :: l -> + mkApp (Lazy.force coq_s_div_approx, + [| hyp_idx env_hyp e1.id; Z.mk k; Z.mk d; + reified_of_omega env e2.body e2.constant; + reify_trace env env_hyp l |]) + | EXACT_DIVIDE (e1,k) :: l -> + let e2_body = map_eq_linear (fun c -> c / k) e1.body in + let e2_constant = floor_div e1.constant k in + mkApp (Lazy.force coq_s_exact_divide, + [| hyp_idx env_hyp e1.id; Z.mk k; + reified_of_omega env e2_body e2_constant; + reify_trace env env_hyp l |]) + | MERGE_EQ(e3,e1,e2) :: l -> + mkApp (Lazy.force coq_s_merge_eq, + [| hyp_idx env_hyp e1.id; hyp_idx env_hyp e2; + reify_trace env (CCEqua e3:: env_hyp) l |]) + | SUM(e3,(k1,e1),(k2,e2)) :: l -> + mkApp (Lazy.force coq_s_sum, + [| Z.mk k1; hyp_idx env_hyp e1.id; + Z.mk k2; hyp_idx env_hyp e2.id; + reify_trace env (CCEqua e3 :: env_hyp) l |]) + | STATE {st_new_eq=new_eq; st_def =def; + st_orig=orig; st_coef=m; + st_var=sigma } :: l -> + mkApp (Lazy.force coq_s_state, + [| Z.mk m; hyp_idx env_hyp orig.id; hyp_idx env_hyp def.id; + reify_trace env (CCEqua new_eq.id :: env_hyp) l |]) + | HYP _ :: l -> reify_trace env env_hyp l + | SPLIT_INEQ(e,(e1,l1),(e2,l2)) :: _ -> + let r1 = reify_trace env (CCEqua e1 :: env_hyp) l1 in + let r2 = reify_trace env (CCEqua e2 :: env_hyp) l2 in + mkApp (Lazy.force coq_s_split_ineq, + [| hyp_idx env_hyp e.id; r1 ; r2 |]) + | (FORGET_C _ | FORGET _ | FORGET_I _) :: l -> reify_trace env env_hyp l + | WEAKEN _ :: l -> failwith "not_treated" + | _ -> failwith "bad history" let rec decompose_tree env ctxt = function Tree(i,left,right) -> @@ -954,7 +936,7 @@ let rec decompose_tree env ctxt = function | Leaf s -> decompose_tree_hyps s.s_trace env ctxt (IntSet.elements s.s_equa_deps) and decompose_tree_hyps trace env ctxt = function - [] -> app coq_e_solve [| replay_history env ctxt trace |] + [] -> app coq_e_solve [| reify_trace env ctxt trace |] | (i::l) -> let equation = try IntHtbl.find env.equations i -- cgit v1.2.3