diff options
author | Frédéric Besson <frederic.besson@inria.fr> | 2016-09-08 14:19:02 +0200 |
---|---|---|
committer | Frédéric Besson <frederic.besson@inria.fr> | 2016-09-08 14:19:02 +0200 |
commit | 9f56baf7bb78a520dc2e7f5f0f94091ebf86dcaf (patch) | |
tree | 692212e73e902b4aacf36f23ae5b375016979158 | |
parent | 76a8288c37e68fd8559f903af60abf8c3f87c007 (diff) |
Fix Bug #5073 : regression of micromega plugin
The computed proof term is now more explicit exact (__arith P1 ... Pn X1 ... Xm)
instead of apply (__arith P1 ... Pn) which unification could fail.
-rw-r--r-- | plugins/micromega/coq_micromega.ml | 24 | ||||
-rw-r--r-- | plugins/micromega/mutils.ml | 12 | ||||
-rw-r--r-- | test-suite/micromega/zomicron.v | 7 |
3 files changed, 22 insertions, 21 deletions
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index db8cbf231..23d37c273 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -961,7 +961,7 @@ struct let (env,n) = _add l ( n+1) v in (e::env,n) in let (env, n) = _add env 1 v in - (env, CamlToCoq.idx n) + (env, CamlToCoq.positive n) let get_rank env v = @@ -1986,21 +1986,27 @@ let micromega_gen micromega_order_change spec res' (Term.mkApp(Lazy.force coq_list, [|spec.proof_typ|])) env' ff_arith ] in + let goal_props = List.rev (prop_env_of_formula ff') in + + let goal_vars = List.map (fun (_,i) -> List.nth env (i-1)) vars in + + let arith_args = goal_props @ goal_vars in + let kill_arith = Tacticals.New.tclTHEN (Tactics.keep []) ((*Tactics.tclABSTRACT None*) (Tacticals.New.tclTHEN tac_arith tac)) in - Tacticals.New.tclTHEN - (Tactics.forward true (Some (Some kill_arith)) (ipat_of_name goal_name) arith_goal) - (Tacticals.New.tclTHENLIST + Tacticals.New.tclTHENS + (Tactics.forward true (Some None) (ipat_of_name goal_name) arith_goal) + [ + kill_arith; + (Tacticals.New.tclTHENLIST [(Tactics.generalize (List.map Term.mkVar ids)); - Tactics.unfold_constr coq_not_gl_ref; - (Tactics.apply (Term.applist (Term.mkVar goal_name,List.rev (prop_env_of_formula ff')))) - ]) - (*Tacticals.New.tclTRY(Tactics.apply_with_bindings_gen true false - [None,(Loc.ghost,((Term.mkVar goal_name) ,Misctypes.NoBindings))]*) + Tactics.exact_check (Term.applist (Term.mkVar goal_name, arith_args)) + ] ) + ] with | ParseError -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment") | Mfourier.TimeOut -> Tacticals.New.tclFAIL 0 (Pp.str "Timeout") diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml index c13e8fc28..b4c6d032b 100644 --- a/plugins/micromega/mutils.ml +++ b/plugins/micromega/mutils.ml @@ -294,18 +294,6 @@ struct else XO (index (n lsr 1)) - let idx n = - (*a.k.a path_of_int *) - (* returns the list of digits of n in reverse order with initial 1 removed *) - let rec digits_of_int n = - if Int.equal n 1 then [] - else (Int.equal (n mod 2) 1)::(digits_of_int (n lsr 1)) - in - List.fold_right - (fun b c -> (if b then XI c else XO c)) - (List.rev (digits_of_int n)) - (XH) - let z x = match compare x 0 with | 0 -> Z0 diff --git a/test-suite/micromega/zomicron.v b/test-suite/micromega/zomicron.v index 3f4c2407d..239bc6936 100644 --- a/test-suite/micromega/zomicron.v +++ b/test-suite/micromega/zomicron.v @@ -82,4 +82,11 @@ Proof. lia. Qed. +(* Bug 5073 *) +Lemma opp_eq_0_iff a : -a = 0 <-> a = 0. +Proof. + lia. +Qed. + + |